Maude system

The Maude system is an implementation of rewriting logic developed at SRI International. It is similar in its general approach to Joseph Goguen's OBJ3 implementation of equational logic, but based on rewriting logic rather than order-sorted equational logic, and with a heavy emphasis on powerful metaprogramming based on reflection.

Maude is free software, and tutorials are available online.

Elementary example

Maude modules (rewrite theories) consist of a term-language plus sets of equations and rewrite-rules. Terms in a rewrite theory are constructed using operators (functions taking 0 or more arguments of some sort, which return a term of a specific sort). Operators taking 0 arguments are considered constants, and one constructs their term-language by these simple constructs.

Example 1

 
 fmod NAT is
   sort Nat .

   op 0 : -> Nat [ctor] .
   op s : Nat -> Nat [ctor] .
 endfm

This rewrite theory specifies all the natural numbers. The sort saying is introduced, that there exists a sort called Nat (short for natural numbers), and below is the specification of how these terms are constructed. The operator s in Example 1 is the successor function representing the next natural number in the sequence of natural numbers i.e. s(N) := N + 1. s(0) is meant to represent the natural number 1 and so on. 0 is a constant, it takes no input parameter(s) but returns a Nat.

Example 2

 
fmod NAT is
  sort Nat .

  op 0 : -> Nat [ctor] .
  op s : Nat -> Nat [ctor] .
  op _+_ : Nat Nat -> Nat .

  vars N M : Nat .

  eq 0 + N = N .
  eq s(N) + M = s (N + M) .

endfm

In Example 2 the + sign is introduced, meant to represent addition of natural numbers. Its definition is almost identical to the previous one, with input and output sorts, but there is a difference: its operator has underscores on each side. Maude lets the user specify whether or not operators are infix, postfix or prefix (default), this is done using underscores as place fillers for the input terms. So the + operator takes its input on each side making it an infix operator. Unlike our previous operator s which takes its input terms after the operator (prefix).

The three stars are Maude's rest-of-line-comments and lets the parser know that it can ignore the rest of the line (not part of the program), with parenthesis meaning section comments:

*** rest of line is ignored by Maude
*** (
section
is
ignored by Maude
)

The extended Nat module also holds two variables and two sets of equations.

vars N M : Nat .

eq 0 + N = N .
eq s(N) + M = s (N + M) .

When Maude "executes", it rewrites terms according to our specifications. And this is done with the statement

reduce in <some module> : <some term> .

or the shorter form

red <some term> .

For this last statement to be used it is important that nothing is ambiguous. A small example from our rewrite theory representing the natural numbers:

reduce in NAT : s(0) + s(0) .
rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: s(s(0))

Using the two equations in the rewrite theory NAT Maude was able to reduce our term into the desired term, the representation of the number two i.e. the second successor of 0. At that point no other application of the two equations were possible, so Maude halts. Maude rewrites terms according to the equations whenever there is a match between the closed terms that one tries to rewrite (or reduce) and the left hand side of an equation in our equation-set. A match in this context is a substitution of the variables in the left hand side of an equation which leaves it identical to the term that one tries to rewrite/reduce.

To illustrate it further one can look at the left hand side of the equations as Maude executes, reducing/rewriting the term.

eq s(N) + M = s (N + M) .

can be applied to the term:

s(0) + s(0)

since the substitution:

N => 0
M => s(0)

s(N) + M [[N => 0, M => s(0)]] == s(0) + s(0)

makes them identical, and therefore it can be reduced/rewritten using this equation. After this equation has been applied to the term, one is left with the term:

s (0 + s(0))

If one takes a close look at that term, they will see that it has a fitting substitution with matches the first equation, at least parts of the term matches the first equation:

eq 0 + N = N .

substitution:

N => s(0)

s (0 + N) [[N => s(0)]] == s (0 + s(0))

0 + s(0) - matches first equation and is rewritten

