A Concrete Final Coalgebra Theorem for ZF Set Theory^{⋆}

Lawrence C. Paulson

                    lcp@cl.cam.ac.uk

Computer Laboratory, University of Cambridge, England

Abstract. A special final coalgebra theorem, in the style of Aczel’s [2], is proved within standard Zermelo-Fraenkel set theory. Aczel’s Anti-Foundation Axiom is replaced by a variant definition of function that admits non-well-founded constructions. Variant ordered pairs and tuples, of possibly infinite length, are special cases of variant functions. Analogues of Aczel’s Solution and Substitution Lemmas are proved in the style of Rutten and Turi [12]. The approach is less general than Aczel’s, but the treatment of non-well-founded objects is simple and concrete. The final coalgebra of a functor is its greatest fixedpoint. The theory is intended for machine implementation and a simple case of it is already implemented using the theorem prover Isabelle [10].

⋆ Thomas Forster alerted me to Quine’s work. Peter Aczel and Andrew Pitts offered considerable advice and help. Daniele Turi gave advice by electronic mail. I have used Paul Taylor’s macros for commuting diagrams. K. Mukai commented on the text. Research funded by the ESPRIT Basic Research Action 6453 ‘Types.’

Table of Contents

1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

2 An Alternative Definition of Pairs and Functions . . . . . . . . 2 2.1 Quine’s Ordered Pairs . . . . . . . . . . . . . . . . . . . . . . . . 2 2.2 Basic Definitions and Properties . . . . . . . . . . . . . . . . . . 4 2.3 Basic Properties of the Cumulative Hierarchy . . . . . . . . . . . 5

3 A Final Coalgebra . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.1 The Functor Q and the Set U . . . . . . . . . . . . . . . . . . . . 7 3.2 U is a Final Coalgebra . . . . . . . . . . . . . . . . . . . . . . . . 9

4 Solutions of Equations . . . . . . . . . . . . . . . . . . . . . . . . . 10 4.1 Preliminaries: the Binary Sum Functor . . . . . . . . . . . . . . 10 4.2 An Expanded Version of U . . . . . . . . . . . . . . . . . . . . . 11 4.3 An Embedding . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 4.4 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4.5 Solution and Substitution Lemmas . . . . . . . . . . . . . . . . . 13 4.6 Special Final Coalgebra Theorem . . . . . . . . . . . . . . . . . . 15

5 Functors Uniform on Maps . . . . . . . . . . . . . . . . . . . . . . 16 5.1 The Constant Functor . . . . . . . . . . . . . . . . . . . . . . . . 16 5.2 Binary Product . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 5.3 Binary Sum . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 5.4 Sum of a Family of Sets . . . . . . . . . . . . . . . . . . . . . . . 18 5.5 Product of a Family of Sets . . . . . . . . . . . . . . . . . . . . . 19 5.6 The Identity Functor . . . . . . . . . . . . . . . . . . . . . . . . 20

6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

A Proof of Prop. 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

1 Introduction

A recurring issue in theoretical computer science is the treatment of infinite computations. One important approach is based upon the final coalgebra. This category-theoretic notion relates to the methods of bisimulation and coinduction, which are heavily used in concurrency theory [6], functional programming [1] and operational semantics [7].

Aczel and Mendler [3] and also Barr [4] have proved that final coalgebras exist in set theory for large classes of naturally occurring functors. This might be supposed to satisfy most people’s requirements. But Aczel [2] has argued the case for a non-standard set theory in which infinite computations, and other non-well-founded phenomena, can be modelled directly. He proposes to replace set theory’s Foundation Axiom (FA) by an Anti-Foundation Axiom (AFA) that guarantees the existence of solutions to x = {x} and more generally of all systems of equations of the form x_{i} = {x_{i}, x_{j}, …}. His general final coalgebra theorem serves as a model construction to justify AFA.

Under AFA, a suitable functor F does not merely have a final coalgebra. That final coalgebra equals F ’s greatest fixedpoint. This is the natural dual of the theorem that a functor’s initial algebra is its least fixedpoint. These fixedpoints are exact, not up to isomorphism.

The elements of the final coalgebra are easily visualised. For instance, the functor A × − (the functor F such that F (Z) = A × Z on objects) yields the set of streams over A. The final coalgebra is also the greatest solution of S = A × S. If s ∈ S then

s = ⟨a_{1}, s_{1}⟩, s_{1} = ⟨a_{2}, s_{2}⟩, s_{2} = ⟨a_{3}, s_{3}⟩, …;

s is the infinite stream ⟨a_{1}, ⟨a_{2}, ⟨a_{3}, …⟩⟩⟩.

In standard set theory, the Foundation Axiom (FA) outlaws infinite descents under the membership relation. Under the standard definition of ordered pair we have b ∈ {a, b} ∈ ⟨a, b⟩. Infinitely nested pairs such as s above would create infinite ∈-descents, and therefore do not exist. In other words, the greatest fixedpoint of A × − is the empty set. This is not the final coalgebra (which does exist).

The approach proposed in this paper is not to change the axiom system, but instead to adopt new definitions of ordered pairs, functions, and derived concepts such as Cartesian products. Under the new definitions, the stream functor’s final coalgebra is indeed its (exact) greatest fixedpoint and each stream is an infinite nest of pairs. Recursion equations are solved up to equality.

My approach handles non-well-founded tuples, and more generally ordered structures. But it does not model true non-well-founded sets, such as solutions of x = {x}. It does not work for the powerset functor, even with cardinality restrictions. I do not know whether it can express nondeterminism; one way of handling sets of outcomes may be to well-order them using the Axiom of Choice.

Aczel’s book [2] puts the case for non-well-founded sets with clarity, simplicity and eloquence. Especially attractive is its presentation of four anti-foundation axioms in a uniform framework. Each axiom creates new sets and gives criteria for set equality. The axioms turn out to be pairwise incomparable; the various logicians who devised these axioms conceived four distinct notions of non-well-founded set. Is this really a fundamental notion?

I have devoted considerable effort to machine-assisted proof in ZF set theory, using the theorem prover Isabelle [8, 9]. It would be easy to separate FA from the other ZF axioms and move most of the formalisation into the resulting theory of ZF^{−}. Isabelle can support parallel developments in ZF and ZF^{−} + AF A. Mechanisation of AFA requires a formalisation of the axiom and its main consequences, such as the Solution Lemma, in a form suitable for working with particular final coalgebras. A partial implementation of my approach to final coalgebras already exists [10].

Outline. My strategy is to construct a final coalgebra to replace AFA, and then to re-play Rutten and Turi’s categorical proofs [12]. Section 2 presents basic motivation — Quine’s ordered pairs and their generalisation to functions — and proves some lemmas about the cumulative hierarchy, V_{α}. Section 3 defines the functor Q^{I} and its greatest fixedpoint U^{I} and proves that U^{I} is a final Q^{I}- coalgebra. Section 4 proves the Solution and Substitution Lemmas for set equations and the special final coalgebra theorem. Section 5 discusses functors that are (or are not!) uniform on maps. Section 6 presents conclusions.

2 An Alternative Definition of Pairs and Functions

Let us begin with informal motivation based on the work of Quine. The following section will make formal definitions.

2.1 Quine’s Ordered Pairs

In standard ZF set theory, the ordered pair ⟨a, b⟩ is defined to be {{a}, {a, b}}. The rank of ⟨a, b⟩ is therefore two levels above those of a and b; there are no solutions to b = ⟨a, b⟩. Quine [11] has proposed a definition of ordered pair that need not entail an increase of rank. Quine’s definition is complicated because (among other things) it avoids using standard ordered pairs. I regard standard pairs as indispensable, and they let us define Quine-like ordered pairs easily.

