Induction and recursion on the partial real line with applications to Real PCF

Martín Hötzel Escardó

Department of computer science, Edinburgh University, King’s Buildings, Mayfield Road, Edinburgh EH9 3JZ, UK, e-mail: mhedcs.ed.ac.uk.

Thomas Streicher

Fachbereich Mathematik, Technische Hochschule Darmstadt, Schloßgartenstraße 7,

 64289 Darmstadt, Germany, e-mail: streichermathematik.th-darmstadt.de.

Abstract

The partial real line is an extension of the Euclidean real line with partial real numbers, which has been used to model exact real number computation in the programming language Real PCF. We introduce induction principles and recursion schemes for the partial unit interval, which allow us to verify that Real PCF programs meet their specification. They resemble the so-called Peano axioms for natural numbers. The theory is based on a domain-equation-like presentation of the partial unit interval. The principles are applied to show that Real PCF is universal in the sense that all computable elements of its universe of discourse are definable. These elements include higher-order functions such as integration operators.

Keywords: Induction, coinduction, exact real number computation, domain theory, Real PCF, universality.

Introduction

The partial real line is the domain of compact real intervals ordered by reverse inclusion [28,21]. The idea is that singleton intervals represent total real numbers, and that the remaining intervals represent (properly) partial real numbers. This is justified by the fact that the singleton map x ↦ {x} is a topological embedding of the Euclidean real line into the partial real line endowed with its Scott topology. The partial real line has been used to model exact real number computation in the framework of the programming language Real PCF [9,10], including computation of integrals [4].

To appear in Theoretical Computer Science 28 November 1997

We introduce induction principles and recursion schemes for the partial unit interval (the domain of closed subintervals of the unit interval with end-points 0 and 1), which allow us to verify that Real PCF programs meet their specification.

The induction principles and recursion schemes discussed in this paper resemble the so-called Peano axioms for natural numbers. They abstractly characterize the partial unit interval up to isomorphism, without reference to real numbers or intervals. Essentially, we replace zero and the successor function by the affine maps x ↦ x/2 and x ↦ (x + 1)/2, which play the rôle of partial real number constructors. This is related to binary expansions and, perhaps surprisingly, to Dedekind sections at the same time.

Preliminary ideas on recursion and induction on the real line appeared in [8], which considers uniform spaces. Our axioms are formulated in the framework of domain theory [1].

Domain theory allows one to derive induction principles and recursion schemes from canonical solutions of domain equations [20,34,24]. Domain equations model recursive definitions of data types, such as lists and trees. Since the partial real line is not an algebraic domain, it is not the canonical solution of any domain equation involving usual functors.

We establish new results about the notion of an inductive retraction introduced in [10], which generalizes canonical solutions of domain equations by means of ideas similar to those of Freyd [14,15]. In particular, we introduce the notion of a biquotient of a bifree algebra, and we show that the inductive retractions are the biquotients of the bifree algebras.

An interesting observation is that the Peano-like axioms discussed above consider only induction and recursion, but the inductive retraction induced by them automatically gives rise to coinduction and corecursion.

The techniques discussed here in a more general setting were also applied in conjunction with the technique introduced in [36] to show that Real PCF extended with a certain computable existential quantifier is universal [10], in the sense that all computable elements of its universe of discourse are definable. These elements include higher-order functions such as supremum and integration operators. Here we consider a further extension of the language with recursive types.

The universality result depends on a notion of computability. In domain theory this is achieved via effective presentations [6,30]. It is straightforward to show that there exists an effective presentation of the partial real line that makes the primitive operations of the language computable. For example, any standard enumeration of the rational basis gives such an effective presentation. But one then wonders whether a cleverer choice of an effective presentation would change the induced set of computable elements and functions, and this is indeed the case in general, as Kanda and Park have shown [19]. We apply the presentation of the partial real line as an inductive retract to show that there is a unique effective presentation of the partial real line that makes the primitive (and hence all) operations computable, up to equivalence of effective presentations. We can thus speak unambiguously about computability on the partial real line.

However, one still wonders how this relates to the classical theory of computability over the (total) real line. It was conjectured in [11] that a real valued function of real variables is computable iff it has a computable extension to a partial real valued function of partial real variables. It has been shown in [5] that this is indeed the case.

Organization

This paper is the full version of the extended abstracts [10,12]. It is organized in the following sections: (1) Domain theory, (2) The partial real line, (3) Peanolike axioms for the partial unit interval, (4) Generalized domain equations, (5) A generalized domain equation for the partial unit interval, (6) Applications to the programming language Real PCF.

1 Domain theory

Our main reference to domain theory is [1]. For its connections with topology see [33,16] (the papers [27] and [31] contain interesting technical and intuitive computational interpretations of topological concepts). Here we establish terminology and recall basic facts. Readers who are familiar with domain theory can proceed directly to Section 2.

1.1 Domains

A poset (partially ordered set) is a set equipped with a partial order (a reflexive, transitive and antisymmetric relation), generally denoted by the symbol ⊑. Existing joins (least upper bounds, suprema) and meets (greatest lower bounds, infima) are denoted by the symbols ⨆ and ⨅ respectively.

A subset Δ of a poset is said to be directed if each finite subset of Δ has an upper bound in Δ. Since the empty set is included in this definition, a directed set is necessarily non-empty.

A dcpo (directed complete poset) is a poset with least upper bounds of directed subsets. A subset U of a dcpo D is Scott open it is an upper set and the condition ⨆ Δ ∈ U for Δ ⊆ D directed implies Δ∩U ≠ ∅. The Scott open sets form a topology, known as the Scott topology. A function f : D → E between dcpos D and E is Scott continuous (continuous with respect to the Scott topologies) iff it is monotone and preserves least upper bounds of directed subsets.

A poset is bounded complete if it has a least element ⊥ (bottom) and joins of bounded subsets. In the presence of directed completeness, bounded completeness is equivalent to the existence of all non-empty meets.

In order to ensure that some facts stated below are true, we need to assume that our dcpos are continuous. Moreover, continuity of dcpos is a fundamental ingredient of the formulation of the notion of an effectively given domain. However, since we use continuity of dcpos only implicitly, via the facts that it entails, we deliberately omit the elaborate usual definition in terms of the so-called way-below relation.

For the bounded complete case, which is what we need in this paper, a telegraphic characterization is available: A bounded complete dcpo D is continuous iff every x ∈ D can be expressed as ⨆{⨅ U|x ∈ U}, where U ranges over Scott open subsets of D—see [27,16].

A familiar example from real analysis illustrates this characterization. The extended real line under its natural order is a bounded complete dcpo (in fact, a complete lattice). In this case the usual notation for suprema and infima is sup and inf. As one easily checks [16, pages 49–50], the Scott topology of this example is nothing but the topology of lower semicontinuity [26, pages 38, 50–52], given by non-trivial open sets of the form (r, +∞]. Hence the above characterization reduces to the fact that every real number x can be expressed as sup{inf(r, ∞]|x ∈ (r, ∞]} = sup{r|r < x}. Therefore the extended real line is a continuous lattice. In fact, this is a fundamental example. Continuity of the interval domain introduced below follows from the the same consideration on end-points of intervals. However, one has to admit that the example of the extended real line is a bit misleading in connection with the terminology information order introduced below. A better example is the interval domain.

In this paper a domain is a bounded complete continuous dcpo D. The order of a domain is referred to as its information order, and the relation x ⊑ y is interpreted as expressing the fact that y contains the same amount of information as x, and possibly more. Alternatively, one says that x is less defined than y. Under these interpretations, the bottom element has an empty information content, or is an undefined element. Computationally, bottom denotes non-terminating computations which don’t produce results.

A domain will be always considered as a topological space under its Scott topology. We often (implicitly) use the fact that the binary meet operation ⊓ : D × D → D is (jointly) continuous for every domain D.

Trivial but useful examples of domains arise as follows. One starts with a set A, adds a new element ⊥, and declares that x ⊑ y iff x = ⊥ or x = y. The resulting domain is called a flat domain and is denoted by A_{⊥}. Typical examples are the flat domains of natural numbers and truth-values, N = ℕ_{⊥} and B = 𝔹_{⊥}, where 𝔹 = {true, false}.

1.2 Retracts and idempotents

A retraction is a continuous function r : D → E for which there exists a continuous map s : E → D with r ∘ s = id_{E}, called a section. In this case E is said to be a retract of D. Retractions are quotient maps and sections are subspace embeddings.

The map s∘r : D → D is an idempotent whose fixed-points form a domain isomorphic to E. Conversely, every idempotent e : D → D gives rise to a domain E = e(D) which is a retract of D with retraction given by the corestriction of e to E and section given by the restriction of e to E.

1.3 Recursive definitions of functions

Any continuous endofunction f : D → D of a dcpo D with a bottom element has a least fixed point given by fix(f) = ⨆_{n∈ℕ} f^{n}(⊥).

If D and E are domains then the continuous functions from D to E, pointwise ordered by

f ⊑ g iff f(x) ⊑ g(x) for all x ∈ D,

form a domain denoted by [D → E]. Existing joins and binary meets are computed pointwise.

Fixed points and function spaces are applied to solve functional equations of the form

f = F (f)

with F : [D → E] → [D → E] continuous. Such a functional equation is often referred to as a recursive definition of f : D → E, and it is implicit that the least solution is taken:

f = fix(F).

1.4 Recursive definitions of domains

(The following material is not needed until Section 4.)

Domain theory also allows one to define domains by recursion:

D ≅ FD,

where F is an endofunctor of the category of domains. Domain equations are used to model recursively defined data types, such a lists and trees.

A solution of a domain equation D ≅ FD is a domain D together with an isomorphism i : FD → D. In order to state what the canonical solution is, it is convenient to use some basic category theory [25].

Let X be a category (for example the category of domains and continuous functions) and F : X → X be a functor.

An F-algebra is an arrow κ : FX → X, and a homomorphism from an algebra κ : FX → X to an algebra a : FA → A is a map h : X → A with h∘κ = a∘Fh. Dually, an F-coalgebra is an arrow δ : X → FX, and a homomorphism from a coalgebra b : B → FB to a coalgebra δ : X → FX is a map k : B → X with Fk ∘ b = δ ∘ k. These definitions are illustrated in the following diagrams:

\begin{matrix}FX & ⟶^{κ} & X \\ ^{Fh}↓ & & ↓^{h} \\ FA & ⟶_{a} & A \end{matrix}  \begin{matrix}B & ⟶^{b} & FB \\ ^{k}↓ & & ↓^{Fk} \\ X & ⟶_{δ} & FX \end{matrix}

One writes h : κ → a and k : b → δ to indicate that h and k are (co)algebra homomorphisms. Algebra (respectively coalgebra) homomorphisms compose and form a category.

If i : FX → X is an initial algebra (in the sense that there is a unique homomorphism from it to any other algebra) then i is an isomorphism in X.

A canonical solution of an equation X ≅ FX is an initial algebra i : FC → C whose inverse i^{−1} : C → FC is a final coalgebra. Such an algebra is called a bifree algebra. By initiality, bifree algebras are unique up to (unique) isomorphism.

