A Data Type of Partial Recursive Functions in Martin-Löf Type Theory

Anton Setzer^{∗}

November 12, 2006

Abstract

In this article we investigate how to represent partial recursive functions in Martin-Löf’s type theory. Our representation will be based on the approach by Bove and Capretta, which makes use of indexed inductive-recursive definitions (IIRD). We will show how to restrict the IIRD used so that we obtain directly executable partial recursive functions, Then we introduce a data type of partial recursive functions. We show how to evaluate elements of this data type inside Martin-Löf’s type theory, and that therefore the functions defined by this data type are in fact partial recursive. The data type formulates a very general schema for defining functions recursively in dependent type theory. The initial version of this data type, for which we introduce an induction principle, needs to be expanded, in order to obtain closure under composition. We will obtain two versions of this expanded data type, and prove that they define the same set of partial recursive functions. Both versions will be large types. Next we prove a Kleene-style normal form theorem. Using it we will show how to obtain a data type of partial recursive functions which is a small set. Finally, we show how to define self-evaluation as a partial recursive function. We obtain a version of this evaluation function, which not only computes recursively a result, but as well a proof that the result is correct.

Keywords: Martin-Löf type theory, computability theory, recursion theory, Kleene index, Kleene brackets, Kleene’s normal form theorem, partial recursive functions, inductive-recursive definitions, indexed induction-recursion, self-evaluation.

1 Introduction

A problem when developing computability theory in Martin-Löf type theory is that the function types only contain total functions, therefore partial recursive functions are not first class objects. One approach to overcome this problem has been taken by Bove and Capretta (e.g. [BC05a, BC05b]), who have shown how to represent partial recursive functions by indexed inductive-recursive definitions (IIRD), and in this article we will investigate their approach. In order to illustrate it, we make use of a toy example. We choose a notation which is closer to that used in computability theory. Assume the partial recursive function f : ℕ ⇀ ℕ defined by

f(0) :≃ 0 ,  f(n + 1) :≃ f(f(n)) .

∗Dept. of Computer Science, University of Wales Swansea,Singleton Park, Swansea SA2 8PP, UK. Tel.: +44 1792 513368, Fax: +44 1792 295651, Email: a.g.setzer@swan.ac.uk, webpage: http://www.cs.swan.ac.uk/∼csetzer/. This research was supported by EPSRC grant GR/S30450/01. Part of this work was done while the author was an invited research follow at the Graduate School of Science and Technology, Kobe University, Japan.

This function is constantly zero, but we want to represent it directly in Martin-Löf type theory, so that we can prove for instance, that it is in fact constantly zero. In order to do this, Bove and Capretta introduce

f(·)↓ : ℕ → Set ,  f(·)[·] : (n : ℕ, p : f(n)↓) → ℕ .

Here f(n)↓ expresses that f(n) is defined, and f(n)[p] computes, depending on n : ℕ and a proof p : f(n)↓, the value of f(n). In the literature, f(·)↓ is often referred to as the accessibility predicate for f. If we define for arguments a, b of f that a ≺ b if and only if the call of f(b) recursively calls f(a), then f(a)↓ if and only if a is in the accessible part of ≺. The approach by Bove/Capretta can be seen as a general method of determining the accessible part of ≺ for a large class of recursively defined functions. If we take the definition of f as it stands, we see that the definitions of f(·)↓ and f(·)[·] refer to each other. f(·)↓ has two constructors defined_{f}^{0}, defined_{f}^{S} corresponding to the two rewrite rules, and we obtain the following introduction and equality rules:

defined_{f}^{0} : f(0)↓ ,  f(0)[defined_{f}^{0}] = 0 ,
defined_{f}^{S} : (n : ℕ, p : f(n)↓, q : f(f(n)[p])↓) → f(n + 1)↓ ,
f(n + 1)[defined_{f}^{S}(n, p, q)] = f(f(n)[p])[q] .

The constructor defined_{f}^{S} has arguments n : ℕ, p : f(n)↓, and if f(n) ≃ m, a proof q : f(m)↓. Then p′ := defined_{f}^{S}(n, p, q) proves f(n + 1)↓ and we have f(n + 1)[p′] = f(m)[q]. We observe that defined_{f}^{S} refers to f(n)[p], so we have to define simultaneously f(·)↓ inductively, while defining f(·)[·] recursively. This is an instance of an IIRD, as introduced by Dybjer [Dyb00, Dyb94]. We will see below that such kind of IIRD can be reduced to inductive definitions. Bove and Capretta face the problem that they cannot define a data type of partial recursive functions (unless using impredicative type theory) and therefore cannot deal with partial recursive functions depending on other partial recursive functions as an argument. A simple example would be to define depending on a partial recursive function f : ℕ ⇀ ℕ (e.g. f as above)

g : List(ℕ) ⇀ List(ℕ) ,  g(l) :≃ map(f, l) .

Here map(f, [n_{0}, …, n_{k}]) :≃ [f(n_{0}), …, f(n_{k})]. In order to define the above directly, we need to define map, depending on an arbitrary partial recursive function f. More complex examples of this kind are discussed in [BC05a]. In this article we will show how to overcome this restriction by introducing a data type of partial recursive functions. This will be based on the closed formulation of IIRD, as developed by P. Dybjer and the author. In order to obtain that all functions represented by an IIRD correspond directly to a partial recursive function, without using search functions, we will impose restrictions on the set of IIRD used. The data type given in this article will define exactly those restricted IIRD. We will then show that the functions given by those indices are all partial recursive, and that they are closed under the standard constructions for defining partial recursive functions, and under the total functions.

Overview. We start by introducing in Sect. 2 our basic notations and type theoretic assumptions. Then we review briefly in Sect. 3 indexed inductive-recursive definitions (IIRD), and show, which restrictions need to be applied in order to obtain IIRD which correspond to directly executable partial recursive functions. In Sect. 4 we formalise a data type of IIRD consisting of all those IIRD which are restricted in the sense of the previous section. In order to prove properties of this data type and to introduce transformations, we need an induction principle, which will be introduced in Sect. 5. In Sect. 6 we show how to compute recursively the functions obtained by this data type inside type theory. This shows that the partial recursive functions are in fact directly executable. In Sect. 7 we prove that this direct execution obtains the correct result. Sect. 8 is a slightly more technical section, in which we prove that we can replace, when computing a partial recursive function for a given argument, recursive references to the function by a reference to a finite approximation of it. In Sect. 9 we show how to combine several partial recursive functions into one. The combination will be called the sum of those functions. In Sect. 10 we investigate the problem that our data type is not closed under reference to other partial recursive functions. We will show two alternative solutions for overcoming this problem, the data types Rec_{0}^{+} and Rec_{1}^{+}. Rec_{0}^{+} can be obtained directly from Rec, while Rec_{1}^{+} involves an induction definition which forms true types. The advantage of Rec_{1}^{+} is that it will be much easier to define recursive functions in it. In order to get the advantages of both, we show in Sect. 11, that both data types define the same set of partial recursive functions. In Sect. 12 we will prove that the partial recursive functions definable in Rec_{0}^{+} and Rec_{1}^{+} are closed under the standard operations for forming partial recursive functions, including closure under total functions. We will show as well that for every index e for a partial recursive function we can introduce an index e′ for another partial recursive functions, which not only computes the same result, but as well a proof that this result is correct. In the final Sect. 13 we show a Kleene style normal form function, namely that every function can be evaluated by finding the least n s.t. a certain total function returns the Boolean value true, and then computing from it by using another total function the result. Using this observation we obtain another data type of partial recursive function Rec_{2}^{+}, which is equivalent to Rec_{0}^{+} and Rec_{1}^{+}, but a small set. We show then how to evaluate elements of Rec_{2}^{+} inside Rec_{2}^{+} itself. We introduce as well a variant of this self-evaluation function, which as well computes a proof that the result is correct. We finish with some concluding remarks (Sect. 14).

Related Work Martin-Löf has suggested to add an itertion type Ω to type theory plus an element ω : Ω, which is a fixed point of the successor function. This type theory has been studied intensively by Palmgren and Stoltenberg-Hansen in [PSH90, PSH92, Pal91]. The problem of this approach is that the resulting type theory is inconsistent, and can therefore be only be used as a programming language, but no longer as a system for proving theorems. Various researchers, e.g. Paulson [Pau93] and Nordström [Nor88], have used accessibility predicates in order to deal with partial functions. However these approaches do not lead to a Turing complete data type of partial recursive functions. Constable and Scott Smith [Con83, CS87] have developed an approach in which they have a type theory with both partial and total types. This is a very elaborate approach, which is implemented in NuPrl, but requires a substantial modification of the underlying type theory. Geuvers, Poll and Zwanenburg studied the addition of the Y-combinator to the type theory and prove a conservativity result. However, their approach is limited, since the result applies only to proofs which can be converted into proofs not using Y – this excludes proofs which reasoning about partial functions in general. The current article is heavily based on the approach by Bove and Capretta [BC05a, BC05b, Bov02a, Bov02b]. Capretta [Cap05] has recently proposed the use of the delay monad in order to represent partial objects. This seems to be a very interesting approach, but requires the extension of type theory by coinductive data types. There are many more approaches. Excellent overviews over the literature can be found in [Cap05, BC05a].

2 Notations and Type theoretic assumptions

2.1 Type Theoretic Assumptions

Definition 2.1 (Basic Logic Notations) (a) We use a[x_{1} := b_{1}, …, x_{n} := b_{n}] for the result of simultaneously substituting in a the variable x_{i} by b_{i} (i = 1, …, n).

(b) Often arguments of functions will be written as subscripts. How to write those arguments will be clear from its use.

(c) We will frequently overload notations, i.e. use the same notation for different operations. This overloading can always be resolved by the reader. When formally carrying out proofs in type theory, one would need to use different notations for the overloaded variants of a notation.

(d) We will often omit parameters, which can be inferred from the context. When working formally in type theory, those parameters need to be reintroduced. When writing them as indices, they will usually simply be omitted, otherwise we sometimes use for a suppressed parameter.

Assumption 2.2 (Type Theoretic Assumptions) (a) We work in extensional type theory. We assume however that many theorems can be, possibly with some restrictions, shown in intensional type theory as well.

(b) We assume the logical framework. So we have a collection of small types called Set and a collection of large types called Type. We have Set : Type and if A : Set then A : Type. Both Set and Type will be closed under the dependent function type (Π) and the dependent product (Σ) of the logical framework.

(c) We do not distinguish in this article between the logical framework dependent function type and product and the set constructions Π and Σ. All of them will be equipped with the η-rule.

Definition 2.3 (Basic Type Theoretic Notations) (a) We usually write (x : A) → B for the dependent function type, which in type theory is often denoted by Πx : A.B. (x : A, y : B) → C := (x : A) → (y : B) → C, (x : A, B) → C := (x : A, y : B) → C for some fresh y. Related abbreviations are to be understood in the same way.

(b) We write Σx : A.B for the dependent sum type, which is sometimes denoted by (x : A) × B.

(c) We use ∀x : A.B and (x : A) → B as two notations for the same type, where ∀x : A.B is used when considering it as a proposition, and (x : A) → B is used when considering it as a data type.

Similarly Σx : A.B and ∃x : A.B denote the same objects.

(d) A × B and A ∧ B are two notations for Σx : A.B, where B does not depend on x.

(e) The canonical elements of Σx : A.B are denoted by ⟨a, b⟩. We write for elements of iterated Σ-types Σa : A.Σb : B(a).C(a, b) short ⟨a, b, c⟩ for ⟨a, ⟨b, c⟩⟩, similarly for longer sequences.

(f) Assume I : Set, A : I → Set written as A_{i} for A(i).

(i) When we want to stress that Σi : I.A_{i} is the disjoint union of (A_{i})_{i:I}, we write sometimes Σ_{i:I}A_{i} for Σi : I.A_{i}.

(ii) For i : I, a : A_{i}, let in_{i}(a) := ⟨i, a⟩, when considering it as the injection of a into Σ_{i:I}A_{i}.

(g) We write π_{0}(a) and π_{1}(a) for the first and second projection of an element a : (Σx : A.B).

(h) We write λ⟨a, b⟩.r for λx.r[a := π_{0}(x), b := π_{1}(x)] for some fresh x. Similar notations (e.g. λ⟨a, b, c⟩.r, Σ⟨a, b⟩ : A.B etc.) are to be understood in the same way.

(i) We write application as in mathematics, not in functional style. So f applied to a is written as f(a). f(a_{1}, …, a_{n}) = f(a_{1})(a_{2}) ⋯ (a_{n}). Sometimes, we identify a function f : (⟨a, b⟩ : Σa : A.B(a)) → C(a, b) with it’s Curried form λa, b.f(⟨a, b⟩) : (a : A, b : B(a)) → C(a, b). Then f(a, b) stands for f(⟨a, b⟩). Whether Currying or iterated application is meant will always be clear from the context.

Definition 2.4 (Finite Sets) (a) We write {a_{1}, …, a_{n}} for the set with n elements, i.e. the set A having constructors a_{i} : A and the usual elimination rules for a set with n elements. In case n = 0 we write ∅, or ⊥, when considering it as the false proposition, for the set with no elements.

(b) Ex falsum quodlibet (latin for “from falsity follows everything”) creates an element of any set from a (non-existing) proof of falsity:

efq : (B : Set, p : ⊥) → B , efq_{B}(p) = case p of { } .

We sometimes omit the parameter B.

(c) ⊤ := {true}, the always true proposition.

(d) We define the set of Booleans is defined as Bool := {tt, ff} : Set.

(e) We define atom as the operation, which converts a Boolean value into a proposition, which is inhabited (i.e. provable), in case the value is true, and not inhabited (i.e. unprovable), in case the value is false:

atom : Bool → Set ,
atom(tt) := ⊤ , atom(ff) := ⊥ .

Definition 2.5 (Natural Numbers) The set of natural numbers is denoted by ℕ. We have the usual notations like 0, n + m, n < m.

Definition 2.6 (The set ℕ_{n}) (a) ℕ_{n} is the finite set with n elements, and by overloading the notation for the natural numbers, we write ℕ_{n} = {0, …, n−1}. We use ℕ_{n} as being defined by induction on ℕ, which can be done by defining ℕ_{0} = ∅, ℕ_{n+1} = {0}+ℕ_{n}. This means that the element i stands more formally for \underbrace{inr(inr(⋯ inr(}_{i times} inl(0)) ⋯)).

(b) If n : ℕ, then by (i < n) → D[i] we mean (i : ℕ_{n}) → D[i], and λi < n.r[i] stands for λi : ℕ_{n}.r[i]. Although sometimes i occurring in D[i] is actually a natural number, it can in our applications always be replaced by an element ℕ_{n}.

Definition 2.7 (Lists) (a) List(A) is the set of lists of elements of type A (where A : Set).

(b) For a list we have nil : List(A), cons : A → List(A) → List(A).

(c) We have the usual definition of length(l) for l : List(A), and for i < length(l) we have the ith element of the list denoted by (l)_{i}.

(d) If l : List(A), then (x ∈ l) → D[x] stands for (i < length(l)) → D[(x)_{i}], and λx ∈ l.s, which is supposed to be an element of (x ∈ l) → D[x], stands for λi < length(l).r[(x)_{i}].

(e) The formula (or type) x ∈ l is defined as (i < length(l))×(x =_{A} (l)_{i}). Similar notations (e.g. ∃x ∈ l, l ⊆ l′) are to be understood correspondingly.

(f) We write sometimes ⟨a_{1}, …, a_{n}⟩ for the list with elements a_{1}, …, a_{n} (in that order). Note that in case of n = 2 this overloads the notation ⟨a, b⟩ (used as well for elements of Σa : A.B(a)).

(g) map is the usual map function, so if l = ⟨a_{1}, …, a_{n}⟩ : List(A), f : A → B, then map(f, l) := ⟨f(a_{1}), …, f(a_{n})⟩ : List(B).

