Realizability Interpretation of Generalized Inductive Definitions

Satoshi Kobayashi^{∗}  Makoto Tatsuta^{†}

Abstract

Generalized inductive definitions give a way of defining a predicate as the least solution P of the equation P ↔ A[P] where a predicate variable P may occur in a formula A[P] positively. This paper gives a q-realizability interpretation of generalized inductive definitions and prove the soundness of the interpretation.

1 Introduction

We study q-realizability of generalized inductive definitions to give a logical system in which we can formalize properties of programs by using generalized inductive definitions and extract a program from a constructive proof by q-realizability. This paper presents an improved version of the main result of [10].

In recent years, the idea of “proof-as-program” has drawn much attention in the area of computer science [2, 8]. The key of the idea is to make use of the existence property of a constructive formal system to produce programs. The existence property holds for a constructive formal system. When we prove an existence theorem constructively, by the existence property, we can extract a program from the proof which computes the solution.

Various metamathematical devices can be used to extract programs. One possibility is to use a q-realizability interpretation or its variants. Actually, Hayashi and Nakano [7] adopted a variant of Grayson-type q-realizability in their system PX to extract a LISP program. Another possibility is to work in constructive type theories [4, 9].

We use realizability to extract programs from constructive proofs.

The inductive definition principle of predicates (or sets) is significant in computer science for the following reasons. Firstly, as is shown by the studies in logic programming and program specification, inductive definitions of predicates by Prolog-like Horn clauses are very useful in program specification. The generalized inductive definitions include the inductive definitions by Horn clauses. Secondly, many important data types such as integers, lists, trees, … etc. are inductively defined. Thirdly, as Hayashi and Nakano [7] pointed out, inductive definitions play essentially important roles in extraction of efficient programs from constructive proofs.

For these reasons, logical systems to formalize properties of programs such as program extraction systems should admit a sufficiently broad class of inductive definitions.

Feferman [5, 6] introduced the constructive theory T_{0} of functions and classes, and defined some forms of realizability for it. T_{0} has axioms for accessibility inductive definition of classes. Buchholz [3] deals with recursive r-realizability for strictly positive ID_{ν}^{i}, which is a theory of ν-times iterated strictly positive inductive definitions. In Hayashi and Nakano’s PX [7], the inductive definition principle called CIG (Conditional Inductive Generation) is available. Operator forms of CIG are restricted to positive rank 0 forms. (Roughly speaking, “rank 0” means “Harrop”.)

Tatsuta [10] deals with a more general case than these works. In his system, an inductive operator form A[X] must be positive and must satisfy the following side condition: every occurrence of X in A[X] must be either strictly positive or contained in a Harrop subformula of A[X]. He defined the q-realizability interpretation for this class of inductive definitions and proved its soundness. The disadvantage of the work is that the side condition seems quite artificial.

∗Department of Applied Mathematics and Informatics, Ryukoku University, Seta, Ohtsu, 520-21, Japan. e-mail:

satoshi@whale.ryukoku.ac.jp

†Research Institute of Electrical Communication, Tohoku University, 2-1-1 Katahira, Sendai 980, Japan. e-mail:

tatsuta@riec.tohoku.ac.jp

This paper is based on [10] and improves the theoretical results given in [10]. In this paper, we define a q-realizability interpretation of arbitrary positive inductive definitions (with no side conditions) and prove the soundness of the interpretation. We show that the artificial side condition given in [10] is superfluous and can be removed.

By the improved result given by this paper, our system can use non-strictly positive inductive definitions, which the system given in [10] cannot cover. Therefore our system can be used to extract programs which treat non-strictly-positive inductive datatypes. In particular, our system can formalize continuations, whose datatype cont is given by cont = 1 + ((cont → α) → α).

Higher order codings of higher order systems such as the second order predicate logic PA2 also give the generalized inductive definitions. By the well-known fact, q-realizability for the system PA2 gives monotone inductive definitions. We do not choose the framework of higher order codings for the following reasons. Firstly, those systems which have the facility of higher order codings are impredicative and too strong to be used in program extraction. Secondly, induction schemata given by higher order codings do not give loop structures to programs since (e q μ) ↔ (e q A[μ]) does not hold where μ ≡ μX.A[X].

The definition of our realizability is essentially due to Tatsuta [10]. The key lemma and the main result were proved by Kobayashi.

Section 2 presents the theory EON + μ. Section 3 defines the q-realizability interpretation for EON + μ. Section 4 proves the soundness theorem of the interpretation.

2 Language and Axioms of EON + μ

In this section, we introduce the formal system EON + μ, which is a theory of finitely iterated inductive definitions. This system is an extension of Beeson’s formal system EON ([1]). To keep the argument as abstract as possible, we chose EON as the base theory rather than Heyting arithmetic. Our system is also an extension of the original version of EON + μ described in Tatsuta [10].

2.1 Language

1. Constant symbols: k, s, p, p_{0}, p_{1}, 0, s_{N}, p_{N} and d.

2. Function symbol: Ap.

3. Predicate symbols: ⊥, ↓, N and =.

4. Predicate variables: P, Q, …. Each predicate variable has its arity. An arity is a nonnegative integer. For each non-negative integer n, we have countably many predicate variables of arity n.

