0 Introduction

Program synthesis by deductive approach has been studied widely [10, 9, 5, 14]. By this method of program synthesis, firstly a program specification of a target program written in the form of logical formulae is given. Secondly we produce the target program from the program specification using theorem proving techniques.

We adopt a deductive approach for program synthesis in this paper. We consider only an input condition and an input output relation as program specification. Program specification is supposed to be given in the form of logical formulae ∀xA(x) → ∃yB(x, y). Logical formulae can express specification naturally and powerfully. They can be manipulated smoothly in logic systems so theoretical treatment of specification is easier in this form.

Intuitionistic logic is the logic on which formal systems based formalize constructive mathematics. Constructive mathematics is the mathematics based on the philosophy requiring the following two principles [3]:

1. “there exists an x” means we can find x explicitly.

2. “truth” has no a priori meaning; a proposition is true just in case we can find a proof of it.

Constructive mathematics has many schools. Therefore there are various kinds of intuitionistic logic. Roughly speaking, intuitionistic logic can be considered as the usual logic without the law of excluded middle. Intuitionistic logic has been discussed in the view of philosophical interest.

Intuitionistic logic can be used as the foundation of computer science. In formal systems based on intuitionistic logic, “there exists an x” means “we can compute x”. Therefore we can compute values with proofs of the existence of values in intuitionistic logic. “Proof as program” represents the principle that constructive proofs are viewed as computer programs. This principle holds in intuitionistic logic. Formal systems based on intuitionistic logic which formalize computer programs are now studied intensively [12, 13].

Realizability interpretation is one of the ways to extract programs from constructive proofs. This interpretation associates a formula A with a formula e q A. It is proved that if ⊢ A then we can get some term e from a proof of A and ⊢ e q A holds. By this fact, we can make a program e from a constructive proof of an appropriate formula A. For example, to extract Lisp programs from constructive proofs is studied [9].

In this paper, programs are synthesized in the following way:

1. A program specification describing an input condition and an input output relation is given in a logical formula.

2. This formula is proved in a formal system based on intuitionistic logic.

3. A program is extracted from this constructive proof by realizability interpretation.

We have developed a formal system EON + μ which is a basis of this method of program synthesis.

EON + μ is an extension of Beeson’s EON[3, 6]. EON is based on intuitionistic logic and combinatory logic. Programs are represented by combinators and computation is represented by term reduction [1]. EON has partial terms representing computations which do not terminate.

EON + μ is constructed by adding the facility of recursive definition of predicates to EON. Recursive definition of predicates enables recursive description of program specification. We can use recursively defined concepts in specification freely. This facility can define predicates representing recursive data structures. Moreover, induction schemata for these recursive data structures are induced from the axioms of EON + μ according to the definition of data structures.

In PX [9], the facility of recursive definition of predicates is called conditional inductive generation and can be used under the syntactical condition that recursive calls of the original predicate occur only in Harrop formulae. The double negation technique helps to treat predicates not satisfying this condition by this restricted class of predicates satisfying this condition.

In this paper, we can use a less restricted class of recursively defined predicates. We admit not only a predicate whose recursive calls occur in Harrop subformulae but a predicate whose recursive calls occur at strictly positive positions. This class includes the class of inductive definition with Horn clauses used in Prolog, because of our weaker restriction of strictly positive occurrences of recursive calls.

We give the extended q-realizability interpretation of EON + μ in EON + μ to treat recursive definition of predicates. A recursively defined predicate is interpreted as another recursively defined predicate naturally corresponding to the original predicate by this q-realizability interpretation. We prove the soundness of the interpretation. We utilize the restricting condition of Harrop subformulae and strictly positive occurrences to prove the interpretation of general induction schemata of recursively defined predicates. The realizers corresponding to the general induction schemata of recursively defined predicates express the general recursive function schemata.

We give the method of program synthesis using the q-realizability interpretation in the usual way. We show complete examples of producing small sample programs by this method.

Section 1 presents the theory EON + μ. Computational meanings of this formal system are discussed. In section 2, recursively defined predicates of EON + μ are discussed. Some examples of program specification and definition of recursive data structures are given. Section 3 gives models of this theory and proves consistency of this theory. Section 4 defines q-realizability interpretation in EON + μ. Soundness theorem of this interpretation is proved. Program synthesis by q-realizability is discussed in section 5.

1 EON + μ

In this section, the formal system EON + μ is presented.

The theory EON was proposed by Beeson [3]. EON includes intuitionistic logic and combinatory logic which can formalize computation. Combinatory terms represent programs and term reduction represents execution of programs. The theory EON + μ is an extension of EON and is constructed by adding the facility of recursive definition of predicates to EON.

1.1 Language

The language of EON + μ is an extension of a first order language which includes recursively defined predicates. We have the following 9 constants:

K, S, p, p_{0}, p_{1}, 0, s_{N}, p_{N}, E. We have the following 1 binary function symbol:

App. The terms are defined as usual in a first order language.

Notation 1.1.1.

We abbreviate App(s, t) as st for terms s, t.

There are auxiliary “new predicate symbols” and the following 4 predicate symbols:

⊥, ↓, N, = . We use x,y,z,… for variables, s,t,… for terms, x, y, z, … for sequences of variables and

s, t, … for sequences of terms. Formulae of EON + μ are defined by E-formulae of EON + μ. E-formulae and Harrop E-formulae are defined mutually.

In the next definition, the set S_{++}(A) of the strictly positive occurrences of new predicate symbols plays an important role.

Definition 1.1.2. (E-formula)

E-formulae, Harrop E-formulae and positive, negative and strictly positive occurrences of new predicate symbols of E-formulae are defined simultaneously. For an E-formula or Harrop Eformula A, S_{+}(A), S_{−}(A) and S_{++}(A) represent the set of positive occurrences of new predicate symbols, the set of negative ones and the set of strictly positive ones respectively.

1. E-formula

(1) ⊥ is an E-formula.

S_{+}(⊥) = S_{−}(⊥) = S_{++}(⊥) = ϕ.

(2) t↓ is an E-formula if t is a term.

S_{+}(t↓) = S_{−}(t↓) = S_{++}(t↓) = ϕ.

(3) N(t) is an E-formula if t is a term.

S_{+}(N(t)) = S_{−}(N(t)) = S_{++}(N(t)) = ϕ.

(4) s = t is an E-formula if s, t are terms.

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

(5) P (t) is an E-formula if P is a new predicate symbol with the arity n and t are n terms t_{1}, ..., t_{n}. S_{+}(P (t)) and S_{++}(P (t)) consist of only one occurrence of P (t).

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). S_{++}(A & B) = S_{++}(A) ∪ S_{++}(B).

(7) ∀xA(x) is an E-formula if A(x) is an E-formula. S_{+}(∀xA(x)) = S_{+}(A(x)). S_{−}(∀xA(x)) = S_{−}(A(x)). S_{++}(∀xA(x)) = S_{++}(A(x)).

(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). S_{++}(A → B) = S_{++}(B).

(9) 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). S_{++}(A ∨ B) = S_{++}(A) ∪ S_{++}(B).

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

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

(11) (μP.(x).A)(t) is an E-formula if A is an E-formula and P is a new predicate symbol of which every occurrence is in S_{+}(A) satisfying the next condition (i) or (ii).

(i) The occurrence is in S_{++}(A). (ii) The occurrence is in a subformula of A which is a Harrop E-formula. Namely every occurrence in S_{+}(A) is in S_{++}(A) or in a Harrop E-formula which is a subformula of A.

S_{+}((μP.(x).A)(t)) = S_{+}(A) − \left\{{all occurrences in S_{+}(A) whose predicate sym- \atop bols are P}\right\} .

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

S_{++}((μP.(x).A)(t)) = S_{++}(A) − \left\{{all occurrences in S_{+}(A) whose predicate sym- \atop bols are P}\right\} .

2. Harrop E-formula S_{+} and S_{−} are defined for a Harrop E-formula in the same way as for an E-formula and we do not present them here.

(1) ⊥ is a Harrop E-formula.

(2) t↓ is a Harrop E-formula if t is a term.

(3) N(t) is a Harrop E-formula if t is a term.

(4) s = t is a Harrop E-formula if s, t are terms.

(5) A & B is a Harrop E-formula if A and B are Harrop E-formulae.

(6) ∀xA(x) is a Harrop E-formula if A(x) is a Harrop E-formula.

(7) A → B is a Harrop E-formula if A is an E-formula and B is a Harrop E-formula.

(8) (μP.(x).A)(t) is a Harrop E-formula if A is a Harrop E-formula and P is a new

predicate symbol of which no occurrences are in S_{−}(A). An occurrence of a new predicate symbol P in an E-formula A is called free if this occurrence

is in S_{+}(A) ∪ S_{−}(A). Otherwise an occurrence of P is called bound. Definition 1.1.3. (Formula)

A formula of EON + μ is an E-formula which has no free occurrences of new predicate symbols.

A Harrop formula of EON + μ is a formula which is also a Harrop E-formula.

Definition 1.1.4. (Abstracted Formula)

An abstracted formula is defined in the following way.

1. A new predicate symbol P with the arity n is an abstracted formula with the arity n.

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

3. (x).A is an abstracted formula with the arity n if A is an E-formula and the length of x is n.

Remark 1.1.5.

In general, we use A(x) to denote free variable occurrences x in A explicitly. In the case of B(x) for an abstracted formula B, we use (x) to denote syntactical objects. For example, P (x) denotes the concatenetion of the symbol P and the string (x).

Notation 1.1.6. (Substitution)

Suppose x is a variable and t is a term.

For an E-formula A, an abstracted formula B and a term u, A[t/x], B[t/x], u[t/x] represents A, B and u respectively where every free occurrence of x is replaced with t and bound variables are renamed to avoid collision of names of variables.

Notation 1.1.7.

For an abstracted formula (x).A, we denote a substituted E-formula A[t/x] by ((x).A)(t).

Proposition 1.1.8.

If A is an abstracted formula with the arity n and t are n terms t_{1},…, t_{n} then A(t) is an E-formula.

Notation 1.1.9.

We use an E-formula A[P] instead of a simple A to denote a free new predicate symbol P of A explicitly. If A[P] is an E-formula, P is a new predicate symbol with the arity n and C is an abstracted formula with the arity n, A[C] represents A[P] where C is substituted for every free occurrence of P in A.

If A is an E-formula, P_{1},…, P_{n} are new predicate symbols, F_{1},…, F_{n} are abstracted formulae and the arity of P_{i} is the same as the arity of F_{i} for 1 ≤ i ≤ n, A_{P_{1},...,P_{n}}[F_{1},…, F_{n}] represents A where F_{i} is substituted for every free occurrence of P_{i} in A simultaneously for 1 ≤ i ≤ n.

1.2 Logical Rules and Axioms

The logic of EON + μ is based on intuitionistic logic and logic of partial terms. We use a natural deduction style [15, 17].

1.2.1 Logic of Partial Terms A formula t↓ for a term t represents “computation of t terminates and t has a value”. Some terms have no values. We call a term which may have no value a partial term.

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

Notation 1.2.1.1.

A formula s ≃ t is an abbreviation for (s↓ → s = t) & (t↓ → s = t).

1.2.2 Intuitionistic Logic

\begin{matrix}A & B \\ A & B \end{matrix} (&I)  {A & B \atop A} (&E_{l})  {A & B \atop B} (&E_{r})
{A \atop A ∨ B} (∨I_{l})  {B \atop A ∨ B} (∨I_{r})  \begin{aligned}A ∨ B & [A] ; ⋮ . ; C & [B] ; ⋮ . ; C \\ & C \end{aligned} (∨E)
[A] ; ⋮ . ; B ; A → B (→I)  \begin{aligned}A & A → B \\ & B \end{aligned} (→E)
[a↓] ; ⋮ . ; A(a) ; ∀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)] [a↓] ; ⋮ . ; C \\ C \end{matrix} ; (∃E)
{⊥ \atop A} (⊥E)

In the rules (∀E) and (∃I), t denotes a term. In the rule (∀I), a variable a does not appear in ∀xA(x) nor any open assumptions except a↓ on which A(a) depends. In the rule (∃E), a variable a does not appear in ∃xA(x), C, nor any open assumptions except A(a) and a↓ on which the upper occurrence of C depends. In the rules (∨E), (→I) and (∃E), [A] represents that an open assumption A is discharged.

We call this logical system NJP.

1.3 Non Logical Axioms

In the following axioms, a free variable can be replaced with an arbitrary term while a universally quantified variable can be replaced only with a term t where t↓ is proved.

1.3.1 Equality

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