Let ⟨a, b⟩ denote the standard ordered pair of a and b. Let tuples of any length consist of ordered pairs nested to the right; thus ⟨a_{1}, …, a_{n}⟩ abbreviates ⟨a_{1}, …, ⟨a_{n−1}, a_{n}⟩⟩ for n > 2. Let A × B denote the standard Cartesian product {⟨a, b⟩ | a ∈ A ∧ b ∈ B}.

Define the variant ordered pair, ⟨a; b⟩ by

⟨a; b⟩ ≡ ({0} × a) ∪ ({1} × b).  (1)

Note that ⟨a; b⟩ is just a + b, the disjoint sum of a and b (in set theory, everything is a set). The new pairing operator is obviously injective, which is a key requirement. Also, it admits non-well-founded constructions: we have ⟨0; 0⟩ = 0 for a start.^{2}

The set equation ⟨A; z⟩ = z has a unique solution z, consisting of every (standard!) tuple of the form ⟨1, …, 1, 0, x⟩ for x ∈ A. The infinite stream

⟨A_{0}; A_{1}; …; A_{n}; …⟩

is the set of all standard tuples of the form

⟨\underbrace{1, …, 1}_{n}, 0, x⟩

for n < ω and x ∈ A_{n}. Now ⟨a; b⟩ is continuous in a and b, in the sense that it preserves arbitrary unions; thus fixedpoint methods can solve recursion equations involving variant tupling. Later we shall see that such equations possess unique fixedpoints.

Variant pairs can be generalised to a variant notion of function:

λ̃_{x∈A}b_{x} ≡ ⋃_{x∈A}{x} × b_{x}  (2)

Note that λ̃_{x∈A}b_{x} is just Σ_{x∈A}b_{x}, the disjoint sum of a family of sets. Also note that ⟨b_{0}; b_{1}⟩ is the special case λ̃_{i∈2}b_{i}, since 2 = {0, 1}. Replacing 2 by larger ordinals such as ω gives us a means of representing infinite sequences. More generally, non-standard functions can represent infinite collections that have non-well-founded elements.

Merely replacing ⟨x, b_{x}⟩ by ⟨x; b_{x}⟩ in the usual definition of function, obtaining {⟨x; b_{x}⟩ | x ∈ A}, would not admit non-well-founded constructions. The rank of such a set exceeds the rank of every b_{x}. For example, if b = {⟨0; b⟩} then {1} × b ∈ b, violating FA; thus b = {⟨0; b⟩} has no solution.

Application of variant functions is expressed using the image operator “. It is easy to check that (λ̃_{x∈A}b_{x}) “ {a} = b_{a} if a ∈ A. Also if R is a relation with domain A, then R = λ̃_{x∈A} R “ {x}; every standard relation is a variant function. The set

{f ⊆ A × ⋃ B | ∀_{x∈A} f “ {x} ∈ B}

consists of all variant functions from A to B and will serve as our definition of variant function space, A ˜→ B.

Since λ̃_{x∈A}b_{x} is not the function’s graph, it does not determine the function’s domain. For instance, λ̃_{x∈A}0 = A × 0 = 0. Clearly λ̃_{x∈A}0 = λ̃_{x∈B}0 for all A and B. If 0 ∈ B then A ˜→ B will contain both total and partial functions: applying a variant function to an argument outside its domain yields 0.

2 As usual in set theory, the number zero is the empty set.

2.2 Basic Definitions and Properties

Once we have defined the variant pairs and functions, we can substitute them in the standard definitions of Cartesian product, disjoint sum and function space. The resulting variant operators are decorated by a tilde: ˜×, ˜+, ˜→, etc. Having both standard and variant operators is the simplest way of developing the theory. The standard operators relate the new concepts to standard set theory and they remain useful for defining well-founded constructions. But the duplication of operators may seem inelegant, and it certainly requires extra care to avoid confusing them.

Definition 1. The variant ordered pair ⟨a; b⟩ is defined by

⟨a; b⟩ ≡ ({0} × a) ∪ ({1} × b).

If {b_{x}}_{x∈A} is an A-indexed family of sets then the variant function λ̃_{x∈A}b_{x} is defined by

λ̃_{x∈A}b_{x} ≡ ⋃_{x∈A}{x} × b_{x}

The variant Cartesian product, disjoint sum and partial function space between two sets A and B are defined by

A ˜× B ≡ {⟨x; y⟩ | x ∈ A ∧ y ∈ B}
A ˜+ B ≡ ({0} ˜× A) ∪ ({1} ˜× B)
A ˜→ B ≡ {f ⊆ A × ⋃ B | ∀_{x∈A} f “ {x} ∈ B}

The operators ˜× and ˜→ can be generalised to a family of sets as usual.

Definition 2. If {B_{x}}_{x∈A} is an A-indexed family of sets then their variant sum and product are defined by

˜∑_{x∈A} B_{x} ≡ {⟨x; y⟩ | x ∈ A ∧ y ∈ B_{x}}

˜∏_{x∈A} B_{x} ≡ {f ⊆ A × ( ⋃_{x∈A} ⋃ B_{x}) | ∀_{x∈A} f “ {x} ∈ B_{x}}

A first attempt at exploiting these definitions is to fix an index set I and solve the equation U = I ˜→ U. There is at least one solution, namely U = {0}, since λ̃_{i∈I} 0 = 0. But we cannot build up variant tuples starting from 0 as we can construct the distinct sets {0}, {0, {0}}, . . .. A variant tuple whose components are all the empty set is itself the empty set.

Since I ˜→ 0 = 0 if I ≠ 0, one possible solution to U = I ˜→ U is U = 0. Also I ˜→ {0} = {0}. As it happens, U = {0} is the greatest solution.

Proposition 3. If U = I ˜→ U then U = 0 or U = {0}.

Proof. Suppose not, for contradiction. Then U contains a non-empty element; there exist y_{0} and x_{0} with y_{0} ∈ x_{0} ∈ U. By the definition of ˜→ it follows that y_{0} = ⟨i, y_{1}⟩ where i ∈ I and y_{1} ∈ x_{1} ∈ U for some x_{1}. Repeating this argument yields the infinite ∈-descent y_{0} = ⟨i, y_{1}⟩, y_{1} = ⟨i, y_{2}⟩, y_{2} = ⟨i, y_{3}⟩, …, contradicting FA. ⊓ ⊔

If tuples are to get built up, we must start with some atoms. To keep the atoms distinct from the variant tuples, each atom should contain some element that is not a (standard) pair. One atom seems sufficient. We may use 1 since by definition 1 = {0} and the empty set is not a pair. Our final coalgebra theorem will therefore be based upon the greatest solution of

U = {1} ∪ (I ˜→ U).

Some background lemmas are needed first.

2.3 Basic Properties of the Cumulative Hierarchy

The following results will help prove closure and uniqueness properties below.

Let α, β range over ordinals and λ, μ range over limit ordinals. The cumulative hierarchy of sets is traditionally defined by cases:

V_{0} = 0
V_{α+1} = P(V_{α})
V_{μ} = ⋃_{α<μ} V_{α}

More convenient is the equivalent definition

V_{α} ≡ ⋃_{β<α} P(V_{β}).  (3)

Kunen [5, pp. 95–7] discusses the cumulative hierarchy, using the notation R(α) instead of V_{α}. Note some elementary consequences of these definitions:

Lemma 4. If α is an ordinal and μ is a limit ordinal then

α ⊆ V_{α}
V_{α} × V_{α} ⊆ V_{α+2}
V_{μ} × V_{μ} ⊆ V_{μ}
V_{μ} + V_{μ} ⊆ V_{μ}

It turns out that V_{μ} is closed under the formation of variant tuples and functions.

Lemma 5. If A ⊆ V_{μ} and b_{x} ⊆ V_{μ} for all x ∈ A then λ̃_{x∈A}b_{x} ⊆ V_{μ}.

