Previous Contents Next

Sub Sorts and Membership Axioms

Chapter 7: Sub Sorts and Membership Axioms

In this chapter, we are going to show how to relate different sorts - something that will be useful for the main coursework.

7.1. Sub Sorts

Suppose we wished to write down a specification in Maude of the kind of arithmetic normally found in programming languages. Usually, there will be two basic data types: integers and reals. (Strictly, there may be several kinds of integers; and the reals are not 'real' at all, but approximations more accurately called floating point - but ignore that for now.) The property that will cause us trouble is that typically if you mix real and integer numbers (or variables) in an expression, the language 'knows' automatically that the result should be real. For example, consider the following Pascal code:


var
    fpParam, fpResult : Real;
    intParam : Integer;

    fpResult := fpParam + intParam;

This is perfectly legal. The compiler has two version of addition, and it (a) knows which one to use; and (b) knows it must first convert (cast) intParam to type Real. In Maude, we get something like this:


fmod MIXED-ARITH1 is
    sorts Integer Real .

    op _+_ : Integer Integer -> Integer .
    op _+_ : Real Real -> Real .
    
    var i : Integer .
    var r : Real .
endfm

***Try reducing a 'mixed' expression
red i + r .

Before we go any further, notice two things.

If we apply Maude to MIXED-ARITH, we get:


Warning: "mixedarith1.maude", line 12: didn't expect token r:
i + r <---*HERE*
Warning: "mixedarith1.maude", line 12: no parse for term.

What this means is that Maude has found the integer variable i and the operator _+_ : Integer Integer -> Integer, and is looking for another integer argument - but it finds a real, so it fails. We could 'fix' this by defining a conversion operator:


op : int2real : Integer -> Real .

but that would be horrible. Here is another version of MIXED-ARITH that works:


fmod MIXED-ARITH is
    sorts Integer Real .

    subsort Integer < Real .

    op _+_ : Integer Integer -> Integer .
    op _+_ : Real Real -> Real .

    var i : Integer .
    var r : Real .
endfm

***Try reducing a 'mixed' expression
red i + r .

Notice the line


subsort Integer < Real .

This says that Integer can be considered to be a sub sort of Real. That is, any operator that can accept a Real as an argument, can also accept an Integer in the same position. This means that when we try to reduce i + r, the operator


op _+_ : Real Real -> Real .

can be used - because the integer argument can be 'promoted' to real:


reduce in MIXED-ARITH : i + r .
rewrites: 0 in -10ms cpu (0ms real) (~ rewrites/second)
result Real: i + r

This time there is no error. Notice that Maude has not 'done' anything with i + r - no rewriting has been done. This is because there are no equations. However, Maude has accepted the expression as legal..

Formally, this is called order sorted algebra - and it will be useful to us when we try to define sorts representing binary words of different, but fixed, lengths.

This concept of sub sorting gives us an idea - we could rewrite our stack example to get rid of all the irritating error-handling behaviour needed:


fmod ORDER-STACK is
    sorts Stack NeStack Elt .

    subsort NeStack < Stack .

    op top : NeStack -> Elt .
    op push : Stack Elt -> NeStack .
    op pop : NeStack -> Stack .

    var E : Elt .
    var F : Elt . *** Only used in reductions
    var S : Stack .
    var NeS : NeStack .

    eq top(push(S,E)) = E .
    eq pop(push(S,E)) = S .
endfm

*** push E on S then take top - should be E
red top(push(S,E)) .

*** push E on S then take top - should be S
red pop(push(S,E)) .

*** push F then E on S then pop it,
*** then take top - should be F
red top(pop(push(push(S,F),E))) .

We have introduced a new sort NeStack - non-empty stacks - and have made non-empty stacks a subsort of all stacks. We have also changed our definitions of top, push and pop. The top operator now takes a non-empty stack as an argument - so it is impossible to apply it to an empty stack (or rather if you do, Maude will recognise it as a type error). Similarly, the push operator now returns a non-empty stack - which it clearly must as we have just pushed something onto it. Finally, pop only takes non-empty stack arguments, but because we might have just popped the last element, it returns an 'ordinary' stack as a result. (The careful amongst you might have noticed that we have quietly dropped isEmpty - that's because it's a bit difficult.)

7.2. Membership Axioms

Sub sorting is a very convenient way of 'promoting', or 'broadening' one sort to a more general 'super sort'. For example, integers to reals. However, what is we wish to do the reverse? Suppose we have a real that is 'actually' an integer - how do we get Maude to (a) recognise that; and (b) automatically 'narrow' its sort? The answer is that we must introduce some rules, or axioms, to manage that for us. They are called membership axioms, and they come in conditional and unconditional forms. Here is an example from the Maude manual.


fmod PATH is
    protecting MACHINE-INT .
    
    sorts Edge Path Path? Node .

    subsorts Edge < Path < Path? .

    *** These (constant) operators just
    *** describe the graph in fig 1
    ops n1 n2 n3 n4 n5 :  -> Node .
    ops a b c d e f : -> Edge .

    *** This is the concatenation operator
    op _;_ : Path? Path? -> Path? [assoc] .

    *** Take a path and find were it starts
    *** and ends
    ops source target : Path -> Node .

    *** How long is a path?
    op length : Path -> MachineInt .

    var E : Edge .
    var P : Path .

    *** is an edge concatenated with a path a
    *** 'real' path or not?
    cmb (E ; P) : Path if target(E) == source(P) .

    *** These equations define the operators
    ceq source(E ; P) = source(E) if E ; P : Path .
    ceq target(P ; E) = target(E) if P ; E : Path .

    eq length(E) = 1 .
    ceq length(E ; P) = 1 + length(P)
        if E ; P : Path .

    *** These equations just describe the example
    *** graph in fig 1.
    eq source(a) = n1 .
    eq target(a) = n2 .
    eq source(b) = n1 .
    eq target(b) = n3 .
    eq source(c) = n3 .
    eq target(c) = n4 .
    eq source(d) = n4 .
    eq target(d) = n2 .
    eq source(e) = n2 .
    eq target(e) = n5 .
    eq source(f) = n2 .
    eq target(f) = n1 .
endfm

The module PATH describes a graph, with nodes n1 to n5 and edges a to f. The actual graph is shown in fig 1.


Fig.1. The Graph Example

We are interested in paths through the graphs - sequences of edges in which the tail of one edge and the head of the next are the same node. To do this, we introduce four sorts:

The concatenation operator _;_ joins sequences of sort Path? - but notice the line

 cmb(E ; P) : Path if target(E) == source(P) .

This is a conditional membership axiom which 'narrows' (E ; P) from Path? to Path provided the end of E is the same node as the start of P. That is, only if a contiguous line can be drawn along the sequence of edges represented by (E ; P) is it a 'real' path.

In the example shown in fig 1, the sequence


(a ; b ; c ; d ; e)

is of sort Path, but the sequence:


(a ; e ; d ; f)

is not (it is of sort Path?) because it is not contiguous.

Previous Contents Next