2 Algebraic Preliminaries

Donald Sannella^{1} and Andrzej Tarlecki^{2}

1 Laboratory for Foundations of Computer Science, University of Edinburgh, Edinburgh, Scotland

  dts@dcs.ed.ac.uk  http://www.dcs.ed.ac.uk/~dts/

2 Institute of Informatics, Warsaw University and Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland

  tarlecki@mimuw.edu.pl  http://wwwat.mimuw.edu.pl/~tarlecki/

The purpose of this chapter is to present the basic definitions and results on which the following chapters rely. Most of this material is quite standard and for that reason the presentation will be concise. More detailed presentations with greater emphasis on motivation, exercises, and examples may be found in [EM85, Wir90, LEW96, ST].

The most basic assumption of work on algebraic specification is that a program is modeled as an algebra, that is, a set of data together with a number of functions over this set. The branch of mathematics which deals with algebras in a 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. This chapter presents the basics of universal algebra, generalized to the many-sorted case as required to model programs which manipulate several kinds or sorts of data. Some extensions useful for modeling more complex programs are sketched at the end of the chapter.

2.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.

Let S be a set (of sorts). An S-sorted set is an S-indexed family of sets X = ⟨X_{s}⟩_{s∈S}, which is empty if X_{s} is empty for all s ∈ S. The empty S-sorted set is written ∅.

Let X = ⟨X_{s}⟩_{s∈S} and Y = ⟨Y_{s}⟩_{s∈S} be S-sorted sets. Union, intersection, Cartesian product, disjoint union, inclusion (subset), and equality of X and Y are defined as follows:

X ∪ Y = ⟨X_{s} ∪ Y_{s}⟩_{s∈S}
X ∩ Y = ⟨X_{s} ∩ Y_{s}⟩_{s∈S}
X × Y = ⟨X_{s} × Y_{s}⟩_{s∈S}

X ⊎ Y = ⟨X_{s} ⊎ Y_{s}⟩_{s∈S} (where X_{s} ⊎ Y_{s} is the disjoint union of X_{s} and Y_{s}) X ⊆ Y iff X_{s} ⊆ Y_{s} for all s ∈ S X = Y iff X ⊆ Y and Y ⊆ X.

An S-sorted function f: X → Y is an S-indexed family of functions f = ⟨f_{s}: X_{s} → Y_{s}⟩_{s∈S}; X is called the domain of f, and Y is called its codomain. An S-sorted function f: X → Y is an identity (an inclusion, surjective, injective, bijective, …) if for every s ∈ S, the function f_{s}: X_{s} → Y_{s} is an identity (an inclusion, surjective, injective, bijective, …). The identity S-sorted function on X will be written as id_{X}: 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)_{s}(x) = g_{s}(f_{s}(x)) for s ∈ S and x ∈ X_{s}.

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′) = ⟨{f_{s}(x) | x ∈ X′_{s}}⟩_{s∈S} ⊆ Y. The coimage of Y′ under f is the S-sorted set f^{−1}(Y′) = ⟨{x ∈ X_{s} | f_{s}(x) ∈ Y′_{s}}⟩_{s∈S} ⊆ X.

An S-sorted binary relation on X, written R ⊆ X × X, is an S-indexed family of binary relations R = ⟨R_{s} ⊆ X_{s} × X_{s}⟩_{s∈S}. For s ∈ S and x, y ∈ X_{s}, xR_{s}y (sometimes written xRy) means ⟨x, y⟩ ∈ R_{s}. R is an S-sorted equivalence (relation) on X if it is reflexive (xR_{s}x), symmetric (xR_{s}y implies yR_{s}x), and transitive (xR_{s}y and yR_{s}z implies xR_{s}z). The symbol ≡ is often used for (S-sorted) equivalence relations.

Let ≡ be an S-sorted equivalence on X. If s ∈ S and x ∈ X_{s}, then the equivalence class of x modulo ≡ is the set [x]_{≡_{s}} = {y ∈ X_{s} | x ≡_{s} y}. The quotient of X modulo ≡ is the S-sorted set X/≡ = ⟨{[x]_{≡_{s}} | x ∈ X_{s}}⟩_{s∈S}.

Let f: X → Y be an S-sorted function. The kernel of f is the S-sorted equivalence relation K(f) = ⟨{⟨x, y⟩ ∈ X_{s} × X_{s} | f_{s}(x) = f_{s}(y)}⟩_{s∈S} ⊆ X × X.

Subscripts selecting components of S-sorted sets (functions, relations, …) are often omitted where there is no danger of confusion.

2.2 Signatures and algebras

An algebra consists of named sets and named functions on these sets. The set of names associated with an algebra is called its signature. The signature of an algebra defines the syntax of the algebra; the algebra itself supplies the semantics by assigning interpretations to the names.

A (many-sorted) signature is a pair Σ = ⟨S, Ω⟩, where S is a set (of sort names) and Ω is an S^{∗} × S-sorted set (of operation names). Here, S^{∗} is the set of finite (including empty) sequences of elements of S. We will sometimes write sorts(Σ) for S and opns(Σ) for Ω. Σ is a subsignature of Σ′ = ⟨S′, Ω′⟩ if S ⊆ S′ and Ω ⊆ Ω′.

Saying that f: s_{1}×⋯×s_{n} → s is in Σ = ⟨S, Ω⟩ means that s_{1} … s_{n} ∈ S^{∗}, s ∈ S, and f ∈ Ω_{s_{1}...s_{n},s}. Then f is said to have arity s_{1} … s_{n} and result sort s. If n = 0, that is f: → s, we use the abbreviation f: s.

Many-sorted signatures will be referred to as algebraic signatures when it is necessary to distinguish them from other kinds of signatures to be introduced later. The above definition of signature permits overloading, since it is possible to have different arities and result sorts for a single operation name.

In the rest of this section, let Σ = ⟨S, Ω⟩ be a signature.

A Σ-algebra A consists of an S-sorted set |A| of carrier sets (or carriers); and, for each f: s_{1} × ⋯ × s_{n} → s in Σ, a function (or operation) (f: s_{1} × ⋯ × s_{n} → s)_{A}: |A|_{s_{1}} × ⋯ × |A|_{s_{n}} → |A|_{s}. The class of all Σ-algebras will be denoted by Alg(Σ).

If f: s_{1} × ⋯ × s_{n} → s is in Σ for n = 0 (i.e., f: s), then |A|_{s_{1}} × ⋯ × |A|_{s_{n}} is a singleton set containing the empty tuple ⟨⟩, and so (f: s)_{A} may be viewed as a constant denoting the value (f: s)_{A}(⟨⟩) ∈ |A|_{s}. Notice that (f: s_{1} ×⋯×s_{n} → s)_{A} is a total function; see Section 2.10 for several ways of extending the definitions to cope with partial functions. Note also that there is no restriction on the cardinality of |A|_{s}; in particular, |A|_{s} may be empty (but not if, e.g., Ω_{ε,s} ≠ ∅).

We always write f_{A} in place of (f: s_{1} × ⋯ × s_{n} → s)_{A} where there is no possibility of confusion.

Example 2.1. Let S1 = {food, car} and let Ω1_{ε,food} = {soup}, Ω1_{ε,car} = {vw}, Ω1_{food,food} = {boil}, Ω1_{food car,car} = {f}, and Ω1_{w,s} = ∅ for all other w ∈ S1^{∗}, s ∈ S1. Then Σ1 = ⟨S1, Ω1⟩ is a signature which can be presented in tabular form as follows:

Σ1 = sorts food, car
opns soup : food
vw : car

boil : food → food f: food × car → car

Let |A1|_{food} = {⊕, ⊗}, |A1|_{car} = {a, b, c}, soup_{A1} = ⊕ ∈ |A1|_{food}, vw_{A1} = b ∈ |A1|_{car} and boil_{A1} : |A1|_{food} → |A1|_{food} = {⊕ ↦ ⊕, ⊗ ↦ ⊕}, and let f_{A1} : |A1|_{food} × |A1|_{car} → |A1|_{car} be defined by the following table:

\begin{matrix}f_{A1} & a & b & c \\ ⊕ & a & c & b \\ ⊗ & b & c & c \end{matrix}

This defines a Σ1-algebra A1. Reference will be made to Σ1 and A1 in examples throughout the rest of this chapter.

Let A and B be Σ-algebras. B is a subalgebra of A if |B| ⊆ |A|, and if f_{B}(b_{1}, …, b_{n}) = f_{A}(b_{1}, …, b_{n}) for any f: s_{1} × ⋯ × s_{n} → s in Σ and b_{1} ∈ |B|_{s_{1}}, …, b_{n} ∈ |B|_{s_{n}}. B is a proper subalgebra of A if it is a subalgebra of A and |B| ≠ |A|. A subalgebra of A is determined by an S-sorted subset |B| of |A| such that for each f: s_{1}×⋯×s_{n} → s in Σ and b_{1} ∈ |B|_{s_{1}}, …, b_{n} ∈ |B|_{s_{n}}, f_{A}(b_{1}, …, b_{n}) ∈ |B|_{s}.

The intersection of any family of (carriers of) subalgebras of A is a (carrier of a) subalgebra of A. This implies that for any X ⊆ |A|, there is a least subalgebra of A that contains X, called the subalgebra of A generated by X. A is reachable if it has no proper subalgebra (equivalently, if A is generated by ∅). It follows that every algebra has a unique reachable subalgebra.

Example 2.2. Let Σ1 = ⟨S1, Ω1⟩ and A1 be as in Example 2.1. Define a Σ1-algebra B1 by |B1|_{food} = {⊕}, |B1|_{car} = {b, c}, soup_{B1} = ⊕ ∈ |B1|_{food}, vw_{B1} = b ∈ |B1|_{car}, boil_{B1} : |B1|_{food} → |B1|_{food} = {⊕ ↦ ⊕}, and f_{B1} : |B1|_{food} × |B1|_{car} → |B1|_{car} = {⟨⊕, b⟩ ↦ c, ⟨⊕, c⟩ ↦ b}. B1 is the subalgebra of A1 generated by ∅. That is, B1 is the reachable subalgebra of A1.

2.3 Homomorphisms and congruences

A homomorphism between algebras is a function between the carrier sets which preserves the operations. Similarly, a congruence relation on an algebra is an equivalence which is preserved by the operations.

Throughout this section, let Σ = ⟨S, Ω⟩ be a signature and let A and B be Σ-algebras.

A Σ-homomorphism h: A → B is an S-sorted function h: |A| → |B| such that for all f: s_{1} × ⋯ × s_{n} → s in Σ and a_{1} ∈ |A|_{s_{1}}, …, a_{n} ∈ |A|_{s_{n}}, h_{s}(f_{A}(a_{1}, …, a_{n})) = f_{B}(h_{s_{1}}(a_{1}), …, h_{s_{n}}(a_{n})).

Example 2.3. Let Σ1 = ⟨S1, Ω1⟩ and A1 be as in Example 2.1. Define a Σ1algebra B1 by |B1|_{food} = |B1|_{car} = {1, 2, 3}, soup_{B1} = 1 ∈ |B1|_{food}, vw_{B1} = 2 ∈ |B1|_{car} and boil_{B1} : |B1|_{food} → |B1|_{food} = {1 ↦ 1, 2 ↦ 3, 3 ↦ 1}, where f_{B1} : |B1|_{food} × |B1|_{car} → |B1|_{car} is defined by the following table:

\begin{matrix}f_{B1} & 1 & 2 & 3 \\ 1 & 1 & 2 & 3 \\ 2 & 2 & 1 & 2 \\ 3 & 2 & 2 & 1 \end{matrix}

Let h1: |A1| → |B1| be the S1-sorted function such that h1_{food} = {⊕ ↦ 1, ⊗ ↦ 3} and h1_{car} = {a ↦ 1, b ↦ 2, c ↦ 2}. It is easy to verify that h1: A1 → B1 is a Σ1-homomorphism by checking the following:

h1_{food}(soup_{A1}) = soup_{B1}
h1_{car}(vw_{A1}) = vw_{B1}
h1_{food}(boil_{A1}(⊕)) = boil_{B1}(h1_{food}(⊕))
h1_{food}(boil_{A1}(⊗)) = boil_{B1}(h1_{food}(⊗))
h1_{car}(f_{A1}(⊕, a)) = f_{B1}(h1_{food}(⊕), h1_{car}(a))
h1_{car}(f_{A1}(⊕, b)) = f_{B1}(h1_{food}(⊕), h1_{car}(b))
h1_{car}(f_{A1}(⊕, c)) = f_{B1}(h1_{food}(⊕), h1_{car}(c))
h1_{car}(f_{A1}(⊗, a)) = f_{B1}(h1_{food}(⊗), h1_{car}(a))
h1_{car}(f_{A1}(⊗, b)) = f_{B1}(h1_{food}(⊗), h1_{car}(b))
h1_{car}(f_{A1}(⊗, c)) = f_{B1}(h1_{food}(⊗), h1_{car}(c)).

The identity function on the carrier of a Σ-algebra is a Σ-homomorphism, and composition of Σ-homomorphisms yields another Σ-homomorphism.

Let h: A → B be a Σ-homomorphism, and let A′ be a subalgebra of A. Let the image of A′ under h be the Σ-subalgebra h(A′) of B such that |h(A′)| = h(|A′|), and f_{h(A′)}(h_{s_{1}}(a_{1}), …, h_{s_{n}}(a_{n})) = h_{s}(f_{A′}(a_{1}, …, a_{n})) for each f: s_{1} × ⋯ × s_{n} → s in Σ and a_{1} ∈ |A′|_{s_{1}}, …, a_{n} ∈ |A′|_{s_{n}}. The coimage of a subalgebra B′ of B under h is a subalgebra h^{−1}(B′) of A, defined analogously.

A Σ-homomorphism h: A → B is a Σ-isomorphism if it has an inverse, i.e., there is a Σ-homomorphism h^{−1} : B → A such that h;h^{−1} = id_{|A|} and h^{−1};h = id_{|B|}. A homomorphism is an isomorphism iff it is bijective.

If there is an isomorphism from A to B, they are called isomorphic and we write h: A ≅ B or just A ≅ B. Then ≅ (as a binary relation on Σ-algebras) is reflexive, symmetric, and transitive, and is therefore an equivalence relation.

Two isomorphic algebras are typically regarded as indistinguishable for all practical purposes: the only way in which they can differ is in the particular choice of data values in the carriers.

Example 2.4. Let Σ1 = ⟨S1, Ω1⟩ and A1 be as in Example 2.1. Define a Σ1algebra B1 by |B1|_{food} = {⊕, ⊗}, |B1|_{car} = {1, 2, 3}, soup_{B1} = ⊗ ∈ |B1|_{food}, vw_{B1} = 2 ∈ |B1|_{car}, and boil_{B1} : |B1|_{food} → |B1|_{food} = {⊕ ↦ ⊗, ⊗ ↦ ⊗}, where f_{B1} : |B1|_{food} × |B1|_{car} → |B1|_{car} is defined by the following table:

\begin{matrix}f_{B1} & 1 & 2 & 3 \\ ⊕ & 2 & 3 & 3 \\ ⊗ & 1 & 3 & 2 \end{matrix}

Let i1: |A1| → |B1| be the S1-sorted function such that i1_{food} = {⊕ ↦ ⊗, ⊗ ↦ ⊕} and i1_{car} = {a ↦ 1, b ↦ 2, c ↦ 3}. This defines a Σ1homomorphism i1: A1 → B1 which is a Σ1-isomorphism, so A1 ≅ B1.

