General Algebras

Øyvind B. Fredriksen

University of Bergen Department of Informatics^{∗}

Abstract We study categories of algebras (for a given signature) constructed from arbitrary categories C with specific finite products. We show how a left adjoint Set \overline{}C may be utilized to construct an initial algebra satisfying a given set of equations. Finally, we give a condition under which satisfaction of equations is independent of the set of variables considered.

1 Introduction

This paper reports work in progress. It is concerned with specifications of abstract data types and in particular with the semantics of such specifications. Here we will only consider one-sorted equational specifications or presentations, having two parts:

• the names (called operation symbols) of the operations involved, together with their arities

• equations describing the properties of the operations. The two sides of an equation are terms constructed from the operation symbols and usually some variables.

As for semantics, a presentation is usually interpreted in so-called total algebras. Such an algebra comprises a carrier set AU_{Σ}, and for each n-ary operation symbol a function AU_{Σ}^{n} \overline{}AU_{Σ}. Terms and equations may then be interpreted, and only those algebras satisfying the equations are considered. These algebras are the objects of a category^{1}. Of particular interest are those algebras which are initial in this category. The initial algebras identify only those terms whose equality follows from the equations.

However, also other semantic models have been suggested: partial algebras ([13]), ordered/monotonic algebras ([10]), continuous algebras ([6]), and topological algebras ([9]).

As a vehicle for bridging the gap between specification of abstract data types and of systems of parallel processes, one might also consider total algebras whose carrier elements are models of parallel computation, e.g. partial orders representing the causal order of the events performed by the system.

∗Postal address: …, Høyteknologisenteret, N–5020 BERGEN, NORWAY. E-mail:

bolme@ii.uib.no

1This paper assumes a fair knowledge of category theory. See e.g. [7].

The theories of the various kinds of models are fairly similar: In each case, similar theorems are proved in similar ways. To simplify and clarify matters and to facilitate the consideration of novel models, it might be useful to construct a general theory subsuming (as many as possible of) the others as special cases.

In [1] we presented our first steps towards this goal. We made a construction based on the following parameters:

• a Cartesian category C

• finite product preserving functors U : C \overline{}Set and F : Set \overline{}C such that F U and^{2} F ∘ U = ISet.

However, we felt that this last condition was rather ad hoc and too restrictive. In this paper we refine our approach in such a way that the abovementioned restriction becomes unnecessary.

In [1] we demonstrated that our approach subsumes the theories of total and ordered algebras (in the sense that it permits the construction of an initial algebra satisfying a given set of equations). For some speculations on the success or failure of our theory in some of the other cases mentioned above, we refer the reader to the same paper. The same goes for a more detailed introduction.

The rest of the paper is organized as follows: In section 2 we review the theory of total algebras. We present our general theory in section 3. In section 4 we make a few concluding remarks.

In order to structure the next two sections, we consider the successive introduction of the two parts of a presentation: operation symbols and equations.

Omitted proofs are entirely straightforward.

1.1 Notational and Other Conventions

If C is a category, its object class is denoted by C_{0} and the (hom-)class of arrows A \overline{}B by C (A, B). A finite (product) mediating arrow is denoted by ⟨f_{0}, …, f_{n−1}⟩.

A natural number is the set of the smaller ones, i.e. n = {0, …, n − 1}. In particular, the number 0 is the empty set.

A function space Set (A, B) may also be denoted by ^{A}B, and may alternatively be regarded as an ‘A-fold product of B-s’. If A is a natural number n, we will usually use the notation B^{n}. If b ∈ B^{n} and i ∈ n, we usually (but not always) write b_{i} for ib.

2 Total Algebras

In this section we briefly review the relevant parts of the theory of total algebras. A fuller account is given in e.g. [5]. We also give some lemmas needed later.

2Please note that we write composition in an arbitrary category in diagrammatic order, i.e. the composite arrow \overline{}^{f} \overline{}^{g} is denoted by f ∘ g. In accordance with this, application of a ‘function’ (e.g. a functor) f to an ‘argument’ x is denoted by xf. This application is left associative.

2.1 Signatures

A (one-sorted) signature Σ is an assignment of a set Σ_{n} (of n-ary operation symbols) to each natural number n. A 0-ary operation symbol is called a constant symbol.

If Σ and Σ′ are signatures, Σ′ is said to include Σ, denoted by Σ ⊆ Σ′, if Σ_{n} ⊆ Σ′_{n} for all n.

A signature chain is an N-indexed sequence Σ_{0}, Σ_{1}, Σ_{2}, … of signatures such that each Σ_{n} ⊆ Σ_{n+1}. (A set chain is an N-indexed sequence V_{0}, V_{1}, V_{2}, … of sets such that each V_{n} ⊆ V_{n+1}.)