We use combinators as the target programming language. k and s are usual basic combinators. We have pairs as primitive by p, p_{0} and p_{1} which correspond to cons, car and cdr in LISP respectively. We have natural numbers as primitive by the zero 0, the successor s_{N} and the predecessor p_{N}. d is a combinator judging the equality of natural numbers and corresponds to an if-then-else statement in usual programming languages. Ap means the functional application. ⊥ means the contradiction. a↓ means that a term a has a value. N(a) means that a term a is a natural number. a = b means that a term a is equal to a term b. A predicate variable is quantified only by a μ constructor and is not quantified by ∀ and ∃.

2.2 Definition (Term)

1. Variables and constants are terms.

2. If t and s are terms, then Ap(t, s) is a term.

We write ts instead of Ap(t, s). pts is usually written as ⟨t, s⟩.

2.3 Definition (E-formula)

We define E-formulae (“E-” stands for “extended”) and their positive (negative) free predicate variables S_{+}(A) (S_{−}(A) resp.) simultaneously as follows.

1. ⊥ is an atomic E-formula. S_{+}(⊥) = S_{−}(⊥) = ∅.

2. t↓ is an atomic E-formula if t is a term. S_{+}(t↓) = S_{−}(t↓) = ∅.

3. N(t) is an atomic E-formula if t is a term. S_{+}(N(t)) = S_{−}(N(t)) = ∅.

4. t = s is an atomic E-formula if t and s are terms.

S_{+}(t = s) = S_{−}(t = s) = ∅.

5. P (t̄) is an atomic E-formula if P is a predicate variable of arity n and t̄ is a list of terms of length n. S_{+}(P (t̄)) = { P }, S_{−}(P (t̄)) = ∅.

6. A & B is an E-formula if A and B are E-formulae.

S_{+}(A & B) = S_{+}(A) ∪ S_{+}(B), S_{−}(A & B) = S_{−}(A) ∪ S_{−}(B).

7. A ∨ B is an E-formula if A and B are E-formulae.

S_{+}(A ∨ B) = S_{+}(A) ∪ S_{+}(B), S_{−}(A ∨ B) = S_{−}(A) ∪ S_{−}(B).

8. A → B is an E-formula if A and B are E-formulae.

S_{+}(A → B) = S_{−}(A) ∪ S_{+}(B), S_{−}(A → B) = S_{+}(A) ∪ S_{−}(B).

9. ∀xA(x) is an E-formula if x is a variable and A(x) is an E-formula.

S_{+}(∀xA(x)) = S_{+}(A(x)), S_{−}(∀xA(x)) = S_{−}(A(x)).

10. ∃xA(x) is an E-formula if x is a variable and A(x) is an E-formula.

S_{+}(∃xA(x)) = S_{+}(A(x)), S_{−}(∃xA(x)) = S_{−}(A(x)).

11. ((x̄).A)(t̄) is an E-formula if A is an E-formula, x̄ is a list of variables of length n and t̄ is a list of terms of length n.

S_{+}(((x̄).A)(t̄)) = S_{+}(A), S_{−}(((x̄).A)(t̄)) = S_{−}(A).

12. (μP.(x̄).A)(t̄) is an E-formula if P is a predicate variable of arity n, x̄ is a list of variables of length n, t̄ is a list of terms of length n and P is not in S_{−}(A).

S_{+}((μP.(x̄).A)(t̄)) = S_{+}(A) − {P }, S_{−}((μP.(x̄).A)(t̄)) = S_{−}(A).

The intended meaning of μP.(x̄).A[P] is the least predicate P such that ∀x̄(P (x̄) ↔ A[P]).

2.4 Notation

A symbol with an overbar denotes a list of expressions. For example, we often use t̄ to denote a list of terms.

t̄↓ denotes t_{1}↓ & … & t_{n}↓. We use the following abbreviations: ¬A denotes (A → ⊥) for an E-formula A. a ≠ b denotes

(a = b → ⊥) for terms a and b.

2.5 Definition

1. P occurs freely in A if P is in S_{+}(A) or in S_{−}(A).

2. A free predicate variable P in A are bound by μ in (μP.(x̄).A)(t̄).

3. P is positive (negative) in A if P is not in S_{−}(A) (S_{+}(A), respectively).

In the following, we consider only such E-formula A that S_{+}(A) ∩ S_{−}(A) = ∅.

The set of free predicate variables FPV (A) of A is defined by FPV (A) = S_{+}(A) ∪ S_{−}(A).

2.6 Definition (E-predicate)

1. Predicate symbols ⊥, ↓, N and = are E-predicates with arity 0,1,1 and 2 respectively.

2. A predicate variable P with arity n is an E-predicate with arity n.

3. μP.(x̄).A is an E-predicate with arity n if (μP.(x̄).A)(x̄) is an E-formula and the length of x̄ is n.

4. (x̄).A is an E-predicate with arity n if A is an E-formula and the length of x̄ is n.

We write arity(A) to denote the arity of E-predicate A. Free predicate variables FPV (F) of an E-predicate F are defined in the same way as an E-formula.

2.7 Definition (Formula, Predicate)

A formula (predicate) is an E-formula (E-predicate, resp.) with no free occurrences of predicate variables.

2.8 Definition (Substitution)

Substitution of terms for variables is defined as usual. For terms t and u and a variable x, t[u/x] denotes a term obtained from t by replacing all the free occurrences of x by u. Substitution of predicates for predicate variables in a formula (or a predicate) is also defined as usual. For a formula A, a predicate variable P and a predicate F, A_{P} [F] denotes a formula obtained from A by replacing all the free occurrences of P by F.