The second substitution and rewrite step rewrites an inner-term (the whole term does not match any of the equations but the inner term does). Then one ends up with our resulting term s(s(0)), and it can seem like a lot of hassle to add 1 + 1, but hopefully you will soon see the strength of this approach.

Another thing worth mentioning is that reduction/rewriting up to this point has taken something very important for granted, which is:

  • Reduction/Rewriting terminates
  • Reduction/Rewriting is confluent (applying the equations in any order will eventually lead to the same resulting term)

This cannot be taken for granted, and for a rewrite theory to be sane, one has to ensure that equational application is confluent and terminating. To prove that term-rewriting terminates is not possible in every instance, which we know from studying the halting problem. To be able to prove that term-rewriting (with regards to the equations) terminates, one can usually create some mapping between terms and the natural numbers, and show that application of the equations reduces the associated value of the term. Induction then proves that it is a halting process since the event of finding smaller natural numbers is a halting process. Naturally equation sets that can cause a term-rewrite to contain cycles will not be terminating. To prove confluence is another important aspect since a rewrite theory lacking this ability will be rather flawed. To prove that the equation set is confluent one has to prove that any application of the equations to any belonging term will lead to the same resulting term (termination is a prerequisite). Details for how to prove termination or confluence will not be given here, it just had to be mentioned, since this is where equations and rewrite-rules differ, which is the next topic of this short overview.

Rewrite rules

Up to this point rewriting and reduction have been more or less the same thing, our first rewrite theory had no rewrite rules, still we rewrote terms, so it is time to illustrate what rewrite rules are, and how they differ from the equations we have seen so far (they do not differ much from equations naturally since we talk about the two concepts almost interchangeably).

The module presented so far NAT which represented the natural numbers and addition on its elements, is considered a functional module/rewrite theory, since it contains no rewrite rules. Such modules are often encapsuled with a fmod and endfm (instead of mod endm) to illustrate this fact. A functional module and its set of equations must be confluent and terminating since they build up the part of a rewrite theory that always should compute the same result, this will be clear once the rewrite rules come into play.

Example 3

 
mod PERSON is

including NAT . *** our previous module

sort Person .
sort State .

op married : -> State [ctor] .
op divorced : -> State [ctor] .
op single : -> State [ctor] .
op engaged : -> State [ctor] .
op dead : -> State [ctor] .

op person : State Nat -> Person [ctor] .

var N : Nat .
var S : State .

rl [birthday] :

person (S, N) => person (S, N + s(0)) .

rl [get-engaged] :

person (single, N) => person (engaged, N) .

rl [get-married] :

person (engaged, N) => person (married, N) .

rl [get-divorced] :

person (married, N) => person (divorced, N) .

rl [las-vegas] :

person (S, N) => person (married, N) .

rl [die] :

person (S, N) => person (dead, N) .

endm

This module introduces two new sorts, and a set of rewrite rules. We also include our previous module, to illustrate how equations and rewrite rules differ. The rewrite rules is thought of as a set of legal state changes, so while equations hold the same meaning on both sides of the equality sign, rewrite rules do not (rewrite rules use a => token instead of an equality sign). You are still the same person after you're married (this is open for debate), but something has changed, your marital status at least. So this is illustrated by a rewrite rule, not an equation. Rewrite rules do not have to be confluent and terminating so it does matter a great deal what rules are chosen to rewrite the term. The rules are applied at "random" by the Maude system, meaning that you can not be sure that one rule is applied before another rule and so on. If an equation can be applied to the term, it will always be applied before any rewrite rule.

A small example is in order:

Example 4

 
rewrite [3] in PERSON : person (single, 0) .

rewrites: 4 in 0ms cpu (0ms real) (~ rewrites/second)

result Person: person (married, s(0))

