Co-induction and Co-recursion in Higher-order Logic^{∗}

Lawrence C. Paulson Computer Laboratory, University of Cambridge

Abstract

A theory of recursive and corecursive definitions has been developed in higher-order logic (HOL) and mechanised using Isabelle. Least fixedpoints express inductive data types such as strict lists; greatest fixedpoints express co-inductive data types, such as lazy lists. Well-founded recursion expresses recursive functions over inductive data types; co-recursion expresses functions that yield elements of co-inductive data types. The theory rests on a traditional formalization of infinite trees.

The theory is intended for use in specification and verification. It supports reasoning about a wide range of computable functions, but it does not formalize their operational semantics and can express noncomputable functions also. The theory is demonstrated using lists and lazy lists as examples. The emphasis is on using co-recursion to define lazy list functions, and on using co-induction to reason about them.

Key words. Isabelle, higher-order logic, co-induction, co-recursion

Copyright \begin{matrix}c \\ ◯ \end{matrix} 1993 by Lawrence C. Paulson

∗Research funded by the SERC (grants GR/G53279, GR/H40570) and by the ESPRIT Basic Research Actions 3245 ‘Logical Frameworks’ and 6453 ‘Types’. Isabelle has enjoyed long-standing support from the British SERC, dating from the Alvey Programme (grant GR/E0355.7).

Contents

1 Introduction 1

2 HOL in Isabelle 2 2.1 Higher-order logic as an meta-logic . . . . . . . . . . . . . . . . . . . 3 2.2 Higher-order logic as an object-logic . . . . . . . . . . . . . . . . . . . 3 2.3 Type definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.4 Further HOL types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.5 Sets in HOL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3 Least and greatest fixedpoints 7 3.1 The least fixedpoint . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.2 The greatest fixedpoint . . . . . . . . . . . . . . . . . . . . . . . . . . 8

4 Infinite trees in HOL 9 4.1 A possible coding of lists . . . . . . . . . . . . . . . . . . . . . . . . . 10 4.2 Infinite trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 4.3 The formal definition of type α node . . . . . . . . . . . . . . . . . . 11 4.4 The binary tree constructors . . . . . . . . . . . . . . . . . . . . . . . 12 4.5 Products and sums for binary trees . . . . . . . . . . . . . . . . . . . 13

5 Well-founded data structures 14 5.1 Finite lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 5.2 A space for well-founded types . . . . . . . . . . . . . . . . . . . . . . 16

6 Lazy lists and co-induction 17 6.1 An infinite list . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 6.2 Equality of lazy lists; the take-lemma . . . . . . . . . . . . . . . . . . 18 6.3 Diagonal set operators . . . . . . . . . . . . . . . . . . . . . . . . . . 19 6.4 Equality of lazy lists as a gfp . . . . . . . . . . . . . . . . . . . . . . 20 6.5 Proving lazy list equality by co-induction . . . . . . . . . . . . . . . . 21

7 Lazy lists and co-recursion 22 7.1 Introduction to co-recursion . . . . . . . . . . . . . . . . . . . . . . . 22 7.2 Harder cases for co-recursion . . . . . . . . . . . . . . . . . . . . . . . 23 7.3 Deriving co-recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

8 Examples of co-induction and co-recursion 25 8.1 A type-checking rule for LList corec . . . . . . . . . . . . . . . . . . 25 8.2 The uniqueness of co-recursive functions . . . . . . . . . . . . . . . . 26 8.3 A proof about the map functional . . . . . . . . . . . . . . . . . . . . 27 8.4 Proofs about the list of iterates . . . . . . . . . . . . . . . . . . . . . 28 8.5 Reasoning about the append function . . . . . . . . . . . . . . . . . . 29 8.6 A comparison with LCF . . . . . . . . . . . . . . . . . . . . . . . . . 31

9 Conclusions 31

1 Introduction

Recursive data structures, and recursive functions over them, are of central interest in Computer Science. The underlying theory is that of inductive definitions [2]. Much recent work has focused on formalizing induction principles in type theories. The type theory of Coq takes inductive definitions as primitive [8]. The secondorder λ-calculus (known variously as System F and λ2) can express certain inductive definitions as second-order abstractions [14].

Of growing importance is the dual notion: co-inductive definitions. Milner and Tofte motivate co-induction through a simple proof about types in a functional language [25]. Tofte has proved the soundness of a type discipline for polymorphic references by co-induction [36].

In operational semantics, we may define a notion of bisimulation between two entities, and define the equality relation to be the union of all bisimulations. Such an equality relation is co-inductively defined. Co-induction is well established for reasoning in the theory of concurrency, such as Milner’s Calculus of Communicating Systems (CCS) [24]. Abramsky’s Lazy Lambda Calculus [1], which defines equality to be the union of all applicative bisimulations, has made co-induction equally important in the theory of functional programming. Howe [19] has generalized Abramsky’s equality theory, while Andrew Gordon [15] has applied it to input/output in functional languages.

Co-induction is also applicable in denotational semantics. Here we do not define the equality relation to be the union of all bisimulations; rather, we take an existing equality relation and and prove that it coincides with such a union. The relation need not be equality; Pitts has derived a co-induction rule for proving facts of the form x ⊑ y in domain theory [34]. Infinite data structures, such as lazy lists and streams, can also be expressed co-inductively. The dual of recursion, called co-recursion, can express certain functions involving co-inductive types.

There are many approaches to formalizing co-induction and co-recursion. Mendler [23] has proposed extending λ2 with inductive and co-inductive types, equipped with recursion and co-recursion operators. More recently, Geuvers [13] has shown that co-inductive types can be contructed from inductive types, and vice versa. Leclerc and Paulin-Mohring [21] investigate various formalizations of streams in the Coq system. Although type-theoretic approaches predominate, Aczel’s Anti-Foundation Axiom (AFA) [3] asserts the existence of non-well-founded sets. Some authors, such as Milner and Tofte [25], propose Aczel’s set theory as a foundation for their work.

Church’s higher-order logic (HOL) is perfectly adequate for formalizing both inductive and co-inductive definitions. The constructions are not especially difficult. A key tool is the Knaster-Tarski theorem, which yields least and greatest fixedpoints of monotone functions. Trees, finite and infinite, are represented as sets of nodes. Recursion is derivable in its most general form, for arbitrary well-founded relations. Co-recursion and co-induction have straightforward definitions.

Compared with other type theories, HOL has the advantage of being simple, stable and well-understood. But λ2 and Coq have an inbuilt operational semantics

Figure 1: Isabelle’s object logics

based on reduction, while a HOL theory can only suggest an operational interpretation. HOL admits non-computable functions, which is sometimes advantageous and sometimes not.

Higher-order logic is extremely successful in verification, mainly hardware verification [7]. The HOL system [16] is particularly popular. T. F. Melham formalized and mechanised a theory of inductive definitions for the HOL system [22]; my work uses different principles to lay the foundation for mechanizing a broader class of definitions. Some of the extensions (mutual recursion, extending the language of type constructors) are also valid in set theory, and are described in elsewhere [33]. One unexplored possibility is that trees may have infinite branching.

The present paper is chiefly concerned with co-induction and co-recursion. §2 briefly introduces Isabelle and its formalization of HOL. §3 describes the least and greatest fixedpoint operators. §4 presents the representation of infinite trees. §5 considers finite lists and other well-founded data structures. §6 concerns lazy lists, deriving co-induction principles for type-checking and equality. §7 introduces and derives co-recursion, while §8 presents examples. Finally, §9 gives conclusions and discusses related work.

2 HOL in Isabelle

The proofs described below have been conducted with the help of Isabelle, a generic theorem prover. Isabelle implements several object-logics (Figure 1). These include first-order logic (FOL), Zermelo-Fraenkel set theory (ZF), Constructive Type Theory (CTT), and higher-order logic (HOL) [32].

Isabelle has logic programming features, such as unification and proof search. Every Isabelle object-logic can take advantage of these. Isabelle’s rewriter and classical reasoning package can be used with logics having the appropriate properties. See the documentation [30, 31] for more information.

For this paper, we may regard Isabelle simply as an implementation of higherorder logic. There are many others, such as TPS [4], EKL [20], IMPS [11] and the HOL system [16]. I shall describe the theory of recursion in formal detail, to facilitate its mechanization in any suitable system.

2.1 Higher-order logic as an meta-logic

Isabelle exploits the power of higher-order logic on two levels. At the meta-level, Isabelle uses a fragment of intuitionistic HOL to mechanize inference in various object-logics. One of these object-logics is classical HOL.

The meta-logic, as a fragment of HOL, is based upon the typed λ-calculus. It uses λ-abstraction to formalize the object-logic’s binding operators, such as ∀x.ϕ(x), ∏_{x∈A} .B(x), ϵx . ϕ(x) and ⋃_{x∈A} . B(x), in the same manner as Church did for higherorder logic [6]. The approach is fully general; each binding operator may involve any fixed pattern of arguments and bound variables, and may denote a formula, term, set, type, etc. In a recent paper [29], I discuss variable binding with examples.

Quantification in the meta-logic expresses axiom and theorem schemes. Binding operators typically involve higher-order definitions. The normalization theorem for natural deduction proofs in HOL can be used to justify the soundness of Isabelle’s representation of the object-logic. I have done a detailed proof for the case of intuitionistic first-order logic [28]; the argument applies, with obvious modifications, to any formalization of a similar syntactic form.

2.2 Higher-order logic as an object-logic

Isabelle’s formalization of higher-order logic follows Gordon [17], which is broadly equivalent to Church [6]. The connectives and quantifiers are defined in terms of three primitives: implication (→), equality (=) and descriptions (ϵx . ϕ(x)). Isabelle emphasizes a natural deduction style; its HOL theory derives natural deduction rules for the connectives and quantifiers from their obscure definitions.

The types σ, τ, …, are simple types. The type of truth values is called bool. The type of individuals plays no role in the sequel; instead, we use types of natural numbers, products, etc. Church used subscripting to indicate type, as in x_{τ}; Isabelle’s notation is x :: τ. Church wrote τσ for the type of functions from σ to τ; Isabelle’s notation is σ ⇒ τ. Nested function types may be abbreviated:

(σ_{1} ⇒ ⋯ (σ_{n} ⇒ τ) ⋯) as [σ_{1}, …, σ_{n}] ⇒ τ

ML-style polymorphism replaces Church’s type-indexed families of constants. Type schemes containing type variables α, β, …, represent families of types. For example, the quantifiers have type (α ⇒ bool) ⇒ bool; the type variable α may be instantiated to any suitable type for the quantification.^{1} As in ML, type operators have a postfix notation. For example, (σ) set is the type of sets over σ, and (σ) list is the type of lists over σ. The parentheses may be omitted if there is no ambiguity; thus natsetset is the type of sets of sets of natural numbers.

The terms are those of the typed λ-calculus. Isabelle’s notation for the application t u_{1} … u_{n} is t(u_{1}, …, u_{n}).

1In Isabelle, type variables are classified by sorts in order to control polymorphism, but this need not concern us here.

The formulae are terms of type bool. They are constructed from the logical constants ∧, ∨, → and ¬. There is no ↔ connective; the equality ϕ = ψ truth values serves as a biconditional. The quantifiers are ∀, ∃ and ∃! (unique existence).

2.3 Type definitions

Traditionally, logicians have regarded types to be nothing more than a means of avoiding paradoxes. Church [6] used just two base types, ι for individuals and o for truth values. But like many computer scientists, I regard types as a useful classification of the universe and sometimes define new types.

In Gordon’s HOL system, a new type τ can be defined from an existing type σ and a predicate ϕ :: σ ⇒ bool. Each element of type τ is represented by some element x :: σ such that ϕ(x) holds. The type definition is valid only if ∃x . ϕ(x) is a theorem, since HOL does not admit empty types. Unicity of types demands a distinction between elements of σ and elements of τ, which can be achieved by introducing an abstraction function abs :: σ ⇒ τ. Each element of τ has the form abs(x) for some x :: σ such that ϕ(x) holds. The function abs has a right inverse, the representation function rep :: τ ⇒ σ, satisfying

ϕ(rep(y)), abs(rep(y)) = y, and ϕ(x) → rep(abs(x)) = x.

As a trivial example, the singleton type unit serves as a nullary Cartesian product. It may be defined from bool by the predicate λx . x = True. Calling the abstraction function abs unit :: bool ⇒ unit, we obtain ⟨⟩ :: unit by means of the definition

                         ⟨⟩ ≡ abs unit(True)

Isabelle and the HOL system have polymorphic type systems; types may contain type variables α, β, …, which range over types. Type variables may also occur in terms:

λf :: [α, β] ⇒ bool . ∃a b . f = (λx y . x = a ∧ y = b)

This is a predicate over the type scheme [α, β] ⇒ bool. It allows us to define α × β, the Cartesian product of two types. We may then write σ × τ for any two types σ and τ.

Unlike the HOL system, Isabelle does not support type definitions. The new type and its abstraction and representation functions must be declared explicitly.

2.4 Further HOL types

Isabelle’s higher-order logic is augmented with Cartesian products, disjoint sums, the natural numbers and arithmetic. Isabelle theories define the appropriate types and constants, and prove a large collection of theorems and derived rules. Much of the formalization is inspired by Martin-Löf’s Constructive Type Theory; see Nordström et al. [26].

The singleton type unit possesses the single value ⟨⟩ :: unit.

The Cartesian product type σ × τ possesses as values ordered pairs ⟨x, y⟩, for x of type σ and y of type τ. We have the usual two projections, as well as the eliminator split:

fst :: (α × β) ⇒ α
snd :: (α × β) ⇒ β
split :: [α × β, [α, β] ⇒ γ] ⇒ γ

Many definitions below are couched in terms of split, which satisfies the equation

split(⟨a, b⟩, c) = c(a, b).

The disjoint sum type σ + τ possesses values of the form Inl(x) for x :: σ and Inr(y) for y :: τ. The eliminator, case, is similar in spirit to split:

case :: [α + β, α ⇒ γ, β ⇒ γ] ⇒ γ

The eliminator performs case analysis on its first argument:

case(Inl(a), c, d) = c(a)
case(Inr(b), c, d) = d(b)

The natural number type, nat, has the usual arithmetic operations +, −, ×, etc., of type [nat, nat] ⇒ nat. The successor function is Suc :: nat ⇒ nat. The eliminators are case analysis and primitive recursion:

                 nat case :: [nat, α, nat ⇒ α] ⇒ α

nat rec :: [nat, α, [nat, α] ⇒ α] ⇒ α

They satisfy the equations

nat case(0, a, b) = a
nat case(Suc(m), a, b) = b(m)
nat rec(0, a, b) = a
nat rec(Suc(m), a, b) = b(m, nat rec(m, a, b))

2.5 Sets in HOL

Set theory in higher-order logic dates back to Principia Mathematica’s theory of classes [37]. Although sets are essentially predicates, Isabelle’s HOL defines the type α set for sets over type α. Type α set posseses values of the form {x . ϕ(x)} for ϕ :: α ⇒ bool. The eliminator is membership:

∈ :: [α, α set] ⇒ bool

It satisfies the equations

(a ∈ {x . ϕ(x)}) = ϕ(a)
{x . x ∈ A} = A

Types distinguish this set theory from axiomatic set theories such as Zermelo-Fraenkel. All elements of a set must have the same type, and formulae such as x ∉ x and x ∈ y ∧ y ∈ z → x ∈ z are ill-typed. For each type α, there is a universal set, namely {x . True}.

Many set-theoretic operations have obvious definitions:

∀_{x∈A} . ψ(x) ≡ ∀x . x ∈ A → ψ(x)
∃_{x∈A} . ψ(x) ≡ ∃x . x ∈ A ∧ ψ(x)
A ⊆ B ≡ ∀_{x∈A} . x ∈ B
A ∪ B ≡ {x . x ∈ A ∨ x ∈ B}
A ∩ B ≡ {x . x ∈ A ∧ x ∈ B}

We have several forms of large union: the bounded union ⋃_{x∈A}.B(x), the unbounded union ⋃x . B(x), and the union of a set of sets, ⋃(S). Their definitions, and those of the corresponding intersection operators, are straightforward:

⋃_{x∈A} . B(x) ≡ {y . ∃_{x∈A} . y ∈ B(x)}
⋂_{x∈A} . B(x) ≡ {y . ∀_{x∈A} . y ∈ B(x)}
⋃x . B(x) ≡ ⋃_{x∈{x.True}} . B(x)
⋂x . B(x) ≡ ⋂_{x∈{x.True}} . B(x)
⋃(S) ≡ ⋃_{x∈S} . x
⋂(S) ≡ ⋂_{x∈S} . x

Our definitions will frequently refer to the range of a function, and to the image of a set over a function:

range(f) ≡ {y . ∃x . y = f(x)}
f “ A ≡ {y . ∃_{x∈A} . y = f(x)}

For reasoning about the set operations, I prefer to derive natural deduction rules. Introduction rules tell us how to construct elements of the set. Elimination rules tell us how to take such an element apart, typically by case analysis on the ways the element could have been created. For example, there are two introduction rules for A ∪ B:

{x ∈ A \atop x ∈ A ∪ B}  {x ∈ B \atop x ∈ A ∪ B}

The elimination rule has two minor premises, which discharge assumptions:

\begin{aligned}x ∈ A ∪ B & [x ∈ A] ; ⋮ . ; θ & [x ∈ B] ; ⋮ . ; θ \\ & θ \end{aligned}

This resembles disjunction elimination: if x ∈ A ∪ B, then either x ∈ A or x ∈ B.

The Isabelle theory includes the familiar properties of the set operations. Isabelle’s classical reasoner can prove many of these automatically. Examples:

(A ∩ B) ∪ C = (A ∪ C) ∩ (B ∪ C)
⋂(A ∪ B) = ⋂(A) ∩ ⋂(B)
(⋃_{x∈C} . A(x) ∪ B(x)) = ⋃(A “ C) ∪ ⋃(B “ C)

3 Least and greatest fixedpoints

The Knaster-Tarski Theorem asserts that each monotone function over a complete lattice possesses a fixedpoint.^{2} Tarski later proved that the fixedpoints themselves form a complete lattice [35]; we shall be concerned only with the least and greatest fixedpoints. Least fixedpoints yield inductive definitions while greatest fixedpoints yield co-inductive definitions.

Our theory of inductive definitions requires only one kind of lattice: the collection, ordered by the relation ⊆, of the subsets of a set. Monotonicity is defined by

mono(f) ≡ ∀A B . A ⊆ B → f(A) ⊆ f(B).

Monotonicity is generally easy to prove. The following results each have one-line proofs in Isabelle:

\begin{matrix}A ⊆ C & B ⊆ D \\ A ∪ B ⊆ C ∪ D \end{matrix} {A ⊆ B \atop f “ A ⊆ f “ B}  \begin{matrix}A ⊆ C & [x ∈ A]_{x} ; ⋮ . ; B(x) ⊆ D(x) \\ (⋃_{x∈A} . B(x)) ⊆ (⋃_{x∈C} . D(x)) \end{matrix}

Armed with facts such as these, it is trivial to prove that a function composed from such operators is itself monotonic.

The fixedpoint operators are called lfp and gfp. They both have type [α set ⇒ α set] ⇒ α set; they take a monotone function and yield a set.

3.1 The least fixedpoint

The least fixedpoint operator is defined by

lfp(f) ≡ ⋂{X . f(X) ⊆ X}

Roughly speaking, lfp(f) contains only those objects that must be included: they are common to all fixedpoints of f. The Isabelle theory proves that lfp is indeed the least fixedpoint of f:

f(A) ⊆ A lfp(f) ⊆ A mono(f)

lfp(f) = f(lfp(f))

2See Davey and Priestley for a modern discussion [9].

The fixedpoint property justifies both introduction and elimination rules for lfp(f), assuming we already know how to construct and take apart sets of the form f(A). Because lfp(f) is the least fixedpoint, it satisfies a better elimination rule, namely induction. The Isabelle theory derives a strong form of induction, which can easily be instantiated to yield structural induction rules:

a ∈ lfp(f) mono(f) [x ∈ f(lfp(f) ∩ {x . ψ(x)})]_{x} ; ⋮ . ; ψ(x)
ψ(a)

