Gentzen-Type Formel System Representing Properties of Function and its Implementation

1. INTRODUCTION

Many methods for proving theorems about pro­ grams have been studie<;l. ((1), (2), (6) etc.) Some of them are works on the fixed point operator (2), (15). We have tried an implementation of an automatic theorem proving system, called TKP 1 (Tsukuba-Keio Prover No.1), which is based on a Gentzen-type formal system represent­ ing the properties of functions (14). The plausi­ bility and the completeness of this system are certified by the monotonic functional interpretation (13), (14) . Moreover, the cut-elimination theorem (3) holds in this system. The basic ex­ pressions of this system are functionals and com­ position of functionals, wherein the usual logical formula is a kind of functional. Connectives be­ tween functionals are decomposed in a way similar to logical connectives. Besides, the system includes the operator for infinitary sum, from which we can apply the fixed point operator in this system. Let us consider to prove ~ f"(x)-+ G. n· CJ In this case the following sequents must be proved.

In order to prove these sequents, we may use the mathematical induction.

First, we prove F 0 (x) .. G. Next f" H (x) + G is tried to prove under the induction hypothesis f"(x) .. G.

Because TKP 1 can directly deal with the com­ position of functionals and provides a kind of facility of fixed point operator and induction, TKP 1 can efficiently process the proofs for prop­ erties of recursive programs. As TKP 1 is developed as the cut-less system, it can easily decompose a theorem to be proved into some subtheorems. And it accomplished the proofs of most problems described in (8), and moreover, acceding to user's demands, assumptions and definitions are acceptable by TKP 1, and it displays the proof-figure in a plain form after problems are proved. In section 2, we shall explain the outline of the formal system and in 3 describe the formal system. The way to prove the problem shall be explained in 4. The out­ line of implementation is given in 5. In 6 we discuss some improvements and its future applications of TKP 1.

2. OUTLINE OF FORMAL SYSTEM

Now we shall briefly explain our system, which is mainly bas'ed on 2 valued logic. The underly­ ing formal system is given in (14), and it can be interpreted by monotonic functionals. The plausi­ bility and the completeness can be certified in a way similar to (13).

Let F and G be functions of the type a .. 8 and 8 .. '( respectively. We denote the composition ofF and G by

F· G (F· G(x)=G(F(x)))

If F and G are compatible and of the same type, the join of F and G is denoted by

FVG

A formula P may have the value true (i) or false (~). Let the function~ always have the value~. and the function I the value i. Then a formula P can be considered as functions ~and I accord­ ing that they have values¢ and i respectively. And the expression P G has the value G if P is true and ~ if P is false. Let us consider the following expression

if P (x) then y else f(x) The value of this expression is y if P (x) is true, and is f(x) if P(x) is false. We can represent this by the following composition.

where P(x) denotes the negation of P(x}. Next, we conside r the program

l oop : g_p then begin H;K;goto loop end end

This can be represel1ted by