Remark 2.8 Note that when actually carrying out proofs on the machine, it is usually easier to replace lists by a pair consisting of n : ℕ and f : ℕ_{n} → A. Then the formula (x ∈ l) → D[x], with l corresponding to n, f stands for (i < n) → D[f(i)].

Definition 2.9 (A + B, Equality) (a) If A, B : Set, then A + B : Set is the disjoint union of A, B with constructors inl : A → (A + B), inr : B : B → (A + B) (for in-left and in-right).

(b) The equality set is denoted by a =_{A} b for a, b : A. We sometimes omit the index A, and assume that it is usually clear whether the equality set or definitional equality is meant.

Definition 2.10 If f : A → A′, then inj(f) := ∀a, a′ : A.f(a) =_{A′} f(a′) → a =_{A} a′ (f is injective).

Definition 2.11 (Families of Sets) (a) If X is a type, Fam(X) := ΣA : Set.A → X.

(b) If C : Fam(X), C = ⟨A, B⟩, then C.A := A, C.B := B.

(c) ∅_{Fam} := ⟨∅, λx.efq(x)⟩, the empty family.

(d) If A, A′ : Set, B : A → Set, B′ : A′ → Set. Then define [B, B′] : (A + B) → Set, [B, B′](inl(a)) = B(a), [B, B′](inr(a′)) = B′(a′).

(e) Assume C : Fam(Set), C′ : Fam(Set). Then C⊕C′ := ⟨C.A+C′.A, [C.B, C′.B]⟩ : Fam(Set).

(f) Assume A : I → Set, B : (i : I, A_{i}) → Set, written as B_{i}(a) for B(i, a). Then [ ]_{i:I}B_{i} : (Σi : I.A_{i}) → Set, [ ]_{i:I}B_{i}(⟨i, a⟩) := B_{i}(a).

(g) Assume C : I → Fam(Set), C_{i} = ⟨A_{i}, B_{i}⟩. Then ⊕_{i:I}C_{i} := ⟨Σ_{i:I}A_{i}, [ ]_{i:I}B_{i}⟩.

(h) Assume an operation like Rec, Rec′ as introduced later having arguments written as indices A : Set, B : A → Set. If we write such an operations with an index C : Fam(Set), we mean the indices C.A, C.B. E.g. Rec_{C} := Rec_{C.A,C.B}, Rec′_{C,a} := Rec_{C.A,C.B,a}, etc.

2.2 Partial Objects

In this article we will introduce various partial objects of some set B, which we usually denote by {e}(a) or {a, e′}_{e}, possibly with some subscripts or superscripts. They will all be elements of PrePar(B(a)) or Par(B(a)), as defined in the next definition.

Definition 2.12 (a) The set of pre-partial objects of the set B is defined as PrePar := Fam(B). If e : PrePar, we define e↓ := π_{0}(e), and for p : e↓, e[p] := π_{1}(e)(p). (So p : e↓ means that e is defined, and e[p] is the value of e depending on the proof p.)

(b) If e : PrePar, the consistency of e, Consistent(e) is defined as ∀p, p′ : e↓.e[p] =_{B} e[p′].

(c) The set of partial objects of the set B is defined as Par(B) := Σe : PrePar(B).Consistent(e). Overloading the notation we define for e : Par(B) e↓ := π_{0}(e)↓ and e[p] := π_{0}(e)[p].

We will usually introduce elements e : Par(B) by first defining e↓, e[p], and then later showing its consistency. Note that elements of Par(B) are usually not directly executable.

Definition 2.13 (a) Let B : Set, e, e′ : PrePar(B) (or : Par(B)), b : B.

\begin{aligned}e ≃ b & :⇔ & ∃p : e↓.e[p] = b , & e ⊑ e′ & :⇔ & ∀b : B.e ≃ b → e′ ≃ b , \\ e ≃ e′ & :⇔ & e ⊑ e′ ∧ e′ ⊑ e . \end{aligned}