1.3.2 Combinatory Logic

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

1.3.3 Pairing

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

We use the following abbreviations for pairing and projection functions. Definition 1.3.3.1.

We mean syntactical identity of expressions of a and b by a ≡ b. Notation 1.3.3.2.

For term s, t,

⟨s, t⟩ ≡ pst,
t_{0} ≡ p_{0}t,
t_{1} ≡ p_{1}t.

1.3.4 Number

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)

Notation 1.3.4.1.

For a natural number n, we define a term \overline{n} and call it a numeral.

1. \overline{0} = 0.

2. \overline{n + 1} = s_{N}\overline{n}.

1.3.5 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, t are closed normal terms, s ≢ t) (D4)

The definition of a normal term is given in 1.4.4 below.

1.3.6 Recursively Defined Predicate Suppose that (μP.(x).A[P])(x) and C(x) are formulae and that the length of x is the arity of P. Let B ≡ μP.(x).A[P].

A[B] → B(x)  (R1)

∀x(A[C] → C(x)) → ∀x(B(x) → C(x))  (R2)

We choose these axioms generalizing the iterated inductive definition [11].

1.4 Computation in EON + μ

EON + μ includes λ-calculus. In EON + μ, programs are represented by λ-terms and execution of programs corresponds to term reduction.

Definition 1.4.1.

u ⟶_{Λ−cont} v is defined for terms u, v as,

1. Kst ⟶_{Λ−cont} s,

2. Sstu ⟶_{Λ−cont} su(tu),

3. p_{0}(pst) ⟶_{Λ−cont} s,

4. p_{1}(pst) ⟶_{Λ−cont} t,

5. p_{N}(s_{N}\overline{n}) ⟶_{Λ−cont} \overline{n}.

Definition 1.4.2.

s ⟶_{Λ−red} t if t is s whose subterms u are replaced by v where u ⟶_{Λ−cont} v. t is a Λ-normal term if there is no term s such that t ⟶_{Λ−red} s.

Definition 1.4.3. (Contraction)

u ⟶_{cont} v is defined for terms u, v as,

1. Kst ⟶_{cont} s,

2. Sstu ⟶_{cont} su(tu),

3. p_{0}(pst) ⟶_{cont} s,

4. p_{1}(pst) ⟶_{cont} t,

5. p_{N}(s_{N}\overline{n}) ⟶_{cont} \overline{n},

6. Ennst ⟶_{cont} s if n is a Λ-normal term not including any subterms Eabcd where a, b, c, d are terms,

7. Enmst ⟶_{cont} t if n, m are Λ-normal terms not including any subterms Eabcd where a, b, c, d are terms, and n ≢ m.

Definition 1.4.4. (Reduction, Normal Term)

s ⟶_{red} t if t is s whose subterms u are replaced by v where u ⟶_{cont} v. A binary relation ⟶_{red}^{∗} is a transitive reflexive closure of ⟶_{red}. t is a normal term if there is no term s such that t ⟶_{red} s.

Theorem 1.4.5. (Church-Rosser Theorem)

If t ⟶_{red}^{∗} u and t ⟶_{red}^{∗} v then there exists s such that u ⟶_{red}^{∗} s and v ⟶_{red}^{∗} s.

Proof 1.4.6.

We can prove this theorem modifying the proof of p.108 – p.109 in Troelstra’s book [17] in the following way.

For the definition 2.2.20 in the book, we add the next clauses:

1. p_{0}(pst) ≥^{∗} s,

2. p_{1}(pst) ≥^{∗} t,

3. p_{N}(s_{N}\overline{n}) ≥^{∗} \overline{n},

4. Ennst ≥^{∗} s if n is a Λ-normal term not including any subterms Eabcd where a, b, c, d are terms,

5. Enmst ≥^{∗} t if n, m are Λ-normal terms not including any subterms Eabcd where a, b, c, d are terms, and n ≢ m.

For the proof of the lemma 2.2.21 in the book, we add the next cases:

1. If t ≡ p_{0}(pt_{1}t_{2}), t′ ≡ t_{1}, t′′ ≡ p_{0}(pt′_{1}t′_{2}) and t_{i} ≥^{∗} t′_{i} (1 ≤ i ≤ 2), then let t′′′ ≡ t′_{1}.

2. If t ≡ p_{1}(pt_{1}t_{2}), t′ ≡ t_{2}, t′′ ≡ p_{1}(pt′_{1}t′_{2}) and t_{i} ≥^{∗} t′_{i} (1 ≤ i ≤ 2), then let t′′′ ≡ t′_{2}.

3. If t ≡ Ennt_{1}t_{2}, t′ ≡ t_{1}, t′′ ≡ Ennt′_{1}t′_{2}, t_{i} ≥^{∗} t′_{i} (1 ≤ i ≤ 2), and n is a Λ-normal term not including any subterms Eabcd where a, b, c, d are terms, then let t′′′ ≡ t′_{1}.

4. If t ≡ Enmt_{1}t_{2}, t′ ≡ t_{2}, t′′ ≡ Enmt′_{1}t′_{2} and t_{i} ≥^{∗} t′_{i} (1 ≤ i ≤ 2), n, m are Λ-normal terms not including any subterms Eabcd where a, b, c, d are terms, and n ≢ m, then let t′′′ ≡ t′_{2}.

Definition 1.4.7.

u ⟶_{incont} v is defined in the same way as u ⟶_{cont} v except that the terms s, t, u in the definition are restricted to normal terms. s ⟶_{inred} t and s ⟶_{inred}^{∗} t are defined from u ⟶_{incont} v in the same way that s ⟶_{red} t and s ⟶_{red}^{∗} t are defined from u ⟶_{cont} v.

In EON + μ, a term t represents a program. Term reduction is an operation which gets t from s where s ⟶_{inred} t. Term reduction represents computation of programs. A normal term represents a resulting value of computation.

The order of computing of s ⟶_{inred}^{∗} t is specified by a sequence

s = t_{0} ⟶_{inred} t_{1} ⟶_{inred} t_{2} ⟶_{inred} ⋯ ⟶_{inred} t_{n} = t.

In general, there are many orders of computing of s ⟶_{inred}^{∗} t. The above theorem says that a result of computing is unique for different orders of computing. Theorem 1.4.8.

1. If for a term t, ⊢ t↓, then there is no infinite sequence of ⟶_{inred}^{∗} starting from t:

t = t_{0} ⟶_{inred}^{∗} t_{1} ⟶_{inred}^{∗} t_{2} ⟶_{inred}^{∗} ⋯

2. If for a term t, ⊢ N(t), then ⊢ t = \overline{n} for some n. We do not give a proof of this theorem in this paper. Definition 1.4.9.

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}). Remark 1.4.10.

If clauses 5. and 6. of the above definition are replaced with

\overline{λx.t} ≡ K\overline{t} if \overline{t} does not include x, then claim 1. of the next proposition does not hold. Proposition 1.4.11.

For λ-terms s, t and a variable x, 1. and 2. hold.

1. \overline{λx.t}↓.

2. s↓ → \overline{(λx.t)s} ≃ \overline{t[s/x]}. Notation 1.4.12.

We use a λ-term t to denote an EON + μ term \overline{t}.

A partial term represents a program which may not terminate.

A natural number n is represented by a numeral \overline{n} in EON + μ. Every partial recursive function is represented in EON + μ.

Proposition 1.4.13. (Recursion Theorem)

There is a term R such that Rf↓ & ∀x(Rfx ≃ f(Rf)x).

Proof 1.4.14.

Let R ≡ λf.tt, where t ≡ λyx.f(yy)x.

Notation 1.4.15.

μf.t ≡ R(λf.t).

Theorem 1.4.16.

All partial recursive functions can be represented by terms in EON + μ.

Proof 1.4.17.

We use t_{f} to denote a term representing a partial recursive function f. We use induction on the definition of partial recursive functions.

1. Basic functions A zero constant and a successor function are represented by 0 and s_{N} respectively. A projection function P_{i}^{n}(x_{1},…, x_{n}) = x_{i} is represented by λx_{1} … x_{n}.x_{i}.

2. Substitution Suppose that

g(x_{1},…, x_{m}),

h_{i}(x_{1},…, x_{n}) (1 ≤ i ≤ m)

are partial recursive functions and

f(x_{1},…, x_{n}) = g(h_{1}(x_{1},…, x_{n}),…, h_{m}(x_{1},…, x_{n})). Let

t_{f} ≡ λx_{1} … x_{n}.t_{g}(t_{h_{1}}x_{1} … x_{n}) … (t_{h_{m}}x_{1} … x_{n}).

3. Primitive recursive schema

Suppose that

f(0, x_{1},…, x_{m}) = g(x_{1},…, x_{m}),
f(n + 1, x_{1},…, x_{m}) = h(n, x_{1},…, x_{m}, f(n, x_{1},…, x_{m}))

and that g, h are partial recursive functions. We have terms t_{g}, t_{h} by induction hypothesis. Let

t_{f} ≡ μf.λnx_{1} … x_{m}.
En0t_{g}(λx_{1} … x_{m}.t_{h}(p_{N}n)x_{1} … x_{m}(f(p_{N}n)x_{1} … x_{n}))x_{1} … x_{m}.

4. Minimization Suppose that g(x, y) is a partial recursive function and that f(x) = μy.g(x, y) where the μ denotes the minimization operator. There exists t_{g} by induction hypothesis. Let t_{f} ≡ λx.(μh.λy.E(t_{g}xy)0(λy.y)(λy.h(s_{N}y))y)0.

We use the next proposition in section 4.

Proposition 1.4.18.

For a term u, variables x, r, (μf.λxr.u)x↓.

Proof 1.4.19.

Let

t ≡ λyxr.F (yy)xr, and

R ≡ λF.tt. Then

μf.λxr.u ≡ R(λfxr.u). Let

a ≡ λyxr.(λfxr.u)(yy)xr. Then,

(μf.λxr.u)x ≃ (λF.tt)(λfxr.u)x
≃ aax
≃ λr.(λfxr.u)(aa)xr.

From λr.(λfxr.u)(aa)xr↓, (μf.λxr.u)x↓.

2 Recursively Defined Predicate

Recursively defined predicates are available in EON + μ. This facility is described in this section.

2.1 Formula

We have an extended formula including recursively defined predicates in EON + μ by the definition 1.1.1 of E-formula. This is explained here.

Example 2.1.1.

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

Remark that P occurs only at the strictly positive position in

x = 0 ∨ ∃y(P (y) & x = s_{N}y) so that the condition (i) of E-formula 1.1.1 is satisfied.

We abbreviate the above formula as B(x). B(x) is the least predicate for which the following holds,

B(x) ↔ x = 0 ∨ ∃y(B(y) & x = s_{N}y).

2.2 Axioms

Proposition 2.2.1.

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

B(x) ↔ A[B].  (R1’)

Proof 2.2.2.

The part of ← holds from (R1). The part of → is proved by letting C ≡ (x).A[B] in (R2).

The axiom (R2) means that B(x) is the least predicate B(x) for which (R1’) holds, i.e., if

C(x) ↔ A[C], then

B(x) → C(x)

holds.

(R2) represents general induction schemata. Induction schemata for various kinds of data structures are induced from (R2).

Example 2.2.3.

Let B(x) be the same as in example 2.1.1.

B(x) ↔ N(x) can be proved. N(x) → B(x) is proved from (R1) and the mathematical induction axiom (N5). B(x) → N(x) is proved from (R2).

2.3 Program Specification

In this paper, we represent a program specification with a formula of EON + μ and produce a term which corresponds to a program satisfying the specification.

The program specification is represented by a formula A(x) for an input condition and a formula B(x, y) for an input output relation where x is an input and y is an output. The formula ∀x(A(x) → ∃yB(x, y)) means that for a given input x satisfying an input condition A(x), we can compute an output y satisfying an input output relation B(x, y). We synthesize a program by proving this formula.

The recursive definition of predicates is convenient for description of program specification. Recursive control structures and recursive data structures are important for programming. Therefore, recursive concepts are important to describe specification. We can represent specification naturally and expressively with recursively defined predicates.

Example 2.3.1. (Factorial)

A formula which represents the input output relation of the factorial program is given in the following.

(μP.(x, y).x = 0 & y = 1 ∨ x ≠ 0 & ∃z(P (p_{N}x, z) & y = x ∗ z))(x, y), where + and ∗ are defined by

x + 0 = x,
x + s_{N}y = s_{N}(x + y),
x ∗ 0 = 0,
x ∗ s_{N}y = x ∗ y + x.

Let B(x, y) be the above formula. Then