We now turn back to domains. A function between domains is strict if it preserves bottom elements. The category of domains and strict continuous functions is denoted by SDom. A functor F : SDom → SDom is said to be locally continuous if for all domains D and E, the map f ↦ Ff : [D → E] → [FD → FE] is continuous.

Every locally continuous functor F : SDom → SDom has a bifree algebra i : FC → C. The reader is referred to [34,1] for its construction. But only the following facts are needed in this paper.

If a : FA → A is an algebra and b : B → FB is a coalgebra, then the unique homomorphisms h : i → a and k : b → i^{−1} can be recursively defined by

h = a ∘ Fh ∘ i^{−1}, k = i ∘ Fk ∘ b.

The functions h and k are said to be defined by structural recursion and corecursion respectively.

Structural recursion generalizes primitive recursion on the natural numbers, whereas structural corecursion generalizes minimization [32].

1.5 Effectively given domains

The reader is referred to [30]. The references [6,24] consider only algebraic domains, which exclude the partial real line. On the other hand, [5] considers a weaker version of [30]. Its drawback, from the point of view of this paper, is that effectively given domains in the weak sense are not closed under the function space construction. However, the reference contains the basic ingredients of [30] in an accessible form.

Essentially, an effective presentation of a domain is an enumerated basis of the domain, subject to certain axioms. An element of such an effectively given domain is defined to be computable if it is the join of a recursively enumerable directed set of basis elements. Computable functions can be defined as computable elements of function spaces, although equivalent direct definitions are also available.

2 The partial real line

The set R = Iℝ of compact real intervals ordered by reverse inclusion is referred to as the partial real line. It fails to be a domain only because it lacks a bottom element (which can be artificially added when necessary). The elements of R are referred to as partial real numbers, and a real number r is notationally identified with the singleton interval {r} and referred to as a total real number. Total real numbers have maximal information content.

The end-points of an interval x are given by

\underline{x} = inf x, \overline{x} = sup x.

By definition, the information order of R is given by

x ⊑ y iff x ⊇ y iff \underline{x} ≤ \underline{y} and \overline{y} ≤ \overline{x}.

Existing joins are given by

⨆ X = ⋂ X = [sup_{x∈X} \underline{x}, inf_{x∈X} \overline{x}].

Binary meets are given by

x ⊓ y = [min(\underline{x}, \underline{y}), max(\overline{x}, \overline{y})].

This coincides with x ∪ y only if x and y intersect.

2.1 Canonical extensions

The singleton map j : ℝ → R defined by j(x) = {x} embeds the real line as a subspace of the partial real line. This is an embedding onto the total reals.

If g : R → R is a function which maps total reals to total reals, then it restricts to a function f : ℝ → ℝ as in the diagram

\begin{matrix}ℝ & ⟶^{f} & ℝ \\ ^{j}↓ & & ↓^{j} \\ R & ⟶_{g} & R \end{matrix}

What is interesting is that if g is continuous with respect to the Scott topology in addition, then f is continuous with respect to the Euclidean topology. This is the case precisely because j : ℝ → R is a subspace embedding.

What is more interesting and does not follow from simple topological considerations such as the above is that the converse is also true: Every continuous map f : ℝ → ℝ extends to a continuous map g : R → R as in the above diagram.

(If a bottom element is added to R, the extension property is an immediate consequence of the fact that the domains are characterized as the densely injective spaces [16, page 127] and that embeddings onto maximal elements are dense. In any case, R belongs to a larger class of domains, which are characterized precisely as the injective spaces over finitary subspace embeddings, which include j : ℝ → R [7]. But in this paper we prefer to give a proof of the above special case of the extension property from first principles.)

Among all extensions there is a canonical extension If : R → R given by

If(x) = {f(r)|r ∈ x},

which is characterized as the most defined continuous extension, in the sense of the order of the function space [R → R]. It is well-defined because continuous functions map connected sets to connected sets and compact sets to compact sets, and hence compact intervals to compact intervals. It is Scott continuous because the direct image-formation operation preserves filtered intersections of compact sets, which in this case correspond to directed joins.

If f is increasing with respect to the natural order of real numbers then its canonical extension is computed pointwise:

If(x) = [f(\underline{x}), f(\overline{x})].

A function f : ℝ → ℝ is notationally identified with its canonical extension If : R → R, and we often define a continuous function f : R → R by first defining a continuous function f : ℝ → ℝ and then implicitly taking its canonical extension.

2.2 The partial unit interval

We shall work mainly with a subspace of the partial real line, the partial unit interval, defined as the domain I = I[0, 1] of closed subintervals of the unit interval [0, 1] ordered by reverse inclusion. Its bottom element is ⊥ = [0, 1]. The singleton map embeds the unit interval as a subspace of the unit interval, and the extension property is preserved.

3 Peano-like axioms for the partial unit interval

In order to separate the main line of argumentation from the details of the individual lemmas, their proofs are collected together at the end of this section.

We define the left and right successor functions succ_{L}, succ_{R} : I → I by

succ_{L}(x) = x/2, succ_{R}(x) = (x + 1)/2.

That is, succ_{L} and succ_{R} are the unique increasing affine maps which map the unit interval to its left and right halves L = [0, 1/2] and R = [1/2, 1] :

succ_{L}(⊥) = L, succ_{R}(⊥) = R.

We regard succ_{L} and succ_{R} as partial real number “constructors” analogous to zero and the successor map succ(x) = x + 1 on the natural numbers.

An important difference is that the natural numbers together with zero and successor form a free algebra, whereas the partial unit interval together with succ_{L} and succ_{R} will form a biquotient of a bifree algebra with respect to some equations. The main such equation is

succ_{L}(1) = succ_{R}(0),

which can be expressed as

succ_{L}(fix(succ_{R})) = succ_{R}(fix(succ_{L}))

by observing that 0 and 1 are the unique fixed points of succ_{L} and succ_{R}.

Another important difference is that natural numbers are constructed from zero by finitely many applications of the successor function, whereas the elements of the partial unit interval are constructed by infinitely many applications of succ_{L} and succ_{R}. For example, every total x ∈ I can be constructed as

x = ⨆_{n} succ_{a_{1}} ∘ ⋯ ∘ succ_{a_{n}}(⊥)

for some sequence a_{i} ∈ {L, R} corresponding to a binary expansion of x. Partial elements are constructed by iterating succ_{L} and succ_{R} in a more elaborate way, as it is shown in Section 5.3.

Pursuing our analogy with natural numbers, we now observe that every natural number is either zero or else the successor of a unique number.

For x, y ∈ R, define

(i) x < y iff \overline{x} < \underline{y}, (ii) x ≤ y iff \overline{x} ≤ \underline{y}, (iii) x ↑ y iff x and y have an upper bound in the information order iff x and y

intersect as intervals.

Then it is clear that exactly one of the following conditions holds:

x < y,  x ↑ y,  x > y.

Lemma 1 (Dyadic Trichotomy) For every x ∈ I,

(i) if x ≤ 1/2 then x = succ_{L}(y) for a unique y, (ii) if x ≥ 1/2 then x = succ_{R}(z) for a unique z, (iii) if x ↑ 1/2 then x = succ_{L}(y) ⊓ succ_{R}(z) for unique y ⊑ 1 and z ⊑ 0.

Recall that a number is notationally identified with a singleton interval, and notice that x ↑ 1/2 iff x ⊑ 1/2, because 1/2 is maximal in information content.

The predecessor function pred(x) = x − 1 on natural numbers, undefined or arbitrarily defined at zero, is a left inverse of the successor function. Similarly, succ_{a} has a left inverse pred_{a} defined by

pred_{L}(x) = min(2x, 1), pred_{R}(x) = max(0, 2x − 1).

The fact that every natural number is either zero or a successor can be expressed by the equation

n = if n = 0 then 0 else succ(pred(n)).

Let B be the flat domain of truth values, and for all r ∈ [0, 1] define a continuous predicate left_{r} : I → B by

left_{r}(x) = (x <_{⊥} r),

where

(x <_{⊥} y) = \begin{cases}true & if x < y, \\ false & if x > y, \\ ⊥ & if x ↑ y. \end{cases}

Also, write

left = left_{1/2}.

Remark 2 In [9–12] the maps succ_{a}, pred_{a} and left_{r} are denoted by cons_{a}, tail_{a} and head_{r} respectively. □

Finally, define the parallel conditional by

pif p then x else y = \begin{cases}x & if p = true, \\ y & if p = false, \\ x ⊓ y & if p = ⊥. \end{cases}

The idea is that, even if the condition is undefined, the most defined partial number which is less defined than x and y can be safely produced anyway.

Lemma 3 (Elementary Axioms)

pred_{L}(succ_{L}(x)) = x,  pred_{R}(succ_{L}(x)) = 0,
pred_{L}(succ_{R}(y)) = 1,  pred_{R}(succ_{R}(y)) = y,
pred_{L}(succ_{L}(x) ⊓ succ_{R}(y)) = x ⊓ 1, pred_{R}(succ_{L}(x) ⊓ succ_{R}(y)) = 0 ⊓ y,
left ∘ succ_{L}(x) ⊑ true,  left ∘ succ_{L}(x) = ⊥ iff x ⊑ 1,
left ∘ succ_{R}(y) ⊑ false,  left ∘ succ_{R}(y) = ⊥ iff y ⊑ 0,
x = pif left(x) then succ_{L}(pred_{L}(x)) else succ_{R}(pred_{R}(x)).

Given a set X, an element x ∈ X and a function g : ℕ → X, there is a unique function f : ℕ → X such that f(0) = x and f(n + 1) = g(n). A similar fact holds for the partial unit interval equipped with succ_{L} and succ_{R}, but we have to take into account the equation succ_{L}(1) = succ_{R}(0).

Lemma 4 (Definition by Cases) Let D be a domain and g_{L}, g_{R} : I → D be continuous maps such that

g_{L}(1) = g_{R}(0).

Then there is a unique continuous map f : I → D such that

f(succ_{L}(x)) = g_{L}(x),
f(succ_{R}(y)) = g_{R}(y),
f(succ_{L}(x) ⊓ succ_{R}(y)) = g_{L}(x) ⊓ g_{R}(y)  if x ⊑ 1 and y ⊑ 0,

namely the function f defined by

f(x) = pif left(x) then g_{L}(pred_{L}(x)) else g_{R}(pred_{R}(x)).

The natural numbers enjoy an induction principle, which can be expressed by saying that if a set of natural numbers contains zero and is closed under the successor operation, then it contains all natural numbers. A similar principle is enjoyed by the partial unit interval endowed with the operations succ_{L} and succ_{R}. But we have to take into account that partial real numbers are constructed by infinitely many applications of the left and right successor maps.

A subset of a domain D is called inductive if it closed under the formation of least upper bounds of directed subsets.

Lemma 5 (Dyadic Induction) Let A ⊆ I be inductive, and assume that the following conditions hold:

(i) (Base case) ⊥ ∈ A. (ii) (Inductive step) x ∈ A and y ∈ A imply

(a) succ_{L}(x) ∈ A,

(b) succ_{R}(y) ∈ A,

(c) succ_{L}(x) ⊓ succ_{R}(y) ∈ A if x ⊑ 1 and y ⊑ 0.

Then A = I.

We apply this lemma in the following form:

Corollary 6 Let D be a domain and f, g : I → D be continuous maps. In order to show that f = g it suffices to show that the following conditions hold:

(i) (Base case) f(⊥) = g(⊥). (ii) (Inductive step) f(x) = g(x) and f(y) = g(y) together imply

(a) f(succ_{L}(x)) = g(succ_{L}(x)),

(b) f(succ_{R}(y)) = g(succ_{R}(y)),

(c) f(succ_{L}(x) ⊓ succ_{R}(y)) = g(succ_{L}(x) ⊓ succ_{R}(y)) if x ⊑ 1 and y ⊑ 0.

Proof. If f and g are continuous then the set A = {x|f(x) = g(x)} is inductive. □

Remark 7 If we omit condition (c) of the inductive step, then in Lemma 5 we conclude that Max I ⊆ A, and in Corollary 6 we conclude that f_{|Max I} = g_{|Max I}. This can be used to prove that a continuous function f̄: I → I is an extension of a continuous function f : [0, 1] → [0, 1], although not necessarily the canonical extension. □

We can define functions on natural numbers by iteration. If X is a set, x is an element of X and g : X → X is a function, then there is a unique function f : ℕ → X such that f(0) = x and f(n + 1) = g(f(n)). A similar fact holds for the partial unit interval equipped with succ_{L} and succ_{R}. We first need a lemma:

Lemma 8 Let D be a domain, g_{L}, g_{R} : D → D be continuous maps, and f : I → D be any continuous solution to the functional equation

f(x) = pif left(x) then g_{L}(f(pred_{L}(x))) else g_{R}(f(pred_{R}(x))).

Then the following statements hold:

(i) f(0), f(1) and f(⊥) are fixed points of g_{L}, g_{R} and g_{L} ⊓ g_{R} respectively. (ii) f is uniquely determined by the values that it assumes at 0, 1, and ⊥.

(iii) f is the least continuous solution iff f(0) = fix(g_{L}), f(1) = fix(g_{L}), and f(⊥) = fix(g_{L} ⊓ g_{R}).

In particular, if g_{L}, g_{R}, and g_{L} ⊓ g_{R} have unique fixed points then there is a unique continuous solution.

Lemma 9 (Dyadic Iteration) Let D be a domain, and g_{L}, g_{R} : D → D be continuous maps such that

g_{L}(fix(g_{R})) = g_{R}(fix(g_{L})).

Then there is a unique continuous map f : I → D satisfying the equations

(Base case)

f(0) = fix(g_{L})
f(1) = fix(g_{R})
f(⊥) = fix(g_{L} ⊓ g_{R})

(Iteration step)

f(succ_{L}(x)) = g_{L}(f(x))
f(succ_{R}(y)) = g_{R}(f(y))
f(succ_{R}(x) ⊓ succ_{R}(y)) = g_{L}(f(x)) ⊓ g_{R}(f(y))  if x ⊑ 1 and y ⊑ 0,

namely the least continuous solution to the equation

f(x) = pif left(x) then g_{L}(f(pred_{L}(x))) else g_{R}(f(pred_{R}(x))).

Finally, the natural numbers system is uniquely specified, up to isomorphism, by the so-called Peano axioms, which are essentially the properties that we informally considered above for the sake of motivation. This idea is made formal in e.g. Stoll [35], where unary systems are used as a tool (a unary system is a set X together with an element x ∈ X and a function s : X → X).

In the following definition, the domain D generalizes the partial unit interval and the maps a_{L} and a_{R} generalize the constructor maps succ_{L} and succ_{R} respectively.

Definition 10 A binary system is a domain D equipped with a pair of continuous maps a_{L}, a_{R} : D → D such that

a_{L}(1) = a_{R}(0),

where

0 =^{def} fix(a_{L}), 1 =^{def} fix(a_{R}).

We also impose the technical condition fix(a_{L} ⊓ a_{R}) = ⊥, which ensures that homomorphisms defined below, as Lemma 9 suggests, make binary systems into a category under ordinary function composition.

A homomorphism from a binary system (D, a_{L}, a_{R}) to a binary system (E, b_{L}, b_{R}) is a continuous map f : D → E such that

f(0) = 0
f(1) = 1
f(⊥) = ⊥
f(a_{L}(x)) = b_{L}(f(x))
f(a_{R}(y)) = b_{R}(f(y))
f(a_{L}(x) ⊓ a_{R}(y)) = b_{L}(f(x)) ⊓ b_{R}(f(y))  if x ⊑ 1 and y ⊑ 0.  □

Binary systems were introduced and investigated in the context of uniform spaces in the extended abstract [8]. Lemma 9 can be formulated as

Theorem 11 (I, succ_{L}, succ_{R}) is an initial object in the category of binary systems.

By this we mean, of course, that there is a unique homomorphism from it to any other binary system. Since any two initial objects are isomorphic, this together with the following theorem axiomatically characterize the binary system (I, succ_{L}, succ_{R}) up to isomorphism, without explicit reference to real numbers or intervals:

Theorem 12 A binary system (D, s_{L}, s_{R}) is initial iff the following conditions hold:

(i) 0 and 1 are the unique fixed points of s_{L} and s_{R}. (ii) 0 ≠ 1 and 0 ⊓ 1 = ⊥. (iii) There are continuous maps l : D → B and p_{L}, p_{R} : D → D such that

\begin{aligned}p_{L}(s_{L}(x)) & = & x, & p_{R}(s_{L}(x)) & = & 0, \\ p_{L}(s_{R}(y)) & = & 1, & p_{R}(s_{R}(y)) & = & y, \\ p_{L}(s_{L}(x) ⊓ s_{R}(y)) & = & x ⊓ 1, & p_{R}(s_{L}(x) ⊓ s_{R}(y)) & = & 0 ⊓ y, \end{aligned}

l(s_{L}(x)) ⊑ true,  l(s_{L}(x)) = ⊥ iff x ⊑ 1,
l(s_{R}(y)) ⊑ false,  l(s_{R}(y)) = ⊥ iff y ⊑ 0,

x = pif l(x) then s_{L}(p_{L}(x)) else s_{R}(p_{R}(x)).

(iv) For any inductive set A ⊆ D, if (a) ⊥ ∈ A,

(b) x ∈ A and y ∈ A imply

s_{L}(x) ∈ A,
s_{R}(y) ∈ A,
s_{L}(x) ⊓ s_{R}(y) ∈ A if x ⊑ 1 and y ⊑ 0,

then A = D.

This and the following lemma are abstract versions of Lemmas 3 and 4.

Lemma 13 (Existence of Destructors) Let D = (D, s_{L}, s_{R}) be a binary system. Then there is at most one triple of continuous maps l : D → B and p_{L}, p_{R} : D → D satisfying the conditions of Theorem 12(iii).

Moreover, in this case D admits definition by cases, in the sense that for each domain E and each pair of continuous maps g_{L}, g_{L} : D → E with

g_{L}(1) = g_{R}(0)

there is a unique continuous map f : D → E such that

f(s_{L}(x)) = g_{L}(x)
f(s_{R}(y)) = g_{R}(y)
f(s_{L}(x) ⊓ s_{R}(y)) = g_{L}(x) ⊓ g_{R}(y)  if x ⊑ 1 and y ⊑ 0.

Proof. of Theorem 12. The previous lemmas show that the initial binary system satisfies the conditions. Conversely, the proof of Lemma 9 uses only the properties of binary systems in the statement of the theorem, without mentioning any particular property of (I, succ_{L}, succ_{R}), except for the equations

left(0) = true,  left(1) = false,
pred_{L}(0) = 0,  pred_{R}(1) = 1,
pred_{L}(⊥) = ⊥,  pred_{R}(⊥) = ⊥,

indirectly in Lemma 8, which easily follow from the other conditions. □

We finish this section with the proofs of the lemmas used to establish Theorems 11 and 12.

Proof. of Lemma 1 (Dyadic Trichotomy): (i): succ_{L} is bijective onto its image. Hence there is at most one y with x = succ_{L}(y). The image of succ_{L} is ↑ ↑L by definition. But x ≤ 1/2 iff L ⊑ x. (ii): Similar. (iii): In this case 1/2 ∈ x. Hence x = [\underline{x}, 1/2] ⊓ [1/2, \overline{x}] = succ_{L}([2\underline{x}, 1]) ⊓ succ_{L}([0, 2\overline{x} − 1]). □

Proof. of Lemma 3 (Elementary Axioms): Routine verification, included for the sake of completeness. The equation pred_{a} ∘ succ_{a} = id holds by construction. Also,

pred_{L}(succ_{R}(y)) = min(2((y + 1)/2), 1) = min(y + 1, 1) = 1,
pred_{R}(succ_{L}(x)) = max(0, 2(x/2) − 1) = max(0, x − 1) = 0.

Since for all p, q ∈ [0, 1] we have that p/2 ≤ (q + 1)/2, as p/2 ∈ L and (q + 1)/2 ∈ R, it follows that

succ_{L}(x) ⊓ succ_{R}(y) = [\underline{x}/2, \overline{x}/2] ⊓ [(\underline{y} + 1)/2, (\overline{y} + 1)/2]
= [\underline{x}/2, (\overline{y} + 1)/2].

Hence pred_{L}(succ_{L}(x) ⊓ succ_{R}(y)) = pred_{L}([\underline{x}/2, (\overline{y} + 1)/2]) = [\underline{x}, 1] = x ⊓ 1. Similarly, one has that pred_{R}(succ_{L}(x) ⊓ succ_{R}(y)) = 0 ⊓ y. The statements about left follow from the fact that succ_{L}(x) ≤ 1/2 and that succ_{L}(x) < 1/2 iff x/2 < 1/2 iff x < 1 iff x ⋢ 1. Similarly, succ_{R}(x) ≥ 1/2, and succ_{R}(y) < 1/2 iff y ⋢ 0. For the last equation, only the case left(x) = ⊥ is not immediate. In this case x ↑ 1/2, which is equivalent to x ⊑ 1/2 as 1/2 is maximal, and means that 1/2 ∈ x. Hence

x = [\underline{x}, 1/2] ⊓ [1/2, \overline{x}]
= succ_{L}(pred_{L}(x)) ⊓ succ_{R}(pred_{R}(x))
= pif left(x) then succ_{L}(pred_{L}(x)) else succ_{R}(pred_{R}(x)). □

Proof. of Lemma 4 (Definition by cases): It is clear from Lemma 1 that there is at most one such function. We show that f as defined in the statement of the lemma is such a function. If x ⋢ 1 then left(succ_{L}(x)) = true and

f(succ_{L}(x)) = g_{L}(pred_{L}(succ_{L}(x))) = g_{L}(x).

Otherwise left(succ_{L}(x)) = ⊥ and

f(succ_{L}(x)) = g_{L}(pred_{L}(succ_{L}(x))) ⊓ g_{R}(pred_{R}(succ_{L}(x)))
= g_{L}(x) ⊓ g_{R}(0) = g_{L}(x) ⊓ g_{L}(1) = g_{L}(x),

because g_{L}(x) ⊑ g_{L}(1), by monotonicity. Similarly, a case analysis on y shows that the equation f(succ_{R}(y)) = g_{R}(y) holds. Assume that x ⊑ 1 and y ⊑ 0. Then