Proof. This follows by the definition of λ̃, monotonicity and the facts noted above:

λ̃_{x∈A}b_{x} = ⋃_{x∈A}{x} × b_{x}
⊆ ⋃_{x∈V_{μ}}{x} × V_{μ}
⊆ V_{μ} × V_{μ}
⊆ V_{μ}
⊓ ⊔

Thus V_{μ+1} has closure properties for variant products and sums analogous to those of V_{μ} for standard products and sums. It is even closed under variant function space. Lemma 6. Let μ be a limit ordinal.

(a) If A ⊆ V_{μ} then A ˜→ V_{μ+1} ⊆ V_{μ+1}.

(b) V_{μ+1} ˜× V_{μ+1} ⊆ V_{μ+1}.

(c) V_{μ+1} ˜+ V_{μ+1} ⊆ V_{μ+1}. Proof. Obvious by the definitions and the previous lemma. ⊓ ⊔

These results will allow application of the Knaster-Tarski fixedpoint theorem to construct a final coalgebra. The next group of results will be used in the uniqueness proof. Lemma 7. If A ∩ V_{α} ⊆ B for every ordinal α then A ⊆ B. Proof. By the Foundation Axiom, V = ⋃_{α} V_{α}, where V is the universal class. Thus A = ⋃_{α}(A ∩ V_{α}). If A ∩ V_{α} ⊆ B for all α then ⋃_{α}(A ∩ V_{α}) ⊆ B and the result follows.

Using the lemma above requires some facts concerning intersection with V_{α}. Definition 8. A set A is transitive if A ⊆ P(A). Lemma 9. V_{α} is transitive for every ordinal α. Proof. See Kunen [5, p. 95]. ⊓ ⊔

Now we can go down the cumulative hierarchy as well as up. Lemma 10. If ⟨a, b⟩ ∈ V_{α+1} then a ∈ V_{α} and b ∈ V_{α}. Proof. Suppose ⟨a, b⟩ ∈ V_{α+1}; this is equivalent to {{a}, {a, b}} ∈ P(V_{α}) and to {{a}, {a, b}} ⊆ V_{α}. Thus {a, b} ∈ V_{α} and since V_{α} is transitive {a, b} ⊆ V_{α}. ⊓ ⊔ Lemma 11. If {b_{x}}_{x∈A} is an A-indexed family of sets then

(a) (λ̃_{x∈A}b_{x}) ∩ V_{α+1} ⊆ λ̃_{x∈A}(b_{x} ∩ V_{α})

(b) (λ̃_{x∈A}b_{x}) ∩ V_{α} ⊆ ⋃_{β<α} λ̃_{x∈A}(b_{x} ∩ V_{β})

Proof. For (a) we have, by the previous lemma,

(λ̃_{x∈A}b_{x}) ∩ V_{α+1} = {⟨x, y⟩ | x ∈ A ∧ y ∈ b_{x}} ∩ V_{α+1}
⊆ {⟨x, y⟩ | x ∈ A ∧ y ∈ b_{x} ∧ y ∈ V_{α}}
= λ̃_{x∈A}(b_{x} ∩ V_{α}).

For (b) we have, by the definition of V_{α} and properties of unions,

(λ̃_{x∈A}b_{x}) ∩ V_{α} = (λ̃_{x∈A}b_{x}) ∩ ⋃_{β<α} P(V_{β})
= ⋃_{β<α}(λ̃_{x∈A}b_{x}) ∩ V_{β+1}
⊆ ⋃_{β<α} λ̃_{x∈A}(b_{x} ∩ V_{β}).

The last step is by (a) above. ⊓ ⊔

3 A Final Coalgebra

Rutten and Turi’s excellent survey [12] of final semantics includes a categorical presentation of Aczel’s main results. Working in the superlarge category of classes and maps between classes, they note that FA is equivalent to ‘V is an initial Palgebra’ while AFA is equivalent to ‘V is a final P-coalgebra.’ Put in this way, AFA certainly looks more attractive than the other anti-foundation axioms.

The present treatment of final semantics follows their development closely. Instead of assuming that V is a final P-coalgebra, we shall define a functor Q^{I}, where I is an arbitrary index set, and construct a final Q^{I}-coalgebra, called U^{I}. The Solution and Substitution Lemmas and the Special Final Coalgebra Theorem carry over directly.

I work not in the category of classes but in the usual category Set of sets, which has standard functions as maps. While the former category allows certain statements to be expressed succinctly, it also requires numerous technical lemmas concerning set-based maps, etc. From the standpoint of mechanised proof, one must also bear in mind that classes have no formal existence under the ZF axioms, and class maps are two removes from existence.

3.1 The Functor Q and the Set U

Let I be an index set, which will remain fixed throughout the paper. A typical choice for I would be some limit ordinal such as ω. Note that ω ˜→ A contains all ω-sequences over A; we shall find that U^{ω} contains all ω-sequences over itself. Moreover, finite sequences can be represented by ω-sequences containing infinitely many 0s, because 0 ∈ U^{I} (see Lemma 31 below).

Definition 12. The functor Q^{I} : Set → Set is defined on objects by

Q^{I}(A) ≡ {1} ∪ (I ˜→ A)

and on maps as follows. If π : A → B then Q^{I}(π) : Q^{I}(A) → Q^{I}(B) satisfies

Q^{I}(π)(1) ≡ 1
Q^{I}(π)(λ̃_{i∈I} a_{i}) ≡ λ̃_{i∈I} π(a_{i}).

Reasons for this definition of Q^{I} were given after Prop. 3. It is easy to check that the functor preserves the identity map and composition. The next step is to define a set U^{I} to be the greatest solution of U^{I} = Q^{I}(U^{I}) and prove that U^{I} is a final Q^{I}-coalgebra. Since U^{I} = {1} ∪ (I ˜→ U^{I}) we may regard the elements of U^{I} as nested I-indexed tuples built up from the atom 1. If some application requires a larger set of atoms, the modifications to the theory should be obvious.

To solve U^{I} = Q^{I}(U^{I}) we may apply the Knaster-Tarski fixedpoint theorem. This gives an explicit definition.

Definition 13. Let μ be a limit ordinal such that I ⊆ V_{μ}. Then

U^{I} ≡ ⋃_{Z⊆V_{μ+1}} Z ⊆ Q^{I}(Z).

Henceforth let us regard I as fixed and drop the superscripts. The next two results indicate that U really is a fixedpoint of Q, in fact the greatest postfixedpoint. This justifies proof by coinduction on U. The second result also confirms that the choice of the ordinal μ above does not matter, provided I ⊆ V_{μ}.

Proposition 14. U = Q(U).

Proof. For the Knaster-Tarski theorem to apply, Q must be a monotone operator over the powerset of V_{μ}. Clearly Q is monotone and, by Lemma 6, Q(V_{μ+1}) ⊆ V_{μ+1}. ⊓ ⊔

Proposition 15. If Z ⊆ Q(Z) then Z ⊆ U.

Proof. The result follows by the definition of U if we can establish Z ⊆ V_{μ+1}. By Lemma 7 it suffices to prove ∀_{z∈Z} z ∩ V_{α} ⊆ V_{μ} for all α. Proceed by transfinite induction on the ordinal α.

Let z ∈ Z. Then z ∈ Q(Z) = {1} ∪ (I ˜→ Z). The case z = 1 is trivial. So we may assume z = λ̃_{i∈I} z_{i}, with z_{i} ∈ Z for all i ∈ I. In this case we have

(λ̃_{i∈I} z_{i}) ∩ V_{α} ⊆ ⋃_{β<α} λ̃_{i∈I} (z_{i} ∩ V_{β})
⊆ ⋃_{β<α} λ̃_{i∈I} V_{μ}
⊆ V_{μ}

