Monotone Recursive Definition of Predicates and Its Realizability Interpretation

Makoto Tatsuta Research Institute of Electrical Communication Tohoku University Sendai 980, JAPAN

             tatsuta@riec.tohoku.ac.jp

Abstract

The main aim of the paper is to construct a logic by which we can formalize properties of programs. Inductive definition or recursive definition plays a very important role for this purpose. Inductive definition has been studied for untyped theories, predicative typed theories and impredicative typed theories. Monotone recursive definition in an untyped theory is studied in this paper. The main point is realizability interpretation of monotone recursive definition.

Untyped predicative theory TID_{0} and TID_{1} are presented, which have monotone recursive definition of predicates. TID_{1} has full monotone recursive definition and TID_{0} has only restricted monotone recursive definition. qrealizability interpretation of TID_{0} and TID_{1} is defined. It is proved that the realizability interpretation of TID_{0} is sound and that the realizability interpretation of TID_{1} is not sound, though TID_{1} and its interpretation seem very natural.

1 Introduction

Our main aim is to construct a logic by which we can formalize properties of programs for verification, synthesis and transformation of programs. We present a theory TID_{0} for this aim.

Inductive definition or recursive definition plays a very important role for this purpose. Many important data structures programs use such as natural numbers, lists and trees are recursively defined by nature. The essence of control structures of programs is a loop structure, which is realized by recursive calls. Specifications and properties of programs can be formally represented in a natural way by recursive definition if the logic has the facility of recursive definition.

Inductive definition in formal theories was studies in the area of mathematical logic. The main purpose of these research was placed on proof theoretic strength of formal theories.

Many formal systems have been studied to formalize programs in the area of computer science. They are almost divided into two groups. One is typed theories and the other is untyped theories. Typed theories are also divided into two groups, which are predicative typed theories and impredicative typed theories.

Inductive definition was studied for theories of each group. For predicative typed theories, extensions of Martin-Löf’s type theory by adding inductive definition were studied [7, 2]. For impredicative typed theories, inductive definition attached to CC was studied [3, 9, 8]. For untyped theories, inductive generation of T_{0} [4], CIG of PX[5], μ of EON + μ [10, 6] were studied.

We study monotone recursive definition in an untyped theory TID_{0}. Only positive inductive definition has been studied [6] for constructive untyped theories before this time. Inductive generation of T_{0} and CIG of PX treat only a positive rank 0 case. EON + μ [10] can use only an almost strictly positive case and EON + μ [6] can treat only a positive case.

The semantics of inductive definition is given by the least fixed point. From the point of view of this semantics, an extension of a monotone case is natural. We try to extend inductive definition to a monotone case and point out some difficulty in this study.

Program extraction is one of the benefits we get when we use a constructive formal theory to treat properties of programs. Program extraction is to get a program from a constructive proof of its specification formula. One method of program extraction is to use realizability interpretation. In PX, for example, a LISP program is extracted from a proof of its specification by realizability. We want to use this facility of program extraction by realizability for TID_{0}.

The main point of this paper is realizability interpretation of monotone recursive definition.

We present untyped predicative theory TID_{0} and TID_{1}, which have monotone recursive definition of predicates. TID_{1} has full monotone recursive definition, which is one of our aims and TID_{0} has only restricted monotone recursive definition. We define q-realizability interpretation of TID_{0} and TID_{1}. This q-realizability interpretation is essentially the same as the realizability of EON + μ [10, 6]. We show that the realizability interpretation of TID_{0} in TID_{1} is sound and that the realizability interpretation of TID_{1} in TID_{1} is not sound, though TID_{1} and its interpretation seem very natural. The soundness proof for TID_{0} includes the soundness proof for a positive case of EON + μ [6] as a special case, though the proof for EON + μ seems much more complicated than the one for TID_{0}. The simplicity of our proof is brought by simplifying the condition to monotonicity.

