Foundations of Algebraic Specification and Formal Software Development

Donald Sannella and Andrzej Tarlecki

Foundations of Algebraic Specification and Formal Software Development

September 29, 2010

Springer

Contents

0 Introduction . . . . 1

0.1 Modelling software systems as algebras . . . . 1

0.2 Specifications . . . . 5

0.3 Software development . . . . 8

0.4 Generality and abstraction . . . 10

0.5 Formality . . . 12

0.6 Outlook . . . 14

1 Universal algebra . . . 15

1.1 Many-sorted sets . . . 15

1.2 Signatures and algebras . . . 18

1.3 Homomorphisms and congruences . . . 22

1.4 Term algebras . . . 27

1.5 Changing signatures . . . 32

1.5.1 Signature morphisms . . . 32

1.5.2 Derived signature morphisms . . . 36

1.6 Bibliographical remarks . . . 38

2 Simple equational specifications . . . 41

2.1 Equations . . . 41

2.2 Flat specifications . . . 44

2.3 Theories . . . 50

2.4 Equational calculus . . . 54

2.5 Initial models . . . 58

2.6 Term rewriting . . . 66

2.7 Fiddling with the definitions . . . 72

2.7.1 Conditional equations . . . 72

2.7.2 Reachable semantics . . . 74

2.7.3 Dealing with partial functions: error algebras . . . 78

2.7.4 Dealing with partial functions: partial algebras . . . 84

2.7.5 Partial functions: order-sorted algebras . . . 87

2.7.6 Other options . . . 91

2.8 Bibliographical remarks . . . 93

3 Category theory . . . 97

3.1 Introducing categories . . . 99

3.1.1 Categories . . . 99

3.1.2 Constructing categories . . . 105

3.1.3 Category-theoretic definitions . . . 109

3.2 Limits and colimits . . . 111

3.2.1 Initial and terminal objects . . . 111

3.2.2 Products and coproducts . . . 113

3.2.3 Equalisers and coequalisers . . . 115

3.2.4 Pullbacks and pushouts . . . 116

3.2.5 The general situation . . . 119

3.3 Factorisation systems . . . 123

3.4 Functors and natural transformations . . . 127

3.4.1 Functors . . . 128

3.4.2 Natural transformations . . . 135

3.4.3 Constructing categories, revisited . . . 139

3.5 Adjoints . . . 144

3.5.1 Free objects . . . 144

3.5.2 Left adjoints . . . 145

3.5.3 Adjunctions . . . 150

3.6 Bibliographical remarks . . . 152

4 Working within an arbitrary logical system . . . 155

4.1 Institutions . . . 157

4.1.1 Examples of institutions . . . 161

4.1.2 Constructing institutions . . . 179

4.2 Flat specifications in an arbitrary institution . . . 186

4.3 Constraints . . . 192

4.4 Exact institutions . . . 197

4.4.1 Abstract model theory . . . 204

4.4.2 Free variables and quantification . . . 207

4.5 Institutions with reachability structure . . . 210

4.5.1 The method of diagrams . . . 213

4.5.2 Abstract algebraic institutions . . . 215

4.5.3 Liberal abstract algebraic institutions . . . 216

4.5.4 Characterising abstract algebraic institutions that admit reachable initial models . . . 219

4.6 Bibliographical remarks . . . 221

Contents xvii

5 Structured specifications . . . 227

5.1 Specification-building operations . . . 228

5.2 Towards specification languages . . . 234

5.3 An example . . . 238

5.4 A property-oriented semantics of specifications . . . 243

5.5 The category of specifications . . . 247

5.6 Algebraic laws for structured specifications . . . 250

5.7 Bibliographical remarks . . . 255

6 Parameterisation . . . 257

6.1 Modelling parameterised programs . . . 258

6.2 Specifying parameterised programs . . . 268

6.3 Parameterised specifications . . . 274

6.4 Higher-order parameterisation . . . 278

6.5 An example . . . 285

6.6 Bibliographical remarks . . . 288

7 Formal program development . . . 291

7.1 Simple implementations . . . 292

7.2 Constructor implementations . . . 300

7.3 Modular decomposition . . . 307

7.4 Example . . . 314

7.5 Bibliographical remarks . . . 320

8 Behavioural specifications . . . 323

8.1 Motivating example . . . 324

8.2 Behavioural equivalence and abstraction . . . 327

8.2.1 Behavioural equivalence . . . 328

8.2.2 Behavioural abstraction . . . 333

8.2.3 Weak behavioural equivalence . . . 335

8.3 Behavioural satisfaction . . . 338

8.3.1 Behavioural satisfaction vs. behavioural abstraction . . . 342

8.4 Behavioural implementations . . . 346

8.4.1 Implementing specifications up to behavioural equivalence . 347 8.4.2 Stepwise development and stability . . . 348

8.4.3 Stable and behaviourally trivial constructors . . . 351

8.4.4 Global stability and behavioural correctness . . . 356

8.4.5 Summary . . . 363

8.5 To partial algebras and beyond . . . 364

8.5.1 Behavioural specifications in FPL . . . 364

8.5.2 A larger example . . . 371

8.5.3 Behavioural specifications in an arbitrary institution . . . 382

8.6 Bibliographical remarks . . . 394

9 Proofs for specifications . . . 399

9.1 Entailment systems . . . 400

9.2 Proof in structured specifications . . . 414

9.3 Entailment between specifications . . . 427

9.4 Correctness of constructor implementations . . . 435

9.5 Proof and parameterisation . . . 440

9.6 Proving behavioural properties . . . 451

9.6.1 Behavioural consequence . . . 451

9.6.2 Behavioural consequence for specifications . . . 463

9.6.3 Behavioural consequence between specifications . . . 466

