Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams

Makoto Tatsuta

Research Institute of Electrical Communication, Tohoku University, 2-1-1 Katahira, Sendai 980, JAPAN

                  e-mail: tatsuta@riec.tohoku.ac.jp

Abstract

The main aim of the paper is to construct a logical system in which properties of programs can be formalized for verification, synthesis and transformation of programs. The paper has 2 main points. One point is a realizability interpretation of coinductive definitions of predicates. The other point is extraction of programs which treat streams. An untyped predicative theory TID_{ν} is presented, which has the facility of coinductive definitions of predicates and is based on constructive logic. Properties defined by the greatest fixed point, such as streams and the extensional equality of streams, can be formalized by the facility of coinductive definitions of predicates in TID_{ν}. A q-realizability interpretation for TID_{ν} is defined and the soundness of the interpretation is proved. By the realizability interpretation, a program which treats streams can be extracted from a proof of its specification in TID_{ν}. General program extraction theorem and stream program extraction theorem are presented.

1 Introduction

Our main aim is to construct a logical system in which we can formalize properties of programs for verification, synthesis and transformation of programs. In the paper, we concentrate on formalization of programs with streams and present a theory TID_{ν}.

Coinductive definitions are very important for this purpose. Properties of streams are represented semantically by the greatest fixed point. The predicate representing what a stream is and the extensional equality of streams are defined semantically by the greatest fixed point. These properties defined by the greatest fixed point can be formalized by coinductively defined predicates and coinduction.

μ-calculus has been studied to formalize programs with streams for verification [3]. μ-calculus has the facility of coinductive definitions of predicates and coinduction and is based on classical logic.

In the paper, we present the theory TID_{ν}, which has the facility of coinductive definitions of predicates and coinduction and is based on constructive logic. By these facilities we can formalize properties of programs with streams in TID_{ν}.

Our theory TID_{ν} is based on constructive logic because we want to use the facility of program extraction by realizability for TID_{ν}. Program extraction is one of the benefits we get when we use a constructive formal theory to formalize properties of programs. Program extraction is to get a program from a constructive proof of its specification formula. One method of program extraction is to use a realizability interpretation. In PX[4], for example, a LISP program is extracted from a proof of its specification formula by a realizability interpretation.

By the facility of coinductive definitions of predicates and a realizability interpretation, we can synthesize programs with streams naturally in TID_{ν} using theorem proving techniques.

The paper has 2 main points. One point is a realizability interpretation of coinductive definitions. The other point is extraction of programs with streams.

We present the untyped predicative theory TID_{ν}, which has coinductive definitions of predicates and is based on constructive logic. We define a q-realizability interpretation for TID_{ν}. We show that the realizability interpretation is sound. We present general program extraction theorem and stream program extraction theorem.

The soundness theorem was proved also in [5]. Both works are independent.

In Section 2, we define the theory TID_{ν}. In Section 3, we briefly explain how useful the facility of coinductive definitions of predicates is to formalize streams. In Section 4, we discuss models of TID_{ν} and prove its consistency. In Section 5, we present the q-realizability interpretation for TID_{ν} and prove the soundness theorem. In Section 6, we give general program extraction theorem, stream program extraction theorem for TID_{ν} and an example of program synthesis.

2 Theory TID_{ν}

We present the theory TID_{ν} in this section. It is the same as Beeson’s EON [1] except for the axioms of coinductive definitions of predicates.

In the paper, we choose λ-calculus with pairing and natural numbers as the target programming language for simplicity since we want to concentrate on the topic of coinductive definitions of predicates. We suppose that the evaluation strategy of terms is lazy or call-by-name because we represent a stream by an infinite list, which is a non-terminating term. We omit also the formalization of the lazy or call-by-name evaluation strategy in TID_{ν} for simplicity.

Definition 2.1. (Language of TID_{ν})

The language of TID_{ν} is based on a first order language and λ-calculus but extended for coinductive definitions of predicates.

The constants are:

p, p_{0}, p_{1}, 0, s_{N}, p_{N}, d. We choose λ-calculus with pairing and natural numbers as the target programming language

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

We have only one function symbol:

App whose arity is 2. It means a functional application of terms.

Terms t are defined as follows:

t ::= x|c|App(t, t)|λx.t where x stands for a variable and c stands for a constant.