B(x, y) ↔ x = 0 & y = 1 ∨ x ≠ 0 & ∃z(B(p_{N}x, z) & y = x ∗ z). (1)

This is the recursive definition of the factorial program. The formula (1) corresponds to the following Prolog program.

B(0, 1).

B(s_{N}x, x ∗ z) ← B(x, z).

Example 2.3.2. (Power of 2)

We discuss the program which computes the least power of 2 which is equal or greater than an input. The specification of this program is described for an input x and an output y as

x ≤ y & ∃n(y = 2^{n} & ∀m(x ≤ 2^{m} → n ≤ m)), where 2^{n} and ≤ are defined in the following way.

2^{0} = 1,
2^{sNx} = 2 ∗ 2^{x}.
x ≤ y ≡ N(x) & N(y) & ∃z(N(z) & x + z = y).

Another representation of the specification of this program is

(μP.(x, y).∃n(x = 2^{n}) & x = y ∨ ¬∃n(x = 2^{n}) & P (x + 1, y))(x, y). (2)

We abbreviate (2) as B(x, y). Remark that this definition calls B(x + 1, y) recursively in the body to specify B(x, y).

The formula (2) corresponds to the following Prolog program.

B(2^{n}, 2^{n}).

B(x, y) ← B(x + 1, y).

2.4 Primitive Recursion

In the assumption ∀x(A[C]→C(x)) of (R2), A[C] calls only C. We can view A[C] as an iteration. In this point of view, we have the following form of another induction principle which uses the primitive recursion.

∀x(A[(x).B(x) & C(x)] → C(x)) → ∀x(B(x) → C(x))  (R3)

In this form, A[(x).B(x) & C(x)] calls both B and C where B ≡ (μP.(x).A[P]).

This primitive recursive form of induction principle can be used in EON + μ.

Theorem 2.4.1. (Primitive Recursion)

(R3) is provable in EON + μ.

Proof 2.4.2.

Taking C ≡ (x).B(x) & C(x) in (R2), we have

∀x(A[(x).B(x) & C(x)] → B(x) & C(x)) → ∀x(B(x) → B(x) & C(x)). From A[(x).B(x) & C(x)] → A[B] and (R1), (R3) is provable.

2.5 Mutual Recursion

The mutual recursive definition of predicates can be used in EON + μ.

Theorem 2.5.1. (Mutual Recursion)

Suppose that

A_{i}[P_{1},…, P_{n}] (1 ≤ i ≤ n) are E-formulae whose free new predicate symbols are P_{1},…, P_{n} and each (μP_{j}.(x).A_{i}[P_{1},…, P_{n}])(t) is also an E-formula for 1 ≤ i, j ≤ n.

There exists the abstracted formulae B_{1},…, B_{n} of EON + μ such that

1. A_{i}[B_{1},…, B_{n}] → B_{i}(x_{i}) (1 ≤ i ≤ n),

2. &_{1≤i≤n} ∀x_{i}(A_{i}[C_{1},…, C_{n}] → C_{i}(x_{i})) → &_{1≤i≤n} ∀x_{i}(B_{i}(x_{i}) → C_{i}(x_{i}))

hold.

We call B_{1},…, B_{n} the least solutions of condition 1.

Proof 2.5.2.

This is proved by induction on n.

Case n = 1.

The claim holds directly by (R1) and (R2). Case n > 1.

By induction hypothesis, there are the least solutions B_{1},…, B_{n−1} of

A_{i}[B_{1},…, B_{n−1}, μP.A_{n}[B_{1},…, B_{n−1}, P]] → B_{i}(x_{i}) (1 ≤ i ≤ n − 1). (3) Let

B_{n} ≡ μP.A_{n}[B_{1},…, B_{n−1}, P]. (4) We show B_{1},…, B_{n} are the least solutions of 1., i.e., the above conditions 1. and 2. hold for these B_{1},…, B_{n}.

From induction hypothesis 1. of (3) and (4),

A_{i}[B_{1},…, B_{n}] → B_{i}(x_{i}) (1 ≤ i ≤ n − 1) holds. By (4) and (R1),

A_{n}[B_{1},…, B_{n}] → B_{n}(x_{n}). Therefore, 1. holds for B_{1},…, B_{n}.

Suppose

∀x_{i}(A_{i}[C_{1},…, C_{n}] → C_{i}(x_{i})) (1 ≤ i ≤ n). (5) We show

∀x_{i}(B_{i}(x_{i}) → C_{i}(x_{i})) (1 ≤ i ≤ n). By (5),

∀x_{n}(A_{n}[C_{1},…, C_{n}] → C_{n}(x_{n})). Using (R2),

∀x_{n}((μP.A_{n}[C_{1},…, C_{n−1}, P])(x_{n}) → C_{n}(x_{n})).

Therefore,

A_{i}[C_{1},…, C_{n−1}, μP.A_{n}[C_{1},…, C_{n−1}, P]] → A_{i}[C_{1},…, C_{n}] (1 ≤ i ≤ n − 1). Therefore, by (5),

A_{i}[C_{1},…, C_{n−1}, μP.A_{n}[C_{1},…, C_{n−1}, P]] → C_{i}(x_{i}) (1 ≤ i ≤ n − 1). By induction hypothesis 2. of (3),

∀x_{i}(B_{i}(x_{i}) → C_{i}(x_{i}))  (1 ≤ i ≤ n − 1).  (6)

By this, A_{n}[B_{1},…, B_{n−1}, C_{n}] → A_{n}[C_{1},…, C_{n}].

A_{n}[B_{1},…, B_{n−1}, C_{n}] → C_{n}.

From (4) and (R2),

∀x_{n}(B_{n}(x_{n}) → C_{n}(x_{n})). (7)

By (6) and (7), 2. holds for B_{1},…, B_{n}.

2.6 Data Types

In EON + μ, we can represent recursive data types using recursively defined predicates. The axiom (R2) induces induction schemata for each recursive data type.

Example 2.6.1. (Lists of Natural Numbers)

Let B(x) be

(μP.(x).x = 0 ∨ x ≠ 0 & ∃y, z(x = pyz & N(y) & P (z)))(x). B(x) represents that x is a list of natural numbers where an empty list is 0. The assumption

of an instance of (R3) for this B(x) is ∀x(x = 0 ∨ x ≠ 0 & ∃y, z(x = pyz & N(y) & B(z) & C(z)) → C(x)).

The assumption is equivalent to

C(0) & ∀y, z(N(y) & B(z) & C(z) → C(pyz)). Therefore, from (R2) using (R3) we get a list induction schema

C(0) & ∀y, z(N(y) & B(z) & C(z) → C(pyz)) → ∀x(B(x) → C(x)).

Example 2.6.2. (Trees of Natural Numbers)

A tree whose leaves are natural numbers is defined by the predicate

B(x) ≡ (μP.(x).N(x) ∨ ∃y, z(P (y) & P (z) & x = pyz))(x). An assumption of an instance of (R3) for this formula is

∀x(N(x) ∨ ∃y, z(B(y) & C(y) & B(z) & C(z) & x = pyz) → C(x)). This is equivalent to

∀x(N(x) → C(x)) &

∀y, z(B(y) & C(y) & B(z) & C(z) → C(pyz)).

Therefore, a tree induction schema is induced from (R2) using (R3).

2.7 Inductive Definition by Horn Clauses

The inductive definition by Horn clauses, which is used in Prolog, can be represented in EON + μ.

Suppose that the inductive definition of P_{1}, …, P_{n} by Horn clauses is given by

P_{i}(t_{i,j}) ← B_{i,j}^{1},…, B_{i,j}^{m_{i,j}}. (1 ≤ j ≤ k_{i}, 1 ≤ i ≤ n) with notation of Prolog. The predicate symbol of B_{i,j}^{l} may be some P_{i} for 1 ≤ i ≤ n.

Let

A_{i}[P_{1},…, P_{n}] ≡ ⋁_{1≤j≤k_{i}} ∃y_{i,j}(x_{i} = t_{i,j} & &_{1≤l≤m_{i,j}} B_{i,j}^{l})

for 1 ≤ i ≤ n where each y_{i,j} includes all the free variables of

x_{i} = t_{i,j} & &_{1≤l≤m_{i,j}} B_{i,j}^{l}.

The axioms corresponding to the above inductive definition are as follows.

A_{i}[P_{1},…, P_{n}] → P_{i}(x_{i}) (1 ≤ i ≤ n) (I1)
&_{1≤i≤n} ∀x_{i}(A_{i}[C_{1},…, C_{n}] → C_{i}(x_{i})) → &_{1≤i≤n} ∀x_{i}(P_{i}(x_{i}) → C_{i}(x_{i}))  (I2)

These P_{1},…, P_{n} satisfying (I1) and (I2) can be represented by the mutual recursion theorem 2.5.1 in EON + μ because P_{1},…, P_{n} occur only at strictly positive positions in

A_{i}[P_{1},…, P_{n}] (1 ≤ i ≤ n).

3 Model

In this section, we give models of EON + μ and prove the consistency of EON + μ.

3.1 Models of EON and EON + E

EON has various models including term models and continuous models.

The normal term model, the closed normal term model, the total term model, the closed total term model are proposed as term models. We have the D_{∞} model and the graph model as continuous models.

Definition 3.1.1. (EON + E)

The constants of EON + E consists of the ones of EON + μ. The language of EON + E is defined in the same way as EON. The axioms of EON + E are the ones of EON + μ except (R1) and (R2).

We compare EON + E with EON. The constants of EON + E are the ones of EON except d, and E. The axioms of EON + E are the ones of EON except the axioms about d, and (D1), (D2), (D3) and (D4).

The closed normal term model is a model of EON + E. We do not give a proof of this fact in this paper.

3.2 Extension of Models of EON + E

We fix an arbitrary model M of EON + E, for example, the closed normal term model. Let its universe be U. A model M′ of EON + μ is constructed from M.

We choose U as a universe of M′.

The constants and predicate symbols of EON + μ which are in EON + E are interpreted in M′ in the same way as those of EON + E are interpreted in M. We extend the interpretation of EON + E to interpret the recursively defined predicates.

Axioms and rules of EON + μ except for (R1)(R2) are still in EON + E. These are proved to be sound concerning this interpretation in the same way as concerning the interpretation of EON + E in M.

In the sequent, a part of the language of EON + μ extended from EON + E, i.e., a recursively defined predicate is interpreted in M′. With respect to this interpretation, we prove that the axioms (R1)(R2) are sound.

3.3 Interpretation of Recursively Defined Predicates

We use the next theorem for the interpretation.

Theorem 3.3.1. (Least Fixed Point)

Let S be a set and p(S) be a powerset of S. Let f : p(S) → p(S) be a monotone function. Then, there exists a ∈ p(S) such that

1. f(a) = a,

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

Proof 3.3.2.

Suppose that x ∈ p(S). For an arbitrary ordinal α, we define f^{α}(x) by transfinite induction on α.

f^{0}(x) = x.

f^{α}(x) = f(f^{β}(x))  if α = β + 1.
f^{α}(x) = ⋃_{β<α} f^{β}(x)  if α is a limit ordinal.

Let a = f^{γ}(ϕ) for an ordinal γ such that |p(S)| < γ.

Notation 3.3.3.

We use lfp.f to denote the above a.

Definition 3.3.4. (Interpretation of a Formula)

M′ ⊧ (μP.(x).A[P])(t) is defined to be t ∈ lfp.F where |x| = n, F : p(U^{n}) → p(U^{n}), F (X) = {x ∈ U^{n} | M′ ⊧ A[(x).x ∈ X]}.

3.4 Soundness of EON + μ

Theorem 3.4.1.

If EON + μ ⊢ A, then M′ ⊧ A.

Proof 3.4.2.

We prove this theorem by induction on the length of a proof. The cases are classified by the last axiom or rule used in the proof.

In the cases of the axioms and rules except for (R1)(R2), this is proved in the same way as for EON + E and M. We omit these cases here and prove only cases (R1)(R2).

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

Case (R1). A[B] → B(x).

Suppose M′ ⊧ A[B]. From the definition of the interpretation, M′ ⊧ A[(x).x ∈ lfp.F] where F is one in the above definition.

{ x ∈ U^{n} | M′ ⊧ A[B] }
= { x ∈ U^{n} | M′ ⊧ A[(x).x ∈ lfp.F] }
= F (lfp.F)
= lfp.F.
If M′ ⊧ A[B], then M′ ⊧ x ∈ lfp.F.

From the definition, M′ ⊧ B(x) iff M′ ⊧ x ∈ lfp.F.

If M′ ⊧ A[B], then M′ ⊧ B(x).

