Previous Contents Next

Basic Maude

Chapter 4: Basic Maude

In this chapter, we will introduce the fundamental syntax of Maude, concentrating on those aspects of most concern to us. You can find manuals and tutorials on the Maude website, and many of our examples in this chapter have been adapted from them (or in some cases, just 'lifted' as-is). You are of course welcome to look at the material on the Maude site: however, for the most part it goes beyond what is required here, and may be rather difficult to interpret. The exception is the Maude Primer which is worth looking at.

4.1. A Simple Maude Module

We start with a simple Maude module for the Natural numbers:


fmod BASIC-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) + N = s(M + N) .
endfm

Modules start with 'fmod name is' and end with 'endfm'. This is a functional module - hence the 'f'. There are other kinds, but we do not need them.

The module BASIC-NAT introduces a new sort called Nat, and three operators. The first operator op 0 : -> Nat . is a function of no arguments, and is hence a constant, since (mathematically) any function which takes no arguments must always return the same value. Pretty much all statements within a module end with '.': and note the space before the '.'. We will return to whitespace in Maude below. The second operator op s : Nat -> Nat . is the successor function (or more accurately, is intended to represent the successor function).

4.1.1. Mixfix Notation

The third operator op _+_ : Nat Nat -> Nat . is the addition function: notice the underscores _ in the definition of _+_. It is notationally very inconvenient to have to write operations like + in the 'conventional' programming language-like syntax for user-defined functions: that is '+(a,b)'. We would prefer to write 'a+b'. Mixfix notation allows us to do this: the presence of underscores in a function name imply that we are using mixfix. The idea is that each argument of the function will replace one of the underscores. For example, consider


op if_then_else_fi : Bool Nat Nat -> Nat .

We could then apply this operator like this:


if B then X else Y fi

where B is a Boolean, and X and Y are Nats. It is your responsibility to ensure that (a) the number of underscores matches the number of arguments; and (b) the arguments replace the underscores in the correct order. It is also your responsibility to not use underscores in identifier names if you do not wish to use mixfix: if Maude sees an operator name without underscores, it automatically assumes you wish to use conventional function notation. So because the operator 's : Nat -> Nat' does not have any underscores, we apply it like this: 's(X)'. In practice, mixfix is extremely convenient if used properly, and eliminates most of the syntactic irritations that traditionally arise when representing mathematics in a programming language-like notation.

Following the operators, we define the behaviour of the addition operator by structural induction in the usual way. Notice that we declare all the variables that appear in the equations. Notice also there are no equations defining the behaviour of s and 0. Strictly speaking, as we saw earlier these generate data and are called constructors. In fact, s and 0 between them can generate all the possible elements of sort Nat, and the addition operator just 'chooses' one of them: the result of an addition will either be 0 or of the form s(s(...s(0)...)). Constructors do not need defining equations, though we can optionally denote them in our algebras by [ctor]: for example,


op 0 : -> Nat [ctor] .

This does not actually affect the logic, and we will generally omit it. Incidentally, there are a number of other flags that can be added to operators using '[...]', and we will see a few more later.

After introducing the operations, we declare some variables. Note we are declaring more than one variable of the same sort on the same line: to do this we use the keyword vars. If we only wanted to declare a single variable, we would use the keyword var. A similar situation occurs when declaring multiple operators on the same line. For example:


ops _+_ _*_ : Nat Nat -> Nat .

Another flag that's useful for our simple natural number algebra is [iter]. In our current version, if we want to represent '5' we need to write:


s(s(s(s(s(0)))))

which is inconvenient. However, if we defined s like this:


op s : Nat -> Nat [iter] .

we can simply write s^5(0) instead, which is better if not perfect. Note you can only use [iter] with operations that have only one argument. Here is another version of BASIC-NAT with [ctor] and [iter] added as appropriate.


fmod BASIC-NAT2 is
        sort Nat .

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

        vars N M : Nat .

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

If we evaluate s^5(0) + s^3(0) we get:


s^8(0)

If we want to do the equivalent in the original BASIC-NAT we would need to write something like s(s(s(s(s(0))))) + s(s(s(0))) and would get:


s(s(s(s(s(s(s(s(0))))))))

which is obviously less convenient.

4.1.2. A Note on Whitespace

Maude has very liberal views on identifiers which, combined with mixfix notation, provides a flexible syntax, that is very convenient. However, it has consequences - the most obvious to new users being its 'sensitivity' to whitespace. Notice in the example above that we have put spaces around all the key tokens - :, -> - and even before the terminal '.' ending each statement. A 'normal' programming language would not require this - but Maude does, and will report syntax errors if you do not do it. Failing to observe this is the most common syntactic problem new users have in my experience. That is, historically a lot of coursework submissions that are syntactically incorrect can be fixed by adding spaces at the appropriate point(s). Another common problem is failing to match brackets properly. These problems are not well-reported by Maude, but are easily fixed with a bit of help. (So just ask!)

4.1.3. Another Example - Booleans

Here is another simple example, that we introduce largely because we will need it for an example later. Notice the use of [ctor] here. (Leaving this out will make no difference.) Also note that the list of equations is incomplete.