When A and B are formulas, we can consider that the composition A · B means 'A and B' , because I· I= I, I· <I>= <I>, <I> · I =<I> and <I> · <I> = <1>, The similar method concerning I and <I> is shown in (21.

Similarly the join A VB beans 'A or B', because IVI=I, IV<I>=I, <I>VI=I and <I>V<I>=<I>.

The program

will show the same result as s : = a. + ... +aN. This represented by the expression of the form

which is called a sequent. .' F + G.; means that G is an extension ofF. In the 2-valued case, for formulas A and B, 'A -· B' means that A implies B, and so is identical with A+ Bin Gentzen' s original form (3) .

Now, we shall consider th·e following recursive definition of the function F (of type a}.

It is well known that F can be defined as the least fixed point .Yo f" (¢ ) (denoted by H). if we . introduce the following function f of the type a +a (11).

On the other hand the function G of the same type as F is defined by

G(x, y} =if p(x) then y else (G(k(x), h(y}) Then we can rewrite Gas follows.

In order to prove that F is the same function as G, it is sufficient to show the following two sequents:

We shall use the first of these to illustrate the proving procedure of our theorem prover discussed in 4. As is shown in the following section, rules of inference will be given symmetrically for the left hand side and the right hand side of -+ ·

3. THE FORMAL SYSTEM

Here, we describe simply the axioms and rules of inference. The meanings of most symbols em­ ployed here have been briefly explained in the previous section. Herein we use Greek capital letters, r, 6 etc., to represent a finite set of functionals such as Fo, ..... , Fm . In Mine r's LCF system (10), 11 ," in both sides denotes the conjunction. In our system,", 11 in the left hand side of + represents the conjunction and ","in the right side denotes the disjunction. A proof-figure is a tree constructed by sequents, in which every uppermost sequent is an axiom and upper sequents and a lower sequent are connected by a rule of inference.

3. 1 Axioms

In general, various assumptions are acceptable by TKP 1 as axioms, however, we establish our system using only logical axioms as the most basic ones.

Logical axioms are sequents of the following form .

1. ~ + u, where <I> is ·the particular constant.
2. l't,F,f2+6,F,62
3. r., APt ... P B, f2 + 61, Afh ... P_.B, 62, where Pi is a formula.

3. 2 Rules of Inference

3. 2 . 1 Rules of Replacement

1. IF, Fl. <I> V F and F V <I> can be replaced by F , the converse also hold.
2. 4> F and F <I> can be replaced by <1>, the con verse also holds.
3. li and l <I> can be replaced by <I> and I respec­ tively, the converse also holds.
4. P::Q, P :::> Q, l (P·Q), l(P V Q) and ll P can be replaced by (P:::>Q)/\ (Q:::>P), lPVQ, lPVlQ lP ·lQ and P respectively, the converse also holds.
5. If <I> occurs in the left hand side of a sequent, then the left side can be replaced by~ and ~ in the right can be omitt~::J.

3. 2. 2 Rules of Inference with respect to Logical Connectives

(1) V - left

where F and G are compatible functionals.

and

(2) a - left

a - right

From the compatibility of F"(1>) and <lF, these rules of inference are reasonable.

(3) '</- left

where g is an arbitrary functional of the same type as h, and P (g/h) denotes the result obtained by replacing h for g. Moreover, we shall use the symbols y-right, 'II -left, ~-right and 3-left as follows.

1;/ - right

where f is an arbitrary free varia~le of the same type as h not contained in the lower sequent.

(4) ~- left

where f is a variable satisfying the condi­ tion in the description of v- right .

1 - right

where g is an arbitrary functional satisfy­ ing the condition in the description of 1;/ - left.

3, 2. 3 Other Rules of Inference

As the occasion demands, we can add the following practical rules.

where A 1 , ··· , Am, B1, ... , Bn are of type a+ B and F and G of typP B · r. These rule~ are easily verified.

4. PROVING PROCEDURE OF TKP 1 AND ITS EXAMPLE

In this section, we illustrate the theorem prover· based on the formal system which is described in the previous section.

4. 1 Illustrative Example

We shall illustrate the proving procedure of TKP 1 by giving the proof of the following example :

As described in thl! previous section, F and G can be defined by the series of formulas :

(4. 2)

(4. 3)

where en(~) and gn( ~) are abbreviated simply by fn and gn, respectively.

Let us illustrate how to prove

in our theorem prover. We adopt (4. 2). (4. 3), (4. 4) and (4. 5) as definitions, and the following as an assumption :

(4.1) is provided in TKP 1.

As

is not an axiom, ( 4. 7) is automatically transform­ ed to (4.8) by (4.4) and (4.5).

Then TKP 1 attempts to prove

At the same time, TKP 1 automatically generates the induction hypothesis as an assumption

In (4. 9) it is clear that f"-case is provable, so we trace the fn+1_ case.

Then we have

The p(x)·Y- case is also easily shown, because, by (4. 3),

The prover tries to prove

• (4.10-4) and the result obtained by the replace­ ment off" with g· in (4.10-4). where this re­ placement is possible according to the hypothesis (4.10). have no logical connectives and do not match to definitions and assumptions (4.1) -(4. 6) and ( 4. 1 0). Therefore TKP 1 fails to prove (4.10-4), and it must backtrack to (4. 8). Now it attempts to prove

At the same time, TKP 1 automatically generates the induction hypothesis f"(x, y) = g"(x, y) and fn+J (x,y) = g"'1 (x,y) .

The case f 0 (x,y)· v (x,y) is trivial. On the

· · a =O co other hand, the case F 1 (x, y)-+ .'£ 0 (x, y) is provable by using the assumption (4.6). Now we show below the proof of

JP(x) · h { p(k(x))·YVlP(k(x)) · g·(k (x.),

h(y))} + Jp(x) · fn+1(k(x). h(y))

t by definition ( 4. 3) and go+ 1 (x, y)

by definition (4. 2) and decomposition of

function

Jp(x) { p(k(x)) · h(y) V 'lp(k(x)) · h(g"(k 2 (x).

h(y)))

+ 1 p(x). {p(k(x)) ·h(y) V Jp(k(x)) ·

h (f"(k 2 (x), h(y)))}

by V - left, V - right and

f"(x,y) = g· (x,y)

1 p(x). p(k(x)). h(y)+'Jp(x). p(k(x))·h(y),

1 p (x) · h(g"(k 2 (x). h(y)))

(Axiom 2.)

Jp(x)· Jp(k(x))· h(g"(k2(x),h(y)))

This completes the proof of

4. 2 Application of Rules of Inference

First, TKP 1 ex<·mines whether the same expres sion exists in both sides of a sequent or not and whether an undefined element exists in the left hand side of a sequent or not. If there exists a same expression in both sides orw in the left hand side in a sequent, the sequent is provable. If a sequent is not provable and includes some logical connectives, TKP 1 transforms it according to the top level logical connectives in the left and right hand side of the sequent.

We shall show the transformation rules. In these rules the left hand side of => is a given sequent and the right hand side is transformed seque nts.

1. l (not)
2. I\ (and)

• ( 4) Implication and Equivalence

Implication and equivalence are replaced by lA VB and (A::::>B)/1. (B!:>A) respectively.

1. Decomposition of Functions

McCarthy' s conditional expression is based on the form of if- then - else, e. g. if p then e 1 ei.se-e;-. --

Such an ex pression p is called a p - type . expression. In the proving process, the following rules are applied to the expression which contains p - type expressions.

• (i) f (p) is decomposed into p
• (ii) f(p op k) and f(k op p) are decomposed respectively into p op f(k) and f(k) op p, where op is a logical connective and k is not a p - type expression.
• (iii) f(l p) is decomposed into 1 p, where p is a p- type expression.
• Undefined Element

These rules are applied in the following order.

• 1 in both side, I\ in left side, V in right side, V in left side, 1\ in right side, implication in both sides,equivalence in both sides, decomposition of function and undefined element.

4. 3 Application of Assumptions and Definitions

When a sequent can not be transformed by rules

of inference >md is not provable, TKP 1 attempts to apply assumptions and definitions which are given by the user to the sequent. In applications of assumptions and definitions, a pattern-match­ ing facility is required. In matching processes for assumptions and definitions, TKP 1 first tries to make assumptions match and then definitions afterwards. When an assumption matches two or more subexpressions of a sequent, it fin;t applies to the innermost expression contained in the left­ most term. If an assumption (or a definition) matches a subexpression, then the right part of the assumption (or the definition) is substituted for the subexpression. The prover tries to prove each new sequent. When TKP 1 can not prove any new sequent, it will try to apply the next assumption (or definition) to the old sequent. If a sequent transformed by an assumption (or a def­ inition) is the same form as a sequent which already appeared in the proving process, it is considered that the matching fails.

4.4 Induction

There are situations in which our formal system must prove the sequents including infinitary sums. Therefore TKP 1 has the procedure for a fixed point operator and mathematical induction. Olr system employs the induction with respect to the number of applications of functions. The proce­ dure of transformation of a fixed point operator is as follows. In this section ex(x) denotes an ex­ pression with subexpression x.

1. ex(<H) is transformed to ex(ro)v ex(t···), (n = 0,1,2, .. . )
2. If the prover can not prove the expression, ex(df) is transformed to ex(f 0 ) V ex(f 1 )Vex(f · · 2 ). (n = 0, 1, 2, ... )
3. The prover generates automatically the induc­ tion hypotheSiS for f n +I Or f nH tO prOVe the given proposition for all n.

The prover attempts to prove the transformed ex­ pression. If it is proved, a proof tree which denotes the proving procedure is constructed. If it fails to prove them, it automatically prints out the trial process of the proof. This output shows us what kind of assumption is required.

5. IMPLEMENTATION

5. 1 TKP 1 and KLISP

Olr program, called TKP 1, is written in KLISP (Keio LISt Processor) language which is a subset of LISP 1. 5 (g) ( 1 .) . KLISP interpre t er on TOSBAC 3400f JO (24 bits/word, 16K words) has about 4K cells of free list. As it has GLISP sys­ tem which translates programs in M - expression into S - expression, so we have written TKP 1 in M - expression.

TKP 1 consists of three phases : tmnslato'!', p'I'oVe'!' and visualize'!'. These are successively executed. Problems in input form are read by the translator of TKP 1 and are translated into inter­ nal forms which can be easily manipulated by the prover. When the prover succeeds in proving the given problems, the prover puts proof trees inS - expression form into an auxiliary memory. Finally the visualizer receives these proof trees and displays the proof figures in printed forlll.

5. 2 Input Form of TKP 1

Using the example of 4. 1, let us explain the input form of TKP 1. Inputs for TKP 1 are assumptions, definitions and a sequent to be proved. Each of assumption, definition and a sequent is called a statement, and any set of statements which contains a sequent is called a problem. In the case of the example of 4. 1, inputs for TKP 1 are as follows.

F<N + 1>(X, Y) = p(X). YV\P(x). H(F <N>

(5. 1) is a sequent to be proved. In our system "?" and "@" means o and w respectively.

$x

where x is an identifier. For example, a ·-(b + c)+ a ~ b + a ·' c is written as follows.

$A * ($ B + $C)-> $A*$ B +$A* $C

( 5. 3) and ( 5. 4) are definitions. A general form of a definition is

where r is usually f<n> (x 1, x 21 ··· , x,.) (m~O), n must be" N + i" ( i is a pos1ti ve integer) and e is an expressio11.

A definition is considered as a kind of an assump­ tion by the processor, but a formal parameter Xi needs not to be written as an arbitrary element $Xi·

5. 3 Translation and Retranslation

Translator translates ( 5. 1) and ( 5. 4) into internal forms. For example ( 5. 1) is translated to (>.'ARROW(((':' F)(= X)(= Y)))((( '~ G) (= X) (= Y)))

If the prover cannot prove a problem, no proof trees are generated. When it fails to prove the problem, the trial process to prove this is always displayed.

When a proof tree is generated, the prover con­ structs a proof tree and puts it into an auxiliary memory.

Visualizer translates this tree to a proof figure using the structure of stairs corresponding to the level of sequent in the proof tree. An example of the proof figure will be shown in the APPENDIX. The detailed grammer of the input form and trans-

6. CONCLUSIONS

Many computer programs to prove theorems about programs have been implemented((!), (6) etc.). One of the main features of our theorem prover is based on a Gentzen - type formal system. Most significant features of TKP 1 are the following : (1) Since cut operation is not required in our formal system, TKP 1 can be implemented as a fully automatic theorem prover. ( 2) The fixed point operator can be decomposed as it is a logical operator. (3) An induction hypothesis is automatically generated. (4) TKP 1 performs a part of course-of-values induction (7), A Gentzen - type theorem prover which has the facility to display proof figures is very useful to show readable and understandable proof proce­ dures. If we make an interactive theorem prover, this feature is very powerful. The other feature involves using an inductive method and fixed point theorem. Some programs using induction meth­ ods have been already studied (1) (10), in our prover, propositions to be proved are not re­ stricted by a particular programming language. Providing assumptions and definitions to this prover, results in a large generality and flexi­ bility with our program. In spite of the ability to prove all examples described in (8), our forma! system and our theorem prover are quite concise, namely, 4K cells are available for the prover and data.

Considering the facts described above, we sum­ marize here some future aspects of the study of our program and formal system.

1. The program can be extended to accept a kind of dynamic assumptions, e.g., procedu­ ral assumptions ( 4).
2. It may be anticipated that this prover should contain useful algebraic theorems, and theo­ rems which are unuseful should be automat­ ically deleted from the system. Theorems prepared should be selected ac­ cording to user's requirements.
3. We concider that our theorem prover will have more extensive applications when pro­ vided with an interactive facilities.