2.1.1 Union of Signatures

Let

• I be a set

• for each i ∈ I Σ_{i} be a signature.

Then the union (signature) ⋃_{i∈I} Σ_{i} of the Σ_{i} is defined by

(⋃_{i∈I} Σ_{i})_{n} = ⋃_{i∈I} (Σ_{i})_{n} .

Lemma 1 Each Σ_{i} ⊆ ⋃_{i∈I} Σ_{i}.

2.1.2 Algebras and Homomorphisms

Let Σ be a signature. The category Set^{Σ} of total Σ-algebras and total Σhomomorphisms is defined by

• A total Σ-algebra A comprises

– a carrier set AU_{Σ}

– for each n ∈ N and f ∈ Σ_{n} a function f_{A} : AU_{Σ}^{n} \overline{}AU_{Σ}.

• A total Σ-homomorphism h : A \overline{}B is a function AU_{Σ} \overline{}BU_{Σ} such that

∀n ∈ N.∀f ∈ Σ_{n}.f_{A} ∘ h = \underbrace{h × ⋯ × h}_{n} ∘f_{B}, (1)

which is equivalent to that for all n ∈ N, f ∈ Σ_{n}, and a ∈ AU_{Σ}^{n} af_{A}h = (a_{0}h, …, a_{n−1}h) f_{B}.

• Composition is composition in Set.

• The identities are defined by id_{A} = id_{AU_{Σ}}.

Lemma 2 Assume that Σ contains a constant symbol c ∈ Σ_{0} and let A be a total Σ-algebra. Then AU_{Σ} is non-empty.

Proof: The function c_{A} : AU_{Σ}^{0} \overline{}AU_{Σ}, where AU_{Σ}^{0} is a singleton, entailing that ∗c_{A} ∈ AU_{Σ}.

2.1.3 The Forgetful Functor Set^{Σ} \overline{}Set

Extend the assignment A ↦ AU_{Σ} to a functor U_{Σ} : Set^{Σ} \overline{}Set by hU_{Σ} = h on arrows.

Even though hU_{Σ} = h, we will usually write hU_{Σ} when we think of it as a function.

2.1.4 Ground Terms

Let T_{Σ} be the least language (with the inclusion order) such that

(2) T_{Σ} = {f (t_{0}, …, t_{n−1}) |n ∈ N cand f ∈ Σ_{n} ∧ ⋀_{i∈n} t_{i} ∈ T_{Σ} } .

(When f is a constant symbol, f () is written simply f, entailing that Σ_{0} ⊆ T_{Σ}.) Each string in the language T_{Σ} is called a ground term.

This definition permits us to carry out proofs by induction on the structure of ground terms.

Lemma 3 T_{Σ} is empty iff Σ_{0} is.

Proof: As 0 is the least language, the least language T_{Σ} such that (2) is 0 iff

0 = {f (t_{0}, …, t_{n−1}) |n ∈ N cand f ∈ Σ_{n} ∧ ⋀_{i∈n} t_{i} ∈ 0}
= Σ_{0}.

Lemma 4 The operation Σ ↦ T_{Σ} is monotone w.r.t. (signature and set) inclusion.

2.1.4.1 Union of Ground Term Languages

Lemma 5 Let

• I be a set

• for each i ∈ I Σ_{i} be a signature.

Then ⋃_{i∈I} T_{Σ_{i}} ⊆ T_{⋃_{i∈I} Σ_{i}}.

Proof: Straightforward, using lemmata 4 and 1.

Lemma 6 Let Σ_{0} ⊆ Σ_{1} ⊆ ⋯ be a signature chain. Then

T_{⋃_{n∈N} Σ_{n}} = ⋃_{n∈N} T_{Σ_{n}}.

Proof: We have to prove that T_{⋃_{n∈N} Σ_{n}} ⊆ ⋃_{n∈N} T_{Σ_{n}}. We will prove that t ∈ T_{⋃_{n∈N} Σ_{n}} ⇒ t ∈ ⋃_{n∈N} T_{Σ_{n}} by induction on t. We have to prove that f (t_{0}, …, t_{m−1}) ∈ T_{⋃_{n∈N} Σ_{n}} ⇒ f (t_{0}, …, t_{m−1}) ∈ ⋃_{n∈N} T_{Σ_{n}}. Therefore, assume the antecedent, which is equivalent to that

•

f ∈ ( ⋃_{n∈N} Σ_{n})_{m}
= ⋃_{n∈N} (Σ_{n})_{m} ,

which is equivalent to that ∃n ∈ N.f ∈ (Σ_{n})_{m}. Therefore, let n ∈ N be such that f ∈ (Σ_{n})_{m}.

