Partial Recursive Functions in Martin-Löf Type Theory

Anton Setzer^{⋆}

Dept. of Computing Science, University of Wales Swansea, Singleton Park, Swansea SA2 8PP, UK. Tel.: +44 1792 513368, Fax: +44 1792 295651,

                    a.g.setzer@swan.ac.uk,
              http://www.cs.swan.ac.uk/~csetzer/

Abstract. In this article we revisit the approach by Bove and Capretta for formulating partial recursive functions in Martin-Löf Type Theory by indexed inductive-recursive definitions. We will show that all inductiverecursive definitions used there can be replaced by inductive definitions. However, this encoding results in an additional technical overhead. In order to obtain directly executable partial recursive functions, we introduce restrictions on the indexed inductive-recursive definitions used. Then we introduce a data type of partial recursive functions. This allows to define higher order partial recursive functions like the map functional, which depend on other partial recursive functions. This data type will be based on the closed formalisation of indexed inductive-recursive definitions introduced by Dybjer and the author. All elements of this data type will represent partial recursive functions, and the set of partial recursive functions will be closed under the standard operations for forming partial recursive functions, and under the total functions. Keywords: Martin-Löf type theory, computability theory, recursion theory, Kleene index, Kleene brackets, partial recursive functions, inductive-recursive definitions, indexed induction-recursion.

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

⋆ Supported by EPSRC grant GR/S30450/01.

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 , eval_{f} : (n : ℕ, p : f(n)↓) → ℕ .