In Section 2, we give definition of theory TID_{0} and TID_{1}. In Section 3, we briefly explain how useful the facility of recursive definition of predicates is and discuss related works. In Section 4, we discuss a model of TID_{1} and prove its consistency. In Section 5, we present q-realizability interpretation of TID_{0} and TID_{1}. We explain that this realizability interpretation of recursively defined predicates is natural. We prove the soundness theorem for TID_{0}. We show that the interpretation of TID_{1} is not sound.

2 Theory TID_{0} and TID_{1}

We present theory TID_{0} and TID_{1} in this section. Both are the same as Beeson’s EON[1] except for the rules of recursive definition of predicates. TID_{0} and TID_{1} are different only in the rules of recursive definition of predicates.

Definition 2.1. (Language of TID_{0} and TID_{1})

The language of TID_{0} and the one of TID_{1} are the same. This is based on a first order language but extended for recursive definition of predicates.

The constants are:

K, S, p, p_{0}, p_{1}, 0, s_{N}, p_{N}, E.

We choose combinators as a target programming language for simplicity. K and S mean the usual basic combinators. We have natural numbers as primitives, which are given by 0, a successor function s_{N} and a predecessor function p_{N}. We also have paring functions p, p_{0} and p_{1} as built-in, which correspond to cons, car and cdr in LISP respectively. E is a combinator judging equality of terms and corresponds to an if-then-else statement in a usual programming language.

We have only one function symbol:

App whose arity is 2. This means a functional application of combinators.

Terms are defined in the same way as for a usual first order logic. For terms s, t, we abbreviate App(s, t) as st. For terms s, t, we also use an abbreviation ⟨s, t⟩ ≡ pst, t_{0} ≡ p_{0}t and t_{1} ≡ p_{1}t.

The predicate symbols are:

⊥, ↓, N, = .

We have predicate variables, which a first order language does not have. The predicate variables are:

X, Y, Z,…, X^{∗}, Y^{∗}, Z^{∗},…. Each predicate variable has a fixed arity. We assume that the arity of X^{∗} is n + 1 if the arity of X is n.

Definition 2.2. (Formula)

1. If a, b are terms,

⊥, a↓, N(a), a = b are formulas.

2. If X is a predicate variable whose arity is n, X(x_{1},…, x_{n}) is a formula.

3. A formula is constructed from logical connectives &, ∨, →, ∀, ∃ in the same way as a first order language.

4. (μX.λx_{1} … x_{n}.A)(t_{1},…, t_{n}) is a formula where X is a predicate variable whose arity is n, A is a formula and t_{1},…, t_{n} are terms.

⊥ means contradiction. N(a) means that a is a natural number. a = b means that a equals to b.

We adopt a logic of partial terms, where some terms may fail to have any values [1]. a↓ means that a has a value.

The last case corresponds to recursively defined predicates. Remark that X and x_{1},…, x_{n} may occur freely in A. The intuitive meaning of a formula

(μX.λx_{1} … x_{n}.A(X, x_{1},…, x_{n}))(t_{1},…, t_{n}) is as follows: Let P be a predicate of arity n such that P is the least solution of an equation

P (x_{1},…, x_{n}) ↔ A(P, x_{1},…, x_{n}). Then (μX.λx_{1} … x_{n}.A(X, x_{1},…, x_{n}))(t_{1},…, t_{n}) means P (t_{1},…, t_{n}) intuitively.

We abbreviate a sequence as a bold type symbol, for example, x_{1},…, x_{n} as x.

Example 2.3.

We give an example of a formula. We assume the arity of a predicate variable P is 1. Then

(μP.λx.x = 0 ∨ ∃y(P (y) & x = s_{N}y))(x)

is a formula.

Among many axioms and inference rules of TID_{0} and TID_{1}, we discuss only inference rules of recursive definition of predicates here. The rest of axioms and inference rules are almost the same as EON [1] and we only list them in the appendix.

Let μ ≡ μP.λx.A(P) where x is a sequence of variables whose length is the same as the arity of a predicate variable P and A(P) is a formula displaying all the occurrences of P in a formula A. Suppose that

