Admissibility of Fixpoint Induction over Partial Types

Karl Crary October 1998

CMU-CS-98-164

School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213

Abstract

Partial types allow the reasoning about partial functions in type theory. The partial functions of main interest are recursively computed functions, which are commonly assigned types using fixpoint induction. However, fixpoint induction is valid only on admissible types. Previous work has shown many types to be admissible, but has not shown any dependent products to be admissible. Disallowing recursion on dependent product types substantially reduces the expressiveness of the logic; for example, it prevents much reasoning about modules, objects and algebras.

In this paper I present two new tools, predicate-admissibility and monotonicity, for showing types to be admissible. These tools show a wide class of types to be admissible; in particular, they show many dependent products to be admissible. This alleviates difficulties in applying partial types to theorem proving in practice. I also present a general least upper bound theorem for fixed points with regard to a computational approximation relation, and show an elegant application of the theorem to compactness.

This research was conducted while the author was at Cornell University. This material is based on work supported in part by ARPA/AF grant F30602-95-1-0047, and AASERT grant N00014-95-1-0985.

Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the author and do not reflect the views of these agencies.

Keywords: Admissibility, fixpoint induction, partial functions, type theory.

1 Introduction

One of the earliest logical theorem provers was the LCF system [12], based on the logic of partial computable functions [21, 22]. Although LCF enjoyed many groundbreaking successes, one problem it faced was that, although it supported a natural notion of partial function, it had difficulty expressing the notion of a total function. Later theorem provers based on constructive type theory, such as Nuprl [5], based on Martin-Löf type theory [19], and Coq [3], based on the Calculus of Constructions [10], faced the opposite problem; they had a natural notion of total functions, but had difficulty dealing with partial functions. The lack of partial functions seriously limited the scope of those theorem provers, because it made them unable to reason about programs in real programming languages where recursion does not always necessarily terminate.

This problem was addressed by Constable and Smith [8], who introduced into their type theory the partial type \overline{T}, which is like a “lifted” version of T. The type \overline{T} contains all members of T as well as all divergent terms. Using the partial type, partial functions from A to B may be given the type A → \overline{B}. That is, when applied to an argument in A, such a function either diverges or converges to a result in B.

In a partial type theory, recursively defined objects may be typed using the fixpoint principle: if f has type \overline{T} → \overline{T} then fix(f) has type \overline{T}. However, the fixpoint principle is not valid for every type T; it is only valid for types that are admissible. This phenomenon was not unknown to LCF; LCF used the related device of fixpoint induction, which was valid only for admissible predicates. When the user attempted to invoke fixpoint induction, the system would automatically check that the goal was admissible using a set of syntactic rules [16].

Despite their obvious uses in program analysis, partial types have seen little use in theorem proving systems [9, 4, 2]. This is due in large part to the fact that too few types have been known to be admissible. Smith [24] gave a significant class of admissible types for a Nuprl-like theory, but his class required product types to be non-dependent. The type Σx:A.B (where x appears free in B) was explicitly excluded. Later, Smith [23] extended his class to include some dependent products Σx:A.B, but disallowed any free occurrences of x to the left of an arrow in B. Partial type extensions to Coq [2] were also restrictive, assuming function spaces to be the only type constructor. These restrictions are quite strong; dependent products are used in encodings of modules [18], objects [20], algebras [17], and even such simple devices as variant records. Furthermore, ruling out dependent products disallows reasoning using fixpoint induction as in LCF [24, 11]. Finally, the restriction is particularly unsatisfying since most types used in practice do turn out to be admissible, and may be shown so by metatheoretical reasoning.

In this paper I present a very wide class of admissible types using two devices, a condition called predicate-admissibility and a monotonicity condition. In particular, many dependent products may be shown to be admissible. Predicate-admissibility relates to when the limit of a chain of type approximations contains certain terms, whereas admissibility relates to the membership of a single type. The term “predicate-admissibility” stems from its similarity to the notion of admissibility of predicates in domain theory (and LCF), where there has been considerable research (this work was influenced by Igarashi [16], for example), but I will not discuss the connection in this paper. Monotonicity is a simpler condition that will be useful for showing types admissible that do not involve partiality.

Type Formation Introduction  Elimination
universe i 𝕌_{i} type formation
(for i ≥ 1)  operators
disjoint union T_{1} + T_{2} inj_{1}(e) case(e, x_{1}.e_{1}, x_{2}.e_{2})
inj_{2}(e)
function space  Πx:T_{1}.T_{2}  λx.e  e_{1}e_{2}
product space  Σx:T_{1}.T_{2}  ⟨e_{1}, e_{2}⟩  π_{1}(e)

π_{2}(e)

natural numbers ℕ  0, 1, 2, …  assorted operations
equality  t_{1} = t_{2} in T  ⋆
partial type  \overline{T}
convergence  t in! T  ⋆

Figure 1: Type Theory Syntax

The paper is organized as follows: In Section 2 I lay out the theory for which these results are formalized. In Section 3 I prove some computational lemmas needed for the admissibility results. The primary result is a least upper bound theorem for fixed points with regard to a computational approximation relation. This result is quite general, and may be applied more widely than just to the purposes for which I use it. I present my main results in Section 4, beginning with a summary of Smith’s original admissibility class and then widening the class using predicate-admissibility and monotonicity. Concluding remarks appear in Section 5.

2 The Type Theory

The type theory in which I formalize the results of this paper is a variant of the Nuprl type theory [5] extended with partial types (that is, types containing possibly divergent objects). This theory is a subset of the type theory of Crary [11] and is similar to Smith’s theory [24]. The major difference between the theory used here and Smith’s is that the latter does not provide a notion of equality; the ramifications of handling equality are discussed in Crary [11].

2.1 Preliminaries

As data types, the theory contains natural numbers (denoted by ℕ), disjoint unions (denoted by T_{1} + T_{2}), dependent products^{1} (denoted by Σx:T_{1}.T_{2}), and dependent function spaces (denoted by Πx:T_{1}.T_{2}). When x does not appear free in T_{2}, I write T_{1}×T_{2} for Σx:T_{1}.T_{2} and T_{1}→T_{2} for Πx:T_{1}.T_{2}. As usual, alpha-equivalent terms are considered identical. When t_{1} and t_{2} are alpha-equivalent, I write t_{1} ≡ t_{2}.

Types themselves are terms in the theory and belong to a predicative hierarchy of universes, 𝕌_{1}, 𝕌_{2}, 𝕌_{3}, etc. The universe 𝕌_{1} contains all types built from the base types only (i.e., built without universes), and the universe 𝕌_{i+1} contains all types build from the base types and the universes 𝕌_{1}, …, 𝕌_{i}. In particular, no universe is a member of itself. Propositions are interpreted as types using the propositions-as-types principle [14], but that will only be relevant in Section 4.3.

1These are sometimes referred to in the literature as dependent sums, but I prefer the terminology to suggest the connection to the non-dependent type T_{1} × T_{2}.

Each type T comes with an intrinsic equality relation denoted by t_{1} = t_{2} ∈ T. Membership is also derived from this relation; t ∈ T when t = t ∈ T. The equality relation is introduced into the type theory as the type t_{1} = t_{2} in T, which is inhabited by the term ⋆ when t_{1} = t_{2} ∈ T and is empty otherwise, provided that t_{1}, t_{2} ∈ T. If either of t_{1} or t_{2} does not belong to T, then t_{1} = t_{2} in T is not well-formed. (Note that t_{1} = t_{2} ∈ T is a metatheoretical assertion whereas t_{1} = t_{2} in T is a type in the theory.) The empty type Void is defined as 0 = 1 in ℕ.

The partial type \overline{T} is like a “lifted” version of T; it contains all the members of T as well as all divergent terms. Partial functions from A to B may then be given the type A → \overline{B}. Two terms are equal in \overline{T} if they both diverge, or if they both converge and are equal in T.

Convergence is expressed within the type theory by the type t in! T, which is inhabited by the term ⋆ when t ∈ \overline{T} and t converges, and is empty if t ∈ \overline{T} but t does not converge. If t ∉ \overline{T} then t in! T is not well-formed. (Again, note that t in! T is a type in the theory, but convergence, which is defined formally below, is a metatheoretical assertion.)

2.2 Computation

Underlying the type theory is the computation system shown in Figure 2. The computation system is defined by a small-step evaluation relation (denoted by t_{1} ↦ t_{2}), and a set of canonical terms. Whether a term is canonical is governed by its outermost operator; the canonical terms are those appearing in the first and second columns of Figure 1. The computation system is call-by-name and contains operators for constructing and destructing functions, pairs and disjoint unions. The computation system also contains various standard operations for computing and analyzing natural numbers, but these are not particularly interesting and are omitted from Figure 2. Of particular interest is the operator fix, which allows the recursive definition of objects is evaluated by the rule fix(f) ↦ f(fix(f)).^{2} Two important properties of evaluation are that evaluation is deterministic and canonical forms are terminal:

Proposition 1 If t ↦ t_{1} and t ↦ t_{2} then t_{1} ≡ t_{2}. Moreover, if t is canonical then t ↛ t′ for any t′.

If t ↦^{∗} t′ and t′ is canonical then I say that t converges (abbreviated t↓) and t converges to t′ (abbreviated t ⇓ t′). Note that if t ⇓ t_{1} and t ⇓ t_{2} then t_{1} ≡ t_{2} and that if t is canonical then t ⇓ t.

The computation system is used in Figure 3 to define the relation t_{1} = t_{2} ∈ T, which specifies the memberships of types and when terms are equal in those types.^{3} This equality relation is constructed to respect evaluation: if t ∈ T and t ↦ t′ then t = t′ ∈ T.