f(succ_{L}(x) ⊓ succ_{R}(y))
= g_{L}(pred_{L}(succ_{L}(x) ⊓ succ_{R}(y))) ⊓ g_{R}(pred_{R}(succ_{L}(x) ⊓ succ_{R}(y)))
= g_{L}(x ⊓ 1) ⊓ g_{R}(0 ⊓ y) = g_{L}(x) ⊓ g_{R}(y),

which concludes the proof. □

Proof. of Lemma 5 (Dyadic Induction): Let B be the basis of I consisting of intervals with distinct dyadic end-points. In order to show that A = I, it suffices to conclude that B ⊆ A, because B is a basis of I. But since

B = ⋃_{n} B_{n}, where B_{n} = {[l/2^{n}, m/2^{n}]|0 ≤ l < m ≤ 2^{n}},

it suffices to show that B_{n} ⊆ A for all n by induction on n. For n = 0 this is immediate because B_{0} = {⊥} and ⊥ ∈ A by hypothesis. Assume that B_{n} ⊆ A, and define

L_{n} = succ_{L}(B_{n}),
R_{n} = succ_{R}(B_{n}),
C_{n} = {succ_{L}(x) ⊓ succ_{R}(y)|x, y ∈ B_{n} ∧ x ⊑ 1 ∧ y ⊑ 0}.

Then L_{n} ⊆ succ_{L}(A) ⊆ A because x ∈ A implies succ_{L}(x) ∈ A by hypothesis. Similarly, R_{n} ⊆ A and C_{n} ⊆ A. Hence L_{n} ∪ R_{n} ∪ C_{n} ⊆ A. But

L_{n} ∪ R_{n} ∪ C_{n}
= \{[\frac{l}{2^{n+1}} , \frac{m}{2^{n+1}} ]| 0 ≤ l < m ≤ 2^{n}\} ∪ \{[\frac{l + 2^{n}}{2^{n+1}} , \frac{m + 2^{n}}{2^{n+1}} ]| 0 ≤ l < m ≤ 2^{n}\}
∪ \{[\frac{l}{2^{n+1}} , \frac{1}{2}] ⊓ [\frac{1}{2}, \frac{m + 2^{n}}{2^{n+1}} ]| 0 ≤ l < 2^{n} ∧ 0 < m ≤ 2^{n}\}
= \{[\frac{l}{2^{n+1}} , \frac{m}{2^{n+1}} ]| 0 ≤ l < m ≤ 2^{n}\} ∪ \{[\frac{l}{2^{n+1}} , \frac{m}{2^{n+1}} ]| 2^{n} ≤ l < m ≤ 2^{n+1}\}
∪ \{[\frac{l}{2^{n+1}} , \frac{m}{2^{n+1}} ]| 0 ≤ l < 2^{n} < m ≤ 2^{n+1}\}
= \{[\frac{l}{2^{n+1}} , \frac{m}{2^{n+1}} ]| 0 ≤ l < m ≤ 2^{n+1}\}
= B_{n+1}.

Therefore B_{n+1} ⊆ A, which concludes the inductive argument. □

Proof. of Lemma 8: (i): One has that f(0) = g_{L}(f(0)) because left(0) = true and pred_{L}(0) = 0. Similarly, f(1) = g_{R}(f(1)). Since left(⊥) = ⊥ and pred_{L}(⊥) = pred_{R}(⊥), we have that f(⊥) = g_{L}(f(⊥)) ⊓ g_{R}(f(⊥)) = (g_{L} ⊓ g_{R})(f(⊥)).

(ii): We show by dyadic induction as in Corollary 6 that if f′ is a continuous solution agreeing with f at 0, 1 and ⊥ then f = f′. (Base case): By hypothesis. (Inductive step): Assume that f(x) = f′(x) and f(y) = f′(y). If left ∘ succ_{L}(x) = true then

f(succ_{L}(x)) = g_{L}(f(pred_{L}(succ_{L}(x)))) = g_{L}(f(x))
= g_{L}(f′(x)) = g_{L}(f′(pred_{L}(succ_{L}(x)))) = f′(succ_{L}(x)).

Otherwise left(succ_{L}(x)) = ⊥ and x ⊑ 1. Therefore,

f(succ_{L}(x)) = g_{L}(f(pred_{L}(succ_{L}(x)))) ⊓ g_{R}(f(pred_{R}(succ_{L}(x))))
= g_{L}(f(x)) ⊓ g_{R}(f(0)) = g_{L}(f′(x)) ⊓ g_{R}(f′(0))
= g_{L}(f′(pred_{L}(succ_{L}(x)))) ⊓ g_{R}(f′(pred_{R}(succ_{L}(x))))
= f′(succ_{L}(x)).

Similarly, f(succ_{R}(y)) = f′(succ_{R}(y)). Assume that x ⊑ 1 and y ⊑ 0. Then

f(succ_{L}(x) ⊓ succ_{R}(y))
= g_{L}(f(pred_{L}(succ_{L}(x) ⊓ succ_{R}(y)))) ⊓ g_{R}(f(pred_{R}(succ_{L}(x) ⊓ succ_{R}(y))))
= g_{L}(f(x ⊓ 1)) ⊓ g_{R}(f(0 ⊓ y)) = g_{L}(f(x)) ⊓ g_{R}(f(y))
= g_{L}(f′(x)) ⊓ g_{R}(f′(y)) = g_{L}(f′(x ⊓ 1)) ⊓ g_{R}(f′(0 ⊓ y))
= g_{L}(f′(pred_{L}(succ_{L}(x) ⊓ succ_{R}(y)))) ⊓ g_{R}(f′(pred_{R}(succ_{L}(x) ⊓ succ_{R}(y))))
= f′(succ_{L}(x) ⊓ succ_{R}(y)).

(iii): In view of (i) and (ii), it suffices to show that if f is the least solution then it satisfies the condition. Assume that f is the least solution. Then f = ⨆_{n} f_{n} where

f_{0}(x) = ⊥
f_{n+1}(x) = pif left(x) then g_{L}(f_{n}(pred_{L}(x))) else g_{R}(f_{n}(pred_{R}(x))).

But f_{n}(0) = g_{L}^{n}(⊥) because left(0) = true and pred_{L}(0) = 0. Hence f(0) = fix(g_{L}). Similarly, f(1) = fix(g_{R}). Also, f_{n+1}(⊥) = (g_{L} ⊓ g_{R})^{n}(⊥), because

f_{n+1}(⊥) = g_{L}(f_{n}(⊥)) ⊓ g_{R}(f_{n}(⊥)) = (g_{L} ⊓ g_{R})(f_{n}(⊥)).

Therefore f(⊥) = fix(g_{L} ⊓ g_{R}). □

Proof. of Lemma 9 (Dyadic Iteration): Define F : [I → D] → [I → D] by

F (f)(x) = pif left(x) then g_{L}(f(pred_{L}(x))) else g_{R}(f(pred_{R}(x))),

and let f : I → D be a continuous map satisfying the base case. By Lemma 8, it suffices to show that f satisfies the recursion step iff f = F (f). But, by Lemma 4, this is equivalent to show that

F (f)(succ_{L}(x)) = g_{L}(f(x))
F (f)(succ_{R}(y)) = g_{R}(f(y))
F (f)(succ_{R}(x) ⊓ succ_{R}(y)) = g_{L}(f(x)) ⊓ g_{R}(f(y)) if x ⊑ 1 and y ⊑ 0.

In fact, assuming that these equations hold, if f = F (f) then f satisfies the recursion step; and, conversely, if f satisfies the recursion step both f and F (f) satisfy the same definition by cases, and therefore they have to be the same by Lemma 4. If x ⋢ 1 then left(succ_{L}(x)) = true and

F (f)(succ_{L}(x)) = g_{L}(f(pred_{L}(succ_{L}(x)))) = g_{L}(f(x)).

Otherwise left(succ_{L}(x)) = ⊥ and

F (f)(succ_{L}(x)) = g_{L}(f(pred_{L}(succ_{L}(x)))) ⊓ g_{R}(f(pred_{R}(succ_{L}(x))))
= g_{L}(f(x)) ⊓ g_{R}(f(0)) = g_{L}(f(x)) ⊓ g_{R}(fix(g_{L}))
= g_{L}(f(x)) ⊓ g_{L}(fix(g_{R})) = g_{L}(f(x)) ⊓ g_{L}(f(1))
= g_{L}(f(x)),

because g_{L}(f(x)) ⊑ g_{L}(f(1)), by monotonicity. Similarly, F (f)(succ_{R}(y)) = g_{R}(f(y)). Assume that x ⊑ 1 and y ⊑ 0. Then

F (f)(succ_{L}(x) ⊓ succ_{R}(y))
= g_{L}(f(pred_{L}(succ_{L}(x) ⊓ succ_{R}(y)))) ⊓ g_{R}(f(pred_{R}(succ_{L}(x) ⊓ succ_{R}(y))))
= g_{L}(f(x ⊓ 1)) ⊓ g_{R}(f(0 ⊓ y)) = g_{L}(f(x)) ⊓ g_{R}(f(y)).  □

Proof. of Lemma 13 (Existence of Destructors): Assume that such maps exist. Claim: For every x ∈ I,

(i) if l(x) = true then x = s_{L}(y) for a unique y, (ii) if l(x) = false then x = s_{R}(z) for a unique z, (iii) if l(x) = ⊥ then x = s_{L}(y) ⊓ s_{R}(z) for unique y ⊑ 1 and z ⊑ 0.

(i): There is at most one such y because p_{L} is a left inverse of s_{L}. Since

x = pif true then s_{L}(p_{L}(x)) else s_{R}(p_{R}(x)) = s_{L}(p_{L}(x)),

We can take y = p_{L}(x). (ii): Similar. (iii): (Uniqueness) Assume that s_{L}(y) ⊓ s_{R}(z) = s_{L}(y′) ⊓ s_{R}(z′) for y, y′ ⊑ 1 and z, z′ ⊑ 0. Then, by applying p_{L} to both sides, we obtain y ⊓ 1 = y′ ⊓ 1. But y ⊓ 1 = y and y′ ⊓ 1 = y′. Therefore y = y′. Similarly, z = z′. (Existence):

x = pif ⊥ then s_{L}(p_{L}(x)) else s_{R}(p_{R}(x)) = s_{L}(p_{L}(x) ⊓ s_{R}(p_{R}(x))).

Hence p_{L}(x) = p_{L}(x) ⊓ 1 and p_{R}(x) = 0 ⊓ p_{R}(x). We can thus let y = p_{L}(x) and z = p_{R}(x), and the proof of the claim is concluded.

It follows that there is at most one f satisfying the definition-by-cases scheme. Therefore there is at most one triple of maps as specified above, because p_{L} and p_{R} satisfy the definition-by-cases scheme, and h is completely specified by the above clauses by virtue of the claim (the inequality l(s_{L}(x) ⊓ s_{R}(y)) ⊑ ⊥ holds by monotonicity). Finally, a function f satisfying the definition-by-cases scheme can be constructed as in Lemma 4, because it only uses the abstract properties of succ_{L}, succ_{R}, left, pred_{L}, and pred_{R} considered in the statement of the present lemma (and proved in Lemma 3). □