(μ1) ≡ A(μ) → μ(x),
(μ2) ≡ ∀x(A(C) → C(x)) → ∀x(μ(x) → C(x)),
(MONO) ≡ ∀x(X(x) → Y (x)) → ∀x(A(X) → A(Y)),
(MONO-Q) ≡ ∀xr(X^{∗}(r, x) → Y^{∗}(r, x)) →
∀xr((r q_{X}[X, X^{∗}] A(X)) → (r q_{X}[X, Y^{∗}] A(X)))

where X, Y, X^{∗}, Y^{∗} are predicate variables, A(X) is a formula displaying all the occurrences of a predicate variable X in a formula A, C(x) is a formula displaying all the occurrences of variables x in a formula C and x covers all the free variables of A(X). The notation q_{X}[X, X^{∗}] is defined in a later section.

We have 2 inference rules for TID_{0} and TID_{1} respectively. For TID_{0} the inference rules are as follows:

(MONO) (MONO-Q)

(μ1) (μR1′)

(MONO) (MONO-Q)

(μ2) (μR2′)

where X, Y, X^{∗}, Y^{∗} do not occur freely in open assumptions of deductions of the premises.

For TID_{1} the inference rules are as follows:

{(MONO) \atop (μ1)} (μR1)

{(MONO) \atop (μ2)} (μR2)

where X, Y do not occur freely in open assumptions of deductions of the premises.

The condition (MONO) states that a formula A(X) is monotone with respect to X.

The additional condition (MONO-Q) states that a formula e q_{X}[X, X^{∗}] A(X) is monotone with respect to X^{∗}.

We define TID^{−} as a theory TID_{1} except for the 2 inference rules of recursive definition of predicates.

3 Monotone Recursive Definition of Predicates

We will explain how useful the recursive definition of predicates is and discuss related works.

Let μ ≡ μP.λx.A(P) where x is a sequence of variables whose length is the same as the arity of a predicate variable P and A(P) is a formula displaying all the occurrences of P in a formula A. Suppose that (MONO) and (MONO-Q) hold for this A. So we can use (μ1) and (μ2) for A in each theory TID_{0} and TID_{1}. We will discuss (μ1) and (μ2).

By (μ1) and (μ2),

μ(x) ↔ A(μ).  (μ1′)

holds. This μ is the least solution of an equation for a predicate variable X:

X(x) ↔ A(X). Because

∀x(A(C) ↔ C(x)) → ∀x(μ(x) → C(x)) holds by (μ2) for any formula C(x).

We often want to define a predicate recursively. For example, we will define the predicate Nat which judges whether the argument is a natural number or not. One way to define it is as follows:

Nat(x) ≡ x = 0 ∨ ∃y(Nat(y) & x = s_{N}y). But it is not a definition in a usual sense since Nat appears also in the right hand side which is the body of the definition of the predicate. What we want to present by this equation is the least solution of a recursion equation for a predicate variable X:

X(x) ↔ x = 0 ∨ ∃y(X(y) & x = s_{N}y). In TID_{0} and TID_{1} this solution can be represented by a formula

(μP.λx.x = 0 ∨ ∃y(P (y) & x = s_{N}y))(x) and (μ1) and (μ2) state this formula is actually the least solution of the equation. By this facility we can define Nat in TID_{0} and TID_{1} as follows:

Nat(x) ≡ (μP.λx.x = 0 ∨ ∃y(P (y) & x = s_{N}y))(x) For this example, (μ2) represents the mathematical induction for natural numbers classified by Nat. (μ2) represents the generalized induction principle in general.

By the facility of recursive definition of predicates, many useful recursive data structures such as natural numbers, lists and trees can be defined inside the theory [10]. The induction principle corresponding to each data structure is derived from (μ2) for each case. The list induction is derived from (μ2) for a definition of lists and the tree induction is derived from (μ2) for a definition of trees.