For terms s, t, we abbreviate App(s, t) as st. For terms s, t, we also use abbreviations ⟨s, t⟩ ≡ pst, t_{0} ≡ p_{0}t and t_{1} ≡ p_{1}t. ⟨x_{0},…, x_{n}⟩ denotes ⟨x_{0}, ⟨… ⟨x_{n−1}, x_{n}⟩…⟩⟩.

The predicate symbols are:

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

b.

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

X, Y, Z,…, X^{∗}, Y^{∗}, Z^{∗},….

Each predicate variable has a fixed arity.

We abbreviate Y(λx.t) as μx.t where Y ≡ λf.(λx.f(xx))(λx.f(xx)).

Definition 2.2. (Formula)

We define a formula A, a set S_{+}(A) of predicate variables which occur positively in A and a set S_{−}(A) of predicate variables which occur negatively in A.

1. If a, b are terms,

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

S_{+}(⊥) = S_{−}(⊥) = ϕ, S_{+}(N(a)) = S_{−}(N(a)) = ϕ, S_{+}(a = b) = S_{−}(a = b) = ϕ.

2. If X is a predicate variable whose arity is n and t_{1},…, t_{n} are terms, X(t_{1},…, t_{n}) is a formula

and S_{+}(X(t_{1},…, t_{n})) = {X}, S_{−}(X(t_{1},…, t_{n})) = ϕ.

3. A & B, A ∨ B, A → B, ∀xA, ∃xA are formulas if A and B are formulas in the same way as a

first order language. Then S_{+}(A & B) = S_{+}(A ∨ B) = S_{+}(A) ∪ S_{+}(B), S_{−}(A & B) = S_{−}(A ∨ B) = S_{−}(A) ∪ S_{−}(B), S_{+}(A → B) = S_{−}(A) ∪ S_{+}(B), S_{−}(A → B) = S_{+}(A) ∪ S_{−}(B), S_{+}(∀xA) = S_{+}(∃xA) = S_{+}(A), S_{−}(∀xA) = S_{−}(∃xA) = S_{−}(A).

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

A is a formula, t_{1},…, t_{n} are terms and X is not in S_{−}(A). Then S_{+}((νX.λx_{1} … x_{n}.A)(t_{1},…, t_{n})) = S_{+}(A) − {X}, S_{−}((νX.λx_{1} … x_{n}.A)(t_{1},…, t_{n})) = S_{−}(A).

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

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

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

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

Example 2.3.

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

(νP.λx.x = ⟨x_{0}, x_{1}⟩ & x_{0} = 0 & P (x_{1}))(x) is a formula.

Among many axioms and inference rules of TID_{ν}, we discuss only axioms of coinductive definitions of predicates here. The rest of axioms and inference rules are almost the same as EON [1] and we only list them in Appendix A.

Definition 2.4. (Coinductive Definitions)

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

We have the following axioms:

∀x(ν(x) → A(ν)),  (ν1)
∀x(C(x) → A(C)) → ∀x(C(x) → ν(x)).  (ν2)

νP.λx.A(P) means the greatest fixed point of the function from a predicate P to a predicate λx.A(P).

We define a theory TID^{−} as the theory TID_{ν} except that the theory TID^{−} does not have the two axioms (ν1) and (ν2) of coinductive definitions of predicates.

3 Coinductive Definitions of Predicates

We explain coinductive definitions of TID_{ν} and show some examples of formalization of streams by coinductive definitions.

Proposition 3.1.

Let ν be νX.λx.A(X). Then

∀x(ν(x) ↔ A(ν))  (ν1′)

holds.

Proof 3.2.

By (ν1), we get ν(x) → A(ν). By letting C be λx.A(ν) in (ν2), A(ν) → ν(x) holds. □

This proposition shows that νP.λx.A(P) is the solution of the following recursive equation of a predicate P:

P (x) ↔ A(P). The axiom (ν2) says that νP.λx.A(P) is the greatest solution of this equation or the greatest fixed point of the function λP.λx.A(P).

Streams can be formalized by coinductive definitions [3]. Therefore we can formalize streams in TID_{ν}.

We represent a stream by an infinite list ⟨a, s⟩ constructed by pairing where a is the first element of the stream, s is the rest of the stream. In this representation, if s is a stream, we can get the first element of s by s_{0} and the rest by s_{1}.

