Putting Theories Together to Make Specifications

Introduction

We have been developing a language in which you can give structured descriptions of theories.

Why are we interested in theories? Because you need a theory to specify a problem before you can develop a program to solve it, whether you intend ·to develop the program ±ntuitively or to synthesise it mechanically by rule. It only makes sense to say 'We want a program which can invert a matrix' in the context of some theory about matrices and the operations on them such as multiplication.

Why are we interested in structured descrip­ tions of theories? Because people find it very hard to understand anything at all unless they have a well-structured description .of it; as for machines, twenty years work in Artificial Intel­ ligence has taught us to beware of letting them

loose on an unstructured description.

What would an unstructured description of a theory be like? Imagine 217 axioms in Predicate Calculus telling you how to find your way around SRI, or 217 semantic equations describing the language Klugegol78. Mi nsky (1975) protests about 'attempts to represent knowledge as collec­ tions of separate simple fragments'. No-one could approve of such monsters as these.

Now consider the analogous situation with programs. They are structured by statements, iterations and procedures. For large programs these have proved inadequate (217 LISP functions!A and SIMULA classes, CLU clusters and ALPHARD forms have been devised to ward off the threatened chaos (Dahl et al 1970, Liskov 1975, Wulf et al 1976). They all introduce abstract data structures by giving the collections of procedures which define the primitive operations on them. They separate the part of the program which implements a struc­ ture from other parts which use it but have no concern with its representation. Similarly in AI Minsky's frame notion (Minsky 1975) offers a way of .bundling together LISP functions into some meaningful entities. Indeed one reason for the move away from a 'logical' representation of knowledge to a procedural one may be that we have some skill at structuring programs but hardly any

at structuring theories.

Our work on theories derives from our attempts to clarify and generalise the above methods of building up programs in terms of abstract data structures. Tackling problem specifications rather than programs turned out to use the same mathematical tools but to be rather less difficult. It is also an area overdue for illumination. The present paper sets forth in taking a state to a description, (iii) valueo~ taking a description and an attribute to a value, (iv) undefined, a constant for a state, and so on. There are some laws, for example:­ apply(a,undefined) =undefined, concatenation of action sequences is associ­ ative.

Lawvere showed how such a theory description can be taken to denote a more abstract algebraic structure, namely a collection of operators susceptible to 'composition' (substitution) and 'tupling'. This is important because he was able to develop some theory about 'theories' (if you can have a theory about 'groups' you can have a theory about 'theories'), and his work enables us to give a mathematical basis to our language for denoting theories. It is not appropriate to go into this mathematics here, but it is a com­ fort to us that we have managed to outline a proper semantics for our language; we hope to develop this and write it up soon for publication.

Not only is it relatively easy to reason about algebraic theories, but there is evidence ~it is relatively easy to reason~ an algebraic theory, indeed that is just the domain which was tackled very successfully by Boyer and Moore (1975) with their LISP theorem.prover, sub­ sequently enhanced to deal with many sorts by Aubin (1976).

We already have some encouraging experience of using algebraic theories (but not structured ones) as a specification tool (Goguen 1976, Goguen, Thatcher and Wagner 1977).

The use of algebraic techniques for speci­ fying abstract data t~es has been studied extensively by Zilles (1974) and by Guttag, Horowitz and Musser (Guttag 1975, Guttag et ~ 1976) who give examples of program verification using such specifications.

We should remark that although we have chosen to use algebraic theories rather than predicate logic or lambda calculus theories, the methods we have used to combine them are rather general and may well apply to other kinds of theory.

We have not written out the above examples of theories in full because they would be long and hard to understand; even eight operators and a dozen laws is a lot to swallow in one bite. A mathematics book would scarcely present the con­ cept of vector space without some preparation on semigroups, groups and fieldsIndeed most of the structure can be explained by saying that the scalars form a field and the vectors a group. We then have to impose some extra conditions (e.g. commutativity of vector addition) and enrich the structure with an extra operator, multiplication of vectors by scalars, which is distributive, etc.

Similarly GPS becomes much easier to under­ stand if we first describe a state-action system, then say that action-sequences are just strings of actions whose effect is the composition of the effect of the component actions. We can independently enrich the idea of state with attributes and values, saying that descriptions are just arrays (finite functions) from attributes to values. Only then can we put it all t ogether and introduce the notion of the differences reduced by an operator.

This then is intuitively what we mean by building up a theory in a structured way: any good textbook does it all the time. Luckily Lawvere's notion of the category of theories supplies the mathematical correlate of this informal exposition and enables us to apply known mathematical methods (·colimits·) to the task of constructing theories by using other theories as ingredients.

One may view a theory as a natural general­ i sation of the notion of abstract data type. Such a type is characterised by the operations which create its elements or apply to them. A theory may consist of several such types with the operations between them, thus avoiding the diffi­ culty of arbitrarily assigning an operation from A's to B's to type A or to type B. Analogous to a group of procedures which realise a data-type, as in SIMULA, CLU or ALPHARD, would be a group of procedures which realise a theory. We learned recently that Nakajima, Honda and Nakahara (1977) had also been working on this idea and had designed a programming language to incorporate it. Their use of theories in a programming language is close to what we had in mind. We hope that the mathematical methods we have for structuring specifications can be adapted to give semantics for such a programming language (see our tentative remarks about programs as theory morphisms later on).

Specifications required for program verification, transformation and synthesis

Program verification has been a continuing concern since McCarthy's classic paper (1.963). Recently there has been considerable interest in synthesising programs from their specifications (Manna and Waldinger 1971, 1975), Dijkstra (1975), Darlington (1975, 1976), one promising method being to take a very naive program as the specif­ ication and transform it into an acceptably efficient one (Darlington and Burstall 1976, Burstall and Darlington 1977, Arsac 1977). All of these techniques for obtaining correct programs must start from a specification. Verification, whether by hand or by machine, makes heavy weather even of non-trivial 'text-book' programs and still seems impractical for the much longer programs met with in practice. This comparative lack of success of verification techniques has obscured the fact that for large programs not only are we unable to carry through a correctness proof, but usually we cannot even specify the problem which the program is supposed to solve.* Similar remarks apply to program synthesis.

* For an overview of specification techniques, with many references, see Liskov and Berzins ( 1977).

There are exceptions. To specify a compiler, and hence verify it, you need to define the source language and the target machine. Scott and Strachey (1971 and subsequent papers) battled valiantly to give us precise semantic definitions of programming languages. Unfortunately, for large languages the specifications are very hard to understand (Robert Milne had one for Algol-68 which he declined to publish on the grounds that no-one would read it). We surmise that a good part of the trouble may be the lack of structure in such a formal definition, the structure that the writer of an informal manual for a language must be very careful to make clear. *

Thus we feel that a better grip on the way to st:ucture the theory in t erms of which specific­ atlons are made is a prerequisite for raising verification and synthesis techniques above the toy problem level. ·

Specifying AI problems

In AI research, as in other disciplines dealing with complex programs, there is a tendency to write the program but never get around to speci­ fying the problem. Further any large program must be composed of subprograms, and these cannot be understood without a clear specification of the subproblems they are supposed to solve. Thus better tools for problem specification at'e a pressing need in AI .

Not only s},otlld. the theories used in speci­ fying these problems and subproblems be well structured, they should also be sufficiently abstract . They should be concerned with the abstract nature of the data and the operations to be p~rformed rather than the particular problem doma1n or the specific machine representation of the data. For example Waltz's (1975) work is about the abstract notion of networks of relation~ rather than just about blocks and shadows or about LISP S-expressions; its full utility can only be exploited if this is kept in mind (see Mackworth 1977) . Our theory language must be able to handle such abstraction and enable us to hide unnecessary detail.