We want to write specification formulas of programs in the theory. Recursive calls are one of the most important control structures of programs. In this case recursively defined predicates are also useful since recursive calls can be represented naturally by recursively defined predicates. Especially predicates defined recursively by Horn clauses in Prolog can be represented directly in the theory [10].

Recursive definition or inductive definition has been studied in untyped predicative theories. The restricting condition for A(P) varies for the theories. In PX[5], we can use (μP.λx.A(P))(t) only when every occurrence of P in A(P) is positive and A(P) is a Harrop formula. In EON + μ [10], we can use it only when every occurrence of P in A(P) is positive and for each occurrence P one of the following 2 conditions holds:

1. the occurrence appears in some Harrop subformula of A(P).

2. the occurrence is strictly positive in A(P).

In EON + μ [6], we can use it only when every occurrence of P in A(P) is positive. In TID_{0} we have presented, we can use it only when both of the following 2 conditions hold:

1. (MONO) A(P) is monotone with respect to P,

2. (MONO-Q) r q A(P) is monotone with respect to P^{∗}.

TID_{0} has the weakest restrictions on A(P) among the above theories.

We want to relax the restricting conditions since recursively defined predicates can be used more widely and more flexibly in the case of weaker restrictions. But the theory is inconsistent if there are no restrictions because we can use μP.¬P and (μP.¬P) ↔ ¬(μP.¬P) holds by (μ1) and (μ2). From the point of view of an intended model, recursively defined predicates means the least fixed point. In this model construction we use only monotonicity. Therefore we have a question: Can we use recursively defined predicates on only the condition that a formula A(P) is monotone with respect to a predicate variable P ? From the point of view of consistency of the theory, the answer is yes. This is stated by the fact TID_{1} is consistent. But the restriction of PX and EON + μ were made also for soundness of realizability interpretation. So we have another question: Is realizability interpretation of monotone recursive definition sound ? The answer is no for our realizability interpretation defined in a later section, though it seems very natural. This is stated by the fact realizability interpretation of TID_{1} is not sound. We can relax the restriction more than positivity, but still we need some restrictions besides monotonicity for our realizability interpretation. This corresponds to TID_{0} and actually realizability interpretation of TID_{0} is sound.

4 Model of TID_{1}

We will briefly explain semantics of TID_{1} by giving its intended model. Since TID_{1} includes TID_{0}, this model also explains semantics of TID_{0}.

We will use the well-known least fixed point theorem for model construction.

Theorem 4.1. (Least Fixed Point)

Suppose S be a set, p(S) be a power set of S. If f : p(S) → p(S) is a monotone function, there exists a such that a ∈ p(S) and

1. f(a) = a,

2. For any b ∈ p(S), if f(b) ⊂ b, then a ⊂ b.

a is abbreviated as lfp(f).

We will construct a model M′ of TID_{1} extending an arbitrary model M of TID^{−}. Our intended model of TID^{−} is the closed normal term model whose universe is the set of closed normal terms and in which equality of elements is decidable [1]. We denote the universe by U.

We will define ρ ⊧ A in almost the same way as for a first order logic where A is a formula and ρ is an environment which assigns a first order variable to an element of U and a predicate variable of arity n to a subset of U^{n} and which covers all the free first order variables and all the free predicate variables of A. We present only the definition for the case (μP.λx.A(P))(t).

Define F as follows:

|x| = n,

F : p(U^{n}) → p(U^{n}),
F (X) = {x ∈ U^{n} | ρ[P := X] ⊧ A(P)},

where ρ[P := X] is defined as follows:

ρ[P := X](P) = X,

ρ[P := X](x) = ρ(x) if x is not P .

Then ρ ⊧ (μP.λx.A(P))(t) is defined as t ∈ lfp(F) if F is monotone. ρ ⊧ (μP.λx.A(P))(t) is defined as true if F is not monotone.

Theorem 4.2.

If TID_{1} ⊢ A, then ρ ⊧ A for any environment ρ which covers all the free variables of A.