We present an example of bit streams. A bit stream is a stream whose elements are 0 or 1. We will define a predicate BS(x) which means that x is a bit stream. When we write down a formula BS(x) in a naive way, BS itself occurs in the body of the definition as follows:

BS(x) ↔ x = ⟨x_{0}, x_{1}⟩ & (x_{0} = 0 ∨ x_{0} = 1) & BS(x_{1}). BS is a solution P of the following equation for a predicate P

P (x) ↔ x = ⟨x_{0}, x_{1}⟩ & (x_{0} = 0 ∨ x_{0} = 1) & P (x_{1}) (1)

or a fixed point of the function

λP.λx.x = ⟨x_{0}, x_{1}⟩ & (x_{0} = 0 ∨ x_{0} = 1) & P (x_{1}). (2)

There may be many solutions P for (1). For example, λx.⊥ is one solution of (1), though it is not our intended solution. λx.⊥ is the least solution. Our intended solution is the greatest solution of (1) or the greatest fixed point of (2). Hence we have the solution in TID_{ν} and it is represented as follows:

BS ≡ νP.λx.x = ⟨x_{0}, x_{1}⟩ & (x_{0} = 0 ∨ x_{0} = 1) & P (x_{1}). Let \overline{0} be μs.⟨0, s⟩. \overline{0} represents the zero stream whose elements are all 0. We can show BS(\overline{0})

by the coinduction axiom (ν2). Let C be λx.(x = \overline{0}) in (ν2), then we have

∀x(x = \overline{0} → x = ⟨x_{0}, x_{1}⟩ & (x_{0} = 0 ∨ x_{0} = 1) & x_{1} = \overline{0}) → ∀x(x = \overline{0} → BS(x)). By definition of \overline{0},

∀x(x = \overline{0} → x = ⟨x_{0}, x_{1}⟩ & (x_{0} = 0 ∨ x_{0} = 1) & x_{1} = \overline{0}) holds and we have

∀x(x = \overline{0} → BS(x)). Let x = \overline{0} then we get BS(\overline{0}).

The coinductive definitions of predicates play an important role also to represent predicates which describe properties of streams [3, 6]. We will define the extensional equality s ≈ t for streams s and t. This equality can be represented by the coinductive definitions of predicates. The relation ≈ is the greatest solution of the following equation for a predicate P:

P (x, y) ↔ x_{0} = y_{0} & P (x_{1}, y_{1}). Therefore the relation ≈ can be formalized in TID_{ν} as follows:

≈ ≡ νP.λxy.x_{0} = y_{0} & P (x_{1}, y_{1}).

4 Models of TID_{ν}

We will briefly explain semantics of TID_{ν} by giving its intended model.

We will use classical set theory and the well-known greatest fixed point theorem for model construction in this section.

Theorem 4.1. (Greatest Fixed Point)

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

1. f(a) = a,

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

a is abbreviated as gfp(f).

We will construct a model M′ of TID_{ν} extending an arbitrary model M of TID^{−}. Our intended model of TID^{−} is the closed total term model whose universe is the set of closed terms [1]. We denote the universe by U.

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

Define F as follows:

|x| = n,

F : p(U^{n}) → p(U^{n}),

F (X) = {x ∈ U^{n} | ρ[P := X] ⊧ A(P)}, where ρ[P := X] is defined as follows:

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

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

Then ρ ⊧ (νP.λx.A(P))(t) is defined as t ∈ gfp(F). Note that F is monotone since a predicate variable P occurs only positively in A(P).

Theorem 4.2.

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

Theorem 4.3.

TID_{ν} is consistent.

5 q-realizability Interpretation for TID_{ν}

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

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

Our realizability in the paper is an extension of Grayson’s realizability. We can also define usual Kleene style q-realizability of coinductively defined predicates in the same way as in the paper.

Definition 5.1. (Harrop formula)

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

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

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

Definition 5.2. (Abstract)

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

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

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

4. If (νX.λx_{1} … x_{n}.A)(x_{1},…, x_{n}) is a formula, νX.λx_{1} … x_{n}.A is an abstract of arity n.

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

Definition 5.3. (q-realizability Interpretation)

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

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

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

1. (e q′ A) ≡ e = 0 & AP[F] where A is Harrop.

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

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

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

5. (e q′ A ∨ B) ≡ N(e_{0}) & (e_{0} = 0 → (e_{1} q′ A)) & (e_{0} ≠ 0 → (e_{1} q′ B)).

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

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