The set List(A) of finite lists over A is a typical example of a least fixedpoint. Lists have two introduction rules:

NIL ∈ List(A) \begin{matrix}M ∈ A & N ∈ List(A) \\ CONS(M, N) ∈ List(A) \end{matrix}

The elimination rule is structural induction:

M ∈ List(A) ψ(NIL)

[x ∈ A y ∈ List(A) ψ(y)]_{x,y} ; ⋮ .

ψ(CONS(x, y))

ψ(M)

The related principle of structural recursion expresses recursive functions on finite lists.

See §5.1 for details of the definition of lists. Elsewhere [33] I discuss the lfp induction rule and other aspects of the lfp theory.

3.2 The greatest fixedpoint

The greatest fixedpoint operator is defined by

gfp(f) ≡ ⋃{X . X ⊆ f(X)}

The dual of the least fixedpoint, it excludes only those elements that must be excluded. The Isabelle theory proves that gfp is the greatest fixedpoint of f:

A ⊆ f(A) A ⊆ gfp(f) mono(f)

gfp(f) = f(gfp(f))

As with lfp(f), the fixedpoint property justifies both introduction and elimination rules for gfp(f). But the elimination rule is not induction; instead, a further introduction rule is co-induction.

Typically gfp(f) contains infinite objects. The usual introduction rules, like those for NIL and CONS above, can only justify finite objects — each rule application justifies only one stage of the construction. But a single application of co-induction can prove the existence of an infinite object. Conversely, we should not expect to have a structural induction rule when there are infinite objects.

To show a ∈ gfp(f) by co-induction, exhibit some set X such that a ∈ X and X ⊆ f(X):

\begin{matrix}a ∈ X & X ⊆ f(X) \\ a ∈ gfp(f) \end{matrix}

This rule is weak co-induction. Its soundness is obvious by the definition of gfp and does not even require f to be monotonic. The set X is typically a singleton or the range of some function.

For monotonic f, co-induction can be strengthened in various ways. The following version is called strong co-induction below:

a ∈ X X ⊆ f(X) ∪ gfp(f) mono(f)
a ∈ gfp(f)

An even stronger version, not required below, is

a ∈ X X ⊆ f(X ∪ gfp(f)) mono(f)
a ∈ gfp(f).

Since lfp and gfp are dual notions, facts about one can be transformed into facts about the other by reversing the orientation of the ⊆ relation and exchanging ∩ for ∪, etc.

Milner’s work on concurrency [24] (with contributions from David Park) is an early use of co-induction. A bisimulation is a binary relation r satisfying a property of the form r ⊆ f(r). Two processes are called equivalent if the pair belongs to any bisimulation; thus, process equivalence is defined to be gfp(f). Two processes can be proved equivalent by exhibiting a suitable bisimulation.

The set LList(A) of lazy lists over A will be our main example of a greatest fixedpoint, starting in §6. The set contains both finite and infinite lists. In fact, LList(A) and List(A) are both fixedpoints of the same monotone function. We have List(A) ⊆ LList(A) and LList(A) shares the introduction rules of List(A), justifying the existence of finite lists.

A new principle, called co-recursion, defines certain infinite lists; co-induction proves that these lists belong to LList(A). Finally, the equality relation on LList(A) happens to coincide with the gfp of a certain function. Co-induction can therefore prove equations between infinite lists. The Isabelle theory proves many familiar laws involving the append and map functions.

Co-induction can also prove that the function defined by co-recursion is unique. Categorists will note that LList(A) is a final co-algebra, just as List(A) is an initial algebra.

4 Infinite trees in HOL

The lfp and gfp operators both have type [α set ⇒ α set] ⇒ α set. Applying them to a monotone function f :: τ set ⇒ τ set automatically instantiates α to τ; the result has type τ set. We should regard τ as a large space, from which lfp and gfp carve out various subspaces. It matters not if τ contains extraneous or ill-formed elements, since a suitable f will discard them.

My approach is to formalize all recursive data structure definitions using one particular τ, with a rich structure. I regard constructions — lists, trees, etc. — as sets of nodes. A node is a (position, label) pair and has type α node. Thus τ is α nodeset, where α is the type of atoms that may occur in the construction.

Data structures are defined as sets of type α nodesetset. The binary operators ⊗ and ⊕, analogues of the Cartesian product and disjoint sum, take two sets of that type and yield another such set. Similarly, List(A) and LList(A) are unary set operators over type α nodesetset; they can even participate in other recursive data structure definitions.

4.1 A possible coding of lists

To understand the definition of type α node, let us examine a simpler case, which only works for lists. The Isabelle theory does not actually define lists in this manner!

The finite or infinite list [x_{0}, x_{1}, …, x_{n}, …] could be represented by the set of pairs

{⟨0, x_{0}⟩, ⟨1, x_{1}⟩, …, ⟨n, x_{n}⟩, …}.

Each pair consists of the position m, a natural number, paired with the label x_{m}. To ‘cons’ an element a to the front of this list, we must add one to all the position numbers. If succfst(⟨m, x⟩) = ⟨Suc(m), x⟩ then succfst “ l increases all the position numbers in l. We may define the list constructors by

                        NIL ≡ {}

CONS(a, l) ≡ {⟨0, a⟩} ∪ succfst “ l

The function λL . {NIL} ∪ (⋃x . ⋃_{l∈L} . {CONS(x, l)}) is clearly monotone by the properties of unions. Its lfp is the set of finite lists; its gfp includes the infinite lists too. Each list has type (σ × σ) set, where σ is the type of the list’s elements.

4.2 Infinite trees

In the representation above, the position of a list element is a natural number. To handle trees, let the position of a tree node be a list of natural numbers, giving the path from the root to that node. For example, the infinite tree could be represented by the set of pairs

\{⟨[0], x_{0}⟩, ⟨[1, 0], x_{1}⟩, …, ⟨[\underbrace{1, …, 1}_{n}, 0], x_{n}⟩, …\}.

The list [1, 1, 0] gives the position of node x_{2} in the tree.

The labelled nodes determine the tree’s structure. A tree that has no labelled nodes is represented by the empty set and is indistinguishable from the empty tree. Each label defines the corresponding position and implicitly implies the existence of all its ancestor nodes. The branch nodes in the tree above are unlabelled, and exist only because of the labelled leaf nodes underneath them.

We can even represent trees with infinite branching:

This is the infinite set of labelled nodes of the form ⟨[k_{0}, k_{1}, …, k_{n−1}], x_{n}⟩ for n ≥ 0 and k_{i} :: nat. I have identified all the labels at level n as x_{n} for simplicity, but the labels could all be distinct.

The definitions discussed below do not exploit the representation in its full generality. Branching is strictly finite — binary, in fact — but the depth may be infinite.

4.3 The formal definition of type α node

A node is essentially a list paired with a label. We could represent lists as described above, but this would immediately be superseded by the resulting representation of trees, a duplication of effort. Luckily, we require only lists of natural numbers. We could encode them by Gödel numbers of the form 2^{k_{0}}3^{k_{1}} ⋯, but they are more simply represented by functions of type nat ⇒ nat.

Let the list [k_{0}, …, k_{n−1}] denote some function f such that