4 Generalized domain equations

(At this point the reader is assumed to be familiar with the theory of domain equations recalled in Section 1.4.)

We introduce a new technique, based on the theory of domain equations, which allows us to handle structural recursion with hypotheses that are weaker than is usual in domain theory. The basic idea is to consider not a distinguished solution D for a domain equation D ≅ FD, but more generally a domain D which is a retract of FD in a special way. We refer to such a domain D as an F-inductive retract.

The constructor and destructor maps for the partial unit interval discussed in Section 3 form an inductive retraction, as it is shown in Section 4.2, which is the object of study of Section 5. In this section we develop the general theory of inductive retracts.

4.1 Inductive retracts

Through this section F is an endofunctor of a category X.

Definition 14 An F-inductive retract is an object X together with an algebra κ : FX → X and a coalgebra δ : X → FX, subject to the condition

f = κ ∘ Ff ∘ δ iff f = id_{X}. □

The arrows κ and δ can be thought as a constructor and a destructor maps respectively. The first equation of the definition is illustrated in the following diagram:

FX ⟶^{κ} X
Ff↑  ↓^{f}
FX ⟵_{δ} X

The right-to-left implication shows that

κ ∘ δ = id_{X}

and hence X is a retract of FX. Also, notice that if ⟨κ, δ⟩ is an F-inductive retraction in X, then ⟨δ, κ⟩ is an F-inductive retraction in the opposite category X^{op}.

4.2 An example: the partial unit interval

In order to obtain an inductive retraction for the partial unit interval, we put the constructors (respectively destructors) together.

Define a functor T : SDom → SDom by

TD = B × D × D, Tf = id_{B} × f × f,

and define and algebra constr : TI → I and an algebra destr : I → TI by

constr = pif ∘ (id_{B} × succ_{L} × succ_{R}),
destr = ⟨left, pred_{L}, pred_{R}⟩.

That is,

constr(p, y, z) = pif p then succ_{L}(y) else succ_{R}(z),
destr(x) = ⟨left(x), pred_{L}(x), pred_{R}(x)⟩.

Proposition 15 The algebra constr : TI → I and the coalgebra destr : I → TI together form a T-inductive retraction.

Proof. The equation f = constr ∘ Tf ∘ destr is equivalent to the equation

f(x) = pif left(x) then succ_{L}(f(pred_{L}(x))) else succ_{R}(f(pred_{R}(x))).

We know that f = id_{I} is a solution by Lemma 3. But succ_{L} and succ_{R} and succ_{R} ⊓ succ_{L} have unique fixed-points. Therefore this is the unique solution by virtue of Lemma 8. □

4.3 Inductive retractions and bifree algebras

The following proposition shows that inductive retractions generalize bifree algebras (cf. Section 1.4):

Proposition 16 Let δ : X ⇆ FX : κ be an F-inductive isomorphism. If F has a bifree algebra then it is isomorphic to κ.

Proof. Let i : FC → C be a bifree algebra, r : i → κ be the unique algebra homomorphism and s : δ → i^{−1} be the unique coalgebra homomorphism. This means that r ∘ i = κ ∘ Fr and i^{−1} ∘ s = Fs ∘ δ. Hence

r ∘ s = r ∘ i ∘ i^{−1} ∘ s = κ ∘ Fr ∘ Fs ∘ δ = κ ∘ F(r ∘ s) ∘ δ.

By inductivity, r ∘ s = id_{X}. Since s = i ∘ Fs ∘ δ, we have that

s ∘ r ∘ i = i ∘ Fs ∘ δ ∘ κ ∘ Fr = i ∘ F(s ∘ r).

Hence s ∘ r : i → i and therefore s ∘ r = id_{C}. □

Throughout the remainder of this section, i : FC → C is an arbitrary bifree algebra and δ : X ⇆ FX : κ is an arbitrary F-inductive retraction.

The first part of the proof of Proposition 16 shows that every inductive retract is a retract of the bifree algebra, in a canonical way:

Lemma 17 If r : i → κ and s : δ → i^{−1} are the unique (co)algebra homomorphisms then the arrows s : X ⇆ C : r form a retraction with r ∘ s = id_{X}.

4.4 Structural recursion and corecursion

Proposition 18 Let r : i → κ, s : δ → i^{−1} and e = s ∘ r : C → C.

(i) For any algebra a : FA → A, there is a homomorphism f : κ → a iff h = h ∘ e, where h : i → a, and in this case f = h ∘ s.

(ii) For any coalgebra b : B → FB, there is a homomorphism g : b → δ iff k = e ∘ k, where k : b → i^{−1}, and in this case g = r ∘ k.

Proof. (i): If f : κ → a then f ∘ r = h because r : i → κ. Therefore f = h ∘ s and h = h ∘ s ∘ r. Conversely, if f ∘ r : i → a then f : κ → a because

f ∘ κ = f ∘ κ ∘ F(r ∘ s) = f ∘ κ ∘ Fr ∘ Fs = f ∘ r ∘ i ∘ Fs
= a ∘ F(f ∘ r) ∘ Fs = a ∘ Ff ∘ F(r ∘ s) = a ∘ Ff.

If h ∘ s ∘ r = h then this holds in particular for f = h ∘ s. (ii): Dual to (i). □

Condition (i) means that h respects the congruence on C induced by the idempotent e = s ∘ r, and that f is the restriction of h to X via s. Dually, condition (ii) means that the image of k is contained in image of e and that g is the corestriction of k to X via r.

Corollary 19

(i) For every algebra a : FA → A there is at most one homomorphism f : κ → a.

(ii) For every coalgebra b : B → FB there is at most one homomorphism g : b → δ.

Only for the last result of this subsection, we assume that our base category X is the category SDom of domains and strict continuous maps.

Proposition 20 Let F : SDom → SDom be locally continuous.

(i) If there is a homomorphism f : κ → a for a given algebra a : FA → A then it can be recursively defined by f = a ∘ Ff ∘ δ.

(ii) If there is a homomorphism g : b → δ for a given coalgebra b : B → FB then it can be recursively defined by g = κ ∘ Fg ∘ b.

Proof. (i): The least solution of the equation is f′ = ⨆_{n} f_{n}, where the sequence f_{n} is inductively defined by f_{0} = ⊥ and f_{n+1} = a ∘ Ff_{n} ∘ δ. Define id_{n} : X → X by id_{0} = ⊥ and id_{n+1} = κ ∘ Fid_{n} ∘ δ. By local continuity of F,

⨆_{n} id_{n} = ⨆_{n} id_{n+1} = ⨆_{n}(κ ∘ Fid_{n} ∘ δ) = κ ∘ F (⨆_{n} id_{n}) ∘ δ.

Hence ⨆_{n} id_{n} = id_{X} by inductivity. Since f is strict, we have that f_{0} = f ∘ id_{0}. Assuming that f_{n} = f ∘ id_{n} we deduce that

f_{n+1} = a ∘ Ff_{n} ∘ δ = a ∘ Ff ∘ Fid_{n} ∘ δ = f ∘ κ ∘ Fid_{n} ∘ δ = f ∘ id_{n+1}.

Hence f_{n} = f ∘ id_{n} for every n. Therefore

f′ = ⨆ f_{n} = ⨆_{n}(f ∘ id_{n}) = f ∘ ⨆_{n} id_{n} = f ∘ id_{X} = f.

(ii): Dual to (i). □

Thus, in order to find a recursive definition of a function f : X → A we can try to find an algebra a : FA → A such that f : κ → a is a homomorphism, and in order to find a recursive definition of a function g : B → X we can try to find a coalgebra b : B → FB such that g : b → δ is a homomorphism. If we succeed in finding such algebra a and coalgebra b, then we obtain a definition of f by structural recursion and a definition of g by structural corecursion.

4.5 Biquotients of bifree algebras

We have seen that any F-inductive retraction δ : X ⇆ FX : κ appears as a retract of the bifree F-algebra i : FC → C via r : i → κ and s : δ → i^{−1} with r ∘ s = id_{X}.

In this subsection, which is not needed in the development that follows, we characterize for a bifree algebra i : FC → C the idempotents e : C → C which admit a splitting e = s ∘ r of the kind just described. Recall that any idempotent in SDom splits through its image. But notice that we are still working in an arbitrary category X.

Definition 21 Let e : C → C be an idempotent and define an algebra a : FC → C and a coalgebra b : C → FC by

a = e ∘ i, b = i^{−1} ∘ e.

We say that e is a biquotient of the bifree algebra i : FC → C if the following conditions hold:

(B1) e : i → a, (B2) e : b → i^{−1}, (B3) h = a ∘ Fh ∘ b iff h = e. □

Theorem 22

(i) If δ : X ⇄ FX : κ is an F-inductive retraction, r : i → κ and s : δ → i^{−1}, then e =^{def} s ∘ r is a biquotient of i. Moreover, κ and δ can be recovered from r and s as

κ = r ∘ i ∘ Fs δ = Fr ∘ i^{−1} ∘ s.

(ii) If e : C → C is a biquotient of i and e = s ∘ r with r ∘ s = id_{X}, then the maps

κ =^{def} r ∘ i ∘ Fs : FX → X
δ =^{def} Fr ∘ i^{−1} ∘ s : X → FX

constitute an F-inductive retraction. Moreover, we have r : i → κ and s : δ → i^{−1}.

Proof. (i): Conditions (B1) and (B2) hold by the following equational reasoning:

e ∘ i ∘ Fe = s ∘ r ∘ i ∘ Fs ∘ Fr = s ∘ κ ∘ Fr ∘ Fs ∘ Fr
= s ∘ κ ∘ Fr = s ∘ r ∘ i = e ∘ i,
Fe ∘ i^{−1} ∘ e = Fs ∘ Fr ∘ i^{−1} ∘ s ∘ r = Fs ∘ Fr ∘ Fs ∘ δ ∘ r
= Fs ∘ δ ∘ r = i^{−1} ∘ s ∘ r = i^{−1} ∘ e.

From this we immediately obtain

e ∘ i ∘ Fe ∘ i^{−1} ∘ e = e ∘ i ∘ i^{−1} ∘ e = e ∘ e = e.

For the other implication of condition (B3), let h : C → C with e ∘ i ∘ Fh ∘ i^{−1} ∘ e = h. It follows that

r ∘ i ∘ Fh ∘ i^{−1} ∘ s = r ∘ h ∘ s.

Hence

r ∘ h ∘ s = r ∘ i ∘ Fh ∘ i^{−1} ∘ s = κ ∘ Fr ∘ Fh ∘ Fs ∘ δ
= κ ∘ F(r ∘ h ∘ s) ∘ δ,

which entails r ∘ h ∘ s = id_{X} as κ and δ form an F-inductive retraction. Thus we get

h = e ∘ h ∘ e = s ∘ r ∘ h ∘ s ∘ r = s ∘ r = e.

The proposed reconstruction of κ and δ from r and s can be seen as follows:

r ∘ i ∘ Fs = κ ∘ Fr ∘ Fs = κ,
Fr ∘ i^{−1} ∘ s = Fr ∘ Fs ∘ δ = δ.

(ii): We have that