8. (e q′ ∃xA(x)) ≡ (e_{1} q′ A(e_{0})).

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

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

Proposition 5.4.

Let ν ≡ νP.λx.A(P).

1. ∀xr((r q ν(x)) ↔ (r q A(ν))).

2. (λxr.r q ∀x(ν(x) → A(ν))) holds if A(X) is not Harrop. (0 q ∀x(ν(x) → A(ν))) holds if A(X) is Harrop.

Proof 5.5.

By the definition of q-realizability and (ν1′). □

Definition 5.6.

For a formula A, a predicate variable P and a term f, we define a term σ_{A}^{P,f} by induction on the construction of A as follows:

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

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}, dr_{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}(r(σ_{A_{1}}^{P,f}q)).

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})(t), then σ_{A}^{P,f} ≡ (μg.λxr.σ_{A_{1}}^{Q,g}(σ_{A_{1}}^{P,f}r))t where Q ≢ P.

Proposition 5.7.

Let ν ≡ νP.λx.A(P). If ν(x) is not Harrop,

λq.μf.λxr.σ_{A(P)}^{P,f}(qxr) q ∀x(C(x) → A(C)) → ∀x(C(x) → ν(x)) holds. If ν(x) is Harrop,

0 q ∀x(C(x) → A(C)) → ∀x(C(x) → ν(x)) holds.

We prove it in Appendix B.

Theorem 5.8. (Soundness Theorem)

If TID_{ν} ⊢ A, we can get a term e from the proof of ⊢ A and TID_{ν} ⊢ (e q A) holds where all the free variables of e are included in all the free variables of A.

Proof 5.9.

By induction on the proof of ⊢ A. The case of the axiom (ν1) is proved by Proposition 5.4. The case of the axiom (ν2) is proved by Proposition 5.7. □

6 Program Synthesis with Streams

In this section, we give general program extraction theorem, stream program extraction theorem for TID_{ν} and an example of program synthesis.

Program synthesis by theorem proving techniques has been studied both in typed theories [2] and untyped theories [4]. For untyped theories, realizability interpretations are used as the foundations of program synthesis by theorem proving techniques. In Section 3, we showed that streams and programs which treat streams can be formalized in TID_{ν} by the facility of coinductive definitions of predicates. In Section 5, we showed that the realizability interpretation can be defined for TID_{ν} and the interpretation is sound. Hence we can synthesize programs which treat streams by theorem proving techniques in TID_{ν} using the realizability interpretation.

We represent streams by infinite lists constructed by pairing. We represent a specification of a program by a formula:

∀x(A(x) → ∃yB(x, y)) where x is an input, y is an output, A(x) is an input condition and B(x, y) is an input output relation.

Theorem 6.1. (Program Extraction)

Suppose that we prove a specification formula ∀x(A(x) → ∃yB(x, y)) of a program in TID_{ν} and we have a realizer j such that

∀x(A(x) → (jx q A(x))). Then we can get a program f and a proof of

∀x(A(x) → B(x, fx)) effectively from the proof of the specification formula.

Proof 6.2.

Since the specification formula is proved in TID_{ν}, by the soundness theorem (Theorem 5.8) of the q-realizability interpretation we have a realizer e such that

e q ∀x(A(x) → ∃yB(x, y)) holds. Let f be λx.(ex(jx))_{0}. Then the claim holds. □

We can synthesize a program in the following steps:

1. We write down a specification formula.

2. We prove the specification formula in TID_{ν}.

3. We extract a program from the proof.

The program extraction theorem says that the third step can be automated completely.

Example 6.3.

We show an example of the program which gets a stream of natural numbers and returns a stream whose each element is the element of the input stream plus one.

The predicate NS(x) which says that x is a stream of natural numbers can be represented in TID_{ν} by the facility of coinductive definitions of predicates as follows:

NS ≡ νX.λx.x = ⟨x_{0}, x_{1}⟩ & N(x_{0}) & X(x_{1}). The input condition of the specification is the formula NS(x).

The input output relation of the specification is the formula ADD1(x, y) which is defined as follows:

ADD1 ≡ νX.λxy.y_{0} = x_{0} + 1 & X(x_{1}, y_{1}). The specification formula is:

∀x(NS(x) → ∃yADD1(x, y)).

