You may have already studied some of the theoretical background of Universal Algebra in other modules. In this chapter, we will 'revise' some of the concepts, and introduce the idea of axiomatization. I say 'revise' because (a) even if you have seen it before, I suspect some of you may not be as au fait with algebra as you perhaps should be; and (b) because I will have a different 'take' on it - because I am concerned with its application - not the theoretical background.
At its simplest, an algebra is single sorted - that is, it is only concerned with one type of 'thing', or sort. You can think of the word sort as being synonymous with type. The reason we do not use type is that it is a 'loaded' word - many years of use in programming languages has meant it has acquired a particular meaning (actually, a range of slightly different meanings). A single-sorted algebra then, only contains a single sort (type), together with constants of that sort, and operations on that sort. Here is an example - about as simple as we can get:
Algebra Nat is
sort Nat
const 0 : Nat
op Succ : Nat -> Nat
end Algebra
This is an algebra called Nat with one sort (also Nat), a constant 0 and an operation Succ. There are a few things to explain here.
If you study algebra, you will find there are two views of constants. The first is that they are something that should be treated as a separate concept. The other is that a constant is really just an operation with no arguments. Think about it - we are talking about mathematical operations here. There are no global variables, so an operation can only compute on its arguments. If it has no arguments, it must always return the same result - a constant. Personally, I prefer the first option - however Maude uses the second (for good pragmatic reasons), so we will do that from now on:
Algebra Nat is
sort Nat
op 0 : -> Nat
op Succ : Nat -> Nat
end Algebra
So our constant 0 is now an operation, but there is nothing between the ':' and the '->': and hence no arguments.
The next simplest example is probably the Booleans:
Algebra Bool is
sort Bool
ops tt ff : -> Bool
op not : Bool -> Bool
ops and or : Bool Bool -> Bool
end Algebra
Bool has a single sort (Bool), two constants (tt and ff - notice we have abbreviated them into a single line to make the code shorter) and three operations: not which takes one argument; and and and or which take two.
Single-sorted algebras are not particularly useful to us in most cases - we need many-sorted algebras.
A many-sorted algebra extends a single-sorted algebra in the obvious way: you can have multiple sorts. For example, you might want to combine Nat and Bool:
Algebra NatBool is
sorts Nat Bool
op 0 : -> Nat
ops tt ff : -> Bool
op Succ : Nat -> Nat
op not : Bool -> Bool
ops and or : Bool Bool -> Bool
op if : Bool Nat Nat -> Nat
end Algebra
Notice that we have added the operation if which uses both Bool and Nat. Without many-sorted algebras, we would not be able to have functions like if. At this point you are probably thinking that it is little cumbersome to have to write out everything in a single algebra. If Nat and Bool already exist, can we not use them? We can:
Algebra NatBool is
including Nat
including Bool
sorts Nat Bool
op if : Bool Nat Nat -> Nat
end Algebra
That is, we have 'imported' the existing algebras. This is obviously useful, but there are a couple of issues to consider.
Hopefully, this gives you the general idea of [the signature of] and algebra, if you were not already familar with it. However, it is not of use for specification without semantics - that is, meaning. We want to add meaning to our signatures such that the following hold.
Fortunately, there is a way to do what we want.
Recall your study of Boolean Algebra - you were probably introduced to the idea of Boolean function (and, or etc.) using truth tables - but you were also probably introduced to at least some axioms. An axiom is simply a rule that must be obeyed. For example, in the case of the Booleans:
not(not(a)) = a
The way you probably think about these rules is: 'I know what Boolean algebra is, and it must obey a set of rules.' However, you can reverse this: you can define a set of rules and then anything that obeys it IS Boolean algebra, regardless of details like the names of the operators etc. This is what we are going to do: our rules, or axioms, will always be either equations:
X = Y
or conditional equations
X = Y if Z
For example, here is our Bool algebra extended with a set of equations:
Algebra Bool is
sort Bool
ops tt ff : -> Bool
op not : Bool -> Bool
ops and or : Bool Bool -> Bool
vars A B C : Bool
eq not(not(A)) = A
eq not(tt) = ff
eq not(ff) = tt
eq and(A,B) = and(B,A)
eq and(A,and(B,C)) = and(and(A,B),C)
eq and(tt,A) = A
eq and(ff,A) = ff
eq or(A,B) = or(B,A)
eq or(A,or(B,C)) = or(or(A,B),C)
eq or(tt,A) = tt
eq or(ff,A) = A
eq not(and(A,B)) = or(not(A),not(B))
eq not(or(A,B)) = and(not(A),not(B))
end Algebra
Hopefully, all (or at least most) of thes are familar: the first group define not, then and, then or, and the last ones (de Morgan's Laws) relate and and or.
Once again, there are a few points to consider.
We said we can also use conditional equations: these are illustrated by the axiomatization of NatBool:
Algebra NatBool is
including Nat
including Bool
sorts Nat Bool
op if : Bool Nat Nat -> Nat
var B : Bool
vars X Y : Nat
ceq if(B,X,Y) = X if B == tt
ceq if(B,X,Y) = Y if B == ff
end Algebra
The important point here is: what is '=='? The answer, briefly, is that it is syntactic equality. That is, in the case of NatBool, if B can be transformed (using the equations in Bool) into tt, then if(B,X,Y) reduces to X; if B can be transformed into ff, then if(B,X,Y) reduces to Y. It may well be the case that we cannot transform B into either - for example, what about not(A)? In that case, neither of the conditional equations can apply. We use '==' instead of '=' to emphasise that the '=' symbol in an equation is somehow 'special'. Strictly speaking, 'A==B' symbol is just an 'abbreviation' for an operator: 'equals(A,B)', which returns true if A and B are syntactically identical, and false otherwise.
At this point you may have noticed that I have studiously avoided any equations defining our first example Nat. This is because it is fundamentally problematic. Think about it: what equations can you give to define the behaviour of the +1 function? Remember, only equations (and conditional equations) are allowed - no other relations (not equal, greater than,...). The answer is that there are no equations possible - or necessary - in this case. This may seem ridiculous. What is to stop us picking a completely ludicrous 'implementation' of the naturals? For example, we could say that the sort Nat only contains the element 0 and Succ(X)=X for all X (that is, X=0). The answer is to do with initiality, or initial algebra semantics. The details are fairly horrendous, but fortunately for this module we can do the easy version. However, to understand the following discussion, you should revise the concept of a homomorphism from Theory of Programming Languages.
We have more-or-less implied that our sets of equations define one single possible implementations - the one which 'obeys' the equations - for our algebra. In fact, there may be many such implementations, or interpretations of the equations. Many of these will be functionally identical, which is no problem. However, others will not. Consider for example our Nat algebra - there is the 'sensible' interpretation and our 'silly' one. The way to resolve this theoretically is as follows. Collect together all the possible interpretations and construct the set of all homomorphisms between them. You will have something that looks like figure 1.
Some of these potential implementations are special. From every one of them we can reach, by [a chain of] homomorphisms every other implementation (including each other: we have taken the slight liberty in the diagram of using double-headed arrows to mean 'homomorphism both ways' - an isomorphism). This set of implementations is known as the isomorphism class, and these are the so-called initial algebras. Our interpretation of our sets of equations is that they represent the behaviour of one of these initial algebras, and not any of the other algebras. There may be more than one initial algebra - but they are all equivalent so it does not matter. To go back to our Nat example, we can construct a homomorphism from the 'proper' one to the 'silly' one - but not vice versa. Therefore, the 'silly' one is disallowed.
We mentioned earlier that the Succ operator in the NAT example was 'special' in some way. To see why, let's look at a slightly extended version of Nat.
Algebra Nat is
sort Nat
const 0 : Nat
op Succ : Nat -> Nat
op + Nat Nat -> Nat
vars A B : Nat
eq 0 + B = B (1)
eq Succ(A) + B = Succ(A + B) (2)
end Algebra
(Note we have slightly cheated in our equation for + - we should write '+(Succ(A),B) = Succ(+(A,B))'. However, the simpler version will be more readable in the example, and we will continue to do this from now on. We have also labelled the equations (1) and (2).) Now we will look at a particular example: 3 + 2. The first thing to notice is that we cannot directly write down '3 + 2', because we do not have any concept of '2' or '3'. We instead have to write 'Succ(Succ(Succ(0))) + Succ(Succ(0))'. These leads to an important observation for Nat:
All instances of the sort Nat can only be written as Succ(...(Succ(0)...), for zero of more applications of the operation Succ.
In other words, between them, Succ and 0 are sufficient to enumerate all the elements of the sort Nat - in a sense, between them, they define the sort Nat. We call such constants and operators constructors - not to be confused with constructors in object oriented programming. The constructors do not have any equations defining them - they somehow just 'are'. The addition operator on the other hand, which is not a constructor, does have defining equations.
Incidentally, what happens with the example?
Succ(Succ(Succ(0))) + Succ(Succ(0))
= Succ(Succ(Succ(0)) + Succ(Succ(0))) using (2)
= Succ(Succ(Succ(0) + Succ(Succ(0)))) using (2)
= Succ(Succ(Succ(0 + Succ(Succ(0))))) using (2)
= Succ(Succ(Succ(Succ(Succ(0))))) using (1)
In the next chapter we will look at how we can get software to deal with equations.