2.9 Logical Rules and Axioms

The underlying logic of our theory is Beeson’s formal system LPT (Logic of Partial Terms). It is a variant of first order intuitionistic predicate calculus. The propositional axioms and rules of inference are as usual.

The quantifier axioms and rules are as follows:

(Q1)  \frac{B → A}{B → ∀xA}  (x not free in B),

(Q2)  \frac{A → B}{∃xA → B}  (x not free in B),
(Q3)  ∀xA & t↓ → A[t/x],
(Q4)  A[t/x] & t↓ → ∃xA.

The equality axioms are as follows:

(E1)  x = x & (x = y → y = x),
(E2)  t ≃ s & ϕ(t) → ϕ(s),

(E3)  t = s → t↓ & s↓.

Here t and s are terms, x and y are variables, and t ≃ s is an abbreviation of t↓ ∨ s↓ → t = s. The axioms of definedness are as follows:

(S1)  x↓  (every variable x),
(S2)  c↓  (every constant symbol c),
(S3)  ts↓ → t↓ & s↓,
(S4)  N(t) → t↓,
(S5)  P (t̄) → t̄↓,
(S6)  (μP.(x̄).A)(t̄) → t̄↓.

In S3 and S4, t and s are terms. In S5 and S6, P is a predicate variable and t̄ is a list of terms.

For details, see Beeson[1, Chapter VI].

2.10 Non-logical Axioms

Non-logical axioms of our theory are those of Beeson’s EON, axioms of abstracts and axioms of inductive definitions stated below.

Axioms of EON

(EON1) k combinator:  kxy = x.
(EON2) s combinator:  sxyz ≃ xz(yz) & sxy↓.
(EON3)  k ≠ s.
(EON4) Pairing:  pxy↓ & p_{0}(pxy) = x & p_{1}(pxy) = y.

(EON5), (EON6) Natural numbers:

N(0) & ∀x(N(x) → [N(s_{N}(x)) & p_{N}(s_{N}x) = x & s_{N}x ≠ 0]),
∀x(N(x) & x ≠ 0 → N(p_{N}x) & s_{N}(p_{N}x) = x).

(EON7), (EON8) Definition by integer cases:

N(a) & N(b) & a = b → d(a, b, x, y) = x,
N(a) & N(b) & a ≠ b → d(a, b, x, y) = y.

(EON9) Induction for all formulae:

ϕ(0) & ∀x(N(x) & ϕ(x) → ϕ(s_{N}x)) → ∀x(N(x) → ϕ(x)).

Axioms of abstracts

(A1)  ((x̄).A)(t̄) ↔ t̄↓ & A[t̄/x̄].

Axioms of inductive definitions

Let μP.(x̄).A[P] and C be predicates of the same arity. Let B ≡ μP.(x̄).A[P]. Then the following R1, R2 are axioms:

(R1)  A[B] → B(x̄),
(R2)  ∀x̄(A[C] → C(x̄)) → ∀x̄(B(x̄) → C(x̄)).

The consistency of the theory can be proved in the same way as [10].

2.11 Lemma

Let B ≡ μP.(x̄).A[P], then we have ∀x̄(B(x̄) ↔ A[B]).

This lemma is proved in [10].

2.12 Bracket abstraction

A combinatory term \overline{t} is defined for a λ-term t in the following way.

1. \overline{x} ≡ x if x is a variable,

2. \overline{c} ≡ c if c is a constant,

3. \overline{s t} ≡ \overline{s} \overline{t},

4. \overline{λx.x} ≡ skk,

5. \overline{λx.y} ≡ ky if y is a variable and x ≢ y,

6. \overline{λx.c} ≡ kc if c is a constant,

7. \overline{λx.st} ≡ s(\overline{λx.s})(\overline{λx.t}).

In the sequel, a term t always denotes a combinatory term \overline{t} except that a substituted term u[t/x] denotes a combinatory term \overline{u}[\overline{t}/x] for terms t,u and a variable x.

Then

λx.t↓,
(λx.t)x ≃ t

hold for a variable x and a term t.

2.13 The Recursion Theorem

Let u_{n} ≡ λyx_{1} ⋯ x_{n}.f(yy)x_{1} ⋯ x_{n} and R_{n} ≡ λf.u_{n}u_{n}. Then we have

∀f∀x_{1},…, x_{n}(R_{n}fx_{1} ⋯ x_{n−1}↓ & R_{n}fx_{1} ⋯ x_{n} ≃ f(R_{n}f)x_{1} ⋯ x_{n}).

Suppose f is a variable and t[f] is a term possibly containing f. We write μ_{n}f.t[f] for R_{n}(λf.t[f]). Then we have

g = μ_{n}f.t[f] → ∀x_{1},…, x_{n}(gx_{1} ⋯ x_{n−1}↓ & gx_{1} ⋯ x_{n} ≃ t[g]x_{1} ⋯ x_{n}).

Sometimes we omit the subscript n of μ_{n}f.t.

3 Realizability Interpretation

3.1 Definition (Extended q-realizability Interpretation)