We have one problem for this program synthesis method. The coinduction cannot be applied to the part ∀x(NS(x)→…) in the above example. We cannot prove ∃yADD1(x, y) by the coinduction in general. Therefore the realizer of the coinduction cannot give a loop structure to the program. On the other hand, the realizer of the induction principle plays an important role for this approach of program synthesis since the realizer corresponds to a loop structure of a program [4, 7]. Therefore we need a new method by which the realizer of the coinduction also corresponds to a loop structure and is useful.

Then we need a more specialized program extraction method for programs with streams by which the coinduction is useful. We give one solution for this problem by the next theorem.

Let nthcdr ≡ μf.λnx.dn0x(f(p_{N}n)(p_{1}x)). nthcdr is the same function as in LISP.

We put two restrictions on the theorem: Let p be a term such that px = nthcdr nx for some n depending on x_{0}. One is that the input condition A(x) must be of the form (νX.λx.x = ⟨x_{0}, x_{1}⟩ & Ã(x_{0}) & X(px))(x) for some Ã. The other is that the input output relation B(x, y) must be the form (νX.λxy.B̃(x, y_{0}) & X(px, y_{1}))(x, y) for some B̃. These restrictions require that the input condition and the input output relation are uniform over data and they are natural when we suppose that the input x and the output y are both streams.

Theorem 6.4. (Stream Program Extraction)

Let nthcdr ≡ μf.λnx.dn0x(f(p_{N}n)x_{1}).

Suppose that the specification formula is ∀x(A(x) → ∃yB(x, y)), A ≡ νX.λx.x = ⟨x_{0}, x_{1}⟩ & Ã(x_{0}) & X(px),

B ≡ νX.λxy.B̃(x, y_{0}) & X(px, y_{1}),

p ≡ λx.nthcdr(nx_{0})x for some formulas Ã(x) and B̃(x, y) and some term n such that

∀x(Ã(x) → N(nx)) holds and we have a term j such that ∀x(A(x) → (jx q A(x))). Then we define

B^{∘} ≡ νX.λx.∃zB̃(x, z) & X(px). If we have e such that

e q ∀x(A(x) → B^{∘}(x)), we can get a term F such that

∀x(A(x) → B(x, F x)) where

filter ≡ μf.λx.⟨x_{00}, fx_{1}⟩, F ≡ λx.filter(ex(jx)).

We prove it in Appendix C.

By this theorem, we can synthesize a program in the following steps:

1. We write down a specification formula ∀x(A(x) → ∃yB(x, y)).

2. We prove the corresponding formula ∀x(A(x) → B^{∘}(x)) in TID_{ν}.

3. We extract a program λx.filter(ex(jx)) from the proof where e is a realizer of the corresponding formula ∀x(A(x) → B^{∘}(x)).

In the second step, we can apply the coinduction to prove the part B^{∘}(x) since B^{∘}(x) is defined by coinductive definitions. Therefore the realizer of the coinduction can give a loop structure to the program.

Example 6.5.

We treat the same example as Example 6.3 again. The specification formula is the formula ∀x(NS(x) → ∃yADD1(x, y)). Let a term n be λx.1 in Theorem 6.4. Then px = x_{1}. Hence the formula ADD1^{∘}(x) is:

ADD1^{∘} ≡ νX.λx.∃z(z = x_{0} + 1) & X(x_{1}). (3)

Therefore the corresponding formula we must prove is:

∀x(NS(x) → ADD1^{∘}(x)). (4)

If we prove this formula in TID_{ν}, we can get a program which satisfies the specification by the stream program extraction theorem.

The conditions of the theorem hold for this case. We can put j ≡ λx.μs.⟨0, s⟩ since

∀x(NS(x) → (μs.⟨0, s⟩ q NS(x))). We prove (4) in the following way here: Firstly, we prove

∀x(NS(x) → ∃z(z = x_{0} + 1) & NS(x_{1})). (5)

This is proved by letting z be x_{0} + 1. Secondly, by letting C be NS in (ν2) for ADD1^{∘}, we have

∀x(NS(x) → ∃z(z = x_{0} + 1) & NS(x_{1})) → ∀x(NS(x) → ADD1^{∘}(x)). (6)

Finally, by (5) and (6), we get (4).

We calculate realizers corresponding to the above proofs as follows: The realizer e_{1} corresponding to the proof of (5) is:

e_{1} ≡ λxr.⟨⟨x_{0} + 1, 0⟩, r_{11}⟩,

e_{1} q ∀x(NS(x) → ∃z(z = x_{0} + 1) & NS(x_{1})).

The realizer e_{2} corresponding to the proof of (6) is:

e_{2} ≡ λq.μf.λxr.σ(qxr),

e_{2} q ∀x(NS(x) → ∃z(z = x_{0} + 1) & NS(x_{1})) → ∀x(NS(x) → ADD1^{∘}(x))

where

σ ≡ λr.⟨⟨r_{00}, r_{01}⟩, fx_{1}r_{1}⟩.

The realizer e corresponding to the proof of (4) is:

e ≡ e_{2}e_{1},

e q ∀x(NS(x) → ADD1^{∘}(x)).

We get

e = μf.λxr.⟨⟨x_{0} + 1, 0⟩, fx_{1}r_{11}⟩.

The extracted program F is:

F x = filter(ex(jx))
= filter(fx(μs.⟨0, s⟩))

where f ≡ μf.λxr.⟨⟨x_{0} + 1, 0⟩, fx_{1}r_{11}⟩. Then we have F x = (μg.λx.⟨x_{0} + 1, gx_{1}⟩)x. This is the program we expect. Remark that the realizer e_{2} of the coinduction (6) gives the loop structure to the program F.

Acknowledgements

I’m deeply grateful to Professor Masahiko Sato for invaluable discussions and comments. I would like to thank Mr. Satoshi Kobayashi and Mr. Yukiyoshi Kameyama for careful comments.

References

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

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

[3] P. Dybjer and H.P. Sander, A Functional Programming Approach to the Specification and Verification of Concurrent Systems, Formal Aspects of Computing 1 (1989) 303–319.

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

[5] S. Kobayashi, Inductive/Coinductive Definitions and Their Realizability Interpretation, Manuscript (1991).

[6] R. Milner, Communication and Concurrency (Prentice Hall, 1989).

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

[8] M. Tatsuta, Monotone Recursive Definition of Predicates and Its Realizability Interpretation, Proceedings of Theoretical Aspects of Computer Software, LNCS 526 (1991) 38–52.

Appendix

A Axioms and Inference Rules of TID_{ν}

The logical axioms and inference rules are the same as those of usual intuitionistic logic.

Axioms for Equality:

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

Axiom for β-conversion:

(λx.a)b = a[x := b]  (B1)

where a[x := b] means a term obtained from a by replacing every free occurrence of x by b.

Axioms for Pairing:

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

Axioms for Natural Numbers:

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

Axioms for d:

∀x, y, a, b(N(x) & N(y) & x = y → dxyab = a),  (D1)
∀x, y, a, b(N(x) & N(y) & x ≠ y → dxyab = b).  (D2)

B Proof of Soundness Theorem

Lemma B.1.

Let G̃^{f} be λyx.∃r(y = fxr & G(r, x)) for an abstract G and a term f and q′ be q_{P_{1},...,P_{n}}[F_{1}, G_{1},…, F_{n}, G_{n}].

(1) If a predicate variable P occurs only positively in a formula A, (r q′_{P} [F, G] A) → (σ_{A}^{P,f}r q′_{P} [F, G̃^{f}] A).

(2) If a predicate variable P occurs only negatively in a formula A, (r q′_{P} [F, G̃^{f}] A) → (σ_{A}^{P,f}r q′_{P} [F, G] A).

Proof B.2.

We suppose that the arity of P is 1 in the proof for simplicity. We will prove (1) and (2) simultaneously by induction on the construction of A. We will show

only some cases, for other cases are proved similarly.

Case A Harrop.

(1) The claim holds since it is r = 0 & A → (λr.r)r = 0 & A.

(2) similar to (1). Case A ≡ P (t).

(1) The claim is F (t) & G(r, t) → F (t) & G̃^{f}((λr.ftr)r, t). Since we have G̃^{f}((λr.ftr)r, t) ↔ ∃s(ftr = fts & G(s, t)), the claim holds by putting s := r.

(2) This case does not exist because P occurs positively in P (t). Case A ≡ ν(t) where ν ≡ νQ.λx.B(P, Q). Let

ν^{∗} ≡ νQ^{∗}.λrx.(r q′_{P,Q}[F, G, ν_{P} [F], Q^{∗}] B(P, Q)),