2The use of a fix operator greatly simplifies the presentation of these results (particularly the proof of Theorem 8), but it could be eliminated and replaced with the Y combinator. Similarly, the choice of a call-by-name computation system simplifies the formalism, but is also not critical to the results.

3Since the definition contains negative occurrences of t_{1} = t_{2} ∈ T, it is not immediately clear that it is a valid definition. Allen [1] and Harper [13] have shown how such a definition may be converted to a conventional inductive definition.

{f ↦ f′ \atop f e ↦ f′ e} {t ↦ t′ \atop π_{i}(t) ↦ π_{i}(t′)} t ↦ t′

case(t, x.e_{1}, x.e_{2}) ↦ case(t′, x.e_{1}, x.e_{2})
(λx.e)t ↦ e[t/x]  π_{i}(⟨t_{1}, t_{2}⟩) ↦ t_{i}  case(inj_{i}(t), x.e_{1}, x.e_{2}) ↦ e_{i}[t/x]
fix(f) ↦ f fix(f)

Figure 2: The Computation System

2.3 The Fixpoint Principle

The central issue of this paper is the fixpoint principle:

f ∈ \overline{T} → \overline{T} ⇒ fix(f) ∈ \overline{T}

The fixpoint principle allows us to type recursively defined objects, such as recursive functions. Unfortunately, unlike in programming languages, where the principle can usually be invoked on arbitrary types, expressive type theories such as the one in this paper contain types for which the fixpoint principle is not valid. I shall informally say that a type is admissible if the fixpoint principle is valid for that type and give a formal definition in Section 4. To make maximum use of a partial type theory, one wants as large a class of admissible types as possible.

In Section 4 I will explore two wide classes of admissible types, one derived from a predicateadmissibility condition and another derived from a monotonicity condition. But first, it is worthwhile to note that there are indeed inadmissible types:

Theorem 2 There exist inadmissible types.

Proof Sketch

This example is due to Smith [24]. Let T be the type of functions that do not halt for all inputs, and let f be the function that halts on zero, and on any other n immediately recurses with n − 1. This is formalized as follows:

T =^{def} Σh:(ℕ → \overline{ℕ}). ((Πx:ℕ. h x in! ℕ) → Void)
f =^{def} λp.⟨λx. if x = 0 then 0 else π_{1}(p)(x − 1), λy. ⋆⟩

Intuitively, any finite approximation of fix(f) will recurse some limited number of times and then give up, placing it in T, but fix(f) will halt for every input, excluding it from T. Formally, the function f has type \overline{T} → \overline{T}, but fix(f) ∉ \overline{T}. (The proof of these two facts appears in Appendix A.) Therefore T is not admissible.

3 Computational Lemmas

Before presenting my main results in Section 4, I first require some lemmas about the computational behavior of the fixpoint operator. The central result is that fix(f) is the least upper bound of the t ∈ T iff t = t ∈ T T type iff T = T T_{1} = T_{2} iff ∃T′_{1}, T′_{2}. (T_{1} ⇓ T′_{1}) ∧ (T_{2} ⇓ T′_{2}) ∧ (T′_{1} = T′_{2}) t_{1} = t_{2} ∈ T iff ∃t′_{1}, t′_{2}, T′. (t_{1} ⇓ t′_{1}) ∧ (t_{2} ⇓ t′_{2}) ∧ (T ⇓ T′) ∧ (t′_{1} = t′_{2} ∈ T′)

n = n′ ∈ ℕ (n, n′ natural numbers) iff n ≡ n′ inj_{1}(a) = inj_{1}(a′) ∈ A + B iff A + B type ∧ a = a′ ∈ A inj_{2}(b) = inj_{2}(b′) ∈ A + B iff A + B type ∧ b = b′ ∈ B ⟨a, b⟩ = ⟨a′, b′⟩ ∈ Σx:A.B iff Σx:A.B type ∧ (a = a′ ∈ A) ∧ (b = b′ ∈ B[a/x]) λx.b = λx.b′ ∈ Πx:A.B iff Πx:A.B type ∧ ∀a = a′ ∈ A. b[a/x] = b′[a′/x] ∈ B[a/x] t = t′ ∈ \overline{T} iff \overline{T} type ∧ (t↓ ⇔ t′↓) ∧ (t↓ ⇒ t = t′ ∈ T) ⋆ ∈ (a = a′ in A) iff (a = a′ in A) type ∧ (a = a′ ∈ A) ⋆ ∈ (a in! A) iff (a in! A) type ∧ a↓

For T ≃ T′ iff T = T′, and for T ≃ T′ iff T = T′ ∈ 𝕌_{i}:

ℕ ≃ ℕ A + B ≃ A′ + B′ iff A ≃ A′ ∧ B ≃ B′ Σx:A.B ≃ Σx:A′.B′ iff A ≃ A′ ∧ ∀a = a′ ∈ A. B[a/x] ≃ B′[a′/x] Πx:A.B ≃ Πx:A′.B′ iff A ≃ A′ ∧ ∀a = a′ ∈ A. B[a/x] ≃ B′[a′/x] \overline{T} ≃ \overline{T′} iff T ≃ T′ ∧ ∀t ∈ T. t↓ (a_{1} = a_{2} in A) ≃

(a′_{1} = a′_{2} in A′) iff A ≃ A′ ∧ a_{1} = a′_{1} ∈ A ∧ a_{2} = a′_{2} ∈ A (a in! A) ≃ (a′ in! A′) iff A ≃ A′ ∧ a = a′ ∈ \overline{A} 𝕌_{i} type 𝕌_{i} ∈ 𝕌_{j} iff i < j

Figure 3: Type Definitions

finite approximations ⊥, f(⊥), f(f(⊥)), … with regard to a computational approximation relation defined below. The compactness of fix (if fix(f) halts then one of its finite approximations halts) will be a simple corollary of this result. However, the proof of the least upper bound theorem is considerably more elegant than most proofs of compactness.

3.1 Computational Approximation

For convenience, throughout this section we will frequently consider terms using a unified representation scheme for terms: A term is either a variable or a compound term θ(x_{11} ⋯ x_{1k_{1}}.t_{1}, …, x_{n1} ⋯ x_{nk_{n}}.t_{n}) where the variables x_{i1}, …, x_{ik_{i}} are bound in the subterm t_{i}. For example, the term Πx:T_{1}.T_{2} is represented Π(T_{1}, x.T_{2}) and the term ⟨t_{1}, t_{2}⟩ is represented ⟨⟩(t_{1}, t_{2}).

Informally speaking, a term t_{1} approximates the term t_{2} when: if t_{1} converges to a canonical form then t_{2} converges to a canonical form with the same outermost operator, and the subterms of t_{1}’s canonical form approximate the corresponding subterms of t_{2}’s canonical form. The formal definition appears below and is due to Howe [15].^{4} Following Howe, when R is a binary relation on closed terms, I adopt the convention extending R to possibly open terms that if t and t′ are possibly open then t R t′ if and only if σ(t) R σ(t′) for every substitution σ such that σ(t) and σ(t′) are closed.

Definition 3 (Computational Approximation)

• Let R be a binary relation on closed terms and suppose e and e′ are closed. Then e C(R) e′ exactly when if e ⇓ θ(x⃗_{1}.t_{1}, …, x⃗_{n}.t_{n}) then there exists some closed e′′ = θ(x⃗_{1}.t′_{1}, …, x⃗_{n}.t′_{n}) such that e′ ⇓ e′′ and t_{i} R t′_{i}.

• e ≤_{0} e′ whenever e and e′ are closed.

• e ≤_{i+1} e′ if and only if e C(≤_{i}) e′

• e ≤ e′ if and only if e ≤_{i} e′ for every i

The following are facts about computational approximation that will be used without explicit reference. The first two follow immediately from the definition, the third is easy using determinism (Proposition 1) and the last is proven using Howe’s method [15].

Proposition 4

• ≤ and ≤_{i} are reflexive and transitive.

• If t ↦ t′ then t′ ≤ t and t′ ≤_{i} t.

• If t ↦ t′ then t ≤ t′ and t ≤_{i} t′.

• (Congruence) If e ≤ e′ and t ≤ t′ then e[t/x] ≤ e′[t′/x].

3.2 Finite Approximations

With this notion of computational approximation in hand, we may now show that the terms ⊥, f ⊥, f(f ⊥), … form a chain of approximations to the term fix(f). Let ⊥ be the divergent term fix(λx.x). Since ⊥ never converges, ⊥ ≤ t for any term t. Let f^{i} be defined as follows:

\begin{matrix}f^{0} & =^{def} & ⊥ \\ f^{i+1} & =^{def} & f(f^{i}) \end{matrix}

Certainly f^{0} ≤ f^{1}, since f^{0} ≡ ⊥. By congruence, f(f^{0}) ≤ f(f^{1}), and thus f^{1} ≤ f^{2}. Similarly, f^{i} ≤ f^{i+1} for all i. Thus f^{0}, f^{1}, f^{2}, … forms a chain; I now wish to show that fix(f) is an upper bound of the chain. Certainly f^{0} ≤ fix(f). Suppose f^{i} ≤ fix(f). By congruence f(f^{i}) ≤ f(fix(f)).

4Howe’s definition actually differs slightly from the one here; he defines ≤ as the greatest fixed point of the operator C. It is not difficult to show that the two definitions are equivalent, as long as the computation system is deterministic (Proposition 1). If the computation system is nondeterministic, the definition here fails to be a fixed point, and the more complicated greatest fixed point definition must be employed.

Thus, since fix(f) ↦ f(fix(f)), it follows that f^{i+1} ≡ f(f^{i}) ≤ f(fix(f)) ≤ fix(f). By induction it follows that fix(f) is an upper bound of the chain. The following corollary follows from congruence and the definition of approximation:

Corollary 5 If there exists j such that e[f^{j}/x]↓ then e[fix(f)/x]↓. Moreover, the canonical forms of e[f^{j}/x] and e[fix(f)/x] must have the same outermost operator.

3.3 Least Upper Bound Theorem

In this section I summarize the proof of the least upper bound theorem. The full proof appears in Appendix A. To begin, we need a lemma stating a general property of evaluation. Lemma 6 captures the intuition that closed, noncanonical terms that lie within a term being evaluated are not destructed; they either are moved around unchanged (the lemma’s first case) or are evaluated in place with the surrounding term left unchanged (the lemma’s second case). The variable x indicates positions where the term of interest is found and, in the second case, the variable y indicates which of those positions, if any, is about to be evaluated.

Lemma 6 If e_{1}[t/x] ↦ e_{2}, and e_{1}[t/x] is closed, and t is closed and noncanonical, then either

• there exists e′_{2} such that for any closed t′, e_{1}[t′/x] ↦ e′_{2}[t′/x], or

• there exist e′_{1} and t′ such that e_{1} ≡ e′_{1}[x/y], t ↦ t′ and for any closed t′′, e′_{1}[t′′, t/x, y] ↦ e′_{1}[t′′, t′/x, y].

It is worthwhile to note that Propositions 1 and 4 and Lemma 6 are the only properties of evaluation used in the proof of the least upper bound theorem, and that these properties are true in computational systems with considerable generality. Consequently, the theorem may be used in a variety of applications beyond the computational system of this paper.

Lemma 7 shows that fix terms may be effectively simulated in any particular computation by sufficiently large finite approximations. The lemma is simplified by using computational approximation instead of evaluation for the simulation, which makes it unnecessary to track which of the approximations are unfolded and which are not, an issue that often complicates compactness proofs.

Lemma 7 (Simulation) For all f, e_{1} and e_{2} (where f is closed and x is the only free variable of e_{1}), there exist j and e′_{2} such that if e_{1}[fix(f)/x] ↦^{∗} e_{2} then e_{2} ≡ e′_{2}[fix(f)/x] and for all k ≥ j, e′_{2}[f^{k−j}/x] ≤ e_{1}[f^{k}/x].

Theorem 8 (Least Upper Bound) For all f, t and e (where f is closed), if ∀j. e[f^{j}/x] ≤ t, then e[fix(f)/x] ≤ t.

Proof Sketch

By induction on l that e[fix(f)/x] ≤_{l} t. (The complete proof in Appendix A addresses free variables.) Suppose e[fix(f)/x] evaluates to some canonical form e′[fix(f)/x] (where e′ is chosen by Lemma 7). Let e′ be of the form θ(x⃗_{1}.t_{1}, …, x⃗_{n}.t_{n}). Using Lemma 7, the assumption ∀k. e[f^{k}/x] ≤ t, and transitivity, we may show that e′[f^{j}/x] ≤ t for all j. Therefore t ⇓ θ(x⃗_{1}.t′_{1}, …, x⃗_{n}.t′_{n}) and t_{i}[f^{j}/x] ≤ t′_{i} for all j. Now, by induction, t_{i}[fix(f)/x] ≤_{l} t′_{i}. Thus e[fix(f)/x] ≤_{l+1} t.

There are two easy corollaries to the least upper bound theorem. One is that fix(f) is the least fixed point of f, and the other is compactness.

Corollary 9 (Least Fixed Point) For all closed f and t, if f(t) ≤ t then fix(f) ≤ t.

Proof

Certainly f^{0} ≡ ⊥ ≤ t. Then f^{1} ≡ f(f^{0}) ≤ f(t) ≤ t. Similarly, by induction, f^{j} ≤ t for any j. Therefore fix(f) ≤ t by Theorem 8. □

Corollary 10 (Compactness) If f is closed and e[fix(f)/x]↓ then there exists some j such that e[f^{j}/x]↓. Moreover, the canonical forms of e[fix(f)/x] and e[f^{j}/x] must have the same outermost operator.

Proof

Suppose there does not exist j such that e[f^{j}/x]↓. Then e[f^{j}/x] ≤ ⊥ for all j. By Theorem 8, e[fix(f)/x] ≤ ⊥. Therefore e[fix(f)/x] does not converge, but this contradicts the assumption,^{5} so there must exist j such that e[f^{j}/x]↓. Since e[f^{j}/x] ≤ e[fix(f)/x], the canonical forms of e[f^{j}/x] and e[fix(f)/x] must have the same outermost operator. □

4 Admissibility

I am now ready to begin specifying some wide classes of types for which the fixpoint principle is valid. First we define admissibility. The simple property of validating the fixpoint principle is too specific to allow any good closure conditions to be shown easily, so we generalize a bit to define admissibility. A type is admissible if the upper bound t[fix(f)] of an approximation chain t[f^{0}], t[f^{1}], t[f^{2}], … belongs to the type whenever a cofinite subset of the chain belongs to the type. This is formalized as Definition 12, but first I define some convenient notation.

Notation 11 For any natural number j, the notation t^{[j]_{f}} means t[f^{j}/w], and the notation t^{[ω]_{f}} means t[fix(f)/w]. Also, the f subscript is dropped when the intended term f is unambiguously clear.

5Although this proof is non-constructive, a slightly less elegant constructive proof is derivable directly from Lemma 7.

Definition 12 A type T is admissible (abbreviated Adm(T)) if:

∀f, t, t′. (∃j. ∀k ≥ j. t^{[k]} = t^{′[k]} ∈ T) ⇒ t^{[ω]} = t^{′[ω]} ∈ T

As expected, admissibility is sufficient to guarantee applicability of the fixpoint principle:

Theorem 13 For any T and f, if T is admissible and f = f′ ∈ \overline{T} → \overline{T} then fix(f) = fix(f′) ∈ \overline{T}.

Proof

\overline{T} type since \overline{T} → \overline{T} type. Note that f^{j} = f^{′j} ∈ \overline{T} for every j. Suppose fix(f)↓. By compactness, f^{j}↓ for some j. Since f^{j} = f^{′j} ∈ \overline{T}, it follows that f^{′j}↓ and thus fix(f′)↓ by Corollary 5. Similarly fix(f′)↓ implies fix(f)↓. It remains to show that fix(f) = fix(f′) ∈ T when fix(f)↓. Suppose again that fix(f)↓. As before, there exists j such that f^{j}↓ by compactness. Hence f^{j} = f^{′j} ∈ T. Since T is admissible, fix(f) = fix(f′) ∈ T. □

A number of closure conditions exist on admissible types and are given in Lemma 14. Informally, basic compound types other than dependent products are admissible so long as their component types in positive positions are admissible. Base types—natural numbers, convergence types, and (for this lemma only) equality types—are always admissible. These are essentially the admissible types of Smith [24], except that for a function type to be admissible Smith required that its domain type be admissible.

Lemma 14

• Adm(A + B) if Adm(A) and Adm(B)

• Adm(Πx:A.B) if ∀a ∈ A. Adm(B[a/x])

• Adm(A × B) if Adm(A) and Adm(B)

• Adm(ℕ)

• Adm(a = a′ in A)

• Adm(\overline{A}) if Adm(A)

• Adm(a in! A)

Proof

The proof follows the same lines as Smith’s proof, except that handling equality adds a small amount of complication to the proof. I show the function case by way of example.

Let f, t and t′ be arbitrary. Suppose j is such that ∀k ≥ j. t^{[k]} = t^{′[k]} ∈ Πx:A.B. I need to show that t^{[ω]} = t^{′[ω]} ∈ Πx:A.B. Since Πx:A.B is inhabited it is a type. Both t^{[j]} and t^{′[j]} converge to lambda abstractions, so, by Corollary 5, t^{[ω]} ⇓ λx.b and t^{′[ω]} ⇓ λx.b′ for some terms b and b′. Suppose a = a′ ∈ A. To get that b[a/x] = b′[a′/x] ∈ B[a/x] it suffices to show that t^{[ω]}a = t^{′[ω]}a′ ∈ B[a/x]. Since Adm(B[a/x]), it suffices to show that ∀k ≥ j. t^{[k]}a = t^{′[k]}a′ ∈ B[a/x], which follows from the supposition. □

Unfortunately, Lemma 14 can show the admissibility of a product space only if it is non-dependent. Dependent products do not have an admissibility condition similar to that of dependent functions. This reason for this is as follows: Admissibility states that a single fixed type contains the limit of an approximation chain if it contains a cofinite subset of that chain. For functions, disjoint union, partial types, and non-dependent products it is possible to decompose prospective members in such a way that admissibility may be applied to a single type (such as the type B[a/x] used in the proof of Lemma 14). In contrast, for a dependent product, the right-hand term’s desired type depends upon the left-hand term, which is changing at the same time as the right-hand term. Consequently, there is no single type into which to place the right-hand term.

However, understanding the problem with dependent products suggests a solution, to generalize the definition of admissibility to allow the type to vary. This leads to the notion of predicateadmissibility that I discuss in the next section.

4.1 Predicate-Admissibility

Definition 15 A type T is predicate-admissible for x in S (abbreviated Adm(T | x : S)) if:

∀f, t, t′, e. e^{[ω]} ∈ S ∧ (∃j. ∀k ≥ j. e^{[k]} ∈ S ∧ t^{[k]} = t^{′[k]} ∈ T [e^{[k]}/x]) ⇒ t^{[ω]} = t^{′[ω]} ∈ T [e^{[ω]}/x]

The term “predicate-admissibility” stems from its similarity to the notion of admissibility of predicates in domain theory (and LCF). If one ignores the inhabiting terms t and t′, which may be seen as evidences of the truth of the predicate T [ ], then predicate-admissibility is saying T [e^{[ω]}] if T [e^{[k]}] for all k greater than some j. This is precisely the notion of admissibility of predicates in domain theory. Indeed, the results here were influenced by the work of Igarashi [16], who established conditions on admissibility of domain-theoretic predicates.