Here f(n)↓ expresses that f(n) is defined and eval_{f}(n, p) computes, depending on n : ℕ and a proof p : f(n)↓, the value 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 eval_{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)↓ ,  eval_{f}(0, defined_{f}^{0}) = 0 ,
defined_{f}^{S} : (n : ℕ, p : f(n)↓, q : f(eval_{f}(n, p))↓) → f(n + 1)↓ ,
eval_{f}(n + 1, defined_{f}^{S}(n, p, q)) = eval_{f}(eval_{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 eval_{f}(n+1, p′) = eval_{f}(m, q). We observe that defined_{f}^{S} refers to eval_{f}(n, p), so we have to define simultaneously f(·)↓ inductively, while defining eval_{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 have 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. Future work. With the above research we will be able to define functions referring to indices of other partial recursive functions. However, we will not yet be able to deal with mutually recursive functions, in which one function refers to another as a whole. In order to deal with this, we will in a follow-up paper introduce partial recursive functions with function arguments represented as oracles. We will then obtain a recursion theorem stating that recursion equations defined using this principle can always be solved.

2 Inductive-Recursive Definitions

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. Inductive-recursive definitions 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 were 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 non-inductive 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(eval_{f}(n, p))↓) → f(n + 1)↓ .

In order to avoid the use of eval_{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 eval_{f}^{aux} : (n : ℕ, p : f(n)↓^{aux}) → ℕ (this definition is now separated from the inductive definition of f(·) ↓) by

eval_{f}^{aux}(0, defined_{f}^{0,aux}) := 0 ,
eval_{f}^{aux}(n + 1, defined_{f}^{S,aux}(n, p, m, q)) := eval_{f}^{aux}(m, 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 = eval_{f}^{aux}(n, p). We introduce a correctness predicate expressing this:

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

One can now simulate f(·)↓ by

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

and simulate eval_{f} by

eval′_{f} : (n : ℕ, p : f(n)↓′) → ℕ , eval′_{f} (n, ⟨p, q⟩) := eval_{f}^{aux}(n, 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 directly executable partial recursive functions.

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.

eval_{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 this principle does not mean that the functions are directly executable, unless one has a proof of f(n)↓ (in which case eval_{f} allows of course to compute the value of f(n)). In order to evaluate f(n), one has to guess the arguments of the constructor in such a way that we obtain an element of f(n)↓, which requires in general a search process. f(n) is still partially recursive (the f(n) are always computable since one can always search for a proof p : f(n)↓, and then compute eval_{f}(n, p)), but we do not regard the search for arguments as a means of directly executing a function. In order to obtain directly executable partial recursive functions we need to determine for each index its constructor. 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(eval_{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(eval_{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 eval_{f}(n, p)). Another problem with non-trivial non-inductive arguments is that when evaluating the partial recursive function, one needs to search for instances of these noninductive argument. Therefore one does not obtain directly executable functions. We could allow non-indexed arguments indexed over the one-element set 1 and the empty set ∅. 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. However, such a search will miss the situation where (x : A) → f(i(x)) is true (even constructively), but unprovable in the type theory in question. Furthermore, we do not regard such a search process as a means of directly executing a function. So in order to obtain directly executable functions, we need to restrict inductive arguments to single valued ones, i.e. in the above situation to arguments of the form p : f(i)↓.

3 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 Kleene-index 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. 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 .

The set defined inductively by a code e : Rec is given as

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

If we understand each IIRD as defining a partial recursive function, f_{e}(a)↓ means that the function with index e is defined for argument a. The function defined recursively is

eval_{e} : (a : A, p : f_{e}(a)↓) → B(a) ,

which, if the IIRD is interpreted as the definition of a partial recursive function, computes the result of this function.

Rec is a restricted IIRD, which means that for each a : A we can determine the type of arguments for the constructor with result f_{e}(a)↓. Let Rec′_{a} be the type of codes for possible arguments for the constructor of an IIRD e with result f_{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 f_{e}(a)↓ and the result of eval_{e}(a, p) for the constructed element p will depend on f_{e}(·)↓ and eval_{e}. Since, when introducing Rec′_{a}, f_{e}(·)↓ and eval_{e} are not available, we define more generally, depending on a : A, e : Rec′_{a}, for general X and Y, having the types of f_{e}(·)↓, eval_{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)

Arg_{a,e(a)}(f_{e}(·)↓, eval_{e}) will be the type of the arguments of the constructor of f_{e}(a)↓. If using arguments p we have constructed q : f_{e}(a)↓, then eval_{e}(a, q) = Eval_{a,e(a)}(f_{e}(·)↓, eval_{e}, p). If we call the constructor for f_{e}(a)↓ tot_{e,a}, then the introduction and equality rules for f_{e}(·)↓ and eval_{e} are as follows:

tot_{e,a} : Arg_{a,e(a)}(f_{e}(·)↓, eval_{e}) → f_{e}(a)↓ ,
eval_{e}(a, tot_{e,a}(p)) = Eval_{a,e(a)}(f_{e}(·)↓, eval_{e}, p) .

We define additionally outside type theory for closed e : Rec the partial recursive function {e} : (a : A) ⇀ B(a). {e} will be defined in such a way that we can prove outside type theory {e}(a)↓ ⇔ ∃p.p : f_{e}(a)↓ and that if p : f_{e}(a)↓, then {e}(a) ≃ eval_{e}(a, p).

In order to define {e}(a), we define recursively (outside type theory) an auxiliary partial recursive function

compute^{aux} : (e : Rec, a : A, e′ : Rec′_{a}) ⇀ B(a)

compute^{aux}(e, a, e′) roughly speaking computes the subcomputation of {e}(a), where we consider the subcode e′ of e(a). However, in the definition we do not assume e′ to be a subcode of e(a). Then we define for e : Rec

{e}(a) ≃ compute^{aux}(e, a, e(a))

Rec′_{a} has 2 constructors:

1. Initial (constant) case: the constructor for f_{e}(a)↓ has no arguments (or more precisely the trivial argument x : {∗} for the one-element set {∗}). eval_{e}(a, p) returns, independently of p, a fixed element b : B(a):

const_{a} : B(a) → Rec′_{a} Arg_{a,const_{a}(b)}(X, Y) = {∗}
Eval_{a,const_{a}(b)}(X, Y, ∗) = b
compute^{aux}(e, a, const_{a}(b)) ≃ b

2. A single inductive argument. The constructor of f_{e}(a)↓ has as an inductive argument p : f_{e}(a′)↓, and depending on m : eval_{e}(a′, p) later arguments. As a partial recursive function this means that we make a recursive call to f_{e}(a′)↓. Depending on the result m, we choose further steps. So the constructor rec_{a} 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 eval_{e}(a′, p) the later arguments of the constructor. We obtain

rec_{a} : (a′ : A, e′ : B(a′) → Rec′_{a}) → Rec′_{a}
Arg_{a,rec_{a}(a′,e′)}(X, Y) = (x : X(a′)) × Arg_{a,e′(Y (a′,x))}(X, Y)
Eval_{a,rec_{a}(a′,e′)}(X, Y, ⟨x, y⟩) = Eval_{a,e′(Y (a′,x))}(X, Y, y)

compute^{aux}(e, a, rec_{a}(a′, g)) ≃ \{ \begin{matrix}compute^{aux}(e, a, g(b)), \\ if compute^{aux}(e, a′, e(a)) ≃ b, \\ ⊥, & if compute^{aux}(e, a′, e(a)) ↑. \end{matrix}

We usually omit the parameter a in const_{a}, rec_{a}. 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 const(b). Arg and Eval are then defined by recursion on Rec′_{a}. f_{e}(·)↓ and eval_{e} are given by an IIRD which is determined by e. 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). Here Fam(Set) := (X : Set) × (X → Set) : Type is the type of families of sets. 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. However, one can usually restrict the domain and codomain of partial recursive functions used to elements of a universe, and therefore obtain Rec_{A,B} to 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.

In order to keep the notations simple we will in the following extend Rec_{A,B} to Rec_{A,B}^{+} in such a way that it refers to partial recursive functions of arbitrary ⟨C, D⟩ : Fam(Set), which means it is a true type, and keep in mind that if ⟨C, D⟩ are restricted to elements of a universe, we obtain Rec_{A,B}^{+} : Set.

There are two alternative ways of dealing with reference 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) ⇀ C(a) which makes use of g : (a : A′) ⇀ C′(a), we combine f, g into one function fg : (a : A′′) ⇀ C′′(a) as follows: We have ⟨A, C⟩, ⟨A′, C′⟩ : Fam(Set). Define

⟨A, C⟩ ⊕ ⟨A′, C′⟩ := ⟨A + A′, [C, C′]⟩

where A + A′ is the disjoint union of A and A′ and

[C, C′] : (A + A′) → Set ,
[C, C′](inl(x)) := C(x) , [C, C′](inr(x′)) := C′(x′) .

Let ⟨A′′, C′′⟩ := ⟨A, C⟩ ⊕ ⟨A′, C′⟩. Then define

\begin{matrix}f ⊕ g : (a : A′′) ⇀ C′′(a) , \\ (f ⊕ g)(inl(a)) ≃ f(a) , (f ⊕ g)(inr(b)) ≃ g(b) . \end{matrix}

Define emb_{inl} : (a : A, Rec′_{A,C,a}) → Rec′_{A′′,C′′,inl(a)} and emb_{inr} : (a′ : A′, Rec′_{A′,C′,a′}) → Rec′_{A′′,C′′,inr(a′)}, by replacing all occurrences of rec(x, g) by rec(inl(x), g) or rec(inr(x), g), respectively. Let fg := f ⊕ g. Assume we can define f recursively by making use of g. We obtain an index e_{fg} of fg by setting e_{fg}(inr(b)) := e_{g}(b) and defining e_{fg}(inl(a)) like the recursive definition of f, but replacing recursive calls to f(a′) by recursive calls to fg(inl(a′)) and calls of g(b) by recursive calls to fg(inr(b)). As an example we show how to define, assuming g : (a : A) ⇀ C(a), h : (a : A) → C(a) ⇀ B(a), the function f : (a : A) ⇀ B(a) , f(a) ≃ h(a, g(a)) . Let C′ := (a : A) × C(a), B′ : C′ → Set, B′(⟨a, c⟩) := C(a). Let h′ : (c : C′) ⇀ B′, h′(⟨a, c⟩) := h(a, c) be the uncurried form of h. Let e_{g} : Rec_{A,C}, e_{h′} : Rec_{C′,B′} be indices for g and h′. Let ⟨A^{+}, B^{+}⟩ := ⟨A, B⟩ ⊕ ⟨A, C⟩ ⊕ ⟨C′, B⟩. Let fgh := f ⊕ g ⊕ h′. Let in_{f}, in_{g}, in_{h} be the left, middle and right injection from A, A, C′, respectively, into A^{+}. Let e′_{g} := λb.emb_{in_{g}}(e_{g}(b)) : (b : B) → Rec′_{A^{+},B^{+},in_{g}(b)} , e′_{h} := λc.emb_{in_{h}}(e_{h}(c)) : (c : C′) → Rec′_{A^{+},B^{+},in_{h}(c)} .

We introduce an index e_{fgh} : Rec_{A^{+},B^{+}} as follows:

e_{fgh}(in_{g}(b)) := e′_{g}(b) ,  e_{fgh}(in_{h}(c)) := e′_{h}(c)
e_{fgh}(in_{f}(a)) := rec(in_{g}(a), λc.rec(in_{h}(⟨a, c⟩), λb.const(b)))

Using extensional equality one can see that there is a bijection g^{≅}(a) : f_{e_{fgh}}(in_{g}(a))↓ ≅ f_{e_{g}}(a)↓, and we have eval_{e_{fgh}}(in_{g}(a), p) = eval_{e_{g}}(a, g^{≅}(a, p)), similarly for f_{e_{fgh}}(in_{h}(a))↓ and f_{e_{h}}(a)↓. Furthermore, the argument of the constructor tot_{e_{fgh},in_{f} (a)} for f_{e_{fgh}}(in_{f}(a))↓ has type

(p : f_{e_{fgh}}(in_{g}(a))↓) × (f_{e_{fgh}}(in_{h}(⟨a, eval_{e_{fgh}}(in_{g}(a), p)⟩))↓ × {∗}) ,

and we have

eval_{e_{fgh}}(in_{f}(a), tot_{e_{fgh},in_{f} (a)}(⟨p, ⟨q, ∗⟩⟩)
= eval_{e_{fgh}}(in_{h}(⟨a, eval_{e_{fgh}}(in_{g}(a), p)⟩), q)

Modulo the aforementioned isomorphisms, this means that f_{e_{fgh}}(in_{f}(a))↓ iff there exists p : f_{e_{g}}(a)↓ and q : f_{e_{h}}(⟨a, eval_{e_{g}}(a, p)⟩)↓, and that eval_{e_{fgh}}(in_{f}(a), ) = eval_{e_{h}}(⟨a, eval_{e_{g}}(a, p)⟩, q), i.e. the function defined by e_{fgh} composed with in_{f} is the composition of the functions given by e_{g} and e_{h}. In general we define

Rec_{A,B}^{+} := (C : Set) × (D : C → Set) × Rec_{C+A,[D,B]} ,

and for e = ⟨C, D, e′⟩ : Rec_{A,B}^{+} we define f_{e}^{+}(·)↓ : A → Set, f_{e}^{+}(a)↓ := f_{e′}(inr(a))↓ and eval_{e}^{+} : (a : A, p : f_{e}^{+}(a)↓) → B(a), eval_{e}^{+}(a, p) := eval_{e′}^{+}(inr(a), p).

2. The approach which is easier for implementing proofs is to extend Rec by a constructor which calls a partial recursive function having an arbitrary type. So we extend Rec_{A,B}, Rec′_{A,B,a} to types Rec_{A,B}^{+}, Rec_{A,B,a}^{+,′} with an additional constructor

call_{a} : (C : Set, D : C → Set, e : Rec_{C,D}^{+}, c : C, g : D(c) → Rec_{A,B,a}^{+,′})

→ Rec_{A,B,a}^{+,′} Arg_{a,call_{a}(C,D,e,c,g)}(X, Y) = (p : f_{C,D,e}(c)↓) × Arg_{a,g(eval_{C,D,e}(c,p))}(X, Y) Eval_{a,call_{a}(C,D,e,c,g)}(X, Y, ⟨p, q⟩) = Eval_{a,g(eval_{C,D,e}(c,p))}(X, Y, q)

Note that with this approach Rec_{C,D}^{+} : Type are defined simultaneously for all ⟨C, D⟩ : Fam(Set) and simultaneously with f_{C,D}(·)↓, eval_{C,D}, Arg, Eval.

With both approaches we can show the following theorem:

Theorem 3.1. (a) The type of partial recursive functions represented by Rec^{+} contains all total functions and is closed under composition, primitive recursion into higher types, and the μ-operator for partial recursive functions.

(b) All partial recursive functions ℕ^{n} ⇀ ℕ are represented in Rec_{ℕ^{n},ℕ}^{+}. For this the restriction of calls of other partial recursive functions to types being elements of a universe containing {ℕ^{k} | k ∈ ℕ} suffices.

(c) If e : Rec_{A,B}^{+} is derived without a context, then we have {e}(a)↓ iff p : f_{e}(a)↓ for some p. Furthermore, if p : f_{e}(a)↓, then {e}(a) ≃ eval_{e}(a, p), and {e} is partial recursive.

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.

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

[DS99] Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive 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.