Program Synthesis from Natural Deduction Proofs

1. Introduction

In this paper, programs on natural numbers will be treated mainly and the number theory based on intuitionistic logic is considered.

Program synthesis by theorem proving approach treats the logical formula which represents the specification of the desired program. Typical specification forms: (Manna and Waldinger [1])

Vx£Cf<">":>3zrfr<i,z>J ------<1>

Here, X is an input vector x·(xl,x2, ··. ,xm) and z is an output vector z=(zl,z2, ··· ,zn), '(x) is an input predicate and ~(x,z) is an output predicate. The aim of program synthesis is to construct a function F such that z=F(x).

The present method is based upon ~del's interpretation, which transforms (1) into (2) below: .

3zVX£<f<x> ':)'\'<x,z<x»J ------<2>

�~del's interpretation assures that there exists a term ! such that Vxlfi<xl ~'f<x,t)] holds. The term t is determined through the proof of (1) and the synthesized program can be defined as F=~x.t.

2. Logical framework

To handle logical formulas in an intuitionistic framework, a good choice is to adopt the natural deduction system, which was devised by G.Gentzen. It is mentioned in many logic

textbooks (e.g. Troelstra[4)).

Before giving ~el's theorem, several definitions are necessarily introduced, since ~del's interpretation utilizes primitive recursive functionals of finite type.

Def.l (Type)

1. Symbol 0 is a type.
2. If 6 and 't are types, then ~H.,) is also a type.

Although the same symbol "0" is used, type symbol 0 should be distinguished from natural number 0.

• Def.2 (Finite type functionals)
• EVery natural number is a functional. type 0
• If type 6 functional and type "( functional are already defined, then a type 6{~) functional is a certain map from the set
• of type ~ functionals into the set of type ~ functionals.

The set of finite type functionals is an extension of the natural number. It is necessary to extend theory to treat finite intuitionistic type functionals. number

Def.3 (System FT)

1. FT terms functionals: and primitive recursive
2. 0 (natural number) is a type 0 term.
3. ii) Each free variable of type f is a type 6
4. term.
5. iii) If f is a type 0 term and s is the successor function, then S(f) is also a type 0 term.
6. iv) If f is a type ' term and x is a bound variable of type "[, then )..xf is a type 6('t) term.
7. If f is a type ((~) term and x is a type ~term, then f(x) is a type 6 term.
8. vi) If g is a type ~term and h is a type 't(O)~) term, then p[g,h] is a type ~(0) term. f [ ] means the primitive recursion.
9. vii) A term is called a primitive recursive functional, if and only if it contains no free variables.
10. FT axioms and rules:
11. All axioms and rules except taken number theory, quantifiers, are of intuitionistic what concern the as FT axioms and
12. rules.

ii) Additional axioms and rules are: Axioms for ~(lambda)

(lxf(x)) (t)=f(t),

~xf(x} .. f,

If f and g are the same, except bound variables, then fzg,

Axioms for p[ 1

f[g,h] (O)=g,

flg,h] (S(n) )=h(n,f[g,h] (n)).

Axiom for ( )

f=g~x=y~ f(x)=g(y)

Substitution rule

Any term can be substituted for a free variable of the same type.

FT has no quantifier symbols. TO treat quantifiers, the system QFT is formulated.

Def.4 (QFT)

QFT is a quantificational extension of FT.

1) Each .formula in FT is also a formula in QFT.

2) If A(a) is a QFT formula and "a" is a free variable, then VxA(x) and 3xA(x) are also QFT formulas, where x is a bound variable of the same type as "a" and x never occurs in A(a).

QFT axioms and rules are not explicitly defined here, since they are not used in this paper.

TO each formula of intuitonistic number theory, G6del's interpretation associates a formula of the form 3x0VyA(x,y), which is called :tV-formula in QFT.

Def. 5 <W-formula)

TO each formula A in intuitioniatic number theory, a3V-formula A* in QFT is associated. The definition is by induction on the logical complexity of A.

0) If A is a prime formula, then A* is A.

From (1) to (4), it is assumed that B and c are subformulas of A and that B* and C* are already defined. B* is 3xVyB' (x,y) and C* is 3uVvc' (u,v).

1) If A is -.B, then A* is :S.zVx .. B' (x,z(x)).

For (5) and (6), it is assumed that F*(a) is :lx'dyF' (a,x,y).

6) If A is 3uF(u), then A* is 3u:\x'4yF' (u,x,y) ··

On the interpretation, the important theorem holds.

Theorem (G6del)

If a formula A \z) , containing at most z free, is provable in intuitionistic number theory and ~\1-formula A* (z) is 3xV9A' (x,y,z), then there exists a vector t of primitive recursive functionals in FT, such that A' (t(z,y),y,-z) is provable in FT.

The proof is so lengthy that it cannot be shown here (Troelstra(4]). Roughly speaking, the theorem is proved by interpreting axioms and rules of intuitionistic number theory into FT axioms and rules. For example, the induction rule (IND) in intuitionistic number theory can be interpreted in FT as follows:

It is not expedient to apply G6del's interpretation directly to a natural deduction, since it is not easy to handle the assumption dependency. The present system converts the original natural deduction proof into the LJ-like sequential form. The conversion technique is described in Gentzen(5]. For simplicity, it is assumed that neither A(O) nor A(Sa) depends on other assumptions.

If A(a) is 3z'iwB(z,w,a), then the corresponding induction rule in FT is

B(tO,w,O) B(zl,tl(a,zl,w2),a~B(t2(a,zl),w2,Sa) B(f'[t0,t2] (t) ,w,t)

other axioms and rules are interpreted similarly and GOdel's theorem can be proved by induction on the complexity of A(~) proof.

3. Synthesizer NJL

This section describes synthesizer NJL, which is a PDP-11 program written in LIPQ[3]. NJL is named after NJ (intuitionistic natural deduction) and Lisp. The rest of this paper illustrates an NJL synthesis example. GOdel's theorem is applied to program synthesis as follows:

(1) Make a logical formula expressing the specification of the desired program. Here, the "quotient remainder theorem" is taken for an example:

VxlVx2[x2f0,3zlaz2(xl=x2.zl+z2~z2<x2)], where xl is a dividend, x2 is a divider, zl is the quotient and z2 is the remainder.

(2) Prove the formula of (1) in the number theory. A brief sketch of the proof is

where Q(a,b) stands for ~zl3z2(a=b.zl+z2~z2~b). NJL is equiped with proof checking capability.

1. Convert the proof of (2) into the sequential form. This step is automatically performed in NJL system.
2. Interpret the proof of (2) into FT. First, NJL makes the corresponding 3'1 -formulas to the sequential forms of (3). For instance, formula of (1) is associated with a 3"-formula

( (E (Zl Xl X2) (Z2 Xl X2)) ( (Xl X2)

(IMP NIL (IMP (NE X2 0)

(AND (EQ Xl (+ (* X2 (Zl Xl X2)) (Z2 Xl X2) ))

(LT (Z2 Xl X2) X2) )) )) )

In NJL, formulas are expressed in prefix form, i.e. ( (E X) (A X)) for 3xA(x), ((X) (A X)) for ~xA(x) and (IMP A B) for A,B. The outer (IMP NIL A) means a sequent -+A.

Next, the applying process is for the primitive programs. desired terms are determined by G0del 1 s theorem. The determination really a proof of G0del 1 s theorem formula of (1). NJL represents recursive functionals by LISP

Def.6 (Representation in LISP)

1. The natural number 0 integer 0 in LISP. is represented by the
2. Each free variable of type 6 is represented by a variable in LISP program.
3. If f is a type 0 term and represented by f 1 in LISP, then S(f) is represented by (ADDl f 1 ) in LISP1.6 or (+ f 1 ) in LIPQ.
4. If f is a type 6 term, represented by f 1 in LISP, and x is a type L term, represented by x 1 in LISP, then Xxf is represented by (LAMBDA (X 1 ) f 1 ) in LISP.
5. If f is a type 6<'U term represented by f 1 and x is a type~ term represented by x 1 , then f(x) is represented by (f 1 x 1 ) in LISP.

6) If g is a type ~ term represented by g 1 and h is a type '1.(0) (l:) term represented by h 1 , then p[g,h] is represented by

(LABEL ROOl

(LAMBDA (X)

(COND ({ZEROP X) g 1 )

(T {hI (SUBl X) (ROOl (SUBl X)))))))

or

(DE ROOl {X)

{COND ( (ZEROP X) gIl

(T (hI (SUBl X) (ROOl (SUBl X))))))

1. Every term which contains no free variables, i.e. primitive recursive functional, is represented by a LISP program.

In this example, Zl and Z2 below are the s ynthesized programs.

(DE Zl {Xl X2)

(COND ((ZEROP Xl) 0)

{T {COND { {LT {S {Z2 {- Xl) X2)) X2) { Zl (- Xl ) X2 ) ) {T {S (Zl (- Xl) X2))) ))))

{DE Z2 {Xl X2)

(COND ({ZEROP Xl) 0)

{T {COND {(LT (S (Z2 (- Xl) X2)) X2) (S (Z2 (- Xl) X2)) ) {T 0) ) ) ) )

This ends the example.

It is well-known that corresponds to recursive Waldinger [1]). induction rule program {Manna and

4. Concluding remarks

Since GOdel 1 s interpretation utilizes the primitive recursive functional, which is an extension of the primitive recursive function on natural numbers, the synthesized program becomes necessarily total (Sato[6]).

NJL can be applied to LISP linear lists. In that case, an induction schema LS2 (McCarthy[?]) is used instead of IND.

ACKNOWLEDGEMENTS

The author wishes to express his sincere thanks to Professor M.Sato at the University of Tokyo for his kind directions and advice. He also gratefully thanks Dr. N.Ikeno and LIPQ group of Musashino Electrical Communication Laboratory for their guidance and encouragement.