by Lemma 11, the induction hypothesis for z_{i} and Lemma 5. Since z ∩ V_{α} ⊆ V_{μ} for all α we have z ⊆ V_{μ} for all z ∈ Z. This establishes Z ⊆ V_{μ+1}. ⊓ ⊔ 3.2 U is a Final Coalgebra

To prove that U is a final coalgebra requires showing that for every map f : A → Q(A) there exists a unique map π : A → U such that π = Q(π) ∘ f:

A  \overline{π} \overline{}U
∥
f ∥

Q(A) \overline{Q(π)} \overline{}Q(U)

For the remainder of this section, let the set A and the map f : A → Q(A) be fixed.

Lemma 16. There exists π : A → U such that π(a) = Q(π)(f(a)) for all a ∈ A.

Proof. The function π is defined by π(a) ≡ ⋃_{n<ω} π_{n}(a), where {π_{n}}_{n<ω} is as follows:

π_{0}(a) ≡ 0
π_{n+1}(a) ≡ Q(π_{n})(f(a))

Suppose a ∈ A and prove π(a) = Q(π)(f(a)) by cases. If f(a) = 1 then the equation reduces to 1 = 1. If f(a) = λ̃_{i∈I} a_{i} then simple continuity reasoning establishes the equation:

π(a) = ⋃_{n<ω} π_{n}(a)
= ⋃_{n<ω} π_{n+1}(a)
= ⋃_{n<ω} λ̃_{i∈I} π_{n}(a_{i})
= λ̃_{i∈I} ⋃_{n<ω} π_{n}(a_{i})
= λ̃_{i∈I} π(a_{i})
= Q(π)(λ̃_{i∈I} a_{i})
= Q(π)(f(a))

To show π : A → U, use coinduction (Prop. 15). Let Z = {π(a) | a ∈ A} and prove Z ⊆ Q(Z). If z ∈ Z then z = π(a) for some a ∈ A. There are two cases, as usual. If f(a) = 1 then z = 1 ∈ Q(Z) and if f(a) = λ̃_{i∈I} a_{i} then z = λ̃_{i∈I} π(a_{i}) ∈ Q(Z).

Since U is the greatest post-fixedpoint of Q, this establishes Z ⊆ U. And since Z is the range of π, this establishes π : A → U. ⊓ ⊔ Lemma 17. If π = Q(π) ∘ f and π′ = Q(π′) ∘ f then π = π′.

Proof. Again using Lemma 7, let us use transfinite induction on the ordinal ξ to prove

∀_{a∈A} π(a) ∩ V_{ξ} ⊆ π′(a).

Let a ∈ A. If f(a) = 1 then π(a) = π′(a) = 1. If f(a) = λ̃_{i∈I} a_{i} then

π(a) ∩ V_{ξ} = (λ̃_{i∈I} π(a_{i})) ∩ V_{ξ}
⊆ ⋃_{η<ξ} λ̃_{i∈I} (π(a_{i}) ∩ V_{η})
⊆ ⋃_{η<ξ} λ̃_{i∈I} π′(a_{i})
= π′(a)

using the hypothesis, Lemma 11, the induction hypothesis for η < ξ and monotonicity of λ̃.

Since π(a) ∩ V_{ξ} ⊆ π′(a) for every ordinal ξ, we have π(a) ⊆ π′(a). By symmetry we have π′(a) ⊆ π(a) and therefore π(a) = π′(a) for all a ∈ A. ⊓ ⊔

Theorem 18. U is a final Q-coalgebra.

Proof. Immediate by the previous two lemmas. ⊓ ⊔

4 Solutions of Equations

In his development of set theory with AFA, Aczel [2] defines systems of setequations and proves the Solution Lemma: each system has a unique solution. Aczel introduces a class X of variables and a class V_{X} of sets built up from variables (but not themselves variables). His Substitution Lemma says that any assignment f : X → V of sets to variables can be extended to a substitution function f̂: V_{x} → V. Aczel uses these lemmas to exhibit a unique morphism for his Special Final Coalgebra Theorem.

Aczel proves the Solution and Substitution Lemmas using concrete set theory, but in Rutten and Turi’s categorical presentation the proofs are much shorter. A key fact in their development is that V is (assuming AFA) a final P-coalgebra. My presentation is similar, replacing V by U, P by Q and AFA by Theorem 18. Also I replace the category of classes by the category of sets, but this I think is only a matter of taste.

4.1 Preliminaries: the Binary Sum Functor

Recall that ˜+ is the variant form of disjoint sum, defined by A ˜+B ≡ ({0} ˜×A)∪ ({1} ˜×B). It is a coproduct in the category Set, which means that for every pair of maps f : A → C and g : B → C there exists a unique map [f, g] : A ˜+ B → C making the diagram commute:

[figure: A; \overline{Ĩnl}; A ˜+ B; Ĩnr; B]

[figure: f; [f, g]; g]

C

Here the injections Ĩnl : A → A ˜+ B and Ĩnr : B → A ˜+ B and the case analysis operator [f, g] are defined in the obvious way.

To make ˜+ into a functor we must define its action on maps. If j : A → A′ and k : B → B′ then j ˜+ k : A ˜+ A′ → B ˜+ B′ is defined (as usual) by

j ˜+ k ≡ [Ĩnl ∘ j, Ĩnr ∘ k].  (4)

Some obvious properties of [f, g] and of j ˜+ k are listed below for later reference.

Lemma 19. Let f : A → C, g : B → C, h : C → D, j : A → A′ and k : B → B′ be maps. Then

[f, g] ∘ Ĩnl = f
[f, g] ∘ Ĩnr = g
h ∘ [f, g] = [h ∘ f, h ∘ g]
[Ĩnl, Ĩnr] = id_{A ˜+B}
[f, g] ∘ (j ˜+ k) = [f ∘ j, g ∘ k]
(j ˜+ k) ∘ Ĩnl = Ĩnl ∘ j
(j ˜+ k) ∘ Ĩnr = Ĩnr ∘ k

4.2 An Expanded Version of U

Let X be a set of variables or indeterminates for use in equations. The set U_{X}^{I} is constructed in the same way as U^{I} except that each level contains a copy of X. Thus an element of U_{X}^{I} is just like an element of U^{I} except that it may contain elements of X at each stage in its construction. In formalizing equations between sets, each left-hand side will consist of a variable from X while each right-hand side will be drawn from U_{X}^{I}. The definition of U_{X}^{I} closely resembles that of U^{I}.

Definition 20. Let μ be a limit ordinal such that X ∪ I ⊆ V_{μ}. Then

U^{I} ≡ ⋃_{Z⊆V_{μ+1}} Z ⊆ Q^{I}(X ˜+ Z).

Let us again drop the superscript I. The proof of the following result is omitted because of its similarity to the proof for U.

Proposition 21. Let U_{X} be defined as above. Then

(a) U_{X} = Q(X ˜+ U_{X}).

(b) If Z ⊆ Q(X ˜+ Z) then Z ⊆ U_{X}.

(c) U_{X} is the final coalgebra for the functor Q(X ˜+ −).

Proof. See Appendix A.

4.3 An Embedding

There is an obvious embedding σ_{X} : U → U_{X} that copies an element of U into U_{X} and never introduces an element of X:

σ_{X}(1) = 1
σ_{X}(λ̃_{i∈I} u_{i}) = λ̃_{i∈I} Ĩnr(σ_{X}(u_{i}))

The equations can be summarised neatly by σ_{X} = Q(Ĩnr ∘ σ_{X}). The embedding will be useful for creating equations with constant right-hand sides.

Although the embedding is obvious, its existence deserves to be proved. Aczel derives the analogous embedding from V into V_{X} by direct recourse to AFA [2]. Rutten and Turi [12] omit this step, which in their categorical style might be done by showing that V_{X} is a final coalgebra for the functor P(X + −).

