Induction and recursion on the partial real line via biquotients of bifree algebras

Martín Hötzel Escardó Department of Computing

Imperial College 180 Queen’s Gate

London SW7 2BZ, United Kingdom m.escardo@doc.ic.ac.uk

Thomas Streicher Fachbereich Mathematik

Technische Hochschule Darmstadt

Schloßgartenstraße 7 64289 Darmstadt, Germany

streicher@mathematik.th-darmstadt.de

Abstract

The partial real line is the continuous domain of compact real intervals ordered by reverse inclusion. The idea is that singleton intervals represent total real numbers, and that the remaining intervals represent partial real numbers. The partial real line has been used to model exact real number computation in the framework of 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. The theory is based on a domain-equation-like presentation of the partial unit interval, which we refer to as a biquotient of a bifree algebra.

1. Introduction

The partial real line is the continuous domain of compact real intervals ordered by reverse inclusion [20]. 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. Moreover, the Lawson topology on the partial real line coincides with the Hausdorff topology considered in interval analysis [15], as it is shown in [9].

The partial real line has been used to model exact real number computation in the framework of the programming language Real PCF [6, 8], including computation of integrals [3].

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, and 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 linear 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.

Preliminary ideas on recursion and induction on the real line appeared in [5], which considers uniform spaces. Our axioms are formulated in the ambient category of continuous Scott domains [1].

In domain theory one usually derives induction principles and recursion schemes from canonical solutions of domain equations [14, 24, 18]. Since the partial real line is not algebraic, it is not the canonical solution of any domain equation involving usual functors.

We establish new results about the notion of inductive retraction introduced in [8], which generalizes canonical solutions of domain equations by means of ideas similar to those of Freyd [11, 12]. 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 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 [26] to establish universality of Real PCF extended with a certain computable existential quantifier [8].

2. The partial unit interval

In this paper a domain is a bounded complete continuous dcpo with bottom [1]. The domain I = I[0, 1] of closed subintervals of the unit interval 𝕀 = [0, 1], ordered by reverse inclusion, is referred to as the partial unit interval. The elements of I 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.

Any continuous function f : 𝕀 → 𝕀 has a Scott continuous canonical extension If : I → I defined by If(x) = {f(r)|r ∈ x}. If f is increasing w.r.t. to the natural order of real numbers then If(x) = [f(inf x), f(sup x)]. A function f : 𝕀 → 𝕀 is notationally identified with its canonical extension If : I → I, and we often define a function f : I → I by first defining a function f : 𝕀 → 𝕀 and then implicitly taking its canonical extension.

3. Peano-like axioms for the partial unit interval

Full proofs of the result of this section can be found in [7]. Define cons_{L}, cons_{R} : I → I by

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

That is, cons_{L} and cons_{R} are the unique increasing affine maps such that

cons_{L}(⊥) = L cons_{R}(⊥) = R,

where L = [0, 1/2] and R = [1/2, 1].

In this section we consider cons_{L} and cons_{R} as partial real number “constructors”, in a similar fashion as zero and successor are considered as natural number constructors. An important difference is that the natural numbers together with zero and successor form a free algebra, whereas I together with cons_{L} and cons_{R} will form a kind of quotient of a free algebra with respect to some equations. The main such equation is

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

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

x = \begin{matrix}⨆ & ↑ \\ n \end{matrix} cons_{a_{1}} ∘ ⋯ ∘ cons_{a_{n}}(⊥)

for some sequence a_{i} ∈ {L, R} corresponding to a binary expansion of x. Partial real numbers are constructed by iterating cons_{L} and cons_{R} in a more elaborate way, as it is shown in §5.2.

The predecessor function, undefined or arbitrarily defined at zero, is a left inverse of the successor function. Similarly, cons_{a} has a left inverse tail_{a} defined by

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

The fact that every 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, define head : I → B by

head(x) = \begin{cases}tt & if sup x < 1/2, \\ ff & if inf x > 1/2, \\ ⊥ & otherwise \end{cases}