Case (R2). ∀x(A[C] → C(x)) → ∀x(B(x) → C(x)).

Suppose that M′ ⊧ ∀x(A[C] → C(x)). Let X = { x ∈ U^{n} | M′ ⊧ C(x) }. Then,

M′ ⊧ ∀x(A[(x).x ∈ X] → x ∈ X).

F (X) ⊂ X.
From the theorem 3.3.1,  lfp.F ⊂ X.
M′ ⊧ ∀x(B(x) → C(x)).

Theorem 3.4.3.

EON + μ is consistent.

4 Realizability Interpretation

In this section, we present q-realizability interpretation for EON + μ and prove the soundness of this interpretation.

4.1 Proof as Program

EON + μ is based on intuitionistic logic. In a formal system based on intuitionistic logic, we can get a term t such that A(t) from a proof of ∃xA(x). Hence we can compute a term t such that A(t) by proving ∃xA(x). Moreover, if we prove ∀x(A(x) → ∃yB(x, y)) then we can get a term v such that B(u, v) from the proof whenever an input term u such that A(u) is given. Therefore we can synthesize a program whose input condition and input output relation are A(x) and B(x, y) respectively by proving ∀x(A(x) → ∃yB(x, y)) [4, 8, 16].

In this paper, the method to extract a program from a proof by q-realizability interpretation is discussed.

We intend to synthesize programs by this approach. A program specification is given by the formula ∀x(A(x) → ∃yB(x, y)) of EON + μ. This formula is proved automatically or semiautomatically in EON + μ. A program is extracted from the produced proof by q-realizability interpretation.

4.2 q-realizability Interpretation

Definition 4.2.1. (Extended q-realizability Interpretation)

For an E-formula A, new predicate symbols P_{1},…, P_{n}, abstracted formulae F_{1},…, F_{n}, G_{1},…, G_{n}, such that the arity of F_{i} is the one of P_{i} and the arity of G_{i} is 1 + the one of P_{i}, a fresh variable e, we define an E-formula

e q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] A by induction on the construction of an E-formula A.

We abbreviate

q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] as q′ and

q_{P_{1},...,P_{n},P} [F_{1}, G_{1},…, F_{n}, G_{n}, F, G] as q′_{P} [F, G]. Remark that we use A_{P_{1},...,P_{n}}[F_{1},…, F_{n}] according to notation 1.1.9.

1. e q′ A ≡ e = 0 & A_{P_{1},...,P_{n}}[F_{1},…, F_{n}] if A is a Harrop E-formula.

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

e q′ Q(t) ≡ e = 0 & Q(t) if Q ≢ P_{i} (1 ≤ i ≤ n).

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

4. e q′ A ∨ B ≡ N(e_{0}) & (e_{0} = 0 → (e_{1} q′ A) & A_{P_{1},...,P_{n}}[F_{1},…, F_{n}]) & (e_{0} ≠ 0 → (e_{1} q′ B) & B_{P_{1},...,P_{n}}[F_{1},…, F_{n}]).

5. e q′ A → B ≡ ∀q((q q′ A) & A_{P_{1},...,P_{n}}[F_{1},…, F_{n}] → (eq q′ B)) & e↓.

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

7. e q′ ∃xA(x) ≡ (e_{1} q′ A(e_{0})) & A(e_{0})_{P_{1},...,P_{n}}[F_{1},…, F_{n}].

8. e q′ (μP.(x).A[P])(t) ≡

(μP^{∗}.(e, x).(e q′_{P} [B_{P_{1},...,P_{n}}[F_{1},…, F_{n}], P^{∗}] A[P]))(e, t), where B ≡ μP.(x).A[P].

Remark 4.2.2.

An E-formula e q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] A expresses the usual q-realizability interpretation

e q A except that all the occurrences of subformulae P_{i}(t) in the formula e q A are replaced by F_{i}(t) and all the occurrences of subformulae r q P_{i}(t) in the formula e q A are replaced by G_{i}(r, t) simultaneously for 1 ≤ i ≤ n.

Another point of the difference of this definition from the usual q-realizability interpretation is the definedness in clause 1, 2 and 5. We intend to simplify the definedness condition of the interpretation of A → B while proposition 4.2.13 holds.

Example 4.2.3.

Let

B ≡ μP.(x).(x = 0 ∨ ∃y(P (y) & x = s_{N}y)). The formula e q B(t) is expanded according to the definition of the extended q-realizability interpretation as follows.

e q B(t)

≡ e q (μP.(x).x = 0 ∨ ∃y(P (y) & x = s_{N}y))(t)
≡ (μP^{∗}.(e, x).(e q_{P} [B, P^{∗}] x = 0 ∨ ∃y(P (y) & x = s_{N}y)))(e, t)  (8)
≡ (μP^{∗}.(e, x).(N(e_{0}) &
(e_{0} = 0 → (e_{1} q_{P} [B, P^{∗}] x = 0) & x = 0) &
(e_{0} ≠ 0 → (e_{1} q_{P} [B, P^{∗}] ∃y(P (y) & x = s_{N}y)) &
∃y(B(y) & x = s_{N}y))))(e, t)  (9)
≡ (μP^{∗}.(e, x).(N(e_{0}) &
(e_{0} = 0 → (e_{1} = 0 & x = 0 & x = 0) &

(e_{0} ≠ 0 → (e_{11} q_{P} [B, P^{∗}] P (e_{10}) & x = s_{N}e_{10}) & B(e_{10}) & x = s_{N}e_{10} &

∃y(B(y) & x = s_{N}y))))(e, t)  (10)
≡ (μP^{∗}.(e, x).(N(e_{0}) &

(e_{0} = 0 → (e_{1} = 0 & x = 0 & x = 0) & (e_{0} ≠ 0 → (e_{110} q_{P} [B, P^{∗}] P (e_{10})) &

(e_{111} q_{P} [B, P^{∗}] x = s_{N}e_{10}) & B(e_{10}) & x = s_{N}e_{10} & ∃y(B(y) & x = s_{N}y))))(e, t)

≡ (μP^{∗}.(e, x).(N(e_{0}) &

(e_{0} = 0 → (e_{1} = 0 & x = 0 & x = 0) & (e_{0} ≠ 0 → P^{∗}(e_{110}, e_{10}) &

e_{111} = 0 & x = s_{N}e_{10} & B(e_{10}) & x = s_{N}e_{10} &

∃y(B(y) & x = s_{N}y))))(e, t)  (11)
↔ (μP^{∗}.(e, x).(N(e_{0}) &

(e_{0} = 0 → e_{1} = 0 & x = 0) & (e_{0} ≠ 0 → P^{∗}(e_{110}, e_{10}) &

e_{111} = 0 & x = s_{N}e_{10} & B(e_{10}))))(e, t)

Remark that the extended q-realizability interpretation of the above sample is different from the usual q-realizability interpretation in the following points.

1. The new predicate symbol P^{∗} is used to interpret a recursive call of P.

2. In (8), q_{P} [B, P^{∗}] plays the substitution of B for P and P^{∗} for the interpretation of P

respectively. The actual substitutions take place in (9),(10) and (11). Notation 4.2.4.

We use

q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}]_{Q_{1},...,Q_{m}}[H_{1}, I_{1},…, H_{m}, I_{m}] to denote

q_{P_{1},...,P_{n},Q_{1},...,Q_{m}}[F_{1}, G_{1},…, F_{n}, G_{n}, H_{1}, I_{1},…, H_{m}, I_{m}] in the sequel. Proposition 4.2.5. (Substitution Property)

(e q A)[y/x] ≡ e[y/x] q A[y/x].

Proof 4.2.6.

By induction on the construction of A. Definition 4.2.7.

For E-formulae A_{1},…, A_{n}, F P S(A_{1},…, A_{n}) is the set of all the free predicate symbols of A_{1},…, A_{n}. Proposition 4.2.8.

Suppose A is an E-formula and F P S(A) = {P_{1},…, P_{n}}. Then

F P S(e q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] A) ⊂ F P S(F_{1}, G_{1},…, F_{n}, G_{n}). Proof 4.2.9.

We use induction on the definition of q-realizability.

1. A is a Harrop E-formula.

F P S(e q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] A)

= F P S(e = 0 & A_{P_{1},...,P_{n}}[F_{1},…, F_{n}])
= F P S(F_{1},…, F_{n}).

2. A ≡ P_{i}(t).

F P S(e q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] A) = F P S(G_{i}).

3. – 7. Clear by induction hypothesis.

8. A ≡ (μP.(x).A[P])(t).

Let B ≡ μP.(x).A[P]. By induction hypothesis,

F P S(e q_{P_{1},...,P_{n},P} [F_{1}, G_{1},…, F_{n}, G_{n}, B_{P_{1},...,P_{n}}[F_{1},…, F_{n}], P^{∗}] A[P])

⊂ F P S(F_{1}, G_{1},…, F_{n}, G_{n}, B_{P_{1},...,P_{n}}[F_{1},…, F_{n}], P^{∗}).

From F P S(B_{P_{1},...,P_{n}}[F_{1},…, F_{n}]) ⊂ F P S(F_{1},…, F_{n}), l.h.s. ⊂ F P S(F_{1}, G_{1},…, F_{n}, G_{n}) ⋃{P^{∗}}. F P S(e q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] A) ⊂ F P S(F_{1}, G_{1},…, F_{n}, G_{n}).

Proposition 4.2.10.

For a formula A, an E-formula e q A is a formula.

Proof 4.2.11.

From the above proposition.

Definition 4.2.12. (q-realizability Interpretation)

q-realizability interpretation of EON + μ is to interpret a formula A as a formula e q A. If EON + μ ⊢ e q A, then the term e is called the realizer of A.

Proposition 4.2.13.

EON + μ ⊢ (e q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] A) → e↓.

Proof 4.2.14.

We abbreviate

q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] as q′.

1. A is a Harrop E-formula. This claim is clear by the definition of q.

2. (1) A ≡ P_{i}(t).

(2) A ≡ Q(t) if Q ≠≡ P_{i} (1 ≤ i ≤ n).

Both are clear by the definition.

3. A ≡ A_{1} & A_{2}.

(e q′ A) → (e_{0} q′ A_{1}). By induction hypothesis,

(e_{0} q′ A_{1}) → e_{0}↓. From e_{0}↓ → e↓,

(e q′ A) → e↓.

4. A ≡ A_{1} ∨ A_{2}.

From N(e_{0}) → e↓, (e q′ A) → e↓.

5. A ≡ A_{1} → A_{2}.

By the definition of q.

6. A ≡ ∀xA_{1}(x).

(e q′ A) → (e0 q′ A_{1}(0)) holds. By induction hypothesis, (e0 q′ A_{1}(0)) → e0↓. From e0↓ → e↓,

(e q′ A) → e↓.

7. A ≡ ∃xA_{1}(x).

(e q′ A) → (e_{1} q′ A_{1}(e_{0})) holds. By induction hypothesis, (e_{1} q′ A_{1}(e_{0})) → e_{1}↓. From e_{1}↓ → e↓,

(e q′ A) → e↓.

8. A ≡ (μP.(x).A_{1}[P])(t).

Let

B ≡ μP.(x).A_{1}[P] and

C ≡ μP^{∗}.(e, x).(e q′_{P} [B_{P_{1},...,P_{n}}[F_{1},…, F_{n}], P^{∗}] A_{1}[P]). Then,

(e q′ A) ↔

(e q′_{P} [B_{P_{1},...,P_{n}}[F_{1},…, F_{n}], C] A_{1}[P])[t/x]

holds. From induction hypothesis, (e q′_{P} [B_{P_{1},...,P_{n}}[F_{1},…, F_{n}], C] A_{1}[P]) → e↓. (e q′ A) → e↓.

4.3 Soundness Theorem

Theorem 4.3.1. (Soundness of q-realizability)

If EON + μ ⊢ A, then we can find a term e whose free variables are among the ones of A effectively from the proof and

EON + μ ⊢ e q A.

The main point of the proof of the soundness theorem is the proof of the interpretation of (R2).

In the rest of this section, we prove this theorem in the following steps. Firstly, a lemma about (R1) and some auxiliary small lemmas are proved. Secondly, a candidate σ of a realizer of (R2) is defined. Thirdly, a lemma about σ and the soundness of (R2) are proved. Finally, the soundness of NJP and the soundness theorem are proved.

Lemma 4.3.2.

Let B ≡ μP.(x).A[P]. Then, EON + μ ⊢ (e q B(x)) ↔ (e q A[B]).

Proof 4.3.3.

From the definition,