Theorem 4.3.

TID_{0} and TID_{1} are consistent.

5 q-realizability Interpretation of TID_{0} and TID_{1}

We will explain motivation of our realizability. We start with a usual q-realizability and try to interpret (μP.λx.A(P, x))(x). Let μ be μP.λx.A(P, x) and suppose that (μ1) and (μ2) hold for this μ. Then μ(x) ↔ A(μ, x) holds. We want to treat μ(x) and A(μ, x) in the same manner. So we require (e q μ(x)) ↔ (e q A(μ, x)). Therefore it is very natural to define e q μ(x) as μ^{∗}(e, x) where μ^{∗}(e, x) is the least solution of a recursive equation for a predicate variable X^{∗}:

X^{∗}(e, x) ↔ (e q A(μ, x))[(r q μ(y)) := X^{∗}(r, y)]. where [(r q μ(y)) := X^{∗}(r, y)] of the right hand side means replacing each subformula r q μ(y) by a subformula X^{∗}(r, y) in a formula e q A(μ, x). We get the following definition of our realizability by describing syntactically this idea. This interpretation is an immediate extension of [10, 6].

Our q-realizability interpretation of TID_{0} and the one of TID_{1} are the same, for the language of TID_{0} and the one of TID_{1} are also the same.

Definition 5.1. (Harrop formula)

1. Atomic formulas ⊥, a↓, N(a) and a = b are Harrop.

2. If A and B are Harrop, then A & B, C → B, ∀xA and (μP.λx.A)(x) are also Harrop.

Since a Harrop formula does not have computational meanings, we can simplify the q-realizability interpretation of them.

Definition 5.2. (Abstract)

1. A predicate constant of arity n is an abstract of arity n.

2. A predicate variable of arity n is an abstract of arity n.

3. If A is a formula, λx_{1} … x_{n}.A is an abstract of arity n.

We identify (λx_{1} … x_{n}.A)(t_{1},…, t_{n}) with A[x_{1} := t_{1},…, x_{n} := t_{n}] where [x_{1} := t_{1},…, x_{n} := t_{n}] denotes a substitution.

Definition 5.3. (q-realizability Interpretation)

Suppose A is a formula, P_{1},…, P_{n} is a sequence of predicate variables whose arities are m_{1},…, m_{n} respectively and F_{1}, G_{1},…, F_{n}, G_{n} is a sequence of abstracts whose arities are m_{1}, m_{1} + 1,…, m_{n}, m_{n} + 1 respectively.

(e q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] A) is defined by induction on the construction of A as follows.

We abbreviate q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] as q′, q_{P_{1},...,P_{n},P} [F_{1}, G_{1},…, F_{n}, G_{n}, F, G] as q′_{P} [F, G], F_{1},…, F_{n} as F and P_{1},…, P_{n} as P.

1. (e q′ A) ≡ e = 0 & A_{P}[F] where A is Harrop.

2. (e q′ P_{i}(t)) ≡ G_{i}(e, t) & e↓.

3. (e q′ Q(t)) ≡ Q^{∗}(e, t) & e↓ where Q ≢ P_{i} (1 ≤ i ≤ n).

4. (e q′ A & B) ≡ (e_{0} q′ A) & (e_{1} q′ B).

5. (e q′ A ∨ B) ≡ N(e_{0}) & (e_{0} = 0 → (e_{1} q′ A) & A_{P}[F]) & (e_{0} ≠ 0 → (e_{1} q′ B) & B_{P}[F]).

6. (e q′ A → B) ≡ ∀q((q q′ A) & A_{P}[F] → (eq q′ B)) & e↓.

7. (e q′ ∀xA(x)) ≡ ∀x(ex q′ A(x)).

8. (e q′ ∃xA(x)) ≡ (e_{1} q′ A(e_{0})) & A(e_{0})_{P}[F].