To show the admissibility of a dependent product type, it is sufficient to show predicate-admissibility of the right-hand side (along with admissibility of the left):

Lemma 16 The type Σx:A.B is admissible if Adm(A) and Adm(B | x : A).

Proof

Let f, t and t′ be arbitrary. Suppose j is such that ∀k ≥ j. t^{[k]} = t^{′[k]} ∈ Σx:A.B. It is necessary to show that t^{[ω]} = t^{′[ω]} ∈ Σx:A.B. Since Σx:A.B is inhabited it is a type. Both t^{[j]} and t^{′[j]} converge to pairs, so, by Corollary 5, t^{[ω]} ⇓ ⟨a, b⟩ and t^{′[ω]} ⇓ ⟨a′, b′⟩ for some terms a, b, a′ and b′. To get that a = a′ ∈ A it suffices to show that π_{1}(t^{[ω]}) = π_{1}(t^{′[ω]}) ∈ A. Since Adm(A), it suffices to show that ∀k ≥ j. π_{1}(t^{[k]}) = π_{1}(t^{′[k]}) ∈ A, which follows from the supposition.

To get that b = b′ ∈ B[a/x] (the interesting part), it suffices to show that π_{2}(t^{[ω]}) = π_{2}(t^{′[ω]}) ∈ B[π_{1}(t^{[ω]})/x]. Since Adm(B | x : A), it suffices to show that π_{1}(t^{[ω]}) ∈ A, which has already been shown, and ∀k ≥ j. π_{1}(t^{[k]}) ∈ A ∧ π_{2}(t^{[k]}) = π_{2}(t^{′[k]}) ∈ B[π_{1}(t^{[k]})/x], which follows from the supposition. □

The conditions for predicate-admissibility are more elaborate, but also more general. I may immediately state conditions for basic types other than functions. Informally, basic compound types other than functions are predicate-admissible so long as their component types are predicate-admissible, and base types are always predicate-admissible. (The proof for these conditions, and all other remaining proofs, appear in Appendix A.)

Lemma 17

• Adm(A + B | y : S) if ∀s ∈ S. (A + B)[s/y] type and Adm(A | y : S) and Adm(B | y : S).

• Adm(Σx:A.B | y : S) if ∀s ∈ S. (Σx:A.B)[s/y] type and Σy:S.A type and Adm(A | y : S) and Adm(B[π_{1}(z), π_{2}(z)/y, x] | z : (Σy:S.A))

• Adm(ℕ | y : S)

• Adm(a_{1} = a_{2} in A | y : S) if ∀s ∈ S. (a_{1} = a_{2} in A)[s/y] type and Adm(A | y : S)

• Adm(\overline{A} | y : S) if ∀s ∈ S. \overline{A}[s/y] type and Adm(A | y : S)

• Adm(a in! A | y : S) if ∀s ∈ S. (a in! A)[s/y] type

Predicate-admissibility of a function type is more complicated because a function argument with the type A[e^{[ω]}/x] does not necessarily belong to any of the finite approximations A[e^{[j]}/x]. To settle this, it is necessary to require a coadmissibility condition on the domain type. Then a function type will be predicate-admissible if the domain is weakly coadmissible and the codomain is predicate-admissible.

Definition 18 A type T is weakly coadmissible for x in S (abbreviated WCoAdm(T | x : S)) if:

\begin{matrix}∀f, t, t′, e. e^{[ω]} ∈ S ∧ (∃j. ∀k ≥ j. e^{[k]} ∈ S) ∧ t = t′ ∈ T [e^{[ω]}/x] ⇒ \\ (∃j. ∀k ≥ j. t = t′ ∈ T [e^{[k]}/x]) \end{matrix}

A type T is coadmissible for x in S (abbreviated CoAdm(T | x : S)) if:

\begin{matrix}∀f, t, t′, e. e^{[ω]} ∈ S ∧ (∃j. ∀k ≥ j. e^{[k]} ∈ S) ∧ t^{[ω]} = t^{′[ω]} ∈ T [e^{[ω]}/x] ⇒ \\ (∃j. ∀k ≥ j. t^{[k]} = t^{′[k]} ∈ T [e^{[k]}/x]) \end{matrix}

Lemma 19 Adm(Πx:A.B | y : S) if ∀s ∈ S. (Σx:A.B)[s/y] type and WCoAdm(A | y : S) and ∀s ∈ S, a ∈ A[s/y]. Adm(B[a/x] | y : S)

Clearly coadmissibility implies weak coadmissibility. A general set of conditions listed in Lemma 20 establish weak and full coadmissibility for various types. Weak and full coadmissibility are closed under disjoint union and dependent sum formation, and full coadmissibility is additionally closed under equality-type formation. I use both notions of coadmissibility, rather than just adopting one or the other, because full coadmissibility is needed for equality types but under certain circumstances weak coadmissibility is easier to show (Proposition 21 below).

Lemma 20

• A + B is (weakly) coadmissible for y in S if ∀s ∈ S. (A + B)[s/y] type and A and B are (weakly) coadmissible for y in S

• WCoAdm(Σx:A.B | y : S) if ∀s ∈ S. (Σx:A.B)[s/y] type and WCoAdm(A | y : S) and ∀s ∈ S, a ∈ A[s/y]. WCoAdm(B[a/x] | y : S)

• CoAdm(Σx:A.B | y : S) if ∀s ∈ S. (Σx:A.B)[s/y] type and Σy:S.A type and CoAdm(A | y : S) and CoAdm(B[π_{1}(z), π_{2}(z)/y, x] | z : (Σy:S.A))

• ℕ is strongly or weakly coadmissible for y in any S

• CoAdm(a_{1} = a_{2} in A | y : S) if ∀s ∈ S. (a_{1} = a_{2} in A)[s/y] type and CoAdm(A | y : S)

• \overline{A} is (weakly) coadmissible for y in S if ∀s ∈ S. \overline{A}[s/y] type and A is (weakly) coadmissible for y is S

• a in! A is strongly or weakly coadmissible for y in S if ∀s ∈ S. (a in! A)[s/y] type

When T does not depend upon S, predicate-admissibility and weak coadmissibility become easier to show:

Proposition 21 Suppose x does not appear free in T. Then:

• Adm(T) if Adm(T | x : S) and S is inhabited

• Adm(T | x : S) if Adm(T)

• WCoAdm(T | x : S)

There remains one more result related to predicate-admissibility. Suppose one wishes to show Adm(T |x : S) where T depends upon x. There are two ways that x may be used in T. First, T might contain an equality type where x appears in one or both of the equands. In that case, predicateadmissibility can be shown with the tools discussed above. Second, T may be an expression that computes a type from x. In this case, T can be simplified using untyped reasoning [15], but another tool will be needed if T performs any case analysis.

Lemma 22 Consider a type case(d, x.A, x.B) that depends upon y from S. Suppose there exist T_{1} and T_{2} such that:

• ∀s ∈ S. d[s/y] ∈ (T_{1} + T_{2})[s/y]

• ∀s ∈ S, t ∈ T_{1}[s/y]. A[s, t/y, x] type

• ∀s ∈ S, t ∈ T_{2}[s/y]. B[s, t/y, x] type

• Σy:S.T_{1} type and Σy:S.T_{2} type Then the following are the case:

• Adm(case(d, x.A, x.B) | y : S) if Adm(A[π_{1}(z), π_{2}(z)/y, x] | z : (Σy:S.T_{1})) and Adm(B[π_{1}(z), π_{2}(z)/y, x] | z : (Σy:S.T_{2}))

• WCoAdm(case(d, x.A, x.B) | y : S) if WCoAdm(A[π_{1}(z), π_{2}(z)/y, x] | z : (Σy:S.T_{1})) and WCoAdm(B[π_{1}(z), π_{2}(z)/y, x] | z : (Σy:S.T_{2}))

• CoAdm(case(d, x.A, x.B) | y : S) if CoAdm(A[π_{1}(z), π_{2}(z)/y, x] | z : (Σy:S.T_{1})) and CoAdm(B[π_{1}(z), π_{2}(z)/y, x] | z : (Σy:S.T_{2}))

4.2 Monotonicity

In some cases a very simple device may be used to show admissibility. We say that a type is monotone if it respects computational approximation, and it is easy to show that all monotone types are admissible.

Definition 23 A type T is monotone (abbreviated Mono(t)) if t = t′ ∈ T whenever t ∈ T and t ≤ t′.

Lemma 24 All monotone types are admissible.

Proof

Let f, t and t′ be arbitrary and suppose there exists j such that t^{[j]} = t^{′[j]} ∈ T. Since t^{[j]} ≤ t^{[ω]} and t^{′[j]} ≤ t^{′[ω]}, it follows that t^{[j]} = t^{[ω]} ∈ T and t^{′[j]} = t^{′[ω]} ∈ T. The result follows directly. □

All type constructors are monotone except universes and partial types, which are never monotone. The proof of this fact is easy [15].

Proposition 25

• Mono(A + B) if Mono(A) and Mono(B)

• Mono(Πx:A.B) if Mono(A) and ∀a ∈ A. Mono(B[a/x])

• Mono(Σx:A.B) if Mono(A) and ∀a ∈ A. Mono(B[a/x])

• Mono(ℕ), Mono(a_{1} = a_{2} ∈ A) and Mono(a in! A)

4.3 Set and Quotient Types