Representing knowledge within an AI program

AI programs are commonly conceived to embody knowledge, whether as program or as data. Proced­ ural. embedding of knowledge may promote efficiency, and 1t may enable one to use existing program structuring techniques to impose some order on the embed~ed knowledge. However procedural embedding has d1sadvantages of inflexibility, and it makes it ~ifficult to incorporate new knowledge, whether 1nput or from inductive learning. Much of the disquiet with knowledge held as data seems to us to stem from its lack of structure , a large collection of axioms or facts unorganised, slowing processing down with irrelevant information.

Again we are exhorted to consider our common­ sense knowledge of the world as composed of a large number of micro-theories about particular aspects . But we are left largely in the dark as to how to put these micro-theories together. This question of 'putting theories together' is close to the heart of our concern.

* Mosses (1977) makes a start in this direction.

Thus although we cannot yet speak from experience, we very much hope that our theory­ building techniques may eventually give some fresh insight into the appropriate organisation of knowledge in AI programs. A way of presenting theories so that people can under­ stand them might help us to see how machines can make use of them.

Theories

We start our exposition of the language Clear by looking more closely at the notion of many-sorted algebraic theory. Our theories will also make provision for errors, like division by zero, but we will defer consideration of this until we have the basic ideas straight.

First we need the notion of a signature, that is a vocabulary of operators with given sorts.