Lemma 22. There exists a unique map σ_{X} : U → U_{X} such that

σ_{X} = Q(Ĩnr ∘ σ_{X}).

Proof. Recalling the equation U_{X} = Q(X ˜+U_{X}), consider the following diagram:

U  \overline{σ_{X}}  \overline{}U_{X} ∥
Q(Ĩnr) ∥

Q(X ˜+ U) \overline{Q(id_{X} ˜+ σ_{X})} \overline{}Q(X ˜+ U_{X})

Since (U, Q(Ĩnr)) is a coalgebra for Q(X ˜+ −) and U_{X} is a final coalgebra, there exists a unique map σ_{X} such that the diagram commutes. Now

σ_{X} = Q(id_{X} ˜+ σ_{X}) ∘ Q(Ĩnr)
= Q((id_{X} ˜+ σ_{X}) ∘ Ĩnr)
= Q(Ĩnr ∘ σ_{X})

by Lemma 19. ⊓ ⊔ 4.4 Substitution

Let f : X → U be a function. Then the substitution function f̂ : U_{X} → U essentially copies its argument, replacing everything of the form Ĩnl(x) by f(x) for x ∈ X. This case analysis can be expressed with the help of the [f, f̂] notation:

f̂(1) = 1
f̂(λ̃_{i∈I} z_{i}) = λ̃_{i∈I} [f, f̂](z_{i})

These two equations can be expressed succinctly by f̂ = Q([f, f̂]).

Clearly, substitution over a ‘term’ containing no ‘variables’ can have no effect. The formal statement of this fact justifies calling σ_{X} an embedding.

Lemma 23 (Embedding). Let f : X → U and g : U_{X} → U be functions. If g = Q([f, g]) then g ∘ σ_{X} = id_{U}.

Proof. By Lemma 22 and Lemma 19 we have

g ∘ σ_{X} = Q([f, g]) ∘ Q(Ĩnr ∘ σ_{X})
= Q([f, g] ∘ Ĩnr ∘ σ_{X})
= Q(g ∘ σ_{X}).

Since U = Q(U), the following diagram commutes:

U  \overline{ĝ ∘ σ_{X}} \overline{}U ∥  ∥

∥  ∥

Q(U) \overline{Q(ĝ ∘ σ_{X})} \overline{}Q(U)

Since U is the final Q-coalgebra, it has only one homomorphism into itself, namely the identity. This yields g ∘ σ_{X} = id_{U}. ⊓ ⊔

4.5 Solution and Substitution Lemmas

If X is a set of variables then a function ν : X → U_{X} defines a system of equations of the form x = ν_{x} for all x ∈ X. Such a system has a unique solution f : X → U such that f(x) = f̂(ν_{x}) for x ∈ X. More concisely, a solution satisfies f = f̂∘ ν.

Lemma 24 (Solution). Let ν : X → U_{X} be a function. There exist unique functions f : X → U and f̂: U_{X} → U such that

f = f̂∘ ν and f̂ = Q([f, f̂]).

Proof. Recalling the equation U_{X} = Q(X ˜+ U), consider the following diagram:

[figure: X; \overline{ν}; U_{X}; \overline{π}; U] ∥
Q([ν, id_{U_{X}}]) ∥

Q(U_{X}) \overline{Q(π)}\overline{}Q(U)

Since (U_{X}, Q([ν, id_{U_{X}}])) is a Q-coalgebra and U is a final Q-coalgebra, there exists a unique map π such that the diagram commutes. By Lemma 19 we have

π = Q(π) ∘ Q([ν, id_{U_{X}}])
= Q(π ∘ [ν, id_{U_{X}}])
= Q([π ∘ ν, π ∘ id_{U_{X}}])
= Q([π ∘ ν, π])

Putting f̂ = π and f = π ∘ ν yields the desired functions. As for uniqueness, if f = f̂∘ ν and f̂ = Q([f, f̂]) then f̂ = π by finality of U. ⊓ ⊔

In this proof, note that Q([ν, id_{U_{X}}]) substitutes using ν but only to depth one. The following lemma justifies the f̂ notation for substitution by f. The idea is to convert f : X → U into a trivial system of equations, then solve them.

Lemma 25 (Substitution). Let f : X → U be a function. There exists a unique function f̂: U_{X} → U such that f̂ = Q([f, f̂]).

Proof. Consider the composed map σ_{X} ∘ f : X → U_{X}. Apply the Solution Lemma with ν = σ_{X} ∘ f, obtaining maps g : X → U and ĝ : U_{X} → U such that g = ĝ ∘ ν and ĝ = Q([g, ĝ]). Now

g = ĝ ∘ σ_{X} ∘ f = f

by Lemma 23. Putting f̂ = ĝ we obtain f̂ = Q([f, f̂]). Uniqueness follows by the uniqueness property of the Solution Lemma. ⊓ ⊔

I should prefer to prove the Substitution Lemma earlier, but the simplest proof seems to rely on the Solution Lemma. Turi has pointed out (by electronic mail) that the Substitution Lemma has a trivial proof if U_{X} is defined to be an initial algebra rather than a final coalgebra. But then U_{X} would contain only finite constructions; the embedding σ_{X} : U → U_{X} would not exist; nonwell-founded objects obtained via the Solution Lemma could not participate in further set equations.

4.6 Special Final Coalgebra Theorem

The main theorem applies to functors that are uniform on maps. This notion is due to Aczel [2], but I follow Rutten and Turi’s [12] formulation.

We shall no longer work in the category Set of sets but rather in the full subcategory Set_{U} whose objects are the subsets of U. Recall that U, in turn, depends upon the choice of index set I; we can make U as large as necessary.

Definition 26. A functor F : Set_{U} → Set_{U} is uniform on maps if for all A ⊆ U there exists a mapping ϕ_{A} : F (A) → U_{A} such that

F (h) = ĥ ∘ ϕ_{A} for all h : A → U.

The mapping ϕ_{A} is called the U_{A} translation.

Let us only consider functors that preserve inclusion maps. This is a natural restriction since all functors preserve identity maps, and inclusion maps are identity maps when regarded as sets. All such functors on Set_{U} have fixedpoints.

Lemma 27. If the functor F : Set_{U} → Set_{U} preserves inclusions then there exists an object J_{F} : Set_{U} such that J_{F} is the greatest fixedpoint and greatest post-fixedpoint of F.

Proof. Apply the Knaster-Tarski fixedpoint theorem to the lattice of subsets of U. The functor F is necessarily monotone because it preserves inclusions; if ι : A → B then F (ι) : F (A) → F (B); thus if A ⊆ B then F (A) ⊆ F (B). ⊓ ⊔

Theorem 28 (Special Final Coalgebra). If the functor F : Set_{U} → Set_{U} preserves inclusions and is uniform on maps then J_{F} is a final F -coalgebra.

Proof. Let (A, f) be an F -coalgebra. We must exhibit a unique map h : A → J_{F} such that h = F (h) ∘ f:

A  \overline{h} \overline{}J_{F} ∥
f ∥

F (A) \overline{F (h)}\overline{}F (J_{F})

Since F is uniform on maps, h = F (h) ∘ f is equivalent to h = ĥ ∘ ϕ_{A} ∘ f. Such a map h is precisely a solution of the system of equations a = ϕ_{A}(f(a)) for a ∈ A. Applying the Solution Lemma with ν = ϕ_{A} ∘ f, we obtain a unique map h : A → U such that h = F (h) ∘ f.

A standard coinduction argument proves h : A → J_{F}. Writing h“A for the image of A under h, we have

h“A = (F (h) ∘ f)“A
= F (h)“(f“A)
⊆ F (h)“F (A)
⊆ F (h“A)

since h : A → h“A and F (h) : F (A) → F (h“A).