9.6.4 Correctness of behavioural implementations . . . 470

9.6.5 A larger example, revisited . . . 472

9.7 Bibliographical remarks . . . 479

10 Working with multiple logical systems . . . 483

10.1 Moving specifications between institutions . . . 484

10.1.1 Institution semi-morphisms . . . 485

10.1.2 Duplex institutions . . . 489

10.1.3 Migrating specifications . . . 491

10.2 Institution morphisms . . . 500

10.3 The category of institutions . . . 509

10.4 Institution comorphisms . . . 517

10.5 Bibliographical remarks . . . 528

References . . . 533

Chapter 1

Universal algebra

The most basic assumption of work on algebraic specification is that programs are modelled as algebras. This point of view abstracts from the concrete details of code and algorithms, and regards the input/output behaviour of functions and the repre- sentation of data as primary. Representing programs in terms of sets (of data values) and ordinary mathematical functions over these sets greatly simplifies the task of reasoning about program correctness. See Section 0.1 for some illustrative exam- ples and more introductory discussion on this point.

The branch of mathematics that deals with algebras in this general sense (as opposed to the study of specific classes of algebras, such as groups and rings) is called universal algebra or sometimes general algebra. However, work on univer- sal algebra by mathematicians has concentrated almost exclusively on the special case of single-sorted algebras with first-order total functions. The generalisation to many-sorted or heterogeneous algebras is required to model programs that manip- ulate several kinds or sorts of data; further generalisations are necessary to handle programs that fail to terminate on some inputs, that generate exceptions during exe- cution, etc. This chapter summarizes the basic concepts and results of many-sorted universal algebra that will be required for the rest of this book. Some extensions useful for modelling more complex programs will be discussed later, in Section 2.7.

In this chapter, all proofs are left as exercises for the reader.

1.1 Many-sorted sets

When using an algebra to model a program which manipulates several sorts of data, it is natural to partition the underlying set of values in the algebra so that there is one set of values for each sort of data. It is often convenient to manipulate such a family of sets as a unit, in such a way that operations on this unit respect the “typing” of data values.

The following sequence of definitions and notational conventions allow us to ma-

nipulate sorted families of sets (of functions, of relations, . . . ) in just the same way

as ordinary sets (functions, relations, . . . ). Ordinary sets (functions, relations, . . . ) correspond to the degenerate case in which there is just one sort, so these definitions also serve to recall the notation and terminology of set theory to be used throughout this book. Let S be a set; the notation hX

i

is a standard shorthand for the family of objects X

indexed by s ∈ S, i.e. the function with domain S which maps each s ∈ S to X

.

Throughout this section, let S be a set (of sorts).

Definition 1.1.1 (Many-sorted set). An S-sorted set is an S-indexed family of sets X = hX

i

, which is empty if X

is empty for all s ∈ S. The empty S-sorted set will be written (ambiguously) as ∅. The S-sorted set X is finite if X

is finite for all s ∈ S and there is a finite set b S ⊆ S such that X

= ∅ for all s ∈ S \ b S.

Let X = hX

i

and Y = hY

i

be S-sorted sets. Union, intersection, Cartesian product, disjoint union, inclusion (subset) and equality of X and Y are defined com- ponentwise as follows:

X ∪Y = hX

∪Y

i

X ∩Y = hX

∩Y

i

X ×Y = hX

×Y

i

X ]Y = hX

]Y

i

(where X

]Y

= ({1} × X

) ∪ ({2} ×Y

)) X ⊆ Y iff (if and only if) X

⊆ Y

for all s ∈ S

X = Y iff X ⊆ Y and Y ⊆ X (equivalently, iff X and Y are equal as functions). u t Exercise 1.1.2. Give a formal explanation of the above statement that “Ordinary sets . . . correspond to the degenerate case [of many-sorted sets] in which there is

just one sort”. How many ∅-sorted sets are there? u t

Notation. It will be very convenient to pretend that X ⊆ X ] Y and Y ⊆ X ] Y . Al- though this is never actually the case, it allows us to treat disjoint union in the same way as ordinary union, the difference being that when X ∩ Y 6= ∅, X ] Y contains two “copies” of the common elements and keeps track of which copy is from X and which from Y . To see that this does not cause problems, observe that there are in- jective S-sorted functions (see the next definition) i1: X → X ] Y and i2:Y → X ] Y defined by i1

(x) = h1, xi for all s ∈ S and x ∈ X

and similarly for i2. A pedant would be able to correct what follows by simply inserting the functions i1 and/or i2

where appropriate in expressions involving ] . u t

Exercise 1.1.3. Extend the above definitions of union, intersection, product and dis- joint union to operations on I-indexed families of S-sorted sets, for an arbitrary in- dex set I. For example, the definition for product is (

hX

i

)

= { f : I →

(X

)

|

f (i) ∈ (X

)

for all i ∈ I} for each s ∈ S. u t

Definition 1.1.4 (Many-sorted function). Let X = hX

i

and Y = hY

i

be S-

sorted sets. An S-sorted function f : X → Y is an S-indexed family of functions f =

h f

: X

→ Y

i

; X is called the domain (or source) of f , and Y is called its codomain

(or target). An S-sorted function f : X → Y is an identity (an inclusion, surjective,

injective, bijective, . . . ) if for every s ∈ S, the function f

: X

→ Y

is an identity (an

1.1 Many-sorted sets 17

inclusion, surjective, injective, bijective, . . . ). The identity S-sorted function on X will be written as id

: X → X .

If f : X → Y and g:Y → Z are S-sorted functions then their composition f ;g : X → Z is the S-sorted function defined by f ;g = h f

;g

i

. That is, if s ∈ S and x ∈ X