A signature is a set of sort names and a set of operator symbols, each with a given sequence of sorts for its arguments and a sequence of sorts for its results (possibly more than one result). We write~ : s 1 , ··· ,sm -> s{, ··· ,s~ to show that

w is an operator with input sorts s 1 , ··· ,sm and output sorts s;, ··· ,s~.*

Example 1 Natural numbers

sorts nat, bool

operations zero

-> nat

succ nat -> nat

is zero: nat -> bool

true -> bool

false - > bool

not bool -> bool

or bool, bool -> bool

Example 2 Geometry (a fragment)

~ line, point, bool

operations join point, point -> line

intersection: line, line -> point

colinear point,point,point->bool

true

-> bool

false

-> bool

not bool -> bool

A theory presentation is a signature together with a set of equations using the operators of the signature and respecting their input and output sorts . The equations have variables which are implicitly universally quantified.

Example 1 (continued)

variables m,n: nat

equations iszero(zero) = true iszero(succ(n)) = false not(true) =false not(false) = true

* for multi-result operators we could use a syn­ tax like "···<l···r ··· where <q,r> =quotient­ and-remaindertm,n)", but we will not need them.

Example 2 (continued)

variables p,q,r: point; l,m: line

A theory is a signature together with a set of equations closed under inference by reflexivit~ transitivity and symmetry of equality and by sub­ stitution. For example 'false = iszero(succ(succ (zero)))' is an equation in the theory defined by the presentation above.

Thus each theory presentation gives rise to a theory but the same theory can be presented in more than one way by choosing different sets of 'axiom' equations to generate it. (The notion of Theory is more basic than Theory Presentation in the sense that one would like to talk about the theory of groups,for example,irrespective of any particular axiomatisation of it.)*

The interpretations of a theory are algebras, where an algebra is a collection of sets, one for each sort, with a function over these sets assign­ ed to each operator of the theory. These func­ tions must obey the equations of the theory. In practice for theories containing bool we will only be interested in 'consistent' interpretations in which true I false.

Theory-building operations

In the last section we were just writing down theories explicitly one at a time. As soon as they get to be interesting they become incompre­ hensible. We wind up with a large set of equations .that no-one can understand and which are almost certainly wrong. So we must build our theories up from small intelligible pieces. For this we need

• (i) the ability to write (small!) explicit
• theories, as above, thus
• (ii) four operations on theories, combine,~, induce and ~. which enable us to build up theory expressions denoting complex
• theories.

theory sorts ···

opns ···

egns ··· ~

We will explain these operations informally,

First we define two explicit theories which will

using examples. be useful

The theory NatO

theory sorts nat

opns 0 -> nat

succ: nat -> nat

* Technically we should call this a 'theory with

signature' rather than just a 'theory' because the choice of a particular set of operators is irr~levant to the abstract notion, just as is the cho~ce of particular axioms (see Lawvere 1963 or Manes 1976).

The theory BoolO

theory sorts bool

opns true -> bool

false: -> bool

1 : bool -> bool

~: bool, bool - > bool

egns I true false

1 false true

false I\ p false

true 1\ p = p endth

(Strictly we ought to insert 'variable p: bool' before 'egns', but we will assume that undeclared single letter identifiers are variables; their type will be obvious. We will also allow our­

selves to use traditional infixed symbols like A·)

Combine

This operation is dull but plays its part in the larger scheme of things. We simply take two theories and add them together. The sorts of the resulting theories are the union of the sorts of the given theories, the operators are the union of their operators, and the equations are the union of their equations. We _use the+ sign for the combine operation.

For example BoolO + NatO could be written explicitly as

theory

sorts bool, nat

opns true : -> bool

false: -> bool

1 : bool -> bool

1\ : bool, bool -> bool

0: -> nat

succ: nat -> nat

egns 1 true = fal se

1 false = true

false A p = false

true A p = p endth

We will see later that combine does not necessarily produce the disjoint union of two theories; it allows for sharing of common sub­ theories.

~

Suppose that we want t o build up a useful theory of the natural numbers,including operators for ordering and for equality. The operators i and eq belong neither to BoolO nor NatO, but they can be added to their comb~nation to-oDtain a new theory

The theory Nat1

enrich BoolO + NatO ~ opns .S,: nat, nat -> bool

eq: nat, nat -> bool

0 < n = true

succ(m) ( 0 = false

- eq (m,n) = m ~ n 1\ n i m ~

succ(m) < succTn) = m < n

egns

This whole expression denotes the new

enriched theory.

In general one may add new sorts as well, thus

enrich

~ opns

egns

The enriched theory inherits all the sorts, operators and equations of the original one. The new operators can have as input and output sorts the original sorts or the new sorts.

Given the enrichment operation we could just start with the empty theory, say f , and regard any explicitly written theory as an enrichment of

I·

Induce

The theory ~ has an operator eq which satisfies not on~e three equations explicitly given but also by substitution, the equations

eq(O,O) = true

eq(succ(O),succ(O)) =true eq(succ(succ(O)),succ(succ(o))) true

and so on. But the equation

eq(n,n) true

is not inferable by substitution and is not part of the theory.

We would like to be able to extend the equations of a theory so that an equation holds for a variable, n, if it holds for every equation obtained by substituting a constant, that is a variable-free term, for n. So we have an oper­ ation induce on a theory which does just this.* Thus in the theory~ Nat1, which we will call Nat, the equations ----

eq(n,n~ = true

eq(m,n = eq(n,m)

reflexive symmetric

eq ( l,m I\ eq (m,n) I\, eq ( l,n) all hold. false transitive

To find equations holding in a theory created by ~ we may. prove by induction on the structure of terms, using the equations of the original theory, that a certain form of equation holds for every variable-free term; we may then assert that the form with a variable must hold in the induced theory. (Such methods of inference will not in general be complete how­ ever.)

In ]QQ1Q every variable-free term is equiv­ alent to true or false by using the equations for , and A , so it suffices to show that an equation holds for both true and false to see that the general . equation holds in~~- Induction here just amounts to case analysis:---For example II true = true and ,, false = false both hold in BoolO, so 11 p = p holds in ~ BoolO. We can-induce BoolO simply Bool. ----

Derive

The third operation derive enables us to take a more complex theory th~eed, perhaps built by combining and enriching some familiar theories, and then to select out from it just those sorts and operations which we require, For example, if we only need eq from Nat (and not ~ or zero or succ) we may write ---

*Technically, ·~! is the theory of the initial algebra of~

The' theory Nategual

derive

~ element, bool

opns equal, true, false

fro..!!!. Nat .£y

element fs nat

bool 1§. bool

equal is eq

true is true

false is false

This denotes a new theory with two sorts and three operators. The equations governing the new operator, equal, are not specified. Indeed we have only given the signature of the no~w thflnt·y. But thd pi·opertiflS pf ~qu:1l are given implicitly by the correspondence equal is eq. Notic.:t-> t.he.t the equations for eq use the auxiliary operator ~. In general an operator of the derived theory may correspond to a ~ -defined operator of the orig­ inal theory, thus "plus2 is f.n. succ(succ(n))" .

For brevity we will omit pairs of the form 'xis x', such as 'true is true'. Also if we already have a theory~ we may write'signature I' to denote its signature .

We use ~ when we want to define a theory in terms of some other theories with which we are already familiar but which, taken together, are too rich for our purpose. We are making a ~ struction from familiar mathematical objects, but the details of the construction are discarded in the more abstract result. An analogy would be the construction of the natural numbers in terms of the sets ¢, !¢},!¢, !¢} }, .... The operations we need on the natural numbers are, say, zero, successor and ~. Other possible operations on these sets, such as cartesian product of two sets, are not meaningful for numbers. In programming work it is well-known that the operations on an abstract data type are defined in terms of those on a more concrete type which represents it; but at the abstract program level the more concrete operationsshould not be available.