• ⋀_{i∈m} t_{i} ∈ T_{⋃_{n∈N} Σ_{n}}, where t_{i} ∈ T_{⋃_{n∈N} Σ_{n}} entails that t_{i} ∈ ⋃_{n∈N} T_{Σ_{n}}, which is equivalent to that ∃n ∈ N.t_{i} ∈ T_{Σ_{n}}. Therefore, let for each i ∈ m n_{i} ∈ N be such that t_{i} ∈ T_{Σ_{n_{i}}}.

We have to prove the consequent, which is equivalent to that there is an n ∈ N such that f (t_{0}, …, t_{m−1}) ∈ T_{Σ_{n}}.

We claim that f (t_{0}, …, t_{m−1}) ∈ T_{Σ_{_{max}_{{n,n_{0},...,n_{m−1}}}}}, which is straightforward to prove, using lemma 4. 2.1.5 Extensions Let Σ be a signature such that Σ_{0} is a ‘special’ set, disjoint from those in Set_{0}.

If V is a set, define a signature Σ (V) (the V -extension of Σ) by

• Σ (V)_{0} = Σ_{0} ∪ V

• Σ (V)_{n} = Σ_{n} otherwise. Lemma 7 The extension operation V ↦ Σ (V)

1. is monotone w.r.t. (set and signature) inclusion

2. preserves chains, i.e. takes set chains to signature chains

3. preserves/distributes over (arbitrary) unions: Σ (⋃_{i∈I} V_{i}) = ⋃_{i∈I} Σ (V_{i}). 2.1.6 The Free Algebra Functor The functor U_{Σ} has a left adjoint F_{Σ} : Set \overline{}Set^{Σ} whose object part is defined by: Let V be a Set-object. The Set^{Σ}-object V F_{Σ} is defined by

• The set V F_{Σ}U_{Σ} = T_{Σ(V)}.

• For each n ∈ N and f ∈ Σ_{n} the function f_{V F_{Σ}} : V F_{Σ}U_{Σ}^{n} \overline{}V F_{Σ}U_{Σ}, i.e. T_{Σ(V)}^{n} \overline{}T_{Σ(V)}, is defined by tf_{V F_{Σ}} = f (t_{0}, …, t_{n−1}) (the string).

Each string in the language V F_{Σ}U_{Σ} = T_{Σ(V)} is called a V -term.

In particular,

V ⊆ Σ_{0} ∪ V
= Σ (V)_{0}
⊆ T_{Σ(V)},

so V -elements (‘-variables’) are V -terms. Let η_{V} denote the inclusion function V \overline{}V F_{Σ}U_{Σ}. Even though each vη_{V} = v, we usually write vη_{V} when we think of it as a term.

Each V -term is on exactly one of two forms:

• vη_{V}

• f (t_{0}, …, t_{n−1}), where n is a natural number, f is an n-ary operation symbol, and t_{0}, …, t_{n−1} are V -terms.

This allows for inductive definitions and proofs.

If A is a total Σ-algebra, a function h : V F_{Σ}U_{Σ} \overline{}AU_{Σ} is a total Σhomomorphism V F_{Σ} \overline{}A iff for all n ∈ N, f ∈ Σ_{n}, and t ∈ V F_{Σ}U_{Σ}^{n} [f (t_{0}, …, t_{n−1})] h = (t_{0}h, …, t_{n−1}h) f_{A}.

The functor F_{Σ} being a left adjoint of U_{Σ} means that each V F_{Σ} is free over V w.r.t. U_{Σ}. The universal arrow is the inclusion η_{V}.

As a special case, 0F_{Σ} is free over the initial Set-object 0, i.e. is itself initial (in Set^{Σ}).