then ( f ;g)

(x) = g

( f

(x)).

Let f : X → Y be an S-sorted function and X

⊆ X, Y

⊆ Y be S-sorted sets. The image of X

under f is the S-sorted set f (X

) = h f

(X

)i

⊆ Y , where f

(X

) = { f

(x) | x ∈ X

} ⊆ Y

for all s ∈ S. The coimage of Y

under f is the S-sorted set f

(Y

) = h f

(Y

)i

⊆ X, where f

(Y

) = {x ∈ X

| f

(x) ∈ Y

} ⊆ X

for all

s ∈ S. u t

Definition 1.1.5 (Many-sorted binary relation). Let X = hX

i

and Y = hY

i

be S-sorted sets. An S-sorted binary relation between X and Y , written R ⊆ X × Y , is an S-indexed family of binary relations R = hR

⊆ X

×Y

i

. For s ∈ S, x ∈ X

and y ∈ Y

, x R

y (sometimes written x R y) means hx, yi ∈ R

. u t The generalisation to n-ary relations, for n ≥ 0, is obvious. As usual, many-sorted functions may be viewed as special many-sorted relations.

Definition 1.1.6 (Kernel of a many-sorted function). Let f : X → Y be an S-sorted function. The kernel of f is the S-sorted binary relation ker( f ) = hker( f

)i

⊆ X × X where ker( f

) = {hx, yi | x, y ∈ X

and f

(x) = f

(y)} ⊆ X

× X

is the kernel

of f

for all s ∈ S. u t

Definition 1.1.7 (Many-sorted equivalence). Let X = hX

i

be an S-sorted set.

An S-sorted binary relation R ⊆ X × X is an S-sorted equivalence (relation) on X if it is:

• reflexive: xR

x;

• symmetric: xR

y implies yR

x; and

• transitive: xR

y and yR

z implies xR

z

for all s ∈ S and x, y, z ∈ X

. The symbol ≡ is often used for (S-sorted) equivalence relations.

Let ≡ be an S-sorted equivalence on X . If s ∈ S and x ∈ X

then the equivalence class of x modulo ≡ is the set [x]

= {y ∈ X

| x ≡

y}. The quotient of X modulo

≡ is the S-sorted set X/≡ = hX

/≡

i

where X

/≡

= {[x]

| x ∈ X

} for all

s ∈ S. u t

Example 1.1.8. Let S = {s

, s

}, and let X and Y be two S-sorted sets defined as follows:

X = hX

i

where X

= { 2,4} and X

= {♣, ♥, ♠}, Y = hY

i

where Y

= {1, 2, 3} and Y

= {1, 2, 3}.

Let f : X → Y be the S-sorted function such that

1This “diagrammatic” order of composition and the semicolon notation will be used consistently throughout this book.

f

= { 2 7→ 1,4 7→ 3}

f

= {♣ 7→ 1, ♥ 7→ 2, ♠ 7→ 2}.

(i.e., f

( 2) = 1 and f

(4) = 3; analogously for f

). Then the kernel of f is the S-sorted equivalence relation ker( f ) = hker( f

)i

where

ker( f

) = {h 2,2i,h4,4i}

ker( f

) = {h♣, ♣i, h♥, ♥i, h♥, ♠i, h♠, ♥i, h♠, ♠i}.

The quotient of X modulo ker( f ) is the S-sorted set X /ker( f ) = hX

/ker( f

)i

where

X

/ker( f

) = {{ 2},{4}}

X

/ker( f

) = {{♣}, {♥, ♠}}. u t

Exercise 1.1.9. Show that if f : X → Y is an S-sorted function, then ker( f ) is an S-

sorted equivalence on X . u t

Exercise 1.1.10. Show that if ≡ is an S-sorted equivalence on X then for all s ∈ S

and x, y ∈ X

, [x]

= [y]

iff x ≡

y. u t

Notation. Subscripts selecting components of S-sorted sets (functions, relations, . . . ) are often omitted when there is no danger of confusion. Then Exercise 1.1.10 would read: “. . . for all s ∈ S and x, y ∈ X

, [x]

= [y]

iff x ≡ y.” u t

1.2 Signatures and algebras

The functions and data types defined by a program have names. These names are used to compute with and reason about the program, and to build larger programs which rely on the functionality the program provides. The connection between a program and an algebra used to model it is provided by these names, which are at- tached to the corresponding components of the algebra. The set of names associated with an algebra is called its signature. The signature of an algebra defines the syntax of the algebra by characterising the ways in which its components may legally be combined; the algebra itself supplies the semantics by assigning interpretations to the names in the signature.

Definition 1.2.1 (Many-sorted signature). A (many-sorted) signature is a pair Σ = hS, Ω i, where:

• S is a set (of sort names); and

• Ω is an S

× S-sorted set (of operation names)

where S

is the set of finite (including empty) sequences of elements of S. We will

sometimes write sorts(Σ ) for S and ops(Σ ) for Ω . Σ is a subsignature of a signature

Σ

= hS

, Ω

i if S ⊆ S

and Ω

⊆ Ω

for all w ∈ S

, s ∈ S. u t

1.2 Signatures and algebras 19

Many-sorted signatures will be referred to as algebraic signatures when it is neces- sary to distinguish them from other kinds of signatures to be introduced later.

Notation. Saying that f : s

× · · · × s

→ s is in Σ = hS, Ω i means that s

. . . s

∈ S

, s ∈ S and f ∈ Ω

. Then f is said to have arity s

. . . s

and result sort s. The abbreviation f : s will be used for f : ε → s (ε is the empty sequence). u t This definition of signature does not accommodate programs containing higher- order functions, or functions returning multiple results. A possible extension to han- dle higher-order functions is briefly discussed in Section 2.7.6. As for functions with multiple results, a function f : s