Procedures for theory-building

We have some primitive operations on theories. The next step is to enable the user to define his own operations using these. For this we intro­ duce procedures - no self-respecting language could be without them.

We shall introduce the simplest mechanisms which provide tolerably convenient facilities, namely

• (i) Theory constants, enabling us to give a name to a theory
• (ii) Theory procedures, taking theories as their parameters and producing a theory as a result. Their bodies use the primitive operations already defined and may call other theory procedures (but we eschew recursion!)

These facilities would be very similar what­ ever domain we were working in. Let us introduce them in the familiar domain of numbers and truth­ values as a warming up exercise . We will assume the primitives* (multiply), /~ivide) and if ··· then ··· else ···

A constant declaration, just assigning a fixed value to an identifier pi, would be

A procedure declaration for a procedure pro­ ducing a number as result would be

A procedure declaration with an auxiliary local variable z would be

Now if we evaluate ~(2) , z takes the value f(2*2, true), i.e. (22/7)*2*2, and g(2) is the cube of this value.

Now the same definitional methcds and syntax will apply to theories , using the theory-b~ilding operat~ons instead of *,if-then-else etc. ~ we do not need conditional expressions for theories) . We will need the type specification for parameter~ as in x : number, since it turns out that there is notion of type for theory parameters.

There is one major difference however between numbers and theories as a domain. Two theories may share some common subtheory. For example the theory of natural numbers has Bool as a sub­ theory since it has predicates like <, so does the theory of character strings which ha; predicates like isempty. We may want to enrich the combin­ ation of these two theories to allow operators

like length: string - > nat

In this new theory we want the truthvalues produced by ~ to be the same as those produced by isempty. We want one copy of Bool not two. Thus Bool is a shared subtheory. ----

Where .have we met this situation before? In LISP or any other language with pointers we have shared substructures. Let us see how the defin­ itional mechanisms we have introduced would behave with shared lists. We will then be ready to tackle theories. We need atoms "A, "B etc., the list constructor cons, the selectors car and cdr . and , crucially, the predicate eq which tests whether two lists are equal in the sense of starting with the same list cell, not just having the same shape. We will not use LISP syntax, but we intend LISP semantics, passing parameters by pointer than than co~ying the list structure. Let us look at examples \the intended values of the expression are given on the right)

true

Thus every use of a constant, parameter or local variable refers to the~ list, to within eq, but writing down an explicit expression twice using cons refers to a different list (i). Two different lists can share a common sublist (iii).

Now our theory- making operations , explicitly writing a theory and enriching one, behave just like cons. ~ut by using theory constants or variables we can arrange for the theories we create to contain shared sub-theories. One of our main technical problems was to make this remark precise, since for theories we do not have the address/value storage model as we do for data structures. In fact the category theory ideas of "diagram" and its "colimit" give a rather general notion of shared substructure . We hope that the reader's intuition using the LISP analogy will give him a reasonably good grip on the intended semantics . Those who wish to know the precise method for determining the denotation of our specifications must await the mathematical semantics in the paper which we are preparing.

The specification language Clear

We will call our proposed specification language "Cl ear". A specification in Clear con­ sists of a sequence of constant and procedure. declarations followed by an expression. The expression denotes a theory, not explicitly but using the theory-building operations and the declared constants and procedures.

Clear can be viewed as a language for com­ municating a precise specification of a problem to people, such as programmers. It could also be implemented on a machine so that 'evaluation' of a Clear specification yielded an explicit represent­ ation of the theory it denotes. A more useful implementation however would be to link Clear to an equational theorem prover which would try to prove that a given equation held in this theory without producingfue theory explicitly. Or it could be incorporated in a system which tried to show that a given program implemented some oper­ ations of this theory. This raises interesting, but still unanswered questions, about the relation between specification structure and program struc­ ture.

We will explain Clear by example. Let us start by building up the theory Nat of natural numbers using the constant facilTfY and the let facility, thus repeating in succinct form the more fragmentary development of Nat above. We start with Bool, the theory of truth values.

The constant Bool now denotes the theory of truth values , Since we applied the induce operation it also has equations such as 11 p = p obtained by case analysis .

The constant Nat now denotes the theory of natural numbers. 1t is built up by first making a local definition of the simple theory NatO with just zero and succ. We then combine th~s with Bool, enriching the combination with extra pred­ ~cates ~and eq, Finally~ applied to the whole expression ensures that the theory contains general equations like eq(m,m) = true.

Procedures in Clear

We often build one theory on top of another. Suppose for example that we have some partially ordered set, then we can "form strings from its elements and define the predicate 'ordered ' for strings . This is just what we would have to do if we wanted to specify some sorting task. A theory of ordered strings can be developed for any partially ordered se t (poset) of elements and the latter can be regarded as a theory parameter (compare Form parameters in ALPHARD). We can write a procedure using the theory- building oper­ ations to construct the theory of ordered strings from this parameter, Now we can apply this pro­ cedure to any theory which has a 'less than or equal' operator satisfying the reflexivity, transitivity and antisymmetry laws, for example the theory Nat. Thus the procedure can only accept as parameter a certain sort of theory; we had better call it a 'meta- sort ' to avoid con­ fusion with the sorts within theories, This ·meta­ sort is itself a theory, in this casethe theory of partial _orderings.