(a) r ∘ i = r ∘ i ∘ F(s ∘ r),
(b) i^{−1} ∘ s = F(s ∘ r) ∘ i^{−1} ∘ s,
(c) s ∘ r ∘ i ∘ Fh ∘ i^{−1} ∘ s ∘ r = h iff h = e,

and hence that

κ ∘ δ = r ∘ i ∘ Fs ∘ Fr ∘ i^{−1} ∘ s
= r ∘ i ∘ F(s ∘ r) ∘ i^{−1} ∘ s
= r ∘ i ∘ i^{−1} ∘ s = r ∘ s = id_{X}.

Let f : X → X with f = κ ∘ Ff ∘ δ. As

κ ∘ Ff ∘ δ = r ∘ i ∘ F(s ∘ f ∘ r) ∘ i^{−1} ∘ s,

for h =^{def} s ∘ f ∘ r we get

h = s ∘ r ∘ i ∘ Fh ∘ i^{−1} ∘ s ∘ r,

from which we get by (c) that h = e. But then

f = r ∘ s ∘ f ∘ s ∘ r = r ∘ h ∘ s = r ∘ e ∘ s = id_{X}

as desired. Finally, r : i → κ and s : δ → i^{−1} because

κ ∘ Fr = r ∘ i ∘ Fs ∘ Fr = r ∘ i by (a),
Fs ∘ δ = Fs ∘ Fr ∘ i^{−1} ∘ s = i^{−1} ∘ s by (b). □

5 A generalized domain equation for the partial unit interval

In this section we investigate the presentation of the unit interval as an inductive retract which was introduced in Section 4.2. We first relate the presentation as an inductive retract to the presentation as a binary system developed in Section 2. We then give some examples of recursive definitions based on the inductive retraction. After that we show how the presentation as an inductive retract is simultaneously related to binary expansions and Dedekind cuts in a natural way. Finally, we briefly consider coinduction on the partial unit interval.

Recall that a functor T : SDom → SDom was defined in Section 4.2 by

TD = B × D × D, Tf = id_{B} × f × f,

and that an algebra constr : TI → I and a coalgebra destr : I → TI, defined by

constr(p, y, z) = pif p then succ_{L}(y) else succ_{R}(z),
destr(x) = ⟨left(x), pred_{L}(x), pred_{R}(x)⟩,

were shown to constitute an inductive retraction.

5.1 Binary algebras

We begin by relating the algebra constr : TI → I to the binary system (I, succ_{L}, succ_{R}) investigated in Section 2.

Define a binary algebra to be an algebra a : TD → D of the form

pif ∘ (id_{B} × a_{L} × a_{R})

for a_{L}, a_{R} : D → D. Such maps are necessarily unique because they have to satisfy the equations a_{L}(x) = a(true, x, y) and a_{R}(y) = a(false, x, y). Of course, the main example of a binary algebra is constr.

Compare the following proposition to Lemma 9 and Definition 10:

Proposition 23 Let a : TD → D be a binary algebra. Then a strict continuous map f : I → D is a homomorphism from constr to a iff

f(succ_{L}(x)) = a_{L}(f(x))
f(succ_{R}(y)) = a_{R}(f(y))
f(succ_{R}(x) ⊓ succ_{R}(y)) = a_{L}(f(x)) ⊓ a_{R}(f(y)).

Compare the following proposition to Lemmas 8 and 9:

Proposition 24 If there is a homomorphism from constr to a binary algebra a : TD → D then it is the least continuous map f : I → D such that

