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 consist of a term-language plus sets of equations and rewrite-rules. Terms in a rewrite theory are constructed using operators. 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 .
 op s : Nat -> Nat .
 endfm

This rewrite theory specifies all the natural numbers. The sort saying is introduced, that there exists a sort called Nat, 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 + 1. s is meant to represent the natural number 1 and so on. 0 is a constant, it takes no input parameter but returns a Nat.

Example 2

fmod NAT is
sort Nat.
op 0 : -> Nat .
op s : Nat -> Nat .
op _+_ : Nat Nat -> Nat.
vars N M : Nat.
eq 0 + N = N.
eq s + M = s .
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, 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.
The three stars are Maude's rest-of-line-comments and lets the parser know that it can ignore the rest of the line, with parenthesis meaning section comments:
*** rest of line 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 + M = s .
When Maude "executes", it rewrites terms according to our specifications. And this is done with the statement
reduce in : .
or the shorter form
red .
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 + s.
rewrites: 2 in 0ms cpu
result Nat: s
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 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 + M = s .
can be applied to the term:
s + s
since the substitution:
N => 0
M => s
s + M N => 0, M => s s + s
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
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
s N => s s
0 + s - matches first equation and is rewritten
The second substitution and rewrite step rewrites an inner-term. Then one ends up with our resulting term s, 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
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 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. 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.
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 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 .
op divorced : -> State .
op single : -> State .
op engaged : -> State .
op dead : -> State .
op person : State Nat -> Person .
var N : Nat.
var S : State.
rl :
person => person .
rl :
person => person .
rl :
person => person .
rl :
person => person .
rl :
person => person .
rl :
person => person .
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. You are still the same person after you're married, 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 in PERSON : person .
rewrites: 4 in 0ms cpu 
result Person: person

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, 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.. 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. In this example one of the equations of the NAT module has been used to reduce the term 0 + s to s, 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.

crl :
person => person if /\ .
crl :
person => person if .

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. 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, but we can describe what is thought to be the equal concerning our theory and what state changes it can go through. 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, and by looking for unwanted situations 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 in PERSON : person =>1 person .
No solution.

Here the Natural numbers have a more familiar look, 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, 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 in PERSON : person =>+ person .
Solution 1 
states: 8 rewrites: 14 in 0ms cpu

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
[rl person(S, N) => person(S, N + 1) [label 'birthday] .]
>
state 1, Person: person
[crl person(S, N) => person(married, N) if S =/= married = true /\ S =/= dead = true [label las-vegas] .]
>
state 7, Person: person

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.