A degenerate example would be a theory pro­ cedure which can take any set as parameter and does not need any operators, for example the pro­ cedure which, given a set of elements, produces the theory of strings of those elements. The meta- sort here is the trivial theory with one sort and no operators.

~ Triv = theory sorts element endth

The theory procedure to make strings is then (proc being short for procedure)

proc Strings (_!: Tri v) =

induce enri"ch X .!?;r

sorts string

opns'unit: element-> string

.A. : -> string

· : string, string -> string

egns .A, s = s

S· J\. = S

(s , t ).u = s , (t.u) enden

As an example we can apply this procedure to Nat to get strings of natural numbers, but we neecr-­ to associate the sorts and operators of the meta­ sort (Triv)of the formal varameter with those of the actual parameter (Nat), that is we need a sort to sort function and a~perator to operator function just as in derive, We write these i n brackets after the actual parameter, thus

Strings (Nat [element is nat])

We may omit pairs of the form 'xis x'.

The actual parameter theory must include all the equations of the meta- sort theory as rewritten under thi s operator to operator func tion, We must prove this for every procedure application. Unlike conventional type checking it is not in general decideable.

Now to do ordered strings we need the theory of partial order for use as a meta- sort.

We can now write the procedure for ordered strings, We use the procedure Strings defined above .

Use of a theory as a meta-sort is rather distinct from its use in defining some data structure such as natural numbers. It enables us to state the presuppositions for some task which we wish to specify, and we are interested in any interpretation of the theory rather than some particular canonical one.

Shared subtheories

We observed already that just as two lists may share substructure so may two theories; this is accomplished by having the same variable appear in both the expressions denoting these theories . The details , which follow, are a little technical and may be skipped if desired.

Suppose that we have a theory variable :£., either a formal parameter or bound by a~.­ Then the theory "enrich! .2.Y_.,,enden" contains this theory! as a subtheory, and so do "! + ... " and "induce !'', The theory 11 derive signature !!_ from T2 .2.Y_ ·· :-endde" contains T as a subtheory if !!_~ontains it. Should T2 also contain! as a m:Ibtheory then the " ··· " nad better map its operators identically (if they both contain Bool, 11 true is false " would not be welcome) . Now rrwe combine two theories T1 and T2 which both have T as a subtheory then Ti+ T2 mny contains T oncir. The same rules hold rr T IS not a variable but is introduced by 11 ~!;;: ·· ·"· All this enables us to have ~. say, as-a subtheory of several theories"Without proliferating many copies of it. Sometimes we do need a fresh copy of a theory :£., so we let '' £QEL :£. 11 denote one, to save writing-it out again explic1tly.

When we apply a procedure E to an argument T the result always includes T~st as if we had - written ;E.('l') + ! instead o~(!). For example String (WaX) is-a theory whichnas not only strirg ~o~t also the operators like succ defined in Nat. Of course when we are writing the defini tloii ·of the procedure ~ these latter operators are not available, Lhe import­ ance of such 'insulation' mechanisms has been pointed out by Wulf and others.

Errors and conditionals

Before going on to look at examples of specifications written in Clear we will incor­ po:~<J.te· h10 UE·E·fu:_ features: errors anrl condit:i.on­ al:o;.

SomH applications of a!· ope:ratc-r to its >lrgur.Jents will not g:.ve a mea:1ingful result, for example dividing by zero or popping an empty stack. Thus we need to consider errors, a topic which is often glossed over in algebraically oriented work, but whose proper treatment is essential fbr a realistic specification language. It is important too that the different levels of abstraction provided by our language should not become confused as soon as an error is encoun­ tered; we do not want a stack underflow to pro­ duce an error message 'array subscript out of bounds '. Goguen (1977) studies this topic in depth, defining error algebras and error theories. We will confine ourselves to an informal glance

at error theories.

The idea is to extend each sort by a set of error elements of that sort, and to have error operators which produce these elements. Thus the theory of stacks might have an error operator

underflow: -> stack

and the theory of arrays might have an error operator

notdefinedfor: index - > value meaning that there is no value for this index in the array. The term 'notdefinedfor(7)' would serve as an informative error result.

To say when an error occurs or to equate two different error expressions we need to use error equations, thus

pop(empty) underflow

pop( underflow) underflow

We call the non- error elements of a sort "OK elements", the non-error operators "OK operators'' and the non-error equations "OK equations". Now we can write a presentation of a theory with a set of erroropns in addition to the previous (OK)opns, and a set of erroregns in addition to the previous (OK)egns. An interpretation of such a theory is an 'error algebra ' , that is an algebra some of whose elements are designated error elements . This designation must obey the following rules:-

1. Error operators always produce an error element ,
2. OK operators produce an error element if any of their arguments is an error element.

Now for an error algebra to satisfy an OK equation or an error equation does to hold for all values of the variables. following must be the case the theozy not have Only the

1. An OK equation mus t hold if both sides eval­ uate to an OK element.
2. An error equation must hold if either side evaluates to an error element.

For example

theory~ nat

opns zero: -> nat

succ : nat -> nat

pred: nat -> nat

erroropns neg: -> nat

egns pred(succ(n)) = n

erroregns pred(zero) = neg

succ(neg) neg

pred(neg) neg endth

Further examples, stack, array and symbol table, are given later.

It often happens that two expressions are equal only under a certain condition, thus

Now we can permit such a conditional equation by regarding it as an abbreviation for

where 'if' is the usual conditional operator defined for each type by the equations

Conditional axioms have been studied using a different approach by Thatcher, Wagner and Wright (1977).

Notice that the fact that our OK equations automatically do not appl y to error values often saves us from adding a condition such as "··· if sf, underflow" .

Notation

We should mention some small further points about notation. If we are naming sorts in a con­ text where several theories are present, the same sort name, s, may appear in two different theories, T1 and T2 making a reference to s ambiguous. We Bien simpiy refer to 11 s of T.r' or 11 s of T2 11 · A similar notation 11 f of Ti"" Wlll disamlii"guate operators. - Often a theory has a particular sort which is so to speak its raison d'etre, for example sort nat in theory Nat (even though ~also has sort bool). To enaDie us to distinguish such a sort we define the principal sort of a theory to be the first sort mentioned in its definition, thus in 'theory sorts s,t ·· · endth ' s is the principal sort and similarly in 'enrich T ~sorts s , t ·· · enden'. Now a helpful conven,ion is to allow the theory name, in lower case, to denote its princ­ ipal sort~ Also when we specify the corres­ pondence between sorts in a derive operation we may omit a pair 's is t ' if s and t are the principal sorts of their respective theories; similarly for the [ · · · ]notation used for actual parameters of procedures, thus 'Strings (Nat~ ' is acceptable for ' Strings(~ [element is~ ) ' .

Examples of specification

We will give two illustrations toffiow how Clear can be used to build up theories from pieces in a systematic way: -

• (i) a theory to specify a symbol table such as one might need in an Algol compiler (an example given by Guttag .!tt.& 1976)
• (ii) a theory to specify a problem solving system for a two dimensional blocks world.

These are, of course, rather small, simple examples, but we hope that they are just complex enough to give the reader some idea of the modular structure that we wish to see in specifications. We hope the reader can grasp this structure with­ out poring over every equation. ~he whole Clear description denotes a theory which does not itself have this structure, sc that the implementer would be at liberty to organise his program in some other way. 3 (Just as we might describe the number 19683 as 3 3 , but you are free to store it in the machine in any way you like, such as binary.) Indeed by using ~we 'throw away ' many of the operators introduced in our Clear description of the theory, so that they do not appear in the final theory and need have no corresponding pro­ cedures in the program which implements it . For example we describe a symbol table in terms of a stack of arrays, because stack and array are familiar concepts, but our specification does not demand that it be implemented in this way.

Here is our plan of campaign showing the main procedures or constants we will define and which other ones will use them.

We will use the theory~ of sets without defining it . The definition-should be fairly obvious . We will also use expressions of the form !f(x) : x E XA p(x)} instead of defining such sets by explicit equations.