ν_{1}^{∗} ≡ νQ^{∗}.λrx.(r q′_{P,Q}[F, G̃^{f}, ν_{P} [F], Q^{∗}] B(P, Q)),

g ≡ μg.λxr.σ_{B(P,Q)}^{Q,g}(σ_{B(P,Q)}^{P,f}r).

We will show ν^{∗}(r, x) → ν_{1}^{∗}(σ_{ν(x)}^{P,f}r, x). By using only rules of NJ, it is equivalent to

∀rx(ν^{∗}(r, x) → ν_{1}^{∗}(σ_{ν(x)}^{P,f}r, x)),

∀rxy(y = σ_{ν(x)}^{P,f}r & ν^{∗}(r, x) → ν_{1}^{∗}(y, x)) and

∀xy(∃r(y = σ_{ν(x)}^{P,f}r & ν^{∗}(r, x)) → ν_{1}^{∗}(y, x)). By (ν2), it is sufficient to show

∀xy(∃r(y = σ_{ν(x)}^{P,f}r & ν^{∗}(r, x)) → (y q′_{P,Q}[F, G̃^{f}, ν_{P} [F], λyx.∃r(y = σ_{ν(x)}^{P,f}r & ν^{∗}(r, x))] B(P, Q)). By using only rules of NJ, it is equivalent to

∀xyr(y = σ_{ν(x)}^{P,f}r & ν^{∗}(r, x) → (y q′_{P,Q}[F, G̃^{f}, ν_{P} [F], λyx.∃r(y = σ_{ν(x)}^{P,f}r & ν^{∗}(r, x))] B(P, Q)) and

∀xr(ν^{∗}(r, x) → (σ_{ν(x)}^{P,f}r q′_{P,Q}[F, G̃^{f}, ν_{P} [F], λyx.∃r(y = σ_{ν(x)}^{P,f}r & ν^{∗}(r, x))] B(P, Q)). (7)

We will show it. Fix x and r. Assume ν^{∗}(r, x). By (ν2) and ν^{∗}(r, x), we have

r q′_{P,Q}[F, G, ν_{P} [F], ν^{∗}] B(P, Q). By the induction hypothesis for B(P, Q), we get

σ_{B(P,Q)}^{P,f}r q′_{P,Q}[F, G̃^{f}, ν_{P} [F], ν^{∗}] B(P, Q). Using the induction hypothesis for B(P, Q) again, we have

σ_{B(P,Q)}^{Q,g}(σ_{B(P,Q)}^{P,f}r) q′_{P,Q}[F, G̃^{f}, ν_{P} [F], ν̃^{∗}^{g}] B(P, Q).

By σ_{ν(x)}^{P,f} ≡ gx, ν̃^{∗}^{g} ≡ λyx.∃r(y = σ_{ν(x)}^{P,f}r & ν^{∗}(r, x)) holds. By σ_{B(P,Q)}^{Q,g}(σ_{B(P,Q)}^{P,f}r) = σ_{ν(x)}^{P,f}r,

σ_{ν(x)}^{P,f}r q′_{P,Q}[F, G̃^{f}, ν_{P} [F], λyx.∃r(y = σ_{ν(x)}^{P,f}r & ν^{∗}(r, x))] B(P, Q) holds and we get the claim (7).

(2) similar to (1). □

Proof B.3. (of Proposition 5.7)

Suppose that ν(x) is not Harrop. Let ν ≡ νP.λx.A(P). Assume

q q ∀x(C(x) → A(C)) and let

f ≡ μf.λxr.σ_{A(P)}^{P,f}(qxr). We will show

f q ∀x(C(x) → ν(x)). Let ν^{∗}(r, x) ≡ (r q ν(x)). It is sufficient to show

∀xr((r q C(x)) → ν^{∗}(fxr, x)). This is equivalent to

∀xy(∃r((r q C(x)) & y = fxr) → ν^{∗}(y, x)).

By (ν2), it is sufficient to show

∀xy(∃r((r q C(x)) & y = fxr) → (y q_{P} [ν, λyx.∃r((r q C(x)) & y = fxr)] A(P))). This is equivalent to

∀xr((r q C(x)) → (fxr q_{P} [ν, λyx.∃r((r q C(x)) & y = fxr)] A(P))). (8)

Fix x and r and assume

r q C(x). We will show

fxr q_{P} [ν, λyx.∃r((r q C(x)) & y = fxr)] A(P). (9)

By the assumption about q,

qxr q A(C). Hence

qxr q_{P} [C, λyx.(y q C(x))] A(P). By positivity and ∀x(C(x) → ν(x)),

qxr q_{P} [ν, λyx.(y q C(x))] A(P). By letting G := λyx.(y q C(x)) in Lemma B.1,

σ_{A(P)}^{P,f}(qxr) q_{P} [ν, λyx.∃r((r q C(x)) & y = fxr)] A(P).

By fxr = σ_{A(P)}^{P,f}(qxr), we have

fxr q_{P} [ν, λyx.∃r((r q C(x)) & y = fxr)] A(P). Then (9) holds. Hence (8) holds. □

C Proof of Stream Extraction Theorem

Lemma C.1.

Suppose that ∀x(Ã(x) → N(nx)), p ≡ λx.nthcdr(nx_{0})x, A ≡ νX.λx.x = ⟨x_{0}, x_{1}⟩ & Ã(x_{0}) & X(px),

B ≡ νX.λxy.B̃(x, y_{0}) & X(px, y_{1}),

B^{∘} ≡ νX.λx.∃zB̃(x, z) & X(px). Then

∀f(∀x(A(x) → (fx q B^{∘}(x))) → ∀x(A(x) → B(x, filter(fx)))) holds.

Proof C.2.

By using only rules of NJ, the above goal is equivalent to

∀xy(∃f(∀x(A(x) → (fx q B^{∘}(x))) & A(x) & y = filter(fx)) → B(x, y)). By (ν2), it is sufficient to show

∀xy(∃f(∀x(A(x) → (fx q B^{∘}(x))) & A(x) & y = filter(fx)) →

B̃(x, y_{0}) & ∃g(∀x(A(x) → (gx q B^{∘}(x))) & A(px) & y_{1} = filter(g(px)))).

By using only rules of NJ, it is equivalent to ∀xf(∀x(A(x) → (fx q B^{∘}(x)) & A(x) →

B̃(x, (filter(fx))_{0}) & ∃g(∀x(A(x) → (gx q B^{∘}(x))) &

A(px) & (filter(fx))_{1} = filter(g(px)))). (10)

We will prove it. Fix x and f and assume that

∀x(A(x) → (fx q B^{∘}(x)),  (11)
A(x).  (12)

By (11) and (12), (fx q B^{∘}(x)) holds. Hence

((fx)_{01} q B̃(x, (fx)_{00})) & ((fx)_{1} q B^{∘}(px)) (13) holds. Therefore B̃(x, (filter(fx))_{0}) holds since (filter(fx))_{0} = (fx)_{00}.

Put g ≡ λy.(f⟨x_{0},…, x_{nx_{0}−1}, y⟩)_{1}. We will show ∀y(A(y) → (gy q B^{∘}(y))). Fix y and assume that A(y). By the definition of A and p⟨x_{0},…, x_{nx_{0}−1}, y⟩ = y,

A(x) ↔ x = ⟨x_{0}, x_{1}⟩ & Ã(x_{0}) & A(px) and

A(⟨x_{0},…, x_{nx_{0}−1}, y⟩) ↔ Ã(x_{0}) & A(y)

hold. By this and (12), Ã(x_{0}) holds. Hence A(⟨x_{0},…, x_{nx_{0}−1}, y⟩) holds. Combining it with (11), we get (f⟨x_{0},…, x_{nx_{0}−1}, y⟩ q B^{∘}(⟨x_{0},…, x_{nx_{0}−1}, y⟩)). Hence ((f⟨x_{0},…, x_{nx_{0}−1}, y⟩)_{1} q B^{∘}(y)) and (gy q B^{∘}(y)) hold. Therefore we get ∀y(A(y) → (gy q B^{∘}(y))).

By (12), A(px) holds. Since, in general, (filter(s))_{1} = filter(s_{1}) holds, we get (filter(fx))_{1} = filter((fx)_{1}) = filter(g(px)). Therefore (10) holds. □

Proof C.3. (of Theorem 6.4)

By the assumptions and the definition of q-realizability, ∀x(A(x) → (ex(jx) q B^{∘}(x))) holds. Letting f be λx.ex(jx) in Lemma C.1, we get ∀x(A(x) → B(x, F x)). □