× · · · × s

→ t

× · · · ×t

may be viewed as a family of m functions

f

: s

× · · · × s

→ t

. . . f

: s

× · · · × s

→ t

.

Generalising the definition of signature to handle such functions in a more di- rect way is easy but makes subsequent developments somewhat messier in a non- interesting way.

The definition above does permit overloaded operation names, since it is possible to have both f : s

× · · · × s

→ s and f :t

× · · · × t

→ t in a signature Σ , where s

. . . s

s 6= t

. . .t

t. A more restrictive definition of signature, adequate for most purposes, would have a set Ω of operation names (and a set S of sort names) with functions arity: Ω → S

and sort: Ω → S. These two definitions are equivalent if each operation name in Ω is taken to be tagged with its arity and result sort.

In the rest of this section, let Σ = hS, Ω i be a signature.

Definition 1.2.2 (Many-sorted algebra). A Σ -algebra A consists of:

• an S-sorted set |A| of carrier sets (or carriers); and

• for each f : s

× · · · × s

→ s in Σ , a function (or operation) ( f : s

× · · · × s

→

s)

: |A|

× · · · × |A|

→ |A|

. u t

If A is a Σ -algebra and s is a sort name in Σ then |A|

, the carrier set of sort s in A, is the universe of data values of sort s; accordingly, we often refer to the elements of carrier sets as values. If f : s

× · · · × s

→ s is in Σ then the operation ( f : s

× · · · × s

→ s)

is a function on the corresponding carrier sets of A. If n = 0 (i.e. f : s), then |A|

× · · · × |A|

is a singleton set containing the empty tuple hi, and then ( f : s)

may be viewed as a constant denoting the value ( f : s)

(hi) ∈ |A|

. Notice that ( f : s

× · · · × s

→ s)

is a total function

so algebras as defined here are only appropriate for modelling programs containing total functions. See Sections 2.7.3–

2.7.5 for several ways of extending the definitions to cope with partial functions.

Note also that there is no restriction on the cardinality of |A|

; in particular, |A|

may be empty and need not be countable.

Notation. Let A be a Σ -algebra and let f : s

× · · · × s

→ s be in Σ . We always write f

in place of ( f : s

× · · · × s

→ s)

when there is no danger of confusion. When n = 0 (i.e. f : s), we write ( f : s)

or f

in place of ( f : s)

(hi). u t

2All functions in this book are total except where they are explicitly designated as partial.

Exercise 1.2.3. If Ω

6= ∅ for some s ∈ S, then there are no hS, Ω i-algebras having an empty carrier of sort s. Characterise signatures for which all algebras have non-

empty carriers of all sorts. u t

Example 1.2.4. Let S1 = {shape, suit} and let Ω 1

= {box}, Ω 1

= {hearts}, Ω 1

= {boxify}, Ω 1

= { f }, and Ω 1

= ∅ for all other w ∈ S1

, s ∈ S1. Then Σ 1 = hS1, Ω 1i is a signature with sort names shape and suit and operation names box: shape, hearts: suit, boxify: shape → shape and f : shape × suit → suit. We can present Σ 1 in tabular form as follows (this notation will be used later with the obvious meaning):

Σ 1 = sorts shape, suit ops box: shape hearts: suit

boxify: shape → shape f : shape × suit → suit We define a Σ 1-algebra A1 as follows:

|A1|

= { 2,4},

|A1|

= {♣, ♥, ♠}, box

= 2 ∈ |A1|

, hearts

= ♥ ∈ |A1|

,

boxify

: |A1|

→ |A1|

= { 2 7→ 2,4 7→ 2},

and f

: |A1|

× |A1|

→ |A1|

is defined by the following table:

f

♣ ♥ ♠ 2 ♣ ♠ ♥ 4 ♥ ♠ ♠

(N

: Reference will be made to Σ 1 and A1 in examples throughout the rest of

this chapter.) u t

Definition 1.2.5 (Subalgebra). Let A and B be Σ -algebras. B is a subalgebra of A if:

• |B| ⊆ |A|; and

• for f : s

× · · · × s

→ s in Σ and b

∈ |B|

, . . . , b

∈ |B|

, f

(b

, . . . , b

) = f

(b

, . . . , b

).

B is a proper subalgebra of A if it is a subalgebra of A and |B| 6= |A|. A subalgebra of A is determined by an S-sorted subset |B| of |A| which is closed under the operations of Σ , i.e. such that for each f : s

× · · · × s

→ s in Σ and b

∈ |B|

, . . . , b

∈ |B|

,

f

(b

, . . . , b

) ∈ |B|

. u t

If B is a (proper) subalgebra of A then B is “smaller” than A in the sense that it

contains fewer data values than A. Both A and B are Σ -algebras though, so A and B

contain interpretations for exactly the same sort and operation names.

1.2 Signatures and algebras 21

Exercise 1.2.6. Let A be a Σ -algebra. Show that the intersection of any family of (carriers of) subalgebras of A is a (carrier of a) subalgebra of A. Use this to show that for any X ⊆ |A|, there is a least subalgebra of A that contains X . This is called the subalgebra of A generated by X . Give an explicit construction of this algebra.

(H

: Consider the family of S-sorted sets X

⊆ |A|, i ≥ 0, where X

= X and X

is obtained from X

by adding the results of applying the operations of A to arguments

in X

.) u t

Definition 1.2.7 (Reachable algebra). Let A be a Σ -algebra. A is reachable if A has no proper subalgebra (equivalently, if A is generated by ∅). u t By Exercise 1.2.6, every algebra has a unique reachable subalgebra.