The range of h is thus a post-fixedpoint of F and is contained in the greatest post-fixedpoint, namely J_{F}. ⊓ ⊔

5 Functors Uniform on Maps

If F is uniform on maps then, in essence, its effect upon a map h : A → U can be expressed as the substitution of h over a pattern derived from the argument; if b ∈ F (A) then F (h)(b) = ĥ(ϕ_{A}(b)). Most natural functors are uniform on maps but there is at least one glaring exception. Let us examine some typical cases, starting with a very easy one.

5.1 The Constant Functor

If C ⊆ U then let K_{C} be the constant functor such that K_{C}(A) = C for all A : Set_{U} and such that K_{C}(f) = id_{C} for all maps f : A → A′.

Proposition 29. If C : Set_{U} then the constant functor K_{C} : Set_{U} → Set_{U} is uniform on maps.

Proof. Let A be a set such that A : Set_{U}. Define ϕ_{A} : C → U_{A} by ϕ_{A}(c) = σ_{A}(c) for all c ∈ C. Now

K_{C}(h)(c) = c = (ĥ ∘ σ_{A})(c) = (ĥ ∘ ϕ_{A})(c)

for all c ∈ C by Lemma 23. ⊓ ⊔

5.2 Binary Product

The set U satisfies the inclusion U ˜× U ⊆ U. So it is easy to see that ˜× : Set_{U} × Set_{U} → Set_{U} is a functor when extended to maps in the standard way. If f : A → A′ and g : B → B′ are maps then f ˜× g : A ˜× B → A′ ˜× B′ is the map that takes ⟨a; b⟩ to ⟨f(a); g(b)⟩.

Proposition 30. If F, G : Set_{U} → Set_{U} are uniform on maps, then the functor

F (−) ˜× G(−) : Set_{U} → Set_{U}

is uniform on maps.

Proof. Let A be a set such that A : Set_{U}, or equivalently A ⊆ U. Clearly we have F (A) ˜× G(A) : Set_{U}. Since F and G are uniform on maps there exist U_{A} translations

ϕ_{A} : F (A) → U_{A} such that F (h) = ĥ ∘ ϕ_{A}, and
ψ_{A} : G(A) → U_{A} such that G(h) = ĥ ∘ ψ_{A}

for all h : A → U. We must define a U_{A} translation for F (−) ˜× G(−).

Let θ_{A} = ϕ_{A} ˜× ψ_{A}. Thus θ_{A}(⟨b; c⟩) = ⟨ϕ_{A}(b); ψ(b)⟩ for all b ∈ F (A) and c ∈ G(A). Now

(F (−) ˜× G(−))(h) = F (h) ˜× G(h)
= (ĥ ∘ ϕ_{A}) ˜× (ĥ ∘ ψ_{A})
= (ĥ ˜× ĥ) ∘ (ϕ_{A} ˜× ψ_{A})
= ĥ ∘ (ϕ_{A} ˜× ψ_{A})
= ĥ ∘ θ_{A}

and θ_{A} is the desired U_{A} translation. Replacing ĥ ˜×ĥ by ĥ above is valid because ĥ ˜× ĥ is applied only to variant pairs in that context. ⊓ ⊔

5.3 Binary Sum

The proposition about ˜+ resembles the one about ˜× presented above, but first we have to show that U is closed under ˜+.

Lemma 31. U ˜+ U ⊆ U.

Proof. Since U ˜+U = ({0} ˜×U)∪({1} ˜×U) and U is closed under ˜×, it suffices to show {0, 1} ⊆ U. By coinduction (Prop. 15) it suffices to show {0, 1} ⊆ Q({0, 1}). This holds because

Q({0, 1}) = {1} ∪ (I ˜→ {0, 1})

and 0 = λ̃_{i∈I} 0 ∈ I ˜→ {0, 1}. ⊓ ⊔

Recall that ˜+ is a functor on Set whose effect on maps was described in Sect. 4.1. Now we know that ˜+ is also a functor in the full subcategory Set_{U}.

Proposition 32. If F, G : Set_{U} → Set_{U} are uniform on maps, then the functor

F (−) ˜+ G(−) : Set_{U} → Set_{U}

is uniform on maps.

Proof. Let A be a set such that A : Set_{U}. Then F (A) ˜+ G(A) : Set_{U} and there exist U_{A} translations

ϕ_{A} : F (A) → U_{A} such that F (h) = ĥ ∘ ϕ_{A}, and
ψ_{A} : G(A) → U_{A} such that G(h) = ĥ ∘ ψ_{A}

for all h : A → U.

Let θ_{A} = ϕ_{A} ˜+ ψ_{A}. Then

(F (−) ˜+ G(−))(h) = F (h) ˜+ G(h)
= (ĥ ∘ ϕ_{A}) ˜+ (ĥ ∘ ψ_{A})
= (ĥ ˜+ ĥ) ∘ (ϕ_{A} ˜+ ψ_{A})
= ĥ ∘ (ϕ_{A} ˜+ ψ_{A})
= ĥ ∘ θ_{A}

and θ_{A} is the desired U_{A} translation. ⊓ ⊔

5.4 Sum of a Family of Sets

Let {B_{x}}_{x∈C} be a C-indexed family of sets. If C ⊆ U and B_{x} ⊆ U for all x ∈ C then we have ˜∑_{x∈C} B_{x} ⊆ U. Note that ˜∑_{x∈C} B_{x} is the usual generalisation of C ˜×B

to allow B to depend upon x ∈ C; the two functors have the same effect upon maps. But the proposition about ˜∑ differs in one key respect from that about ˜×: the index set is not given by a functor but is constant.

Proposition 33. If C : Set_{U} and {F_{x} : Set_{U} → Set_{U}}_{x∈C} is a C-indexed family of functors that are uniform on maps, then the functor

˜∑_{x∈C} F_{x}(−) : Set_{U} → Set_{U}

is uniform on maps.

Proof. Let A be a set such that A : Set_{U}. Then ˜∑_{x∈C} F_{x}(A) : Set_{U}. There exists

a U_{A} translation ϕ_{x,A} : F_{x}(A) → U_{A} such that F_{x}(h) = ĥ ∘ ϕ_{x,A} for all x ∈ A and h : A → U.

The U_{A} translation for ˜∑_{x∈C} F_{x}(−), called θ_{A}, is defined by

θ_{A}(⟨x; y⟩) = ⟨σ_{A}(x), ϕ_{x,A}(y)⟩

for all x ∈ C and c ∈ F_{x}(A). Recall that σ_{A} is the inclusion map from U into U_{A}. Now by Lemma 23 we have

ĥ(θ_{A}(⟨x; y⟩)) = ĥ(⟨σ_{A}(x), ϕ_{x,A}(y)⟩)
= ⟨ĥ(σ_{A}(x)), ĥ(ϕ_{x,A}(y))⟩
= ⟨x, F_{x}(h)⟩
= ( ˜∑_{x∈C} F_{x}(h))(⟨x; y⟩)

which proves ĥ ∘ θ_{A} = ( ˜∑_{x∈C} F_{x}(−))(h). ⊓ ⊔

5.5 Product of a Family of Sets

Again let {B_{x}}_{x∈C} be a C-indexed family of sets. If C ⊆ I (not C ⊆ U as above!)

and B_{x} ⊆ U for all x ∈ C then ˜∏_{x∈C} B_{x} ⊆ I ˜→ U ⊆ U.

Thus ˜∏ : Set_{U}^{I} → Set_{U} is a functor whose effect on maps is as follows. If {f_{x} : B_{x} → B′_{x}}_{x∈C} is a C-indexed family of maps then

˜∏_{x∈C} f_{x} : ˜∏_{x∈C} B_{x} → ˜∏_{x∈C} B′_{x}