fmod BOOLEAN is
        sort Boolean .

        op true : -> Boolean [ctor] .
        op false : -> Boolean [ctor] .

        op not : Boolean -> Boolean .
        op _and_ : Boolean Boolean -> Boolean .
        op _or_ : Boolean Boolean -> Boolean .

        var A : Boolean .

        eq not(true) = false .
        eq not(false) = true .
        eq true and A = A .
        eq false and A = false .
        eq true or A = true .
        eq false or A = A .
endfm

Notice that we have made no provision in this example for the associativity and commutativity of operators and and or. We address this in a later section. Also, Maude has a built-in version of the Booleans (the sort is Bool), so you do not have to declare your own. (In fact, Bool is the only built-in algebra in Maude.)

4.2. Module Hierarchies

To simplify and organise our descriptions of systems we can structure them hierarchically by a system of importation. Maude provides two ways of doing this: protecting and importing. Here is an example using protecting


fmod NAT+OPS is
        protecting BOOLEAN .
        protecting BASIC-NAT .

        ops _*_ _-_ : Nat Nat -> Nat .
        ops _<=_ _>_ : Nat Nat -> Bool .

        vars N M : Nat .
        eq 0 * N = 0 .
        eq s(M) * N = (M * N) + N .
        eq 0 - N = 0 .
        eq s(M) - 0 = s(M) .
        eq s(M) - s(N) = M - N .
        eq 0 <= N = true .
        eq s(M) <= 0 = false .
        eq s(M) <= s(N) = M <= N .
        eq M > N = not(M <= N) .
endfm

Recall that earlier we were concerned about what might happen if we 'changed' an operator that appears in a module we import. By using protecting we are saying that we are, essentially, not changing the behaviour of anything in the modules we are importing. However, in the next example (natural numbers modulo 3) we must use importing because we are modifying the behaviour of BASIC-NAT:


fmod NAT 3 is
        including BASIC-NAT .

        var N : Nat .

        eq s(s(s(N))) = N .
endfm

Generally, we will be using protecting.

4.3. Rewriting

We have seen how to create simple modules: how do we go about using them? First you need to set your path to point to Maude. This can be found at:


/compsci/jupiter/maude-linux/bin

The precise way you do this depends on which shell you are using. If you are using the 'traditional' default csh, then create (or edit if it exists) the file .cshrc (note the leading '.') and put in it the line:


set path = ($path /compsci/jupiter/maude-linux/bin)

If you are using a different shell, then you are on your own - but basically you need to modify the environment variable PATH (note all capitals).

Download the first example, and type


maude.linux basicnat.maude

You should see something like:


                     \||||||||||||||||||/
                   --- Welcome to Maude ---
                     /||||||||||||||||||\
            Maude 2.0.1 built: Aug  1 2003 17:25:59
             Copyright 1997-2003 SRI International
                   Thu Jan  8 20:26:59 2004
Maude>