A Σ-congruence on A is an (S-sorted) equivalence ≡ on |A| which respects the operations of Σ: for all operations f: s_{1} × ⋯ × s_{n} → s in Σ and values a_{1}, a′_{1} ∈ |A|_{s_{1}}, …, a_{n}, a′_{n} ∈ |A|_{s_{n}}, if a_{1} ≡_{s_{1}} a′_{1} and … and a_{n} ≡_{s_{n}} a′_{n} then f_{A}(a_{1}, …, a_{n}) ≡_{s} f_{A}(a′_{1}, …, a′_{n}).

The intersection of any family of Σ-congruences on A is a Σ-congruence on A, which implies that for any S-sorted binary relation R on |A| there exists a least (with respect to ⊆) Σ-congruence on A which includes R.

Let ≡ be a Σ-congruence on A. The quotient of A modulo ≡ is the Σ-algebra A/≡ such that |A/≡| = |A|/≡, and f_{A/≡}([a_{1}]_{≡_{s_{1}}} , …, [a_{n}]_{≡_{sn}}) = [f_{A}(a_{1}, …, a_{n})]_{≡_{s}} for each f: s_{1} × ⋯ × s_{n} → s and a_{1} ∈ |A|_{s_{1}}, …, a_{n} ∈ |A|_{s_{n}}.

Example 2.5. Let Σ1 = ⟨S1, Ω1⟩ and A1 be as in Example 2.1, and let ≡ = ⟨≡_{s}⟩_{s∈S1} be the S1-sorted congruence on |A1| defined by ≡_{food} = {⟨⊕, ⊕⟩, ⟨⊗, ⊗⟩} and ≡_{car} = {⟨a, a⟩, ⟨b, b⟩, ⟨b, c⟩, ⟨c, b⟩, ⟨c, c⟩}. A1/≡ is the Σ1-algebra defined by

|A1/≡|_{food} = {{⊕}, {⊗}}, |A1/≡|_{car} = {{a}, {b, c}},
soup_{A1/≡} = {⊕} ∈ |A1/≡|_{food}, vw_{A1/≡} = {b, c} ∈ |A1/≡|_{car},
boil_{A1/≡}: |A1/≡|_{food} → |A1/≡|_{food} = {{⊕} ↦ {⊕}, {⊗} ↦ {⊕}},

where f_{A1/≡}: |A1/≡|_{food} ×|A1/≡|_{car} → |A1/≡|_{car} is defined by the following table:

\begin{matrix}f_{A1/≡} & \{a\} & \{b, c\} \\ \{⊕\} & \{a\} & \{b, c\} \\ \{⊗\} & \{b, c\} & \{b, c\} \end{matrix}

The kernel of any Σ-homomorphism h: A → B is a Σ-congruence on A. Moreover, if ≡ is a Σ-congruence on A, and h_{s}(a) = [a]_{≡_{s}} for s ∈ S, a ∈ |A|_{s}, then ⟨h_{s}: |A|_{s} → (|A|/≡)_{s}⟩_{s∈S} is a Σ-homomorphism h: A → A/≡. Therefore, a binary relation on |A| is a Σ-congruence on A iff it is the kernel of a Σ-homomorphism from A.

Proposition 2.6. Let ≡ be a Σ-congruence on A. If h: A → B is a Σhomomorphism such that ≡ ⊆ K(h), then there is a unique Σ-homomorphism g: A/≡ → B such that h_{s}(a) = g_{s}([a]_{≡_{s}}) for all s ∈ S and a ∈ |A|_{s}.

The above property characterizes quotient algebras up to isomorphism. It follows in particular that for any Σ-homomorphism h: A → B, A/K(h) is isomorphic to h(A).

2.4 Term algebras

Throughout this section, let Σ = ⟨S, Ω⟩ be a signature and let X be an Ssorted set (of variables), where x ∈ X_{s} 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_{s} and X_{s′} be disjoint for s ≠ s′ ∈ S.

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

• |T_{Σ}(X)| is the least S-sorted set such that x ∈ |T_{Σ}(X)|_{s} for all s ∈ S and x ∈ X_{s}, and f(t_{1}, …, t_{n}) ∈ |T_{Σ}(X)|_{s} for all f: s_{1} × ⋯ × s_{n} → s in Σ and t_{1} ∈ |T_{Σ}(X)|_{s_{1}}, …, t_{n} ∈ |T_{Σ}(X)|_{s_{n}},

• for all f: s_{1} × ⋯ × s_{n} → s in Σ and t_{1} ∈ |T_{Σ}(X)|_{s_{1}}, …, t_{n} ∈ |T_{Σ}(X)|_{s_{n}}, f_{T_{Σ}(X)}(t_{1}, …, t_{n}) = f(t_{1}, …, t_{n}) ∈ |T_{Σ}(X)|_{s}.

Note the distinction between syntactic term formation f(t_{1}, …, t_{n}) and the application of the operation named f. If s ∈ S and t ∈ |T_{Σ}(X)|_{s}, 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.

The Σ-algebra of ground terms is the Σ-algebra T_{Σ} = T_{Σ}(∅) of terms without variables. If s ∈ S and t ∈ |T_{Σ}|_{s}, then t is a ground Σ-term.

Example 2.7. Let Σ1 = ⟨S1, Ω1⟩ be as in Example 2.1. Then T_{Σ1} is the Σ1-algebra defined by

|T_{Σ1}|_{food} = {soup(), boil(soup()), boil(boil(soup())), … },

|T_{Σ1}|_{car} = \begin{cases}vw(), f(soup(), vw()), f(boil(soup()), vw()), \\ f(soup(), f(soup(), vw())), … \} \end{cases}

where the operations of T_{Σ1} are the term-formation operations

soup_{T_{Σ1}} = soup() ∈ |T_{Σ1}|_{food}, vw_{T_{Σ1}} = vw() ∈ |T_{Σ1}|_{car},

boil_{T_{Σ1}} : |T_{Σ1}|_{food} → |T_{Σ1}|_{food} = \begin{cases}soup() ↦ boil(soup()), \\ boil(soup()) ↦ boil(boil(soup())), … \}, \end{cases}

and similarly for f: food × car → car.

It is implicitly assumed above that the result sort of each term is determined unambiguously. If the signature Σ and the set of variables X do not ensure this property, then appropriate sort decorations must be added to terms. We will henceforth assume that variables and constants (0-ary operations) of the same sort are distinct, which allows us to drop the parentheses “()” in terms like boil(soup()) above. So, in the example we would have:

|T_{Σ1}|_{food} = {soup, boil(soup), … },
|T_{Σ1}|_{car} = {vw, f(soup, vw), f(boil(soup), vw), … }

In examples we will also use infix notation for binary operations when convenient.