f(x) = pif left(x) then a_{L}(f(pred_{L}(x)) else a_{R}(f(pred_{R}(x)).

Proof. By Proposition 20 we know that if there is a homomorphism constr → a, then it is the least continuous function f such that

f = a ∘ Tf ∘ destr,

which is equivalent to the above equation. □

5.2 Examples of recursive definitions

Proposition 25 The complement map compl : I → I defined by compl(x) = 1 − x can be recursively defined by

compl(x) = pif left(x)
then succ_{R}(compl(pred_{L}(x)))
else succ_{L}(compl(pred_{R}(x))).

Proof. This follows from Proposition 24, because compl is easily seen to be an algebra homomorphism from constr to pif ∘ (id_{B} × succ_{R} × succ_{L}). □

Proposition 26 The map exp : I[0, 1] → I[1, 2] defined by exp(x) = 2^{x} can be recursively defined by

exp(x) = pif left(x) then \sqrt{exp(pred_{L}(x))} else \sqrt{2 exp(pred_{L}(x))}.

Proof. Define a_{L}, a_{R} : I[1, 2] → I[1, 2] by a_{L}(x) = \sqrt{x} and a_{R}(x) = \sqrt{2x}. Then exp is again easily seen to be an algebra homomorphism from constr to pif ∘ (id_{B} × a_{L} × a_{R}), and the result again follows from Proposition 24. □

More examples of definitions of elementary functions by dyadic recursion can be found in [9,11], and a recursive definition of Riemann integration can be found in [4].

5.3 Bifurcated binary expansions

The canonical solution of the domain equation D ≅ TD is the domain BTree of infinite binary trees with nodes labeled by truth values, ordered nodewise, together with the bifree algebra

mktree : T(BTree) → BTree

that maps a list ⟨p, s, t⟩ to the tree with root labeled by the truth value p and with left and right subtrees s and t respectively [24]:

mktree(p, s, t) = \begin{aligned}& & p \\ & ↙ & & ↘ \\ s & & & & t \end{aligned}

Let

num : mktree → constr : BTree → I
bin : destr → mktree^{−1} : I → BTree

be the unique (co)algebra homomorphisms. By Lemma 17, num ∘ bin = id_{I}, so that I is a retract of BTree. The tree bin(x) can be thought as a bifurcated binary expansion of the partial number x.

By unfolding the definitions one sees that num and bin are the unique continuous maps such that

num(mktree(p, s, t)) = pif p then succ_{L}(num(s)) else succ_{R}(num(t))

and

bin(x) = mktree(left(x), bin(pred_{L}(x)), bin(pred_{R}(y))).

5.4 Dedekind sections

We show that bin(x) is essentially the Dedekind section of x ∈ I. Recall that the Dedekind section of a real number x is given by the pair of sets {q ∈ ℚ|q < x} and {q ∈ ℚ|q > x}.

First, notice that an infinite binary tree over B can be defined as a function 2^{∗} → B, where 2 = {0, 1}. Second, notice that the set 2^{∗} of finite sequences over the set 2 is in bijection with the set of dyadic rationals

𝔻 = {m/2^{n} ∈ (0, 1)|m, n ∈ ℕ},

via the unique map ϕ : 2^{∗} → 𝔻 such that

ϕ(ϵ) = 1/2,  ϕ(0α) = succ_{L}(ϕ(α)),  ϕ(1α) = succ_{R}(ϕ(α)).

Here ϵ is the empty sequence, α ranges over finite sequences, and succ_{L} and succ_{R} are considered as maps 𝔻 → 𝔻. It follows that an infinite binary tree over B can be considered as a function 𝔻 → B. Under this interpretation one has that

mktree(p, s, t)(1/2) = p,
mktree(p, s, t)(succ_{L}(d)) = s(d),
mktree(p, s, t)(succ_{R}(d)) = t(d).

Proposition 27 (Dedekind-section representation)

For every x ∈ I, the binary tree bin(x) is the characteristic function of the dyadic Dedekind section of x, in the sense that for all d ∈ 𝔻,

bin(x)(d) = \begin{cases}true & if d < x, \\ false & if d > x, \\ ⊥ & if d ↑ x. \end{cases}

Proof. The set 𝔻 satisfies the following dyadic induction principle: If A ⊆ 𝔻 contains 1/2 and is closed under succ_{L} and succ_{R}, then A is the whole of 𝔻 (cf. Remark 7). We show that the equation holds for all x and d by dyadic induction on d. By definition of bin and mktree, we have that bin(x)(1/2) = left(x), which establishes the base case. Now assume that the equation holds for all x and a given d ∈ 𝔻. Then the fact that bin(x)(succ_{L}(d)) = bin(pred_{L}(x))(d) establishes one half of the induction step, because d < pred_{L}(x) = min(2x, 1) iff d/2 < x iff succ_{L}(d) < x, and, similarly, d > pred_{L}(x) iff succ_{L}(d) > x. The other half is established in a symmetric fashion. □

5.5 Computing with Dedekind sections

We now apply the theory of inductive retractions developed in Section 4 to show how to compute with partial real numbers via Dedekind sections. Some proofs are postponed to the end of the subsection.

We begin by looking for a recursive definition of the normalization idempotent

BTree ⟵^{norm} BTree = BTree ⟵^{bin} I ⟵^{num} BTree

not involving the intermediate domain I. Of course, the normalization idempotent has the Dedekind sections as its fixed points.

If we have an algebra constr′ : T(BTree) → BTree such that bin is a homomorphism from constr to constr′, then norm : mktree → constr′, because num : mktree → constr, by definition, and homomorphisms compose. Therefore norm is the unique continuous map such that

norm ∘ mktree = constr′ ∘ Tnorm,

or, equivalently, such that

norm (mktree(p, s, t)) = constr′(p, norm(s), norm(t)),

which produces the desired recursive definition. Moreover, if constr′ is a binary algebra (Section 5.1), in the sense that we can find maps succ′_{L}, succ′_{R} : BTree → BTree such that

constr′ = pif ∘ (id_{B} × succ′_{L} × succ′_{R}),

then we can recursively define norm by

norm (mktree(p, s, t)) = pif p then succ′_{L}(norm(s)) else succ′_{R}(norm(t)).

Lemma 28 Let succ′_{L}, succ′_{R} : BTree → BTree be continuous maps, and define

constr′ = pif ∘ (id_{B} × succ′_{L} × succ′_{R}).

If the diagrams

I ⟶^{succ_{L}} I
bin↓  ↓^{bin}
BTree ⟶_{succ′_{L}} BTree

I ⟶^{succ′_{R}} I
bin↓  ↓^{bin}
BTree ⟶_{succ′_{R}} BTree

commute then bin : constr → constr′. In order to construct such maps succ′_{L} and succ′_{R}, we first consider the following construction: Lemma 29 Let left′_{0}, left′_{1} : BTree → B be recursively defined by

left′_{0} (mktree(p, s, t)) = pif p then left′_{0}(s) else false,
left′_{1} (mktree(p, s, t)) = pif p then true else left′_{1}(t).

Then

left′_{0} = left_{0} ∘ num and left′_{1} = left_{1} ∘ num.

The continuous maps of the hypothesis of Lemma 28 can be constructed as follows: Lemma 30 Let succ′_{L}, succ′_{R} : BTree → BTree be defined by

succ′_{L}(t) = mktree(left′_{1}(t), t, bin(0)),
succ′_{R}(t) = mktree(left′_{0}(t), bin(1), t).

Then the diagrams displayed in Lemma 28 commute. Notice that bin(0) and bin(1) are the binary trees with all nodes labeled by respectively true and false. We have thus established Proposition 31 The normalization idempotent can be recursively defined by

norm (mktree(p, s, t)) = pif p then succ′_{L}(norm(s)) else succ′_{R}(norm(t)).

Next we define left′ : BTree → B and pred′_{L}, pred′_{R} : BTree → BTree by

left′ (mktree(p, s, t)) = pif p then left′_{1}(s) else left′_{0}(t),
pred′_{L} (mktree(p, s, t)) = pif p then s else bin(1),
pred′_{R} (mktree(p, s, t)) = pif p then bin(0) else t.

Proposition 32 For each a ∈ {L, R}, the following diagrams commute:

I ⟶^{succ_{a}} I
bin↓  ↑^{num}
BTree ⟶_{succ′_{a}} BTree

I ⟶^{left} B
bin↓  ↑^{id}
BTree ⟶_{left′} B

I ⟶^{pred_{a}} I
bin↓  ↑^{num}
BTree ⟶_{pred′_{a}} BTree

We finish this subsection with the proofs of the above claims.

Lemma 33 The function bin : I → BTree is multiplicative, in the sense that it preserves binary meets.

Proof. The function bin is the least fixed-point of the continuous functional F defined by

F (f) = mktree ∘ Tf ∘ destr.

The function mktree is multiplicative because binary meets of triples are computed componentwise, and binary meets of trees are computed nodewise. If f is multiplicative so is Tf. Also destr = ⟨left, pred_{L}, pred_{R}⟩ is multiplicative because left, pred_{R} and pred_{L} are multiplicative, as it can be easily checked. Hence if f is multiplicative so is F (f), because multiplicative functions are closed under composition. Therefore the least fixed-point of F is multiplicative, because the binary meet operation preserves directed joins. □

Proof. of Lemma 28: By Lemma 33, if the diagrams commute then

bin ∘ constr(p, y, z) = bin(pif p then succ_{L}(y) else succ_{R}(z))
= pif p then bin(succ_{L}(y)) else bin(succ_{R}(z))
= pif p then succ′_{L}(bin(y)) else succ′_{R}(bin(z))
= succ′(p, bin(y), bin(z))
= succ′ ∘ Tbin(p, y, z),

and hence bin : constr → constr′. □

Proof. of Lemma 29: Define

f_{0} = ⊥  f_{n+1} (mktree(p, s, t)) = pif p then f_{n}(s) else false,
id_{0} = ⊥  id_{n+1} (mktree(p, s, t)) = mktree(p, id_{n}(s), id_{n}(t)).

Then left′_{0} and id : BTree → BTree are the least upper bounds of the chains f_{n} and id_{n} respectively. We show by induction on n that left_{0}∘num∘id_{n} = f_{n}. For the base case this is immediate, because left_{0} and num are both strict. For the inductive step, notice that left_{0} is multiplicative, and that hence it distributes over the parallel conditional. Also, notice that left_{0} ∘ succ_{L} = left_{0}, because x < 0 iff x/2 < 0, and that left_{0} ∘ succ_{R}(x) = false, because succ_{R}(x) ≥ 1/2. Hence left_{0} ∘ num ∘ id_{n+1} (mktree(p, s, t))

= left_{0} ∘ num (mktree(p, id_{n}(s), id_{n}(t)))
= left_{0}(pif p then succ_{L}(num(id_{n}(s))) else succ_{R}(num(id_{n}(s)))
= pif p then left_{0}(succ_{L}(num(id_{n}(s)))) else left_{0}(succ_{R}(num(id_{n}(s))))
= pif p then left_{0}(num(id_{n}(s))) else false
= pif p then f_{n}(s) else false
= f_{n+1} (mktree(p, s, t)) ,

which finishes our inductive argument. Therefore

left′_{0} = ⨆_{n} f_{n} = ⨆ left_{0} ∘ num ∘ id_{n} = left_{0} ∘ num ∘ ⨆ id_{n} = left_{0} ∘ num.

The proof for left′_{1} is symmetric. □

Proof. of Lemma 30: Since left′_{1} = left_{1} ∘ num by Lemma 29, and since num ∘ bin, we conclude that left_{1} = left′_{1} ∘bin. Since left∘succ_{L}(x) = (x/2 <_{⊥} 1/2) = (x <_{⊥} 1) = left_{1}(x),

bin ∘ succ_{L}(x)

= mktree(left ∘ succ_{L}(x), bin(pred_{L}(succ_{L}(x))), bin(pred_{R}(succ_{L}(x))))
= mktree(left_{1}(x), bin(x), bin(0))
= mktree(left′_{1}(bin(x)), bin(x), bin(0))
= succ′_{L} ∘ bin(x).

The proof for succ_{R} is symmetric. □

Proof. of Proposition 32: By Lemma 30, we have that bin∘succ_{a} = succ′_{a}∘bin. Hence

succ_{a} = num ∘ succ_{a} ∘ bin,

because num ∘ bin = id_{I}. For left we have that

left′ ∘ bin(x)

= left′(mktree(left(x), bin(pred_{L}(x)), bin(pred_{R}(x))))
= pif left(x) then left′_{1}(bin(pred_{L}(x))) else left′_{0}(bin(pred_{R}(x)))
= pif left(x) then left_{1}(pred_{L}(x)) else left_{0}(pred_{R}(x)),

by virtue of Lemma 29. If left(x) = true then x < 1/2 and hence pred_{L}(x) < 1. Thus, in this case the last term is

left_{1}(pred_{L}(x)) = true = left(x).

Similarly, if left(x) = false then

left_{1}(pred_{R}(x)) = false = left(x).

Otherwise left(x) = ⊥. Then x ⊑ 1/2 and hence pred_{L}(x) ⊑ 1 and pred_{R}(x) ⊑ 0. Therefore in this case the last term is

left_{1}(pred_{L}(x)) ⊓ left_{0}(pred_{R}(x)) = ⊥ ⊓ ⊥ = ⊥ = left(x).

For pred_{L} we have that

num ∘ pred′_{L} ∘ bin(x)
= num ∘ pred′_{L}(mktree(left(x), bin(pred_{L}(x)), bin(pred_{R}(x))))
= num(pif left(x) then bin(pred_{L}(x)) else bin(1))
= num ∘ bin(pif left(x) then pred_{L}(x) else 1)
= pif left(x) then pred_{L}(x) else 1

If left(x) = true then the last term is pred_{L}(x). If left(x) = false then the last term is 1 = pred_{L}(x). Otherwise, left(x) = ⊥. Then x ⊑ 1/2 and pred_{L}(x) ⊑ 1. Hence in this case the last term is

pred_{L}(x) ⊓ 1 = pred_{L}(x).

For pred_{R} we have a symmetric proof. □

5.6 Coinduction

Dana Scott suggested that we should also consider a characterization of the partial unit interval via “co-Peano axioms” based on coinduction and coiteration. Although we don’t have such a characterization yet, a coinduction principle related to the ideas of Smyth [32] and Fiore [13] immediately follows by considering the bifree T-algebra.

A bisimulation on the partial unit interval is a binary relation ∼⊆ I × I such that

x ∼ y implies that left(x) = left(y) and pred_{a}(x) ∼ pred_{a}(y) for a ∈ {R, L}.

We say that x and y are bisimilar if they are related by some bisimulation.

Proposition 34 (Coinduction) If x, y ∈ I are bisimilar then x = y.

Proof. Let x and y be bisimilar partial numbers. Then bin(x) and bin(y) are bisimilar trees. Hence bin(x) = bin(y) by [13]. Therefore x = y because bin is split mono. □

Of course, we can replace equalities by inequalities thus obtaining the notion of a simulation and a more general coinduction principle for establishing inequalities.

6 Applications to the programming language Real PCF

Real PCF [9] is an extension of the programming language PCF [29,22] with data types for the partial unit interval and the partial real line. For simplicity and without essential loss of generality, we only discuss the partial unit interval. A sketch of the treatment of the whole partial real line can be found in [11].

In this section we consider two fundamental questions: (1) What is an appropriate notion of computability for the partial real line? (2) Having found such a notion, is Real PCF universal, in the sense that all computable functions are expressible in the language?

We answer these questions by means of the recursion techniques introduced in the previous section.

6.1 The programming language PCF

PCF stands for Programming language for Computable Functions. It consists of the terms of Scott’s LCF (Logic of Computable Functions). This logic was introduced in a widely circulated manuscript produced in 1969, recently published as [29], which contains the first steps towards domain theory—see also [17].

PCF is not intended as a practical programming language. Rather, it is intended as a paradigmatic programming language for the investigation of theoretical issues such as operational and denotational semantics, computational adequacy, full abstraction, program reasoning, universality [22,18]. As such, it is very concise.

We shall be deliberately informal concerning syntax and semantics. Only Scott’s model of PCF will be considered, and therefore it will not be necessary to say what a model is.

PCF is a functional programming language [3]. The PCF basic data types are the flat domains N and B of natural numbers and truth values. The remaining data types are obtained by iterating the function space construction (Section 1.3). One thus has types [N → B], [[N → B] → B], [N → [N → N]] and so on.

The primitive operations for the truth values type are true, false and the conditional form if p then x else y.

The primitive operations for the natural numbers type are 0, succ, pred and a test for equality with zero.

Since PCF doesn’t have cartesian products, functions of the form, say, f : N × N → N have to be represented as “curried” functions of the form f : N → [N → N]. In this case, instead of f(x, y), one writes f(x)(y).

For every type D there is a fixed point operator fix : [D → D] → D. This allows one to have recursive definitions.

Finally, one has function application and function definition. Function application produces f(x) ∈ E from f ∈ [D → E] and x ∈ D. Function definition is achieved by λ-abstraction. Instead of explicitly defining a function, say, ¬ : B → B by

¬p = if p then false else true,

one defines a nameless function

λp.if p then false else true.

In practice, however, it will not be necessary to explicitly use curried functions, the fixed point operator and λ-abstraction, provided it is clear that our definitions can be easily converted to PCF notation.

All functions definable in PCF are continuous. The same is true for the extensions of PCF considered below.

6.2 Recursive types

PCF extended with recursive types is called FPC (fixed-point calculus). It was introduced by Plotkin [24]—see also [18].

First, one has more type constructors such as cartesian products and sums. Together with cartesian products come the projections D × E → D and D × E → E, which are available as primitive. Similarly for sums.

Second, one can define types by recursion. But instead of writing, say,

D ≅ B × D × D,

one writes

μD. B × D × D

to denote the canonical solution. But, as above, it is not necessary to explicitly use this notation provided it is clear that we know how to convert our definitions to FPC notation.

The primitive operations associated to a recursive type D ≅ FD are the bifree algebra i : FD → D and its inverse i^{−1} : D → FD.

6.3 The programming language Real PCF

Real PCF is PCF extended with ground data types I and R—see [9]. We shall discuss only the extension with I.

The primitive operations are the parallel conditional, the constructors succ_{L}, succ_{R}, and the destructors left, pred_{L}, pred_{R}. Actually, there are more primitive operations. But the additional ones are only needed to define the operational semantics of Real PCF. As we shall see, the ones that we have singled out are enough for our purposes.

Virtually all recursive definitions considered in the previous sections immediately give rise to recursive Real PCF programs, after appropriate conversion to fixed-point operator and λ-abstraction notation.

The ones which consider the type of boolean binary trees discussed in Section 5.3 require a further extension of Real PCF with recursive types, which could be referred to as Real FPC. Alternatively, one could encode the type of boolean binary trees in the function type [N → B], as it is done in [10].

6.4 Universal programming languages

Definition 35 A programming language L is universal if every computable element of the universe of discourse of L is definable in L. □

This depends on a notion of computability in the universe of discourse. In domain theory this is achieved via the notion of an effective presentation (Section 1.5).

Before tackling Real PCF, we recall some basic facts about PCF proved by Plotkin [22]. It is easy too see that all partial recursive functions ℕ^{k} → ℕ are PCF definable via the natural numbers type N. However, simple computable functions such as the parallel conditional and the existential quantification function ∃ : [N → B] → B defined by

∃(p) = \begin{cases}true & if p(n) = true for some n ∈ ℕ, \\ false & if p(⊥) = false, \\ ⊥ & otherwise \end{cases}

fail to be PCF definable. Plotkin showed that if we extend PCF with the parallel conditional then all computable first-order functions become definable, and that if we further extend PCF with the existential quantifier then all computable functions of all orders become definable.

Streicher [36] generalized this result to an extension of PCF with recursive types, parallel-or and the existential quantifier [24], and Escardó [10] generalized it to Real PCF. Here we consider Real PCF extended with recursive types.

It is straightforward to show that there exists an effective presentation of I that makes the primitive constructors and destructors computable. For example, any standard enumeration of the rational basis gives such an effective presentation. But one may wonder if a cleverer choice of an effective presentation would change the induced set of computable elements and functions, and this is indeed the case in general [19]. We show in Section 6.5 below that this is not the case in our situation.

6.5 A characterization of computability over the partial real line

Definition 36 Two effective presentations b and b′ of a domain D are equivalent if they can be reduced to each other, in the sense that the identity id_{D} : D → D is computable both as a map (D, b) → (D, b′) and as map (D, b′) → (D, b). □

(Notice that this is the notion of equivalence of objects in concrete categories discussed in [2], specialized to the category of effectively given domains and computable maps considered as concrete over the category of domains and continuous functions, via the forgetful functor which forgets effective presentations.)

Theorem 37 Any two effective presentations of I which make constr : TI → I and destr : I → TI computable are equivalent.

Proof. Let b′ and b′′ be two such effective presentations, and let I′ and I′′ denote I endowed with b′ and b′′. By Corollary 19, id_{I} : I → I is the unique algebra homomorphism constr → constr, and by Proposition 20, id_{I} is the least fixed point of the functional

F : [I → I] → [I → I]

defined by

F (f) = constr ∘ Tf ∘ destr.

By hypothesis, constr is computable both as a map TI′ → I′ (1′) and as a map TI′′ → I′′ (1′′), and destr is computable both as a map I′ → TI′ (2′) and as a map TI′′ → I′′ (2′′). By (1′′) and (2′) we conclude that F is computable as a map [I′ → I′′] → [I′ → I′′], which shows that id_{I} is computable as a map I′ → I′′. Similarly, by (1′) and (2′′) we conclude that it is also computable as a map I′′ → I′. □

6.6 Universality of Real PCF

We prove that Real PCF extended with recursive types and the existential quantifier is universal by means of the technique introduced in [36].

Here are the main steps of the technique:

(i) Take a universal domain U of PCF, for example [N → B] (see [23]). (ii) Show that for every domain D in the extended language there is a defin-

able retraction

D ⇆_{s_{D}}^{r_{D}} U

with r_{D} ∘ s_{D} = id_{D}. (iii) Given d ∈ D computable, s_{D}(d) ∈ U is computable because s_{D} is com-

putable. (iv) Since PCF extended with parallel-or and ∃ is universal and U is a PCF

domain, s_{D}(d) is definable.

(v) Hence d is definable as d = r_{D}(s_{D}(d)), and r_{D} and s_{D}(d) are definable. (vi) Therefore every computable element is definable.

The crucial step consists in showing that D is a definable retract of U, and this is not so simple in the presence of recursive types. But by the general results of [36], it suffices to show that every ground type is a definable retract of U. This has been done for the PCF ground types, so that we only need to do it for our new ground type I.

Theorem 38 Real PCF extended with recursive types and ∃ : [N → B] → B] is a universal programming language.

Notice that Real PCF includes a parallel conditional.

Proof. By Section 5.3, we know that num : mktree → constr and bin : destr → mktree^{−1} form a retraction with num ∘ bin = id_{I}. Since BTree is a recursive type, and since num and bin are recursively definable from constr, destr, mktree and mktree^{−1} by Proposition 20, we see that I is a definable retract of BTree. But we already know that BTree is a definable retract of U. Since definable retracts compose, I is a definable retract of U. □

This general result does not tell the full story about definability of computable first order functions (over the partial unit interval). By means of a more direct method of proof similar to that of [22], in [11] it is shown that the existential quantifier is not needed to obtain the definability result at first-order types.

Conclusions

We have defined and studied inductive retractions. We have shown that they correspond to well-behaved quotients of bifree algebras, referred to as biquotients. We have applied this notion exclusively to the study of the partial real line and its recursion schemes and induction principles.

It might be worthwhile to look at other applications of this notion. Typically one would like to have a characterization of those (in)equational theories E over a signature Σ [1] such that the quotient of T_{∞}(Σ) by E is a biquotient. This might be interesting especially for the case of stream domains extending the work on partially commutative monoids in trace theory towards infinite behaviours.

Acknowledgements

The first named author was supported by the Brazilian agency CNPq, an EPSRC project “Programming Languages for Real Number Computation: Theory and Implementation”, and an ARC project “A Computational Approach to Measure and Integration Theory”.

References

[1] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D.M. Gabbay, and T.S.E Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1–168. Clarendon Press, Oxford, 1994.

[2] J. Adamek, H. Herrlich, and G.E. Strecker. Abstract and Concrete Categories. John Wiley & Sons Inc., 1990.

[3] R. Bird and P. Wadler. Introduction to Functional Programming. Prentice-Hall, New York, 1988.

[4] A. Edalat and M.H. Escardó. Integration in Real PCF (extended abstract). In Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 382–393, New Brunswick, New Jersey, USA, July 1996.

[5] A. Edalat and Ph. Sünderhauf. A domain-theoretic approach to computability on the real line. This volume.

[6] H. Egli and R.L. Constable. Computability concepts for programming languages. Theoretical Computer Science, 2:133–145, 1976.

[7] M.H. Escardó. Properly injective spaces and function spaces. Topology and its Applications. To appear.

[8] M.H. Escardó. Induction and recursion on the real line. In C. Hankin, I. Mackie, and R. Nagarajan, editors, Theory and Formal Methods 1994: Proceedings of the Second Imperial College Department of Computing Workshop on Theory and Formal Methods, pages 259–282, Mller Centre, Cambridge, 11–14 September 1994. IC Press. 1995.

[9] M.H. Escardó. PCF extended with real numbers. Theoretical Computer Science, 162(1):79–115, August 1996.

[10] M.H. Escardó. Real PCF extended with ∃ is universal. In A. Edalat, S. Jourdan, and G. McCusker, editors, Advances in Theory and Formal Methods of Computing: Proceedings of the Third Imperial College Workshop, April 1996, pages 13–24, Christ Church, Oxford, 1996. IC Press.

[11] M.H. Escardó. PCF extended with real numbers: A domain-theoretic approach to higher-order exact real number computation. Technical Report ECS-LFCS-97-374, Department of Computer Science, University of Edinburgh, 1997. PhD thesis, Imperial College of the University of London, 1997.

[12] M.H. Escardó and T. Streicher. Induction and recursion on the partial real line via biquotients of bifree algebras (extended abstract). In Proceedings of the Twelveth Annual IEEE Symposium on Logic in Computer Science, Warsaw, Polland, June 1997.

[13] M.P. Fiore. A coinduction principle for recursive data types based on bisimulation. Information and Computation, 127(2):186–198, 1996.

[14] P. J. Freyd. Algebraically complete categories. Lecture Notes in Mathematics, 1488:95–104, 1991.

[15] P. J. Freyd. Remarks on algebraically compact categories. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Applications of Categories in Computer Science: Proceedings of the LMS Symposium, Durham, 1991. Cambridge University Press, 1992. LMS Lecture Notes Series, 177.

[16] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, New York, 1980.

[17] Michael J. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF. Springer-Verlag LNCS 78, 1979.

[18] C. A. Gunter. Semantics of Programming Languages – Structures and Techniques. The MIT Press, London, 1992.

[19] A. Kanda and D. Park. When are two effectively given domains identical? In K. Weihrauch, editor, Theoretical Computer Science 4^{th} GI Conference, LNCS, 1979.

[20] D.J. Lehmann and M.B. Smyth. Algebraic specification of data types: a synthetic approach. Math. Syst. Theory, 14:97–139, 1981.

[21] R.E. Moore. Interval Analysis. Prentice-Hall, Englewood Cliffs, 1966.

[22] G. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(1):223–255, 1977.

[23] G. Plotkin. B^{ω} as a universal domain. Journal of Computer and System Sciences, 17:209–236, 1978.

[24] G. Plotkin. Domains. Post-graduate Lectures in advanced domain theory, University of Edinburgh, Department of Computer Science. http:// ida.dcs.qmw.ac.uk/ sites/ other/ domain.notes.other, 1980.

[25] A. Poigné. Basic category theory. In S. Abramsky, D.M. Gabbay, and T.S.E Maibaum, editors, Handbook of Logic in Computer Science, volume 1, pages 413–640. Clarendon Press, Oxford, 1992.

[26] H.L. Royden. Real Analysis. Collier Macmillan Publishing, third edition, 1988.

[27] D. S. Scott. Continuous lattices. In F.W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lectures Notes in Mathematics, pages 97– 136. Springer-Verlag, 1972.

[28] D. S. Scott. Lattice theory, data types and semantics. In Formal semantics of programming languages, pages 66–106, Englewood Cliffs, 1972. Prentice-Hall.

[29] D. S. Scott. A type-theoretical alternative to CUCH, ISWIM and OWHY. Theoretical Computer Science, 121:411–440, 1993. Reprint of a manuscript produced in 1969.

[30] M.B. Smyth. Effectively given domains. Theoretical Computer Science, 5(1):256–274, 1977.

[31] M.B. Smyth. Power domains and predicate transformers: a topological view. In J. Diaz, editor, Automata, Languages and Programming, pages 662–675. Springer-Verlag, 1983. LNCS 154.

[32] M.B. Smyth. I-categories and duality. In M.P. Fourman, P.T. Johnstone, and Pitts A.M., editors, Applications of Categories in Computer Science, pages 270–287, Cambridge, 1992. Cambridge University Press. London Mathematical Society Lecture Notes Series 177.

[33] M.B. Smyth. Topology. In S. Abramsky, D. M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 1, pages 641–761. Clarendon Press, Oxford, 1992.

[34] M.B. Smyth and G. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal of Computing, 11(4):761–783, 1982.

[35] R. Stoll. Set Theory and Logic. W.H. Freeman and Company, San Fransisco, 1966.

[36] T. Streicher. A universality theorem for PCF with recursive types, parallel-or and ∃. Mathematical Structures for Computing Science, 4(1):111 – 115, 1994.