In addition to the type constructors discussed so far, the Nuprl type theory also contains two fairly novel types, Constable’s set and quotient types [6]. These types allow the use of logical predicates a = a′ ∈ {x : A | B} iff {x : A | B} type ∧ a = a′ ∈ A ∧ ∃b. b ∈ B[a/x] a = a′ ∈ xy:A//B iff (xy:A//B) type ∧ a ∈ A ∧ a′ ∈ A ∧ ∃b. b ∈ B[a, a′/x, y]

For T ≃ T′ iff T = T′, and for T ≃ T′ iff T = T′ ∈ 𝕌_{i}:

{x : A | B} ≃ {x : A′ | B′} iff A ≃ A′ ∧ ∀a = a′ ∈ A. B[a/x] ≃ B[a′/x] ∧ ∀a = a′ ∈ A. B′[a/x] ≃ B′[a′/x] ∧ (B if and only if B′) ∃t. t ∈ Πx:A. B → B′ ∧ ∃t. t ∈ Πx:A. B′ → B

(xy:A//B) ≃ (xy:A′//B′) iff A ≃ A′ ∧ ∀a_{1} = a′_{1} ∈ A. ∀a_{2} = a′_{2} ∈ A. B[a_{1}, a_{2}/x, y] ≃ B[a′_{1}, a′_{2}/x, y] ∧ ∀a_{1} = a′_{1} ∈ A. ∀a_{2} = a′_{2} ∈ A. B′[a_{1}, a_{2}/x, y] ≃ B′[a′_{1}, a′_{2}/x, y] ∧ (B if and only if B′) ∃t. t ∈ Πx:A. Πy:A. B → B′ ∧ ∃t. t ∈ Πx:A. Πy:A. B′ → B ∧ (reflexivity) ∃t. t ∈ Πx:A. B[x/y] ∧ (symmetry) ∃t. t ∈ Πx:A. Πy:A. B → B[y, x/x, y] ∧ (transitivity) ∃t. t ∈ Πx:A. Πy:A. Πz:A. B → B[y, z/x, y] → B[z/y]

Figure 4: Set and Quotient Type Definitions

(encoded as types using the propositions-as-types principle [14]) to refine or coarsen types in various ways.

The set type {x:T | P } is the subtype of T that contains all t ∈ T such that P [t/x] is inhabited (i.e., such that the proposition corresponding to P [t/x] is true). The quotient type xy:T//E[x, y] (when E[−, −] corresponds to an equivalence relation on T) is the supertype of T that coarsens the equality on T as follows: t_{1} = t_{2} ∈ xy:T//E if and only if t_{1}, t_{2} ∈ T and E[t_{1}, t_{2}/x, y] is inhabited (i.e., true). The set and quotient types are defined formally in Figure 4.

The set type {x:A | B[x]} is much like the dependent product type Σx:A.B[x] in that both provide a member a of A such that B[a] is inhabited, but differ in that the dependent product provides that inhabitant and the set type suppresses it. Given this parallel between the dependent product and set types, it is natural to expect that set types would have a similar admissibility rule: that {x : A | B} if A is admissible and B is predicate-admissible for x in A. Somewhat surprisingly, this turns out not to be the case. Suppose that t^{[k]} ∈ {x : A | B} for all k ≥ j. Then for every k ≥ j, there exists some term b_{k} ∈ B[t^{[k]}/x]. We would like it to follow by predicate-admissibility that there exists b_{ω} ∈ B[t^{[ω]}/x], but it does not. The problem is that each b_{k} can be a completely different term, and predicate-admissibility applies only when each b_{k} is of the form b[f^{k}/w] for a single fixed b.

Intuitively, the desired rule fails because the set type {x : A | B} suppresses the computational content of B and therefore B can be inhabited non-uniformly, by unrelated terms for related members of A. In contrast, if the chain t^{[j]}, t^{[j+1]}, t^{[j+2]}, … belongs to Σx:A.B, then the chain π_{2}(t)^{[j]}, π_{2}(t)^{[j+1]}, π_{2}(t)^{[j+2]}, … uniformly inhabits B.

For a concrete example, consider:

T =^{def} \{g : ℕ → \overline{ℕ} | ∃n:ℕ. (g n in! ℕ) → Void\}
f =^{def} λh. λx. if x = 0 then 0 else h(x − 1)
t =^{def} λy. wy

The type T is not admissible: For all k, (t^{[k]_{f}})k diverges, so t^{[k]_{f}} ∈ T; but t^{[ω]_{f}} converges for all arguments, so t^{[ω]_{f}} ∉ T. However, ∃n:ℕ. (gn in! ℕ) → Void is predicate-admissible for g in ℕ → \overline{ℕ}. The problem is that the inhabiting integers are not related by computational approximation; that is, they are not uniform.

To show a set type admissible, we need to be able to show that the selection predicate can be inhabited uniformly:

Lemma 26 The type {x : A | B} is admissible if:

• Adm(A), and

• Adm(B | x : A), and

• there exists b such that b[a/x] ∈ B[a/x] whenever a ∈ A and ∃b′. b′ ∈ B[a/x].

We may give a similar predicate-admissibility condition:

Lemma 27 Adm({x : A | B} | y : S) if ∀s ∈ S. ({x : A | B})[s/y] type and Σy:S.A type and Adm(A|y : S) and Adm(B[π_{1}(z), π_{2}(z)/y, x]|z : Σy:S.A), and there exists b such that b[a, s/x, y] ∈ B[a, s/x, y] whenever s ∈ S and a ∈ A[s/y] and ∃b′. b′ ∈ B[a, s/x, y]

Coadmissibility and monotonicity work on single terms, not chains, so the uniformity issue does not arise, resulting in conditions fairly similar to those for dependent products:

Lemma 28

• WCoAdm({x : A | B} | y : S) if ∀s ∈ S. {x : A | B}[s/y] type and WCoAdm(A | y : S) and ∀s ∈ S, a ∈ A[s/y]. WCoAdm(B[a/x] | y : S)

• CoAdm({x : A|B}|y : S) if ∀s ∈ S. {x : A|B}[s/y] type and Σy:S.A type and CoAdm(A|y : S) and WCoAdm(B[π_{1}(z), π_{2}(z)/y, x] | z : (Σy:S.A))

• Mono({x : A | B}) if Mono(A)

The conditions for quotient types are similar to those for set types:

• Adm(xy:A//B) if Adm(A) and Adm(B[π_{1}(z), π_{2}(z)/x, y] | z : A × A), and there exists b such that b[a, a′/x, y] ∈ B[a, a′/x, y] whenever a ∈ A and a′ ∈ A and ∃b′. b′ ∈ B[a, a′/x, y].

• Adm(xy:A//B |z : S) if ∀s ∈ S.(xy:A//B)[s/z] type and Σz:S.(A×A) type and Adm(A|z : S) and Adm(B[π_{1}(z′), π_{1}(π_{2}(z′)), π_{2}(π_{2}(z′))/z, x, y] | z′ : Σz:S.(A × A)), and there exists b such that b[a, a′, s/x, y, z] ∈ B[a, a′, s/x, y, z] whenever s ∈ S and a ∈ A[s/z] and a′ ∈ A[s/z] and ∃b′. b′ ∈ B[a, a′, s/x, y, z].

• WCoAdm(xy:A//B | z : S) if ∀s ∈ S. (xy:A//B)[s/z] type and WCoAdm(A | z : S) and ∀s ∈ S, a ∈ A[s/z], a′ ∈ A[s/z]. WCoAdm(B[a, a′/x, y] | z : S)

• CoAdm(xy:A//B|z : S) if ∀s ∈ S. (xy:A//B)[s/z]type and Σz:S.(A×A)type and CoAdm(A|z : S) and CoAdm(B[π_{1}(z′), π_{1}(π_{2}(z′)), π_{2}(π_{2}(z′))/z, x, y] | z′ : Σz:S.(A × A))

• Mono(xy:A//B) if Mono(A)

4.4 Summary

Figure 5 provides a summary of the basic admissibility results of this chapter. It is worthwhile to note that all these results are proved constructively, with the exception of (weak and full) coadmissibility of partial types. The following theorem shows that the proofs of coadmissibility of partial types are necessarily classical; if a constructive proof existed then one could extract an algorithm meeting the theorem’s specification, which can be used to solve the halting problem.

Theorem 30 There does not exist an algorithm that computes an integer j such that ∀k ≥ j. t = t′ ∈ \overline{T} [e^{[k]}/x], when given S, T, f, t, t′, e and i such that:

• ∀s ∈ S. \overline{T} [s/x] type

• CoAdm(T | x : S)

• e^{[ω]} ∈ S

• ∀k ≥ i. e^{[k]} ∈ S

• t = t′ ∈ \overline{T} [e^{[ω]}/x]

Recall the inadmissible type T from Theorem 2. That type fails the predicate-admissibility condition because of the negative appearance of a function type, which could not be shown weakly coadmissible, and it fails the monotonicity condition because it contains the partial type \overline{ℕ}.

5 Conclusions

An interesting avenue for future investigation would be to find some negative results characterizing inadmissible types. Such negative results would be particularly interesting if they could be given

For T ≡
A + B Πx:A.B Σx:A.B

Adm(T) if

T type and Adm(A) ∧ Adm(B) ∀a ∈ A. Adm(B[a/x]) Adm(A) ∧ Adm(B | x : A)
Adm(A | y : S) ∧
WCoAdm(A | y : S) ∧ Adm(B[π_{1}(z), π_{2}(z)/y, x]
Adm(T | y : S) if Adm(A | y : S) ∧ ∀s ∈ S, a ∈ A[s/y]. | z : (Σy : S.A)) ∧
∀s ∈ S. T [s/y] type and Adm(B | y : S)  Adm(B[a/x] | y : S) Σy:S.A type
WCoAdm(A | y : S) ∧
WCoAdm(T | y : S) if WCoAdm(A | y : S) ∧  ∀s ∈ S, a ∈ A[s/y].
∀s ∈ S. T [s/y] type and WCoAdm(B | y : S) — WCoAdm(B[a/x] | y : S)
CoAdm(A | y : S) ∧
CoAdm(B[π_{1}(z), π_{2}(z)/y, x]
CoAdm(T | y : S) if  CoAdm(A | y : S) ∧  | z : (Σy : S.A)) ∧
∀s ∈ S. T [s/y] type and CoAdm(B | y : S)  —  Σy:S.A type
Mono(A) ∧  Mono(A) ∧
Mono(T) if  Mono(A) ∧ Mono(B) ∀a ∈ A. Mono(B[a/x]) ∀a ∈ A. Mono(B[a/x])
For T ≡
ℕ, a in! A a_{1} = a_{2} in A \overline{A}

Adm(T) if

T type and yes yes Adm(A)

Adm(T | y : S) if

∀s ∈ S. T [s/y] type and yes Adm(A | y : S) Adm(A | y : S)

WCoAdm(T | y : S) if

∀s ∈ S. T [s/y] type and yes  CoAdm(A | y : S) WCoAdm(A | y : S)

CoAdm(T | y : S) if

∀s ∈ S. T [s/y] type and yes  CoAdm(A | y : S) CoAdm(A | y : S)
Mono(T) if  yes  yes  —

Figure 5: Admissibility, coadmissibility and monotonicity conditions

a syntactic character, like the results of this chapter. Along these lines, it would be interesting to find whether the inability to show coadmissibility of function types represents a weakness of this proof technique or an inherent limitation.

The results presented above provide metatheoretical justification for the fixpoint principle over many types. In order for these results to be useful in theorem proving, they must be introduced into the logic. One way to do this, and the way it is done in my implementation of partial types in the Nuprl proof assistant [11], is to introduce types to represent the assertions Adm(T), Adm(T |x : S), etc., that are inhabited exactly when the underlying assertion is true (in much that same way as the equality type is inhabited exactly when the equands are equal), and to add rules relating to these types that correspond to the lemmas of Section 4. This brings the tools into the system in a semantically justifiable way, but it is unpleasant in that it leads to a proliferation of new types and inference rules stemming from discoveries outside the logic. It would be preferable to deal with admissibility within the logic. A theory with intensional reasoning principles, such as the one proposed in Constable and Crary [7], would allow reasoning about computation internally. Then these results could be proved within the theory and the only extra rule that would be required would be a single rule relating admissibility to the the fixpoint principle.

However they are placed into the logic, these results allow for recursive computation on a wide variety of types. This make partial types and fixpoint induction a useful tool in type-theoretic theorem provers. It also makes it possible to study many recursive programs that used to be barred from the logic because they could not be typed.

References

[1] Stuart Allen. A non-type-theoretic definition of Martin-Löf’s types. In Second IEEE Symposium on Logic in Computer Science, pages 215–221, Ithaca, New York, June 1987.

[2] Philippe Audebaud. Partial objects in the calculus of constructions. In Sixth IEEE Symposium on Logic in Computer Science, pages 86–95, Amsterdam, July 1991.

[3] Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, Gérard Huet, César Muñoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saïbi, and Benjamin Werner. The Coq Proof Assistant Reference Manual. INRIA-Rocquencourt, CNRS and ENS Lyon, 1996.

[4] David A. Basin. An environment for automated reasoning about partial functions. In Ninth International Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science. Springer-Verlag, 1988.

[5] R.L. Constable, S.F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, D.J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, J.T. Sasaki, and S.F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.

[6] Robert L. Constable. Constructive mathematics as a programming logic I: Some principles of theory. In Topics in the Theory of Computation, volume 24 of Annals of Discrete Mathematics, pages 21–37. Elsevier, 1985. Selected papers of the International Conference on Foundations of Computation Theory 1983.

[7] Robert L. Constable and Karl Crary. Computational complexity and induction for partial computable functions in type theory. Technical report, Department of Computer Science, Cornell University, 1997.

[8] Robert L. Constable and Scott Fraser Smith. Partial objects in constructive type theory. In Second IEEE Symposium on Logic in Computer Science, pages 183–193, Ithaca, New York, June 1987.

[9] Robert L. Constable and Scott Fraser Smith. Computational foundations of basic recursive function theory. In Third IEEE Symposium on Logic in Computer Science, pages 360–371, Edinburgh, Scotland, July 1988.

[10] Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988.

[11] Karl Crary. Type-Theoretic Methodology for Practical Programming Languages. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, August 1998.

[12] Michael J. Gordon, Arthur J. Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

[13] Robert Harper. Constructing type systems over an operational semantics. Journal of Symbolic Computation, 14:71–84, 1992.

[14] W. Howard. The formulas-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 479–490. Academic Press, 1980.

[15] Douglas J. Howe. Equality in lazy computation systems. In Fourth IEEE Symposium on Logic in Computer Science, 1989.

[16] Shigeru Igarashi. Admissibility of fixed-point induction in first-order logic of typed theories. Technical Report AIM-168, Computer Science Department, Stanford University, May 1972.

[17] Paul Bernard Jackson. Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, January 1995.

[18] David MacQueen. Using dependent types to express modular structure. In Thirteenth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 277–286, St. Petersburg Beach, Florida, January 1986.

[19] Per Martin-Löf. Constructive mathematics and computer programming. In Sixth International Congress of Logic, Methodology and Philosophy of Science, volume 104 of Studies in Logic and the Foundations of Mathematics, pages 153–175. North-Holland, 1982.

[20] Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207–247, April 1994.

[21] Dana Scott. Outline of a mathematical theory of computation. In Fourth Princeton Conference on Information Sciences and Systems, pages 169–176, 1970.

[22] Dana Scott. Lattice theoretic models for various type-free calculi. In Fourth International Congress of Logic, Methodology and Philosophy of Science. North-Holland, 1972.

[23] Scott F. Smith. Hybrid partial-total type theory. International Journal of Foundations of Computer Science, 6:235–263, 1995.

[24] Scott Fraser Smith. Partial Objects in Type Theory. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, January 1989.

A Proofs

Theorem 2 There exist inadmissible types.

Proof

This example is due to Smith [24]. Let the type T and the function f be defined as follows:

T =^{def} Σh:(ℕ → \overline{ℕ}). ((Πx:ℕ. h x in! ℕ) → Void)
f =^{def} λp.⟨g, λy. ⋆⟩
g =^{def} λx. if x = 0 then 0 else π_{1}(p)(x − 1)

It is easy to verify that \overline{T} type. We wish to show that f has type \overline{T} → \overline{T}. Suppose t = t′ ∈ \overline{T}. We need g[t/p] = g[t′/p] ∈ ℕ → \overline{ℕ} and λy. ⋆ ∈ (Πx:ℕ. (g[t/p])x in! ℕ) → Void. The former is easily shown; to show the latter, I assume that (g[t/p])n converges for every natural number n and draw a contradiction. It follows that Πx:ℕ. (g[t/p])x in! ℕ is empty and λy. ⋆ is vacuously a function from any empty type to Void. Suppose (g[t/p])n converges for every natural number n. Then the term if n = 0 then 0 else π_{1}(t)(n − 1) also converges for every natural number n. It follows that t↓, since π_{1}(t)(0)↓, and hence t ∈ T. Thus (Πx:ℕ. π_{1}(t)(x) in! ℕ) → Void is inhabited (by π_{2}(t)) and consequently it cannot be the case that π_{1}(t)(n)↓ for every natural number n. But this is a contradiction since π_{1}(t)(n − 1)↓ for every n > 1. Therefore f ∈ \overline{T} → \overline{T}. However, it is not the case that fix(f) ∈ \overline{T}. Suppose fix(f) ∈ \overline{T}. Then fix(f) ∈ T since fix(f) converges (in two steps). Thus π_{2}(fix(f)) ∈ (Πx:ℕ. π_{1}(fix(f))(x) in! ℕ) → Void, which implies that π_{1}(fix(f)) is not total on ℕ, but it is easy to show by induction that π_{1}(fix(f)) is in fact total (on ℕ). Therefore fix(f) ∉ \overline{T} and hence T is not admissible. □

Lemma 6 If e_{1}[t/x] ↦ e_{2}, and e_{1}[t/x] is closed, and t is closed and noncanonical, then either

• there exists e′_{2} such that for any closed t′, e_{1}[t′/x] ↦ e′_{2}[t′/x], or

• there exist e′_{1} and t′ such that e_{1} ≡ e′_{1}[x/y], t ↦ t′ and for any closed t′′, e′_{1}[t′′, t/x, y] ↦ e′_{1}[t′′, t′/x, y].

Proof

Suppose e_{1} ≡ x. Then t ≡ e_{1}[t/x] ↦ e_{2}. Let e′_{1} = y and t′ = e_{2}. Then e′_{1}[t′′, t/x, y] ≡ t ↦ t′ ≡ e′_{1}[t′′, t′/x, y]. The remaining cases are by induction on the derivation of e_{1}[t/x] ↦ e_{2}. I show the lambda rules; the other cases are similar. Suppose the rule used is:

(λz.b)a ↦ b[a/z]

The term e_{1}[t/x] must have the form of a lambda abstraction applied to an argument. Thus e_{1} must be of the form (λz.b)a, since e_{1} ≡ x is already handled and e_{1} ≡ x a is impossible because t is noncanonical. Let e′_{2} = b[a/z] and suppose t′ is closed. Then:

e_{1}[t′/x] ≡ (λz.b[t′/x])(a[t′/x])
↦ b[t′/x](a[t′/x]/z)
≡ b[a/z][t′/x]  (since t′ is closed)
≡ e′_{2}[t′/x]

Suppose the rule used is:

{f ↦ f′ \atop f a ↦ f′ a}

Then it must be the case that e_{1} is of the form f_{1} a (since e_{1} ≡ x is already handled) and f_{1}[t/x] ↦ f_{2} (for some f_{2}). Hence the induction hypothesis holds for f_{1}. Suppose the first case holds: there exists f′_{2} such that for any closed t′, f_{1}[t′/x] ↦ f′_{2}[t′/x]. Let e′_{2} = f′_{2} a and suppose t′ is closed. Then:

e_{1}[t′/x] ≡ (f_{1}[t′/x])(a[t′/x])
↦ (f′_{2}[t′/x])(a[t′/x])
≡ e′_{2}[t′/x]

Suppose the second case holds: there exist f′_{1} and t′ such that f_{1} ≡ f′_{1}[x/y], t ↦ t′ and for any closed t′′, f′_{1}[t′′, t/x, y] ↦ f′_{1}[t′′, t′/x, y]. Let e′_{1} = f′_{1} a and suppose t′′ is closed. Then:

e′_{1}[t′′, t/x, y] ≡ (f′_{1}[t′′, t/x, y])(a[t′′, t/x, y])
≡ (f′_{1}[t′′, t/x, y])(a[t′′, t′/x, y]) (since y is not free in a)
↦ (f′_{1}[t′′, t′/x, y])(a[t′′, t′/x, y])
≡ e′_{1}[t′′, t′/x, y]
□

Lemma 7 For all f, e_{1} and e_{2} (where f is closed and x is the only free variable of e_{1}), there exist j and e′_{2} such that if e_{1}[fix(f)/x] ↦^{∗} e_{2} then e_{2} ≡ e′_{2}[fix(f)/x] and for all k ≥ j, e′_{2}[f^{k−j}/x] ≤ e_{1}[f^{k}/x].

Proof

I show the lemma for evaluations of length exactly one. The result then follows by induction on the length of the evaluation sequence, summing the numbers j.

Use Lemma 6. Suppose the first case holds: there exists e′_{2} such that for any closed t, e_{1}[t/x] ↦ e′_{2}[t/x]. Then e_{1}[fix(f)/x] ↦ e′_{2}[fix(f)/x] and, for any k, e_{1}[f^{k}/x] ↦ e′_{2}[f^{k}/x]. Thus e′_{2}[f^{k−0}/x] ≤ e_{1}[f^{k}/x]. Suppose the second case holds: there exists e′_{1} such that e_{1} ≡ e′_{1}[x/y], and for any closed t, e′_{1}[t, fix(f)/x, y] ↦ e′_{1}[t, f(fix(f))/x, y]. Let e′_{2} = e′_{1}[f x/y]. Then e_{1}[fix(f)/x] ↦ e′_{2}[fix(f)/x]. Suppose k ≥ 1, then e′_{2}[f^{k−1}/x] ≡ e′_{1}[f^{k−1}, f^{k}/x, y] ≤ e′_{1}[f^{k}, f^{k}/x, y] ≡ e_{1}[f^{k}/x]. □

Theorem 8 For all f, t and e (where f is closed), if ∀j. e[f^{j}/x] ≤ t, then e[fix(f)/x] ≤ t.

Proof

By induction on l that for all f, t and e (where f is closed), (∀j. e[f^{j}/x] ≤ t) ⇒ e[fix(f)/x] ≤_{l} t. The result follows by the definition of ≤. The basis is trivial.

Assume the induction hypothesis for l and ∀j. e[f^{j}/x] ≤ t. Let σ be a substitution such that σ(e[fix(f)/x]) and σ(t) are closed and suppose, without loss of generality, that σ does not substitute for x. Then σ(e[fix(f)/x]) ≡ σ(e)[fix(f)/x], σ(e[f^{j}/x]) ≡ σ(e)[f^{j}/x] (for any j), and the only free variable of σ(e) is x. Suppose σ(e[fix(f)/x]) ⇓ e′. By Lemma 7, e′ ≡ e′′[fix(f)/x] and, for some j and all k ≥ j, e′′[f^{k−j}/x] ≤ σ(e)[f^{k}/x]. Then, by assumption and transitivity, ∀k ≥ j. e′′[f^{k−j}/x] ≤ σ(t). Therefore, changing variables to replace k−j with k, e′′[f^{k}/x] ≤ σ(t) for any k.

Let e′′ = θ(x⃗_{1}.t_{1}, …, x⃗_{n}.t_{n}) (and suppose, without loss of generality, that x does not appear in any x⃗_{i}). Then σ(t) ⇓ θ(x⃗_{1}.t′_{1}, …, x⃗_{n}.t′_{n}) where, for 1 ≤ i ≤ n and any k, t_{i}[f^{k}/x] ≤ t′_{i}. By induction, t_{i}[fix(f)/x] ≤_{l} t′_{i}, for any i. Therefore σ(e[fix(f)/x]) ≤_{l+1} σ(t) and hence e[fix(f)/x] ≤_{l+1} t. □

Lemma 17

• Adm(A + B | y : S) if ∀s ∈ S. (A + B)[s/y] type and Adm(A | y : S) and Adm(B | y : S).

• Adm(Σx:A.B | y : S) if ∀s ∈ S. (Σx:A.B)[s/y] type and Σy:S.A type and Adm(A | y : S) and Adm(B[π_{1}(z), π_{2}(z)/y, x] | z : (Σy:S.A))

• Adm(ℕ | y : S)

• Adm(a_{1} = a_{2} in A | y : S) if ∀s ∈ S. (a_{1} = a_{2} in A)[s/y] type and Adm(A | y : S)

• Adm(\overline{A} | y : S) if ∀s ∈ S. \overline{A}[s/y] type and Adm(A | y : S)

• Adm(a in! A | y : S) if ∀s ∈ S. (a in! A)[s/y] type

Proof

I show the product and equality cases; the other cases are similar but easier.

Case 1: For the product case, let f, t, t′ and e be arbitrary. Suppose e^{[ω]} ∈ S and j is such that ∀k ≥ j. e^{[k]} ∈ S ∧ t^{[k]} = t^{′[k]} ∈ (Σx:A.B)[e^{[k]}/y]. It is necessary to show that t^{[ω]} = t^{′[ω]} ∈ (Σx:A.B)[e^{[ω]}/y]. Since e^{[ω]} ∈ S, it follows that (Σx:A.B)[e^{[ω]}/y]type. Both t^{[j]} and t^{′[j]} converge to pairs, so, by Corollary 5, t^{[ω]} ⇓ ⟨a, b⟩ and t^{′[ω]} ⇓ ⟨a′, b′⟩ for some terms a, b, a′ and b′. To get that b = b′ ∈ B[e^{[ω]}/y][a/x], it suffices to show that π_{2}(t^{[ω]}) = π_{2}(t^{′[ω]}) ∈ B[e^{[ω]}/y][π_{1}(t^{[ω]})/x]. Rearranging, it suffices to show equality in B[π_{1}(z), π_{2}(z)/y, x][⟨e, π_{1}(t)⟩^{[ω]}/z].

Since Adm(B[π_{1}(z), π_{2}(z)/y, x] | z : (Σy:S.A)), it suffices to show that ⟨e, π_{1}(t)⟩^{[ω]} ∈ Σy:S.A and ∀k ≥ j. ⟨e, π_{1}(t)⟩^{[k]} ∈ Σy:S.A ∧ π_{2}(t^{[k]}) = π_{2}(t^{′[k]}) ∈ B[π_{1}(z), π_{2}(z)/y, x][⟨e, π_{1}(t)⟩^{[k]}/z]. The former will follow from a ∈ A[e^{[ω]}/y] and the supposition. The left half of the latter also follows from the supposition. Rearranging the right half, it suffices to show that π_{2}(t^{[k]}) = π_{2}(t^{′[k]}) ∈ B[e^{[k]}/y][π_{1}(t^{[k]})/x], which follows from the supposition. The proof that a = a′ ∈ A[e^{[ω]}/y] is similar but easier. Hence t^{[ω]} = t^{′[ω]} ∈ (Σx:A.B)[e^{[ω]}/y].

Case 2: For the equality case, again let f, t, t′ and e be arbitrary. Suppose e^{[ω]} ∈ S and j is such that ∀k ≥ j. e^{[k]} ∈ S ∧ t^{[k]} = t^{′[k]} ∈ (a_{1} = a_{2} in A)[e^{[k]}/y]. It is necessary to show that t^{[ω]} = t^{′[ω]} ∈ (a_{1} = a_{2} in A)[e^{[ω]}/y]. Since e^{[ω]} ∈ S, it follows that (a_{1} = a_{2} in A)[e^{[ω]}/y] type. Both t^{[j]} and t^{′[j]} converge to ⋆, so, by Corollary 5, t^{[ω]} and t^{′[ω]} converge to ⋆. It remains to show that a_{1}[e^{[ω]}/y] = a_{2}[e^{[ω]}/y] ∈ A[e^{[ω]}/y]. Since Adm(A | y : S), it suffices to show that ∀k ≥ j. e^{[k]} ∈ S ∧ a_{1}[e^{[k]}/y] = a_{2}[e^{[k]}/y] ∈ A[e^{[k]}/y]. This follows since (a_{1} = a_{2} in A)[e^{[k]}/y] is inhabited for all k ≥ j. □

Lemma 19 Adm(Πx:A.B | y : S) if ∀s ∈ S. (Σx:A.B)[s/y] type and WCoAdm(A | y : S) and ∀s ∈ S, a ∈ A[s/y]. Adm(B[a/x] | y : S)

Proof

Let f, t, t′ and e be arbitrary. Suppose e^{[ω]} ∈ S and j is such that ∀k ≥ j. e^{[k]} ∈ S ∧ t^{[k]} = t^{′[k]} ∈ (Πx:A.B)[e^{[k]}/y]. I need to show that t^{[ω]} = t^{′[ω]} ∈ (Πx:A.B)[e^{[ω]}/y]. Since e^{[ω]} ∈ S, it follows that (Πx:A.B)[e^{[ω]}/y] type. Both t^{[j]} and t^{′[j]} converge to lambda abstractions, so, by Corollary 5, t^{[ω]} ⇓ λx.b and t^{′[ω]} ⇓ λx.b′ for some terms b and b′. Suppose a = a′ ∈ A[e^{[ω]}/y]. To get that b[a/x] = b′[a′/x] ∈ B[e^{[ω]}, a/y, x] it suffices to show that t^{[ω]}a = t^{′[ω]}a′ ∈ B[e^{[ω]}, a/y, x].

Since e^{[ω]} ∈ S, it follows that Adm(B[a/x] | y : S). Therefore, it suffices to show that for some j′ and all k ≥ j′, t^{[k]}a = t^{′[k]}a′ ∈ B[e^{[k]}, a/y, x]. Since WCoAdm(A | y : S), there exists j′′ such that ∀k ≥ j′′. a = a′ ∈ A[e^{[k]}/y]. Therefore j′ = max(j, j′′) suffices. □

Lemma 20

• A + B is (weakly) coadmissible for y in S if ∀s ∈ S. (A + B)[s/y] type and A and B are (weakly) coadmissible for y in S

• WCoAdm(Σx:A.B | y : S) if ∀s ∈ S. (Σx:A.B)[s/y] type and WCoAdm(A | y : S) and ∀s ∈ S, a ∈ A[s/y]. WCoAdm(B[a/x] | y : S)

• CoAdm(Σx:A.B | y : S) if ∀s ∈ S. (Σx:A.B)[s/y] type and Σy:S.A type and CoAdm(A | y : S) and CoAdm(B[π_{1}(z), π_{2}(z)/y, x] | z : (Σy:S.A))

• ℕ is strongly or weakly coadmissible for y in any S

• CoAdm(a_{1} = a_{2} in A | y : S) if ∀s ∈ S. (a_{1} = a_{2} in A)[s/y] type and CoAdm(A | y : S)

• \overline{A} is (weakly) coadmissible for y in S if ∀s ∈ S. \overline{A}[s/y] type and A is (weakly) coadmissible for y is S

• a in! A is strongly or weakly coadmissible for y in S if ∀s ∈ S. (a in! A)[s/y] type

Proof

The proof is largely similar to the preceding proofs, but inverted. I show the proofs for full coadmissibility of products and partial types.

Case 1: For the product case, let f, t, t′ and e be arbitrary. Suppose e^{[ω]} ∈ S, j is such that ∀k ≥ j. e^{[k]} ∈ S, and t^{[ω]} = t^{′[ω]} ∈ (Σx:A.B)[e^{[ω]}/y]. It is necessary to show that there exists j′ such that ∀k ≥ j′. t^{[k]} = t^{′[k]} ∈ (Σx:A.B)[e^{[k]}/y]. For any k ≥ j, (Σx:A.B)[e^{[k]}/y] type. Both t^{[ω]} and t^{′[ω]} converge to pairs, so, by compactness, there exists some j′′ such that for all k ≥ j′′, t^{[k]} and t^{[k]} converge to pairs. Thus it suffices to show that for some j′ ≥ max(j, j′′) and all k ≥ j′, π_{1}(t^{[k]}) = π_{1}(t^{′[k]}) ∈ A[e^{[k]}/y] and π_{2}(t^{[k]}) = π_{2}(t^{′[k]}) ∈ B[e^{[k]}, π_{1}(t^{[k]})/y, x]. I show the latter; the former is similar.

Rearranging, it suffices to show equality in B[π_{1}(z), π_{2}(z)/y, x][⟨e, π_{1}(t)⟩^{[k]}/z]. By coadmissibility, it suffices to show ⟨e, π_{1}(t)⟩^{[ω]} ∈ Σy:S.A and ∃j′′′. ∀k ≥ j′′′. ⟨e, π_{1}(t)⟩^{[k]} ∈ Σy:S.A and π_{2}(t^{[ω]}) = π_{2}(t^{′[ω]}) ∈ B[π_{1}(z), π_{2}(z)/y, x][⟨e, π_{1}(t)⟩^{[ω]}/z]. The first follows from the supposition and the second will follow from π_{1}(t^{[k]}) ∈ A[e^{[k]}/y] and the supposition. Rearranging the third, is suffices to show that π_{2}(t^{[ω]}) = π_{2}(t^{′[ω]}) ∈ B[e^{[ω]}/y][π_{1}(t^{[ω]})/x], which follows from the supposition.

Case 2: For the partial type case, let f, t, t′ and e be arbitrary. Suppose e^{[ω]} ∈ S, j is such that ∀k ≥ j. e^{[k]} ∈ S, and t^{[ω]} = t^{′[ω]} ∈ \overline{A}[e^{[ω]}/y]. I need to show that there exists j′ such that ∀k ≥ j′. t^{[k]} = t^{′[k]} ∈ \overline{A}[e^{[k]}/y]. For any k ≥ j, \overline{A}[e^{[k]}/y] type. Suppose t^{[ω]} does not converge. (Note the non-constructivity of this argument.) Then t^{′[ω]} does not converge and neither does t^{[k]} or t^{′[k]} for any k (since t^{[k]} ≤ t^{[ω]} and t^{′[k]} ≤ t^{′[k]} for all k). Thus for all k ≥ j, t^{[k]} = t^{′[k]} ∈ \overline{A}[e^{[k]}/y].

Suppose t^{[ω]} converges. Then t^{[ω]} = t^{′[ω]} ∈ A[e^{[ω]}/y]. By coadmissibility, there exists j′ such that ∀k ≥ j′. t^{[k]} = t^{′[k]} ∈ A[e^{[k]}/y]. Hence ∀k ≥ max(j, j′). t^{[k]} = t^{′[k]} ∈ \overline{A}[e^{[k]}/y]. □

Lemma 22 (Predicate-admissibility and weak and full coadmissibility of case analysis.)

Proof

The proof follows the same lines as those of Lemmas 17 and 20.

Lemma 26 The type {x : A | B} is admissible if:

• Adm(A), and

• Adm(B | x : A), and

• there exists b such that b[a/x] ∈ B[a/x] whenever a ∈ A and ∃b′. b′ ∈ B[a/x].

Proof

Let f, t and t′ be arbitrary. Suppose j is such that ∀k ≥ j. t^{[k]} = t^{′[k]} ∈ {x : A | B}. Since {x : A | B} is inhabited it is a type. Since Adm(A), t^{[ω]} = t^{′[ω]} ∈ A. By set membership, for all k ≥ j there exists b′ such that b′ ∈ B[t^{[k]}/x]. Thus b[t^{[k]}/x] ∈ B[t^{[k]}/x] for all k ≥ j. Hence b[t^{[ω]}/x] ∈ B[t^{[ω]}/x] follows by predicate-admissibility. □

Lemma 27 (Predicate-admissibility of set types.)

Proof

The proof follows the same lines as Lemma 26.

Lemma 28 (Weak and full coadmissibility and monotonicity of set types.)

Proof

The proof follows the same lines as Lemma 20 and Proposition 25.

Lemma 29 (Admissibility, predicate-admissibility, weak and full coadmissibility and monotonicity of quotient types.)

The proof follows the same lines as the proofs for the set type.

Theorem 30 There does not exist an algorithm that computes an integer j such that ∀k ≥ j. t = t′ ∈ \overline{T} [e^{[k]}/x], when given S, T, f, t, t′, e and i such that:

• ∀s ∈ S. \overline{T} [s/x] type

• CoAdm(T | x : S)

• e^{[ω]} ∈ S

• ∀k ≥ i. e^{[k]} ∈ S

• t = t′ ∈ \overline{T} [e^{[ω]}/x]

Proof

Suppose such an algorithm exists. Let g be an arbitrary term that computes a total function on integers; that is, g ∈ ℕ → ℕ. Given the algorithm, we may effectively determine whether g iterated on 1 ever computes 0, which is certainly undecidable. Let f = λh. λn. if n =_{N} 0 then 0 else h(gx) and let h = fix(f). Note that f ∈ \overline{ℕ → \overline{ℕ}}→ℕ→\overline{ℕ} and h ∈ ℕ→\overline{ℕ}. By construction, g iterated on 1 computes 0 if and only if h(1)↓.

We will use the algorithm to determine an upper bound on the number of recursive calls needed to simulate h. Let

S = \overline{ℕ}
T = x in! ℕ
f = as above
t, t′ = let y = h(1) in ⋆
e = w(1)
i = 0

Observe that e^{[ω]} = h(1) and e^{[k]} = (f^{k})(1), so the first four preconditions of the algorithm are satisfied. Moreover, CoAdm(T | x : S) can be shown constructively. For the final precondition, suppose t↓. Then h(1)↓ so t ∈ h(1) in! ℕ.

Therefore let j be the result computed by the algorithm. I show that f^{j}(1)↓ exactly when h(1)↓. Since f^{j}(1) approximates h(1), it follows that f^{j}(1)↓ implies h(1)↓. By the algorithm specification, t ∈ \overline{f^{j}(1) in! ℕ}. If h(1)↓ then t↓, so t ∈ f^{j}(1) in! ℕ and consequently f^{j}(1)↓.

Let h′ = \overbrace{f(f ⋯ f}^{j times}(λy.1) ⋯), and observe that f^{j}(1)↓ exactly when h′(1) ⇓ 0. Consequently h(1)↓ exactly when h′(1) ⇓ 0. However, h′ is total, so we may decide whether h(1)↓ by running h′(1). □