(b) Assume f, g : (a : A) → Par(B(a)) (or f, g : (a : A) → PrePar(B(a)). Then we define f ⊆ g :⇔ ∀a : A.f(a) ⊑ g(a), f ≅ g :⇔ f ⊆ g ∧ g ⊆ f.

When in the above situation, f or g is of the form {e} (possibly with some subscripts or superscripts; such kind of notations will be introduced at various places in this article), we sometimes write e instead of {e}, e.g. e ⊆ e′ instead of {e} ⊆ {e′}.

2.3 Finite Functions

We introduce the set of multivalued finite functions (a : A) ⇀_{fin}^{multi} B(a) as lists of pairs ⟨a, b⟩ for a : A, b : B(a). Then we define finite functions (a : A) ⇀_{fin} B(a) as consistent elements of (a : A) ⇀_{fin}^{multi} B(a).

Definition 2.14 (Multivalued Finite Functions) Assume C = ⟨A, B⟩ : Fam(Set), which we keep fixed.

(a) (a : A) ⇀_{fin}^{multi} B := List(Σa : A.B).

(b) Let g : (a : A) ⇀_{fin}^{multi} B(a). We define {g}^{finfun} : A → PrePar(B(a)) by

{g}^{finfun}(a)↓ :⇔ ∃b : B(a).⟨a, b⟩ ∈ g , {g}^{finfun}(a)[⟨b, q⟩] := b .

(c) ∅_{finfun} := nil : (a : A) ⇀_{fin}^{multi} B(a). We sometimes omit the subscript finfun.

(d) Assume g : (a : A) ⇀_{fin}^{multi} B(a), a : A, b : B(a). Then

g[a ↦ b] := cons(⟨a, b⟩, g) : (a : A) ⇀_{fin}^{multi} B(a) .

(e) (⟨a, b⟩)_{finfun} := ∅_{finfun}[a ↦ b].

(f) Assume g : (a : A) ⇀_{fin}^{multi} B(a), B′ : A → Set, h : (a : A, B(a)) → B′(a). Then h ∘_{finfun,left} g := k, where k := map(λ⟨a, b⟩.⟨a, h(a, b)⟩, g). We usually omit the subscripts finfun, left of ∘.

(g) Assume A, A′ : Set, B′ : A′ → Set, h : A → A′, B : A → Set, B(a) := B′(h(a)). Assume g : (a : A) ⇀_{fin}^{multi} B(a). Then

g ∘_{finfun,right} h^{−1} := k ,

where k := map(λ⟨a, b⟩.⟨h(a), b⟩, g). We usually omit the indices finfun, right from ∘.

Definition 2.15 (Finite Functions) Assume C = ⟨A, B⟩ : Fam(Set), which we keep fixed.

(a) (a : A) ⇀_{fin} B := Σf : ((a : A) ⇀_{fin}^{multi} B(a)).∀a : A.Consistent({f}^{finfun}(a)).

If f : (a : A) ⇀_{fin}^{multi} B(a), and we later determine p : Consistent(f), then we will then consider f as an element of (a : A) ⇀_{fin} B(a), even so the element of (a : A) ⇀_{fin} B(a) is more precisely ⟨f, p⟩.

(b) We can lift in an obvious way {·}^{finfun}, ∅_{finfun}, (⟨a, b⟩)_{finfun}, h ∘_{finfun,left} g to operations on (a : A) →_{finfun} B(a) to (a : A) →_{finfun} B(a). This overloads the corresponding notations. We usually omit indices as when dealing with multivalued finite functions. In case of {·}^{finfun} we obtain in fact {g}^{finfun}(a) : Par(B(a)).

(c) Assume g : (a : A) ⇀_{fin} B(a), g = ⟨f, p⟩, a : A, b : B(a), p′ : ∀b′ : B(a).{g}^{finfun}(a) ≃ b′ → b′ =_{B(a)} b. Then

g[a ↦ b]_{p′} := ⟨f[a ↦ b], p′′′⟩ ,

where p′′′ : Consistent(f[a ↦ b]) is obtained from p and p′. If p′ is obvious, the subscript p′ will be omitted.

(d) Assume A, A′ : Set, B′ : A′ → Set, h : A → A′, B : A → Set, B(a) := B′(h(a)). Assume g = ⟨f, p⟩ : (a : A) ⇀_{fin} B(a), A′ : Set, p′ : inj(h). Then

g ∘_{finfun,right,p′} h^{−1} := ⟨f ∘_{finfun,right} h^{−1}, p′′⟩ ,

and p′′ : Consistent(f ∘_{finfun,right} h^{−1}) is obtained from p and p′.

We usually omit the indices finfun, right, and, if it is obvious, p′ from ∘.

(e) Assume g : (a : A) ⇀_{fin} B(a), g = ⟨f, p⟩. Then length(g) := length(f). Assume furthermore h : (a : A, b : B(a)) → ℕ. Then ∑_{a:dom(g)} .h(a, g(a)) := ∑_{i<length(l)} h(π_{0}((f)_{i}), h_{1}((f)_{i})). Note that g ≅ g′ ⇏ length(g) = length(g′), and g ≅ g′ ⇏ ∑_{a:dom(g)} h(a, g(a)) = ∑_{a:dom(g′)} h(a, g′(a)), since in f an element ⟨a, b⟩ might occur more than once.

3 Inductive-Recursive Definitions and Partial Recursive Functions

Before formulating the data type of partial recursive definitions as a data type of IIRD let us sketch briefly Dybjer’s notion of IIRD.

Dybjer introduced first the simpler notion of inductive-recursive definitions (IRD). In IRD one defines a set U : Set together with a function T : U → D where D : Type. IRD emerged first as universes, i.e. D = Set. Universes are sets of sets, which are given by a set U of codes for sets, and a decoding function T : U → Set, which determines for every code a : U the set T(a) : Set it denotes. Strictly positive inductive definitions are given by a set U together with constructors C : A_{1} → ⋯ A_{n} → U, where A_{i} can refer to U strictly positively: (1) Either A_{i} is a set, which was defined before one started to introduce U. Arguments of C referring to such sets are called non-inductive arguments. (2) Or A_{i} is of the form (B_{1} → ⋯ → B_{m} → U) for some sets B_{i} defined before U was introduced. Arguments referring to such sets are called inductive arguments. In dependent type theory, we can extend inductive definitions by allowing A_{i} to refer to previous arguments, i.e. we get C : (a_{1} : A_{1}, …, a_{n} : A_{n}) → U, and A_{i} might depend on a_{j} for j < i. However, closer examination reveals that only dependencies on noninductive arguments are possible: When introducing the constructor C, U has not been defined yet, so we are not able to define any sets depending on it. In an IRD of U : Set and T : U → D, A_{i} might refer to previous inductive arguments via T: if a_{j} : A_{j} = (B_{1} → ⋯ → B_{k} → U), and j < i, then A_{i} might make use of T(a_{j}(b_{1}, …, b_{k})). An example is the constructor Π̂ expressing the closure of a universe under the dependent function type (which is often written as Π(A, B)): Π̂ has type (a : U, b : T(a) → U) → U and the type of the second argument b of Π̂ depends on T(a). The intuition why this is a good predicative definition is that one defines the elements of U inductively. Whenever one introduces a new element of U, one computes recursively T applied to it. Therefore, when referring to a previous inductive argument, we can make use of T applied to it. When applying this principle, one notices that one often needs to define several universes (U_{i}, T_{i}) simultaneously. Indexed inductive-recursive definitions IIRD extend the principle of IRD so that it allows to define U : I → Set and T : (i : I, u : U(i)) → D[i] simultaneously for all i : I. Here I : Set, and i : I ⇒ D[i] : Type. The constructors of U(i) might refer to U(j) for any j in a strictly positive way, and make use of T applied to previous inductive arguments.

Reduction to inductive definitions. When formalising the representation of partial recursive functions as IIRD in general, one wants to represent partial recursive functions f : (x : A) ⇀ B(x) for arbitrary A : Set, B : A → Set. Such functions will be translated into IIRD with index set A and D[x] := B(x). Note that D[x] : Set. In [DS06] Dybjer and the author have shown that IIRD with D[x] : Set can always be reduced to indexed inductive definitions. We sketch the idea briefly by taking the example from the introduction. Remember that defined_{f}^{S} had type

defined_{f}^{S} : (n : ℕ, p : f(n)↓, q : f(f(n)[p])↓) → f(n + 1)↓ .

In order to avoid the use of f(n)[p] in the type of defined_{f}^{S}, one introduces first an inductive definition of a set f(n)^{aux}↓ : ℕ → Set, with constructors

defined_{f}^{0,aux} : f(0)↓^{aux} ,
defined_{f}^{S,aux} : (n : ℕ, p : f(n)^{aux}↓, m : ℕ, q : f(m)^{aux}↓) → f(n + 1)^{aux}↓ .

Then we compute recursively f(·)^{aux}[·] : (n : ℕ, p : f(n)^{aux}↓) → ℕ (this definition is now separated from the inductive definition of f(·)↓) by

f(0)^{aux}[defined_{f}^{0,aux}] := 0 ,
f(n + 1)^{aux}[defined_{f}^{S,aux}(n, p, m, q)] := f(m)^{aux}[q] .

p : f(n)^{aux}↓ proves that f(n) is defined, provided that, whenever we made use of defined_{f}^{S,aux}(n, p, m, q), we had m = f(n)^{aux}[p]. We introduce a correctness predicate expressing this:

Corr_{f}: (n : ℕ, p : f(n)^{aux}↓) → Set ,  Corr_{f}(0, defined_{f}^{0,aux}) := ⊤ ,
Corr_{f}(n + 1, defined_{f}^{S,aux}(n, p, m, q) :=
Corr_{f}(n, p) ∧ Corr_{f}(m, q) ∧ m =_{ℕ} f(n)^{aux}[p] .

One can now simulate f(·)↓ by

f(·)↓′ : ℕ → Set , f(n)↓′ := Σp : f(n)^{aux}↓.Corr_{f}(n, p) ,

and simulate f(·)[·] by

f(·)′[·] : (n : ℕ, p : f(n)↓′) → ℕ , f(n)′[⟨p, q⟩]  := f(n)^{aux}[p] .

In [DS06] this reduction has been carried out in detail and there we were able to show that indeed all IIRD with target type of T being a set can be simulated by indexed inductive definitions. Note that this reduction adds an additional overhead. So we assume when verifying the correctness of partial recursive functions on the machine one probably prefers to use the original IIRD.

Restrictions to the class of IIRD. Bove and Capretta have shown that the set of partial recursive functions definable this way is Turing-complete – it contains all partial recursive functions on ℕ – and that a large class of recursion schemes can be represented this way. However, not all IIRD having the above types correspond to functions, which can be computed partial-recursively. Here by “compute partialrecursively” we mean that we can consider f as a partial recursive function and in this way compute the value of f(n), where the computation terminates if and only if f(n)↓, and, if f(n)↓, returns the value of f.

1. We need to replace general IIRD by restricted IIRD. The concepts of general and restricted IIRD were investigated in [DS01, DS06]. In general IIRD, one introduces constructors for the inductively defined set U and then determines for each constructor C depending on its arguments a⃗ the i s.t. C(a⃗) : U(i). In the example used in the introduction we used in fact such kind of general IIRD. We have a constructor defined_{f}^{S}, and we state that defined_{f}^{S}(n, p, q) : f(n+1)↓, so the index n + 1 depends on the arguments n, p, q. The problem with this is that it allows to define multivalued functions: Nothing prevents us from adding a second constructor defined_{f}^{S,′}(n) : f(n + 1)↓, s.t.

f(n + 1)[defined_{f}^{S,′}(n)] returns a different value, e.g. 5. This corresponds to adding contradictory rewrite rules, such as f(n + 1) ⟶ 5.

Furthermore, allowing multiple constructors would prevent us in general to partial-recursively compute the functions: In order to partial-recursively compute f(n), one has to find the arguments of the constructor in such a way that we obtain an element of f(n)↓. This requires in general a search process. In case the elements of the index set of the set of constructors are finitely representable (e.g. it is a finite set or ℕ, or, more generally, an element of an inductive data type without infinite branching degrees), we could search for such an index. Otherwise, because of the incompleteness of type theory, we might have an index in a consistent extension of the type theory used, which does not exist in the current type theory. (Or, looking at it from a nonconstructive perspective, we might have an index in the “standard” model of type theory, but not in the type theory). So a search process for a proof in the current type theory might not find the index needed.

In order to obtain partial-recursively computable functions we therefore require that we are able to determine for each index its constructor and which arguments are needed. This corresponds to restricted IIRD as introduced in [DS06]. If one defines in restricted IIRD U : I → Set, one needs to determine, depending on i the set of constructors having result type U(i). The initial example can be represented as a restricted IIRD by defining it as follows:

f(n)↓ := case n of 0  → data C_{f}^{0} S(n′) → data C_{f}^{S}(p : f(n′)↓, q : f(f(n′)[p])↓) .

So f(0)↓ has constructor C_{f}^{0}, and f(S(n′))↓ has constructor C_{f}^{S} with arguments p : f(n′)↓ and q : f(f(n′)[p])↓.

2. In order to avoid multivalued functions, for each argument a : A there should be at most one constructor of type f(a)↓. One can easily achieve that there is always exactly one constructor – if there is none, one can always add the constructor C : (p : f(a)↓) → f(a)↓ corresponding to black hole recursion (i.e. rewrite rule f(a) ⟶ f(a)).

3. We disallow non-inductive arguments. Non-inductive arguments, except for the empty set and the one-element set might result in multivalued functions (different choices for one argument of the constructor might yield different proofs of f(n)↓ and therefore different values of f(n)[p]). Another problem with non-trivial non-inductive arguments is that when computing the function partial-recursively, one needs to search for instances of these non-inductive argument. Therefore, as argued before, one does not obtain in general partialrecursively computable functions. We could allow non-indexed arguments indexed over the one-element set 1 and the empty set ∅, since this does not require a search process. But arguments indexed over 1 can be ignored, and arguments indexed over ∅ have the effect that f(a) ↑, which can alternatively be obtained by using black-hole recursion as above.

4. Inductive arguments should be single ones. In general IIRD of a set U, the constructor might have an inductive argument of the form (x : A) → U(i(x)). In our setting such an inductive argument would be of the form (x : A) → f(i(x))↓, which expresses f(i(x)) is defined for all x : A. Such an argument requires the evaluation of f for possibly infinitely many values i(x) (x : A), which is non-computable. One can search for a proof of (x : A) → f(i(x)) and use this search process as a means of evaluating f. As we indicated before (in this case the incompleteness is a problem even in simple situations, if A is infinite), this does in general not result in partial-recursively computable functions.

So in order to obtain partial-recursively computable functions, we will restrict inductive arguments to single valued ones, i.e. in the above situation to arguments of the form p : f(i)↓.

4 A Data Type of Partial Recursive Functions

In [BC05a] it was pointed out that one of the limitations of their approach is that they cannot define partial recursive functions referring to other partial recursive functions as a whole. We have given a toy example in the introduction (the function g : List(ℕ) ⇀ List(ℕ)). In computability theory one overcomes this problem by introducing Kleene-indices for partial recursive functions. Then one can define for instance map by having two natural numbers as arguments, one which is a Kleeneindex for a partial recursive function, and the second one a code for a list. In order to do the same using the approach by Bove/Capretta, we will introduce a data type of codes for the IIRD we were referring to above. This data type is a subtype of the data type of IIRD introduced in [DS06] (see as well [DS01, DS03, DS99]). This shows the consistency of the new rules introduced in this article. Assume A : Set, B : A → Set fixed. Unless explicitly needed, we suppress in the following dependencies on A, B (which would be added as initial indices). We regard a partial recursive function f : (a : A) ⇀ B(a) as being given by an IIRD, and introduce the data type Rec of codes for those IIRD, which correspond according to the previous section to partial recursive functions. So the set Rec will as well be the set of codes for partial recursive functions. We have formation rule:

Rec : Set .

(Without suppressing the dependency on A, B this set would be called Rec_{A,B}; similarly for later operations defined in this section). For e : Rec we define

{e} : A → PrePar(B(a)) .

(We will later after the definition of Rec is finished show the consistency of {e}(a), and can extend it therefore to an element of Par(B(a))). In fact we define for e : Rec inductively

{e}(·)↓ : A → Set ,

while recursively defining for a : A p : {e}(a)↓

{e}(a)[p] : B(a) .

{e}(a)↓ means that the function with index e is defined for argument a, and if p : {e}(a)↓, then {e}(a)[p] is result of evaluating {e}(a) using this proof. Rec is a restricted IIRD, which means that for each a : A we can determine the type of arguments for the constructor with result {e}(a)↓. Let Rec′_{a} be the type of codes for possible arguments for the constructor of an IIRD e with result {e}(a)↓. Then an element of Rec is given by an element of Rec′_{a} for each a : A. So we have the following formation and equality rule:

Rec′ : A → Set ,  Rec = (a : A) → Rec′_{a} .

The type of the arguments of the constructor of {e}(a)↓ and the result of {e}(a)[p] for the constructed element p will depend on {e}(·)↓ and {e}(·)[·]. Since, when introducing Rec′_{a}, {e}(·)↓ and {e}(·)[·] are not available, we define more generally, depending on a : A, e : Rec′_{a}, for general X and Y having the types of {e}(·)↓, {e}(·)[·], respectively, the following operations:

Arg_{a,e} : (X : A → Set, Y : (a′ : A, x : X(a′)) → B(a′)) → Set ,
Eval_{a,e} : (X : A → Set, Y : (a′ : A, x : X(a′)) → B(a′), Arg_{a,e}(X, Y)) → B(a) .

Let for e′ : Rec′_{a}

{a, e′}_{e}^{aux} : PrePar(B(a)) ,
{a, e′}_{e}^{aux}↓ := Arg_{a,e′}({e}(·)↓, {e}(·)[·]) : Set ,
{a, e′}_{e}^{aux}[p] := Eval_{a,e′}({e}(·)↓, {e}(·)[·], p) : B(a) (where p : {a, e′}_{e}^{aux}↓) .

(We will later show the consistency of {a, e′}_{e}^{aux}, and therefore can consider it as an element of Par(B(a)).) Then

{a, e(a)}_{e}^{aux}↓

will be the type of the arguments of the constructor of {e}(a)↓. If using arguments p we have constructed q : {e}(a)↓, then

{e}(a)[q] = {a, e(a)}_{e}^{aux}[p] .

If we call the constructor for {e}(a)↓ tot_{e,a}, then the introduction and equality rules for {e}(·)↓ and {e}(·)[·] are as follows:

tot_{e,a} : {a, e(a)}_{e}^{aux}↓ → {e}(a)↓ ,
{e}(a)[tot_{e,a}(p)] = {a, e(a)}_{e}^{aux}[p] .

Essentially, {e}(a)↓ is defined as {a, e(a)}_{e}^{aux}↓ (we only put a constructor around this). {a, e′}_{e}^{aux}↓ is an auxiliary definition, which defines, whether the subcomputation for argument a given by e′ is defined, provided that the complete function has index e. {a, e′}_{e}^{aux}[p] defines, how to compute the value for this subcomputation, depending on a proof p : {a, e′}_{e}^{aux}↓. Rec′_{a} has 2 constructors:

1. Initial (constant) case: the constructor for {e}(a)↓ has no arguments (or more precisely the trivial argument x : {∗} for the one-element set {∗}). {e}(a)[p] returns, independently of p, a fixed element b : B(a) (we use the notation return, since it makes writing of codes for partial recursive functions more readable: when we reach return, we return a result obtained):

return : B(a) → Rec′_{a} , Arg_{a,return(b)}(X, Y) = {∗} ,
Eval_{a,return(b)}(X, Y, ∗) = b .

So we obtain, if e′ = return(b),

\begin{aligned}\{a, e′\}_{e}^{aux}↓ & = & \{∗\} , \\ \{a, e′\}_{e}^{aux}[p] & = & b . \end{aligned}

{a, e′}_{e}^{aux}↓ is always defined, and the result of evaluating it returns b. This means that {a, e′}_{e}^{aux}↓ is the constant function, which returns always b.

2. A single inductive argument. The constructor of {e}(a)↓ has as an inductive argument p : {e}(a′)↓, and depending on b := {e}(a′)[p] later arguments. As a partial recursive function this means that we make a recursive call to {e}(a′)↓. Depending on the result b, we choose further steps. So the constructor rec of Rec′_{a} needs to have as arguments a′ and a function e′ : B(a′) → Rec′_{a}, which determines depending on the result b : B(a′) of {e}(a′)[p] the later arguments of the constructor. We obtain

rec : (a′ : A, g : B(a′) → Rec′_{a}) → Rec′_{a} ,
Arg_{a,rec(a′,g)}(X, Y) = Σx : X(a′).Arg_{a,g(Y (a′,x))}(X, Y) ,
Eval_{a,rec(a′,g)}(X, Y, ⟨x, y⟩) = Eval_{a,g(Y (a′,x))}(X, Y, y) .

So we obtain, if e = rec(a′, g),

{a, e′}_{e}^{aux}↓ = Σp : {e}(a′)↓.{a, g({e}(a′)[p])}_{e}^{aux}↓ ,
{a, e′}_{e}^{aux}[⟨p, q⟩] = {a, g({e}(a′)[p])}_{e}^{aux}[q] .

So {a, e′}_{e}^{aux}↓ holds, if we have a proof p : {e}(a′)↓, and if {e}(a′)[p] = b′, we have for the subcomputation e′′ := g(b′) of e′ a proof q : {a, e′′}_{e}^{aux}↓. Then {e′}(a)[⟨p, q⟩] ≃ {a, e′′}_{e}^{aux}[q]. This means that {a, e′}_{e}^{aux} is the function, which first computes {e}(a′), and if that computation terminates with result b, then computes {a, g(b)}_{e}^{aux} and returns its result.

We observe that Rec′_{a} is an inductively defined set: it is like a W-type with branching degrees (B(a))_{a:A}, but with additional leaves return(b). Arg and Eval can be defined by recursion on Rec′_{a}, after the definition of Rec′_{a} is finished. {e}(·)↓ and {e}(·)[·] are given by an IIRD which is determined by e.

5 An Induction Principle for the Data Type of Partial Recursive Functions.

In order to prove properties of elements of Rec, we need an induction principle for it corresponding to the fact that it is the least set introduced by the introduction rules. In case of general IIRD (see especially [DS06], but as well [DS01, DS03]) we had introduced this induction principle. Adapted to our setting, this principle is as follows: Assume as before A : Set, B : A → Set (these arguments will be suppressed), a : A, e : Rec′_{a}. Depending on X : A → Set, Y : (a′ : A, x : X(a′)) → B(a′) and b : Arg_{a,e}(X, Y) we defined a set of pairs ⟨a′, p⟩ s.t. rec(a′, g) occurred in the part of e used by b and s.t. b contained the element p : X(a). These correspond in IIRD to the inductive arguments used there, or more precisely to the pairs ⟨i, x⟩ consisting of the index i for the inductive argument and the inductive argument x used itself. In our setting we have only single-valued inductive arguments, and therefore only finitely many of them. Therefore the set of inductive arguments is finite, and we can represent the inductive arguments as a finite function, namely an element of (a : A) ⇀_{fin} X(a). If we specialise this to the situation where X = {e}(·)↓ and Y = {e}(·)[·], then the inductive arguments are given by a function h := calls_{e}(a, e′, p) : (a : A) ⇀_{fin} {e}(a)↓ (where e : Rec, a : A, e′ : Rec′_{a}, p : {a, e′}_{e}^{aux}↓), which will be defined in the following. The domain of h will be the set of a′ s.t. rec(a′, g) (i.e. an inductive argument with index a′) occurs in the part of e′ used by p. Then {h}^{finfun}(a)[ ] = p′ for the proof p′ used in p (i.e. the actual inductive argument). For convenience we define as well a finite function callresults which returns {e}(a′)[p] rather than p : {e}(a′)↓.

Definition 5.1 (a) Assume e : Rec, a : A, e′ : Rec′_{a}, p : {a, e′}_{e}^{aux}↓. We define

calls_{e}(a, e′, p) : (a′ : A) ⇀_{fin}^{multi} {e}(a)↓ ,

by recursion on e′ as follows:

calls_{e}(a, return(b), ∗) := ∅_{finfun} ,
calls_{e}(a, rec(a′, g), ⟨p, p′⟩) := calls_{e}(a, g({e}(a′)[p]), p′)[a′ ↦ p] .

We will later see that there is at most one proof of {e}(a)↓ and therefore Consistent({calls_{e}(a, e′, p)}^{finfun}(a′)),

calls_{e}(a, e′, p) : (a′ : A) ⇀_{fin} {e}(a)↓ .

(b) We define assuming e, a, e′, p as before

callresults(a, e′, p) : (a′ : A) ⇀_{fin}^{multi} B(a′) ,
callresults(a, e′, p) := (λa, p.{e}(a)[p]) ∘ calls_{e}(a, e′, p) .

When we have obtained calls_{e}(a, e′, p) : (a′ : A) ⇀_{fin} {e}(a)↓, then we obtain as well

callresults_{e}(a, e′, p) : (a′ : A) ⇀_{fin} B(a) .

Lemma 5.2 Assume a, a′ : A, e : Rec′_{a}, g : B(a′) → Rec′_{a}, p : {e}(a′)↓, b := {e}(a′)[p], p′ : {a, g(b)}_{e}^{aux}↓. Let h := calls_{e}(a, rec(a′, g), ⟨p, p′⟩).

(a) {h}^{finfun}(a′) ≃ p.

(b) calls_{e}(a, g(b)) ⊆ h.

Proof: Immediate.

Assume, we want to prove, assuming D : (a : A, p : {e}(a)↓) → Set, that the following holds:

(a : A, p : {e}(a)↓) → D(a, p) .

(This corresponds to the formula ∀a : A.∀p : {e}(a)↓.D(a, p).) Let for a : A, p : {a, e(a)}_{e}^{aux}↓, h(a, p) := calls_{e}(a, e(a), p) : (a : A) ⇀_{fin} {e}(a)↓. Then the step function is

step : (\begin{matrix}a : A, \\ p : \{a, e(a)\}_{e}^{aux}↓, \\ ih : (a′ : A, p : \{h(a, p)\}^{finfun}(a′)↓)) → D(a′, \{h(a, p)\}^{finfun}(a′)[p]) \end{matrix} → D(a, tot_{e,a}(p)) .

The induction principle for {e}(·)↓ says that if we have such a step function, then we obtain a function

g : (a : A, p : {e}(a)↓) → D(a, p) ,

s.t. we have

g(a, tot_{e,a}(p)) = step(a, p, λa′ : A.λp : {h(a, p)}^{finfun}(a′)↓.g(a′, {h(a, p)}^{finfun}(a′)[p]) .

The elimination and equality rules for {e}(·)↓ is the principle, that for any step function (possibly depending on some context) there exist a function g as above satisfying the equality just mentioned. This principle can be introduced as well by introducing a suitable recursion operator – we refrain from doing so in order not to avoid introducing too many unnecessary notations. We leave it to the reader to observe that this induction principle is equivalent to the one introduced in [DS06], which corresponds to the fact that a family of sets defined by an IIRD is the least family closed under the corresponding operator. See as well [DS03] for an analysis of the relationship to initial algebras. The following lemma follows immediately using the induction principle:

Lemma 5.3 If p : {e}(a)↓. Then there exist p′ : {a, e(a)}_{e}^{aux}↓ s.t. p =_{{e}(a)↓} tot_{e,a}(p′).

The length of elements of {e}(a)↓, {a, e′}_{e}^{aux}↓. We introduce a length function for these elements. Most proofs carried out in this article will be carried out by induction on this length, which makes it easier to argue then by using directly using the induction principle. When we say later induction on e we will often mean more precisely induction on length(e).

Lemma and Definition 5.4 Assume A : Set, B : A → Set, e : Rec_{A,B} fixed. There exist functions (we overload the name length here, which is already used for lists; we omit as well the additionally needed subscripts A, B, e)

length : (a : A, p : {e}(a)↓) → ℕ ,
length^{aux} : (a : A, e′ : Rec′_{a}, p : {a, e′}_{e}^{aux}↓) → ℕ .

s.t. the following holds

(a) length(a, tot_{e,a}(p)) = length^{aux}(a, e(a), p).

(b) Let h := calls_{e}(a, e′, p). If a′ : A, p : {h}^{finfun}(a′)↓, q := {h}^{finfun}(a′)[p], then length(a′, q) < length^{aux}(a, e′, p).

(c) If ⟨p, p′⟩ : {a, rec(a′, g)}_{e}^{aux}↓, then

length(a, p) < length^{aux}(a, rec(a′, g), ⟨p, p′⟩) ,
length^{aux}(a, p′, g({e}(a′)[p])) < length^{aux}(a, rec(a′, g), ⟨p, p′⟩) .

We will usually omit the superscript aux of length^{aux}.

Proof: We define length(a, p) by induction on a, p as

length(a, tot_{e,a}(p)) := length^{aux}(a, e(a), p)

where

length^{aux}(a, e′, p) := ∑_{a′∈dom(calls_{e}(a,e′,p))}(length(a′, calls_{e}(a, e′, p)(a′)) + 1) .

The conditions follow obviously.

Theorem 5.5 (Consistency of {e}(a), {a, e′}_{e}^{aux}) (a) If p, p′ : {e}(a)↓, then p =_{{e}(a)↓} p′.

(b) If p, p′ : {a, e′}_{e}^{aux}↓ then p =_{{a,e′}_{e}^{aux}↓} p′.

(c) Consistent({e}(a)), Consistent({a, e′}_{e}^{aux}).

(d) calls_{e}(a, e′, p) : (a′ : A) ⇀_{fin} {e}(a)↓, callresults_{e}(a, e′, p) : (a′ : A) ⇀_{fin} B(a).

Proof: We will write = instead of =_{A} for some set A. We show (a), (b) simultaneously by induction on length(p). Then (c), (d) follow by (a), (b). (a) reduces to (b), since by Lem. 5.3 we can assume p = tot_{e,a}(p_{0}), p′ = tot_{e,a}(p′_{0}), length(p) = length(p_{0}), length(p′) = length(p′_{0}). So we need only to show (b). Case e′ = return(b). Then p = ∗ = p′. Case e′ = rec(a′, g). Then p = ⟨p_{0}, p_{1}⟩, p′ = ⟨p′_{0}, p′_{1}⟩, and we have by IH and Lemma 5.4 (c) p_{0} = p′_{0}, p_{1} = p′_{1}, therefore p = p′.

6 Evaluation of Elements of Rec

In [Set06] we introduced the evaluation of elements of Rec_{e} applied to arguments a : A as an external operation. We are going to show how to introduce this as an internal operation. This will be done by introducing a reduction relation, s.t., if iterated reduction terminates (or more precisely reduces to itself), we can extract from the resulting element a b : B(a), and have b = {e}(a)[ ]. The reductions will be carried on elements of a data structure which is close to a monad. The data structure is Rec′_{a} (as before we keep A : Set and B : A → Set fixed). We define the following monad like operations:

return′ : (a : A, b : B(a)) → Rec′_{a} ,
return′_{a}(b) := return(b) ,
(∗) : (a : A, a′ : A, e : Rec′_{a}, h : B(a) → Rec′_{a′}) → Rec′_{a′} ,

written as e ∗_{a,a′} h and defined by induction on e:

return(b) ∗_{a,a′} h = h(b) ,
rec(a′′, h′) ∗_{a,a′} h = rec(a′′, λb′′ : B(a′′).h′(b′′) ∗_{a,a′} h) .

Now define

defined : (a : A, Rec′_{A,B,a}) → Bool ,
defined_{a}(return(b)) := tt ,
defined_{a}(rec(a, h)) := ff ,
Defined : (a : A, e : Rec′_{A,B,a}) → Set ,
Defined_{a}(e) := atom(defined_{a}(e)) .

Defined_{a}(e) is true, if the computation of e is finished. We define the function which extracts the resulting element of B(a), if the computation has terminated

Extract : (a : A, e : Rec′_{a}, p : Defined_{a}(e)) → B(a) ,
Extract_{a}(return(b), p) = b ,
Extract_{a}(rec(a′, h), p) = efq_{B(a)}(p) .

Next we define, the one step reduction of an element of Rec′_{a}, assuming an element e : Rec corresponding to the global function:

Red : (e : Rec, a : A, e′ : Rec′_{a}) → Rec′_{a} ,
Red_{e,a}(return(b)) := return(b) ,
Red_{e,a}(rec(a′, h)) := e(a′) ∗_{a′,a} h .

So return(b) does not evaluate any further. rec(a′, h) reduces to a computation which consists of first a computation of e(a′), followed, if the result was b′, by a computation of h(b′). Let

Red_{e,a}^{n}(b) := \underbrace{Red_{e,a}^{n}(Red_{e,a}^{n}(⋯ Red_{e,a}^{n}(}_{n times} b) ⋯)) .

Then one can easily see

Defined_{a}(Red_{e,a}^{n}(b)) → ∀m ≥ n.Red_{e,a}^{m}(b) = Red_{e,a}^{n}(b) .  (∗)

We can now define for a : A, e′ : Rec_{a}, e : Rec the partial object {a, e′}_{e}^{comp,aux} : Par(B(a)) by

{a, e′}_{e}^{comp,aux}↓ := Σn : ℕ.Defined_{a}(Red_{e,a}^{n}(e′)) ,
{a, e′}_{e}^{comp,aux}[⟨n, p⟩] := Extract_{a}(Red_{e,a}^{n}(e′), p) : B(a) ,

where Consistent({a, e′}_{e}^{comp,aux}) follows by (∗). Then we define for e : Rec, a : A {e}^{comp}(a) : Par(B(a)) by

{e}^{comp}(a) := {a, e(a)}_{e}^{comp,aux} .

Assuming e : Rec, a : A, b : B(a) has been derived under an empty context, and that the underlying type theory is normalising w.r.t. weak head normal form for closed term, then {a, e′}_{e}^{comp,aux} and therefore as well {e}^{comp}(a) are externally computable: All we need is to iteratively apply Red_{e,a}^{n} iteratively to e′ until we obtain defined_{a}(Red_{e,a}^{n}(e′)) = tt, and then compute Extract_{a}(Red_{e,a}^{n}(e′, true). So we see that for every e : Rec we obtain a partial recursive function {e}^{comp}(a).

7 Correctness of the Evaluation of Elements of Rec

Theorem 7.1 Assume e : Rec, a : A, e′ : Rec′_{a}. Then (a) {a, e′}_{e}^{comp,aux} ≃ {a, e′}_{e}^{aux}.

(b) {e}^{comp} ≅ {e}.

In order to prove Theorem 7.1, we show first the following lemma:

Lemma 7.2 Assume e : Rec, a : A, e′ : Rec′_{a}, a′ : A, e′′ : B(a) → Rec′_{a′}. Then we have:

(a) There exists q : Defined′_{a}(Red_{e,a′}^{n}(e′∗_{a,a′} e′′)), if for some k, m ≤ n s.t. k+m = n we have some p : Defined_{a}(Red_{e,a}^{k}(e′)) and for b := Extract_{a}(Red_{e,a}^{k}(e′), p) we have some p′ : Defined_{a′}(Red_{e,a′}^{m}(e′′(b))).

Furthermore, if such q, k, m, p, p′ exists, then

Extract_{a′}(Red_{e,a′}^{n}(e′ ∗_{a,a′} e′′, q) = Extract_{a′}(Red_{e,a′}^{m}(e′′(b)), p′) .

(b) {a, e′}_{e}^{aux}↓ ⇔ ∃n : ℕ.Defined(Red_{e,a}^{n}(e′))

(c) For all p : {a, e′}_{e}^{aux}↓, n : ℕ, q : Defined(Red_{e,a}^{n}(e′)) we have

{a, e′}_{e}^{aux}[p] = Extract(Red_{e,a}^{n}(e′), q) .

If we have shown this lemma, then Theorem 7.1 follows: 7.1 (a) follows immediately by (b) and (c). 7.1 (b) follows by 7.1 (a).

Proof of Lemma 7.2: We will omit indices of Extract, Defined, Red and ∗.

• Proof of (a) by induction on n:

- Case e′ = return(b): Then Defined′(Red^{k}(e′)) holds for all k, Extract(Red^{k}(e′), p) = b, Red^{n}(e′ ∗ e′′) = Red^{n}(e′′(b)), therefore the assertion holds (with k := 0, m := n).

- Case e′ = rec(a′′, h). We have e′ ∗ e′′ = rec(a′′, λb′′ : B(a′′).h(b′′) ∗ e′′). We have ¬Defined(Red^{0}(e′ ∗ e′′)), ¬Defined(Red^{0}(e′)). Furthermore

Red^{n+1}(e′ ∗ e′′) = Red^{n}(e(a′′) ∗ λb′′ : B(a′′).h(b′′) ∗ e′′) ,
Red^{k+1}(e′) = Red^{k}(e(a′′) ∗ h) .

Defined(Red^{n+1}(e′ ∗ e′′)) if and only if Defined(Red^{n}(e(a′′) ∗ λb′′ : B(a′′).h(b′′) ∗ e′′)), which holds by applying the IH twice if and only if there exists k, l, m ≤ n s.t. k+l+m = n and there exist p′′ : Defined(Red^{k}(e(a′′))), for b′′ := Extract(Red^{k}(e(a′′)), p′′) there exists p : Defined(Red^{l}(h(b′′))), and for b := Extract(Red^{l}(h(b′′)), p) we have Defined(Red^{m}(e′′(b))). Again by IH this holds if there exists k′, k′′ ≤ n s.t. k′ + k′′ = n and p : Defined(Red^{k′}(e(a′′) ∗ h)) and with b := Extract(Red^{k′}(e(a′′)∗h), p) we have Defined(Red^{m}(e′′(b))). Since Red^{k′}(e(a′′) ∗ h) = Red^{k′+1}(rec(a′′, h)) we obtain the equivalence in (a). The equality statement of (a) follows similarly.

• We show direction “⇐” of (b) and statement (c) simultaneously by induction on n.

- Case e′ = return(b). We have {a, e′}_{e}^{aux}↓, Red^{n}(e′) = e′ and Defined(Red^{n}(e′)) for all n, {a, e′}_{e}^{aux}[p] = b = Extract(Red^{n}(e′), p′).

- Case e′ = rec(a′, h). Considering the left sides of the equivalence and equation, we obtain {a, rec(a′, h)}_{e}^{aux}↓ = Σp : {e}(a′)↓.{a, h({e}(a′)[p])}_{e}^{aux}↓, therefore {a, e′}_{e}^{aux}↓ iff there exists p : {e}(a′)↓ s.t. with b := {e}(a′)[p] we get q : {a, h(b)}_{e}^{aux}↓. Furthermore for p, q as above we get {a, e′}_{e}^{aux}[⟨p, q⟩] = {a, h(b)}_{e}^{aux}[q]. If we consider the right sides of the equivalence and equation we get ¬(Defined(Red_{e,a}^{0}(e′)), Red_{e,a}^{n+1}(e′) = Red_{e,a}^{n}(e(a′) ∗ h), therefore Defined(Red_{e,a}^{n+1}(e′)) if and only if there exist m, m′ ≤ n.m + m′ = n, p : Defined(Red_{e,a′}^{m′}(e(a′)) s.t. with b := Extract(Red_{e,a′}^{m}(e(a′)), p) we get q : Defined(Red_{e,a}^{m′}(h(b))). Furthermore for n, m, m′ and a proof p′ : Defined(Red_{e,a}^{n+1}(e′)) obtained from p, q as above we obtain Extract(Red_{e,a}^{n+1}(e′), p′) = Extract(Red_{e,a}^{m′}(h(b), q)). The statements follow now by the IH.

The statement (b), direction “⇒” follows by a similar argument, but by induction on p : {a, e′}_{e}^{aux}↓.

8 Finite Approximations of {e}(a)↓

We are later going to translate elements of e : Rec′_{C,a} into an element e′ : Rec′_{C′,a′} for suitable C, C′, a, a′. We need to establish a correctness statement concerning the relationship between {a, e}_{e_{0}}^{aux} and {a′, e′}_{e′_{0}}^{aux}. The problem is that e_{0} : Rec_{C} has to be replaced by some e′_{0} : Rec_{C′}, and in general it is difficult to define such e′_{0} from e_{0} (or vice versa). Therefore we introduce a variant of {·, ·}_{·}^{aux}, where we refer to finite approximations of functions g : (a : C.A) → C.B rather than elements of Rec_{C}. Then it will usually be easy to define from g corresponding to e a corresponding function g′ corresponding to the translated index e′.

Definition 8.1 ({a, e}_{g}^{fin}) (a) For g : (a : A) ⇀_{fin} B(a), a : A, e : Rec′_{A,B,a} we define {a, e}_{g}^{fin} : PrePar(B(a)) as follows (by Lemma 8.2 (a) it will follow that {a, e}_{g}^{fin} : Par(B(a))):

• If e = return(b), then

\begin{aligned}\{a, e\}_{g}^{fin}↓ & := & \{∗\} : Set , \\ \{a, e\}_{g}^{fin}[∗] & := & b : B(a) . \end{aligned}

• If e = rec(a, h), then

{a, e}_{g}^{fin}↓ := Σp : {g}^{finfun}(a)↓.{a, h({g}^{finfun}(a)[p])}_{g}^{fin}↓ : Set ,

{a, e}_{g}^{fin}[⟨p, p′⟩] := {a, h({g}^{finfun}(a)[p])}_{g}^{fin}[p′] .

(b) Assume g : (a : A) ⇀_{fin} B(a), a : A, e : Rec′_{A,B,a}, p : {a, e}_{g}^{fin}↓. We define callresults_{g}(a, e, p) : (a : A) ⇀_{fin} B(a) (which will be the finite approximation of g used in p) s.t. callresults_{g}(a, e, p) ⊆ g as follows:

callresults_{g}(a, return(b), ∗) := ∅_{finfun} ,
callresults_{g}(a, rec(a′, k), ⟨p, p′⟩) = callresults_{g}(a, k(b), p′)[a′ ↦ b]_{q} ,
where b = {g}^{finfun}(a′)[p].

Here in the second clause q is determined by the fact that callresults_{g}(a, k(b), p′) ⊆ g.

Lemma 8.2 (a) Consistent({a, e}_{g}^{fin}).

(b) Assume g ⊆ g′. Then {a, e}_{g}^{fin} ⊑ {a, e}_{g′}^{fin}.

(c) Assume p : {a, e′}_{e}^{aux}↓, g := callresults_{e}(a, e′, p) (which is the finite approximation of e which is used in p). Then {a, e′}_{e}^{aux} ≃ {a, e′}_{g}^{fin}.

(d) (callresults_{g}(a, e, p) is the minimal finite approximation of g used in p) Assume g : (a : A) ⇀_{fin} B(a), e : Rec_{A,B}, p : {a, e′}_{g}^{fin}↓, and let g′ := callresults_{g}(a, e′, p). Then {a, e′}_{g}^{fin} ≃ {a, e′}_{g′}^{fin}. Furthermore, if g ⊆ g′′, p′′ : {a, e}_{g′′}^{fin}↓, then callresults_{g}(a, e, p) ≅ callresults_{g′′}(a, e, p′′).

(e) (callresults_{e}(a, e′, p) is the minimal finite approximation of e used in p) Assume g : (a : A) ⇀_{fin} B(a), e : Rec_{A,B}, g ⊆ {e}. Assume p : {a, e′}_{g}^{fin}↓. Then {a, e′}_{g}^{fin} ≃ {a, e′}_{e}^{aux}. Furthermore, if p′ : {a, e′}_{e}^{aux}↓, then callresults_{e}(a, e′, p′) ≅ callresults_{g}(a, e′, p).

Proof: Easy induction on e or e′.

9 Sum of Elements of Rec

In this section, we are going to introduce various operations, which allow to combine several recursive functions into one. We first determine an embedding from elements e′ : Rec′_{C,a} into e′_{0} : Rec′_{C′,g(a)} for an homomorphism g : C → C′ (i.e. g : A → A′ s.t. B(a) = B′(g(a))). The correctness statement will refer to finite approximations of elements of Rec_{e} rather than elements of Rec_{e}. The reason is that {a, e′}_{e}^{aux}↓ and {g(a), e′_{0}}_{e_{0}}^{aux}↓ refer to different e and e_{0}, namely e : Rec_{C} and e_{0} : Rec_{C′}. We do not know how to define e_{0}, since this function will be defined after the embedding of e′ to e′_{0} has been completed. However, the relationship between the finite approximations can easily be defined.

Lemma and Definition 9.1 Assume A : Set and C′ = ⟨A′, B′⟩ : Fam(Set), Assume g : A → A′. Let B := λa : A.B′(g(a)) : A → Set, C := ⟨A, B⟩ : Fam(Set). (When applying this lemma, usually B, B′ are given first and we have a : A ⇒ B(a) = B′(g(a))). Then there exist

emb_{C,C′,g} : (a : A, e : Rec′_{C,a}) → Rec′_{C′,g(a)} ,

s.t. the following holds: Assume inj_{g} : inj(g). Assume a : A, e : Rec′_{C,a}. Let a_{0} := g(a), e_{0} := emb_{C,C′,g}(a, e).

(a) Assume h : (a : A) ⇀_{fin} B(a), h_{0} := h ∘_{inj_{g}} g^{−1} : (a : A′) ⇀_{fin} B′(a). Then {a, e}_{h}^{fin} ⊑ {a_{0}, e_{0}}_{h_{0}}^{fin}.

(b) Assume h_{0} : (a : A′) ⇀_{fin} B′(a), p_{0} : {a_{0}, e_{0}}_{h_{0}}^{fin}↓. Let r_{0} := callresults_{h_{0}}(a_{0}, e_{0}, p_{0}). Then for all a′_{0} : A s.t. {r_{0}}^{finfun}(a′_{0})↓, we have a′_{0} = g(a′) for some a′. Let r : (a : A) → B(a) s.t. r ∘ g^{−1} = r_{0}. Then {a, e}_{r}^{fin} ≃ {a_{0}, e_{0}}_{r_{0}}^{fin} ≃ {a_{0}, e_{0}}_{h_{0}}^{fin}.

We usually omit the indices C, C′ of emb_{C,C′,g}.

Proof: We define emb_{g}(a, e) by induction on e and show the statements (a), (b). Note that in (b) we only have to show {a, e}_{r}^{fin}↓. Once this is established, then the remaining equalities follow by (a) and Lem. 8.2 (d).

• Case e = return(b). Then emb_{g}(a, e) := return(b). The correctness statements are trivial.

• Case e = rec(a′, k). emb_{g}(a, e) := rec(g(a′), λb : B(a′).emb_{g}(k(b))). For statement (a) assume p = ⟨p′, p′′⟩ : {a, e}_{h}^{fin}↓, and let e_{0} := emb_{g}(a, e). We have p′ : {h}^{finfun}(a′)↓, and with b := {h}^{finfun}(a′)[p′] : B(a′), p′′ : {a, k(b)}_{h}^{fin}↓. There exists p′_{0} : {h_{0}}^{finfun}(a′_{0})↓, and we have {h_{0}}^{finfun}(a′_{0})[p′_{0}] = b. By IH for k(b) there exists p′′_{0} : {a_{0}, emb_{g}(k(b))}_{h_{0}}^{fin}↓. Therefore ⟨p′_{0}, p′′_{0}⟩ : {a_{0}, e_{0}}_{h_{0}}^{fin}↓, and we get {a, e}_{h}^{fin}[ ] = {a, k(b)}_{h}^{fin}[ ] = {a_{0}, emb_{g}(k(b))}_{h_{0}}^{fin}[ ] = {a_{0}, e_{0}}_{h_{0}}^{fin}[ ]. For assertion (b) assume p_{0} = ⟨p′_{0}, p′′_{0}⟩ : {a_{0}, h_{0}}_{e_{0}}^{fin}↓. We have p′_{0} : {h_{0}}^{finfun}(a′_{0})↓, and with b := {h_{0}}^{finfun}(a′_{0})[p′_{0}] : B(a′), p′′_{0} : {a_{0}, emb(k(b))}_{h_{0}}^{fin}↓. Let r′_{0} := callresults_{h_{0}}(emb(k(b)), p′′_{0}). Let r_{0} := r′_{0}[a′_{0} ↦ b]. By IH there exists r′ s.t. r′ ∘ g^{−1} = r′_{0}, p′′_{1} : {a, k(b)}_{r′}^{fin}↓. Let r := r′[a′ ↦ b], which is consistent since r_{0} is consistent and g is injective. r ∘ g^{−1} = r_{0}. There exist p′′ : {a, k(b)}_{r}^{fin}↓, p′ : {r}^{finfun}(a′)↓, and we get therefore ⟨p′, p′′⟩ : {a, e}_{r}^{fin}↓.

Definition 9.2 ((Embedding from C_{i} into the disjoint union of C_{i}) (a) For C, C′ : Fam(Set), C = ⟨A, B⟩, C′ = ⟨A′, B′⟩

emb_{inl,C,C′} := emb_{C,C⊕C′,λx.inl(x)}
: (a : A, Rec′_{C,a}) → Rec′_{C⊕C′,inl(a)} ,
emb_{inr,C,C′} := emb_{C′,C⊕C′,λx.inr(x)}
: (a : A′, Rec′_{C′,a}) → Rec′_{C⊕C′,inr(a)} .

(b) For I : Set, C : I → Fam(Set), C_{i} = ⟨A_{i}, B_{i}⟩, i : I let

emb_{i,C} := emb_{C_{i},⊕_{i:I}C_{i},λx.in_{i}(x)}
: (a : A_{i}, e : Rec′_{C_{i},a}) → Rec′_{⊕_{i:I}C_{i},in_{i}(a)} .

Lemma and Definition 9.3 Assume C = ⟨A, B⟩ : Fam(Set), C′ = ⟨A′, B′⟩ : Fam(Set).

(a) Assume e : Rec_{C}, e′ : Rec_{C′}. Then we can define e ⊕_{C,C′} e′ : Rec_{C⊕C′} s.t. the following holds (we usually omit the indices C, C′ of ⊕):

(i) For a : A, {e}(a) ≃ {e ⊕ e′}(inl(a)). (ii) For a : A′, {e′}(a) ≃ {e ⊕ e′}(inr(a)).

Note that we overload the notation ⊕.

(b) Assume e : (a : A) → Rec′_{C⊕C′,inl(a)}, e′ : Rec_{C′}. Then we can define e⊕_{C,C′}^{inr} e′ s.t. the following holds (we usually omit the indices C, C′ of ⊕^{inr}):

(i) For a : A, {e ⊕ e′}(inl(a)) ≃ {inl(a), e(a)}_{e⊕e′}^{aux}. (ii) For a : A′, {e′}(a) ≃ {e ⊕ e′}(inr(a)).

Again we usually omit the indices C, C′ of ⊕. Note that we overload the symbol ⊕.

(c) Assume e : Rec_{C}, e′ : (a : A′) → Rec′_{C⊕C′,inr(a)}, Then we can define e ⊕_{C,C′}^{inl} e′ s.t. a similar statement as in (b) holds. We usually omit the indices C, C′ of ⊕^{inl}.

Proof: (a):

e ⊕ e′ := λx.case x of inl(a) → emb_{inl}(a, e(a)) inr(a) → emb_{inr}(a, e′(a)) .

We show (1) ∀a : A.∀p : {e}(a)↓.∃p′ : {e ⊕ e′}(inl(a))↓.{e}(a)[p] = {e ⊕ e′}(inl(a))[p′].

(2) ∀a : A.∀p : {e ⊕ e′}(inl(a))↓.∃p′ : {e}(a)↓.{e}(a)[p′] = {e ⊕ e′}(inl(a))[p].

by induction on length(p). Then we obtain (i) (using uniqueness of elements of {e}(a)↓). Assertion (ii) follow similarly. Proof of (1): Assume a : A, p : {e}(a)↓, k := callresults_{e}(a, e(a), p). There exists p′ : {a, e(a)}_{k}^{fin}↓, and therefore p′_{0} : {inl(a), emb_{inl}(a, e(a))}_{k∘inl^{−1}}^{fin}↓ = {inl(a), (e ⊕ e′)(inl(a))}_{k∘inl^{−1}}^{fin}↓. By IH we have for a′ : A s.t. {k}^{finfun}(a′)↓ {k ∘ inl^{−1}}^{finfun}(inl(a′)) ≃ {k}^{finfun}(a′) ≃ {e}(a′) ≃ {e ⊕ e′}(inl(a′)). Therefore we obtain from p′_{0} some p_{0} : {inl(a), (e ⊕ e′)(inl(a))}_{e⊕e′}^{aux}↓ and {e}(a)[p] = {a, e(a)}_{k}^{fin}[p′] = {inl(a), (e ⊕ e′)(inl(a))}_{k∘inl^{−1}}^{fin}[p′_{0}] = {inl(a), (e ⊕ e′)(inl(a))}_{e⊕e′}^{aux}[p_{0}] = {e ⊕ e′}(inl(a))[tot_{e⊕e′,a_{0}}(p_{0})]. Statement (2) can be shown similarly. (b):

e ⊕ e′ := λx.case x of inl(a) → e(a) inr(a) → emb_{inr}(a, e′(a)) .

(i) follows by definition and (ii) follows as for (a).

(c) follows similarly.

We introduce now similar operations for the potentially infinite disjoint union of families of sets.

Lemma and Definition 9.4 Assume I : Set, C : I → Fam(Set), written as C_{i} for C(i). Let C_{i} = ⟨A_{i}, B_{i}⟩. Assume e : (i : I) → Rec_{C_{i}}. Then we can define ⊕_{i:I}e_{i} : Rec_{⊕_{i:I}C_{i}} s.t.

{e_{i}}(a) ≃ {⊕_{i:I}e_{i}}(in_{i}(a)) .

Proof: Straightforward generalisation of Lemma and Definition 9.3 (a).

10 Reference to Other Partial Recursive functions

If one wants to show the closure of the resulting set of partial recursive functions under operations like composition, one sees that one needs the possibility to refer to other partial recursive functions, which is not available in the above calculus. In the context of dependent type theory, allowing this will cause one problem: we want to refer in the definition of partial recursive functions to other partial recursive functions g of any type (c : C) ⇀ D(c) where ⟨C, D⟩ : Fam(Set). If we want to allow reference to arbitrary such functions, we will end up with Rec_{A,B} : Type instead of Rec_{A,B} : Set. (We will no longer suppress the arguments A, B of Rec.) This causes problems when defining partial recursive functions having elements of Rec_{A,B} as arguments. There are two solutions for this problems.

• One solution is to restrict the domain and codomain of partial recursive functions used to elements of a universe. Then Rec_{A,B} will be a set. If one is for instance interested in functions occurring in traditional computability theory only, one can restrict oneself to a universe {ℕ^{k} | k ∈ ℕ}, i.e. U := ℕ : Set and for n : ℕ T(n) := ℕ^{n} : Set.

• The other solution will be given in Sect. 13, where we will show that we can always restrict the domain and codomain of other functions used to specific sets, and that therefore Rec can be replaced by a set.

There are two alternative ways of dealing with references to other partial recursive functions:

1. The conceptually easier one is to treat such references as recursive calls of simultaneously defined functions. In order to represent f : (a : A) ⇀ B(a) which makes use of g : (a : A′) ⇀ B′(a), we combine f, g into one function fg : (a : A′′) ⇀ B′′(a), where C := ⟨A, B⟩, C′ := ⟨A′, B′⟩, C′′ := C ⊕ C′, C′′ = ⟨A′′, B′′⟩. Let f be given as an element of (a : A) → Rec′_{C′′,inl(a)}, g be given as an element of Rec_{C′}. Then we can represent f and g as one function fg := f ⊕^{inr} g. In general we define

Rec_{0,C}^{+} := ΣC′ : Fam(Set).Rec_{C⊕C′} ,

and for e = ⟨C′, e′⟩ : Rec_{0,A,B}^{+} we define

{e}_{0} : A → PrePar(B(a)) ,
{e}_{0}(a)↓ := {e′}_{0}(inl(a))↓ ,
{e}_{0}(a)[p] := {e′}_{0}(inl(a))[p] .

2. The approach which is makes it easier to define partial recursive functions is to extend Rec by a constructor which calls a partial recursive function having an arbitrary type. So we extend Rec_{C}, Rec′_{C,a} to types Rec_{1,C}^{+}, Rec_{1,C,a}^{+,′} with an additional constructor call as follows (We write Arg_{1}, Eval_{1}, {·}_{1} for the variants of Arg, Eval, {·}, respectively, which refer to Rec_{1}^{+}):

call : (C′ : Fam(Set), e : Rec_{1,C′}^{+}, a′ : C′.A, g : C′.B(a′) → Rec_{1,C,a}^{+,′})

→ Rec_{1,C,a}^{+,′} , Arg_{1,a,call(C′,e,a′,g)}(X, Y) = Σp : {e}_{1,C′}(a′)↓.Arg_{1,a,g({e}_{1,C′} (a′)[p])}(X, Y) , Eval_{1,a,call(C′,e,a′,g)}(X, Y, ⟨p, q⟩) = Eval_{1,a,g({e}_{1,C′} (a′)[p])}(X, Y, q) .

If we extend {a, e′}_{e}^{aux} in a straightforward way to an operation {a, e′}_{1,e}^{aux} having arguments e : Rec_{1}^{+}, a : A, e′ : Rec_{1,a}^{+,′}, then we obtain in the special case e′ = call(C′, e′′, a′, g)

{a, e′}_{1,e}^{aux}↓ = Σp : {e′′}_{1,C′}(a′)↓.({a, g({e′′}_{1,C′}(a′)[p])}_{1,e}^{aux}↓ ,
{a, e′}_{1,e}^{aux}[⟨p, q⟩] = {a, g({e′′}_{1,C′}(a′)[p])}_{1,e}^{aux}[q] .

We defined as well the variant {·, ·}_{1,·}^{fin} of {·, ·}_{·}^{aux} using finitary approximations of functions (a : A) → B(a). In case of e = return(b) or e = rec(a, g), it is defined as for {·, ·}_{·}^{fin}. In case of e = call(C′, e′′, a′, g), the definition is as follows:

{a, e′}_{1,h}^{fin}↓ = Σp : {e′′}_{1,C′}(a′)↓.({a, g({e′′}_{1,C′}(a′)[p])}_{1,h}^{fin}↓) ,
{a, e′}_{1,h}^{fin}[⟨p, q⟩] = {a, g({e′′}_{1,C′}(a′)[p])}_{1,h}^{fin}[q] .

Furthermore, calls_{e}(a, e′, p) is extended to calls_{1,e}(a, e′, p) for e : Rec_{1}^{+}, a : A, e′ : Rec_{1,a}^{+,′}, p : {a, e′}_{1,e}^{aux}↓ by extending the previous definition and defining

calls_{1,e}(a, call(C′, e′′, a′, g′), ⟨p, p′⟩) := calls_{1,e}(g′({e′′}_{1}(a′)[p]), p′) .

Note that with this approach Rec_{1,C}^{+} : Type are defined simultaneously for all C : Fam(Set) and simultaneously with {·}_{1,C}(·)↓, {·}_{1,C}(·)[·], Arg_{1}, Eval_{1}.

The induction principle for Rec_{1,C,a}^{+,′} is now simultaneously for all ⟨C, a, e⟩

s.t. C : Fam(Set), a : C.A, and e : Rec_{1,C,a}^{+,′}. In case of call(C′, e′′, a′, g′) :

Rec_{1,C,a}^{+,′} the induction hypothesis is for ⟨C′, e′′(a′′), a′⟩ (for all a′′ : C′.A) and ⟨C, g′(b), a⟩ for b : C′.B(a′). The induction principle for p : {e}_{1}(a)↓ will not refer to calls_{1,e}(a, e′, p), but to a finite set (which we will not define explicitly here; more precisely it is a type rather than a set), which determines all ⟨C′, e′, a′, p′′⟩ s.t. e′ : Rec_{1,C′}^{+}, a′ : C′.A, p′′ : {e′}_{1,C′}(a′)↓ are referred to in p. So in case of ⟨call(C′, e′′, a′, g′), ⟨p, p′⟩⟩, this contains ⟨C′, e′′, a′, p⟩ and the elements referred to in p′. We can define for e : Rec_{1,C}^{+} a course of value recursion principle: Define

for e : Rec_{1,C,a}^{+,′} all pairs ⟨C′, e′⟩ s.t. C′ : Fam(Set), e′ : Rec_{1,C′}^{+,′} occurs in e, and call them subterms of e. For instance in case of call(C′, e′, a′, g′), these subterms would be ⟨C′, e′⟩, all subterms of e′(a′′) (where a′′ : C′.A), and all subterms of ⟨C, g(b)⟩ (where b : C′.B(a′)). We sometimes talk more loosely as e′ instead of ⟨C′, e′⟩ as being a subterm of e. The subterms of e : Rec_{1,C}^{+} are the subterms of e(a) for a : C.A. Then course of value induction states that a property holds if from the property holding for all subterms of e we can infer the property for e itself.

Remark 10.1 (Evaluation of elements of Rec_{0}^{+}, Rec_{1}^{+}) (a) We can easily lift the evaluation of elements of e : Rec_{A,B} to elements of e : Rec_{0,A,B}^{+} by defining {·}_{0}^{comp} : (e : Rec_{0,A,B}^{+}, a : A) → Par(B(a)), {e}_{0}^{comp}(a) := {π_{1}(e)}^{comp}(inl(a)). From the evaluation method for {·}^{comp} we obtain therefore an evaluation method for {·}_{0}^{comp} and therefore for {·}_{0}.

(b) In case of Rec_{1,A,B}^{+}, to define such an evaluation in a direct way would require a bit more work, although it is not too difficult. However, since in the next section we show how to translate elements of Rec_{1}^{+} into elements of Rec_{0}^{+}, we obtain via this translation and (a) an evaluation method for Rec_{1}^{+}.

11 Proof of the Equivalence of the Two Versions of Rec^{+}.

We show that Rec_{0}^{+} and Rec_{1}^{+} are equivalent.

Theorem 11.1 There exist functions trans_{0,1}^{+} : Rec_{0}^{+} → Rec_{1}^{+} and trans_{1,0}^{+} : Rec_{1}^{+} → Rec_{0}^{+} s.t. for e : Rec_{0}^{+}, e′ : Rec_{1}^{+}, a : A, the following holds:

(a) {e}_{0} ≅ {trans_{0,1}^{+}(e)}_{1}.

(b) {e′}_{1} ≅ {trans_{1,0}^{+}(e′)}_{0}.

Definition of trans_{0,1}^{+} and proof of (a): First note that Rec can be embedded in a straightforward way into Rec_{1}^{+} (by induction on Rec) s.t. {e}(·)↓ and {e}(·)[·] are preserved in the usual way (this proof is by induction on the length of the element of {e}(a)↓ or {e}_{1}(a)↓ respectively). We identify Rec with the subset of Rec_{1}^{+} and do not mention in the following the embedding operation. We first define trans_{0,1}^{+}: Assume e : Rec_{0,C}^{+}, e = ⟨C′, e′⟩, where C′ : Fam(Set), e′ : Rec_{C⊕C′}. Assume C = ⟨A, B⟩, C′ = ⟨A′, B′⟩. Let trans_{0,1}^{+}(e) := e_{0} : Rec_{1,C}^{+}, where

e_{0} := λa : A.call(C ⊕ C′, e′, inl(a), λb : B(a).return(b)) .

We have (using the identification of Rec with a subset of Rec_{0}^{+}) that

\begin{matrix}\{e_{0}\}_{1}(a)↓ = \{e′\}_{1}(inl(a))↓ × \{∗\} = \{e\}_{0}(a)↓ × \{∗\} , \\ \{e_{0}\}_{1}(a)[⟨p, ∗⟩] = \{e′\}_{1}(inl(a))[p] = \{e\}_{0}(a)[p] . \end{matrix}

Therefore the assertion follows. Definition of trans_{1,0}^{+} and proof of (b): The idea for the translation is to to first collect all ⟨C′_{i}, e′_{i}⟩, s.t. call(C′_{i}, e′_{i}, …) occurs in a given element of Rec_{1}^{+}, into one function ⟨⊕_{i:I}C′_{i}, ⊕_{i:I}e′_{i}⟩. Then replace, using the IH, e′_{i} by e′′_{i} : Rec_{0}^{+} which correspond to some e′′′_{i} : Rec_{C′′′}. Now construct from e and e′′′_{i} an ẽ : Rec_{C⊕C′′′}, s.t. {ẽ}(inl(a)) ≃ {e}_{1}(a), where references to some {e′_{i}}_{1}(a′) in e by using the constructor call are replaced by recursive calls to inr(⟨i, inl(a′)⟩), and {ẽ}(inr(⟨i, a⟩)) ≃ {e′′′_{i}}(a) is obtained by lifting of e′′′_{i}. We first define a translation of elements of Rec_{1,C,a}^{+,′}. For this we need a corresponding notation for Rec_{0}^{+}. In this notation, we refer to a family of functions e′′ : (i : D.I) → Rec_{1,D.C(i)}^{+}, which are the functions e′′(i) s.t. call(D.C(i), e′′(i), …) occurs in the code e for the partial recursive function to be translated. Note that e′′(i) : Rec_{1}^{+}, and not e′′(i) : Rec_{0}^{+}: at this stage we do not know yet how to translate e′′(i) into an element of Rec_{0}^{+}. This will then be done in the proof of the theorem by using the IH (for which we need the fact that e′′(i) is a subterm of e).

Definition 11.2 (a) Assume D = ⟨I, C⟩ : Fam(Fam(Set)), i.e. I : Set, C : I → Fam(Set). Then D.I := I, D.C := C, ⊕D := ⊕_{i:I}C(i).

(b) If C : Fam(Set), D : Fam(Fam(Set)), then ⊕(C, D) := C ⊕ (⊕D))

(c) Assume C = ⟨A, B⟩ : Fam(Set), a : A.

Rec_{0,C,a}^{+,′} := ΣD : Fam(Fam(Set)).Rec′_{⊕(C,D),inl(a)} × (i : D.I) → Rec_{1,D.C(i)}^{+} .

The translation from Rec_{1,C,a}^{+,′} to Rec_{0,C,a}^{+,′} is as follows:

Lemma and Definition 11.3 Assume C = ⟨A, B⟩ : Fam(Set), a : A. We can define

trans′_{1,0} : (a : A, e : Rec_{1,C,a}^{+,′}) → Rec_{0,C,a}^{+,′} ,

s.t. the following holds: Assume trans′_{1,0}(a, e) = ⟨D, e′, e′′⟩. Let C̃′ := ⊕(D), C̃′ = ⟨Ã′, B̃′⟩, C̃ := ⊕(C, D), C̃ = ⟨Ã, B̃⟩.

(a) Assume g : (a : A) ⇀_{fin} B(a) s.t. p : {a, e}_{1,g}^{fin}↓. Then there exists g′ : (a : Ã) ⇀_{fin} B̃(a) s.t. the following holds:

• {g′}^{finfun}(inl(a′)) ⊑ {g}^{finfun}(a′).

• {g′}^{finfun}(inr(in_{i}(a′))) ⊑ {e′′(i)}_{1}(a′).

• {a, e}_{g}^{fin} ≃ {inl(a), e′}_{1,g′}^{fin}.

(b) Assume g′ : (a : Ã) ⇀_{fin} B̃(a) s.t. p′ : {inl(a), e′}_{1,g′}^{fin}↓.

Assume that {g′}^{finfun}(inr(in_{i}(a′))) ⊑ {e′′(i)}_{1}(a′). Then there exists g : (a : A) ⇀_{fin} B(a) s.t. the following holds:

• {g}^{finfun}(a′) ⊑ {g′}^{finfun}(inl(a′)).

• {a, e}_{g}^{fin} ≃ {inl(a), e′}_{1,g′}^{fin}.

(c) e′′(i) are subterms of e.

Proof of Lemma and Definition 11.3: We write briefly trans′ instead of trans′_{1,0} in this proof, which is carried out by induction on e. We note that if g′ is defined depending on g s.t. the conditions of statement (a) hold, or g is defined depending on g′ s.t. the conditions of statement (b) hold, then it is automatically consistent, even if g, g′ was introduced only as a multivalued finite function rather than a finite function. So we do not have to care about giving proofs of consistency.

• Case e = return(b): trans′(a, e) := ⟨∅, return(b), λx.efq(x)⟩. The assertions follow trivially.

• Case e = rec(a′, h): We make the following definitions

trans′(a, h(b)) =: ⟨D_{b}, e′_{b}, e′′_{b}⟩  (for b : B(a′); given by IH) ,
D_{b} =: ⟨I_{b}, C′_{b}⟩ ,  C′_{b} =: ⟨A′_{b}, B′_{b}⟩ ,
I_{0} := Σ_{b:B(a)}I_{b} : Set ,
C′_{0} : I_{0} → Fam(Set) , C′_{0}(⟨b, i⟩) := C′_{b}(i) ,
e′′_{0} : (i : I_{0}) → Rec_{1,C′_{0}(i)}^{+} ,
e′′_{0}(⟨b, i⟩) := e′′_{b}(i) ,
D_{0} := ⟨I_{0}, C′_{0}⟩ : Fam(Set) ,
C̃′ := ⊕(D_{0}) ,  C̃′ =: ⟨Ã′, B̃′⟩ ,
C̃ := ⊕(C, D_{0}) ,  C̃ =: ⟨Ã, B̃⟩ ,
C̃′_{b} := ⊕(D_{b}) ,  C̃′_{b} =: ⟨Ã′_{b}, B̃′_{b}⟩ ,
C̃_{b} := ⊕(C, D_{b}) ,  C̃_{b} =: ⟨Ã_{b}, B̃_{b}⟩ ,
k_{b} : Ã_{b} → Ã ,  k_{b}(inl(a)) := inl(a) ,
k_{b}(inr(in_{i}(a))) := inr(in_{⟨b,i⟩}(a)) , (note that k_{b} is injective) ,
e′_{0} := rec(inl(a′), λb : B(a′).emb_{k_{b}}(e′_{b})) .

Then

trans′(a, e) := ⟨D_{0}, e′_{0}, e′′_{0}⟩ .

Condition (c) holds by IH.

We show (a): Assume g : (a : A) ⇀_{fin} B(a), ⟨p_{0}, p_{1}⟩ : {a, e}_{1,g}^{fin}↓, i.e. p_{0} : {g}^{finfun}(a′)↓, and with b := {g}^{finfun}(inl(a′))[p_{0}], p_{1} : {a, h(b)}_{1,g}^{fin}↓. By IH we have g′_{1} : (a : Ã_{b}) ⇀_{fin} B̃_{b}(a) s.t. the assertion holds for k(b), g, g′_{1}. Let g′_{2} := g′_{1} ∘k^{−1}, g′ := g′_{2}[inl(a′) ↦ b]. One can easily see that g′ is in relationship to g according to (a) and therefore consistent. By IH we have p′_{1} : {inl(a), e′_{b}}_{g′_{1}}^{fin}↓, therefore p′′_{1} : {inl(a), emb_{k_{b}}(e′_{b})}_{g′_{2}}^{fin}↓, therefore p′′′_{1} : {inl(a), emb_{k_{b}}(e′_{b})}_{g′}^{fin}↓. Furthermore, p′′′_{0} : {g′}^{finfun}(inl(a′))↓. Therefore p′′′ := ⟨p′′′_{0}, p′′′_{1}⟩ : {inl(a), e′_{0}}_{g′}^{fin}↓, and we have {inl(a), e′_{0}}_{g′}^{fin}[p′′′] = {inl(a), emb_{k_{b}}(e′_{b})}_{g′}^{fin}[p′′′_{1}] = {inl(a), emb_{k_{b}}(e′_{b})}_{g′_{2}}^{fin}[p′′_{1}] = {inl(a), e′_{b}}_{g′_{1}}^{fin}[p′_{1}] = {a, h(b)}_{1,g}^{fin}[p_{1}] = {a, e}_{1,g}^{fin}[p].

(b) follows similarly.

Case e = call(Ĉ, ê, â, h). Let Ĉ = ⟨Â, B̂⟩, and for b : B̂(â), trans′(a, h(b)) = ⟨D_{b}, e′_{b}, e′′_{b}⟩, D_{b} = ⟨I_{b}, C′_{b}⟩. Let D_{0} := ⟨I_{0}, C′_{0}⟩ where I_{0} := {∗} + Σ_{b:B(a)}.I_{b}, C′_{0}(inl(∗)) = Ĉ, C′_{0}(inr(⟨b, i⟩)) = C_{b}(i). Let e′′_{0} : (i : I_{0}) → Rec_{1,C′_{0}(i)}^{+},

e′′_{0}(inl(∗)) := ê, e′′_{0}(inr(in(⟨b, i⟩))) = e′′_{b}(i). Let C̃′ = ⟨Ã′, B̃′⟩, C̃ = ⟨Ã, B̃⟩, C̃′_{b} = ⟨Ã′_{b}, B̃′_{b}⟩, C̃_{b} = ⟨Ã_{b}, B̃_{b}⟩ as before. Let k_{b} : Ã_{b} → Ã, k_{b}(inl(a)) = inl(a), k_{b}(inr(in_{i}(a))) = inr(in_{inr(⟨b,i⟩)}(a)). k_{b} is injective. Then define

e′_{0} := rec(inr(inl(∗)), â, λb : B̂(a).emb_{k_{b}}(e′_{b})) ,
trans′(a, e) := ⟨D_{0}, e′_{0}, e′′_{0}⟩ ,

and the assertions (a) - (c) follow as in the previous case.

Proof of Theorem 11.1, direction trans_{1,0}^{+} : Rec_{1}^{+} → Rec_{0}^{+}. We write in this part of the proof trans for trans_{1,0}^{+}, trans′ for trans′_{1,0}. If we do not suppress the parameter C, we write trans_{C}, trans′_{C}. We first define trans_{C}(e) by induction on e, simultaneously for all C : Fam(Set): Assume a : A,

trans′(a, e(a)) = ⟨⟨I_{a}, C′_{a}⟩, e′_{a}, e′′_{a}⟩ ,

where, with

C̃′_{a} := C ⊕ ⊕_{i:I_{a}}C′_{a}(i) = ⟨Ã′_{a}, B̃′_{a}⟩ ,

we have

e′_{a} : Rec_{C̃′_{a},inl(a)} ,  e′′_{a} : (i : I_{a}) → Rec_{1,C′_{a}(i)}^{+} .

By IH

trans_{C′_{a}(i)}(e′′_{a}(i)) = ⟨C′′_{a}(i), e′′′_{a}(i)⟩ .

where, with

C′′′_{a}(i) := C′_{a}(i) ⊕ C′′_{a}(i) = ⟨A′′′_{a}(i), B′′′_{a}(i)⟩ ,

we have e′′′_{a}(i) : Rec_{C′′′_{a}(i)}. Let

\begin{aligned}C̃′′_{a} & := & C ⊕ ⊕_{i:I_{a}}C′′′_{a}(i) & = & ⟨Ã′′_{a}, B̃′′_{a}⟩ , \\ C′′′′ & := & ⊕_{a:A} ⊕_{i:I_{a}} C′′′_{a}(i) & = & ⟨A′′′′, B′′′′⟩ , \\ C̃ & := & C ⊕ C′′′′ & = & ⟨Ã, B̃⟩ . \end{aligned}

Let

h_{C̃′_{a},C̃} : Ã′_{a} → Ã ,

h_{C̃′_{a},C̃}(inl(a′)) = inl(a′), h_{C̃′_{a},C̃}(inr(⟨i, a′⟩)) = inr(⟨a, ⟨i, inl(a′)⟩⟩). Let

h_{C′′′_{a}(i),C̃} : C′′′_{a}(i) → C̃ ,

h_{C′′′_{a}(i),C̃}(a′) = inr(⟨a, ⟨i, a′⟩⟩). Define trans(e) := ⟨C′′′′, ẽ⟩ : Rec_{0,C}^{+}, where ẽ: RecC̃,

ẽ(inl(a)) = emb_{h_{C̃′_{a},C̃}} (e′_{a}) ,
ẽ(inr(⟨a, ⟨i, a′⟩⟩)) = emb_{h_{C{′′′ \atop a}(i),C̃}} (e′′′_{a}(i)) .

We show

∀C : Fam(Set).∀e : Rec_{1,C}^{+}.∀a : C.A.{e}_{1}(a) ⊑ {trans_{C}(e)}_{0}(a) ,

i.e.

∀C : Fam(Set).∀e : Rec_{1,C}^{+}.∀a : C.A.∀p : {e}_{1}(a)↓.∃p′ : {trans_{C}(e)}_{0}(a)↓.
{e}_{1}(a)[p] = {trans_{C}(e)}_{0}(a)[p′] .

This statement will be shown by induction on p, simultaneously for all C, e. Assume C, e, a, p as in the assertion, and all the variables as used in the definition of trans_{C}(e). Let k := calls_{1,C,e}(a, p) : (a : A) ⇀_{fin} B(a). We get p′ : {a, e(a)}_{1,C,k}↓. By Lem. 11.3 there exists k′ : (a′ : Ã_{a}) ⇀_{fin} B̃_{a}(a′) s.t.

{k′}^{finfun}(inl(a′)) ⊑ {k}^{finfun}(a′) ,
{k′}^{finfun}(inr(⟨i, a′⟩)) ⊑ {e′′_{a}(i)}_{1}(a′) ,
{inl(a), e′_{a}}_{k′}^{fin}↓ .

Let

k′′ := k′ ∘ (h_{C̃′_{a},C̃})^{−1} : (a′ : Ã) ⇀_{fin} B̃(a′) .

Then we get {inl(a), emb_{h_{C̃′_{a},C̃}} (e′_{a})}_{k′′}^{fin}↓ and therefore {inl(a), ẽ(inl(a))}_{k′′}^{fin}↓. If {k′′}^{finfun}(inl(a′))↓, then

\{k′′\}^{finfun}(inl(a′)) ≃ \{k′\}^{finfun}(inl(a′)) ≃ \{k\}^{finfun}(a′) ≃ \{e\}_{1}(a′) {IH \atop ≃} \{ẽ\}(inl(a′)). If {k′′}^{finfun}(inr(a′))↓, then a′ = ⟨a, ⟨i, inl(a′′)⟩⟩, {k′′}^{finfun}(inr(a′)) ≃ {k′}^{finfun}(inr(⟨i, a′′⟩)) ≃ {e′′_{a}(i)}_{1}(a′′)

{IH \atop ≃} \{e′′′_{a}(i)\}(inl(a′′)) ≃ \{ẽ\}(inr(⟨a, ⟨i, inl(a′′)⟩⟩)) ≃ \{ẽ\}(inr(a′)).

So we obtain k′′ ⊆ {ẽ}. By {inl(a), ẽ(inl(a))}_{k′′}^{fin}↓ therefore {inl(a), ẽ(inl(a))}aux ; ẽ↓,

{ẽ}(inl(a))↓ .

Similarly we obtain {e}_{1}(a)[ ] = {ẽ}(inl(a))[ ]. The other direction, i.e.

∀C : Fam(Set).∀e : Rec_{1,C}^{+}.∀a : C.A.{trans_{C}(e)}_{0}(a) ⊑ {e}_{1}(a) ,

can be shown in the same way.

12 Closure Properties of Representable Partial Recursive Functions

Notation 12.1 (a) In this section we consider partial objects constructed from other partial objects in the usual way. For instance {e_{0}}(⟨a, {e_{1}}(b)⟩) is the partial object e s.t.

\begin{aligned}e↓ & := & Σp : \{e_{1}\}(b)↓.\{e_{0}\}(⟨a, \{e_{1}\}(b)[p]⟩)↓ , \\ e[⟨p, q⟩] & := & \{e_{0}\}(⟨a, \{e_{1}\}(b)[p]⟩)[q] . \end{aligned}

Other composed partial objects are to be understood similarly.

(b) Let in this section (a : A) ⇀ B(a) := Rec_{A,B}, (a : A) ⇀_{0} B(a) := Rec_{0,A,B}^{+}, (a : A) ⇀_{1} B(a) := Rec_{1,A,B}^{+}. Furthermore (a : A) ⇀ (b : B) ⇀ C(a, b) := (⟨a, b⟩ : Σa : A.B(a)) ⇀ C(a, b), similarly for longer versions and ⇀_{0}, ⇀_{1}. When e is such a Curried version, we write {e}(a, b) instead of {e}(⟨a, b⟩), similarly for longer versions.

We could deal with more complex partial objects as mentioned in Notation 12.1 (a) by defining operations like ⟨·, ·⟩_{right} : A → PrePar(B) → PrePar(A × B), or compose : (A → PrePar(B)) → PrePar(A) → PrePar(B), and then replacing ⟨a, {e_{1}}(b)⟩ as in the example by e_{2} := ⟨a, {e_{1}}(b)⟩′, and {e_{0}}(e_{2}) by compose(λa.{e_{0}}(a), e_{2}). We leave it to the reader to make this more formal.

Remark 12.2 We prove in the following closure properties of partial recursive functions, using the version of ⇀_{1}, since in that version they are most easily expressed. By the last statement (h), these closure properties hold as well for ⇀_{0}. One could as well prove these closure properties directly in ⇀_{0}, with a little bit of more effort. This means that the more complex induction principle used for defining ⇀_{1} is not needed for proving those closure properties.

Theorem and Definition 12.3 (Closure Properties of Partial Recursive Functions)

(a) (Closure under total functions) Assume ⟨A, B⟩ : Fam(Set), f : (a : A) → B(a). Then we can define totToPar(f) : (a : A) ⇀_{1} B(a) s.t. {totToPar(f)}(a) ≃ b ↔ f(a) = b.

(b) (Composition) Assume ⟨A, B⟩ : Fam(Set), D : A → Set. If e′ : (a : A) ⇀_{1} B(a) and e : (a : A) ⇀_{1} B(a) ⇀_{1} D(a), then there we can define e ∘ e′ : (a : A) ⇀_{1} D(a) s.t. {e ∘ e′}(a) ≃ {e}(a, {e′}(a)). We define as well the following special forms of composition:

• If A, B, D : Set, e′ : A ⇀_{1} B, e′′ : B ⇀_{1} D then e′ ∘_{1} e : A ⇀_{1} D s.t. {e′ ∘_{1} e}(a) ≃ {e′}({e}(a)).

• If A, B : Set, D : A → B → Set, E : B → Set, F : A → Set, e_{2} : (a : A) ⇀_{1} Σb : B.D(a, b), e_{1} : (b : B) ⇀_{1} E(b), e_{0} : (a : A) ⇀_{1} (b : B(a)) ⇀_{1} (d : D(a, b)) ⇀_{1} (d′ : E(b)) ⇀_{1} F (a). Then we have e_{0} ∘_{2} e_{1} ∘_{2} e_{2} : (a : A) ⇀_{1} F (a) s.t. {e_{0}∘_{2}e_{1}∘_{2}e_{2}}(a) ≃ {e_{0}}(a, π_{0}({e_{2}}(a)), π_{1}({e_{2}}(a)), {e_{1}}(a, π_{0}({e_{2}}(a)))).

Furthermore when writing compositions we often use total functions f and then write f instead of totToPar(f). We will often as well Curry f e.g. use instead of f : (⟨a, b⟩ : Σa : A.B(a)) → C(a, b) simply f : (a : A, b : B(a)) → C(a, b).

(c) We can define

evalrec^{aux} : (a : A) ⇀ (e : Rec′_{A,B,a}) ⇀ (e_{0} : (a : A) ⇀ B(a))
⇀ Σb : B(a).{a, e}_{e_{0}}^{aux} ≃ b ,

s.t. {evalrec^{aux}}(⟨a, e, e_{0}⟩) ≃ ⟨b, p⟩ ↔ {a, e}_{e_{0}}^{aux} ≃ b. Note that we are referring to ⇀ instead of ⇀_{1}.

(d) (Correct self-evaluation for elements of (a : A) ⇀ B(a)) We can define

evalrec : (e : (a : A) ⇀ B(a)) ⇀_{1} (a : A) ⇀_{1} B(a) ,
evalcorrect : (e : (a : A) ⇀ B(a)) ⇀_{1} (a : A)
⇀_{1} Σb : B(a).{e}(a) ≃ b ,

s.t. {evalcorrect}_{1}(e, a) ≃ ⟨b, p⟩ ↔ {evalrec}_{1}(e, a) ≃ b ↔ {e}(a) ≃ b. Note the use of ⇀ and ⇀_{1}.

(e) Partial recursive functions with correctness proofs.

If e : (a : A) ⇀_{1} B(a), then there exists

e′ : (a : A) ⇀_{1} Σb : B(a).{e}(a) ≃ b

s.t. {e′}(a) ≃ ⟨b, p⟩ ↔ {e}(a) ≃ b.

(f) (Primitive recursion) Assume A : Set, B : (a : A) → ℕ → Set,

\begin{aligned}e_{0} & : & (a : A) ⇀_{1} B(a, 0) , \\ e_{1} & : & (a : A) ⇀_{1} (n : ℕ) ⇀_{1} B(a, n) ⇀_{1} B(a, n + 1) . \end{aligned}

Then there exists e := primrec(e_{0}, e_{1}) : (a : A) ⇀_{1} (n : ℕ) ⇀ B(a, n) s.t. {e}(a, 0) ≃ {e_{0}}(a), {e}(a, n + 1) ≃ {e_{1}}(a, n, {e}(a, n)).

(g) (Closure under μ) Assume A : Set, e : A ⇀ ℕ ⇀ Bool. Then we can define

μ(e) : A ⇀_{1} ℕ ,

s.t.

{μ(e)}(a) ≃ n ↔ {e}(a, n) ≃ tt ∧ ∀k < n.{e}(a, n) ≃ ff .

We write μ(f) instead of μ(totToPar(f)). Furthermore we can define in case of f : A → ℕ → Bool

μ^{+}(f) : (a : A) → Σn : ℕ.atom(f(a, n))

s.t. μ^{+}(f) ≃ ⟨n, q⟩ ↔ μ(f) ≃ n. Furthermore we can define an internalised version μ_{0}^{+} : (f : (a : A) → ℕ → B(a)) ⇀_{1} (a : A) ⇀_{1} Σn : ℕ.atom(f(a, n)), s.t. {μ_{0}^{+}}_{1}(f, a) ≃ {μ^{+}(f)}_{1}(a).

(h) Except for (c) all the above closure properties hold as well with ⇀_{1} replaced by ⇀_{0}.

Proof: First (h) holds, since we can first translate all ingredients which are elements of ⇀_{0} into elements of ⇀_{1} , then apply the operation for ⇀_{1} and then translate it back into ⇀_{0} . Then one can easily see that the desired properties hold. In order to prove (a) - (g), we will usually only give the definition of the resulting partial recursive function – that the given property holds is straightforward. We will usually suppress the parameter C in call(C, e, a, k). (a): totToPar(e) := λa.return(f(a)). (b):

e ∘ e′ := λa : A.call( , e′, a, λb : B(a). call( , e, ⟨a, b⟩, λd : D(a).return(d))) .

The other composition operations can be defined similarly. (c):

evalrec^{aux}(a, return(b), e_{0}) := return(⟨b, q⟩) ,
evalrec^{aux}(a, rec(a′, h), e_{0}) := rec(\begin{matrix}⟨a′, e_{0}(a′), e_{0}⟩, \\ λ⟨b, p⟩ : Σb : B(a′).\{a′, e_{0}(a′)\}_{e_{0}}^{aux} ≃ b. rec(\begin{matrix}⟨a, h(b), e_{0}⟩ \\ λ⟨b′, p′⟩ : Σb : B(a).\{a, h(b)\}_{e_{0}}^{aux} ≃ b′. return(⟨b′, q′⟩))) , \end{matrix} \end{matrix}

where the proofs q, q′ are obtained from the parameters in an obvious way. The correctness condition follows now easily. (d): evalcorrect := λ⟨e, a⟩.call( , evalrec^{aux}, ⟨a, e(a), e⟩, λ⟨b, p⟩.return(⟨b, p′⟩)), where p′ : {e}(a) ≃ b is obtained from p : {a, e(a)}_{e}^{aux} ≃ b. evalrec is obtained by composing the first projection with evalcorrect. (e): We can define e_{0} : (a : A) ⇀_{0} B(a) s.t. ∀a : A.{e}_{1}(a) ≃ {e_{0}}_{0}(a). Let e_{0} = ⟨C_{1}, e_{1}⟩ with C_{1} = ⟨A_{1}, B_{1}⟩, e_{1} : (a : A + A_{1}) ⇀ [B, B_{1}](a) and {e_{0}}_{0}(a) ≃ {e_{1}}(inl(a)). Now define

e′ := λa : A.call(\begin{matrix}, evalcorrect, ⟨e_{1}, inl(a)⟩, \\ λ⟨b, p⟩ : (Σb : B(a).\{e_{1}\}(inl(a)) ≃ b). return(⟨b, p′⟩)) , \end{matrix}

where p′ : {e}_{1}(a) ≃ b is obtained from p. The assertion follows now easily. (f): primrec(e_{0}, e_{1}) := e where

e(a, 0) := call( , e_{0}, a, λb : B(⟨a, 0⟩).return(b)) ,
e(a, n + 1) := rec(\begin{matrix}⟨a, n⟩, \\ λb : B(⟨a, n⟩). \\ call( , e_{1}, ⟨a, n, b⟩, λb : B(⟨a, n + 1⟩).return(b))) . \end{matrix}

(g): We define first μ′(e) : A ⇀_{1} ℕ ⇀_{1} ℕ s.t.

{μ′(e)}_{1}(a, n) ≃ m ↔ m ≥ n ∧ {e}_{1}(a, m) ≃ tt ∧ ∀k < n.m ≤ k → {e}_{1}(a, m) ≃ ff .

μ′(e) := λ⟨a, m⟩.call(\begin{matrix}, e, ⟨a, m⟩, \\ λb : Bool.if b then return(m) else rec(⟨a, m + 1⟩, λk.return(k))) . \end{matrix}

It is easy to see that the desired property holds. Then μ(e) := μ′(e) ∘ (λa.⟨a, 0⟩).

Concerning μ^{+}(f) we obtain from μ(f) and part (e) of the theorem an

e′ : (a : A) ⇀_{1} Σn : ℕ.{μ(f)}_{1}(a) ≃ n ,

s.t. {e′}_{1}(a) ≃ ⟨n, p⟩ ↔ {μ(f)}_{1}(a) ≃ n. We have {μ(f)}_{1}(a) ≃ n → atom(f(a)) and obtain therefore a function h : (Σn : ℕ.{μ(f)}_{1}(a) ≃ n) → (Σn : ℕ.atom(f(n))). Now μ^{+}(f) := h ∘_{1} e′. The definition of μ_{0}^{+} is similar to that of μ^{+}(f) using the same steps, where in the first step we define

μ′_{0} : (f : (a : A) → B(a)) ⇀_{1} (a : A) ⇀_{1} (n : ℕ) ⇀ ℕ ,
μ′_{0}(f, a, n) := if f(a, n) then return(m) else rec(⟨f, a, m + 1⟩, λk.return(k)) .

Note that because f is total we do not need to use the self-evaluation function evalrec.

13 Normal Form Theorem, Size Problem, Self-Evaluation

Based on the evaluation of elements of Rec introduced in Sect. 6 and its correctness proof given in Sect. 7, we can derive the normal form theorem 13.1, which is similar to Kleene’s normal form theorem for partial recursive functions. This will allow to define a new type Rec_{2}^{+} of partial recursive functions (Theorem and Definition 13.3), which is equivalent to Rec_{0}^{+}, Rec_{1}^{+}, but an element of Set. This solves the size problem (that Rec_{0}^{+}, Rec_{1}^{+} are true types). Furthermore, using evalcorrect as defined in Theorem and Definition 12.3 (d) we can define self-evaluation for elements of Rec_{2}^{+}, including a version which computes as well a correctness proof.

13.1 The Normal Form Theorem for Rec_{1}^{+}

Theorem 13.1 (a) For e : Rec_{1,A,B}^{+} there exists f : A → ℕ → Bool and g : (a : A, n : ℕ, atom(f(a, n))) → B(a) s.t. for all a : A, b : B(a)

{e}_{1}(a) ≃ b ⇔ ∃n : ℕ.∃p : atom(f(a, n)).g(a, n, p) = b .

(b) (Normal Form Theorem) Depending on f, g as defined in (a) we can define a function h_{f,g} : (Σa : A.Σn : ℕ.atom(f(a, n))) → B(a), s.t. for all e : Rec_{1,A,B}^{+}

{e}_{1}(a) ≃ {h_{f,g} ∘ μ^{+}(f)}_{1}(a) .

(c) Let A_{0} : Set, A_{0} := Σf : (A → ℕ → Bool).Σg : (a : A, n : ℕ, atom(f(a, n))) → B(a).A. Let B_{0} : A_{0} → Set, B_{0}(⟨f, g, a⟩ := B(a). Then we can define k : Rec_{1,A_{0},B_{0}}^{+} s.t. {k}_{1}(⟨f, g, a⟩) ≃ {h_{f,g} ∘ μ^{+}(f)}_{1}(a).

Proof: (a): We have e′ : Rec_{1}^{+} s.t. {e}_{1}(a) ≃ {e′}_{0}(a). Let e′ = ⟨C′′, e′′⟩, C′′ = ⟨A′′, B′′⟩. Then {e′}_{0}(a) ≃ {e′′}(inl(a)). By Theorem 7.1 {e′′}(inl(a)) ≃ {e′′}^{comp}(inl(a)). Let f(a, n) := defined_{a}(Red_{e′′,inl(a)}^{n}(e′′(inl(a)))), g(a, n, p) := Extract_{a}(Red_{e′′,inl(a)}^{n}(e′′(inl(a))), p). We have by definition {e′′}^{comp}(inl(a)) ≃ b ↔ ∃n : ℕ.∃p : atom(f(a, n)).g(a, n, p) = b, i.e the assertion. (b): We define h_{f,g}(⟨a, n, p⟩) := g(a, n, p). Then the assertion follows immediately. (c):

k(⟨f, g, a⟩) := call( , μ_{0}^{+}, ⟨f, a⟩, λ⟨n, p⟩ : Σn : ℕ.Σp : atom(f(a, n)).return(h_{f,g}(⟨a, n, p⟩))) .

13.2 Solving the Size Problem

Theorem 13.2 For every C : Fam(Set) there exists C′ : Fam(Set) s.t.

∀e : Rec_{1,C}^{+}.∃e′ : Rec_{C⊕C′}.∀a : C.A.{e}_{1}(a) ≃ {e′}(inl(a)) .

Remark on the proof: The solution given in the following will use a lot of theory developed before and will result in a rather complex family C′. One could carry out this proof directly by implementing the function used in the normal form theory directly in Rec_{0}^{+}, and obtain a much simpler family C′. Proof: Let k as in Theorem 13.1 (c). Then for every e there exists f, g s.t. {e}_{1}(a) ≃ {k}_{1}(⟨f, g, a⟩). Let k′ : Rec_{0,C′′}^{+} s.t. {k}_{1}(b) ≃ {k′}_{0}(inl(b)) for some C. Let k′ = ⟨C′′′, k′′⟩, k′′ : Rec_{C′′⊕C′′′}. Let C′ := C′′ ⊕ C′′′. Assume e : Rec_{1,C}^{+} and let f, g be chosen as above. Let e_{0} : (a : A) → Rec′_{C⊕C′,inl(a)}, e_{0}(a) := rec(inr(inl(⟨f, g, a⟩)), λb : B(a).return(b)). Let e_{1} := e_{0} ⊕^{inr} k′′ : Rec_{C⊕C′}. Then {e_{1}}(inl(a)) ≃ {k′′}(inl(⟨f, g, a⟩)) ≃ {k}_{1}(⟨f, g, a⟩) ≃ {e}_{1}(a).

Theorem and Definition 13.3 ((Solution of the size problem for Rec_{C}) Assume the following definitions:

(a) Rec_{2,C}^{+} := Rec_{C⊕C′} : Set, where C′ is defined depending on C as in Theorem 13.2.

(b) For e : Rec_{2,C}^{+}, a : A let {e}_{2}(a) : PrePar(B(a)), {e}_{2}(a)↓ := {e}(inl(a))↓, {e}_{2}(a)[p] := {e}(inl(a))[p].

Then for e : Rec_{1,C}^{+} there exists e′ : Rec_{2,C}^{+} s.t. {e}_{1} ≅ {e}_{2}, and vice versa.

Proof: By the above.

13.3 Self-Evaluation for Rec_{2}^{+}

We write in this section (a : A) ⇀ B(a), (a : A) ⇀_{0} B(a), (a : A) ⇀_{1} B(a), (a : A) ⇀_{2} B(a) for Rec_{A,B}, Rec_{0,A,B}^{+}, Rec_{1,A,B}^{+}, Rec_{2,A,B}^{+}, respectively.

Theorem and Definition 13.4 For C = ⟨A, B⟩ : Fam(Set) There exists

(i) eval_{2,C} : (e : (a : A) ⇀_{2} B(a)) ⇀_{2} (a : A) ⇀_{2} B(a),

(ii) evalcorrect_{2,C} : (e : (a : A) ⇀_{2} B(a)) ⇀_{2} (a : A) ⇀_{2} Σb : B(a).{e}_{2}(a) ≃ b.

s.t.

(i) {eval_{2}}_{2}(⟨e, a⟩) ≃ {e}_{2}(a),

(ii) {evalcorrect_{2}}_{2}(⟨e, a⟩) ≃ ⟨b, p⟩ ↔ {e}_{2}(a) ≃ b.

Proof: Let ((a : A) ⇀_{2} B(a)) = ((a : Ã) ⇀ B̃(a)) where ⟨Ã, B̃⟩ = ⟨A, B⟩⊕⟨A′, B′⟩ for some A′, B′. There exists

evalcorrect : (e : (a : Ã) ⇀ B̃(a)) ⇀_{1} (a : Ã) ⇀_{1} Σb : B̃(a).{e}(a) ≃ b ,

s.t. {evalcorrect}_{1}(e, a) ≃ ⟨b, p⟩ ↔ {e}(a) ≃ b. By composing it with inl : A → Ã, and transferring p : {e}(inl(a)) ≃ b into p : {e}_{2}(a) ≃ b, and using ((a : A) ⇀_{2} B(a)) = ((a : Ã) ⇀ B̃(a)), we obtain some

e′ : (e : (a : A) ⇀_{2} B(a)) ⇀_{1} (a : A) ⇀_{1} Σb : B(a).{e}_{2}(a) ≃ b .

Now let evalcorrect_{2} be s.t. {evalcorrect_{2}}_{2}(d) ≃ {e′}_{1}(d). eval_{2} can be defined by composing evalcorrect_{2} with a projection. (Note that because of the equivalence of {·}_{1} and {·}_{2}, Rec_{2}^{+} is closed under the standard operations for forming partial recursive functions.)

14 Conclusion

In this paper we have explored the representation of partial recursive function by indexed inductive-recursive definitions. We have introduced a data type of partial recursive functions and we have seen how to (partial) recursively evaluate elements of this data type inside type theory. We have seen that reference to other partial recursive functions requires the extension of this data type and we have obtained two data types Rec_{0}^{+} and Rec_{1}^{+}, both of which are large types. Then we have shown that they are equivalent, and have proved a normal form theorem. This allowed to show that we can restrict the size of additional types needed, and therefore to introduce a fourth data type Rec_{2}^{+}, which is equivalent to Rec_{0}^{+} and Rec_{1}^{+}, but a small set. We have seen as well how to define self-evaluation inside Rec_{2}^{+} and how to find apart from results of the computed function as well proofs that it is correct. The data type Rec_{1}^{+} provided a very general recursion schema which allows to easily define general recursive functions while referring to the full type hierarchy. We believe that this general schema can be exploited further, for instance in generic programming – we could take codes for partial recursive functions and compute from them new codes.

14.1 Future Work

A fifth data type of partial recursive functions and the delay monad. We could define a fifth data type of partial recursive functions by referring to the normal form theorem and observing that for every partial recursive function e : Rec_{1}^{+} there exist functions f and g s.t. {e}_{1}(a) ≃ {h_{f,g} ∘ μ^{+}(f)}_{1}(a). Since f and g can be encoded into one function h : (a : A) → ℕ → ({∗} + B(a)), we could define

Rec_{3}^{+} := (a : A) → ℕ → ({∗} + B(a)) ,
{·}_{3} : Rec_{3}^{+} → (a : A) → Par(B(a)) ,
{h}_{3}(a)↓ := Σn : ℕ.Σb : B(a).f(a, n) = inr(b) ∧ ∀m < n.f(a, n) = inl(∗)
{h}_{3}(a)[⟨n, b, p, q⟩] := b .

By searching for the least n s.t. h(a, n) is of the form inr(b), we can compute {⟨f, g⟩}_{3}(a) inside type theory partial-recursively. It goes beyond this article to investigate this idea further (e.g. to show closure under standard operations for forming partial recursive functions). Note that this data type is closely related to the delay monad used in [Cap05]. Elements h of the functions from A into the delay monad for B, i.e. in (a : A) → B(a)^{ν} correspond directly to f : Rec_{3}^{+} s.t. we have n < m → (f(a, n) = inr(b)) → f(a, m) = inr(b): Assume h, and define f. We first unpack h(a) n times, e.g. replace step(b) by b and leave return(b) as it is. If we obtain return(b), f(a, n) = inr(b), otherwise f(a, n) = inl(∗). On the other hand, from f with the property before we can in an obvious way obtain an element h : (a : A) → B(a)^{ν} by using guarded recursion: First define f′ : (a : A, n : ℕ) → B(a)^{ν} by f′(a, n) = return(b), if f(a, n) = inr(b), and f′(a, n) = step(f′(a, n + 1)), if f(a, n) = inl(∗). Now define h(a) := f′(a, 0). Using extensional type theory we can see that the two translations are inverse to each other. We will leave it to a future paper to investigate this idea further.

Higher type recursion. The original motivation for this article was to be able to define functions which refer recursively to themselves as a whole. There was no room in this paper to investigate this idea further. However, we have some promising ideas how to pursue in this direction.

Provably correct programs. One of the main goals of developing the theory of dependent type theory is its use in program verification, which requires some suitable notion of partial recursive functions. It will be interesting to see in which sense the work of this article can be used in the verification of recursively defined programs. We belief that the idea that from a partial recursive function we were able to obtain a partial recursive function which computes the same result plus a correctness proof is of particular use in the area of program verification.

References

[BC05a] A. Bove and V. Capretta. Modelling general recursion in type theory. Mathematical Structures in Computer Science, 15(4):671–708, August 2005.

[BC05b] A. Bove and V. Capretta. Recursive functions with higher order domains. In P. Urzyczyn, editor, Typed Lambda Calculi and Applications., volume 3461 of LNCS, pages 116–130. Springer, 2005.

[Bov02a] A. Bove. General recursion in type theory. In H. Geuvers and F. Wiedijk, editors, Types for Proofs and Programs, International Workshop TYPES 2002, The Netherlands, LNCS 2646, pages 39–58, April 2002.

[Bov02b] A. Bove. General Recursion in Type Theory. PhD thesis, Department of Computing Science, Chalmers University of Technology, November 2002.

[Cap05] Venanzio Capretta. General recursion via coinductive types. Logical Methods in Computer Science, 1(2):1–18, 2005.

[Con83] Robert L. Constable. Partial functions in constructive formal theories. In Theoretical Computer Science, pages 1–18, 1983.

[Coq94] Thierry Coquand. Infinite objects in type theory. In H. Barendregt and T. Nipkow, editors, Selected Papers 1st Int. Workshop on Types for Proofs and Programs, TYPES’93, Nijmegen, The Netherlands, 24–28 May 1993, volume 806, pages 62–78. Springer-Verlag, Berlin, 1994.

[CS87] Robert L. Constable and Scott F. Smith. Partial objects in constructive type theory. In Proceedings, Symposium on Logic in Computer Science, 22-25 June 1987, Ithaca, New York, USA, pages 183–193. IEEE Computer Society, 1987.

[DS99] Peter Dybjer and Anton Setzer. A finite axiomatization of inductiverecursive definitions. In J.-Y. Girard, editor, Typed Lambda Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, pages 129–146, 1999.

[DS01] Peter Dybjer and Anton Setzer. Indexed induction-recursion. In R. Kahle, P. Schroeder-Heister, and R. Stärk, editors, Proof Theory in Computer Science, pages 93 – 113. LNCS 2183, 2001.

[DS03] Peter Dybjer and Anton Setzer. Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124:1 – 47, 2003.

[DS06] Peter Dybjer and Anton Setzer. Indexed induction-recursion. Journal of Logic and Algebraic Programming, 66:1 – 49, 2006.

[Dyb94] Peter Dybjer. Inductive families. Formal Aspects of Comp., 6:440–465, 1994.

[Dyb00] Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2):525–549, June 2000.

[GPZ99] Herman Geuvers, Erik Poll, and Jan Zwanenburg. Safe proof checking in type theory with y. In CSL ’99: Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic, pages 439–452. Springer-Verlag, 1999.

[ML84] Per Martin-Löf. Intuitionistic type theory. Bibliopolis, Naples, 1984.

[Nor88] Bengt Nordström. Terminating recursion. BIT, 28:605 – 619, 1988.

[NPS90] B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf’s type theory. An Introduction. Oxford University-Press, Oxford, 1990.

[Pal91] Erik Palmgren. A construction of type: Type in Martin-Löf’s partial type theory with one universe. J. Symb. Log., 56(3):1012–1015, 1991.

[Pau93] Lawrence C. Paulson. Constructing recursion operators in intuitionistic type theory. CoRR, cs.LO/9301102, 1993.

[PSH90] Erik Palmgren and Viggo Stoltenberg-Hansen. Domain interpretations of Martin-Löf’s partial type theory. Ann. Pure Appl. Logic, 48(2):135–196, 1990.

[PSH92] Erik Palmgren and Viggo Stoltenberg-Hansen. Remarks on Martin-Löf’s partial type theory. BIT, 32(1):70–83, 1992.

[Set06] Anton Setzer. Partial recursive functions in Martin-Löf Type Theory. In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors, Logical Approaches to Computational Barriers: Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006. Proceedings., pages 505 – 515. Springer Lecture Notes in Computer Science 3988, 2006.