9. (e q′ (μX.λx.A(X))(t)) ≡ (μX^{∗}.λex.(e q′_{X}[μ_{P}[F], X^{∗}] A(X)))(e, t) where μ ≡ μX.λx.A(X).

In the above definition,_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] means a substitution. Our realizability interpretation is something like a realizability interpretation with a substitution.

This interpretation works well for TID_{0} but goes wrong for TID_{1}. The interpretation of TID_{0} is sound but the interpretation of TID_{1} is not sound. The difference is brought by the additional condition (MONO-Q). In general, we cannot conclude that e q_{X}[X, X^{∗}] A is monotone with respect to X^{∗} even if A is monotone with respect to X. For such A, we in general cannot use (μ1) and (μ2) for e q (μX.λx.A)(t) in TID_{1}. On the other hand, we can always use (μ1) and (μ2) for e q (μX.λx.A)(t) in TID_{1} if the additional (MONO-Q) guarantees that e q_{X}[X, X^{∗}] A is monotone with respect to X^{∗}.

Theorem 5.4. The q-realizability interpretation is not sound for TID_{1}. That is, there is a formula A such that TID_{1} ⊢ A holds but TID_{1} ⊢ e q A does not hold for any e.

Proof 5.5. Let X,Y be predicate variables of arity 0 and

μ ≡ μX.(X → X) & Y,

μ^{∗}(r) ≡ (r q μ),
A ≡ μ → Y.

Then clearly TID_{1} ⊢ A holds. But TID_{1} ⊢ e q A does not hold for any e. We will show it by a model given in Section 4. We have

(e q A) ↔ ∀r(μ^{∗}(r) & μ → Y^{∗}(er) & er↓) & e↓,

μ^{∗}(r) ≡ (μX^{∗}.λr.(r q[μ, X^{∗}] (X → X) & Y))(r)
↔ (μX^{∗}.λr.∀q(X^{∗}(q) & μ → X^{∗}(r_{0}q) & r_{0}q↓) & r↓ & Y^{∗}(r_{1}))(r).

Choose ρ such that ρ ⊧ Y and ρ[Y^{∗}] = ϕ. Define F as follows:

F : p(U) → p(U),

F (V) = {r ∈ U | ρ[X^{∗} := V] ⊧ ∀q(X^{∗}(q) & μ → X^{∗}(r_{0}q) & r_{0}q↓) & r↓ & Y^{∗}(r_{1})}. Since F is not monotone, ρ′ ⊧ μ^{∗}(r) holds for any u ∈ U and ρ′ = ρ[r := u]. Put u = 0 and ρ′ = ρ[r := 0]. Then we have

ρ′ ⊧ μ^{∗}(r),

ρ′ ⊧ μ,
ρ′ |̸= Y^{∗}(er).

Therefore we have

ρ′ |̸= μ^{∗}(r) & μ → Y^{∗}(er) & er↓. Hence

ρ |̸= ∀r(μ^{∗}(r) & μ → Y (er) & er↓).

Therefore TID_{1} ⊬ e q A. □

We will discuss the realizability interpretation of TID_{0} in TID_{1}.

Proposition 5.6. Suppose that (MONO-Q) holds for every B(X) such that A has a subformula (μX.λx.B(X))(t). Then

TID_{1} ⊢ (e q A) → e↓.

Proof 5.7. By induction on A. □

Proposition 5.8. Let μ ≡ μP.λx.A(P) and suppose that (MONO-Q) holds for A(P). Then

TID_{1} ⊢ (e q μ(x)) ↔ (e q A(μ)) holds. Proof 5.9. From (μ1) and (μ2). □ This proposition shows that the definition of realizability satisfies our first motivation. Proposition 5.10. If TID_{0} ⊢ (MONO) and TID_{0} ⊢ (MONO-Q) hold,

TID_{1} ⊢ λx.x q (μ1) holds. Proof 5.11. Immediate from proposition 5.8. □ Proposition 5.12.

TID_{1} ⊢ λq.μf.λxr.qx(mfx(m(λxr.r)xr)) q (μ2), where