Example 1.2.8. Let Σ 1 = hS1, Ω 1i and A1 be as defined in Example 1.2.4. Define a Σ 1-algebra B1 by

|B1|

= { 2},

|B1|

= {♥, ♠}, box

= 2 ∈ |B1|

, hearts

= ♥ ∈ |B1|

,

boxify

: |B1|

→ |B1|

= { 2 7→ 2},

f

: |B1|

× |B1|

→ |B1|

= {h 2,♥i 7→ ♠,h2,♠i 7→ ♥}.

B1 is the subalgebra of A1 generated by ∅. That is, B1 is the reachable subalgebra

of A1. u t

Definition 1.2.9 (Product algebra). Let A and B be Σ -algebras. The product alge- bra A × B is the Σ -algebra defined as follows:

• |A × B| = |A| × |B|; and

• for each f : s

× · · · × s

→ s in Σ and ha

, b

i ∈ |A × B|

, . . . , ha

, b

i ∈ |A × B|

, f

(ha

, b

i, . . . , ha

, b

i) = h f

(a

, . . . , a

), f

(b

, . . . , b

)i ∈ |A × B|

.

This generalises to the product

hA

i

of a family of Σ -algebras, indexed by an arbitrary set I (possibly empty), as follows:

• |

hA

i

| =

h|A

|i

; and

• for each f : s

× · · · × s

→ s in Σ and f

∈ |

hA

i

|

, . . . , f

∈ |

hA

i

|

, f Π

( f

, . . . , f

)(i) = f

( f

(i), . . . , f

(i)) for all i ∈ I. u t Exercise 1.2.10. Definition 1.2.9 shows how two Σ -algebras can be combined to form a new Σ -algebra by taking the Cartesian product of their carriers. According to Exercise 1.2.6, the same thing can be done (with subalgebras of a fixed algebra) using intersection. Try to formulate definitions of union and disjoint union of alge- bras, where |A ∪ B| = |A| ∪ |B| and |A ] B| = |A| ] |B| respectively. What happens?

u

t

1.3 Homomorphisms and congruences

A homomorphism between algebras is the analogue of a function between sets, and a congruence relation on an algebra is the analogue of an equivalence relation on a set. An algebra has more structure than a set, so homomorphisms and congruences are required to respect the additional structure (i.e. the behaviour of the operations).

Homomorphisms and congruences are important basic tools for relating algebras and constructing new algebras from old ones.

Throughout this section, let Σ = hS, Ω i be a signature.

Definition 1.3.1 (Homomorphism). Let A and B be Σ -algebras. A Σ -homomorphism h: A → B is an S-sorted function h: |A| → |B| which respects the operations of Σ , i.e. such that for all f : s

× · · · × s

→ s in Σ and a

∈ |A|

, . . . , a

∈ |A|

, h

( f

(a

, . . . , a

)) = f

(h

(a

), . . . , h

(a

)). A Σ -homomorphism h: A → B is an identity (an inclusion, surjective, . . . ) if it is an identity (an inclusion, surjective,

. . . ) when viewed as an S-sorted function. u t

Notation. If h: A → B is a Σ -homomorphism, then |h|: |A| → |B| denotes h viewed as an S-sorted function. The only difference between h and |h| is that in the case of

|h| we have “forgotten” that the additional condition required of a homomorphism

is satisfied. u t

Informally, the homomorphism condition says that the behaviour of the opera- tions in A is reflected in that of the operations in B. This condition can be expressed in the form of a diagram as follows:

|A|

× · · · × |A|

|A|

- h

× · · · × h

h

-

? f

|B|

× · · · × |B|

|B|

? f

where (h

×· · ·×h

)(a

, . . . , a

) = (h

(a

), . . . , h

(a

)) for all a

∈ |A|

, . . . , a

∈

|A|

. The homomorphism condition amounts to the requirement that this diagram commutes, i.e. that composing the functions on the top and right-hand arrows gives the same result as composing the functions on the left-hand and bottom arrows. Such commuting diagrams will be used heavily in later chapters, particularly in Chapter 3.

Example 1.3.2. Let Σ 1 = hS1, Ω 1i and A1 be as defined in Example 1.2.4. Define

a Σ 1-algebra C1 by

1.3 Homomorphisms and congruences 23

|C1|

= |C1|

= {1, 2, 3}, box

= 1 ∈ |C1|

,

hearts

= 2 ∈ |C1|

,

boxify

: |C1|

→ |C1|

= {1 7→ 1, 2 7→ 3, 3 7→ 1},

and f

: |C1|

× |C1|

→ |C1|

is defined by the following table:

f

1 2 3 1 1 2 3 2 2 1 2 3 2 2 1

Let h1: |A1| → |C1| be the S1-sorted function such that h1

= { 2 7→ 1,4 7→ 3},

h1

= {♣ 7→ 1, ♥ 7→ 2, ♠ 7→ 2}.

It is easy to verify that h1: A1 → C1 is a Σ 1-homomorphism by checking the fol- lowing:

h1

(box

) = box

h1

(hearts

) = hearts

h1

(boxify

( 2)) = boxify

(h1

( 2)) h1

(boxify

(4)) = boxify

(h1

(4))

h1

( f

( 2,♣)) = f

(h1

( 2),h1

(♣)) h1

( f

( 2,♥)) = f

(h1

( 2),h1

(♥)) h1

( f

( 2,♠)) = f

(h1

( 2),h1

(♠)) h1

( f

(4, ♣)) = f

(h1

(4), h1

(♣)) h1

( f

(4, ♥)) = f

(h1

(4), h1

(♥))

h1

( f

(4, ♠)) = f

(h1

(4), h1

(♠)). u t Exercise 1.3.3. Let A be a Σ -algebra. Show that id