For an E-formula A, a fresh variable e, predicate variables P̄ ≡ P_{1},…, P_{n}, predicates F̄ ≡ F_{1},…, F_{n} and Ḡ ≡ G_{1},…, G_{n} such that arity(F_{i}) = arity(P_{i}) and arity(G_{i}) = arity(P_{i}) + 1, we define an E-formula

e qP̄[F̄; Ḡ] A

by induction on the construction of A. If n = 0, we write e q A for it. We abbreviate

qP̄[F̄; Ḡ]

as q′ and

q_{P̄,Q}[F̄, H; Ḡ, J]

as q′_{Q}[H; J]. Generally, if q′ is an abbreviation of qP̄[F̄; Ḡ], then q′Q̄[H̄; J̄] is an abbreviation of q_{P̄,Q̄}[F̄, H̄; Ḡ, J̄]. In the following, we write AP̄[F̄] for the result of simultaneous substitution of F̄ for P̄ in A. The definition is as follows.

1. e q′ P_{i}(t̄) ≡ G_{i}(e, t̄).

2. e q′ A ≡ e = 0 & A if A is an atomic E-formula which is not of the form P_{i}(t̄).

3. e q′ A & B ≡ (p_{0}e q′ A) & (p_{1}e q′ B).

4. e q′ A ∨ B ≡ N(p_{0}e) & (p_{0}e = 0 → AP̄[F̄] & (p_{1}e q′ A)) & (p_{0}e ≠ 0 → BP̄[F̄] & (p_{1}e q′ B)).

5. e q′ A → B ≡ e↓ & ∀q(AP̄[F̄] & (q q′ A) → (eq q′ B)).

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

7. e q′ ∃xA(x) ≡ p_{0}e↓ & A(p_{0}e)P̄[F̄] & (p_{1}e q′ A(p_{0}e)).

8. e q′ ((x̄).A)(t̄) ≡ ((r, x̄).(r q′ A))(e, t̄).

9. e q′ (μQ.(x̄).A[Q])(t̄) ≡ (μQ^{∗}.(e, x̄).(e q′_{Q}[BP̄[F̄]; Q^{∗}] A[Q]))(e, t̄), where B is μQ.(x̄).A[Q] and Q^{∗} is a fresh predicate variable whose arity is arity(Q) + 1.

It is easy to see that the above definition is well-defined. The point is that if Q is positive (negative) in A[Q], then Q^{∗} is positive (negative, resp.) in e q′_{Q}[B, Q^{∗}] A[P].

3.2 Remark

The notation (e q_{P_{1}...P_{n}}[F_{1},…, F_{n}; G_{1},…, G_{n}] A) used in this paper differs slightly from the notation used in [10]. The expression (e q_{P_{1}...P_{n}}[F_{1}, G_{1},…, F_{1}, G_{n}] A) used in [10] denotes the same formula as the expression (e q_{P_{1}...P_{n}}[F_{1},…, F_{n}; G_{1},…, G_{n}] A) used in this paper.

3.3 Lemma

(i) (Substitution Property)

(e qP̄[F̄; Ḡ] A)[y/x]
≡ e[y/x] qP̄[F̄[y/x]; Ḡ[y/x]] A[y/x].

Here F̄[y/x] is F_{1}[y/x],…, F_{n}[y/x]. (ii) Suppose A is an E-formula and FPV (A) ⊆ { P̄ }. Then the free predicate variables of

e qP̄[F̄; Ḡ] A are among those of F̄, Ḡ. (iii) If A is a formula, then e q A is also a formula. (iv) (e qP̄[F̄; Ḡ] A) → e↓.

These claims are proved in [10].

4 Soundness Theorem

Now we shall show the soundness of our q-realizability interpretation. The soundness for the axioms and rules of EON is proved in the same way as [1]. We prove that the axioms A1, R1 and R2 are realizable.

4.1 Lemma

⟨λr.⟨0, r⟩, λr.p_{1}r⟩ realizes the axiom (A1).

This lemma is proved immediately by the definition of realizability. The following three lemmas are proved in [10].

4.2 Lemma

Suppose ∀x̄(H_{1}(x̄) → H_{2}(x̄)). Then,

1. if P is positive in A[R̄, P], we have

(e q_{R̄,P} [F̄, H_{1}; Ḡ, J] A[R̄, P])
→ (e q_{R̄,P} [F̄, H_{2}; Ḡ, J] A[R̄, P]),

2. if P is negative in A[R̄, P], we have

(e q_{R̄,P} [F̄, H_{2}; Ḡ, J] A[R̄, P])
→ (e q_{R̄,P} [F̄, H_{1}; Ḡ, J] A[R̄, P]).

4.3 Lemma

We have

e q′_{P} [B; (e, x̄).e q′ B(x̄)] A[R̄, P]
≡ e q′ A[R̄, B],

where q′ is an abbreviation of qR̄[F̄; Ḡ].

4.4 Lemma

Let B ≡ μP.(x̄).A[P]. Then,

(e qR̄[F̄; Ḡ] B(x̄)) ↔ (e qR̄[F̄; Ḡ] A[B])

holds.

4.5 Corollary

λx.x realizes the axiom R1.

4.6 Definition

For an E-formula A, a predicate variable P and a term f, we shall define a term σ_{A}^{P,f} as follows: 1. If A ≡ P (t̄), then σ_{A}^{P,f} ≡ λr.ft̄r.

2. If A is an atomic E-formula which is not of the form P (t̄), then σ_{A}^{P,f} ≡ λr.r.