V F_{Σ} being free over V w.r.t. U_{Σ} with universal arrow η_{V} means that for each Set^{Σ}-object A and Set-arrow f : V \overline{}AU_{Σ} there exists a unique Set^{Σ}-arrow (denoted by) f^{#} : V F_{Σ} \overline{}A such that η_{V} ∘ f^{#}U_{Σ} = f.

2.1.6.1 Term Languages The term language V F_{Σ}U_{Σ} = T_{Σ(V)} is empty iff Σ (V)_{0} = Σ_{0} ∪ V is, i.e. iff both Σ_{0} and V are.

Corollary 1 Let V and V′ be sets such that V ⊆ V′. Then V F_{Σ}U_{Σ} ⊆ V′F_{Σ}U_{Σ}.

Proof: Straightforward, using lemmata 4 and 7, part 1..

2.1.6.1.1 Union of Term Languages

Corollary 2 Let

• I be a set

• for each i ∈ I V_{i} be a set.

Then ⋃_{i∈I} V_{i}F_{Σ}U_{Σ} ⊆ (⋃_{i∈I} V_{i}) F_{Σ}U_{Σ}.

Proof: Straightforward, using corollary 1.

Lemma 8 Let V_{0} ⊆ V_{1} ⊆ ⋯ be a set chain. Then

( ⋃_{n∈N} V_{n}) F_{Σ}U_{Σ} = ⋃_{n∈N} V_{n}F_{Σ}U_{Σ}.

Proof: Straightforward, using lemmata 6 and 7, parts 2. and 3..

2.2 Presentations

2.2.1 Equations

If V is a set, a V -equation is a pair of V -terms, i.e. an element of V F_{Σ}U_{Σ}^{2}. An equation is a V -equation for some set V.

2.2.1.1 Union of Equation Sets

Corollary 3 Let

• I be a set

• for each i ∈ I V_{i} be a set.

Then ⋃_{i∈I} V_{i}F_{Σ}U_{Σ}^{2} ⊆ (⋃_{i∈I} V_{i}) F_{Σ}U_{Σ}^{2}.

Proof: Straightforward, using corollary 1.

Lemma 9 Let V_{0} ⊆ V_{1} ⊆ ⋯ be a set chain. Then (⋃_{n∈N} V_{n}) F_{Σ}U_{Σ}^{2} = ⋃_{n∈N} V_{n}F_{Σ}U_{Σ}^{2}.

Proof: By corollary 3 and lemma 8 we have to prove that (⋃_{n∈N} V_{n}F_{Σ}U_{Σ})^{2} ⊆ ⋃_{n∈N} V_{n}F_{Σ}U_{Σ}^{2}. Therefore, let (t, u) ∈ (⋃_{n∈N} V_{n}F_{Σ}U_{Σ})^{2}, which is equivalent to that t, u ∈ ⋃_{n∈N} V_{n}F_{Σ}U_{Σ}, where t ∈ ⋃_{n∈N} V_{n}F_{Σ}U_{Σ} iff ∃n ∈ N.t ∈ V_{n}F_{Σ}U_{Σ}. Therefore, let n ∈ N be such that t ∈ V_{n}F_{Σ}U_{Σ}. Similarly, let m ∈ N be such that u ∈ V_{m}F_{Σ}U_{Σ}.

We have to prove that (t, u) ∈ ⋃_{n∈N} V_{n}F_{Σ}U_{Σ}^{2}, which is equivalent to that ∃n ∈ N. (t, u) ∈ V_{n}F_{Σ}U_{Σ}^{2}. We claim that (t, u) ∈ V_{max{m,n}}F_{Σ}U_{Σ}^{2}, which is straightforward to prove, using corollary 1.

2.2.2 Satisfaction

Let A be a total Σ-algebra.

2.2.2.1 Satisfaction of a Single Equation What does it mean for A to satisfy an equation? The standard answer is as follows: No matter which values (in AU_{Σ}) are assigned to the variables of the equation, its two sides evaluate to the same value. Generalizing a bit, we might also consider variables not occurring in the equation. (These should not matter, and indeed they do not. We will return to this issue in paragraph 3.2.1.4.)

Therefore, let V be a set (of variables) and (t, u) be a V -equation. An assignment of values in AU_{Σ} to the variables in V is simply a function f : V \overline{}AU_{Σ}, and the evaluation of the V -terms t and u is provided by its Σhomomorphic extension f^{#}U_{Σ}. Thus, A V -satisfies (t, u), denoted by A ⊧_{V} t = u, if ∀f ∈ Set (V, AU_{Σ}) .t (f^{#}U_{Σ}) = u (f^{#}U_{Σ}), or, equivalently, if ∀h ∈ Set^{Σ} (V F_{Σ}, A) .t (hU_{Σ}) = u (hU_{Σ}).

2.2.2.2 Satisfaction of a Set of Equations Let E be a set of equations. The total Σ-algebra A is said to satisfy E if it satisfies every equation in E.

The pair (Σ, E) is called a presentation. A total (Σ, E)-algebra is a total Σ-algebra satisfying E.

The total (Σ, E)-algebras determine a full subcategory Set^{(Σ,E)} of Set^{Σ}.

2.2.2.2.1 An Initial Algebra Let ≡_{E} denote the congruential closure of the ground instances of the equations in E. Then the quotient total Σ-algebra 0F_{Σ}/ ≡_{E} is an initial total (Σ, E)-algebra.

3 General Algebras

In the total case, the rôle played by the category Set is to provide sets, serving as carriers of algebras, and functions, serving as components of algebras and as homomorphisms. The key idea of this paper is that this rôle may be taken over by some other category. (The idea itself is not new ([12, page 221]), but we believe our treatment of initiality and of the independence of satisfaction of the set of variables considered, to be so.)

However, not any category will do. We have to be able to form the finite powers AU_{Σ}^{n}. To allow headroom for the generalization to several sorts, we at once generalize this to finite products B_{0} ×⋯×B_{n−1}. A category with all finite products is said to be Cartesian.

However, the mere existence of products is not quite enough. For each tuple of objects we need a specific product (object and projections). The assignment of a product to each object tuple is usually called a finite product structure ([3, page 196]), but for the sake of brevity, we will introduce the term Cartesian structure. (Of course, any Cartesian category may be equipped with a Cartesian structure. The point is that we have to decide on one in particular.)

A functor F from one category with Cartesian structure to another is usually said to be strict finite product preserving (also [3, page 196]) if it preserves the structure, i.e. if it takes the product (object and projections) of each tuple B_{0}, …, B_{n−1} to the product of B_{0}F, …, B_{n−1}F. For the sake of brevity, we will call such a functor Cartesian. Cartesian functors also preserve (finite) mediating and product arrows, natural transformations τ from one Cartesian functor to another satisfy τ_{B_{0}×···×B_{n−1}} = τ_{B_{0}} × ⋯ × τ_{B_{n−1}}, and the ^{#} operation of an adjunction between Cartesian functors preserves (finite) product arrows.

The categories with Cartesian structure and the Cartesian functors constitute a category CartStruct.

3.1 Signatures

3.1.1 Algebras and Homomorphisms

Let C be a category with a Cartesian structure. Define the category C^{Σ} of Σ-algebras and Σ-homomorphisms by

• A Σ-algebra A comprises – a carrier C-object AU_{Σ}

– for each n ∈ N and f ∈ Σ_{n} a C-arrow f_{A} : AU_{Σ}^{n} \overline{}AU_{Σ}.

• A Σ-homomorphism h : A \overline{}B is a C-arrow AU_{Σ} \overline{}BU_{Σ} such that (1).

• Composition is composition in C.

• The identities are defined by id_{A} = id_{AU_{Σ}}.

3.1.2 Initiality

In the total case the initial algebra was obtained as the image of an initial object under a left adjoint \overline{}Set^{Σ}, viz. the left adjoint Set \overline{}Set^{Σ} of the forgetful functor Set^{Σ} \overline{}Set. This suggests that we should look for a left adjoint \overline{}C^{Σ}, e.g. a left adjoint C \overline{}C^{Σ} of the forgetful functor C^{Σ} \overline{}C. Unfortunately, we have been unable to define such a left adjoint in general. (Moreover, C does not necessarily possess an initial object.)

However, as Set^{Σ} has an initial object, a left adjoint Set^{Σ} \overline{}C^{Σ} would be useful. But, are there any functors between C^{Σ} and Set^{Σ}, or more generally, D^{Σ}, where D is some category with a Cartesian structure? The operation of lifting will enable us to construct such functors from Cartesian functors between C and D.

3.1.3 Lifting

Extend the assignment C ↦ C^{Σ} to a functor −^{Σ} : CartStruct \overline{}Cat by: If C and D are CartStruct-objects and F is a CartStruct-arrow C \overline{}D, the Cat-arrow, i.e. the lifted functor, F^{Σ} : C^{Σ} \overline{}D^{Σ} is defined by

• If A is a C^{Σ}-object, the D^{Σ}-object AF^{Σ} is defined by

– The D-object AF^{Σ}U_{Σ} = AU_{Σ}F.

– For each n ∈ N and f ∈ Σ_{n} the D-arrow f_{AF^{Σ}} = f_{A}F.

• (h : A \overline{}B) ⟼ hF.

Theorem 1 Let

• C and D be categories with Cartesian structure

• F : C \overline{}D and U : D \overline{}C be Cartesian functors

such that F U. Then F^{Σ} U^{Σ}. (‘Lifting preserves adjunctions.’)

Proof: Let A ∈ C^{Σ}_{0}. We have to prove that AF^{Σ} is free over A w.r.t. U^{Σ}. A universal arrow from A to U^{Σ} is an element of C^{Σ} (A, AF^{Σ}U^{Σ}) ⊆

C (AU_{Σ}, AF^{Σ}U^{Σ}U_{Σ}), where

AF^{Σ}U^{Σ}U_{Σ} = AF^{Σ}U_{Σ}U
= AU_{Σ}F U.

Let η : I_{C} \overline{}^{.} F ∘ U be the unit of the adjunction. Then η_{AU_{Σ}} is a C-arrow AU_{Σ} \overline{}AU_{Σ}F U. By naturality of η it is in fact a C^{Σ}-arrow A \overline{}AF^{Σ}U^{Σ}.

We claim that AF^{Σ} is free over A w.r.t. U^{Σ} with universal arrow η_{AU_{Σ}}, which is fairly straightforward to prove.

3.1.4 An Initial Algebra

Let F : Set \overline{}C and U : C \overline{}Set be Cartesian functors such that F U. Then also F^{Σ} U^{Σ}, where F^{Σ} : Set^{Σ} \overline{}C^{Σ}.

Corollary 4 0F_{Σ}F^{Σ} is initial in C^{Σ}.

3.2 Presentations

3.2.1 Satisfaction

3.2.1.1 Satisfaction of a Single Equation

3.2.1.1.1 Satisfaction w.r.t. a Set of Variables It seems difficult to generalize the definition of satisfaction of an equation by a total algebra given in subparagraph 2.2.2.1. In [1] we defined a C^{Σ}-object A to satisfy a set E of equations if AU^{Σ} did, leading to the restriction F ∘ U = ISet mentioned in the introduction.

However, the concept of satisfaction of an equation by a total algebra A may be formulated in another way that is easily generalizable. [11] attributes the idea to Lawvere. In our opinion, the idea may best be explained by appealing to denotational semantics of simple applicative languages, where the denotation of a term is a function from environments to values, where an environment is a function from variables to values. In our case, the set of variables is V and the set of values is AU_{Σ}, making the set of environments ^{V} AU_{Σ} and the set of possible term denotations Set (^{V} AU_{Σ}, AU_{Σ}). The ‘semantic function’

h_{AV} : V F_{Σ}U_{Σ} \overline{}Set (^{V} AU_{Σ}, AU_{Σ}) is then defined in the following way: The

function th_{AV} : ^{V} AU_{Σ} \overline{}AU_{Σ} is defined by g (th_{AV}) = t (g^{#}U_{Σ}).

Corollary 5 A total Σ-algebra A V -satisfies a V -equation (t, u) iff th_{AV} = uh_{AV}.

However, we need a compositional definition of h_{AV}. Such a definition is provided by the following two corollaries:

Corollary 6 Let v ∈ V and g : V \overline{}AU_{Σ}. Then g (vη_{V} h_{AV}) = vg.

Corollary 7 [f (t_{0}, …, t_{n−1})] h_{AV} = ⟨t_{0}h_{AV} , …, t_{n−1}h_{AV} ⟩ ∘ f_{A}

The intended generalization may seem to require the existence of arbitrary (non-finite) products ^{V} AU_{Σ}. However, this is not the case, as an equation contains a finite number of variables only. However, this finite number may be arbitrarily large, so we need an infinite set of variables altogether. On the other hand, a countable number is sufficient, as the variables of distinct equations are completely unrelated, although they may have the same names.

To simplify matters, we identify variables with the natural numbers. Furthermore, the only sets of variables (natural numbers) we will consider, are the natural numbers themselves and the set N of (all) natural numbers.

Corollary 8 NF_{Σ}U_{Σ}^{2} = ⋃_{n∈N} nF_{Σ}U_{Σ}^{2}

Proof: Straightforward, using lemma 9.

Thus, an N-equation is an n-equation for some natural number n. Moreover, there is a least such number.

Please notice that m ≤ n iff m ⊆ n, in which case mF_{Σ}U_{Σ} ⊆ nF_{Σ}U_{Σ} (by corollary 1), entailing that mF_{Σ}U_{Σ}^{2} ⊆ nF_{Σ}U_{Σ}^{2}.

Let n be a natural number. The function h_{An} : nF_{Σ}U_{Σ} \overline{}Set (AU_{Σ}^{n}, AU_{Σ}) then satisfies vη_{n}h_{An} = the vth projection AU_{Σ}^{n} \overline{}AU_{Σ}.

Let A be a C^{Σ}-object. The function^{3} h_{An} : nF_{Σ}U_{Σ} \overline{}C (AU_{Σ}^{n}, AU_{Σ}) is defined by

• vη_{n}h_{An} = the vth projection AU_{Σ}^{n} \overline{}AU_{Σ}

• [f (t_{0}, …, t_{m−1})] h_{An} = ⟨t_{0}h_{An}, …, t_{m−1}h_{An}⟩ ∘ f_{A}.

The Σ-algebra A is now said to n-satisfy an n-equation (t, u), denoted by A ⊧_{n} t = u, if th_{An} = uh_{An}.

Define a function g_{An} : n \overline{}C (AU_{Σ}^{n}, AU_{Σ}) by vg_{An} = vη_{n}h_{An}. (In the total case, a (vg_{An}) = va.)

3.2.1.1.2 Absolute Satisfaction Whether the algebra A n-satisfies an n-equation, should ideally not depend on n. In paragraph 3.2.1.4 we will show that under a certain condition this is indeed the case, but for the moment we will content ourselves with the following: Let (t, u) be an N-equation, and let n be the least natural number such that (t, u) is an n-equation. The Σ-algebra A is said to satisfy the equation (t, u), denoted by A ⊧ t = u, if it n-satisfies it.

3.2.1.2 Satisfaction of a Set of Equations Let E be a set of N-equations, making (Σ, E) a presentation. The Σ-algebra A is said to satisfy E, or to be a (Σ, E)-algebra, if it satisfies every equation in E. The (Σ, E)-algebras determine a full subcategory C^{(Σ,E)} of C^{Σ}.

3.2.1.3 Satisfaction and Lifting

Lemma 10 Let

• C and D be categories with Cartesian structure

• F : C \overline{}D be a Cartesian functor

• A be a C^{Σ}-object.

3Its domain is a set.

Then

1. Let t be an n-term. Then th_{AF^{Σ},n} = th_{An}F.

2. Let v ∈ n. Then vg_{AF^{Σ},n} = vg_{An}F.

3. An n-equation n-satisfied by A is also n-satisfied by AF^{Σ}.

4. An N-equation satisfied by A is also satisfied by AF^{Σ}.

5. A set of N-equations satisfied by A is also satisfied by AF^{Σ}.

Proof:

1. Straightforward induction on t.

2. Straightforward, using 1..

3. Straightforward, using 1..

4. Straightforward, using 3..

5. Straightforward, using 4..

3.2.1.4 More on Absolute Satisfaction We will now show that under a certain condition n-satisfaction does not depend on n.

Let m and n be natural numbers such that m ≤ n. Then for each i ∈ m ig_{An} is a C-arrow AU_{Σ}^{n} \overline{}AU_{Σ}, entailing that ⟨0g_{An}, …, (m − 1) g_{An}⟩ is a C-arrow AU_{Σ}^{n} \overline{}AU_{Σ}^{m}.

Lemma 11 Let t be an m-term. Then th_{An} = ⟨0g_{An}, …, (m − 1) g_{An}⟩ ∘ th_{Am}.

Lemma 12 Assume that C = Set and that mF_{Σ}U_{Σ} is non-empty. Then ⟨0g_{An}, …, (m − 1) g_{An}⟩ is epi.

Proof: We have to prove that ⟨0g_{An}, …, (m − 1) g_{An}⟩ : AU_{Σ}^{n} \overline{}AU_{Σ}^{m} is surjective. Therefore, let a ∈ AU_{Σ}^{m}. We have to prove that there is a b ∈ AU_{Σ}^{n} such that

a = b ⟨0g_{An}, …, (m − 1) g_{An}⟩
= (b [0g_{An}] , …, b [(m − 1) g_{An}])
= [0b, …, (m − 1) b] ,

which is equivalent to that ⋀_{i∈m} ia = ib, determining b on m ⊆ n. If i ∈ n \ m, ib may be taken to be any element of AU_{Σ}. Thus, we have to prove that AU_{Σ} is non-empty.

As mF_{Σ}U_{Σ} is non-empty, m is non-empty or Σ contains a constant symbol. Thus, there are two cases:

• m is non-empty. Let i ∈ m, entailing that ia ∈ AU_{Σ}.

• Σ contains a constant symbol, entailing that AU_{Σ} is non-empty (by lemma 2).

Assume that there is a faithful Cartesian functor V : C \overline{}Set (this being the abovementioned condition).

Lemma 13 Assume that mF_{Σ}U_{Σ} is non-empty. Then ⟨0g_{An}, …, (m − 1) g_{An}⟩ is epi.

Proof: As the faithful V reflects epics, we may prove this by proving that ⟨0g_{An}, …, (m − 1) g_{An}⟩ V is epi, where

⟨0g_{An}, …, (m − 1) g_{An}⟩ V = ⟨0g_{An}V, …, (m − 1) g_{An}V ⟩
= ⟨0g_{AV^{Σ},n}, …, (m − 1) g_{AV^{Σ},n}⟩ ,

which is epi (by lemma 12).

Corollary 9 Let (t, u) be an m-equation. Then A ⊧_{m} t = u iff A ⊧_{n} t = u.

Proof: We have to prove that

th_{Am} = uh_{Am}

⇔ th_{An} = uh_{An}
⇔ ⟨0g_{An}, …, (m − 1) g_{An}⟩ ∘ th_{Am} = ⟨0g_{An}, …, (m − 1) g_{An}⟩ ∘ uh_{Am},

where ⇒ is trivial, whereas ⇐ follows from the fact that ⟨0g_{An}, …, (m − 1) g_{An}⟩ is epi (in the presence of the m-terms t and u).

This shows that n-satisfaction is indeed independent of n (under the condition that there is a faithful Cartesian functor C \overline{}Set).

In the total case lemma 12 may be used directly in the proof of corollary 9. Moreover, V -satisfaction is independent of V (for arbitrary variable sets V), which may be proved in a similar fashion.

3.2.2 Initiality

Recall the initial total (Σ, E)-algebra 0F_{Σ}/ ≡_{E}. Then (0F_{Σ}/ ≡_{E}) F^{Σ} ∈ C^{(Σ,E)}_{0}.

Theorem 2 (0F_{Σ}/ ≡_{E}) F^{Σ} is initial in C^{(Σ,E)}.

Proof: Let A ∈ C^{(Σ,E)}_{0}, entailing that AU^{Σ} ∈ Set^{(Σ,E)}_{0} (by lemma 10, part 5). We have to prove that

∃_{1}h ∈ C^{(Σ,E)} [(0F_{Σ}/ ≡_{E}) F^{Σ}, A]
= C^{Σ} [(0F_{Σ}/ ≡_{E}) F^{Σ}, A] ,

which is equivalent to that

∃_{1}h ∈ Set^{Σ} (0F_{Σ}/ ≡_{E}, AU^{Σ})
= Set^{(Σ,E)} (0F_{Σ}/ ≡_{E}, AU^{Σ}) ,

which holds.

4 Concluding Remarks

We have made a general construction based on some parameters: an adjunction F U : C \overline{}Set in CartStruct. From C we have constructed the category of Σalgebras and its full subcategory of (Σ, E)-algebras. Using the functors, we have shown that the two categories have initial objects closely related to the ordinary term and quotient algebras, which we believe to be new results. The same goes for the condition under which we have found satisfaction to be independent of the set of variables considered.

We will conclude the paper by pointing out some (possible) directions for (our) future research:

• To base the approach on algebraic (Lawvere) theories ([8]) (instead of on presentations)

• To (try to) apply our theory to some of the cases mentioned in the introduction: topological and continuous algebras, and in particular total algebras whose carrier elements are e.g. partial orders

• Generalization to several sorts

• By considering a category of signatures one might possibly obtain an institution ([2]) depending on C. This way of constructing institutions should then be compared to others, e.g. chartering ([4]).

Acknowledgements Thanks are due to S. Hegner, N. Husberg, S. Meldal, P. D. Mosses, A. Tarlecki, E. G. Wagner, and M. Walicki.

References

[1] Ø. B. Fredriksen. From sets with structure to algebras with structure. In R. J. R. Back and K. Sere, editors, Proceedings of the 5th Nordic Workshop on Program Correctness, number 18 in Åbo Akademi Reports on Computer Science and Mathematics, Ser. B, pages 62–71, Åbo Akademi University, Dept. of Computer Science, DataCity, SF–20520 Åbo, Finland, May 1994.

[2] J. A. Goguen and R. M. Burstall. Introducing institutions. In E. Clarke and D. Kozen, editors, Logics of Programs. Proceedings 1983, number 164 in Lecture Notes in Computer Science, pages 221–255. Springer-Verlag, 1984.

[3] J. A. Goguen and R. M. Burstall. Some fundamental algebraic tools for the semantics of computation. Part 1: Comma categories, colimits, signatures and theories. Theoretical Comput. Sci., 31:175–209, 1984.

[4] J. A. Goguen and R. M. Burstall. A study in the foundations of programming methodology: Specifications, institutions, charters and parchments. In D. Pitt, S. Abramsky, A. Poigné, and D. Rydeheard, editors, Category Theory and Computer Programming, number 240 in Lecture Notes in Computer Science, pages 313–333. Springer-Verlag, 1986.

[5] J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. In R. T.-Y. Yeh, editor, Current Trends in Programming Methodology. Volume IV. Data Structuring, chapter 5, pages 80–149. Prentice-Hall, Inc., 1978.

[6] J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Initial algebra semantics and continuous algebras. J. ACM, 24(1):68–95, Jan. 1977.

[7] H. Herrlich and G. E. Strecker. Category Theory. An Introduction. Allyn and Bacon, Inc., 1973.

[8] F. W. Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences, 50:869–872, 1963.

[9] K. Meinke. Topological methods for algebraic specification. Report CSR 21–93, University of Wales, University College of Swansea, Computer Science Department, Singleton Park, Swansea SA2 8PP, Great Britain, May 1993.

[10] B. Möller. On the algebraic specification of infinite objects — ordered and continuous models of algebraic types. Acta Inf., 22:537–578, 1985.

[11] A. Poigné. Algebra categorically. In D. Pitt, S. Abramsky, A. Poigné, and D. Rydeheard, editors, Category Theory and Computer Programming, number 240 in Lecture Notes in Computer Science, pages 76–102. Springer-Verlag, 1986.

[12] H. Schubert. Categories. Springer-Verlag, 1972.

[13] M. Wirsing, P. Pepper, H. Partsch, W. Dosch, and M. Broy. On hierarchies of abstract data types. Acta Inf., 20:1–33, 1983.