: A → A (the identity S-sorted function) is a Σ -homomorphism. Let h: A → B and h

: B → C be Σ -homomorphisms.

Show that |h|;|h

|: |A| → |C| is a Σ -homomorphism h;h

: A → C. u t Exercise 1.3.4. Let h: A → B be a Σ -homomorphism, and let A

be a subalgebra of A. Let the image of A

under h be the Σ -algebra h(A

) defined as follows:

• |h(A

)| = |h|(|A

|); and

• for each f : s

×· · ·×s

→ s in Σ and a

∈ |A

|

, . . . , a

∈ |A

|

, f

(h

(a

), . . . , h

(a

)) = h

( f

(a

, . . . , a

)).

Show that h(A

) is a well-defined Σ -algebra (in particular, that the function f

: |h(A

)|

×

· · · × |h(A

)|

→ |h(A

)|

is well-defined for each f : s

× · · · × s

→ s in Σ ) and that it is a subalgebra of B. Formulate a definition of the coimage of a subalgebra B

of

B under h, and show that it is a subalgebra of A. u t

Exercise 1.3.5. Let h: A → B be a Σ -homomorphism, and suppose X ⊆ |A|. Show that the subalgebra of B generated by |h|(X ) ⊆ |B| is the image of the subalgebra of A generated by X . Show that it follows that if h: A → B is surjective and A is

reachable then B is reachable. u t

Exercise 1.3.6. Let B be a reachable Σ -algebra. Show that for any Σ -algebra A, there is at most one Σ -homomorphism h: B → A, and that any Σ -homomorphism h: A → B

is surjective. u t

Definition 1.3.7 (Isomorphism). Let A and B be Σ -algebras. A Σ -homomorphism h: A → B is a Σ -isomorphism if it has an inverse, i.e. there is a Σ -homomorphism h

: B → A such that h;h

= id

and h

;h = id

. (Exercise: Show that if h

exists then it is unique.) Then A and B are called isomorphic and we write h: A ∼ = B

or just A ∼ = B. u t

Exercise 1.3.8. Let h: A ∼ = B and h

: B ∼ = C be Σ -isomorphisms. Show that their com- position is a Σ -isomorphism h;h

: A ∼ = C. Show that ∼ = (as a binary relation on Σ - algebras) is reflexive and symmetric, and is therefore an equivalence relation. u t Two isomorphic algebras are typically regarded as indistinguishable for all practi- cal purposes. It is easy to see why: the only way in which they can differ is in the particular choice of data values in the carriers. The size of the carriers and the way that the operations behave on the values in the carriers is exactly the same. For this reason we are often satisfied with a definition of an algebra “up to isomorphism”, i.e. a description of an isomorphism class of algebras in a context where one would expect a definition of a single algebra. An example of this is in Fact 1.4.10 below.

The notion of isomorphism can be generalised to other kinds of structures, where it embodies exactly the same concept of indistinguishability. See Chapter 3 for this generalisation and for many more examples of definitions of objects “up to isomor- phism”.

Example 1.3.9. Let Σ 1 = hS1, Ω 1i and A1 be as defined in Example 1.2.4. Define a Σ 1-algebra D1 by

|D1|

= { 2,4},

|D1|

= {1, 2, 3}, box

= 4 ∈ |D1|

, hearts

= 2 ∈ |D1|

,

boxify

: |D1|

→ |D1|

= { 2 7→ 4,4 7→ 4},

and f

: |D1|

× |D1|

→ |D1|

is defined by the following table:

f

1 2 3 2 2 3 3 4 1 3 2 Let i1: |A1| → |D1| be the S1-sorted function such that

i1

= { 2 7→ 4,4 7→ 2}

i1

= {♣ 7→ 1, ♥ 7→ 2, ♠ 7→ 3}.

This defines a Σ 1-homomorphism i1: A1 → D1 which is a Σ 1-isomorphism, so A1 ∼ =

D1. u t

1.3 Homomorphisms and congruences 25

Exercise 1.3.10. Show that a homomorphism is an isomorphism iff it is bijective.

u t Exercise 1.3.11. Show that there is an injective homomorphism h: A → B iff A is

isomorphic to a subalgebra of B. u t

Example 1.3.12. Let Σ = hS, Ω i be the signature sorts s

ops a: s f : s → s

and define Σ -algebras A and B by

|A|

= Nat (the natural numbers), a

= 0 ∈ |A|

,

f

: |A|

→ |A|

= {n 7→ n + 1 | n ∈ Nat},

|B|

= {n ∈ Nat | the Turing machine with G¨odel number n halts on all inputs}, a

= the smallest n ∈ |B|

,

f

: |B|

→ |B|

= {n ∈ |B|

7→ the smallest m ∈ |B|

such that m > n}.

Let i: |A| → |B| be the S-sorted function such that i

(n) = the (n + 1)

smallest element of |B|

for all n ∈ |A|

. The function i

is well-defined since |B|

is infinite. This defines a Σ -homomorphism i: A → B which is an isomorphism.

Although A ∼ = B, the Σ -algebras A and B are not “the same” from the point of view of computability: everything in A is computable, in contrast to B (|B|

is not recursively enumerable and f

is not computable). Isomorphisms capture structural similarity, ignoring what the values in the carriers are and what the operations actu- ally compute. This example shows that, for some purposes, properties stronger than

structural similarity are important. u t

Definition 1.3.13 (Congruence). Let A be a Σ -algebra. A Σ -congruence on A is an (S-sorted) equivalence ≡ on |A| which respects the operations of Σ : for all f : s

× · · · × s

→ s in Σ and a

, a

∈ |A|

, . . . , a

, a

∈ |A|

, if a

≡

a

and . . . and a

≡

a

then f

(a

, . . . , a

) ≡