e q B(x) ≡ (μP^{∗}.(e, x).(e q_{P} [B, P^{∗}] A[P]))(e, x). Let R[P^{∗}] ≡ e q_{P} [B, P^{∗}] A[P]. Since P^{∗} does not appear in A[P],

R[F] ≡ e q_{P} [B, F] A[P] is proved by induction on the construction of A.

Therefore, from proposition 2.2.1, (μP^{∗}.(e, x).(e q_{P} [B, P^{∗}] A[P]))(e, x)

↔ (e q_{P} [B, (e, x).e q B(x)] A[P]).

We prove the following by induction on the construction of A.

(e q_{P} [B, (e, x).e q B(x)] A[P]) ≡ e q A[B]. Therefore,

EON + μ ⊢ (e q B(x)) ↔ (e q A[B]).

Proposition 4.3.4.

Suppose that P in an E-formula A[P] occurs only in a part of Harrop E-formulae. Then,

q q_{P_{1},...,P_{n},P} [F_{1}, G_{1},…, F_{n}, G_{n}, F, G] A[P] ≡

q q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] A[F_{P_{1},...,P_{n}}[F_{1},…, F_{n}]].

Proof 4.3.5.

By induction on the construction of A[P].

Proposition 4.3.6.

Suppose P occurs only positively in A[P].

1. A[B] & ∀x(B(x) → C(x)) → A[C] holds.

2. For abstracted formulae F, G, every F and G occurs only positively in e q_{P} [F, G] A[P].

Proof 4.3.7.

Both claims are proved using induction on the construction of A[P]. Remark that P occurs only at the positive position of A[P].

Proposition 4.3.8.

∀ex((e q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] A[P_{1},…, P_{n}]) & A[F_{1},…, F_{n}]→

(e q_{P_{1},...,P_{n}}[F_{1}, (r, x).F_{1}(x) & G_{1}(r, x),…, F_{n}, (r, x).F_{n}(x) & G_{n}(r, x)] A[P_{1},…, P_{n}]))

holds.

Proof 4.3.9.

We abbreviate P_{1},…, P_{n} as P, F_{1},…, F_{n} as F,

q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] as q’, and

q_{P_{1},...,P_{n}}[F_{1}, (r, x).F_{1}(x) & G_{1}(r, x),…, F_{n}, (r, x).F_{n}(x) & G_{n}(r, x)] as q”.

We show this proposition by induction on the construction of A[P].

1. A[P] is a Harrop E-formula. By e q′ A[P] ≡ e q′′ A[P].

2. (1) A[P] ≡ P_{i}(t).

By

e q′ A[P] ≡ G_{i}(e, t) & e↓,
A[P] ≡ F_{i}(t),
e q′′ A[P] ≡ F_{i}(t) & G_{i}(e, t) & e↓.

(2) A[P] ≡ Q(t) (Q ≢ P_{i}).

By e q′ A[P] ≡ e q′′ A[P].

3. A[P] ≡ A_{1}[P] & A_{2}[P].

By induction hypothesis for A_{1}[P] and A_{2}[P].

4. A[P] ≡ A_{1}[P] ∨ A_{2}[P].

By induction hypothesis for A_{1}[P] and A_{2}[P], we have (e q′ A[P]) → (e q′′ A[P]).

5. A[P] ≡ A_{1}[P] → A_{2}[P].

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

From proposition 4.3.4, we have

(q q′′ A_{1}[P]) → (q q′ A_{1}[P]). Using induction hypothesis, we have the claim.

6. A[P] ≡ ∀xA_{1}[P](x).

7. A[P] ≡ ∃xA_{1}[P](x).

Both cases are proved by induction hypothesis for A_{1}[P](x).

8. A[P] ≡ (μQ.(x).A_{1}[P, Q])(t).

By the substitution property proposition 4.2.5 and

A[P] ≡ (μQ.(x).A_{1}[P, Q])(x)[t/x], it is sufficient to show only the case

A[P] ≡ (μQ.(x).A_{1}[P, Q])(x). From the definition, we have

e q′ A[P] ≡ (μQ^{∗}.(r, x).r q′_{Q}[(x).A[F], Q^{∗}] A_{1}[P, Q])(e, x), A[F] ≡ (μQ.(x).A_{1}[F, Q])(x), e q′′ A[P] ≡ (μQ^{∗}.(r, x).r q′′_{Q}[(x).A[F], Q^{∗}] A_{1}[P, Q])(e, x).

Using (R2), it is sufficient to show ∀ex((e q′_{Q}[(x).A[F], (r, x).A[F] → (r q′′ A[P])] A_{1}[P, Q]) & A[F] → (e q′′ A[P])).

Fix e and x and suppose

e q′_{Q}[(x).A[F], (r, x).A[F] → (r q′′ A[P])] A_{1}[P, Q],  (12)
A[F].

From (R1’), A[F] ↔ A_{1}[F, A[F]] holds. Combined with (12), by induction hypothesis for A_{1}[P, Q], we have

e q′′_{Q}[(x).A[F], (r, x).A[F] & (A[F] → (r q′′ A[P]))] A_{1}[P, Q]. From proposition 4.3.6,

e q′′_{Q}[(x).A[F], (r, x).r q′′ A[P]] A_{1}[P, Q] holds. From (R1), we have e q′′ A[P].

Definition 4.3.10.

For an E-formula A, a new predicate symbol P and a term f, we define a term σ_{A}^{P,f} by induction on the construction of A in the following way.

1. A is a Harrop E-formula, then σ_{A}^{P,f} ≡ λr.0.

2. A ≡ P (t), then σ_{A}^{P,f} ≡ λr.ftr.

3. A ≡ Q(t), then σ_{A}^{P,f} ≡ λr.r if Q ≢ P.

4. A ≡ A_{1} & A_{2}, then σ_{A}^{P,f} ≡ λr.⟨σ_{A_{1}}^{P,f}r_{0}, σ_{A_{2}}^{P,f}r_{1}⟩.

5. A ≡ A_{1} ∨ A_{2}, then σ_{A}^{P,f} ≡ λr.⟨r_{0}, Er_{0}0σ_{A_{1}}^{P,f}σ_{A_{2}}^{P,f}r_{1}⟩.

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

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

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

9. A ≡ (μQ.(x).A_{1}[Q])(t), then σ_{A}^{P,f} ≡ (μg.λxr.σ_{A_{1}[Q]}^{Q,g}(σ_{A_{1}[Q]}^{P,f}r))t where Q ≢ P.

Remark 4.3.11.

A formula A can be viewed as the tree whose nodes correspond to logical connectives in A and whose leaves correspond to atomic formulae in A. A term constructed by p can be viewed as a tree whose nodes correspond to p and whose leaves correspond to the arguments of p. Then the tree of a realizer of A is almost isomorphic to the tree of the formula A. A term σ_{A}^{P,f}e represents the term e where every leaf r of the tree e corresponding to a leaf P (t) of the tree A is replaced by ftr when the tree e is almost isomorphic to the tree A.

Proposition 4.3.12.

Let A[P] be an E-formula and B be an abstracted formula where P_{1},…, P_{n} ∉ F P S(B(y)), then

(r q_{P_{1},...,P_{n},P} [F_{1}, G_{1},…, F_{n}, G_{n}, B, (e, x).fxe q B(x)] A[P])
→(σ_{A}^{P,f}r q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}] A[B]).

Proof 4.3.13.

We use induction on the construction of A. 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}, B, (e, x).fxe q B(x)]

as q′′ and σ_{A}^{P,f} as σ_{A}.

1. A is a Harrop E-formula. This case is clear by the definition of q.

2. (1) A ≡ P (t).

From the definition,

(r q′_{P} [B, (e, x).fxe q B(x)] A[P]) ≡ (ftr q B(t)) & r↓, and

σ_{A}r q′ A[B] ≡ (λr.ftr)r q′ B(t), Since P_{1},…, P_{n} ∉ F P S(B(y)), by proposition 4.3.4,

l.h.s. ≡ (λr.ftr)r q B(t). Then the claim holds.

(2) A ≡ P_{i}(t).

(3) A ≡ Q(t).

These cases are clear by the definition of q.

3. A[P] ≡ A_{1}[P] & A_{2}[P].

r q′′ A[P] ≡ r q′′ A_{1}[P] & A_{2}[P]
≡ (r_{0} q′′ A_{1}[P]) & (r_{1} q′′ A_{2}[P]).

By induction hypothesis,

l.h.s. → (σ_{A_{1}}r_{0} q′ A_{1}[B]) & (σ_{A_{2}}r_{1} q′ A_{2}[B])
≡ (⟨σ_{A_{1}}r_{0}, σ_{A_{2}}r_{1}⟩ q′ A_{1}[B] & A_{2}[B])
↔ (σ_{A}r q′ A[B]).

4. A[P] ≡ A_{1}[P] ∨ A_{2}[P].

r q′′ A[P] ≡ r q′′ A_{1}[P] ∨ A_{2}[P]
≡ N(r_{0}) & (r_{0} = 0 → (r_{1} q′′ A_{1}[P]) & A_{1}[B]_{P_{1},...,P_{n}}[F_{1},…, F_{n}]) &
(r_{0} ≠ 0 → (r_{1} q′′ A_{2}[P]) & A_{2}[B]_{P_{1},...,P_{n}}[F_{1},…, F_{n}]).

By induction hypothesis,

l.h.s. → N(r_{0}) &
(r_{0} = 0 → (σ_{A_{1}}r_{1} q′ A_{1}[B]) & A_{1}[B]_{P_{1},...,P_{n}}[F_{1},…, F_{n}]) &
(r_{0} ≠ 0 → (σ_{A_{2}}r_{1} q′ A_{2}[B]) & A_{2}[B]_{P_{1},...,P_{n}}[F_{1},…, F_{n}])
↔ (⟨r_{0}, Er_{0}0σ_{A_{1}}σ_{A_{2}}r_{1}⟩ q′ A[B])
↔ (σ_{A}r q′ A[B]).

5. A[P] ≡ A_{1}[P] → A_{2}[P].

r q′′ A[P] ≡ r q′′ A_{1}[P] → A_{2}[P]
≡ ∀q((q q′′ A_{1}[P]) & A_{1}[B]_{P_{1},...,P_{n}}[F_{1},…, F_{n}] →
(rq q′′ A_{2}[P])) & r↓.

By induction hypothesis,

(rq q′′ A_{2}[P]) → (σ_{A_{2}}(rq) q′ A_{2}[B]). Since P in A_{1}[P] occurs only in Harrop E-formulae by the definition of an E-formula, proposition 4.3.4 says,

q q′′ A_{1}[P] ≡ q q′ A_{1}[B]. Therefore,

r q′′ A[P] → ∀q((q q′ A_{1}[B]) & A_{1}[B]_{P_{1},...,P_{n}}[F_{1},…, F_{n}] →
(σ_{A_{2}}(rq) q′ A_{2}[B])) & r↓.

Remark that we use here our syntactical condition that recursive calls of predicates occur only in Harrop subformulae or at strictly positive positions to infer this formula using proposition 4.3.4. Here r↓ then (λrq.σ_{A_{2}}(rq))r ≃ λq.σ_{A_{2}}(rq). The right hand side is defined by proposition 1.4.18. Hence the left hand side is defined. σ_{A}r↓. Therefore,

r q′′ A[P] → ∀q((q q′ A_{1}[B]) & A_{1}[B]_{P_{1},...,P_{n}}[F_{1},…, F_{n}] →
(σ_{A_{2}}(rq) q′ A_{2}[B])) & σ_{A}r↓
↔ (σ_{A}r q′ A[B]).

6. A[P] ≡ ∀xA_{1}[P](x).

r q′′ ∀xA_{1}[P](x) ≡ ∀x(rx q′′ A_{1}[P](x)).

By induction hypothesis,

l.h.s. → ∀x(σ_{A_{1}[P](x)}(rx) q′ A_{1}[B](x))
↔ (λx.σ_{A_{1}[P](x)}(rx) q′ A[B])
↔ (σ_{A}r q′ A[B]).

7. A ≡ ∃xA_{1}(x).

r q′′ ∃xA_{1}[P](x) ≡ A_{1}[B](r_{0})_{P_{1},...,P_{n}}[F_{1},…, F_{n}] & (r_{1} q′′ A_{1}[P](r_{0})).

By induction hypothesis,

l.h.s. → A_{1}[B](r_{0})_{P_{1},...,P_{n}}[F_{1},…, F_{n}] & (σ_{A_{1}(r_{0})}r_{1} q′ A_{1}[B](r_{0}))
≡ (⟨r_{0}, σ_{A_{1}(r_{0})}r_{1}⟩ q′ ∃xA_{1}[B](x))
↔ (σ_{A}r q′ A[B]).