( By the way, to exit Maude type quit.) If you are running Maude within a different environment (Windows, MacOS) then you will have to type a slightly different command (e.g. on a Mac it's maude.darwin).

To evaluate something within Maude, you must reduce it, using the reduce command (shortened to red). At the prompt, type:

  red s(0) + s(s(0)) . 

Notice the final '.' and the space before it! This is necessary when you type in reductions (or put them in a file) as well as for statements in Maude. You should see:


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

You have just asked Maude to evaluate s(0)+s(s(0)) (i.e. 1+2) and got the answer s(s(s(0))) (i.e. 3). To see things in a little more detail, type set trace on . before performing the reduction. You should see:


Maude> set trace on .
Maude> red s(0) + s(s(0)) .
reduce in BASIC-NAT : s(0) + s(s(0)) .
*********** equation
eq s(M) + N = s(M + N) .
M --> 0
N --> s(s(0))
s(0) + s(s(0))
--->
s(0 + s(s(0)))
*********** equation
eq 0 + N = N .
N --> s(s(0))
0 + s(s(0))
--->
s(s(0))
rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: s(s(s(0)))

Maude first applies the equation s(M) + N = s(M + N) to rewrite s(0) = s(s(0)) to s(0 + s(s(0))), and then applies equation 0 + N = N to rewrite 0 + s(s(0)) to s(s(0)). To understand what is going on, the lines beginning 'eq' denote the equation that Maude is about to apply; the lines containing '-->' show what the variables in the equation are instantiated to; the next line shows the left-hand side of the equation after the variables have been instantiated (i.e. the term that is to be rewritten); and the lines after the '--->' show the right-hand side of the equation after the variables have been instantiated (ie. the result of the rewrite).

Try some experiments with BASIC-NAT, BOOLEAN and NAT+OPS to get the hang of things. You'll probably want to do

set trace off .

(or restart Maude) as your expressions get more complex, or you will find the output gets a bit 'voluminious'.

4.3.1. Small Technical Point

As you experiment with BOOLEAN you will get some complaints from Maude about 'multiple distinct parses'. This is because there is already a built in version of the Booleans (Bool) with constants true and false. Unless you distinguish them, it cannot tell them apart: did you intend to use your own BOOLEAN or the built-in BOOL?. There are two ways to do this. First, rename true and false to (e.g.) tt and ff inside BOOLEAN (try it), or secondly to explictly tell Maude the sort(s) you intend it to use. For example, instead of typing


red true and true .

type


red (true).Boolean and true .

You could have typed (true).Boolean and (true).Boolean, but this is not necessary (why?).

4.4. Associativity and Commutivity

We have discussed associative and commutative operators in the term rewriting chapter, and clearly some of the operators above are commutative and/or associative. We cannot just add equations asserting this without getting a non-terminating rewriting system, so instead we annotate the operators with the desired property or properties using the assoc and comm flags. For example:


op _+_ : Nat Nat -> Nat [assoc comm] .

Modify the modules in this chapter appropriately, and try some experiments with them.

There are many such directives that can be appended to operators - and some of the pre-defined modules that you will use will employ some of them. However, the only ones you will ever need to use are assoc and comm. Also, if you do use assoc and/or comm, please take the trouble to check that the operators you apply them to are associative or commutative or both, as appropriate - a common error in coursework.

4.5. Some Assorted Practical Things

Maude is a very useful, and flexible, system. However: (a) it can take some getting used to; and (b) it is not that good at error reporting. In this section, we will look at some practical issues that will (hopefully) help.

4.5.1. Maude Commands

Maude has a wide range of internal commands, some of which are more useful than others from our point of view. The most helpful ones are these.

4.5.2. Syntax Problems

As has been said, the main syntax problem is failure to put spaces in the right places. Another common problem, that is badly-handled by current Maude versions, is mis-matched brackets, and certain kinds of 'missing' syntax (e.g. leaving off the '.' at the end of statements). There may be no error messages, and no real sign that anything is wrong.

We will step through the process of tracking down such an error. Here is a deliberately faulty example: it's a bit complex (and based on an example later in the module) but we need an example with more than one module to show how to track down errors. Most of the code has been left out of the notes for simplicity - you need to look in the file to see all of it. If you look near the end - the last but one equation - you will see a comment marking a line with a missing bracket.

   
    *** Lots left out but in the actual file

    var X : IntStr .
    var T : Int .
    vars I J K : Int .
    eq W1 = 1 .
    eq W2 = -1 .
    eq W3 = 1 .
    eq W4 = -1 .
    eq C(I,J,K) = K .
    eq convImp(T,X) = (conv1(T,X), conv2(T,X), 
                       conv3(T,X), conv4(T,X)) .

    eq conv1(T,X) = ips(W1,X(T - 3),0) .
    eq conv2(T,X) = ips(W2,X(T - 2),C(conv1(T - 1, X))) .
    *** Missing bracket, next line
    eq conv3(T,X) = ips(W3,X(T - 1),C(conv2(T - 1, X)) .
    eq conv4(T,X) = ips(W4,X(T),C(conv3(T - 1, X))) .
endfm

If we run this through Maude and then hit return we get:


maude.linux convImp.maude 
                     \||||||||||||||||||/
                   --- Welcome to Maude ---
                     /||||||||||||||||||\
            Maude 2.0.1 built: Aug  1 2003 17:25:59
             Copyright 1997-2003 SRI International
                   Thu Jan  8 21:34:47 2004
Maude> 
> 

Type 'control-C', and you will see something like this:


Advisory: <standard input>, line 2 (fmod CONV-IMP): discarding incomplete
    module.

This tells you that there is a problem (normally 'control-C' does basically nothing) and that the faulty module is CONV-IMP. At first sight it seems that you also get the line number ('line 2') but unfortunately this is just the second line of input that you have typed.

If you cannot see the problem, then try putting these two lines part-way through the module:


endfm
eof

In this case, we put them after the first block of equations:



    var X : IntStr .
    var T : Int .
    vars I J K : Int .
    eq W1 = 1 .
    eq W2 = -1 .
    eq W3 = 1 .
    eq W4 = -1 .
endfm
eof
    eq C(I,J,K) = K .
    eq convImp(T,X) = (conv1(T,X), conv2(T,X),
                       conv3(T,X), conv4(T,X)) .

Maude now ignores everything after 'eof' - and now when we type 'control-C' the error is gone. This means we know that the problem is after the 'eof'. We can repeat the process if necessary to further narrow down the problem.

4.6. Writing Equations

Maude is essentially a programming notation, that sits within the paradigm of equational programming. As always, when you first use a new programming paradigm, things can be difficult (recall the first time you wrote logic, and functional, programs; or the first time you wrote object oriented programs; even conventional procedural programs).

In terms of expressing solutions to problems in Maude, the closest alternative paradigm is functional programming - and functional programming examples can be helpful. Remember, that in equational languages - as in functional languages - there is no iteration (you must use recursion) and there is no assignment (the equation 'X=Y' means 'X is equal to Y' - not 'make X equal to Y').

In the next chapter we will look at some specific, and small, examples.

Previous Contents Next