f

(a

, . . . , a

). u t Exercise 1.3.14. Show that the intersection of any family of Σ -congruences on A is a Σ -congruence on A. Use this to show that for any S-sorted binary relation R on |A|

there is a least (with respect to ⊆) Σ -congruence on A which includes R.

Show that the kernel of any Σ -homomorphism h: A → B is a Σ -congruence on A.

Show that a surjective Σ -homomorphism is an isomorphism iff its kernel is the

identity. u t

Definition 1.3.15 (Quotient algebra). Let A be a Σ -algebra, and let ≡ be a Σ -

congruence on A. The quotient algebra of A modulo ≡ is the Σ -algebra A/≡ defined

by:

• |A/≡| = |A|/≡; and

• for each f : s

×· · ·×s

→ s and a

∈ |A|

, . . . , a

∈ |A|

, f

([a

]

s1

, . . . , [a

]

) =

[ f

(a

, . . . , a

)]

. u t

Exercise 1.3.16. Show that A/≡ in Definition 1.3.15 is a well-defined Σ -algebra.

u t Example 1.3.17. Let Σ 1 = hS1, Ω 1i and A1 be as defined in Example 1.2.4, and let

≡ = h≡

i

be the S1-sorted binary relation on |A1| defined by

≡

= {h 2,2i,h4,4i}

≡

= {h♣, ♣i, h♥, ♥i, h♥, ♠i, h♠, ♥i, h♠, ♠i}.

This defines a congruence on A1. A1/≡ is the Σ 1-algebra defined by

|A1/≡|

= {{ 2},{4}},

|A1/≡|

= {{♣}, {♥, ♠}}, box

= { 2} ∈ |A1/≡|

, hearts

= {♥, ♠} ∈ |A1/≡|

,

boxify

: |A1/≡|

→ |A1/≡|

= {{ 2} 7→ {2},{4} 7→ {2}},

and f

: |A1/≡|

× |A1/≡|

→ |A1/≡|

is defined by the following table:

f

{♣} {♥, ♠}

{2} {♣} {♥, ♠}

{4} {♥, ♠} {♥, ♠} u t

Exercise 1.3.18. Let ≡ be a Σ -congruence on A, and let h

(a) = [a]

for s ∈ S, a ∈ |A|

. Show that hh

: |A|

→ (|A|/≡)

i

is a Σ -homomorphism h: A → A/≡ with

ker(h) = ≡. u t

Exercise 1.3.19. Let h: A → B be a Σ -homomorphism. Show that A/ker(h) is iso- morphic to h(A). (H

: The isomorphism is given by [a]

7→ h

(a) for s ∈ S,

a ∈ |A|

.) u t

Exercise 1.3.20. Let ≡ be a Σ -congruence on A. Show that for any Σ -homomorphism h: A → B such that ≡ ⊆ ker(h), there exists a unique Σ -homomorphism g: A/≡ → B such that h

(a) = g

([a]

) for all s ∈ S, a ∈ |A|

. u t Exercise 1.3.21. Show that there is a surjective homomorphism h: A → B iff there is

a congruence ≡ on A such that B is isomorphic to A/≡. u t

Exercise 1.3.22. Let A be a Σ -algebra, let ≡ be a congruence on A and let B be a subalgebra of A/≡. Show that there is a subalgebra C of A and congruence ≡

on

C such that B = C/≡

. u t

Exercise 1.3.23. Let h: A → B be a Σ -homomorphism. Show that there is a unique

Σ -congruence ≡ on A and a unique injective Σ -homomorphism g: A/≡ → B such

that h

(a) = g

([a]

) for all s ∈ S, a ∈ |A|

. u t

1.4 Term algebras 27

1.4 Term algebras

For any signature Σ there is a special Σ -algebra whose values are just well-formed terms (i.e. expressions) built from the operation names in Σ . A Σ -algebra of terms with variables is similarly determined by a signature Σ = hS, Ω i and an S-sorted set of variables. These algebras are rather boring insofar as modelling programs is concerned — the term algebra models a program which does no real computation.

But the homomorphisms from these algebras to other algebras turn out to be very useful technical tools, as shown by the definitions below.

Throughout this section, let Σ = hS, Ω i be a signature and let X be an S-sorted set (of variables), where x ∈ X

for s ∈ S means that the variable x is of sort s (written x: s). Note that “overloading” of variable names is permitted here, since there is no requirement that X

and X

be disjoint for s 6= s

∈ S.

Definition 1.4.1 (Term algebra). The Σ -algebra T

(X ) of terms with variables X is the Σ -algebra defined as follows:

• |T

(X )| is the least (with respect to ⊆) S-sorted set of words (sequences) over the alphabet

S ∪

w∈S^∗ s∈S

Ω

∪

s∈S

X

∪ {: , ( , , , )}

such that:

– the word “x: s” ∈ |T

(X )|

for all s ∈ S and x ∈ X

; and

– for all f : s

× · · · × s

→ s in Σ and all words t

∈ |T

(X )|

, . . . ,t

∈ |T

(X )|

, the word “ f (t

, . . . ,t

): s” ∈ |T

(X )|

.

• for all f : s

× · · · × s

→ s in Σ and all words t

∈ |T

(X )|

, . . . ,t

∈ |T

(X )|

, f

Σ(X )

(t

, . . . ,t

) = (the word) “ f (t

, . . . ,t

): s” ∈ |T

(X )|

.

(Quotation marks are used here solely to emphasize that terms are words, and are not part of the words they delimit.) If s ∈ S and t ∈ |T

(X )|

then t is a Σ -term of sort s with variables X ; the free variables of t is the set FV(t) ⊆ X of variables that actually occur in t: for s ∈ S and x ∈ X