8. A[P] ≡ (μQ.(x).A_{1}[P, Q])(t). Let B ≡ μQ.(x).A_{1}[P, Q]. We can assume Q ∉ F P S(B(y)) renaming bound predicate symbols.

r q′′ (μQ.(x).A_{1}[P, Q])(t)
≡ (μQ^{∗}.(r, x).(r q′′_{Q}[(x).A[B], Q^{∗}] A_{1}[P, Q]))(r, t)

≡ (μQ^{∗}.(r, x).(r q′_{Q,P} [(x).A[B], Q^{∗}, B, (e, x).(fxe q B(x))]
A_{1}[P, Q]))(r, t).

By induction hypothesis,

l.h.s.

→ (μQ^{∗}.(r, x).σ_{A_{1}}r q′_{Q}[(x).A[B], Q^{∗}] A_{1}[B, Q])(r, t)
↔ (σ_{A_{1}}[t/x]r q′ (μQ.(x).A_{1}[B, Q])(t))
↔ (σ_{A}r q′ A[B]).

Lemma 4.3.14.

There exists a term e which q-realizes the axiom (R2). Proof 4.3.15.

Let B ≡ μP.(x).A[P]. Suppose that

∀x(A[C] → C(x)),  (13)
q q ∀x(A[C] → C(x)).  (14)

Let f be μf.λxr.qx(σ_{A}^{P,f}r).

Under these conditions, we prove