3. If A ≡ A_{1} & A_{2}, then σ_{A}^{P,f} ≡ λr.⟨σ_{A_{1}}^{P,f}(p_{0}r), σ_{A_{2}}^{P,f}(p_{1}r)⟩.

4. If A ≡ A_{1} ∨ A_{2}, then σ_{A}^{P,f} ≡ λr.⟨p_{0}r, d(p_{0}r)0σ_{A_{1}}^{P,f}σ_{A_{2}}^{P,f}(p_{1}r)⟩.

5. If A ≡ A_{1} → A_{2}, then σ_{A}^{P,f} ≡ λrq.σ_{A_{2}}^{P,f}(r(σ_{A_{1}}^{P,f}q)).

6. If A ≡ ∀xA_{1}(x), then σ_{A}^{P,f} ≡ λrx.σ_{A_{1}(x)}^{P,f}(rx).

7. If A ≡ ∃xA_{1}(x), then σ_{A}^{P,f} ≡ λr.⟨p_{0}r, σ_{A_{1}(p_{0}r)}^{P,f}(p_{1}r)⟩.

8. If A ≡ ((x̄).A_{1})(t̄), then σ_{A}^{P,f} ≡ λr.r.

9. If A ≡ (μQ.(ȳ).A_{1}[P, Q])(t̄), then σ_{A}^{P,f} ≡ gt̄, where g is defined as g ≡ μ_{m+1}g.λȳr.σ_{A_{1}}^{Q,g}(σ_{A_{1}}^{P,f}r) and m is the length of ȳ.

Suppose that a subformula r q P (t̄) occurs in a formula e q A. Then we use a term σ_{A}^{P,f} to replace the term r by the term ft̄r in a realizer e. A term σ_{A}^{P,f}e means a term obtained from e by replacing all such r by ft̄r.

Note that the following (i)–(iii) hold:

(i) FV(σ_{A}^{P,f}) ⊆ FV(A) ∪ { f },

(ii) σ_{A[P]}^{P,f} ≡ σ_{A[P′]}^{P′,f} and σ_{A[P,Q]}^{P,f} ≡ σ_{A[P,Q′]}^{P,f} for predicate variables Q and Q′,

(iii) σ_{A}^{P,f}↓.

4.7 Key Lemma

Let A[R̄, P] be an E-formula with FPV (A) ⊆ { R̄, P }. Let P′ be a predicate variable with arity(P′) = arity(P) and F̄, Ḡ, H, J, J′ be predicates with arity(F_{i}) = arity(R_{i}), arity(G_{i}) = arity(R_{i})+1 (for all i), arity(H) = arity(P), arity(J) = arity(J′) = arity(P)+1. We abbreviate

q_{R̄,P,P′}[F̄, H, H; Ḡ, J, J′]

as q′. Then,

(I) if P is positive in A[R̄, P], we have

λf.σ_{A}^{P,f} q′ (∀x̄(P (x̄) → P′(x̄)) → (A[R̄, P] → A[R̄, P′])),

and

(II) if P is negative in A[R̄, P], we have

λf.σ_{A}^{P,f} q′ (∀x̄(P (x̄) → P′(x̄)) → (A[R̄, P′] → A[R̄, P])).

Proof

We prove the following (I′) and (II′):

(I′) If P is positive in A, we have

∀f(∀x̄∀r(H(x̄) & J(r, x̄) → J′(fx̄r, x̄))
→∀r(A[F̄, H] & (r q′ A[R̄, P]) → σ_{A}^{P,f}r q′ A[R̄, P′]))

(II′) If P is negative in A, we have

∀f(∀x̄∀r(H(x̄) & J(r, x̄) → J′(fx̄r, x̄))
→∀r(A[F̄, H] & (r q′ A[R̄, P′]) → σ_{A}^{P,f}r q′ A[R̄, P])).

Then, (I) and (II) holds. We prove (I′) and (II′) simultaneously by induction on the complexity of A.

Case 1. Assume A[R̄, P] ≡ P (t̄). We must show

∀f(∀x̄∀r(H(x̄) & J(r, x̄) → J′(fx̄r, x̄))
→∀r(H(t̄) & J(r, t̄) → J′(σ_{A}^{P,f}r, t̄))).

But this is trivial, for σ_{A}^{P,f}r ≃ ft̄r.

Case 2. Assume A[R̄, P] is an atomic E-formula which is not of the form P (t̄). This case is also trivial, since P does not occur in A.

Case 3. Assume A ≡ A_{1} & A_{2}. This case is easy and left to the reader.

Case 4. Assume A ≡ A_{1} ∨ A_{2}. This case is also easy.

Case 5. Assume A ≡ A_{1}[R̄, P] → A_{2}[R̄, P].

Subcase (i): Assume P is positive in A. Then P is negative in A_{1} and positive in A_{2}. Suppose ∀x̄∀r(H(x̄) & J(r, x̄) → J′(fx̄r, x̄)). By the induction hypothesis,

∀r(A_{1}[F̄, H] & (r q′ A_{1}[R̄, P′]) → σ_{A_{1}}^{P,f}r q′ A_{1}[R̄, P]),  (1)
∀r(A_{2}[F̄, H] & (r q′ A_{2}[R̄, P]) → σ_{A_{2}}^{P,f}r q′ A_{2}[R̄, P′]).  (2)

Suppose