Stack

Since we can put any kind of element on a stack we take as a parameter theory a trivial theory, one with a singl e sort and no operators . This describes the 'val ues ' which go on the stack. The operators, such as push and pop , are well­ known. Notice that no 'side- effects ' are allowe~ We explicitly produce a new stack from push and pop .

Array

We define arr ays with any kind of element as indices, not just integers . However the indices must have an equality r elation defined over them in order for us to 'look up' indices in the array, so we have a parameter theory of meta- sort Id , a theory of identifiers with one sort besides-cool and an equivalence operator == over that sort . We write the array access function as a[i] instead of, say, get (a,i) .

~

Symbol table

A compiler needs to maintain a symbol table relating each identifier to a value such as a machine address or an address plus a type. In an Algol-like language with blocks each block introduces new identifiers which may or may not have occurred before. It associates new values with them, and these override any previous values until the end of the block is encountered and the table reverts to its prior state. Thus we need a theory with sorts : symbol, value, table; it has operators: nilst - an empty table, extend - used to mark entry to a new block put - to add a symbol value pair, get(written ··· ( ··· ]) - to retrieve a value, contract - used when the end of the block is reached. Guttag ~ ~ (1976) have already given an equational specification of a symbol table as an abstract data structure. In contrast to their direct specification we will build up ours from the familiar concepts of stack and array, then use ~ to extract just those operations which are required for a symbol table.

proc Symtab (Symbol: Id, Value: Triv) = let Table = Stack (Array (Symbol, Value)) in ill 1'ab!e1 =eri'ffch Table~ ---

opns extend: tab~ table

putst : symbol,value,table -> table ··· [ ··· ]: table,symbol ->value nilst : -> table

erroropns undef: symbol -> value

eqns extend(t) = push(nilarray,t)

puts1(s, v, t)9lush(put ( s, v, top( t)) ,pop( t))

t[s] = top(t)fs~ if in(i,top(t))

t[s] = pop(t) s if, in(i top(t))

erroregns underflow s = undef(s) in

sorts table __ _

M 1. = enrich Symbol + Value E,y

opns nilst : -> table

extend: table -> table

putst : symbol,value,table -> table

··· [ ··· ]: table,symbol -> value

contract: table -> table

erroropns undef: symbol -> value ~ in

~signature 1. from Table1 .J:?.y

nilst is nilst~

contract ~ pop endde

Tabletop and Blocks World