TID_{1} ⊢ m q (MONO).

We prove it in the appendix. Theorem 5.13. (Soundness Theorem) If TID_{0} ⊢ A, we can get a term e from a proof and TID_{1} ⊢ (e q A) holds where all the free variables of e are included in all the free variables of A. Proof 5.14. By induction on the proof of TID_{0} ⊢ A. Use proposition 5.10 and proposition 5.12. □ By the soundness of realizability, we get the term existence property, the disjunction property, the program extraction theorem and consistency with some choice axioms in a usual way. Theorem 5.15. (Term Existence Property) If TID_{0} ⊢ ∃xA(x), we can get a term t from a proof and TID_{1} ⊢ A(t) holds.

Theorem 5.16. (Program Extraction) If there exists a term j such that TID_{1} ⊢ ∀x(A(x) → (j(x) q A(x))) and TID_{0} ⊢ ∀x(A(x) → ∃yB(x, y)), we can get a program f from a proof and TID_{1} ⊢ ∀x(A(x) → f(x)↓ & B(x, f(x))) holds.

We show the discussion of realizability of [10, 6] is a special case of the above discussion.

Proposition 5.17. If P occurs only positively in A(P), (MONO) and (MONO-Q) hold.

Corollary 5.18. TID_{0} is an extension of EON + μ where EON + μ is presented in [6].

If we choose an appropriate monotone realizer m for A(P) where P is positive in A(P), we get almost the same soundness proof for EON + μ as in [10, 6]. But the soundness proof of this paper is simpler than soundness proofs for EON + μ in [10, 6] because of the monotonicity condition.

Acknowledgements

I’m deeply grateful to Prof. Masahiko Sato for invaluable discussions and comments.

References

[1] M. Beeson. Foundations of Constructive Mathematics. Springer, 1985.

[2] R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.

[3] T. Coquand and C. Paulin. Inductively Defined Types. Manuscript, 1989.

[4] S. Feferman. Constructive theories of functions and classes, In: M. Boffa, D. van Dalen and K. McAloon, editors. Logic Colloquium ’78, Proceedings of the Logic Colloquium at Mons, pages 159–224. North-Holland, 1979.

[5] S. Hayashi and H. Nakano. PX: A Computational Logic. MIT Press, 1988.

[6] S. Kobayashi and M. Tatsuta. Realizability Interpretation of Generalized Inductive Definitions. Submitted, 1989.

[7] P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

[8] C. Paulin-Mohring. Extracting F_{ω}’s programs from proofs in the Calculus of Constructions. In 16^{th} Symp. Principles of Programming Languages, pages 89–104. ACM, 1989.

[9] F. Pfenning and C. Paulin-Mohring. Inductively Defined Types in the Calculus of Constructions. Technical Report CMU-CS-89-209, School of Computer Science, Carnegie Melon University, 1989.

[10] M. Tatsuta. Program Synthesis Using Realizability. Theoretical Computer Science, to appear.

A Axioms and Inference Rules of TID_{0} and TID_{1}

Axioms for Partial Terms:

x↓ (x is a variable)  (T1)
c↓ (c is a constant)  (T2)
N(t) → t↓ (t is a term)  (T3)
s = t → s↓ & t↓ (s, t are terms)  (T4)
st↓ → s↓ & t↓ (s, t are terms)  (T5)

(s↓ → s = t) & (t↓ → s = t) is abbreviated as s ≃ t. The logical axioms and inference rules are the same as the ones of a usual intuitionistic logic except for the following quantifier rules.

\begin{matrix}{A(a) \atop ∀xA(x)} (∀I) & \begin{matrix}∀xA(x) & t↓ \\ A(t) \end{matrix} (∀E) \\ \begin{matrix}A(t) & t↓ \\ ∃xA(x) \end{matrix} (∃I) & \begin{matrix}∃xA(x) & [A(a)] ; ⋮ . ; C \\ C \end{matrix} ; (∃E) \end{matrix}