A_{1}[F̄, H] → A_{2}[F̄, H]  (3)

and

r q′ (A_{1}[R̄, P] → A_{2}[R̄, P]).  (4)

We must show that

σ_{A}^{P,f}r q′ (A_{1}[R̄, P′] → A_{2}[R̄, P′]),

that is,

∀q(A_{1}[F̄, H] & (q q′ A_{1}[R̄, P′]) → σ_{A}^{P,f}rq q′ A_{2}[R̄, P′]).  (5)

Suppose

A_{1}[F̄, H]  (6)

and

q q′ A_{1}[R̄, P′].  (7)

By (1),

σ_{A_{1}}^{P,f}q q′ A_{1}[R̄, P].  (8)

Since (4) means

∀u(A_{1}[F̄, H] & (u q′ A_{1}[R̄, P])
→ru q′ A_{2}[R̄, P]),

we have, from (6) and (8),

r(σ_{A_{1}}^{P,f}q) q′ A_{2}[R̄, P].  (9)

From (3) and (6), we get

A_{2}[F̄, H].  (10)

By (2), (9) and (10), we have

σ_{A_{2}}^{P,f}(r(σ_{A_{1}}^{P,f}q)) q′ A_{2}[R̄, P′].

But σ_{A}^{P,f}rq ≃ σ_{A_{2}}^{P,f}(r(σ_{A_{1}}^{P,f}q)). Hence we have got (5).

Subcase (ii): The case that P is negative in A. This subcase is proved similarly to Subcase (i). Case 6. Assume A ≡ ∀yA_{1}(y). This case is easy. Case 7. Assume A ≡ ∃yA_{1}(y). This case is also easy. Case 8. Assume A ≡ ((x̄).A_{1})(t̄). This case is also easy. Case 9. Assume A ≡ A[R̄, P] ≡ (μQ.(ȳ).A_{1}[R̄, P, Q])(t̄). Subcase (i): Assume P is positive in A. Let

K[R̄, P] ≡ μQ.(ȳ).A_{1}[R̄, P, Q].

Then, we have

A[R̄, P] ≡ K[R̄, P](t̄)

and

K[F̄, H](ȳ) ↔ A_{1}[F̄, H, K[F̄, H]].  (11)

Let

g ≡ μ_{m+1}g.λȳr.σ_{A_{1}}^{Q,g}(σ_{A_{1}}^{P,f}r),

where m is the length of ȳ. Recall that σ_{A}^{P,f} = gt̄. Suppose

∀x̄∀r(H(x̄) & J(r, x̄) → J′(fx̄r, x̄)).

We must show

∀r(K[F̄, H](t̄) & (r q′ K[R̄, P](t̄)) → gt̄r q′ K[R̄, P′](t̄)).

More generally, we prove

∀r∀ȳ(K[F̄, H](ȳ) & (r q′ K[R̄, P](ȳ)) → gȳr q′ K[R̄, P′](ȳ)).

This formula is equivalent to

∀r∀ȳ((μQ^{∗}.(r, ȳ).(r q′_{Q}[K[F̄, H]; Q^{∗}] A_{1}[R̄, P, Q]))(r, ȳ)
→(K[F̄, H](ȳ) → L(gȳr, ȳ))),  (12)

where

L ≡ μQ^{∗}.(r, ȳ).(r q′_{Q}[K[F̄, H]; Q^{∗}] A_{1}[R̄, P′, Q]).

To prove this formula using induction axiom R2, we let

M ≡ (r, ȳ).(K[F̄, H](ȳ) → L(gȳr, ȳ))

and prove

∀r∀ȳ((r q′_{Q}[K[F̄, H]; M] A_{1}[R̄, P, Q]) → M(r, ȳ))  (13)

Now we assume

r q′_{Q}[K[F̄, H]; M] A_{1}[R̄, P, Q],  (14)
K[F̄, H](ȳ),  (15)

and prove

L(gȳr, ȳ).

By (11), we have

A_{1}[F̄, H, K[F̄, H]].  (16)

By the induction hypothesis,

A_{1}[F̄, H, K[F̄, H]] & (r q′_{Q}[K[F̄, H]; M] A_{1}[R̄, P, Q])

→σ_{A_{1}}^{P,f}r q′_{Q}[K[F̄, H]; M] A_{1}[R̄, P′, Q].

Hence by (14) and (16),

σ_{A_{1}}^{P,f}r q′_{Q}[K[F̄, H]; M] A_{1}[R̄, P′, Q].

Let

q′′ ≡ q′_{Q,Q′}[K[F̄, H], K[F̄, H]; M, L].

Since Q′ is not free in A_{1}[R̄, P′, Q], we have

σ_{A_{1}}^{P,f}r q′′ A_{1}[R̄, P′, Q].  (17)

By the induction hypothesis,

∀h(∀ȳ∀r(K[F̄, H](ȳ) & M(r, ȳ) → L(hȳr, ȳ)) →∀u(A_{1}[F̄, H, K[F̄, H]] & (u q′′ A_{1}[R̄, P′, Q])

→σ_{A_{1}}^{Q,h}u q′′ A_{1}[R̄, P′, Q′])).

Since ∀ȳ∀r(K[F̄, H](ȳ) & M(r, ȳ) → L(gȳr, ȳ)) holds, we have