, x ∈ FV(t)

if t contains the subword “x: s”.

The Σ -algebra of ground terms is the Σ -algebra T

= T

(∅) of terms without variables. If s ∈ S and t ∈ |T

|

then t is a ground Σ -term. u t The values of T

(X ) are “fully-typed” terms formed using the variables in X and the operation names in Σ , and the operations of T

(X ) just build complicated terms from simpler terms. Note that a term t ∈ |T

(X )| need not contain all the variables in X , and that some variables may occur more than once in t. T

is also called the Σ -word algebra, and its carriers |T

| are sometimes called the Herbrand universe for Σ .

Example 1.4.2. Let Σ 1 = hS1, Ω 1i be as defined in Example 1.2.4. Then T

is the

Σ 1-algebra defined by

|T

|

= { “box(): shape”,

“boxify(box(): shape): shape”,

“boxify(boxify(box(): shape): shape): shape”, . . . },

|T

|

= { “hearts(): suit”,

“ f (box(): shape, hearts(): suit): suit”,

“ f (boxify(box(): shape): shape, hearts(): suit): suit”,

“ f (box(): shape, f (box(): shape, hearts(): suit): suit): suit”, . . . }

where the operations of T

are the term formation operations box

= “box(): shape” ∈ |T

|

,

hearts

= “hearts(): suit” ∈ |T

|

, boxify

Σ 1

: |T

|

→ |T

|

= { “box(): shape” 7→ “boxify(box(): shape): shape”,

“boxify(box(): shape): shape” 7→ “boxify(boxify(box(): shape): shape): shape”, . . . },

and similarly for f : shape × suit → suit. u t

Notation. Sort decorations (e.g. “: shape” in “box(): shape”) are often unambigu- ously determined, and they will usually be omitted when this is the case. When Ω

∩ X

= ∅ for some s ∈ S, then variables of sort s cannot be confused with con- stants (0-ary operations) of sort s and so we will usually drop the parentheses “()”

in the latter. We will omit quotation marks whenever it is clear from the context that we are dealing with terms. Finally, in examples we will use infix notation for binary

operations when convenient. u t

Example 1.4.2 (revisited). We repeat Example 1.4.2, making use of these nota- tional conventions.

Let Σ 1 = hS1, Ω 1i be as defined in Example 1.2.4. Then T

is the Σ 1-algebra defined by

|T

|

= {box, boxify(box), boxify(boxify(box)), . . .},

|T

|

= {hearts, f (box, hearts), f (boxify(box), hearts), f (box, f (box, hearts)), . . .}

where the operations of T

are the term formation operations box

= box ∈ |T

|

,

hearts

= hearts ∈ |T

|

, boxify

Σ 1

: |T

|

→ |T

|

= {box 7→ boxify(box), boxify(box) 7→ boxify(boxify(box)), . . .},

and similarly for f : shape × suit → suit. u t

Example 1.4.3. The notational conventions above will almost always be applicable.

They cannot be adopted from the outset (i.e. in Definition 1.4.1) because of the

relatively rare examples where confusion can arise. For example, let Σ 2 = hS2, Ω 2i

1.4 Term algebras 29

be the signature with sorts s, s

,t and operations a: s, a: s

, f : s → t and f : s

→ t (no mistakes here, repetition of names is intented).

According to the definition, |T

|

= {“ f (a(): s):t”, “ f (a(): s

):t”}. If all sort dec- orations were omitted then both of the terms in this set would become “ f (a())” and so |T

|

would have just this single element. The “outer” decoration can be omitted but the “inner” decoration is required, thus e.g. “ f (a(): s)”.

Similarly, if X is an S2-sorted set of variables such that a ∈ X

, then “ f (a(): s)”

and “ f (a: s)” are different terms in |T

(X )|

, so the convention of writing “a(): s”

as “a: s” cannot be used.

Since the definitions permit variables and operation names like f (a(): s) and even

“ or , or (), the custom of writing terms as sequences of symbols without explicit separators can cause confusion. Luckily, such names never arise in practice and so for the purposes of this book this problem can safely be forgotten. u t Fact 1.4.4. For any Σ -algebra A and S-sorted function v: X → |A| there is exactly one Σ -homomorphism v

: T

(X ) → A that extends v, i.e. such that v

(ι

(x)) = v

(x) for all s ∈ S, x ∈ X

, where ι

: X → |T

(X )| is the embedding that maps each variable in X to its corresponding term.

S-sorted sets Σ -algebras

X |T

(X )|

|A|

⊂ ι

-

?

|v

|

@

@

@

@

@

@

@ R v

T

(X )

A

? v

u t The existence and uniqueness of v

follow easily from the requirement that v

ex- tends v (this fixes the value of v

for any variable as a term in |T

(X )|) and that v

is a Σ -homomorphism (this determines the value of v

for any term f (t

, . . . ,t

) ∈

|T

(X )| as a function of the values of v

for its immediate subterms t

, . . . ,t

∈

|T

(X )|). The homomorphism which results is the function which evaluates Σ -terms based on the assignment of values in A to variables in X given by v.

Definition 1.4.5 (Term evaluation). Let A be a Σ -algebra A and let v: X → |A| be an S-sorted function. By Fact 1.4.4 there is a unique Σ -homomorphism v

: T

(X ) → A that extends v. Let s ∈ S and let t ∈ |T

(X )|

be a Σ -term of sort s; the value of t in A under the valuation v is v

(t) ∈ |A|

. When t ∈ |T

|

the value of t does not depend on v; then the value of t in A is ∅

(t) where ∅: ∅ → |A| is the empty function.

To make the algebra explicit, we write t

(v) for v

(t), and t

for t

(∅) when t is

ground. u t