Axioms for Equality:

∀x(x = x)  (E1)
∀x, y(x = y & A(x) → A(y))  (E2)

Axioms for Combinators:

∀x, y(Kxy = x)  (C1)
∀x, y(Sxy↓)  (C2)
∀x, y, z(Sxyz ≃ xz(yz))  (C3)

Axioms for Pairing:

∀x, y(p_{0}(pxy) = x)  (P1)
∀x, y(p_{1}(pxy) = y)  (P2)
∀x(p_{0}x↓)  (P3)
∀x(p_{1}x↓)  (P4)

Axioms for Natural Numbers:

N(0)  (N1)
∀x(N(x) → N(s_{N}x))  (N2)
∀x(N(x) → p_{N}(s_{N}x) = x)  (N3)
∀x(N(x) → s_{N}x ≠ 0)  (N4)
A(0) & ∀x(N(x) & A(x) → A(s_{N}x)) → ∀x(N(x) → A(x))  (N5)

Decidable Equality:

∀x, y(x = y ∨ x ≠ y)  (D1)
∀x, y, a, b(x = y → Exyab = a)  (D2)

∀x, y, a, b(x ≠ y → Exyab = b)  (D3)
s ≠ t (s and t are closed normal terms and s ≢ t)  (D4)

B Proof of proposition 5.12

Suppose that

m q ∀x(X(x) → Y (x)) → ∀x(A(X) → A(Y)). By expanding it, we get

∀f(∀xr(X^{∗}(r, x) & X(x) → Y^{∗}(fxr, x)) & ∀x(X(x) → Y (x)) →

∀xr((r q_{X}[X, X^{∗}] A(X)) & A(X) → (mfxr q_{X}[Y, Y^{∗}] A(X)))). (1)

Lemma B.1. Suppose that

m q ∀x(X(x) → Y (x)) → ∀x(A(X) → A(Y)). Then

(r q_{X}[F, G] A(X)) & A(F) → (m(λxr.r)xr q_{X}[F, λrx.(F (x) & G(r, x))] A(X)) holds.

Proof B.2. Put

X := F,
Y := F,
X^{∗} := G,
Y^{∗} := λrx.(F (x) & G(r, x)),
f := λxr.r

in (1). Then we get the conclusion of the lemma. □

Proof B.3. (of proposition 5.12) We assume that

q q ∀x(A(C) → C(x)),  (2)
A(C) → C(x).  (3)

Let

f ≡ μf.λxr.qx(mfx(m(λxr.r)xr)).

We will show

f q ∀x(μ(x) → C(x)) under these conditions. This is equivalent to

∀xr((μP^{∗}.λrx.(r q_{P} [μ, P^{∗}] A(P)))(r, x) & μ(x) → (fxr q C(x))). Therefore by (μ2) it is sufficient to show

∀xr((r q_{P} [μ, λrx.(μ(x) → (fxr q C(x)))] A(P)) → μ(x) → (fxr q C(x))). From lemma B.1 and (MONO-Q) it is sufficient to show

∀xr((m(λxr.r)xr q_{P} [μ, λrx.(fxr q C(x))] A(P))&A(μ)→(fxr q C(x))).(4)

Put X := μ, Y := C, X^{∗} := λrx.(fxr q C(x)), Y^{∗} := λrx.(r q C(x)), f := f

in (1), then we get

∀xr((r q_{X}[μ, λrx.(fxr q C(x))] A(X)) & A(μ) → (mfxr q A(C))). (5)

We will show (4). Fix x and r and suppose that

m(λxr.r)xr q_{P} [μ, λrx.(fxr q C(x))] A(P),  (6)
A(μ).  (7)

We will show fxr q C(x) under these conditions. By (5), (6) and (7), we have

mfx(m(λxr.r)xr) q A(C). By (2),

qx(mfx(m(λxr.r)xr)) q C(x). By the definition of f, we have

fxr q C(x).□