f(i) = \{ \begin{matrix}Suc(k_{i}) & if 0 ≤ i < n; \\ 0 & if i = n. \end{matrix}

Note that f(i) could be anything for i > n. The constant function λi . 0 represents the empty list. To ‘cons’ an element a to the front of the list f, we use Push(a, f), which is defined in terms of nat case (§2.4):

Push(a, f) ≡ (λi . nat case(i, Suc(a), f))

Each node is represented by a pair (f, x), where f :: nat ⇒ nat stands for a list and x :: α + nat is a label. The disjoint sum type allows a label to contain either an element of type α or a natural number; some constructions below require natural numbers in trees.

To prove that equality is a gfp, we shall have to impose a minor restriction on f. The take-lemma, which says that two lazy lists are equal if all their corresponding finite initial segments are equal [5], is a standard reasoning method in lazy functional programming. The take-lemma is valid because a lazy list is nothing more than the set of its finite parts. We may similarly prove that two infinite data structures are equal, if we ensure that a tree cannot contain a node at an infinite depth.

The set of all nodes is therefore defined as follows:

Node ≡ {p . ∃f x n . p = ⟨f, x⟩ ∧ f(n) = 0}  (1)

The second conjunct ensures that the position list is finite: f(n) = 0 for some n. Strangely, no other well-formedness conditions need to be imposed upon nodes or node sets; the fixedpoint operators exclude the undesirable elements.

Since Node has a complex type, namely

                     ((nat ⇒ nat) × (α + nat)) set,

let us define α node to be the type of nodes taking labels from α. As decribed in §2.3, we must declare abstraction and representation functions:

           Abs Node :: ((nat ⇒ nat) × (α + nat)) set ⇒ α node
           Rep Node :: α node ⇒ ((nat ⇒ nat) × (α + nat)) set

4.4 The binary tree constructors

Possibly infinite binary trees represent all data structures in this theory. Binary trees are sets of nodes. The simplest binary tree, Atom(a), consists of a label alone. If M and N are binary trees, then M · N is the tree consisting of the two branches M and N. Thus there are two primitive tree constructors:

              Atom :: α + nat ⇒ α nodeset
                (·) :: [α nodeset, α nodeset] ⇒ α nodeset

Writing [] for λi . 0, we could define these constructors semi-formally as follows:

Atom(a) ≡ {⟨[], a⟩}
M · N ≡ {⟨Push(0, f), x⟩}_{⟨f,x⟩∈M} ∪ {⟨Push(1, f), x⟩}_{⟨f,x⟩∈N}

These have the expected properties for infinite binary trees. The constructors are injective; we can recover a from Atom(a); we can recover M and N from M · N by stripping the initial 0 or 1. We always have Atom(a) ≠ M · N because Atom(a) contains [] as a position while M · N does not. Trees need not be well-founded; for example, there are infinite trees such that M = M · M.

The formal definitions of Atom and (·) have to obey the constraints of our notation. Thus, they are cluttered with calls to Suc, split, etc., along with Abs Node and Rep Node for the type definition. Such details add nothing of substance to the observations above.

apfst(h, p) ≡ split(p, λx y . ⟨h(x), y⟩)

       Push Node(k, nd) ≡ Abs Node(apfst(Push(k), Rep Node(nd)))

Atom(a) ≡ {Abs Node(⟨λi . 0, a⟩)}

                M · N ≡ Push Node(0) “ M ∪ Push Node(Suc(0)) “ N

Now apfst(h, ⟨x, y⟩) = ⟨h(x), y⟩, so Push Node(k) takes the node represented by ⟨f, a⟩ to the one represented by ⟨Push(k, f), a⟩. Finally, the image Push Node(0)“M applies this operation upon every node in M.

4.5 Products and sums for binary trees

One objective of this theory is to justify fixedpoint definitions of the data structures, such as

List(A) ≡ lfp(λZ . {NIL} ⊕ (A ⊗ Z)),

where ⊗ is some form of Cartesian product and ⊕ is some form of disjoint sum. We cannot found these upon the usual HOL ordered pairs and injections. In both ⟨x, y⟩ and Inl(x), the type of the result is more complex than that of the arguments; the lfp call would be ill-typed. Therefore we must find alternative definitions of ⊗ and ⊕.

Since (·) is injective, we may use it as an ordered pairing operation and define the product A ⊗ B by

A ⊗ B ≡ ⋃_{x∈A} . ⋃_{y∈B} . {x · y}

Now A, B and A ⊗ B all have the same type, namely α nodesetset.

Disjoint sums are typically coded in set theory by

A + B ≡ {⟨0, x⟩}_{x∈A} ∪ {⟨1, y⟩}_{y∈B}.

In the present setting, this requires distinct trees to play the roles of 0 and 1. Perhaps we could find two distinct sets of nodes, such as the empty set and the universal set, but this would complicate matters below.^{3} Precisely to avoid such complications, natural numbers are always allowed as labels — recall that Atom has type α + nat ⇒ α nodeset. The derived constructors

                       Leaf :: α ⇒ α nodeset
                       Numb :: nat ⇒ α nodeset

3The equation {} · {} = {} would frustrate the development of well-founded trees.

are defined by

                       Leaf(a) ≡ Atom(Inl(a))
                       Numb(k) ≡ Atom(Inr(k))

We may now define disjoint sums in the traditional manner:

In0(M) ≡ Numb(0) · M
In1(N) ≡ Numb(Suc(0)) · N
A ⊕ B ≡ (In0 “ A) ∪ (In1 “ B)

Both injections have type α nodeset ⇒ α nodeset, while A, B and A ⊕ B all have type α nodesetset. Since the latter type is also closed under ⊗ and contains copies of α and nat, it has enough structure to contain virtually every sort of finitely branching tree. Note that ⊕ and ⊗ are monotonic, by the monotonicity of unions and images.

The eliminators for ⊗ and ⊕ are analogous to those for the product and type types, namely split and case. They are defined in the normal manner, using descriptions, and satisfy the corresponding equations:

Split(M · N, c) = c(M, N)
Case(In0(M), c, d) = c(M)
Case(In1(N), c, d) = d(N)

5 Well-founded data structures

In other work [33], I have investigated the formalization of recursive data structures in Zermelo-Fraenkel (ZF) set theory. Those include mutually recursive data structures as well as simple lists. They also allow recursively defined set constructions to take part in new recursive definitions, as in term(A) = A × list(term(A)).

That work has been mechanized within an Isabelle implementation of ZF set theory, just as the present work has been mechanized within an Isabelle implementation of HOL. My ZF work uses standard ordered pairing (defined by ⟨a, b⟩ ≡ {{a}, {a, b}}) as the basis for all data structures. ZF’s Foundation Axiom implies ⟨x, y⟩ ≠ y, and more generally that all such data structures are well-founded.

The present HOL theory suffers no such limitation, handling both finite and infinite data structures.^{4} The finite data structures are similar to the ZF ones described elsewhere [33], so I shall say little about them here. It is perhaps remarkable that ZF and HOL can be made to look so similar.

4To obtain infinite data structures in ZF, we could adopt Aczel’s Anti-Foundation Axiom [3] or simply formalize M · N in ZF.

5.1 Finite lists

We can now define the operator List to be the least solution to the recursion equation

List(A) = {NIL} ⊕ (A ⊗ List(A)).

The Knaster-Tarski Theorem applies because ⊕ and ⊗ are monotonic. We can even prove that List is a monotonic operator over type α nodesetset, justifying definitions such as Term(A) = A ⊗ List(Term(A)).

The formal definition of List(A) uses lfp to get the least fixedpoint:

List Fun(A) ≡ λZ . {Numb(0)} ⊕ (A ⊗ Z)

                    List(A) ≡ lfp(List Fun(A))
                       NIL ≡ In0(Numb(0))

CONS(M, N) ≡ In1(M · N)

From these we can easily derive the list introduction rules (§3.1), and various injectivity properties:

CONS(M, N) ≠ NIL (CONS(K, M) = CONS(L, N)) = (K = L ∧ M = N)

The case analysis eliminator for lists is defined using those for ⊕ and ⊗ (for recursion, see the next section):

List case(M, c, d) ≡ Case(M, λx . c, λu . Split(u, d))

It satisfies the equations

                       List case(NIL, c, d) = c  (2)

List case(CONS(M, N), c, d) = d(M, N)  (3)

Later (§6) we shall define LList(A), which includes infinite lists, as the greatest fixedpoint of List Fun(A). Our definitions of NIL, CONS and List case will continue to work, even for the infinite lists. If N is an infinite list then CONS(M, N) is also infinite.

Since List(A) contains no infinite lists, we may instantiate the lfp induction rule to obtain structural induction (§3.1). By induction we may prove the properties expected of a well-founded data structure, such as

N ∈ List(A)

CONS(M, N) ≠ N (4)

The Isabelle theory proceeds to define the type α list to contain those values of type α nodeset that belong to the set List(range(Leaf)). If x_{1}, x_{2}, …, x_{n} have type α then the list [x_{1}, x_{2}, …, x_{n}] is represented by

CONS(Leaf(x_{1}), CONS(Leaf(x_{2}), … CONS(Leaf(x_{n}), NIL) …)).

Type α list has two constructors, Nil :: α list and Cons :: [α, α list] ⇒ α list, and the usual induction rule, recursion operator, etc. This type definition (§2.3) is the final stage in making lists convenient to use; the details are routine and omitted.

5.2 A space for well-founded types

Lisp’s symbolic expressions are built up from identifiers and numbers by pairing. Formalizing S-expressions in HOL further demonstrates the Isabelle theory. More importantly, it leads to a uniform treatment of recursive functions for virtually all finitely branching well-founded data structures. An essential feature of S-expressions is that they are finite. Therefore, let us define them using lfp:

          Sexp ≡ lfp(λZ . range(Leaf) ∪ range(Numb) ∪ (Z ⊗ Z))  (5)

Observe how range expresses the sets of all Leaf(a) and Numb(k) constructions. We can develop Sexp in the same manner as List(A), deriving an induction rule, a case analysis operator, etc.

But Sexp is a rather special subset of our universe, itself suitable for defining recursive data structures. It contains all constructions of the form Leaf(a), Numb(k) and M ·N, and therefore also In0(M) and In1(N). Thus it is closed under ⊗ and ⊕. Defined by lfp, all the constructions in it are finite.

Now Sexp is not necessarily large enough to contain List(A) for arbitrary A, since A might contain infinite constructions. But Sexp is closed under List: we can easily prove List(Sexp) ⊆ Sexp, expressing that lists of finite constructions are themselves finite constructions. Similarly, Sexp is closed under all other finite data structures that I have investigated. See my set theory paper [33] for more details.

Recursion on Sexp gives us recursion on all these well-founded data structures. Isabelle’s HOL theory contains a derivation of well-founded recursion. This justifies defining any function whose recursive calls decrease its argument under some wellfounded relation. The immediate subexpression relation on Sexp is the set of pairs

(≺) ≡ ⋃_{M∈Sexp} . ⋃_{N∈Sexp} . {⟨M, M · N⟩, ⟨N, M · N⟩}.

Structural induction on Sexp proves that this relation is well-founded. The transitive closure of a relation can be defined using lfp, and can be proved to preserve wellfoundedness [33]. So M ≺^{+} N expresses that M is a subexpression of N. Wellfounded recursion justifies any function on S-expressions whose recursive calls take subexpressions of the original argument.

Let us apply this to lists. Recall that

CONS(M, N) ≡ In1(M · N) ≡ Numb(Suc(0)) · (M · N).

A sublist is therefore a subexpression. Structural recursion on lists is an instance of well-founded recursion:

List rec(M, c, d) ≡ wfrec(≺^{+}, M, λM g . List case(M, c, λx y . d(x, y, g(y))))

We immediately obtain List rec(NIL, c, d) = c. The fact N ≺^{+} CONS(M, N) justifies the recursion equation

                        M ∈ Sexp N ∈ Sexp

List rec(CONS(M, N), c, d) = d(M, N, List rec(N, c, d)).

Most familiar list functions — append, reverse, map — have obvious definitions by structural recursion. But the theory does not insist upon structural recursion; it can express functions such as quicksort in their natural form, using well-founded recursion in its full generality.

Definition (5) is not the only possible way of characterizing the set of finite constructions. We could instead formalize the finite powerset operator using lfp [33]. The set of all finite, non-empty sets of nodes would be larger than Sexp while satisfying the same key closure properties. Defining a suitable well-founded relation on this set might be tedious.

The Isabelle theory gives a comprehensive treatment of well-founded data structures in higher-order logic. We turn now to the non-well-founded case.

6 Lazy lists and co-induction

Defining the set of lists as a greatest instead of a least fixedpoint admits infinite as well as finite lists. We can then model computation and equality, realizing to some extent the theory of lists in lazy functional languages [5]. However, our “lazy lists” have no inbuilt operational semantics; after all, HOL can express non-computable functions.

The set of lazy lists is defined by

                    LList(A) ≡ gfp(List Fun(A));

recall that List Fun and the list operations NIL, CONS and List case were defined in §5.1. The fixedpoint property yields introduction rules for LList(A):

                NIL ∈ LList(A) \begin{matrix}M ∈ A & N ∈ LList(A) \\ CONS(M, N) ∈ LList(A) \end{matrix}

These may resemble their finite list counterparts (§3.1), but they differ significantly, for CONS is well-behaved even when applied to an infinite list. In particular, the List case equation (3) works for everything of the form CONS(M, N).

Since LList(A) is a greatest fixedpoint, it does not have a structural induction principle. Well-foundedness properties such as the list theorem (4) have no counterparts for LList(A). We can even construct a counterexample and prove that it belongs to LList(A) by co-induction.

The weak co-induction rule for LList(A) performs type checking for infinite lists:

M ∈ X X ⊆ List Fun(A, X)

                            M ∈ LList(A) (6)

The strong co-induction rule, as described in §3.2, implicitly includes LList(A):

M ∈ X X ⊆ List Fun(A, X) ∪ LList(A)

                            M ∈ LList(A) (7)

6.1 An infinite list

Our example of non-well-foundedness is the infinite list of M’s:

                  Lconst(M) = CONS(M, Lconst(M))  (8)

We cannot, of course, define infinite lists directly:

Lconst(M) ≡ CONS(M, CONS(M, …)) ??

Co-recursion, a general method for defining infinite lists, is discussed below. For now, let us construct Lconst(M) explicitly as a fixedpoint:

Lconst(M) ≡ lfp(λZ . CONS(M, Z))

The Knaster-Tarski Theorem applies because lists are sets of nodes and CONS is monotonic in both arguments. (Recall from §4.4 that (·) is defined in terms of the monotonic operations union and image.) I have used lfp but gfp would work just as well — we need only the fixedpoint property (8).

Just as we cannot define Lconst(M) directly, we cannot prove that it is a lazy list by the introduction rules alone. The co-induction rule (6) proves Lconst(M) ∈ LList({M}) if we can find a set X containing Lconst(M) and included in List Fun({M}, X). A suitable X is {Lconst(M)}. Obviously Lconst(M) ∈ {Lconst(M)}. We must also show

              {Lconst(M)} ⊆ List Fun({M}, {Lconst(M)}).

The fixedpoint property (8) transforms this to

          {CONS(M, Lconst(M))} ⊆ List Fun({M}, {Lconst(M)}),

which is obvious by the definitions of CONS and List Fun.

We can simplify such proofs by deriving introduction rules for List Fun:

                         NIL ∈ List Fun(A, X)  (9)

M ∈ A N ∈ X

                     CONS(M, N) ∈ List Fun(A, X)

(10)

6.2 Equality of lazy lists; the take-lemma

Because HOL lazy lists are sets of nodes, the equality relatrion on LList(A) is an instance of ordinary set equality. By investigating this relation further, we may obtain convenient methods for proving that two lazy lists are equal.

Let take(k, l) return l’s first k elements as a finite list. Bird and Wadler [5] use the take-lemma to prove equality of lazy lists l_{1} and l_{2}:

∀k . take(k, l_{1}) = take(k, l_{2})
l_{1} = l_{2}

It embodies a continuity principle shared by our HOL formalization.

The definition (1) of nodes (in §4.3) requires each node to have a finite depth. A node contains a pair ⟨f, x⟩, where x is the label and f codes the position. Our definition ensures f(k) = 0 for some k, which is the depth of the node. We can formalize the depth directly, using the least number principle:

LEAST k . ϕ(k) ≡ ϵk . ϕ(k) ∧ (∀j . j < k → ¬ϕ(j))
ndepth(nd) ≡ split(Rep Node(nd), λf x . LEAST k . f(k) = 0)

Our generalization of take, called ntrunc, applies to all data structures, not just lists. It returns the set of all nodes having less than a given depth:

ntrunc(k, N) ≡ {nd . nd ∈ N ∧ ndepth(nd) < k}

Elementary reasoning derives results describing ntrunc’s effect upon various constructions:

ntrunc(0, M) = {}

          ntrunc(Suc(k), Leaf(a)) = Leaf(a)
          ntrunc(Suc(k), Numb(a)) = Numb(a)
           ntrunc(Suc(k), M · N) = ntrunc(k, M) · ntrunc(k, N)

Since In0(M) ≡ Numb(0) · M we obtain

              ntrunc(Suc(0), In0(M)) = {}
         ntrunc(Suc(Suc(k)), In0(M)) = In0(ntrunc(Suc(k), M))

and similarly for In1.

Our generalization of take enjoys a generalization of the take-lemma:

∀k . ntrunc(k, M) = ntrunc(k, N)

M = N (11)

This obvious fact is a key result. It gives us a method for proving the equality of any constructions M and N. We could apply this “ntrunc-lemma” directly, but instead we shall package it into a form suitable for co-induction.

6.3 Diagonal set operators

In order to prove list equations by co-induction, we must demonstrate that the equality relation is the greatest fixedpoint of some monotone operator. To this end, we define diagonal set operators for ⊗ and ⊕. A diagonal set has the form {⟨x, x⟩}_{x∈A}, internalizing the equality relation on A.

A binary relation on sets of nodes has type (α nodeset × α nodeset) set. The operators ⊗_{D} and ⊕_{D} combine two such relations to yield a third. The operator diag, of type α set ⇒ (α × α) set, constructs arbitrary diagonal sets.

diag(A) ≡ ⋃_{x∈A} . {⟨x, x⟩}
r ⊗_{D} s ≡ ⋃_{p∈r} . ⋃_{q∈s} . split(p, λx x′ . split(q, λy y′ . {⟨x · y, x′ · y′⟩}))
r ⊕_{D} s ≡ (⋃_{p∈r} . split(p, λx x′ . {⟨In0(x), In0(x′)⟩})) ∪
(⋃_{q∈s} . split(q, λy y′ . {⟨In1(y), In1(y′)⟩}))

The need for split obscures the definitions of ⊗_{D} and ⊕_{D}, but we can derive introduction rules that clearly express the content of these relations. For ⊗_{D} we have

\begin{matrix}⟨M, M′⟩ ∈ r & ⟨N, N′⟩ ∈ s \\ ⟨M · N, M′ · N′⟩ ∈ r ⊗_{D} s \end{matrix}

while for ⊕_{D} we have the pair of rules

{⟨M, M′⟩ ∈ r \atop ⟨In0(M), In0(M′)⟩ ∈ r ⊕_{D} s} {⟨N, N′⟩ ∈ s \atop ⟨In1(N), In1(N′)⟩ ∈ r ⊕_{D} s}

The idea is that ⊗_{D} and ⊕_{D} build relations in the same manner as ⊗ and ⊕ build sets. Since fst “ r is the first projection of the relation r, we can summarize the idea by three obvious equations:

                  fst “ diag(A) = A

fst “ (r ⊗_{D} s) = (fst “ r) ⊗ (fst “ s)
fst “ (r ⊕_{D} s) = (fst “ r) ⊕ (fst “ s)

Category theorists may note that ⊗ and ⊕ are functors on a category of sets where the morphisms are binary relations; in this category, ⊗_{D} and ⊕_{D} give the functors’ effects on the morphisms. Next, we shall do the same thing to the functor LList.

6.4 Equality of lazy lists as a gfp

Just as ⊗_{D} and ⊕_{D} extend ⊗ and ⊕ to act upon relations, let LListD extend LList. Thanks to our new operators, the definition is simple and resembles that of LList:

LListD Fun(r) ≡ λZ . diag({Numb(0)}) ⊕_{D} (r ⊗_{D} Z)

               LListD(r) ≡ gfp(LListD Fun(r))

The theorem that list equality is a gfp can now be stated as a succinct equation between relations:

                  LListD(diag(A)) = diag(LList(A))  (12)

Here diag(LList(A)) is the equality relation on LList(A), while LListD(diag(A)) is the gfp of LListD Fun(diag(A)). The Isabelle proof of Equation (12) is fairly complex; let us discuss it briefly.

The key fact to prove is a sort of contrapositive to the ntrunc-lemma:

∀M N . ⟨M, N⟩ ∈ LListD(diag(A)) → ntrunc(k, M) = ntrunc(k, N)  (13)

Proof By complete induction on k, we may assume Equation (13) after replacing k by any smaller natural number j. By the fixedpoint property

       LListD(diag(A)) = diag({Numb(0)}) ⊕_{D} (r ⊗_{D} LListD(diag(A))),

if ⟨M, N⟩ ∈ LListD(diag(A)) then there are two cases. If M = N = In0(Numb(0)) = NIL then ntrunc(k, M) = ntrunc(k, N) is trivial. Otherwise M = CONS(x, M′) and N = CONS(x, N′), where ⟨M′, N′⟩ ∈ LListD(diag(A)). Recall the definition CONS(x, y) ≡ In1(x · y) and the properties of ntrunc (§6.2); we obtain

ntrunc(k, CONS(x, y)) = \{ \begin{matrix}\{\} & if k < 2, and \\ CONS(ntrunc(j, x), ntrunc(j, y)) & if k = Suc(Suc(j)). \end{matrix}

Now if k = Suc(Suc(j)) then ntrunc(k, M) = ntrunc(k, N) reduces to an instance of the induction hypothesis, ntrunc(j, M′) = ntrunc(j, N′).

Combining Equation (13) with the ntrunc-lemma (11) yields half of our desired result:

                  LListD(diag(A)) ⊆ diag(LList(A))

This is the more important half, since it lets us show M = N by showing ⟨M, N⟩ ∈ LListD(diag(A)), which can be done using co-induction. The opposite inclusion,

                  diag(LList(A)) ⊆ LListD(diag(A)),

follows by showing that diag(LList(A)) is a fixedpoint of LListD Fun(diag(A)), since LListD(diag(A)) is the greatest fixedpoint. This argument is an example of co-induction.

6.5 Proving lazy list equality by co-induction

The weak co-induction rule for list equality yields M = N provided ⟨M, N⟩ ∈ r where r is a suitable bisimulation between lazy lists:

⟨M, N⟩ ∈ r r ⊆ LListD Fun(diag(A), r)

M = N (14)

Co-induction has many variant forms (§3.2). Strong co-induction includes the equality relation implicitly in every bisimulation:

        ⟨M, N⟩ ∈ r r ⊆ LListD Fun(diag(A), r) ∪ diag(LList(A))

M = N (15)

Expanding the definitions of NIL, CONS and LListD Fun creates unwieldy formulae. The Isabelle theory derives two rules to avoid this, resembling the List Fun rules (9) and (10):

                   ⟨NIL, NIL⟩ ∈ LListD Fun(diag(A), r)  (16)

x ∈ A ⟨M, N⟩ ∈ r

             ⟨CONS(x, M), CONS(x, N)⟩ ∈ LListD Fun(diag(A), r)

(17)

7 Lazy lists and co-recursion

We have defined the infinite list Lconst(M) = [M, M, …] as a fixedpoint. The construction obviously generalizes to other repetitive lists such as [M, N, M, N, …]. But how can we define infinite lists such as [1, 2, 3, …]? And how can we define the usual list operations, like append and map? Structural recursive definitions (in terms of List rec) would work for elements of List(A) but not for the infinite lists in LList(A).

Co-recursion is a dual form of structural recursion. Recursion defines functions that consume lists, while co-recursion defines functions that create lists. Corecursion originated in the category theoretic notion of final co-algebra; Mendler [23] and Geuvers [13], among others, have investigated it in type theories.

In this paper I shall not attempt to treat co-recursion categorically, or describe the general case in all its complexity. Instead I shall simply treat a key example: lazy lists. Because co-recursion is still widely unfamiliar, I shall begin with motivation and examples, leaving its HOL deriviation for last.

7.1 Introduction to co-recursion

Co-recursion defines a lazy list in terms of some seed value a :: α and a function f :: α ⇒ unit + (β nodeset × α). Recall from §2.4 that unit is the nullary product type, whose sole value is ⟨⟩, while × and + are the product and sum type operators. Thus LList corec has type

              [α, α ⇒ unit + (β nodeset × α)] ⇒ β nodeset.

It must satisfy

LList corec(a, f) = \{ \begin{matrix}NIL & if f(a) = Inl(⟨⟩); \\ CONS(x, LList corec(b, f)) & if f(a) = Inr(⟨x, b⟩). \end{matrix}

The idea should be clear: f takes the seed a and either returns Inl(⟨⟩), to end the list here, or returns Inr(⟨x, b⟩), to continue the list with next element x and seed b. By keeping the seed forever M and always returning it as the next element, co-recursion can express Lconst(M):

            Lconst(M) ≡ LList corec(M, λM . Inr(⟨M, M⟩))

Consider the functional Lmap, which applies a function to every element of a list:

Lmap(g, [x_{0}, x_{1}, …, x_{n}, …]) = [g(x_{0}), g(x_{1}), …, g(x_{n}), …]

The usual recursion equations are

                    Lmap(g, NIL) = NIL  (18)

Lmap(g, CONS(M, N)) = CONS(g(M), Lmap(g, N)) .  (19)

Co-recursion handles these easily. To compute Lmap(g, M), take M as the seed. If M = NIL then end the result list; if M = CONS(x, M′) then continue the result list with next element g(x) and seed M′. The formal definition uses List case to inspect M:

Lmap(g, M) ≡

LList corec(M, λM . List case(M, \begin{matrix}Inl(⟨⟩), \\ λx M′ . Inr(⟨g(x), M′⟩))) \end{matrix}

This definition of map has little in common with the standard recursive one. Append comes out stranger still, and other standard functions seem to be lost altogether.

7.2 Harder cases for co-recursion

With co-recursion, the case analysis is drivien by the output list, rather than the input list. The append function highlights this peculiarity. The usual recursion equations for append perform case analysis on the first argument:

                  Lappend(NIL, N) = N

Lappend(CONS(M_{1}, M_{2}), N) = CONS(M_{1}, Lappend(M_{2}, N))

But a NIL input does not guarantee a NIL output, as it did for Lmap; consider

                 Lappend(NIL, CONS(M, N)) = CONS(M, N).

The correct equations for co-recursion involve both arguments:

                 Lappend(NIL, NIL) = NIL  (20)
         Lappend(NIL, CONS(N_{1}, N_{2})) = CONS(N_{1}, Lappend(NIL, N_{2}))  (21)

Lappend(CONS(M_{1}, M_{2}), N) = CONS(M_{1}, Lappend(M_{2}, N))  (22)

The second line above forces Lappend(NIL, N) to continue executing until it has made a copy of N. This looks inefficient. In the context of the polymorphic λcalculus, Geuvers [13] discusses stronger forms of co-recursion that allow the seed to return an entire list at once. But my HOL theory has no operational significance; efficiency is meaningless; we may as well keep co-recursion simple.

The seed for Lappend(M, N) is the pair ⟨M, N⟩. The co-recursive definition performs case analysis on both lists:

• If M = NIL then it looks at N:

– If N = NIL then end the result list.

– If N = CONS(N_{1}, N_{2}) then continue the result list with next element N_{1} and seed ⟨NIL, N_{2}⟩.

• If M = CONS(M_{1}, M_{2}) then continue the result list with next element M_{1} and seed ⟨M_{2}, N⟩.

We can formalize this using LList corec, List case and split:

   Lappend(M, N) ≡
      LList corec(⟨M, N⟩, λp . split(p,

λM N . List case(M, List case(N, Inl(⟨⟩), λN_{1} N_{2} . Inr(⟨N_{1}, ⟨NIL, N_{2}⟩⟩)), λM_{1} M_{2} . Inr(⟨M_{1}, ⟨M_{2}, N⟩⟩))))

Now let us try to define a function to flatten a list of lists according to the following recursion equations:

                     Lflat(NIL) = NIL  (23)
              Lflat(CONS(M, N)) = Lappend(M, Lflat(N))  (24)

Since co-recursion is driven by the output, we need to know when a CONS is produced. We can refine Equation (24) by further case analysis:

              Lflat(CONS(NIL, N)) = Lflat(N)

Lflat(CONS(CONS(M_{1}, M_{2}), N)) = CONS(M_{1}, Lflat(CONS(M_{2}, N)))

Unfortunately, the outcome of CONS(NIL, N) is still undecided; it could be NIL or CONS. Given the argument Lconst(NIL) — an infinite list of NILs — Lflat should run forever. There is no effective way to check whether an infinite list contains a non-NIL element.

I do not know of any natural formalizaton of Lflat. Since HOL can formalize non-computable functions, we can force Lflat(Lconst(NIL)) = NIL using a description. Such a definition would be of little relevance to computer science. Really Lflat(Lconst(NIL)) should be undefined, but HOL does not admit partial functions.

The filter functional, which removes from a list all elements that fail to satisfy a given predicate, poses similar problems. If no list elements satisfy the predicate, then the result is logically NIL, but there is no effective way to reach this result. Leclerc and Paulin-Mohring [21] discuss approaches to this problem in the context of the Coq system.

7.3 Deriving co-recursion

The characteristic equation for co-recursion can be stated using case and split:

      LList corec(a, f) =  (25)

case(f(a), λu . NIL, λv . split(v, λx b . CONS(x, LList corec(b, f))))

To realize this equation, recall that an element of LList(A) is a set of nodes, each of finite depth. A primitive recursive function can approximate the co-recursion operator for nodes up to some given depth k:

lcorf(0, a, f) = {}
lcorf(Suc(k), a, f) = case(f(a), λu . NIL, λv . split(v, λx b . CONS(x, lcorf(k, b, f))))

Now we can easily define co-recursion:

LList corec(a, f) ≡ ⋃k . lcorf(k, a, f)

Equation (25) can then be proved as two separate inclusions, with simple reasoning about unions and (in one direction) induction on k.

The careful reader may have noticed that lcorf(k, a, f) is not strictly primitive recursive, because the parameter a varies in the recursive calls. To be completely formal, we must define a function over a using higher-order primitive recursion. In the Isabelle theory, lcorf(k, a, f) becomes LList corec fun(k, f, a), whose primitive recursion definition employs nat rec (§2.4):

    LList corec fun(k, f) =

nat rec(k, λa . {}, λj r a . case(f(a), λu . NIL, λv . split(v, λx b . CONS(x, r(b)))))

Obscure as this may look, it trivially implies the equations for lcorf given above.

8 Examples of co-induction and co-recursion

This section demonstrates defining functions by co-recursion and verifying their equational and typing properties by co-induction.

8.1 A type-checking rule for LList corec

One advantage of LList corec over ad-hoc definitions is that the result is certain to be a lazy list. To express this well-typing property in the simplest possible form, let U :: α nodesetset abbreviate the universal set of constructions: U ≡ {x . True}. We can now state the typing theorem as

                     LList corec(a, f) ∈ LList(U).

Proof Apply the weak co-induction rule (6) to the set

                   V ≡ range(λx . LList corec(x, f)).

We must show V ⊆ List Fun(U, V), which reduces to

                   LList corec(a, f) ∈ List Fun(U, V).

There are two cases. We simplify each case using Equation (25):

• If f(a) = Inl(⟨⟩), it reduces to NIL ∈ List Fun(U, V), which holds by Rule (9).

• If f(a) = Inr(⟨x, b⟩), it reduces to

                 CONS(x, LList corec(b, f)) ∈ List Fun(U, V).

This holds by Rule (10) because x ∈ U and LList corec(b, f) ∈ V.

This result, referring to the universal set, may seem weak compared with our previous well-typing result, Lconst(M) ∈ LList({M}), from §6.1. It is difficult to bound the set of possible values for x for the case f(a) = Inr(⟨x, b⟩). Sharper results can be obtained by performing separate co-induction proofs for each function defined by co-recursion.

8.2 The uniqueness of co-recursive functions

Equation (25) characterizes LList corec uniquely; the proof is a typical example of proving an equation by co-induction. Let us define an abbreviation for the corecursion property:

is corec(f, h) ≡ ∀x . h(x) = case(f(a), λu . NIL, λv . split(v, λx b . CONS(x, h(b))))

Existence, namely is corec(f, λx . LList corec(x, f)), is immediate by Equation (25). Let us now prove uniqueness:

                    is corec(f, h_{1}) is corec(f, h_{2})

h_{1} = h_{2}

Proof By extensionality it suffices to prove h_{1}(x) = h_{2}(x) for all x. Now consider the bisimulation {⟨h_{1}(u), h_{2}(u)⟩}_{u}, formalized in HOL by

r ≡ range(λu . ⟨h_{1}(u), h_{2}(u)⟩).

Apply the co-induction rule (14), with r as above and putting A ≡ U, the universal set. We must show r ⊆ LListD Fun(diag(U), r), which reduces to

⟨h_{1}(u), h_{2}(u)⟩ ∈ LListD Fun(diag(U), r).

There are two cases. In each, we apply the co-recursion properties of h_{1} and h_{2}:

• If f(a) = Inl(⟨⟩), it reduces to ⟨NIL, NIL⟩ ∈ LListD Fun(diag(U), r), which holds by Rule (16).

• If f(a) = Inr(⟨x, b⟩), it reduces to

⟨CONS(x, h_{1}(b)), CONS(x, h_{2}(b))⟩ ∈ LListD Fun(diag(U), r).

This holds by Rule (17) because x ∈ U and ⟨h_{1}(b), h_{2}(b)⟩ ∈ r.

Note the close structural similarity between this co-induction proof and the previous one, even though the former proves set membership while the latter proves an equation. The role of r in this equality proof is reminsicent of process equivalence proofs in Calculus of Communicating Systems (CCS) [24], where the bisimulation associates corresponding states of two processes. The equality can also be proved using the ntrunc-lemma (11) directly, by complete induction on k; the proof is considerably more complex.

8.3 A proof about the map functional

To demonstrate that the theory has some relevance to lazy functional programming, this section proves a simple result: that map distributes over composition.

                            M ∈ LList(A)

Lmap(f ∘ g, M) = Lmap(f, Lmap(g, M))

Proof The bisimulation {⟨Lmap(f ∘ g, u), Lmap(f, Lmap(g, u))⟩}_{u∈LList(A)}, may be formalized using the image operator:

r ≡ (λu . ⟨Lmap(f ∘ g, u), Lmap(f, Lmap(g, u))⟩) “ LList(A)

As in the previous co-induction proof, apply Rule (14). The key is to show

⟨Lmap(f ∘ g, u), Lmap(f, Lmap(g, u))⟩ ∈ LListD Fun(diag(U), r)

for arbitrary u ∈ LList(A). There are again two cases, this time depending on the form of u. We simplify each case using the recursion equations for Lmap, which follow from its co-recursive definition (§7.1).

• If u = NIL, the goal reduces to ⟨NIL, NIL⟩ ∈ LListD Fun(diag(U), r), which holds by Rule (16).

• If u = CONS(M′, N), it reduces to

⟨\begin{matrix}CONS(f(g(M′)), Lmap(f ∘ g, N)), \\ CONS(f(g(M′)), Lmap(f, Lmap(g, N)))⟩ ∈ LListD Fun(diag(U), r). \end{matrix}

This holds by Rule (17) because f(g(M′)) ∈ U and

⟨Lmap(f ∘ g, N), Lmap(f, Lmap(g, N))⟩ ∈ r.

The co-inductive argument bears little resemblance to the usual proof in the Logic for Computable Functions (LCF) [27, page 283]. On the other hand, all these coinductive proofs have a monotonous regularity. A similar argument proves

                            M ∈ LList(A)

Lmap(λx . x, M) = M.

8.4 Proofs about the list of iterates

Consider the function Iterates defined by

Iterates(f, M) ≡ LList corec(M, λM . Inr(⟨M, f(M)⟩)).

A generalization of Lconst, it constructs the infinite list [M, f(M), …, f^{n}(M), …] by the recursion equation

              Iterates(f, M) = CONS(M, Iterates(f, f(M))).

The equation

Lmap(f, Iterates(f, M)) = Iterates(f, f(M))  (26)

has an entirely straightforward co-inductive proof, using the bisimulation

{⟨Lmap(f, Iterates(f, u)), Iterates(f, f(u))⟩}_{u∈LList(A)}.

Combining the previous two equations immediately yields

            Iterates(f, M) = CONS(M, Lmap(f, Iterates(f, M))).

Harder is to show that this equation uniquely characterizes Iterates(f):

∀x . h(x) = CONS(x, Lmap(f, h(x)))

                           h = Iterates(f)

The bisimulation for this proof is unusually complex. Let f^{n} stand for the function that applies f to its argument n times. Since Lmap is a curried function — a point easily missed with Isabelle’s peculiar syntax! — the function Lmap(f)^{n} applies Lmap(f) to a given list n times. The bisimulation has two index variables:

r ≡ {⟨Lmap(f)^{n}(h(u)), Lmap(f)^{n}(Iterates(f, u))⟩}_{u∈LList(A), n≥0}

Proof First note two facts, both easily justified by induction on n:

Lmap(f)^{n}(CONS(b, M)) = CONS(f^{n}(b), Lmap(f)^{n}(M))  (27)
f^{n}(f(x)) = f^{Suc(n)}(x)  (28)

By extensionality it suffices to prove h(x) = Iterates(f, x) for all x. Again we apply the weak co-induction rule (14), with the bisimulation r shown above. After simplification, we must show

⟨Lmap(f)^{n}(h(u)), Lmap(f)^{n}(Iterates(f, u))⟩ ∈ LListD Fun(diag(U), r)

for arbitrary n ≥ 0 and u ∈ LList(A). By the recursion equations for h and Iterates, the pair expands to

⟨Lmap(f)^{n}(CONS(u, Lmap(f, h(u)))), Lmap(f)^{n}(CONS(u, Iterates(f, f(u))))⟩

and now two applications of Equation (27) yield

⟨CONS(f^{n}(u), Lmap(f)^{n}(Lmap(f, h(u)))), CONS(f^{n}(u), Lmap(f)^{n}(Iterates(f, f(u))))⟩

Applying Rule (17) to show membership in LListD Fun(diag(U), r), we are left with the subgoal

⟨Lmap(f)^{n}(Lmap(f, h(u))), Lmap(f)^{n}(Iterates(f, f(u)))⟩ ∈ r.

By Equations (26) and (28) we obtain

⟨Lmap(f)^{Suc(n)}(h(u)), Lmap(f)^{Suc(n)}(Iterates(f, u))⟩ ∈ r,

which is obviously true, by the definition of r.

Andy Pitts [34] describes a similar co-induction proof in domain theory. The function Iterates does not lend itself to reasoning by structural induction, but is amenable to Scott’s fixedpoint induction; I proved Equation (26) in the Logic for Computable Functions (LCF) [27, page 286].

8.5 Reasoning about the append function

Many accounts of structural induction start by proofs about append. But append is not an easy example for co-induction. Remember that the co-recursive definition does not give us the usual pair of equations, but rather the three equations (20)– (22). Proofs by the weak co-induction rule (14) typically require the same three-way case analysis. Consider proving that map distributes over append:

                     M ∈ LList(A) N ∈ LList(A)

         Lmap(f, Lappend(M, N)) = Lappend(Lmap(f, M), Lmap(f, N))

Proof Applying the weak co-induction rule with the bisimulation

{⟨Lmap(f, Lappend(u, v)), Lappend(Lmap(f, u), Lmap(f, v))⟩}_{u∈LList(A),v∈LList(A)},

we must show

         ⟨\begin{matrix}Lmap(f, Lappend(u, v)), \\ Lappend(Lmap(f, u), Lmap(f, v))⟩ ∈ LListD Fun(diag(U), r). \end{matrix}

Considering the form of u and v, there are three cases:

• If u = v = NIL, the pair reduces by Equations (18) and (20) to ⟨NIL, NIL⟩, and Rule (16) solves the goal.

• If u = NIL and v = CONS(N_{1}, N_{2}), the pair reduces by Equations (18), (19)

and (21) to

⟨\begin{matrix}CONS(f(N_{1}), Lmap(f, Lappend(NIL, N_{2}))), \\ CONS(f(N_{1}), Lappend(NIL, Lmap(f, N_{2})))⟩. \end{matrix}

Using Equation (18) to replace the second NIL by Lmap(f, NIL) restored the form of the bisimulation, so that Rule (17) can conclude this case.

• If u = CONS(M_{1}, M_{2}), the pair reduces by Equations (19) and (22) to

⟨\begin{matrix}CONS(f(M_{1}), Lmap(f, Lappend(M_{2}, v))), \\ CONS(f(M_{1}), Lappend(Lmap(f, M_{2}), Lmap(f, v)))⟩. \end{matrix}

Now Rule (17) solves the goal. Two easy theorems state that NIL is the identity element for Lappend:

                 M ∈ LList(A)
             Lappend(NIL, M) = M

                                       M ∈ LList(A)

                                    Lappend(M, NIL) = M

Both proofs have only two cases because M is the only variable.

The strong co-induction rule (15) can also prove the distributive law above in only two cases. Recall from §6.5 that the latter rule implicitly includes the equality relation in the bisimulation; if we can reduce the pair to the form ⟨a, a⟩, then we are done. The simpler proof applies the strong co-induction rule (15), using the same bisimulation as before. Now we must show

 ⟨\begin{matrix}Lmap(f, Lappend(u, v)), \\ Lappend(Lmap(f, u), Lmap(f, v))⟩ ∈ LListD Fun(diag(U), r) ∪ diag(LList(U)). \end{matrix}

There are two cases, considering the form of u. If u = CONS(M_{1}, M_{2}) then reason exactly as in the previous proof. If u = NIL, the goal reduces to

     ⟨Lmap(f, v), Lmap(f, v)⟩ ∈ LListD Fun(diag(U), r) ∪ diag(LList(U)).

The pair belongs to diag(LList(U)) because Lmap(f, v) ∈ LList(U).

Most of our co-induction examples prove equations. But co-induction can also prove typing rules:

                     M ∈ LList(A) N ∈ LList(A)

                      Lappend(M, N) ∈ LList(A)

Again, strong co-induction works better for Lappend than weak co-induction. The weak rule (6), requires case analysis on both arguments of Lappend; three cases must be considered. The strong rule (7) requires only case analysis on the first argument. The two proofs are closely analogous to those of the distributive law.

A classic example of structural induction is the associativity of append:

       Lappend(Lappend(M_{1}, M_{2}), M_{3}) = Lappend(M_{1}, Lappend(M_{2}, M_{3}))

With weak co-induction, the proof is no longer trivial; it involves a bisimulation in three variables and the proof consists of four cases: NIL-NIL-NIL, NIL-NIL-CONS, NIL-CONS, and CONS. Strong co-induction with the bisimulation

   {⟨Lappend(Lappend(u, M_{2}), M_{3}), Lappend(u, Lappend(M_{2}, M_{3}))⟩}_{u∈LList(A)}

accomplishes the proof easily. There are only two cases. If u = CONS(M, M′) then the pair reduces to

                ⟨\begin{matrix}CONS(M, Lappend(Lappend(M′, M_{2}), M_{3})), \\ CONS(M, Lappend(M′, Lappend(M_{2}, M_{3})))⟩ \end{matrix}

and Rule (17) applies as usual. If u = NIL then both components collapse to Lappend(M_{2}, M_{3}), and the pair belongs to the diagonal set.

8.6 A comparison with LCF

Scott’s Logic for Computable Functions (LCF) is ideal for reasoning about lazy data structures.^{5} Types denote domains and function symbols denote continuous functions. Strict and lazy recursive data types can be defined. Domains contain the bottom element ⊥, which is the denotation of a divergent computation. Objects can be partial, with components that equal ⊥. A function f can be partial, with f(x) = ⊥ for some x. A lazy list can be partial, with its head, tail or some elements equal to ⊥. The relation x ⊑ y, meaning “x is less defined or equal to y,” compares partial objects.

LCF’s fixedpoint operator expresses recursive objects, including partial functions and recursive lists. The fixedpoint induction rule reasons about the unwinding of recursive objects. It subsumes the familiar structural induction rules and even generalizes them to reason about infinite objects, when the induction formula is chain-complete. Since all formulae of the form x ⊑ y and x = y are chain-complete, LCF can prove equations about lazy lists.

Can our HOL treatment of lazy lists compare with LCF’s? The Isabelle theory defines the new type α llist to contain the elements of LList(range(Leaf)), replacing the clumsy set reasoning by automatic type checking. We can still define lists by co-recursion and prove equations by co-induction.

The resulting theory of lazy lists is superficially similar to LCF’s. But it lacks general recursion and cannot handle divergent computations. Leclerc and Paulin-Mohring’s construction of the prime numbers in Coq [21] reflects these problems. Corecursion cannot express the filter functional, needed for the Sieve of Eratosthenes.

A direct comparison between fixedpoint induction and co-induction is difficult. The rules differ greatly in form and their area of overlap is small. Fixedpoint induction can reason about recursive programs at an abstract level, for instance to prove equivalence of partial functions. Co-induction can prove the equivalence of infinite processes.

I prefer LCF for problems that can be stated entirely in domain theory. But LCF is a restrictive framework: all types must denote domains; all functions must be continuous. HOL is a general logic, free of such restrictions, and yet capable of handling a substantial part of the theory of lazy lists.

9 Conclusions

The present theory gives a comprehensive account of finite recursive data structures, generalizing Melham’s theory [22]. Melham’s approach is concrete: one particular tree structure represents all recursive types. My least fixedpoint approach is more abstract, which facilitates extensions such as mutual recursion [33] and infinite branching trees. Users may also add new monotone operators to the type definition language. And types need not be free (such that each constructor function is injective); for example, we may define the set Fin(A) of all finite subsets of A as a least fixedpoint:

5Scott’s paper is unpublished. My book [27] describes an implementation derived from the original Edinburgh LCF [18]. Isabelle implements LCF as an extension of first-order logic.

Fin(A) ≡ lfp (λZ . {{}} ∪ (⋃_{y∈Z}⋃_{x∈A}{{x} ∪ y}))

The theory also justifies non-well-founded data structures. I prefer it to Aczel’s non-well-founded sets [3]. Set theory’s Foundation Axiom codifies a basic principle, that the universe of sets is constructed in stages. Aczel’s Anti-Foundation Axiom (AFA) proposes a wholly different conception of the universe. One can argue its case on philosophical grounds, but never on grounds of convenience. A convenience argument is likely to fail in any case: Isabelle already implements the HOL theory, while the AFA looks difficult to mechanize.

The theory requires much work, however. Its treatment of lazy lists is clumsy compared with LCF’s, requiring stronger principles of co-induction and co-recursion. Its connection with similar work in stronger type theories [13, 21] deserves investigation. Leclerc and Paulin-Mohring [21] remark that Coq can express finite and infinite data structures in a manner strongly reminiscent of the Knaster-Tarski Theorem. They proceed to consider a representation of streams that specifies the possible values of the stream member at position i, where i is a natural number. Generalizing this approach to other infinite data structures requires generalizing the notion of position: perhaps as in §4.2.

Although my theory of recursion is mechanized, users who wish to define recursive data structures face a tedious job. Isabelle still provides no commands to automate this as in the HOL system [22] or Coq [10]. Jacob Frost [12] has performed Milner and Tofte’s co-induction example [25] using Isabelle’s HOL. He specified some of the data structures axiomatically; a convenient implementation of the theory above could construct them from first principles.

Acknowledgements. Jacob Frost and Sara Kalvala commented on a draft of this paper. Martin Coen helped to set up the environment for co-induction proofs. Andrew Pitts gave much advice, for example on proving that equality is a gfp. Tobias Nipkow made substantial contributions to Isabelle; he originated Isabelle’s implementation of HOL and developed its theory of well-founded recursion.

References

[1] Samson Abramsky. The lazy lambda calculus. In David A. Turner, editor, Resesarch Topics in Functional Programming, pages 65–116. Addison-Wesley, 1977.

[2] Peter Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739–782. North-Holland, 1977.

[3] Peter Aczel. Non-Well-Founded Sets. CSLI, 1988.

[4] Peter B. Andrews, Dale A. Miller, Eve L. Cohen, and Frank Pfenning. Automating higher-order logic. In W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving: After 25 Years, pages 169–192. American Mathematical Society, 1984.

[5] Richard Bird and Philip Wadler. Introduction to Functional Programming. Prentice-Hall, 1988.

[6] Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

[7] L. J. M. Claesen and M. J. C. Gordon, editors. Higher Order Logic Theorem Proving and Its Applications. North-Holland, 1993.

[8] Thierry Coquand and Christine Paulin. Inductively defined types. In COLOG-88: International Conference on Computer Logic, pages 50–66. Springer, 1990. LNCS 417.

[9] B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.

[10] Gilles Dowek et al. The Coq proof assistant user’s guide. Technical Report 134, INRIA-Rocquencourt, 1991.

[11] William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. IMPS: An interactive mathematical proof system. Journal of Automated Reasoning, 11(2), 1993.

[12] Jacob Frost. A case study of co-induction in Isabelle HOL. Technical report, University of Cambridge Computer Laboratory, 1993. In preparation.

[13] Herman Geuvers. Inductive and coinductive types with iteration and recursion. In Bengt Nordström, Kent Petersson, and Gordon Plotkin, editors, Types for Proofs and Programs, pages 193–217, Båstad, June 1992.

[14] Jean-Yves Girard. Proofs and Types. Cambridge University Press, 1989. Translated by Yves LaFont and Paul Taylor.

[15] Andrew Donald Gordon. Functional Programming and Input/Output. PhD thesis, University of Cambridge, 1993. Computer Laboratory Technical Report 285.

[16] M. J. C. Gordon and T. F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.

[17] Michael J. C. Gordon. HOL: A proof generating system for higher-order logic. In Graham Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73–128. Kluwer Academic Publishers, 1988.

[18] Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation. Springer LNCS 78, 1979.

[19] Douglas J. Howe. Equality in lazy computation systems. In 4th Annual Symposium on Logic in Computer Science, pages 198–203. ieee Computer Society Press, 1989.

[20] J. A. Ketonen. EKL—a mathematically oriented proof checker. In R. E. Shostak, editor, 7th International Conference on Automated Deduction, pages 65–79. Springer LNCS 170, 1984.

[21] F. Leclerc and Ch. Paulin-Mohring. Programming with streams in Coq. a case study: the sieve of Eratosthenes. In B. Nordström, K. Petersson, and G. Plotkin, editors, Workshop of Types for Proofs and Programs, pages 245– 261, June 1992. Båstad, Sweden.

[22] Thomas F. Melham. Automating recursive type definitions in higher order logic. In Graham Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341–386. Springer, 1989.

[23] N. P. Mendler. Recursive types and type constraints in second-order lambda calculus. In 2nd Annual Symposium on Logic in Computer Science, pages 30– 36. ieee Computer Society Press, 1987.

[24] Robin Milner. Communication and Concurrency. Prentice-Hall, 1989.

[25] Robin Milner and Mads Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87:209–220, 1991.

[26] Bengt Nordström, Kent Petersson, and Jan Smith. Programming in Martin-Löf’s Type Theory. An Introduction. Oxford University Press, 1990.

[27] Lawrence C. Paulson. Logic and Computation: Interactive proof with Cambridge LCF. Cambridge University Press, 1987.

[28] Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5(3):363–397, 1989.

[29] Lawrence C. Paulson. Set theory as a computational logic: I. From foundations to functions. Technical Report 271, University of Cambridge Computer Laboratory, 1992.

[30] Lawrence C. Paulson. Introduction to Isabelle. Technical Report 280, University of Cambridge Computer Laboratory, 1993.

[31] Lawrence C. Paulson. The Isabelle reference manual. Technical Report 283, University of Cambridge Computer Laboratory, 1993.

[32] Lawrence C. Paulson. Isabelle’s object-logics. Technical Report 286, University of Cambridge Computer Laboratory, 1993.

[33] Lawrence C. Paulson. Set theory for verification: II. Induction and recursion. Technical report, University of Cambridge Computer Laboratory, 1993. Draft.

[34] Andrew M. Pitts. A co-induction principle for recursively defined domains. Technical Report 252, University of Cambridge Computer Laboratory, April 1992.

[35] Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.

[36] Mads Tofte. Type inference for polymorphic references. Information and Computation, 89:1–34, 1990.

[37] A. N. Whitehead and B. Russell. Principia Mathematica. Cambridge University Press, 1962. Paperback edition to *56, abridged from the 2nd edition (1927).