is the usual pointwise map that takes λ̃_{x∈C}b_{x} to λ̃_{x∈C}f_{x}(b_{x}).

Proposition 34. If C ⊆ I and {F_{x} : Set_{U} → Set_{U}}_{x∈C} is a C-indexed family of functors that are uniform on maps, then the functor

˜∏_{x∈C} F_{x}(−) : Set_{U} → Set_{U}

is uniform on maps.

Proof. Let A be a set such that A : Set_{U}. Then ˜∏_{x∈C} F_{x}(A) : Set_{U}. There exists

a U_{A} translation ϕ_{x,A} : F_{x}(A) → U_{A} such that F_{x}(h) = ĥ ∘ ϕ_{x,A} for all x ∈ A and h : A → U.

Let θ_{A} = ˜∏_{x∈C} ϕ_{x,A}. Now

( ˜∏_{x∈C} F_{x}(−))(h) = ˜∏_{x∈C} F_{x}(h)

= ˜∏_{x∈C} ĥ ∘ ϕ_{x,A}

= ( ˜∏_{x∈C} ĥ) ∘ ( ˜∏_{x∈C} ϕ_{x,A})

= ĥ ∘ ( ˜∏_{x∈C} ϕ_{x,A})
= ĥ ∘ θ_{A}

and θ_{A} is the desired U_{A} translation. ⊓ ⊔ 5.6 The Identity Functor

These results suggest that any functor that operates on ‘constructions’ in a pointwise fashion is probably uniform on maps. But there is one glaring exception.

Proposition 35. The identity functor Id : Set_{U} → Set_{U} is not uniform on maps.

Proof. Suppose Id : Set_{U} → Set_{U} is uniform on maps. Then if A ⊆ U then there is a mapping ϕ_{A} : A → U_{A} such that h = ĥ ∘ ϕ_{A} for all h : A → U.

Let A = {1} and define h_{1}, h_{2} : {1} → U by h_{1}(1) = 1 and h_{2}(1) = ⟨1; 1⟩. Then 1 = ĥ_{1}(ϕ_{A}(1)); by the definition of substitution, this implies ϕ_{A}(1) = 1. Also ⟨1; 1⟩ = ĥ_{2}(ϕ_{A}(1)); by the definition of substitution, this implies ϕ_{A}(1) = ⟨a; b⟩ for some a, b ∈ A ˜+ U_{A}. But then 1 = ⟨a; b⟩, which is absurd. ⊓ ⊔

An alternative proof uses the Special Final Coalgebra Theorem. If Id is uniform on maps then J_{Id} is a final Id-coalgebra. But a final Id-coalgebra must be a singleton set, while J_{Id} = U and U contains 0 and 1 as elements.

This circumstance is awkward. The natural way of constructing suitable functors is to combine constant and identity functors by products, sums, etc. Since the identity functor is not uniform on maps, this approach fails. Various similar functors are uniform on maps, such as − ˜× K_{{0}} and − ˜× −; both have the singleton set {0} as their greatest fixedpoint. Assuming AFA does not help; the identity functor is not uniform on maps in Aczel’s system either.

6 Conclusions

In semantics it is not customary to worry about the construction of a particular object provided it has the desired abstract properties. From this point of view, the general theorems of Aczel and Mendler [3] and Barr [4] yield final coalgebras for a great many functors.

But there is an undoubted interest in Aczel’s weaker final coalgebra theorem, proved using the Anti-Foundation Axiom (AFA) [2]. Its appeal is its concreteness. The set of streams over A is simply the greatest fixedpoint of the functor A × −, which is also that functor’s final coalgebra. Its elements are easily visualised objects of the form ⟨a_{0}, a_{1}, a_{2}, …⟩.

The original motivation for my work was to treat streams and other infinite data structures. I wished to use the standard ZF axiom system as it was automated using Isabelle. Thomas Forster suggested that Quine’s treatment of ordered pairs might help. Generalizing this treatment led to the new definition of functions (and thus infinite streams), in order to compare the approach with AFA. This part of the work closely follows Aczel, and Rutten and Turi [12], from the Substitution Lemma onwards.

My Special Final Coalgebra Theorem is less general than Aczel’s, especially as regards concurrency. Here is a typical example. Let P_{f} be the finite powerset operator, which returns the set of all finite subsets of its argument. Consider the set P of processes defined as the final coalgebra of P_{f}(A × −). With AFA the final coalgebra is the greatest solution of P = P_{f}(A × P), and if p ∈ P then

p = {⟨a_{1}, p_{1}⟩, …, ⟨a_{n}, p_{n}⟩}

with n < ω, a_{1}, …, a_{n} ∈ A and p_{1}, …, p_{n} ∈ P. My approach does not handle general set constructions, only variant tuples and functions; I do not know how to model P_{f} respecting set equalities such as {x, y} = {y, x} = {x, y, x}.

My approach works best in its original application, infinite data structures. We can model the main constructions in U^{ω}. Since U^{ω} ⊆ V_{ω+1}, each infinite data structure is a subset of V_{ω} and thus is a set of hereditarily finite sets.^{3} Section 2.1 discussed infinite streams. The set S of streams over A is the greatest solution of S = A ˜× S, and is the final coalgebra of the functor A ˜× −.

Thus we have an account of non-well-founded phenomena that is concrete enough to be understood directly. One can argue about the constructive validity of the cumulative hierarchy, but V_{ω} is uncontroversial even from an intuitionistic viewpoint. In contrast the general final coalgebra theorems [3, 4], with their quotient-of-sum constructions, are anything but concrete.

Aczel has shown that by adopting AFA we can obtain final coalgebras as greatest fixedpoints, dualising a standard result about initial algebras. My approach is another way of doing the same thing, though for fewer functors. Whether or not one choose to adopt AFA hinges on a number of issues: philosophical, theoretical, practical. Variant tuples and functions are a simple alternative.

References

1. Abramsky, S., The lazy lambda calculus, In Resesarch Topics in Functional Programming, D. A. Turner, Ed. Addison-Wesley, 1977, pp. 65–116

2. Aczel, P., Non-Well-Founded Sets, CSLI, 1988

3. Aczel, P., Mendler, N., A final coalgebra theorem, In Category Theory and Computer Science (1989), D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts,, A. Poigné, Eds., Springer, pp. 356–365, LNCS 389

4. Barr, M., Terminal coalgebras in well-founded set theory, Theoretical Comput. Sci. 114, 2 (1993), 299–315

5. Kunen, K., Set Theory: An Introduction to Independence Proofs, North-Holland, 1980

6. Milner, R., Communication and Concurrency, Prentice-Hall, 1989

7. Milner, R., Tofte, M., Co-induction in relational semantics, Theoretical Comput. Sci. 87 (1991), 209–220

8. Paulson, L. C., Set theory for verification: I. From foundations to functions, J. Auto. Reas. 11, 3 (1993), 353–389

9. Paulson, L. C., Set theory for verification: II. Induction and recursion, Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993, To appear in J. Auto. Reas.

10. Paulson, L. C., A fixedpoint approach to implementing (co)inductive definitions, In 12th Conf. Auto. Deduct. (1994), A. Bundy, Ed., Springer, pp. 148–161, LNAI 814

3 An hereditarily finite set is one built in finitely many stages from the empty set.

11. Quine, W. V., On ordered pairs and relations, In Selected Logic Papers. Random House, 1966, ch. VIII, pp. 110–113, Orginally published 1945–6

12. Rutten, J. J. M. M., Turi, D., On the foundations of final semantics: Non-standard sets, metric spaces, partial orders, In Semantics: Foundations and Applications (1993), J. de Bakker, W.-P. de Roever,, G. Rozenberg, Eds., Springer, pp. 477– 530, LNCS 666

A Proof of Prop. 21

Abbreviate the functor Q(X ˜+ −) as Q_{X}. This simplifies the statement of the Proposition:

Proposition. Let U_{X} = ⋃_{Z⊆V_{μ+1}} Z ⊆ Q_{X}(Z). Then

(a) U_{X} = Q_{X}(U_{X}).

(b) If Z ⊆ Q_{X}(Z) then Z ⊆ U_{X}.

(c) U_{X} is the final Q_{X}-coalgebra.

Proof of (a). Apply the Knaster-Tarski theorem. Clearly Q_{X} is monotone; by Lemma 6, Q_{X}(V_{μ+1}) ⊆ V_{μ+1}. ⊓ ⊔

Before continuing, we need some more elementary facts about the cumulative hierarchy.

Lemma 36. If α is an ordinal then

A × B ⊆ V_{α} implies A, B ⊆ V_{α}
A + B ⊆ V_{α} implies A, B ⊆ V_{α}
A ˜× B ⊆ V_{α+1} implies A, B ⊆ V_{α+1}
A ˜+ B ⊆ V_{α+1} implies A, B ⊆ V_{α+1}

Proof. The first part holds by Lemma 10 and the transitivity of V_{α}. The other parts hold by similar tedious reasoning from the definitions. ⊓ ⊔

We now tackle the next part of Prop. 21.

Proof of (b). Use the definition of U_{X} after first establishing Z ⊆ V_{μ+1}. By the previous Lemma, it suffices to prove X ˜+ Z ⊆ V_{μ+1}. By Lemma 7, it suffices to prove

∀_{w∈X ˜+Z} w ∩ V_{α} ⊆ V_{μ}

for all α. Proceed by transfinite induction on the ordinal α.

Let w ∈ X ˜+ Z. There are two cases. The first case is w = ⟨0; x⟩ = 0 + x for x ∈ X. Since X ⊆ V_{μ}, clearly 0 + x ⊆ V_{μ}. The second case is w = ⟨1; z⟩ = 1 + z for z ∈ Z. We must show 1 + z ⊆ V_{μ}; by Lemma 4 it suffices to show z ⊆ V_{μ}.

Since z ∈ Z, we have z ∈ Q_{X}(Z) = {1} ∪ (I ˜→ X ˜+ Z). The case z = 1 is trivial. So we may assume z = λ̃_{i∈I} w_{i}, with w_{i} ∈ X ˜+ Z for all i ∈ I. In this case we have

(λ̃_{i∈I} w_{i}) ∩ V_{α} ⊆ ⋃_{β<α} λ̃_{i∈I} (w_{i} ∩ V_{β})
⊆ ⋃_{β<α} λ̃_{i∈I} V_{μ}
⊆ V_{μ}

by Lemma 11, the induction hypothesis for w_{i} and Lemma 5. Since w ∩ V_{α} ⊆ V_{μ} for all α we have w ⊆ V_{μ} for all w ∈ X ˜+ Z. This establishes X ˜+ Z ⊆ V_{μ+1} as required. ⊓ ⊔

The final part of Prop. 21 is that U_{X} is the final Q_{X}-coalgebra. This requires showing that for every map f : A → Q_{X}(A) there exists a unique map π : A → U_{X} such that π = Q_{X}(π) ∘ f:

A  \overline{π} \overline{}U_{X} ∥
f ∥

Q_{X}(A) \overline{Q_{X}(π)} \overline{}Q_{X}(U_{X})

Let the set A and the map f : A → Q_{X}(A) be fixed, and consider each property separately. Note that the functor Q_{X} operates on maps as follows:

Q_{X}(π)(λ̃_{i∈I} a_{i}) = λ̃_{i∈I} (id_{X} ˜+ π)(a_{i})

Lemma 37. There exists π : A → U_{X} such that π(a) = Q_{X}(π)(f(a)) for all a ∈ A.

Proof. The function π is defined by π(a) ≡ ⋃_{n<ω} π_{n}(a), where {π_{n}}_{n<ω} is as follows:

π_{0}(a) ≡ 0
π_{n+1}(a) ≡ Q_{X}(π_{n})(f(a))

Suppose a ∈ A and prove π(a) = Q(π)(f(a)) by cases. If f(a) = 1 then the equation reduces to 1 = 1. The other possibility is f(a) = λ̃_{i∈I} b_{i} where b_{i} ∈ X ˜+ A if i ∈ I. Continuity reasoning, using the previous lemma, establishes the equation:

π(a) = ⋃_{n<ω} π_{n}(a)
= ⋃_{n<ω} π_{n+1}(a)
= ⋃_{n<ω} Q_{X}(π_{n})(λ̃_{i∈I} b_{i})
= ⋃_{n<ω} λ̃_{i∈I} (id_{X} ˜+ π_{n})(b_{i})
= λ̃_{i∈I} ⋃_{n<ω}(id_{X} ˜+ π_{n})(b_{i})
= λ̃_{i∈I} (id_{X} ˜+ π)(b_{i})
= Q_{X}(π)(λ̃_{i∈I} b_{i})
= Q_{X}(π)(f(a))

Note that ⋃_{n<ω}(id_{X} ˜+ π_{n})(b_{i}) = (id_{X} ˜+ π)(b_{i}) above holds by case analysis on b_{i} ∈ X ˜+ A and continuity of the variant injections.

To show π : A → U_{X}, use coinduction. Let Z = {π(a) | a ∈ A} and prove Z ⊆ Q_{X}(Z). If z ∈ Z then z = π(a) for some a ∈ A. There are two cases, as usual. If f(a) = 1 then z = 1 ∈ Q_{X}(Z). If f(a) = λ̃_{i∈I} b_{i} (where b_{i} ∈ X ˜+ A) then

z = π(a) = Q_{X}(π)(λ̃_{i∈I} b_{i}) = λ̃_{i∈I} (id_{X} ˜+ π)(b_{i}) ∈ Q(X ˜+ Z) = Q_{X}(Z).

Since U_{X} is the greatest post-fixedpoint of Q_{X}, this establishes Z ⊆ U_{X}. And since Z is the range of π, this establishes π : A → U_{X}. ⊓ ⊔

Lemma 38. If π = Q_{X}(π) ∘ f and π′ = Q_{X}(π′) ∘ f then π = π′.

Proof. Using Lemma 7, let us use transfinite induction on the ordinal ξ to prove

∀_{a∈A} π(a) ∩ V_{ξ} ⊆ π′(a).

Let a ∈ A. If f(a) = 1 then π(a) = π′(a) = 1. If f(a) = λ̃_{i∈I} b_{i} (where b_{i} ∈ X ˜+A) then

π(a) ∩ V_{ξ} = (λ̃_{i∈I} (id_{X} ˜+ π)(b_{i})) ∩ V_{ξ}
⊆ ⋃_{η<ξ} λ̃_{i∈I} ((id_{X} ˜+ π)(b_{i}) ∩ V_{η})
⊆ λ̃_{i∈I} (id_{X} ˜+ π′)(b_{i})
= π′(a)

using the hypothesis, Lemma 11 and monotonicity of λ̃. The reasoning also uses

(id_{X} ˜+ π)(b_{i}) ∩ V_{η} ⊆ (id_{X} ˜+ π′)(b_{i}),

which holds by case analysis on b_{i} ∈ X ˜+ A, a further application of Lemma 11, and the induction hypothesis for η′ where η′ < η < ξ.

Since π(a) ∩ V_{ξ} ⊆ π′(a) for every ordinal ξ, we have π(a) ⊆ π′(a). By symmetry we have π′(a) ⊆ π(a) and therefore π(a) = π′(a) for all a ∈ A. ⊓ ⊔

Theorem 39. U_{X} is a final Q_{X}-coalgebra.

Proof. Immediate by the previous two lemmas. ⊓ ⊔

This article was processed using the LaTEX macro package with LLNCS style