Now let us specify a very crude model of a set of blocks on a tabletop together with some commands for moving them. We will stick to two dimensions and assume square blocks all of the same size. We can do this in terms of a one­ dimensional array indexed by places on the table, each element of the array is a stack of blocks. We enrich this array of stacks theory with some extra operations: create an empty array of stack~ put a block on the stack at a given place, move a block from the stack at a place onto the stack at another place. We now use derive to get rid of the unwanted operations on stacks and arrays, jus t retaining t hese operations on an array of stacks, which we rename a tabletop. We do however need an equality for tabletops , because later we want to do problem solving and see whether we have the required goal tabletop. For this we use a theory procedure Stackeg (Value: Id) of stacks with equality ( : stack~~ bool). Its defin­ ition from Stack (Value: Triv) by enrichment is left as an easy exerc1se. Similarly for Arrayeg (Index: Id, Value: Id).

proc Tabl~(Block: Id, Place: Id) =

let Stackofblo~ S"tackeg (BloCK") in

let Arrayofstacks = Arrayeg(~,Stackofblocks~n

let ! - enr1ch Arrayofstacks~

- opns empty: -5 arrayofst

put: place, block, arrayofst->arrayofst I!Dve: place, place, arrayofs t->arrayofst erroropns error: - > arrayofst

egns empty[p] =nil stack

put(p,b,a) = put(p,push(b,a[p]),a)

move(p,p',put(p,b,a)) = put(p' b a)

erroregns m011e(p,p ,a)=error:lf isempt:;(Jpj)

enden in

derive signature enrich~+~ .£y sorts tabletop

opns empty: - > tabletop

put place,block,tabletop -> tabletop

move place,place,tabletop -> table t op

tabletop, tabh·top ··> hoo.l

e:':'roTopns error: -> tahletop

~ !E.Y t~bletop is arrayofst ~nd~

The problem solver will seek a string of actions to t :ransform one tabletop to anoth·~r .. To provide thE·se b.ctior.s we define some commands, just expressions of the form "makemove(place1, place2)" using an operator "makemove" with no equations (like succ for numbers). Now we can define a dynamic Blocks World, in which you can execute commands to change the tabletop.

State-action system and Problem Solver

Quite separately from the Blocks World, but ~ter to be combined with it, we define a Problem Solver theory for some arbitrary system with states and actions. First we define the stateaction system alone with just these two sorts, then we have a procedure Iterate to enrich any state-action system to give ttie effect of a whole string of actions. A problem solver is then defined for such a system, with an operation solve which must attain any reachable set of goal states . Note that we do not say how solve is to be programmed, just specifyfrs desired result.

const State-action-system =

• ill State QOQOEOt Id in let Action =,mId in. enrich ~ +Action + Set (Action) EJL opns do: action,state =->"st~ acts: -> set(action) erroropns error: -> state ~
• proc Iterate (Sas: State-action-s stem let Action-st~ng-~~ elemen ~action]~ enrich Sas+Acb.on-'S"'triiig ]5[": opns aor act~on str~ng,state -> state egns do(nil,s) = s do(as.unit(a),s) = do(a,do(as,s)) enden

Blocks World Problem Solver

We now put this all together by deriving the required operations for a state-action system from the Blocks World, and applying the theory producing procedure Problem-Solver to it, The resulting theory spec~f~es the notion of solving a problem for our Blocks World, that is finding a sequence of suitable moves to get from one state to a specified set of states. (In practice we would have to add extra operators to describe the start and goal states.) We choose to represent blocks and places by natural numbers, but we leave as a parameter the set of natural numbers de.termining just which places are involved.

A number of questions arise from these

~

examples .

• (i) The language pays for the extra structure and localness by being rather cumbersome. Is this inevitable? We tried to moderate the longwindedness by some conventions, but feared to sprinkle too much sugar lest the reader lose sight of the basic mechanisms.
• (ii) Should we distinguish two kinds of enrich­ ment (a) adding new sorts and operators and equations about them, but without constrain­ ing existing operators further, (b) imposing further equations on the existing operators?
• (iii) Could we improve on the rather clumsy way sharing is indicated in derive?
• (iv) The induce operation is rather different from the others, a little mysterious. We stuck it in whenever we were talking about a part­ icular data structure. Could it be inserted more systematically? Perhaps we should distinguish between theories used as meta­ sorts , which generally do not need induce, and other theories, which generally do. Does induce allow us to make all the induc­ tive inferences we need?
• (v) Is our transfer of the LISP sharing paradigm to theories the best approach? Can we make good our claim to understand its semantics?

Programs and theory morphisms

In this section we discuss in a tentative way how programs, as opposed to specifications , might fit into our algebraic framework. For this we will need to define a 'morphism' between theories, which represents one theory in another . (The theories and their morphisms form a category, Lawvere 1963). The idea is that a program is essentially a means of representing one theory (the specification) in a~other theory (the machine), that is a morphism from one to the other.

We can often represent operators of one theory by operators of another, to be precise by derived operators of the other theory. By a derived operator of a theory we mean one which can be expressed in terms of the primitive oper­ ators. In a theory with primitives 'not' and 'and' the operator

?.xy. , (1x A1y)

is a derived operator (·or·). In general we may build any term in the primitive operators using suitable variables, using the familiar "}.. notation to bind these variables. These oper­ ators include nullary ones, that is constant terms. An operator may be represented by more than one derived operator of the other theory. Since our theories may involve several sorts we must also represent each sort of the first theory by a sort of the second.

Now the operators of the first theory obey certain equations, so naturally the same equations must be true of the corresponding derived oper­ ators of the second theory,

We call such a connection between two theories a theory morphism. Here is the definition.*

A theory morphism from a theory J to a theory ~· is

• (i) A function f from the sorts of T to the sorts of~·· We writes iss' to me~ f(s) = s'.
• (ii) A function g from the operators of T to nonempty sets of derived operators of f·, such that any equation of · gives rise to an equation of T' when each operator GJ of T is replaced by "in.y operator in g(iAI). The input and output sorts of an operator in g(~) must be the f-images of those of iAI. We write iAI is W 1 to mean g(~) = w 1 ·

By the obvious extension, the· theory morphism maps each derived operator of T to a set of derived operators of Z'; this""holds in particular for nullary operators i.e. constant terms.

Consider for example Id, the theory of ident­ ifiers with an equivalence-operator, and Nat the theory of natural numbers. We can define a mor­ phism from Id to Nat by

sorts identifier is nat

bool is bool

opns true

,

~: ~~;le}