∀u(A_{1}[F̄, H, K[F̄, H]] & (u q′′ A_{1}[R̄, P′, Q]) → σ_{A_{1}}^{Q,g}u q′′ A_{1}[R̄, P′, Q′]).

Hence by (16) and (17),

σ_{A_{1}}^{Q,g}(σ_{A_{1}}^{P,f}r) q′′ A_{1}[R̄, P′, Q′].

Since Q is not free in A_{1}[R̄, P′, Q′],

σ_{A_{1}}^{Q,g}(σ_{A_{1}}^{P,f}r) q′_{Q′}[K[F̄, H]; L] A_{1}[R̄, P′, Q′].

Renaming Q′ to Q,

σ_{A_{1}}^{Q,g}(σ_{A_{1}}^{P,f}r) q′_{Q}[K[F̄, H]; L] A_{1}[R̄, P′, Q].

By the definition of g, we have gȳr ≃ σ_{A_{1}}^{Q,g}(σ_{A_{1}}^{P,f}r). Therefore,

gȳr q′_{Q}[K[F̄, H]; L] A_{1}[R̄, P′, Q].

By the axiom R1,

(gȳr q′_{Q}[K[F̄, H]; L] A_{1}[R̄, P′, Q]) → L(gȳr, ȳ).

Hence L(gȳr, ȳ). Thus we have derived (13).

Case (ii): The case that P is negative in A_{1}. This subcase is proved similarly to Subcase (i). This completes the proof. □

4.8 Corollary

(i) If P is positive in A[R̄, P], we have

∀f(∀x̄(H(x̄) → H′(x̄))
&∀x̄∀r(H(x̄) & J(r, x̄) → J′(fx̄r, x̄))
→∀r(A[F̄, H] & (r q′′ A[R̄, P]) → σ_{A}^{P,f}r q′′ A[R̄, P′])),

where q′′ is q_{R̄,P,P′}[F̄, H, H′; Ḡ, J, J′]. That is,

λf.σ_{A}^{P,f} q′′ (∀x̄.(P (x̄) → P′(x̄)) → (A[R̄, P] → A[R̄, P′])).

(ii) Let

D ≡ (r, x̄).(B(x̄) → fx̄r q C(x̄)).

If P is positive in A[P], we have

∀x̄(B(x̄) → C(x̄))
→∀r(A[B] & (r q_{P} [B; D] A[P]) → σ_{A}^{P,f}r q A[C]).

Proof

(i) Suppose ∀x̄(H(x̄) → H′(x̄)). By the above lemma,

∀f(∀x̄∀r(H(x̄) & J(r, x̄) → J′(fx̄r, x̄))

→∀r(A[F̄, H] & (r q′ A[R̄, P]) → σ_{A}^{P,f}r q′ A[R̄, P′])),

where q′ is q_{R̄,P,P′}[F̄, H, H; Ḡ, J, J′]. Since P′ does not occur in A[R̄, P],

(r q′ A[R̄, P]) ↔ (r q′′ A[R̄, P]).

Moreover, by Lemma 4.2,

(σ_{A}^{P,f}r q′ A[R̄, P′]) → σ_{A}^{P,f}r q′′ A[R̄, P′].

Hence (i) holds.

(ii) Suppose ∀x̄(B(x̄) → C(x̄)). Let

q′′ ≡ q_{P,P′}[B, C; D, (r, x̄).(r q C(x̄))].

By (i),

∀h(∀x̄∀r(B(x̄) & D(r, x̄) → hx̄r q C(x̄))
→∀r(A[B] & (r q′′ A[P]) → σ_{A}^{P,h}r q′′ A[P′]))

Since ∀x̄∀r(B(x̄) & D(r, x̄) → fx̄r q C(x̄)) holds, we have

∀r(A[B] & (r q′′ A[P]) → σ_{A}^{P,f}r q′′ A[P′]).

Since P′ is not free in A[P] and P is not free in A[P′],

∀r(A[B] & (r q_{P} [B; D] A[P]) → σ_{A}^{P,f}r q_{P′}[C; (r, x̄).(r q C(x̄))] A[P′]).

By Lemma 4.3,

∀r(A[B] & (r q_{P} [B; D] A[P]) → σ_{A}^{P,f}r q A[C]).

□ Now let us construct a realizer of the induction axiom R2.

4.9 Theorem

Let B ≡ μP.(x̄).A[P]. Then

λq.μf.λx̄r.qx̄(σ_{A}^{P,f}r) q (∀x̄(A[C] → C(x̄)) → ∀x̄(B(x̄) → C(x̄)))

holds.

Proof Suppose

∀x̄(A[C] → C(x̄))  (18)

and

q q ∀x̄(A[C] → C(x̄)).  (19)

Let f ≡ μf.λx̄r.qx̄(σ_{A}^{P,f}r). We show that

∀r, x̄(B(x̄) & (r q B(x̄)) → fx̄r q C(x̄)) & ∀x̄(fx̄↓).  (20)

∀x̄(fx̄↓) is trivial. The remaining part is equivalent to

∀r, x̄((μP^{∗}.(r, x̄).(r q_{P} [B; P^{∗}] A[P]))(r, x̄)

→(B(x̄) → fx̄r q C(x̄))).

So, by R2, it is sufficient to prove that

(r q_{P} [B; D] A[P]) → D(r, x̄)  (21)

where D ≡ (r, x̄).(B(x̄) → fx̄r q C(x̄)). Suppose