Here we tell the Maude system to rewrite our input term according to the rewrite theory, and we tell it to stop after 3 rewrite steps (remember that rewrite rules do not have to be terminating or confluent so an upper bound is not a bad idea), we just want see what sort of state we end up in after randomly choosing 3 matching rules. And as you can see the state this person ends up in might look a bit strange. (When you're married at the age of one you kind of stick out a bit in kindergarten I guess). It also says 4 rewrite steps, although we specifically stated an upper limit of 3 rewrite steps, this is because rewrite steps that are the result of applying equations does not count (they do not change the term, at least if the equations are sane). In this example one of the equations of the NAT module has been used to reduce the term 0 + s(0) to s(0), which accounts for the 4'th rewrite step.

To make this rewrite theory a bit less morbid, we can alter some of our rewrite rules a bit, and make them conditional rewrite rules, which basically means they have to fulfill some criteria to be applied to the term (other than just matching the left hand side of the rewrite rule).

crl [las-vegas] :

person (S, N) => person (married, N) if (S =/= married) /\ (S =/= dead) .

crl [die] :

person (S, N) => person (dead, N) if (S =/= dead) .

It seems reasonable that you cannot die once you're dead, and you cannot marry as long as you are married. The leaning toothpicks (/\) are supposed to resemble a logical AND which means that both criteria have to be fulfilled to be able to apply the rule (apart from term matching). Equations can also be made conditional in a similar manner.

Why rewriting logic?

Maude sets out to solve a different set of problems than ordinary imperative languages like C, Java or Perl. It is a formal reasoning tool, which can help us verify that things are "as they should", and show us why they are not if this is the case. In other words, Maude lets us define formally what we mean by some concept in a very abstract manner (not concerning ourselves with how the structure is internally represented and so on), but we can describe what is thought to be the equal concerning our theory (equations) and what state changes it can go through (rewrite rules). This is extremely useful to validate security protocols and critical code. The Maude system has proved flaws in cryptography protocols by just specifying what the system can do (in a manner similar to the PERSON rewrite theory), and by looking for unwanted situations (states or terms that should not be possible to reach) the protocol can be shown to contain bugs, not programming bugs but situations happen that are hard to predict just by walking down the "happy path" as most developers do.

We can use Maude's built-in search to look for unwanted states, or it can be used to show that no such states can be reached.

A small example from our PERSON module once again.

search [1] in PERSON : person (single, 1) =>1 person (married, 2) .

No solution.

Here the Natural numbers have a more familiar look (the basic Maude modules prelude.maude has been loaded, that can be done with the command "in prelude", or 1 can be replaced by s(0) and 2 by s(s(0)) if you don't want to load the default Maude-modules), naturally Maude has built-in support for ordinary structures like integers and floats and so on. The natural numbers are still members of the built-in sort Nat. We state that we want to search for a transition using one rewrite rule (=>1), which rewrites the first term into the other. The result of the investigation is not shocking but still, sometimes proving the obvious is all we can do. If we let Maude use more than one step we should see a different result:

search [1] in PERSON : person (single, 1) =>+ person (married, 2) .

Solution 1 (state 7)
states: 8 rewrites: 14 in 0ms cpu (0ms real) (~ rewrites/second)

To see what led us in that direction we can use the built in command show path which lets us know what rule applications led us to the resulting term. The token (=>+) means one or more rule application.

show path 7 .
state 0, Person: person (single, 1)
===[[rl person(S, N) => person(S, N + 1) [label 'birthday]] .]
===>
state 1, Person: person (single, 2)
===[[crl person(S, N) => person(married, N) if S =/= married = true /\ S =/= dead = true [label las-vegas]] .]
===>
state 7, Person: person (married, 2)

As we can see the rule application "birthday" followed by "las-vegas" got us where we wanted. Since all rewrite theories or modules with many possible rule applications will generate a huge tree of possible states to search for with the search command, this approach is not always the solution. We also have the ability to control what rule applications should be attempted at each step using meta-programming, due to the reflective property or rewriting logic.

References

Further reading
  • Clavel, Durán, Eker, Lincoln, Martí-Oliet, Meseguer and Talcott (2007). All About Maude - A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic. Springer. ISBN 978-3-540-71940-3.CS1 maint: multiple names: authors list (link)
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.