is ,}

false is \false} A .!§. 1\}

Suppose that we enrich Nat with a multiplic­ ation operator to get, say, Natmult. Then we could have a morphism from Bool to Natmult

sorts bool is nat

opns false is 0,2,4, ·.· 1

true is 1,3,5 , .··

,

is succ}

A is *}

Representing sets by strings and stacks by array-index pairs are other well-known examples.

As a matter of fact such theory morphisms play an ess·ential role in our mathematical semantics for Clear. But here we are concerned with their connection with programs. It seems that if we restrict ourselves to an applicative language (without assignment) our theory morphisms are the mathematical correlate of a SIMULA class, CLU cluster or ALPHARD form, with the theory T playing ti:B (generalised) role of the newly define'a data type and the theory b' being the existing data type used to represent it. The derived operators in the morphism from J to ·· are the procedures in the class, cluster or form declaration.

We do need one generalisation however since in the programming case the procedures may well be recursive. Fortunately Wright, Thatcher, Wagner and Goguen (1976) have defined a notion of rationti theories and their morphisms** allowing recursive~

* Our theory morphisms are different from Lawvere's

which represent an operator by a single derived operator. · ·

** We would also need -:r.ati.onal theories to make Clear deal properly with infinite data, such as infinite trees, defined inductively.

derived operations (not just ~ but recursion too) ; this seems to model the real programming situation (always provided that we regard an imperative pro­ gram as a notational variant of an applicative one!).

Now we see that a specification is just a theory, a machine (or more abstractly the prim­ itive operators and sorts of a programming lang­ uage) is another theory, and a program to realise the specification is just a (rational) morphism from the specification theory to the machine theory.

Of course we should not describe this mor­ phism in an unstructured way, indeed there should be a programming language analogous to the specif­ ication language Clear, but describing morphisms not theories.** This would be the correlate of SIMULA etc. or more closely of the iota language of Nakajima et al, and of Parnas' (1972) method of programming with modules. We have worked on such a language but decided to first get straight the rather easier case of a specification lang­ uage.

How would the structure of such a program relate to the structure of. the specification which it implements? The degree of closeness would be up to the implementer, but it would be n~tural to use the various theories defined for specification purposes to define the task of subparts of the program. In general one would expect the specif­ ication would be simpler than the program, and to specify parts of the program one would need to elaborate the theories used in the specification with new sorts and operators. For example one might decide to use the GPS method to solve the blocks world problem, and one would have to enrich the state-action theory with new sorts like 'difference' and operators like 'reduces'.

A speculative conclusion: the main intel­ lectual task of programming is elaborating the theories which describe all the conce ts used in the actual program. Writing the code defining the morphisms) is a much more humdrum business.

Ah well! This is all delightfully vague and a great deal of work needs to be done. But it does promise to be interesting.

Conclusions

The main point of this paper is that it is pos sible to specify complex tasks provided that we do not try towrite the specifications in an unstructured way. Our particular language pro­ posal is only important in bringing into fbcus the problem of devising structured descriptions of specifications and suggesting the kind of oper­ ations which should be used to build them up. The basic ideas developed for data abstraction in programming languages should guide us in this task, and we firmly believe that the mathematical ideas about the category of theories can help us to grasp the rather deep concepts involved.

** We have a base for such development in the equational languages we have already implemented OBJ (Goguen and Tardo 1977) and NPL (Burstall

1977).

Acknowledgements

We owe a deep debt to the pioneers McCarthy, Landin, Eilenberg, MacLane and Lawvere, also to James Thatcher, Eric Wagner and Jesse Wright at IBM and to John Darlington at Edinburgh (now London) for long and educative collaboration. Many other colleagues have been very helpful especially Patrick Cousot (Grenoble), John Reynolds (Syracuse/ Edinburgh), Gordon Plotkin, David MacQueen and Jerald Schwarz (Edinburgh) and Joseph Tardo (Los Angeles) , J .A.G. wishes to thank Saunders MacLane for initiating him into category theory, and William Lawvere for help on the way, R.M.B. wishes to thank members of IFIP Working Group 2, 3 for much education and encourage­ ment , also Professor Veillon for a visit to USMG Grenoble· where he started on this work, and to Professor Avizienis for help in visiting Los Angeles. Alan Bundy and Michael Woodger kindl y read and made helpful comments on a draft .

We are grateful to the National Science Foundation and the Science Research Council for supporting this work , including an SRC Visiting Fellowship at Edinburgh for J .A.G.

• Our very sincere thanks to Eleanor Kerse for her meticulous, speedy and cheerful typing,
• Personal thanks go to Seija Burstall , Charlotte Linde and Chogyam Trungpa Rinpoche.