and the parallel conditional by

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

Lemma 3.1 (Elementary axioms)

tail_{L}(cons_{L}(x)) = x
tail_{L}(cons_{R}(y)) = 1
tail_{L}(cons_{L}(x) ⊓ cons_{R}(y)) = x ⊓ 1
tail_{R}(cons_{L}(x)) = 0
tail_{R}(cons_{R}(y)) = y
tail_{R}(cons_{L}(x) ⊓ cons_{R}(y)) = 0 ⊓ y
head(cons_{L}(x)) ⊑ tt
head(cons_{L}(x)) = ⊥ iff x ⊑ 1
head(cons_{R}(y)) ⊑ ff
head(cons_{R}(y)) = ⊥ iff y ⊑ 0

x = pif head(x)

then cons_{L}(tail_{L}(x)) else cons_{R}(tail_{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 I equipped with cons_{L} and cons_{R}, but we have to take into account the equation cons_{L}(1) = cons_{R}(0).

Lemma 3.2 (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(cons_{L}(x)) = g_{L}(x)
f(cons_{R}(y)) = g_{R}(y)
f(cons_{L}(x) ⊓ cons_{R}(y)) = g_{L}(x) ⊓ g_{R}(y)
if x ⊑ 1 and y ⊑ 0,

namely the function f defined by

f(x) = pif head(x)
then g_{L}(tail_{L}(x)) else g_{R}(tail_{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 cons_{L} and cons_{R}.

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

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

1. (Base case) ⊥ ∈ A.

2. (Inductive step) x ∈ A and y ∈ A imply

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

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

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

Then A = I.

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 cons_{L} and cons_{L}. We first need a lemma:

Lemma 3.4 (Dyadic recursion) 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 head(x)

then g_{L}(f(tail_{L}(x))) else g_{R}(f(tail_{R}(x))).

Then the following statements hold:

1. f(0), f(1) and f(⊥) are fixed points of g_{L}, g_{R} and g_{L} ⊓ g_{R} respectively.

2. f is uniquely determined by the values that it assumes at 0, 1, and ⊥.

3. f is the least 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 f is the unique solution.

Lemma 3.5 (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(cons_{L}(x)) = g_{L}(f(x))
f(cons_{R}(y)) = g_{R}(f(y))
f(cons_{R}(x) ⊓ cons_{R}(y)) = g_{L}(f(x)) ⊓ g_{R}(f(y))
if x ⊑ 1 and y ⊑ 0,

namely the least continuous solution to the equation of Lemma 3.4.

Finally, the set of natural numbers 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 [25], 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 cons_{L} and cons_{R} respectively.

Definition 3.6 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} and 1 =^{def} fix a_{R}.

We also impose the technical condition fix (a_{L} ⊓ a_{R}) = ⊥, which ensures that homomorphisms defined below, as Lemma 3.5 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 [5]. Lemma 3.5 can be formulated as

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

Compare the following lemma to Lemmas 3.1 and 3.2, where c_{L}, c_{R}, h, t_{L}, t_{R} play the rôle of cons_{L}, cons_{R}, head, tail_{L}, and tail_{R} respectively:

Lemma 3.8 Let D = (D, c_{L}, c_{R}) be a binary system. Then there is at most one triple of continuous maps h : D → B and t_{L}, t_{R} : D → D such that

t_{L}(c_{L}(x)) = x
t_{L}(c_{R}(y)) = 1
t_{L}(c_{L}(x) ⊓ c_{R}(y)) = x ⊓ 1
t_{R}(c_{L}(x)) = 0
t_{R}(c_{R}(y)) = y
t_{R}(c_{L}(x) ⊓ c_{R}(y)) = 0 ⊓ y
h(c_{L}(x)) ⊑ tt
h(c_{L}(x)) = ⊥ iff x ⊑ 1
h(c_{R}(y)) ⊑ ff
h(c_{R}(y)) = ⊥ iff y ⊑ 0

x = pif h(x) then c_{L}(t_{L}(x)) else c_{R}(t_{R}(x)).

Definition 3.9 If such maps exist then they are called the destructors of (D, c_{L}, c_{R}). □

Definition 3.10 A binary system (D, c_{L}, c_{R}) satisfies the dyadic induction principle if for any inductive set A ⊆ D the conditions

1. (Base case) ⊥ ∈ A,

2. (Inductive step) x ∈ A and y ∈ A imply

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

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

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

together entail that A = D. □

Definition 3.11 A binary system (D, c_{L}, c_{R}) is inductive if

1. 0 and 1 are the unique fixed points of c_{L} and c_{R}.

2. 0 ≠ 1 and 0 ⊓ 1 = ⊥.

3. It has destructors.

4. It satisfies the dyadic induction principle. □

The following theorem axiomatically characterizes the binary system (I, cons_{L}, cons_{R}) up to isomorphism, without explicit reference to real numbers or intervals.

Theorem 3.12 A binary system is inductive iff it is initial. In particular, any two inductive binary systems are isomorphic.

4. Bifree algebras generalized

In this section we introduce a new technique for defining structural recursion schemes based on the theory of domain equations. The basic idea is to consider not a distinguished domain D such that D ≅ FD, but instead a domain D such that D is a retract of FD in a special way. We refer to such a domain D as an F-inductive retract. It turns out that Finductive retracts generalize special F-invariant objects in the sense of Freyd [11, 12]. We therefore could have adopted the (rather long) terminology special semi-invariant object.

4.1. Inductive retractions

In the remaining of this section X is any category and F is an endofunctor of X.

We first recall a concept due to Freyd [12]:

Definition 4.1 A bifree F-algebra is an initial algebra i : FC → C such that its inverse i^{−1} : C → FC is a final coalgebra. □

Definition 4.2 An F-inductive retraction is a pair of arrows

X ⇆_{β}^{α} FX

such that f = α ∘ Ff ∘ β iff f = id_{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 X^{op}.

The following proposition shows that inductive retractions generalize bifree algebras:

Proposition 4.3 Let β : X ⇆ FX : α be an Finductive 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}. □

In the remaining of this section, i : FC → C is a bifree algebra and β : X ⇆ FX : α is an F-inductive retraction.

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

Lemma 4.4 If r : i → α and s : β → i^{−1} are the unique (co)algebra homomorphisms then s : X ⇆ C : r is a retraction with r ∘ s = id_{X}.

4.2. Structural recursion

Proposition 4.5 Let r : i → α, s : β → i^{−1}, e = s ∘ r : C → C, h : i → a, and k : b → i^{−1}.

1. For any algebra a : FA → A, there is a homomorphism f : α → a iff h = h ∘ e, and in this case f = h ∘ s.

2. For any coalgebra b : B → FB, there is a homomorphism g : b → β iff k = e ∘ k, and in this case g = r ∘ k.

Proof (1): 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. (2): Dual to (1). □

Roughly, condition (1) 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 (2) 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 4.6

1. For any algebra a : FA → A there is at most one homomorphism f : α → a.

2. For any 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 4.7 Let F : SDom → SDom be locally continuous.

1. If there is a homomorphism f : α → a for a given algebra a : FA → A then it is the least f′ : X → A such that f′ = a ∘ Ff′ ∘ β.

2. If there is a homomorphism g : b → β for a given coalgebra b : B → FB then it is the least g′ : B → X such that g′ = α ∘ Fg′ ∘ b.

Proof (1): The least solution of the above 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.

(2): Dual to (1). □ Thus, in order to find a recursive definition of a function f : X → A we can try to find an algebra 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 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.3. 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}. We now 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 [1]. But notice that we are still working in an arbitrary category X.

Definition 4.8 Let e : C → C be an idempotent and define

C ⇆_{b}^{a} 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:

(i) e : i → a

(ii) e : b → i^{−1}

(iii) h = a ∘ Fh ∘ b iff h = e. □

Theorem 4.9

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

2. 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 (1): Conditions (i) and (ii) 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 get immediately that

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

For the other implication of condition (iii), 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 Finductive retract. 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 ∘ β = β.

(2): 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. Structural recursion on the partial unit interval

In order to obtain an inductive retraction for the partial unit interval, we put the real number constructors (resp. destructors) together. Define T : SDom → SDom by

TD = B × D × D,

and define I ⇆_{destr}^{cons} TI by

cons = pif ∘ (id × cons_{L} × cons_{R}),
destr = ⟨head, tail_{L}, tail_{R}⟩.

Theorem 5.1 cons and destr form a T-inductive retraction.

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

f(x) = pif head(x)
then cons_{L}(f(tail_{L}(x)))
else cons_{R}(f(tail_{R}(x))).

By Lemma 3.1, f = id is a solution. But cons_{L} and cons_{R} and cons_{R} ⊓ cons_{L} have unique fixed-points. Therefore f = id is the unique solution by virtue of Lemma 3.4. □

5.1. Binary T-algebras

We now relate the algebra cons : TI → I to the binary system (I, cons_{L}, cons_{R}).

Definition 5.2 A binary T-algebra is a T-algebra a : TD → D of the form

pif ∘ (id × a_{L} × a_{R})

for (necessarily unique) a_{L}, a_{R} : D → D. □

Compare the following proposition to Lemma 3.5 and Definition 3.6:

Proposition 5.3 Let a : TD → D be a binary Talgebra. Then a strict continuous map f : I → D is a homomorphism from cons to a iff

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

Compare the following proposition to Lemmas 3.4 and 3.5:

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

f(x) = pif head(x)

then a_{L}(f(tail_{L}(x)) else a_{R}(f(tail_{R}(x)).

Proof By Proposition 4.7 we know that if there is a homomorphism from cons to a, then it is the least continuous function f such that

f = a ∘ Tf ∘ destr,

which is equivalent to the above equation. □

5.2. 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 : TBTree → BTree

which maps a list ⟨p, s, t⟩ to the tree with root labeled by p and with left and right subtrees s and t respectively [18]. Let

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

be the unique (co)algebra homomorphisms. By Lemma 4.4, num ∘ bin = id, so that I is a retract of BTree. The tree bin (x) is referred to as the bifurcated binary expansion of the partial number x in [7].

5.3. 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, we have a coinduction principle related to the ideas of Smyth [23] and Fiore [10].

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

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

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

Theorem 5.6 (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). Therefore x = y because bin is split mono. □

5.4. Examples

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

compl(x) = pif head(x)

then cons_{R}(compl(tail_{L}(x))) else cons_{L}(compl(tail_{R}(x))).

Proof This follows from Proposition 5.4, because compl is an algebra homomorphism from cons to pif ∘ (id × cons_{R} × cons_{L}). □

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

exp(x) = pif head(x)
then \sqrt{exp(tail_{L}(x))}
else \sqrt{2 exp(tail_{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 an algebra homomorphism from cons to pif ∘ (id × a_{L} × a_{R}), and the result again follows from Proposition 5.4. □ More examples can be found in [6, 7], and a recursive definition of Riemann integration can be found in [3].

6. Applications to Real PCF

Real PCF [6] is an extension of PCF [21, 16] with a ground type for the partial real line and some primitive functions, which include the real number constructors and destructors discussed in Section 3. The remaining primitives are necessary to obtain the operational semantics of Real PCF, but they are not needed to obtain the results discussed below, so that we don’t pause to introduce them. For simplicity, we only discuss the partial unit interval. A treatment of the partial real line can be found in [7].

Definition 6.1 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 effective presentation (see [4, 18] for the algebraic case and [22] for the general continuous case).

Before tackling Real PCF, we recall some basic facts about PCF proved by Plotkin [16]. It is easy too see that all partial recursive functions [19] are PCF definable. However, simple computable functions such as the parallel conditional and an existential quantifier ∃ : [N → B] → B 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 [26] generalized this result to an extension of PCF with recursive types, parallel-or and ∃ [18], and Escardó [8] generalized it to Real PCF. We now briefly consider Real PCF extended with recursive types.

It is straightforward to show that there exists an effective presentation of the partial real line which makes the primitive constructors and destructors computable; for example, any standard enumeration of the rational basis gives such an effective presentation. Let’s fix any such effective presentation and call it the standard effective presentation. One then 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 [13]. We show in Section 6.1 below that this is not the case in our application.

6.1. Absoluteness of the standard effective presentation

Definition 6.2 Two effective presentations b and b′ of a domain D are equivalent if 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 6.3 Any two effective presentations of I which make cons : 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 4.6, id_{I} : I → I is the unique algebra homomorphism cons → cons, and by Proposition 4.7, id_{I} is the least fixed point of functional

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

defined by

F (f) = cons ∘ Tf ∘ destr.

By hypothesis, cons is computable both as as map (1′) TI′ → I′ and as a map (1′′) TI′′ → I′′, and destr is computable both as a map (2′) I′ → TI′ and as a map (2′′) TI′′ → I′′. 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.2. Universality of Real PCF

We prove that Real PCF extended recursive types and ∃ is computationally complete by means of the technique introduced in [26]. Here are the main steps of the technique:

1. Take a universal domain U of PCF, for example [N → B] (see [17]).

2. Show that for every domain D in the extended language there is a definable retraction

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

with r_{D} ∘ s_{D} = id_{D}.

3. Given d ∈ D computable, s_{D}(d) ∈ U is computable because s_{D} is computable.

4. Since PCF extended with parallel-or and ∃ is universal and U is a PCF domain, s_{D}(d) is definable.

5. Hence d is definable as d = r_{D}(s_{D}(d)), and r_{D} and s_{D}(d) are definable.

6. 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 [26], 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.

Theorem 6.4 Real PCF extended with recursive types, the parallel conditional and ∃ is a universal programming laguage.

Proof By Section 5.2, we know that

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

form a retraction with num ∘bin = id_{I}. Since BTree is a recursive type, and since num and bin are definable, 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 real interval I). By means of a more direct method of proof similar to that of [16], in [7] it is shown that the existential quantifier is not needed to obtain the definability result at first-order types.

7. Conclusions

We have studied a notion of the most well-behaved quotients of bifree algebras, namely the so-called biquotients. We have applied this notion exclusively to the study of the partial real line and its recursion and induction principles.

It might be worthwhile to look at other applications of this notion. Typically one would like to have a characterisation of those equational theories E over a signature Σ 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.

8. Acknowledgements

The first 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] 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, New Brunswick, New Jersey, USA, July 1996.

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

[5] 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, Møller Centre, Cambridge, 11–14 September 1994. IC Press. 1995.

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

[7] M.H. Escardó. PCF extended with real numbers: A domain-theoretic approach to higher-order exact real number computation. PhD thesis, Imperial College, Department of Computing, November 1996.

[8] M.H. Escardó. Real PCF extended with ∃ is universal. In A. Edalat, S. Jourdan, and G. Mc-Cusker, 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.

[9] M.H. Escardó and D.M. Claudio. Scott domain theory as a foundation for interval analysis. Technical Report 218, UFRGS/II, Porto Alegre, Brazil, 1993.

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

[11] P. J. Freyd. Algebraically complete categories. In A. Carboni et al., editors, Proc. 1990 Como Category Theory Conference, pages 95–104, Berlin, 1991. Springer-Verlag. Lecture Notes in Mathematics Vol. 1488.

[12] 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.

[13] 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.

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

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

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

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

[18] 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.

[19] H. Rogers. Theory of Recursive Functions and Effective Computability. McGraw-Hill, New York, 1967.

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

[21] 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.

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

[23] 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.

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

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

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