(r q_{P} [B; D] A[P]) & B(x̄).

Then, since B(x̄) ↔ A[B], we get A[B]. From (18) and R2, we have

∀x̄(B(x̄) → C(x̄)).  (22)

By Corollary 4.8 (ii), we have σ_{A}^{P,f}r q A[C]. Since P is positive in A[P], (22) implies A[B] → A[C]. So we have A[C]. Then, by (19), qx̄(σ_{A}^{P,f}r) q C(x̄). By the definition of f, fx̄r ≃ qx̄(σ_{A}^{P,f}r) holds. Therefore we get fx̄r q C(x̄). Thus we have (21). Then the theorem holds. □

4.10 Theorem (soundness of realizability)

If EON + μ ⊢ A holds, then we can get a term e effectively from the proof and EON + μ ⊢ e q A holds.

Proof

The soundness for the axioms and rules of EON is proved in [1].

The axiom A1 is realized by Lemma 4.1. The axiom R1 is realized by Corollary 4.5. The axiom R2 is realized by Theorem 4.9. □

This theorem improves the result of [10]. In [10], the system can only use μP.x̄.A[P] under the following conditions: each occurrence of a predicate variable P in an E-formula A[P] must be (1) positive and (2) either strictly positive in A[P] or in some Harrop subformula of A[P]. On the other hand, in our system the condition (2) can be omitted and our system can use μP.x̄.A[P] under the condition (1). In particular, our system covers non-strictly positive inductive definitions, which the system in [10] cannot cover.

4.11 Corollary

(1) The term existence property holds for EON + μ. That is, if EON + μ ⊢ ∃xA(x) holds, we can get a term t effectively from the proof and EON + μ ⊢ A(t) holds.

(2) The disjunction property holds for EON + μ. That is, if EON + μ ⊢ A ∨ B holds, then EON + μ ⊢ A holds or EON + μ ⊢ B holds.

These claims are proved easily by using the soundness theorem.

4.12 Theorem (program extraction)

Suppose that EON + μ ⊢ A(x) → (jx q A(x)). If EON + μ ⊢ ∀x(A(x) → ∃yB(x, y)) holds, we can get a term f effectively from the proof and EON + μ ⊢ ∀x(A(x) → fx↓ & B(x, fx)) holds.

Proof

By the soundness theorem and EON + μ ⊢ ∀x(A(x) → ∃yB(x, y)), we can get a term e from the proof and EON + μ ⊢ (e q ∀x(A(x) → ∃yB(x, y))) holds. Put f ≡ p_{0}(ex(jx)). Then the claim holds. □

By the program extraction theorem, we can extract a program f from the constructive proof of the formula ∀x(A(x) → ∃yB(x, y)) in EON + μ.

Recently some meaningful examples of programs which uses non-strictly positive inductive definitions. Martin Hoffmann found an example of breadth first search of trees, which uses continuations. The type of continuations is given by a non-strictly positive datatype cont, which is defined by cont = D|C of ((cont → α) → α). In our system, the predicate C(x) which states that x is a continuation can be described as follows:

C ≡ μP.λx.x = D ∨ ∃y(x = C(y) & ∀f(∀z(P (z) → A(f(z))) → A(y(f))))

for some predicate A(x).

When A(x) is not Harrop, the above inductive definition cannot be used in the system of [10], but our system can use the above inductive definition.

5 Concluding Remarks

In this paper, we treated Kleene-style q-realizability. The results of this paper can be applied to Grayson-style q-realizability by small modification. The proof of the soundness theorem for Grayson-style realizability will be simpler than our proof for Kleene-style realizability.

The results of this paper can be also applied to usual r-realizability by small modification. The soundness theorem for r-realizability will give fundamental tools to prove choice principles, consistency and conservative extension results in the area of mathematical logic.

References

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

[2] M. Beeson, Proving programs and programming proofs, in: R. Barcan Marcus, G.J.W. Dorn and P. Weingarter, eds., Logic, Methodology, and Philosophy of Science VII (North-Holland, Amsterdam, 1985) 51–82.

[3] W. Buchholz, S. Feferman, W. Pohlers and W. Sieg, Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, Lecture Notes in Math. 897 (Springer, Berlin, 1981).

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

[5] S. Feferman, A language and axioms for explicit mathematics, Lecture Notes in Math. 450 (Springer, Berlin, 1975) 87–139.

[6] S. Feferman, Constructive theories of functions and classes, in: M. Boffa, D. van Dalen and K. McAloon, eds., Logic Colloquium ’78, Proceedings of the Logic Colloquium at Mons (North-Holland, Amsterdam, 1979) 159–224.

[7] S. Hayashi and H. Nakano, PX: A Computational Logic (MIT Press, Cambridge, 1988).

[8] P. Martin-Löf, Constructive mathematics and computer programming, in: L. J. Cohen et al, eds., Logic, Methodology, and Philosophy of Science VI (North-Holland, 1982) 153–179.

[9] B. Nordström, K. Petersson and J.M. Smith, Programming in Martin-Löf’s Type Theory (Oxford University Press, Oxford, 1990).

[10] M. Tatsuta, Program Synthesis Using Realizability, Theoretical Computer Science 90 (1991) 309–353.

[11] A.S. Troelstra and D. van Dalen, Constructivism in Mathematics, Volume I, II (North-Holland, 1988).