∀rx(((r q B(x)) & B(x) → (fxr q C(x))) & ∀x fx↓. (15) Let R[B, P^{∗}] ≡ r q_{P} [B, P^{∗}] A[P]. From the definition of q,

r q B(x) ≡ (μP^{∗}.(r, x).R[B, P^{∗}])(r, x). From (R2),

∀rx(R[B, (r, x).B(x) → (fxr q C(x))] & B(x) → (fxr q C(x)))

→ ∀rx((r q B(x)) & B(x) → (fxr q C(x))).

Therefore it is sufficient to prove the next formula in the sequent.

∀rx(R[B, (r, x).B(x) → (fxr q C(x))] & B(x) → (fxr q C(x))). We fix r, x now. Suppose that

R[B, (r, x).B(x) → (fxr q C(x))],  (16)
B(x).

Combined with (R2’),

A[B] (17)

holds. By (16), (17) and proposition 4.3.8, R[B, (r, x).fxr q C(x)] holds.

From (13) and (R2),

∀x(B(x) → C(x)) (18)

holds.

By proposition 4.3.6 and this,

R[B, (r, x).fxr q C(x)] → R[C, (r, x).fxr q C(x)].

R[C, (r, x).fxr q C(x)] holds.

From proposition 4.3.12,

(r q_{P} [C, (r, x).fxr q C(x)] A[P]) → (σ_{A}^{P,f}r q A[C]).

σ_{A}^{P,f}r q A[C] holds.

By (17), (18) and proposition 4.3.6, we have A[C].

Therefore, by (14), we have qx(σ_{A}^{P,f}r) q C(x). From proposition 4.2.13, qx(σ_{A}^{P,f}r)↓. By the definition of f, fxr ≃ qx(σ_{A}^{P,f}r) holds. Then fxr = qx(σ_{A}^{P,f}r). Therefore, fxr q C(x).

∀x fx↓ is proved by proposition 1.4.18. Therefore, (15) holds. Let e ≡ λq.μf.λxr.qx(σ_{A}^{P,f}r), then this lemma holds.

Proposition 4.3.16. (Soundness of q-realizability for NJP)

If NJP ⊢ A, then we can find a term e whose free variables are among the ones of A effectively from the proof and

NJP ⊢ e q A.

Proof 4.3.17.

We prove

NJP, Γ ⊢ A implies NJP, Γ, (u q Γ) ⊢ e q A by the induction on the length of the proof of A where Γ, u and e denote formulae, distinct variables not occurring in Γ and a term constructed from the proof respectively. Cases are classified according to the last rule used in the proof.

We abbreviate NJP, Γ ⊢ A as Γ ⊢ A. In cases from (&I) to (∃I) where no formula is discharged in a rule, NJP, Γ ⊢ A is abbreviated as ⊢ A.

Case (&I).

By induction hypothesis there are a and b such that ⊢ a q A and ⊢ b q B. If A & B is a Harrop formula, then let e ≡ 0. Otherwise, let e ≡ ⟨a, b⟩. Then the claim holds.

Case (&E_{l}).

By induction hypothesis, there is q such that ⊢ q q A & B. If A & B is Harrop, then let e ≡ 0. Otherwise let e ≡ q_{0}.

Case (&E_{r}).

By induction hypothesis, there is q such that ⊢ q q A & B. If A & B is Harrop, then let e ≡ 0. Otherwise let e ≡ q_{1}.

Case (∨I_{l}).

By induction hypothesis, there is a such that ⊢ a q A. Let e ≡ ⟨0, a⟩.

Case (∨I_{r}).

By induction hypothesis, there is b such that ⊢ b q B. Let e ≡ ⟨1, b⟩.

Case (→E).

By induction hypothesis there are a and f such that ⊢ a q A and ⊢ f q A → B. If A → B is Harrop, B is also Harrop. Then let e ≡ 0. Otherwise, let e ≡ fa.

Case (∀I).

By induction hypothesis there is a such that ⊢ a q A(x). If ∀xA(x) is Harrop, then let e ≡ 0. Otherwise, let e ≡ λx.a.

Case (∀E).

By induction hypothesis there is a such that ⊢ a q ∀xA(x). If ∀xA(x) is Harrop, then let e ≡ 0. Otherwise, let e ≡ at.

Case (∃I).

By induction hypothesis there is a such that ⊢ a q A(t). Let e ≡ ⟨t, a⟩.

Case (⊥E).

By induction hypothesis ⊥ is proved. Let e ≡ 0.

Case (∨E).

This rule is

\begin{matrix}Γ_{1} ⊢ A ∨ B & Γ_{2}, A ⊢ C & Γ_{3}, B ⊢ C \\ Γ_{1}, Γ_{2}, Γ_{3} ⊢ C. \end{matrix} (∨E)

By induction hypothesis,

Γ_{1}, (u q Γ_{1}) ⊢ e q A ∨ B,  (19)
Γ_{2}, (v q Γ_{2}), A, (a q A) ⊢ c q C,  (20)
Γ_{3}, (w q Γ_{3}), B, (b q B) ⊢ d q C  (21)

hold. Let

f ≡ Ee_{0}0(λa.c)(λb.d)e_{1}. Then, from (20) and (21),

Γ_{2}, (v q Γ_{2}), A & (e_{1} q A) & e_{0} = 0 ⊢ f q C, Γ_{3}, (w q Γ_{3}), B & (e_{1} q B) & e_{0} ≠ 0 ⊢ f q C.

By (19),

Γ_{1}, (u q Γ_{1}) ⊢ e_{0} = 0 & A & (e_{1} q A) ∨ e_{0} ≠ 0 & B & (e_{1} q B)

holds. Then Γ_{1}, (u q Γ_{1}), Γ_{2}, (v q Γ_{2}), Γ_{3}, (w q Γ_{3}) ⊢ f q C.

Case (→I).

This rule is

{Γ, A ⊢ B \atop Γ ⊢ A → B.} (→I)

By induction hypothesis,

Γ, (u q Γ), A, (a q A) ⊢ b q B.

Γ, (u q Γ) ⊢ A & (a q A) → (b q B).
Γ, (u q Γ) ⊢ ∀a(A & (a q A) → (b q B)).

Let

e ≡ λa.b,

then

Γ, (u q Γ) ⊢ e q A → B.

Case (∃E).

This rule is

\begin{matrix}Γ_{1} ⊢ ∃xA(x) & Γ_{2}, A(a) ⊢ C \\ Γ_{1}, Γ_{2} ⊢ C \end{matrix} (∃E)

where a does not occur in Γ_{2} nor C. By induction hypothesis,

Γ_{1}, (u q Γ_{1}) ⊢ e q ∃xA(x),
Γ_{2}, (v q Γ_{2}), A(a), (b q A(a)) ⊢ c q C

hold. Hence

Γ_{1}, (u q Γ_{1}) ⊢ A(e_{0}) & (e_{1} q A(e_{0})),
Γ_{2}, (v q Γ_{2}) ⊢ A(e_{0}) & (e_{1} q A(e_{0})) → (c[e_{0}/a, e_{1}/b] q C).

Let

f ≡ c[e_{0}/a, e_{1}/b].

Then

Γ_{1}, (u q Γ_{1}), Γ_{2}, (v q Γ_{2}) ⊢ f q C.

Proof 4.3.18. (Soundness Theorem)

We prove it by induction on the length of the proof of A. Cases are classified according to the last axiom or rule used in the proof.

1. Logical rules.

The cases for logical rules are proved from proposition 4.3.16.

2. Non logical axioms.

Case Axioms except for (E2), (N5), (D1), (R1) and (R2). These axioms are all Harrop. Therefore let e ≡ 0 then the claim holds.

Case (E2).

If A(y) is Harrop, then let e ≡ 0. Otherwise let

e ≡ λxyq.(λx.q_{1})y, then e q (E2).

Case (N5).

If A(x) is Harrop, then let e ≡ 0. Otherwise, let

f ≡ μf.λx.Ex0(λr.q_{0})(λr.q_{1}(p_{N}x)⟨0, f(p_{N}x)⟩)0,
e ≡ λqxr.fx.

Then,

f0 = q_{0},
f(s_{N}x) = q_{1}x⟨0, fx⟩.

Hence e q (N5).

Case (D1).

Let

e ≡ λxy.Exy⟨0, 0⟩⟨1, 0⟩. Then e q (D1) holds.

Case (R1).

From lemma 4.3.2, λx.x q (R1).

Let

e ≡ λx.x.

Case (R2).

(R2) is q-realized by lemma 4.3.14.

Remark 4.3.19.

In EON + μ, recursively defined predicates are restricted by the syntactical condition that recursive calls of predicates occur only in Harrop subformulae or at strictly positive positions.

This restricting condition is only a sufficient condition for the soundness of q-realizability interpretation. We do not know whether the soundness theorem can be proved under the weaker restriction of recursively defined predicates.

5 Program Synthesis by q-realizability Interpretation

In this section, we explain the method of program synthesis using q-realizability interpretation and present some examples.

5.1 Method

We produce a program by synthesis using realizability in the following way.

1. A specification represented by a formula is given.

2. The specification formula is proved in EON + μ.

3. A program is synthesized by extracting it from the proof.

We treat only functional programs in this paper. Because functional programs have theoretically good features. They have no side effects so that they can be treated algebraically. They are represented by combinators neatly.

Programs are written in the form of combinators here. Combinators are computed by term reduction. Some computers are designed for term reduction of combinatory terms directly and can compute it efficiently [18].

A program specification is described with a formula which presents an input condition and an input output relation. If the program has n inputs x_{1},… x_{n}, then an input condition is represented as a formula A(x_{1},…, x_{n}) and an input output relation is represented as B(x_{1},…, x_{n}, y) where y is an output. For example, the factorial program has one input x and an output y. A formula representing an input condition that an input x is a natural number is N(x). A formula representing an input output relation that an output y is the factorial of an input x is

(μP.(x, y).x = 0 & y = 1 ∨ x ≠ 0 & ∃z(P (p_{N}x, z) & y = x ∗ z))(x, y).

We call a formula ∀x_{1},…, x_{n}(A(x_{1},…, x_{n}) → ∃yB(x_{1},…, x_{n}, y)) a specification formula of a program. A programs is produced by proving a specification formula.

The specification formula is proved in EON + μ. This stage is the key of this method of program synthesis. First, programs depend directly on proofs they are extracted from. We need develop an appropriate proof to produce a good program. Second, only this stage cannot be automated completely. Automated theorem proving has been discussed extensively, but the final method has not been established yet. Moreover, for this method of program synthesis, we must prove it in EON + μ which is based on intuitionistic logic. We must not use the law of excluded middle in the proofs and cannot use usual refutation methods using the resolution principle.

The extraction of programs from proofs is automated completely. We can use q-realizability interpretation of EON + μ for this purpose. The proofs decide the extracted programs logically. This is the reason why we need make appropriate proofs to get intended programs.

By this method, we produce correct programs only. Using q-realizability interpretation, not only programs but also verification proofs of total correctness of these programs are generated simultaneously.

5.2 Program Extraction

Definition 5.2.1. (Semi Self-realizing Formula)

A formula A is semi self-realizing if and only if there is a closed term j_{A} such that

EON + μ ⊢ A → (j_{A}x q A) where x are all the free variables x_{1},…, x_{n} of A.

Proposition 5.2.2.

A Harrop formula is semi self-realizing.

Remark 5.2.3.

We have as semi self-realizing formulae not only Harrop formulae. For example,

∃x(x = y) is semi self-realizing with j = λy.⟨y, 0⟩ and not Harrop. Theorem 5.2.4.

If EON + μ ⊢ ∀x(A(x)→∃yB(x, y)) and A(x) is semi self-realizing, then we can find a term f effectively from this proof and

EON + μ ⊢ ∀x(A(x) → B(x, fx) & fx↓). Proof 5.2.5.

By the soundness theorem, we can get a term e such that

EON + μ ⊢ e q ∀x(A(x) → ∃yB(x, y)). From the definition of q-realizability,

EON + μ ⊢ ∀xq(A(x) & (q q A(x)) →
B(x, p_{0}(exq)) & (p_{1}(exq) q B(x, p_{0}(exq)))).

We have a self-realizer j_{A} of A(x). Let q be j_{A}x and f ≡ λx.p_{0}(ex(j_{A}x)), then

EON + μ ⊢ ∀x(A(x) → B(x, fx)). By proposition 4.2.13,

EON + μ ⊢ (p_{1}(ex(j_{A}x)) q B(x, p_{0}(ex(j_{A}x)))) → p_{1}(ex(j_{A}x))↓. Here

p_{1}(ex(j_{A}x))↓ → ex(j_{A}x)↓,
ex(j_{A}x)↓ → p_{0}(ex(j_{A}x))↓.

Then,

EON + μ ⊢ ∀x(A(x) → B(x, fx) & fx↓).

This theorem shows that we can get a program f and a verification proof of total correctness simultaneously from the proof of ∀x(A(x) → ∃yB(x, y)).

5.3 Examples of Program Synthesis

We present some examples of program synthesis by this method here.

Example 5.3.1. (Factorial Program)

The specification formula of the factorial program is

∀x(N(x) → ∃y((μP.(x, y).x = 0 & y = 1 ∨ x ≠ 0 & ∃z(P (p_{N}x, z) & y = x ∗ z))(x, y))) where + and ∗ are defined as in section 2.

This formula is proved using mathematical induction easily. Let

F act ≡ μP.(x, y).F actBody[P](x, y),
F actBody[P](x, y) ≡ x = 0 & y = 1 ∨ x ≠ 0 & ∃z(P (p_{N}x, z) & y = x ∗ z).

Then the specification formula is

∀x(N(x) → ∃y F act(x, y)). The proof of the specification formula is

\begin{matrix}\begin{matrix}{0 = 0 & 1 = 1 \atop F actBody[F act](0, 1)} & (R1) \\ F act(0, 1) \end{matrix} ; ∃y F act(0, y) & {⋮ . [1] \atop ∀x(N(x) & ∃y F act(x, y) → ∃y F act(s_{N}x, y))} \\ ∃y F act(0, y) & ∀x(N(x) & ∃y F act(x, y) → ∃y F act(s_{N}x, y)) \end{matrix} (N5)
∀x(N(x) → ∃y F act(x, y)).

The proof [1] is

{(2) \atop N(x) & ∃w F act(x, w)} ; ∃w F act(x, w)

s_{N}x ≠ 0

{(1) \atop F act(x, w)} s_{N}x ∗ w = s_{N}x ∗ w
F act(x, w) & s_{N}x ∗ w = s_{N}x ∗ w

∃z(F act(x, z) & s_{N}x ∗ w = s_{N}x ∗ z)

s_{N}x ≠ 0 & ∃z(F act(x, z) & s_{N}x ∗ w = s_{N}x ∗ z)

F actBody[F act](s_{N}x, s_{N}x ∗ w) (R1)

F act(s_{N}x, s_{N}x ∗ w)

∃y F act(s_{N}x, y)

∃y F act(s_{N}x, y) (1)

N(x) & ∃w F act(x, w) → ∃y F act(s_{N}x, y) (2)

∀x(N(x) & ∃w F act(x, w) → ∃y F act(s_{N}x, y)).

The corresponding realizers of the proof is constructed in the following way. The part [1] of the construction is

\begin{matrix}\begin{matrix}0 & \begin{matrix}{q \atop q_{1}} ; q_{11}\{q_{10}/w\} & 0 \\ ⟨q_{11}, 0⟩ \end{matrix} ; ⟨q_{10}, ⟨q_{11}, 0⟩⟩ \\ ⟨0, ⟨q_{10}, ⟨q_{11}, 0⟩⟩⟩ \end{matrix} ; ⟨1, ⟨0, ⟨q_{10}, ⟨q_{11}, 0⟩⟩⟩⟩ & λx.x \\ ⟨1, ⟨0, ⟨q_{10}, ⟨q_{11}, 0⟩⟩⟩⟩ \end{matrix} ; ⟨s_{N}x ∗ q_{10}, ⟨1, ⟨0, ⟨q_{10}, ⟨q_{11}, 0⟩⟩⟩⟩⟩ ; λq.⟨s_{N}x ∗ q_{10}, ⟨1, ⟨0, ⟨q_{10}, ⟨q_{11}, 0⟩⟩⟩⟩⟩ ; λxq.⟨s_{N}x ∗ q_{10}, ⟨1, ⟨0, ⟨q_{10}, ⟨q_{11}, 0⟩⟩⟩⟩⟩

where {t/x} represents that a free variable x is bound to t. Let

e ≡ λxr.(μf.λx.Ex0(λr.⟨1, ⟨0, 0⟩⟩)

(λr.⟨x ∗ f(p_{0}(p_{N}x)), ⟨1, ⟨0, ⟨(f(p_{N}x))_{0}, ⟨(f(p_{N}x))_{1}, 0⟩⟩⟩⟩⟩)0)x.

Then the realizers extracted from the proof are

\begin{matrix}\begin{matrix}\begin{matrix}{0 \atop ⟨0, 0⟩} & λx.x \\ ⟨0, 0⟩ \end{matrix} ; ⟨1, ⟨0, 0⟩⟩ & {⋮ . [1] \atop λxq.⟨s_{N}x ∗ q_{10}, ⟨1, ⟨0, ⟨q_{10}, ⟨q_{11}, 0⟩⟩⟩⟩⟩} \\ ⟨⟨1, ⟨0, 0⟩⟩, λxq.⟨s_{N}x ∗ q_{10}, ⟨1, ⟨0, ⟨q_{10}, ⟨q_{11}, 0⟩⟩⟩⟩⟩⟩ \end{matrix} & λqxr.f \\ e \end{matrix}

where

λqxr.f q (N5). Since 0 q N(x), then an extracted program fact is given by

fact ≡ λx.(ex0)_{0}. By mathematical induction (N5), we can prove

∀x(N(x) → fact x = (μf.λx.Ex0(λr.1)(λr.(x ∗ f(p_{N}x)))0)x). This is an ordinary factorial program and under the condition N(x),

fact x = (μf.λx.Ex0(λr.1)(λr.(x ∗ f(p_{N}x)))0)x, fact 0 = 1, fact (s_{N}x) = x ∗ (fact x)

hold. Example 5.3.2. (Append of Lists)

We use the usual list notation here.

[] ≡ 0.
[a. b] ≡ pab.

We define lists of natural numbers as in section 2.

List(x) ≡ (μP.(x).x = [] ∨ x ≠ [] & ∃u, v(x = [u.v] & N(u) & P (v)))(x). An input output relation for inputs x, y and an output z of the append program is represented as

Append(x, y, z) ≡ (μP.(x, y, z).x = [] & y = z ∨
∃u, v, w(x = [u.v] & z = [u.w] & P (v, y, w)))(x, y, z).

The specification formula is ∀x, y(List(x) & List(y) → ∃z(Append(x, y, z) & List(z))).

This is proved by list induction on x which is discussed in section 2.

We use the following abbreviations.

List(x) ≡ μP.(x).ListBody[P](x),
ListBody[P](x) ≡ x = [] ∨ x ≠ [] & ∃u, v(x = [u.v] & N(u) & P (v)),
Append(x, y, z) ≡ μP.(x, y, z).AppBody[P](x, y, z),
AppBody[P](x, y, z) ≡ x = [] & y = z ∨ ∃u, v, w(x = [u.v] & z = [u.w] & P (v, y, w)).

The realizer of list induction, i.e., (R2) for List(x) is

L = λq.μf.λxr.qx(σ_{ListBody[P](x)}^{P,f}r),

where

σ_{ListBody[P](x)}^{P,f} = λr.⟨r_{0}, Er_{0}0(λr.0)(λr.⟨0, ⟨r_{110}, ⟨r_{1110}, ⟨0, fr_{1110}r_{11111}⟩⟩⟩⟩)r⟩.

We prove the specification formula and generate the realizer of it from the proof. Let

A(x, y) ≡ List(x) & List(y),
B(x, y, z) ≡ Append(x, y, z) & List(z),
C(x) ≡ ∀y(List(y) → ∃zB(x, y, z)),
D(x) ≡ ∃u, v(x = [u.v] & N(u) & C(v)),
E(x, u, v) ≡ x = [u.v] & N(u) & C(v).

The proof of the specification formula is the following.

\begin{aligned}{(3) \atop A(x, y)} ; List(y) & \begin{aligned}{(3) \atop A(x, y)} ; List(x) & \begin{matrix}\begin{matrix}{(2) \atop ListBody[C](x)} & {(1) \atop x = []} ; ⋮ . [1] ; C(x) & {(1) \atop x ≠ [] & D(x)} ; ⋮ . [2] ; C(x) \\ C(x) \end{matrix} ; (1) ; ListBody[C](x) → C(x) ; (2) ; ∀x(ListBody[C](x) → C(x)) & (R2) \\ ∀x(List(x) → C(x)) \end{matrix} ; List(x) → C(x) \\ & C(x) \end{aligned} ; List(y) → ∃zB(x, y, z) \\ & ∃zB(x, y, z) \end{aligned} ; A(x, y) → ∃zB(x, y, z) ; (3) ; ∀xy(A(x, y) → ∃zB(x, y, z)).

Subproof [1] is

\begin{matrix}\begin{matrix}\begin{matrix}x = [] & y = y \\ x = [] & y = y \end{matrix} ; AppBody[Append](x, y, y) & (R1) \\ Append(x, y, y) \end{matrix} & {(1) \atop List(y)} \\ B(x, y, y) \end{matrix} ; ∃zB(x, y, z) ; List(y) → ∃zB(x, y, z) ; (1) ; C(x).

Subproof [2] is

\begin{aligned}{x ≠ [] & D(x) \atop D(x)} & \begin{matrix}\begin{aligned}{(3) \atop List(y)} & {(2) \atop E(x, u, v)} ; C(v) ; List(y) → ∃zB(v, y, z) \\ & ∃zB(v, y, z) \end{aligned} & \begin{aligned}{(1) \atop B(v, y, w)} & {(2) \atop E(x, u, v)} \\ & ⋮ . [3] \end{aligned} ; ∃zB(x, y, z) \\ ∃zB(x, y, z) \end{matrix} ; (1) \\ & ∃zB(x, y, z) \end{aligned} ; (2) ; List(y) → ∃zB(x, y, z) ; (3) ; C(x).

Subproof [3] is

\begin{matrix}\begin{matrix}\begin{matrix}{E(x, u, v) \atop x = [u.v]} & [u.w] = [u.w] & {B(v, y, w) \atop Append(v, y, w)} \\ x = [u.v] & [u.w] = [u.w] & Append(v, y, w) \end{matrix} ; ∃u, v, w(x = [u.v] & [u.w] = [u.w] & Append(v, y, w)) ; AppBody[Append](x, y, [u.w]) & (R1) \\ Append(x, y, [u.w]) \end{matrix} & \begin{aligned}{E(x, u, v) \atop N(u)} & {B(v, y, w) \atop List(w)} \\ & ⋮ . [4] \end{aligned} ; List([u.w]) \\ B(x, y, [u.w]) \end{matrix} ; ∃zB(x, y, z).

Subproof [4] is

\begin{matrix}\begin{aligned}[u.w] = [] ∨ [u.w] ≠ [] & {(1) \atop [u.w] = []} ; ListBody[List]([u.w]) & \begin{matrix}{(1) \atop [u.w] ≠ []} & \begin{matrix}[u.w] = [u.w] & N(u) & List(w) \\ [u.w] = [u.w] & N(u) & List(w) \end{matrix} ; ∃u, v([u.w] = [u.v] & N(u) & List(v)) \\ [u.w] ≠ [] & ∃u, v([u.w] = [u.v] & N(u) & List(v)) \end{matrix} ; ListBody[List]([u.w]) \\ & ListBody[List]([u.w]) \end{aligned} ; (1) & (R1) \\ List([u.w]). \end{matrix}

The realizer of the specification formula is calculated from this proof in the following way where we show intermediate realizers corresponding to all the inference steps. Suppose

0 q x = [],

p q List(y),
α ≡ λyp.⟨y, ⟨⟨0, 0⟩, p⟩⟩.

Then the realizers corresponding to subproof [1] are

\begin{matrix}\begin{matrix}0 0 0 ; ⟨0, 0⟩ & λx.x \\ ⟨0, 0⟩ \end{matrix} & p \\ ⟨⟨0, 0⟩, p⟩ \end{matrix} ; ⟨y, ⟨⟨0, 0⟩, p⟩⟩ ; λp.⟨y, ⟨⟨0, 0⟩, p⟩⟩ ; α.

Suppose 0 q N(u), r q List(w),

s ≡ E[u.w][]⟨0, 0⟩⟨1, 0⟩,

δ ≡ E[u.w][]⟨0, 0⟩⟨1, ⟨0, ⟨u, ⟨w, ⟨0, r⟩⟩⟩⟩⟩.

We use

s q [u.w] = [] ∨ [u.w] ≠ [],

(Exyab)_{0} = Exya_{0}b_{0},

E(Exy01)0ab = Exyab.

Then the realizers corresponding to subproof [4] are

\begin{matrix}\begin{aligned}s & {0 \atop ⟨0, 0⟩} & \begin{matrix}0 & \begin{aligned}0 & 0 & r \\ & ⟨0, r⟩ \end{aligned} ; ⟨u, ⟨w, ⟨0, r⟩⟩⟩ \\ ⟨0, ⟨u, ⟨w, ⟨0, r⟩⟩⟩⟩ \end{matrix} ; ⟨1, ⟨0, ⟨u, ⟨w, ⟨0, r⟩⟩⟩⟩⟩ \\ & & δ \end{aligned} & λx.x \\ δ. \end{matrix}

Suppose

b q B(v, y, w),

t q E(x, u, v),

γ ≡ ⟨[u.w], ⟨⟨1, ⟨u, ⟨v, ⟨w, ⟨0, b_{0}⟩⟩⟩⟩⟩, δ[b_{1}/r]⟩⟩.

Then the realizers corresponding to subproof [3] are

\begin{matrix}\begin{matrix}\begin{aligned}{t \atop 0} & 0 & {b \atop b_{0}} \\ & ⟨0, b_{0}⟩ \end{aligned} ; ⟨u, ⟨v, ⟨w, ⟨0, b_{0}⟩⟩⟩⟩ ; ⟨1, ⟨u, ⟨v, ⟨w, ⟨0, b_{0}⟩⟩⟩⟩⟩ & λx.x \\ ⟨1, ⟨u, ⟨v, ⟨w, ⟨0, b_{0}⟩⟩⟩⟩⟩ \end{matrix} & \begin{aligned}{t \atop 0} & {b \atop b_{1}} \\ & ⋮ . [4] \end{aligned} ; δ[b_{1}/r] \\ ⟨⟨1, ⟨u, ⟨v, ⟨w, ⟨0, b_{0}⟩⟩⟩⟩⟩, δ[b_{1}/r]⟩ \end{matrix} ; γ.

In subproof [2], we use rules in which formulae are discharged. So substitutions of realizers are need to calculate the corresponding realizers to subproof [2]. We use {t/x} represents that a free variable x is bound to t in the construction of realizers. Suppose

p q List(y),

d q x ≠ [] & D(x),
β ≡ λyp.γ[(d_{1111}yp)_{1}/b, (d_{1111}yp)_{0}/w, d_{10}/u, d_{110}/v].

The realizers corresponding to [2] are

\begin{aligned}{d \atop d_{1}} & \begin{matrix}\begin{aligned}p & {d_{111}\{d_{10}/u, d_{110}/v\} \atop d_{1111}} ; d_{1111}y \\ & d_{1111}yp \end{aligned} & \begin{matrix}(d_{1111}yp)_{1}\{(d_{1111}yp)_{0}/w\} & d_{111}\{d_{10}/u, d_{110}/v\} \\ ⋮ . [3] \end{matrix} ; γ[(d_{1111}yp)_{1}/b, (d_{1111}yp)_{0}/w, d_{10}/u, d_{110}/v] \\ γ[(d_{1111}yp)_{1}/b, (d_{1111}yp)_{0}/w, d_{10}/u, d_{110}/v] \end{matrix} \\ & γ[(d_{1111}yp)_{1}/b, (d_{1111}yp)_{0}/w, d_{10}/u, d_{110}/v] \end{aligned} ; λp.γ[(d_{1111}yp)_{1}/b, (d_{1111}yp)_{0}/w, d_{10}/u, d_{110}/v] ; β.

We calculate the realizers for the whole proof. Let a q A(x, y),

d q ListBody[C](x),

and

f ≡ μf.λxr.Er_{0}0(λdyp.⟨y, ⟨⟨0, 0⟩, p⟩⟩)

(λdyp.⟨[d_{10}.(d_{1111}yp)_{0}], ⟨

⟨1, ⟨d_{10}, ⟨d_{110}, ⟨(d_{1111}yp)_{0},

⟨0, (d_{1111}yp)_{10}⟩ ⟩⟩⟩⟩, E[d_{10}.(d_{1111}yp)_{0}][]⟨0, 0⟩⟨1,

⟨0, ⟨d_{10}, ⟨(d_{1111}yp)_{0}, ⟨0, (d_{1111}yp)_{11}⟩

⟩⟩⟩

⟩⟩)(σ_{ListBody[P](x)}^{P,f}r),

e ≡ λxya.fxa_{0}ya_{1}.

Then realizers of the main proof are

\begin{aligned}{a \atop a_{1}} & \begin{aligned}{a \atop a_{0}} & \begin{matrix}\begin{matrix}q & {0 \atop ⋮ . [1]} ; α & {q_{1} \atop ⋮ . [2]} ; β \\ Eq_{0}0(λd.α)(λd.β)q_{1} \end{matrix} ; λq.Eq_{0}0(λd.α)(λd.β)q_{1} ; λxq.Eq_{0}0(λd.α)(λd.β)q_{1} & L \\ f \end{matrix} ; fx \\ & fxa_{0} \end{aligned} ; fxa_{0}y \\ & fxa_{0}ya_{1} \end{aligned} ; λa.fxa_{0}ya_{1} ; e.

List(x) is semi self-realizing. The self-realizer is j = μl.λx.Ex[](λr.⟨0, 0⟩)(λr.⟨1, ⟨0, ⟨x_{0}, ⟨x_{1}, ⟨0, lx_{1}⟩⟩⟩⟩⟩)0.

The followings hold for this self-realizer.

x ≠ [] → (jx)_{110} = x_{0},
x ≠ [] → (jx)_{1110} = x_{1},
x ≠ [] → (jx)_{11111} = jx_{1}.

We get an append program

append = λxy.(exy⟨jx, jy⟩)_{0}
= λxy.(fx(jx)y(jy))_{0}.

Unfolding and using the above facts for j,

List(y) → ∀x(ListBody[(x).(append x y = (μf.λxy.Ex[](λr.y)(λr.[x_{0} . fx_{1}y])0)xy)]

→append x y = (μf.λxy.Ex[](λr.y)(λr.[x_{0} . fx_{1}y])0)xy)

holds. From list induction,

List(y) → ∀x(List(x) → append x y = (μf.λxy.Ex[](λr.y)(λr.[x_{0} . fx_{1}y])0)xy). Then under the condition List(x) & List(y) & N(u),

append x y = (μf.λxy.Ex[](λr.y)(λr.[x_{0} . fx_{1}y])0)xy, append [] y = y, append [u. x] y = [u. (append x y)]

hold. Therefore a usual form of an append program results.

6 Concluding Remarks

In this paper, we present the theory EON + μ as a basis for program synthesis. In this theory, programs can be represented as combinatory terms which can present all partial recursive functions. Recursive concepts can be described naturally and expressively by recursively defined predicates. Program specifications are written in the form of logical formulae using this facility. We present q-realizability interpretation of this theory by which we can extract programs from proofs of specification formulae.

This method of synthesis helps theoretical approach of programming. First, we can produce programs with verification proofs of total correctness. The verification stage can be saved. Programs can be treated smoothly with verification proofs to synthesize and transform them. Second, we can consider proofs as programs. Programs can be researched by discussing their proofs.

In the future, we have two goals. First, we need develop automated theorem proving for this method of program synthesis. The theorem proving must be done by intuitionistic logic in our method. Semi-automated theorem provers with good man machine interfaces will propose refined programming environments. Second, we need programming languages which fit these logical frameworks [16].

Acknowledgements

I would like to thank Prof. Nobuo Yoneda for his suggestion and encouragement and Dr. Hayao Nakahara for invaluable discussions and proof readings. I am grateful to Prof. Masahiko Sato for his encouragement and valuable comments and Prof. Takayasu Ito for valuable comments. I also would like to thank Mr. Satoshi Kobayashi for proof readings and valuable comments, and Mr. Yukiyoshi Kameyama, Mr. Hiroyuki Sato and Mr. Hiroaki Takada for careful comments. I wish to express thanks to my wife Michiko for her mental support.

References

[1] H.P. Barendregt, The Lambda Calculus: Its Syntax and Semantics (North-Holland, Amsterdam, 1981).

[2] J.L. Bates and R.L. Constable, Proofs and Programs, ACM Trans. Prog. Lang. Syst. 7(1) (1985) 113–136.

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

[4] 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.

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

[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, Extracting Lisp programs from constructive proofs: A formal theory of constructive mathematics based on Lisp, Publ. RIMS 19 (Kyoto Univ., 1983) 169–191.

[8] S. Hayashi, PX: a system extracting programs from proofs, in: M. Wirsing, ed., Proceedings of IFIP Working Conference on Formal Description of Programming Concepts-III (North-Holland, Amsterdam, 1986).

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

[10] Z. Manna, and R. Waldinger, A deductive approach to program synthesis, ACM Trans. Prog. Lang. Syst. 2(1) (1980) 90–121.

[11] P. Martin-Löf, Hauptsatz for the intuitionistic theory of iterated inductive definitions, in: J.E. Fenstad, ed., Proceedings of the Second Scandinavian Logic Symposium (North-Holland, Amsterdam, 1971) 179–216.

[12] 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, Amsterdam, 1982) 153–179.

[13] P. Martin-Löf, Intuitionistic Type Theory (Bibliopolis, Napoli, 1984).

[14] H. Nakahara, Proofs and Programs: A naïve approach to program extraction, Ph.D. Thesis, Univ. of Tokyo, 1988.

[15] D. Prawitz, Natural Deduction (Almqvist & Wiksell, Stockholm, 1965).

[16] M. Sato, Typed Logical Calculus, Technical Report 85-13, Dept. of Information Science, Faculty of Science, Univ. of Tokyo, 1985.

[17] A. Troelstra, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, in: Lecture Notes in Mathematics 344 (Springer, Berlin, 1973).

[18] D.A. Turner, A New Implementation Technique for Applicative Languages, Software Practice and Experience 9(1) (1979) 31–49.

Contents

0 Introduction 1

1 EON + μ  5

1.1 Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.2 Logical Rules and Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

1.2.1 Logic of Partial Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.2.2 Intuitionistic Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

1.3 Non Logical Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.3.1 Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.3.2 Combinatory Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.3.3 Pairing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.3.4 Number . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 1.3.5 Decidable Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 1.3.6 Recursively Defined Predicate . . . . . . . . . . . . . . . . . . . . . . . . . 13

1.4 Computation in EON + μ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

2 Recursively Defined Predicate 21 2.1 Formula . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.2 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.3 Program Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.4 Primitive Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.5 Mutual Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.6 Data Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

2.7 Inductive Definition by Horn Clauses . . . . . . . . . . . . . . . . . . . . . . . . . 28

3 Model 30 3.1 Models of EON and EON + E . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.2 Extension of Models of EON + E . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.3 Interpretation of Recursively Defined Predicates . . . . . . . . . . . . . . . . . . 31 3.4 Soundness of EON + μ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32

4 Realizability Interpretation 34 4.1 Proof as Program . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 4.2 q-realizability Interpretation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 4.3 Soundness Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

5 Program Synthesis by q-realizability Interpretation 59 5.1 Method . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 5.2 Program Extraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 5.3 Examples of Program Synthesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

6 Concluding Remarks 72