Let A be a Σ-algebra, v: X → |A| be an S-sorted function, s ∈ S, and t ∈ |T_{Σ}(X)|_{s} be a Σ-term of sort s. The value of t in A under the valuation v is v^{#}(t) ∈ |A|_{s}, defined as follows:

• v^{#}(x) = v(x) for all s ∈ S and x ∈ X_{s}; and

• v^{#}(f(t_{1}, …, t_{n})) = f_{A}(v^{#}(t_{1}), …, v^{#}(t_{n})) for all f: s_{1} × ⋯ × s_{n} → s in Σ and t_{1} ∈ |T_{Σ}(X)|_{s_{1}}, …, t_{n} ∈ |T_{Σ}(X)|_{s_{n}}.

Proposition 2.8. For any Σ-algebra A and S-sorted function v: X → |A|, v^{#} : T_{Σ}(X) → A is the unique Σ-homomorphism that extends v, i.e., such that v_{s}^{#}(x) = v_{s}(x) for all s ∈ S, x ∈ X_{s}.

It is easy to see that the value of a term t ∈ |T_{Σ}(X)| depends only on the valuation of variables in FV (t). In particular, the value of a ground term t ∈ |T_{Σ}| does not depend on the valuation. Hence we write t_{A} = ∅^{#}(t), where ∅: ∅ → |A| is the empty function, for the value of t in A.

The Σ-algebra A is reachable iff every element in |A| is the value of a ground Σ-term, or equivalently, iff it is isomorphic to a quotient of T_{Σ}. It follows that there is a one-to-one correspondence between isomorphism classes of reachable Σ-algebras and congruences on T_{Σ}.

When the algebra A above is a term algebra T_{Σ}(Y) for some S-sorted set Y, valuations are called substitutions (of terms in T_{Σ}(Y) for variables), and the value of a term t under a substitution θ: X → |T_{Σ}(Y)|, written t[θ], is just the result of substituting θ(x) for all x in t in the usual sense. We write t[x ↦ u] for the result of replacing x in t by u, regarding x ↦ u as a shorthand for the obvious substitution which is the identity on all variables in X other than x (here, Y is X ∪ FV (u)).

2.5 Signature morphisms

A signature morphism defines a mapping from the sort and operation names in one signature to those in another signature, in such a way that the arity and result sort of operations are respected.

More formally, let Σ = ⟨S, Ω⟩ and Σ′ = ⟨S′, Ω′⟩ be signatures. A signature morphism σ: Σ → Σ′ is a pair σ = ⟨σ_{sorts}, σ_{opns}⟩ where σ_{sorts} : S → S′ and σ_{opns} = ⟨σ_{w,s}: Ω_{w,s} → Ω′_{σ_{sorts}^{∗}(w),σ_{sorts}(s)}⟩_{w∈S^{∗},s∈S} (where for w = s_{1} … s_{n} ∈ S^{∗}, σ_{sorts}^{∗}(w) = σ_{sorts}(s_{1}) … σ_{sorts}(s_{n})). Both σ_{sorts} and σ_{opns} (and its components σ_{w,s} for all w ∈ S^{∗}, s ∈ S) will be denoted by σ.

Signature morphisms as defined above will be referred to as algebraic signature morphisms when it is necessary to distinguish them from other kinds of signature morphisms to be introduced later.

Example 2.9. Let Σ = ⟨S, Ω⟩ be the signature

sorts warm, cold, vehicle
opns borscht : cold

heat : cold → warm heat : warm → warm h: warm × vehicle → vehicle Let Σ1 = ⟨S1, Ω1⟩ be the signature in Example 2.1. Define σ_{sorts} : S → S1 and σ_{opns} = ⟨σ_{w,s}: Ω_{w,s} → Ω1_{σ_{sorts}^{∗}(w),σ_{sorts}(s)}⟩_{w∈S^{∗},s∈S} by σ_{sorts} = {warm ↦ food, cold ↦ food, vehicle ↦ car}, σ_{ε,cold} = {borscht ↦ soup}, σ_{cold,warm} = {heat ↦ boil}, σ_{warm,warm} = {heat ↦ boil}, σ_{warm vehicle,vehicle} = {h ↦ f}, and σ_{w,s} = ∅ for all other w ∈ S^{∗}, s ∈ S. Then σ: Σ → Σ1 is a signature morphism.

In the rest of this section, let σ: Σ → Σ′ be a signature morphism. This gives rise to a translation of Σ-terms to Σ′-terms, and of Σ′-algebras and homomorphisms to Σ-algebras and homomorphisms, as defined below. Note that the direction of translation of algebras and homomorphisms is “backwards” with respect to the direction of the signature morphism.

Let A′ be a Σ′-algebra. The σ-reduct of A′ is the Σ-algebra A′ _{σ} such that |A′ _{σ}|_{s} = |A′|_{σ(s)} for all s ∈ S, and f_{A′ _{σ}} = σ(f)_{A′} for all f: s_{1} ×⋯×s_{n} → s in Σ. Similarly, if h′: A′ → B′ is a Σ′-homomorphism, the σ-reduct of h′ is the Σ-homomorphism h′ _{σ}: |A′ _{σ}| → |B′ _{σ}| such that (h′ _{σ})_{s} = h′_{σ(s)} for all s ∈ S.

If Σ is a subsignature of Σ′, then we write A′ _{Σ} for A′ _{σ} where σ: Σ → Σ′ is the obvious signature inclusion (and similarly for homomorphisms). Then A′ _{Σ} is just A′ with some carriers and/or operations removed.

Example 2.10. Let σ: Σ → Σ1 and A1 be as in Examples 2.9 and 2.1 respectively. Then A1 _{σ} is the Σ-algebra such that |A1 _{σ}|_{warm} = |A1 _{σ}|_{cold} = {⊕, ⊗} = |A1|_{food}, |A1 _{σ}|_{vehicle} = {a, b, c} = |A1|_{car}, borscht_{A1 _{σ}} = ⊕ = soup_{A1}, (heat : cold → warm)_{A1 _{σ}} = {⊕ ↦ ⊕, ⊗ ↦ ⊕} = boil_{A1}, (heat : warm → warm)_{A1 _{σ}} = {⊕ ↦ ⊕, ⊗ ↦ ⊕} = boil_{A1} and h_{A1 _{σ}} = {⟨⊕, a⟩ ↦ a, ⟨⊕, b⟩ ↦ c, … } = f_{A1}.

Let X be an S-sorted set of variables such that X_{s} and X_{s′} are disjoint for s ≠ s′ ∈ S. Define X′ = ⟨⋃_{σ(s)=s′} X_{s}⟩_{s′∈S′}. The translation of a Σ-term t ∈ |T_{Σ}(X)| by σ is the Σ′-term σ(t) ∈ |T_{Σ′}(X′)| obtained by replacing each operation name f in t by σ(f). (The disjointness assumption on X is for notational convenience only. It may be avoided by taking the disjoint union in the definition of X′.)

Example 2.11. Let σ: Σ → Σ1 be the signature morphism in Example 2.9, where Σ = ⟨S, Ω⟩ and Σ1 = ⟨S1, Ω1⟩. Let X be the S-sorted set of variables x: cold, x′: warm, y: warm, z: vehicle. The S1-sorted set of variables X′ is then x: food, x′: food, y: food, z: car, and

σ(h(heat(x), h(x′, z))) = f(boil(x), f(x′, z)),
σ(h(x′, h(heat(heat(borscht)), z))) = f(x′, f(boil(boil(soup)), z)),

and so on.

The following result states that the value of a term is invariant under change of signature.

Proposition 2.12. Let X be an S-sorted set of variables such that X_{s} and X_{s′} are disjoint for s ≠ s′ ∈ S, and X′ = ⟨⋃_{σ(s)=s′} X_{s}⟩_{s′∈S′}. Let A′ be a Σ′-algebra and v′: X′ → |A′| be a valuation. Define v: X → |A′ _{σ}| by v_{s}(x) = v′_{σ(s)}(x) for s ∈ S and x ∈ X_{s}. Then for any Σ-term t ∈ |T_{Σ}(X)|, v^{#}(t) = (v′)^{#}(σ(t)). In particular, if t is a ground term, then t_{A′ _{σ}} = σ(t)_{A′}.

2.6 Equations

In the simple algebraic specifications considered in this chapter, equations are used as axioms to constrain the permitted behaviour of operations.

Throughout this section, let Σ = ⟨S, Ω⟩ be a signature.

A Σ-equation ∀X. t = t′ consists of an S-sorted set X (of variables) such that X_{s} and X_{s′} are disjoint for s ≠ s′ ∈ S, and two Σ-terms t, t′ ∈ |T_{Σ}(X)|_{s} for some sort s ∈ S. A Σ-equation ∀∅. t = t′, sometimes abbreviated t = t′, is called a ground (Σ-) equation.

A Σ-algebra A satisfies (or, is a model of ) a Σ-equation ∀X. t = t′, written A ⊧_{Σ} ∀X. t = t′, if for every (S-sorted) function v: X → |A|, v^{#}(t) = v^{#}(t′).

A satisfies (or, is a model of) a set Φ of Σ-equations, written A ⊧_{Σ} Φ, if A ⊧_{Σ} φ for every equation φ ∈ Φ. A class A of Σ-algebras satisfies a Σ-equation φ, written A ⊧_{Σ} φ, if A ⊧_{Σ} φ for every A ∈ A. Finally, a class A of Σ-algebras satisfies a set Φ of Σ-equations, written A ⊧_{Σ} Φ, if A ⊧_{Σ} Φ for every A ∈ A. We sometimes write ⊧ in place of ⊧_{Σ} where Σ is obvious.

The explicit quantification over X in a Σ-equation ∀X. t = t′ is essential. For example, if |A|_{s} = ∅ but X_{s} ≠ ∅ for some s in S, then A trivially satisfies any equation ∀X. t = t′. Thus variables in X may influence satisfaction even if they do not actually occur in t or t′.

Satisfaction of Σ-algebras is preserved under subalgebras and homomorphic images: if A ⊧ φ then φ is satisfied by any subalgebra of A and by any homomorphic image of A (and thus by any algebra isomorphic to A).

Let σ: Σ → Σ′ be a signature morphism. The translation of Σ-terms to Σ′-terms defined above extends in the obvious way to a translation of Σequations to Σ′-equations. We will write σ(∀X. t = t′) for ∀X′. σ(t) = σ(t′), where X′_{s′} = ⋃_{σ(s)=s′} X_{s} for each s′ ∈ S′ as above.

An important result that brings together some of the main definitions above is as follows:

Lemma 2.13 (Satisfaction Lemma [BG80]). If σ: Σ → Σ′ is a signature morphism, φ is a Σ-equation, and A′ is a Σ′-algebra, then A′ ⊧_{Σ′} σ(φ) iff A′ _{σ} ⊧_{Σ} φ.

This states that the translations of syntax (terms, equations) and semantics (algebras) induced by signature morphisms are coherent with the definition of satisfaction. The proof follows from Proposition 2.12.

2.7 Presentations and theories

A signature, together with a set of equations over that signature, constitutes a simple form of specification. We refer to these as flat (meaning unstructured) specifications in order to distinguish them from the structured specifications to be introduced in later chapters.

Throughout this section, let Σ be a signature.

A presentation (also known as a flat specification) is a pair ⟨Σ, Φ⟩ where Φ is a set of Σ-equations (called the axioms of ⟨Σ, Φ⟩). A presentation ⟨Σ, Φ⟩ is sometimes referred to as a Σ-presentation.

A model of a presentation ⟨Σ, Φ⟩ is a Σ-algebra A such that A ⊧_{Σ} Φ. Mod_{Σ}(Φ) is the class of all models of ⟨Σ, Φ⟩. Taking ⟨Σ, Φ⟩ to denote the semantic object Mod_{Σ}(Φ) is sometimes called taking its loose semantics.

Example 2.14. Let Bool = ⟨ΣBool, ΦBool⟩ be the following presentation.

Bool = sorts bool
opns true : bool
false : bool

¬: bool → bool

∧: bool × bool → bool

axioms ¬true = false

¬false = true

∀p:bool. p ∧ true = p ∀p:bool. p ∧ false = false ∀p:bool. p ∧ ¬p = false

Define ΣBool-algebras A1, A2, and A3 as follows:

|A1|_{bool} = {⋆}  |A2|_{bool} = {a, b, c}  |A3|_{bool} = {1, 0}
true_{A1} = ⋆  true_{A2} = a  true_{A3} = 1
false_{A1} = ⋆  false_{A2} = b  false_{A3} = 0
¬_{A1} = \{⋆ ↦ ⋆\}  ¬_{A2} = \begin{cases}a ↦ b, \\ b ↦ a, \\ c ↦ c\} \end{cases}  ¬_{A3} = \begin{cases}1 ↦ 0, \\ 0 ↦ 1\} \end{cases}

\begin{matrix}∧_{A1} & ⋆ \\ ⋆ & ⋆ \end{matrix}  \begin{matrix}∧_{A2} & a & b & c \\ a & a & b & b \\ b & b & b & b \\ c & c & b & b \end{matrix}  \begin{matrix}∧_{A3} & 1 & 0 \\ 1 & 1 & 0 \\ 0 & 0 & 0 \end{matrix}

Each of these algebras is a model of Bool. (Reference will be made to Bool and to A1, A2, and A3 in later sections of this chapter.)

For any class A of Σ-algebras, Th_{Σ}(A) (the theory of A) denotes the set of all Σ-equations satisfied by each Σ-algebra in A:

Th_{Σ}(A) = {φ | φ is a Σ-equation and A ⊧_{Σ} φ}.

The closure of a set Φ of Σ-equations is the set Cl_{Σ}(Φ) = Th_{Σ}(Mod_{Σ}(Φ)); Φ is closed if Φ = Cl_{Σ}(Φ).

Proposition 2.15. For any sets Φ and Ψ of Σ-equations and classes A, B of Σ-algebras:

1a. If Φ ⊆ Ψ then Mod_{Σ}(Ψ) ⊆ Mod_{Σ}(Φ). 1b. If A ⊆ B then Th_{Σ}(B) ⊆ Th_{Σ}(A). 2a. Φ ⊆ Th_{Σ}(Mod_{Σ}(Φ)). 2b. A ⊆ Mod_{Σ}(Th_{Σ}(A)). 3a. Mod_{Σ}(Φ) = Mod_{Σ}(Th_{Σ}(Mod_{Σ}(Φ))). 3b. Th_{Σ}(A) = Th_{Σ}(Mod_{Σ}(Th_{Σ}(A))).

A Σ-equation φ is a semantic (or model-theoretic) consequence of a set Φ of Σ-equations, written Φ ⊧_{Σ} φ, if φ ∈ Cl_{Σ}(Φ) (equivalently, if Mod_{Σ}(Φ) ⊧_{Σ} φ). We will write Φ ⊧ φ instead of Φ ⊧_{Σ} φ where the signature Σ is obvious.

Proposition 2.16. Semantic consequence is preserved by translation along signature morphisms: for any signature morphism σ: Σ → Σ′, set Φ of Σequations, and Σ-equation φ,

if Φ ⊧_{Σ} φ then σ(Φ) ⊧_{Σ′} σ(φ).

Proposition 2.17. Let σ: Σ → Σ′ be a signature morphism and let Φ′ be a closed set of Σ′-equations. Then σ^{−1}(Φ′) is a closed set of Σ-equations.

A theory is a presentation ⟨Σ, Φ⟩ such that Φ is closed. A presentation ⟨Σ, Φ⟩ (where Φ need not be closed) presents the theory ⟨Σ, Cl_{Σ}(Φ)⟩. A theory ⟨Σ, Φ⟩ is sometimes referred to as a Σ-theory. For any theories ⟨Σ, Φ⟩ and ⟨Σ′, Φ′⟩, a theory morphism σ: ⟨Σ, Φ⟩ → ⟨Σ′, Φ′⟩ is a signature morphism σ: Σ → Σ′ such that σ(φ) ∈ Φ′ for every φ ∈ Φ.

Example 2.18. Let Σ be the signature

Σ = sorts s, b
opns tt : b
ff : b
not : s → b
and : s × b → b

and recall the presentation Bool = ⟨ΣBool, ΦBool⟩ in Example 2.14. Define a signature morphism σ: Σ → ΣBool by σ_{sorts} = {s ↦ bool, b ↦ bool}, σ_{ε,b} = {tt ↦ true, ff ↦ false}, σ_{s,b} = {not ↦ ¬}, and σ_{s b,b} = {and ↦ ∧}. Let Φ = { ∀x:s. and(x, and(x, not(x))) = ff , ∀x:s. and(x, ff ) = ff }. Then Cl_{Σ}(Φ) includes Σ-equations that were not in Φ, such as the equation ∀x, y:s. and(y, and(x, and(x, not(x)))) = ff . The presentations ⟨Σ, Cl_{Σ}(Φ)⟩ and ⟨ΣBool, Cl_{ΣBool}(ΦBool)⟩ are theories – the latter is the theory presented by Bool – and σ: ⟨Σ, Cl_{Σ}(Φ)⟩ → ⟨ΣBool, Cl_{ΣBool}(ΦBool)⟩ is a theory morphism.

Proposition 2.19. Let σ: Σ → Σ′ be a signature morphism, Φ be a set of Σ-equations, and Φ′ be a set of Σ′-equations. Then the following conditions are equivalent:

1. σ is a theory morphism σ: ⟨Σ, Cl_{Σ}(Φ)⟩ → ⟨Σ′, Cl_{Σ′}(Φ′)⟩.

2. σ(Φ) ⊆ Cl_{Σ′}(Φ′).

3. For every A′ ∈ Mod_{Σ′}(Φ′), A′ _{σ} ∈ Mod_{Σ}(Φ).

2.8 Equational calculus

The set of consequences of a presentation ⟨Σ, Φ⟩ has been defined in a modeltheoretic way. In this section we present a calculus for deriving consequences of a set of equational axioms in a “syntactic” way. It turns out that these two notions of consequence coincide.

A Σ-equation φ is a syntactic (or proof-theoretic) consequence of Φ, written Φ ⊢_{Σ} φ, if φ can be derived from Φ by application of the following inference rules:

Reflexivity:  \overline{∀X. t = t} t ∈ |T_{Σ}(X)|

Symmetry:  \frac{∀X. t = t′}{∀X. t′ = t}

Transitivity:  \frac{∀X. t = t′  ∀X. t′ = t′′}{∀X. t = t′′}

Congruence:  \frac{∀X. t_{1} = t′_{1}  ⋯  ∀X. t_{n} = t′_{n}}{∀X. f(t_{1}, …, t_{n}) = f(t′_{1}, …, t′_{n})}

for f: s_{1} × ⋯ × s_{n} → s and t_{i}, t′_{i} ∈ |T_{Σ}(X)|_{s_{i}} for i ≤ n

Instantiation:  \frac{∀X. t = t′}{∀Y. t[θ] = t′[θ]} θ: X → |T_{Σ}(Y)|

Example 2.20. Recall the presentation Bool = ⟨ΣBool, ΦBool⟩ from Example 2.14. The following derivation proves ΦBool ⊢_{ΣBool} ∀p:bool. ¬(p ∧ ¬false) = ¬p:

\frac{\overline{∀p:bool. p = p} \frac{¬false = true}{∀p:bool. ¬false = true}}{∀p:bool. p ∧ ¬false = p ∧ true}

∀p:bool. ¬(p ∧ ¬false) = ¬(p ∧ true)

\frac{∀p:bool. p ∧ true = p}{∀p:bool. ¬(p ∧ true) = ¬p}

∀p:bool. ¬(p ∧ ¬false) = ¬p

As mentioned above, ⊢_{Σ} is both sound (only valid consequences may be derived) and complete (all valid consequences may be derived) for ⊧_{Σ}.

Theorem 2.21. For any set Φ of Σ-equations and any Σ-equation φ, Φ ⊢_{Σ} φ if and only if Φ ⊧_{Σ} φ.

Simplifying the above calculus by omitting explicit quantifiers in equations yields an unsound system because algebras may have empty carrier sets. In particular, unused variables cannot always be removed from equations. The instantiation rule allows quantified variables to be eliminated when it is sound to do so [GM85].

2.9 Initial models

The class of algebras given by the loose semantics of a Σ-presentation always includes degenerate Σ-algebras with a single value of each sort in Σ, and usually includes unreachable Σ-algebras. Equational axioms are not sufficient to eliminate such obviously undesired models. One standard remedy is to take the so-called initial semantics of presentations.

Let A be a model of a presentation ⟨Σ, Φ⟩. We say that A contains junk if it is not reachable, and that A contains confusion if it satisfies a ground Σ-equation that is not in Cl_{Σ}(Φ).

Example 2.22. Recall the presentation Bool = ⟨ΣBool, ΦBool⟩ and its models A1, A2, and A3 given in Example 2.14. A1 contains confusion (A1 ⊧_{ΣBool} true = false ∉ Cl_{ΣBool}(ΦBool)) but not junk; A2 contains junk (there is no ground ΣBool-term t such that t_{A2} = c ∈ |A2|_{bool}) but not confusion; A3 contains neither junk nor confusion. There are models of Bool containing both junk and confusion.

A Σ-algebra A ∈ Mod_{Σ}(Φ) is an initial model of ⟨Σ, Φ⟩ if for every B ∈ Mod_{Σ}(Φ) there is a unique Σ-homomorphism h: A → B.

The initial models of an equational presentation are those that have no junk and no confusion. An initial model may be constructed as a quotient of the algebra T_{Σ} of ground Σ-terms by the least congruence generated by the axioms:

Theorem 2.23. ⟨Σ, Φ⟩ has an initial model.

Proof sketch. An initial model of ⟨Σ, Φ⟩ is the quotient T_{Σ}/≡_{Φ}, where ≡_{Φ} is the Σ-congruence generated by Φ: t ≡_{Φ} t′ ⟺ Φ ⊧_{Σ} ∀∅. t = t′, for all t, t′ ∈ |T_{Σ}|. The existence and uniqueness of a Σ-homomorphism from T_{Σ}/≡_{Φ} to any B ∈ Mod_{Σ}(Φ) follows from Proposition 2.6. ⊓ ⊔ Example 2.24. The model T_{ΣBool}/≡_{ΦBool} of Bool (see Example 2.14) is defined as follows:

|T_{ΣBool}/≡_{ΦBool}|_{bool} = {[true]_{≡_{ΦBool}} , [false]_{≡_{ΦBool}} }

true_{T_{ΣBool} /≡_{ΦBool}} = [true]_{≡_{ΦBool}}
false_{T_{ΣBool} /≡_{ΦBool}} = [false]_{≡_{ΦBool}}

¬_{T_{ΣBool} /≡_{ΦBool}} = {[true]_{≡_{ΦBool}} ↦ [false]_{≡_{ΦBool}} , [false]_{≡_{ΦBool}} ↦ [true]_{≡_{ΦBool}} }

∧_{T_{ΣBool} /≡_{ΦBool}} [true]_{≡_{ΦBool}} [false]_{≡_{ΦBool}}
[true]_{≡_{ΦBool}} [true]_{≡_{ΦBool}} [false]_{≡_{ΦBool}}
[false]_{≡_{ΦBool}} [false]_{≡_{ΦBool}} [false]_{≡_{ΦBool}}

where

[true]_{≡_{ΦBool}} = {true, ¬false, ¬(false ∧ true), ¬(false ∧ ¬false), … },
[false]_{≡_{ΦBool}} = {false, ¬true, ¬(true ∧ true), ¬(true ∧ ¬false), … }.

This is an initial model of Bool by the proof sketched for Theorem 2.23. ΣBool-homomorphisms from T_{ΣBool}/≡_{ΦBool} to A1, A2, and A3 are as follows:

h1: T_{ΣBool}/≡_{ΦBool} → A1

h1_{bool} = {[true]_{≡_{ΦBool}} ↦ ⋆, [false]_{≡_{ΦBool}} ↦ ⋆}

h2: T_{ΣBool}/≡_{ΦBool} → A2

h2_{bool} = {[true]_{≡_{ΦBool}} ↦ a, [false]_{≡_{ΦBool}} ↦ b}

h3: T_{ΣBool}/≡_{ΦBool} → A3

h3_{bool} = {[true]_{≡_{ΦBool}} ↦ 1, [false]_{≡_{ΦBool}} ↦ 0}

Taking a presentation to denote the (non-empty) class of its initial models is called taking its initial semantics. The initiality property identifies a model of ⟨Σ, Φ⟩ up to isomorphism: any two initial models are isomorphic, and any model isomorphic to an initial model is itself initial. We therefore refer to the initial model of a presentation.

Example 2.25. A3 is an initial model of Bool (see Example 2.14) since it is isomorphic to T_{ΣBool}/≡_{ΦBool}. On the other hand, A1 and A2 are not isomorphic to A3 and hence are not initial models. This can be checked directly as well: for example, ∄h: A1 → A2 and ∄h: A1 → A3.

2.10 Variations on a theme

The simple specification framework presented above is the classical one in the field of algebraic specifications. A wide variety of modifications have been made to increase its expressive power and to take account of the various features of software systems which it does not handle adequately. This section is devoted to a sketch of some of these modifications; details may be found in the cited references.

2.10.1 Conditional equations

Equational axioms can be generalized to (positive) conditional equational axioms of the form ∀X. t_{1} = t′_{1} ∧ … ∧ t_{n} = t′_{n} ⇒ t_{0} = t′_{0}. A Σ-algebra A satisfies such an axiom if for every (S-sorted) function v: X → |A|, if v^{#}(t_{1}) = v^{#}(t′_{1}) and … and v^{#}(t_{n}) = v^{#}(t′_{n}), then v^{#}(t_{0}) = v^{#}(t′_{0}). With these changes, most results still apply with appropriate minor modifications. For example, any presentation ⟨Σ, Φ⟩, where Φ is a set of conditional Σequations, has an initial model which can be constructed in a similar way as in the proof of Theorem 2.23 (see, e.g., [MT92]). There is also a sound and complete proof system for conditional equational consequence [Sel72].

2.10.2 Partial algebras

An obvious way to generalize the standard definition of an algebra is to allow partial functions as interpretations of operation names. Homomorphisms between such partial algebras are required to preserve definedness of operations, and (as usual) their results when these are defined. Term evaluation is defined as in ordinary algebras, except that terms need not have defined values. An equation ∀X. t = t′ is satisfied in a partial algebra A when for all valuations v: X → |A|, the values of t and t′ under v either are defined and equal, or are both undefined. Additional axioms are required to assert definedness: ∀X. D(t) holds in A when the value of t is defined under all valuations of X in A. Every presentation ⟨Σ, Φ⟩, where Φ is a set of Σequations and definedness formulas, has an initial model which contains no junk, is minimally defined (i.e., the value of a ground term t is defined only if Φ ⊧_{Σ} ∀∅. D(t)), and contains no confusion, i.e., the values of two ground terms t, t′ are defined and equal only if Φ ⊧_{Σ} ∀∅. t = t′.

This is one possible approach to the specification of partial algebras, following [BW82]. There are various other choices for the basic definitions [Rei87, Bur86].

2.10.3 Error algebras

To model operations that may produce erroneous or exceptional results, we can partition each of the carrier sets of an algebra into an error part and an OK part. Operations in signatures are classed as safe or unsafe, where the former are required to yield OK values when applied to OK arguments. Homomorphisms are required to preserve OK-ness. Like operations, variables in equations are classed as safe or unsafe; the former range over OK values only, while the latter range over all values. Again, all presentations have initial models, in which operations propagate errors unless otherwise specified.

The details of this approach may be found in [GDLE84]. Again, there are many other approaches, see for instance [Gog78] or [BBC86].

2.10.4 Order-sorted algebras

In order to model sort inclusion and coercions, signatures may be enriched with an order relation on the set of sorts. An order-sorted Σ-algebra A is required to respect the sort ordering in the order-sorted signature Σ: if s ≤ s′ in Σ then we require that |A|_{s} ⊆ |A|_{s′}. Overloading is forced by requiring operations to be applicable to values from subsorts of their argument sorts and to yield results in supersorts of their result sorts. Under certain conditions terms are guaranteed to have least sorts and unambiguous values. Then once more, all presentations have initial models and there is a version of the equational calculus that is sound and complete for order-sorted satisfaction.

For details see [GM85]. Alternative approaches are [Gog84, Poi84, Smo86]; see also [Mos93, GD94, CHKM97].

2.10.5 First-order predicate logic

Signatures may be modified to enable them to include (typed) predicate names in addition to operation names, e.g., ≤: nat × nat. Atomic formulas are then formed by applying predicates to terms; in first-order predicate logic with equality, the predicate =: s×s is implicitly available for any sort s. Formulas are built from atomic formulas using the usual logical connectives and quantifiers. Algebras are modified to include relations on their carriers to interpret predicate names (giving what are sometimes called relational structures). Homomorphisms are required to preserve predicates as well as operations. The satisfaction of a sentence (a formula without free variables) by an algebra is as usual in first-order logic. Presentations involving predicates and first-order axioms do not always have initial models or even reachable models. Details of first-order predicate logic for use in algebraic specifications may be found in, e.g., [GB92].

2.10.6 Higher-order functions

Higher-order functions (which take functions as parameters and/or return functions as results) can be accommodated by interpreting certain sort names as (subsets of) function spaces. Given a set S of (base) sorts, let S^{→} be the closure of S under formation of function types: S^{→} is the smallest set such that S ⊆ S^{→} and for all s_{1}, …, s_{n}, s ∈ S^{→}, s_{1} × ⋯ × s_{n} → s ∈ S^{→}. Then a higher-order signature Σ is a pair ⟨S, Ω⟩ where Ω is an S^{→}-indexed set of operation names. This determines an ordinary signature Σ^{→} comprised of the sort names S^{→} and the operation names in Ω (as constants of sorts in S^{→}) together with operation names apply : (s_{1} × ⋯ × s_{n} → s) × s_{1} × ⋯ × s_{n} → s for every s_{1}, …, s_{n}, s ∈ S^{→}. A higher-order Σ-algebra is just an ordinary (total) Σ^{→}-algebra, and analogously for the definitions of higher-order Σhomomorphism, higher-order Σ-equation, higher-order presentation, etc. A higher-order Σ-algebra A is extensional if for all sorts s_{1} ×⋯×s_{n} → s ∈ S^{→} and values f, g ∈ |A|_{s_{1}×···×s_{n}→s}, f = g whenever apply_{A}(f, a_{1}, …, a_{n}) = apply_{A}(g, a_{1}, …, a_{n}) for all a_{1} ∈ |A|_{s_{1}}, …, a_{n} ∈ |A|_{s_{n}}. In an extensional algebra A, every carrier |A|_{s_{1}×···×s_{n}→s} is isomorphic to a subset of the function space |A|_{s_{1}} ×⋯×|A|_{s_{n}} → |A|_{s}. Higher-order equational presentations always have initial extensional reachable models. See [MTW88] for details, and for alternative approaches see, e.g., [Poi86, Mei92].

2.10.7 Polymorphic types

Programming languages such as Standard ML [Pau96] can be used to define polymorphic types such as α list and polymorphic values such as the function head:∀α. α list → α. To specify such types and functions, signatures are modified to contain type constructors in place of sort names. Terms built using these type constructors and type variables (such as α above) are the polymorphic types of the signature. The set Ω of operation names is then indexed by non-empty sequences of polymorphic types, where f ∈ Ω_{t_{1}...t_{n},t} means f: ∀FV (t_{1}) ∪ … ∪ FV (t_{n}) ∪ FV (t). t_{1} × ⋯ × t_{n} → t. There are various choices for algebras over such signatures. The most straightforward is to require each algebra A to incorporate a (single-sorted) algebra of carriers, Carr(A), having sets which interpret types as values and an operation to interpret each type constructor. Then, for each operation f ∈ Ω_{t_{1}...t_{n},t} and for each instantiation of type variables i: V → |Carr(A)|, A has to provide a function f_{A,i}: i^{#}(t_{1}) × ⋯ × i^{#}(t_{n}) → i^{#}(t). Various conditions may be imposed to ensure that the interpretation of polymorphic operations is parametric, by requiring f_{A,i} and f_{A,i′} to be appropriately related for different type variable instantiations i, i′. Axioms contain (universal) quantifiers for type variables in addition to quantifiers for ordinary variables, as in System F [GLT89]; alternatively, type-variable quantification may be left implicit, as in Extended ML [KST97].

2.10.8 Non-deterministic functions

Non-deterministic functions may be handled by interpreting operation names in algebras as relations or, equivalently, as set-valued functions. Homomorphisms are required to preserve possible values of functions: for any homomorphism h: A → B and operation f: s_{1} × ⋯ × s_{n} → s, if a is a possible value of f_{A}(a_{1}, …, a_{n}) then h_{s}(a) is a possible value of f_{B}(h_{s_{1}}(a_{1}), …, h_{s_{n}}(a_{n})). Universally quantified inclusions between sets of possible values may be used as axioms: t ⊆ t′ means that every possible value of t is a possible value of t′. See [Nip86, Huß89, BS93, BK98] for details.

2.10.9 Continuous algebras

Following [Sco76], partial functions may be specified as least solutions of recursive equations. To accommodate this, we can use continuous algebras, i.e., ordinary (total) Σ-algebras with carriers that are complete partially ordered sets (so-called cpos) and operation names interpreted as continuous functions on these sets. The “bottom” element ⊥ of the carrier for a sort, if it exists, represents the completely undefined value of that sort. The order on carriers induces an order on (continuous) functions in the usual fashion. A homomorphism between continuous algebras is required to be continuous as a function between cpos. For details see, e.g., [GTWW77]. It is possible to define a language of axioms that allows direct reference to least upper bounds of chains and/or to the order relation itself (see, e.g., [TW86]).

Bibliography

[BBC86] G. Bernot, M. Bidoit, and C. Choppy. Abstract data types with exception handling: an initial approach based on a distinction between exceptions and errors. Theoretical Computer Science, 46(1):13–45, 1986.

[BG80] R.M. Burstall and J.A. Goguen. The semantics of clear, a specification language. In D. Björner, editor, Proc. Copenhagen Winter School on Abstract Software Specification, volume 86 of Lecture Notes in Computer Science, pages 292–332. Springer, 1980.

[BK98] M. Białasik and B. Konikowska. A logic for nondeterministic specifications. In E. Orłowska, editor, Logic at work. Essays dedicated to the memory of H. Rasiowa. Kluwer, 1998.

[BS93] R. Berghammer and G. Schmidt. Relational specifications. In Algebraic Methods in Logic and Computer Science, volume 28 of Banach Center Publications, pages 167–190. Institute of Mathematics, Polish Academy of Sciences, Warsaw, 1993.

[Bur86] P. Burmeister. A Model Theoretic Oriented Approach to Partial Algebras. Akademie-Verlag, Berlin, 1986.

[BW82] M. Broy and M. Wirsing. Partial abstract types. Acta Informatica, 18(1):47–64, 1982.

[CHKM97] M. Cerioli, A. Hauxthausen, B. Krieg-Brückner, and T. Mossakowski. Permissive subsorted partial logic in CASL. In Michael Johnson, editor, Algebraic Methodology and Software Technology (AMAST’97), volume 1349 of Lecture Notes in Computer Science, pages 91–107. Springer, 1997.

[EM85] Hartmut Ehrig and Bernd Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer, 1985.

[GB92] J.A. Goguen and R.M. Burstall. Institutions: abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39(1):95–146, 1992.

[GD94] J. Goguen and R. Diaconescu. An Oxford survey of order sorted algebra. Mathematical Structures in Computer Science, 4:363–392, 1994.

[GDLE84] M. Gogolla, K. Drosten, U. Lipeck, and H.-D. Ehrich. Algebraic and operational semantics of specifications allowing exceptions and errors. Theoretical Computer Science, 34:289–313, 1984.

[GLT89] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.

[GM85] J. Goguen and J. Meseguer. Completeness of many-sorted equational logic. Houston Journal of Mathematics, 11(3):307–334, 1985.

[Gog78] J.A. Goguen. Abstract errors for abstract data types. In Proc. IFIP Working Conference on the Formal Description of Programming Concepts. North-Holland, 1978.

[Gog84] M. Gogolla. Partially ordered sorts in algebraic specifications. In Proc. 9th Colloquium on Trees in Algebra and Programming, pages 139–153. Cambridge University Press, 1984.

[GTWW77] J. Goguen, J. Thatcher, E. Wagner, and J. Wright. Initial algebra semantics and continuous algebras. Journal of the Association for Computing Machinery, 24(1):68–95, 1977.

[Huß89] H. Hußmann. Nichtdeterministische algebraische Spezifikation. PhD

thesis, Universität Passau, 1989.

[KST97] S. Kahrs, D. Sannella, and A. Tarlecki. The definition of Extended ML: a gentle introduction. Theoretical Computer Science, 173:445–484, 1997.

[LEW96] J. Loeckx, H.-D. Ehrich, and B. Wolf. Specification of Abstract Data Types. Wiley, 1996.

[Mei92] K. Meinke. Universal algebra in higher types. Theoretical Computer Science, 100(2):385–417, 1992.

[Mos93] Peter D. Mosses. The use of sorts in algebraic specifications. In M. Bidoit and C. Choppy, editors, Recent Trends in Data Type Specification, Selected Papers from the 8th Workshop on Specification of Abstract Data Types, volume 655 of Lecture Notes in Computer Science, pages 66–91. Springer, 1993.

[MT92] K. Meinke and J. Tucker. Universal algebra. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, Vol. 1, pages 189–411. Oxford University Press, 1992.

[MTW88] B. Möller, A. Tarlecki, and M. Wirsing. Algebraic specifications of reachable higher-order algebras. In Recent Trends in Data Type Specification, Selected Papers from the 5th Workshop on Specification of Abstract Data Types, volume 332 of Lecture Notes in Computer Science, pages 154–169. Springer, 1988.

[Nip86] T. Nipkow. Non-deterministic data types: models and implementations. Acta Informatica, 22:629–661, 1986.

[Pau96] L.C. Paulson. ML for the Working Programmer. Cambridge University Press, 2nd edition, 1996.

[Poi84] A. Poigné. Another look at parameterization using algebraic specifications with subsorts. In Proc. 11th Symp. on Mathematical Foundations of Computer Science, volume 176 of Lecture Notes in Computer Science, pages 471–479. Springer, 1984.

[Poi86] A. Poigné. On specifications, theories, and models with higher types. Information and Control, 68:1–46, 1986.

[Rei87] H. Reichel. Initial Computability, Algebraic Specifications, and Partial Algebras. Oxford University Press, 1987.

[Sco76] D. Scott. Data types as lattices. SIAM Journal of Computing, 5:522– 587, 1976.

[Sel72] A. Selman. Completeness of calculi for axiomatically defined classes of algebras. Algebra Universalis, 2:20–32, 1972.

[Smo86] G. Smolka. Order-sorted Horn logic: semantics and deduction. SEKI report SR-86-17, FB Informatik, Universität Kaiserslautern, 1986.

[ST] D. Sannella and A. Tarlecki. Foundations of Algebraic Specifications and Formal Program Development. Cambridge University Press. To appear.

[TW86] A. Tarlecki and M. Wirsing. Continuous abstract data types. Fundamenta Informaticae, 9:95–126, 1986.

[Wir90] Martin Wirsing. Algebraic specification. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, chapter 13, pages 675–788. Elsevier Science Publishers B.V. (North Holland), 1990.