Commenting Proofs

1. Introduction

This paper constitutes a summary of a sem­ inar entitled "Commenting Proofs" given at the Artificial Intelligence Laboratory at M. I. T. during the spring of 1974. The seminar was con­ cerned with new syntactical structures in formal proofs which deri ve from their pragmatic and semantic aspects. These structures can be used to provide a semantical interpretation for proofs quite distinct from that of Model Theory and rather more akin to the construction semantics for Intuitionistic Peano Arithmetic developed by K. Godel and the A. L procedural interpretation of the logical connectives and quantifiers a la C. Hewit's Planner Language. The work is act­ ually a synthesis of elements from Yessenin­ Volpin's foundational studies (1) and G. Sussman's work on building a "causal" history of a compu­ tation from the comments of the corresponding documented program (2 ).

For the most part we shall restrict our­ selves to the context of Peano Arithmetic and the primative recuresive arithmetic of addition, multiplication and exponentiation in particular. At the end of this report a few remarks will be made on how these ideas are extended to a richer deductive environment.

In our work we distinguish between formal proofs (a sequence of sentences satisfying the usual syntactic criteria) and "real "proofs (a formal proof constructed by someone in accord­ ance with a motivational system of goals). In the latter case each line may be commented by intrinsic (formal-syntactic) remarks and extrin­ sic (goal related) remarks. These remarks not only explain the purpose of a particular line, but at the same time establish connections with other lines (previous lines and lines yet to be construct­ ed). In fact these remarks point to connections between the very signs that make up the lines of

COMMENTING PROOFS

James R. Geiser Massachusetts Institute of Technology Artificial Intelligence Laboratory Cambridge, Massachusetts

the proof. These connections, which, using Yessenin-Volpin's terminology, are called identificational connections or ids , are the links of a very detailed syntactic structure which resides implicitly in real proofs, a struc­ ture of causal chains connecting the occurences of symbols. This is the new syntactic structure mentioned in the first paragraph.

With this sort of information it becomes possible to answer a question like "what part of the term 11·111 is responsible for the third stroke in the right hand side of the equation ll· lll = llllll ? ". Such a part will be called an ingredient of a term, consisting of a certain list structure whose atoms are the occurences of symbols in the term. H we think of a term t being evaluated to its ntime ral value It I =ll ··· 1 then the ingredients represent the computational history of each stroke in ltl.

Much of the present report is concerned with de­ fining the ingredients of a term and characteriz­ ing their dependence on the computational paths used to evaluate the term. The semantics which arises from this comes from considering a proof as encoding a procedure for manipulating list structures so that if, for example, the proof is of t=s then the encoded procedure induces an isomorphism from the ingredients of t onto the ingredients of s. While ingredients and the re­ sulting semantics can be implimented it seems best at this point to treat these ideas theoretically and to be aware of their possible relevance to such concepts as consistency, relevant entail­ ment, computational efficiency and methods of proof. We wont develope these connections in this report other than to briefly point out a con­ nection between computational efficiency and the "normal" form of an ingredient in section .7.

2. Recursive Arithmetic.

Recursive Arithmetic consists syntactically of terms and equations, and deductively of comp­ utations (constucted by means of the recursion axioms and the substitution rule).

Terms are expressions formed from 1, +, , exp, (, ) by means of the following rules.

1. 1 is a term.
2. H tis a term then so is tl.
3. H t and s are terms then so are (t + s), t. s, and exp(t, s) ·

We shall use the symbols t, r, s, ··· , t 1 , q, s1, ··· to denote terms. We shall make use of the usual conventions for ignoring paran­ theses. Also note that our use of the word ''term" doesn't allow for the occurences of free variables, i.e. they are always to be closed.*

Terms of the form 1, 11, ··· , 1 {n) (n concatenated strokes) are called numerals.

An equation is an expresion of the form t = s.

The Recursion Axiom Schemata:

Addition Al (t + I)= tl.

A2 (t + s 1 ) = (t + s ) 1.

M2 t· (s 1) = t· s + t.

Multiplication Ml t· 1 = t.

Exponentiation El exp(t, 1) = t.

E2 exp(t, s1) = exp(t, s )· t.

The Substitution Rule Schema:

Line LA t = s(r)

Line LB r = r'

Line LC t = S"(r' ).

Here s(r) denotes a term in which the term r has one or more indicated occurences, and s (r') denotes the term resulting from the replacement in s(r) of r by r' at the indicated. occurences of r in s(r). Note that this is more general than uniform substitution. We say that LC follows from LA and LB by substitution.

A proof or computation is formally de­ fined as a sequence of equations each of which is a instance of a recursion axiom or else follows by substitution from two previous equations. We consider two simple yet illuminating examples,

Example 2.1.

Ll 1 + 11 =(I + 1 )1

LZ 1+1=11

L3 I + 11 = 111.

Example z. Z ,

ll l·ll-1·1+1

LZ lol=l

L3 l· II= I +I

L4 1+1=11

L5 1·11 = 11.

3, Commenting Proofs .

·We begin commenting these computations by means of intrinsic and extrinsic remarks-­ this terminology is after Sussman, Then we use these remarks to generate ids between the oc­ curences of symbols in the computation. By

• The notational methods that we shall develope for +, · , and exp, will serve to handle all · other primitive recursive functions.

tracing out chains of ids we can establish an ac­ countability for every sign in the computation. This will at the same time make explicit the semantics of the computation, i.e. which oc­ curences of symbols are synonomous and what are the computational roles of each sign.

The intrinsic or formal comments make

note of : 1) if the line is an axiom; in which case a pointer is generated to the axiom schema in question; 2 )if the line follows by substitution; in which case pointers are generated to the lines from which it follows and to the occurences of the term to be replaced,

The extrinsic or goal-relateJ remarks consist of:

1. the top level goal statement (i, e. find the value of term t );
2. the assertion that line L (s::= s') is generated in order to simplify by substitution a term t(s) in a previous line L 1 ;
3. the assertion that line L" is the result of a substitution rule from lines L, L' whose pur­ pose it was to achieve simplification by means of this substitution;
4. the assertion that the line matches the top level goal.

Example z. I Commented.

The top level goal is to evaluate 1 + 11.

• ll 1 + 11 = (1 + 1 )1 (Axiom AZ) (Purpose is to simplify 1 + 11 of top level goal. ) LZ I+ 1 = 11 (Axiom AI) (Purpose is to sim-
• plify I+ 1 of r. h, s, of Ll using substitution.) L3 1 + 11 =Ill (Sub. Ll, LZ) (Purpose is to fulfill the goal of LZ. L3 matches top level goal.)

Example 2. 2 is commented in a similar manner.

4. ldentificational Connections.

We now add a third type of comment to the analyzed computation, namely we make note of the identificational connections (ids). First of all each axiom is to be accompanied by certain ids as follows, ~

For example, in A2 we would say that s and t in the r. h. s. are rewritten from the s and t in the 1. h. s. and this justifies their synonymity. On the other hand we also make an identificational connection betv;een the two occurences of 1 and this constitutes our semantical interpretation of +in terms of the sucessor function xl.

Now consider M2. We say that both t's in the r. h. s. are rewritten from the 1. h. s t. Similarly the s in the r. h. s. is rewritten from the s in the 1. h. s ·· However, we associate the second t in the r. h. s. with the stroke 1 of the l.h.s.---this is part of our semantical interpre­ tation of· · Thus we are looking at m· n as say­ ing add m to itself n times; in this computation n acts as a counter for then different rewrittings of m. The strokes of mare the counter or con­ trol elements in this case.

Let A be an axiom and id(A) the set of ids associated with A. More explicitly: if a stroke p on the r. h. s is simply rewritten froma stroke q on the 1. h. s. (without a control element) then put id(p, q) in id(A); if on the other hand pin the r. h. s. is rewrittent from q in the 1. h. s. under the control element q' and using an axiom for the operation f (either· or exp) then put id(p, (q,q',f)) in id(A) · *

Ids come from the substitution rule in ac­ cordance with the following schema.

These ids actually come from the extrinsic com­ ments associated with these lines : Lb 1 s purpose is to simplify the indicated s in the r. h. s. of La. Hence the s in the 1. n. s. of Lb is rewritten from the sin the r. h. s. of La. Lc achieves the goal of Lb; hence the context r in the r. h. s. of Lc is rewritten from the context r in the r. h. s. of La and the s' in the r. h. s. of Lc is rewritten from the s' of the r.h.s. of Lb. Also, the l.h.s. of Lc is rewritten from the 1. h. s. of La.

Fully commented by ids Examples 2. 2 look like the following. 2.1 and

Example 2.1 Commented by ids.

* A set of ids like id(A) is usually taken symetrically, i.e., if id(u, v) is in id(A) then so is id(v, u).

Example 2. 2 Commented by ids ·

We can now trace out paths of ids, there­ by diagramming the computational relations be­ tween the different occurences of strokes in the proof. For example, in Example 2. 1, if we de­ note the occurences of strokes in L3 by p, p 1 , p", q, q 1 , q 11 (left to right) then we can see that p is connected to q, p' is connected to q' and p" is connected to q". Further more these are the only connections between the strokes of L3. This yields a very nice correspondence bet:-.ween the 1. h. s. and the r. h. s. strokes of L3.

The case of Example 2. 2 is more com­ plicated in that some of the occurences of strokes act as counter elements and when in this role they do not get rewritten. Lable the strokes in LS p,p',p" q q' (left to right). Trace out a path from q or q' of LS to a pattern of strokes p, p', and p" of LS, using the ids for the axioms and the substitution rule. We see that q traces out to the pattern (p, p 1 , · ) and q' traces out to the pattern (p, p", · ). Thus we are lead to say that q is rewritten from p under the control element p' while q' is rewritten from p under the control element p ". (p, p 1 , · ) and (p, p 11 , · ) are the patterns in 1· 11 of LS "responsible" for q and q' respect­ ively in this computation. These patterns, which will be precisely defined in section 6, we call the ingredients of I· 11. Generally speaking, when a term t is evaluated (i. e. proved equal to some numeral n ) we may identify the ingredients oft responsible for each stroke in n · In section 7 we determine how the ingredients depend on the computation path used to evaluate the term t.

5. Computation Paths ·

On the previous pages we have presented two examples in some detail inorder to give an intuitive picture of what is happening with proofs, comments and ids. We shall now turn to a detailed study of the possible computation paths from a term.

We shall restrict our attention to compu­ tations which have the following (standard) form:

L2i-l L2i L2it-l tl"' Si =: tt == ti+ 1 s·' I ti+2 L2n-l t1 = tn.

where Ll is an axiom and fori :: 1, ·.· , n-2, L2it 1 follows from L2i-l and L2i by substitution. We shall assume that these computations have been commented and the appropriate ids have been made.

The sequence of terms t (= t 1 ), t 2 , ··· , tn is called a computation path from t to tn, Consi­ der a step of the computation (called a simple reduction). ----

We write r(s)--r(s 1 ) to indicate that r(s 1 ) has been obtained from r(s) by a simple reduction. H u = v is al) axiom we shall also write u _.. v and call it a simple reduction,

Define ID(r(s)-+r(s')) to be the set of derived ids between the signs of r(s) and r(s 1 ). Specifically : 1) H pis an occurence of a stroke in r(s 1 ) which is rewritten from q in r(s) via the ida then id(p,q) is in ID(r(s)-+r(s 1 )). 2) H p is an occurence of a stroke in r (s') which is rewritten from q in s 1 of Lb via c and q is re­ written from q' in s of the 1. h. s. of Lb (i.e. the id id(q',q) is in id(s = s 1 ), see section 4), and q 1 is rewritten from q" in s in the r. h. s. of La via b, then id(p,q") is in ID(r(s)-+r(s')). 3) H pis an occurence of a stroke in r(s') and is rewritten from q in s 1 of Lb via c and q is re­ written from q 1 in s of the 1. h. s. of Lb under the control of q" in the 1. h. s, of Lb for the function f (i.e. id((q 1 ,q",f),q) is in id(s:: s 1 )), and q'and q" are rewritten from q* and q** respectively in s in the r. h. s, of La via b then id(p, (q*, q**· f)) is in ID(r(s)-r(s 1 )), 4) H u = v is an axiom define ID(u -v) to be equal to id (u :: v ).

. Every occurence of a stroke pin r(s 1 ) is associated through ID(r(s) ---+r(s 1 )) with a unique stroke q in r(s} of La or a unique pattern (q*,q**,f) of strokes in r(s).

If t 1 , ··· tn is a computation path P and tn is a numeral then Pis called an evaluation path and tn is called the value of t 1 w. r. t. P.

Define T(t) to be the set of all terms oc­ curing in the computation paths from t; the re1ation s- r determines a partial ordering of T(t) which we will now investigate.

The notation s--,.r denotes a computation path frim s to r. We say that t 1 -- ,.tn is a sub­ te rr~ path if none of the reductions ti ~ti-l involve the main function (outer most function symbol in polish notation).

DefinitionS. l A loop consists of two different computation paths going from a term t to a term t 1 , A diamond is a loop which has either form I or II below. We illustrate this using · as the main function symbol.

Form I

Form II

(where the indicated paths are subterm com· putation paths) (where both broken pathe are subterm paths; we may assume that each involves that same as­ sociated subterm paths s--·s' and r--,.r 1 ·

Definition 5. 2 Two computation paths are simple variants if they differ by a diamond, i, e. they look like

Two paths are homologous if there is a sequence of computation paths Pl, P2, ·. ,, Pn such that Pl and Pn are the two paths in question and for i::l, ... ,n-1, Pi and Pi-1 are simple variants. Note that homologous evaluation paths assign the same value to a term.

t·

Lemma 5. 3a. A split of the form

can be resolved into a diamond. (The dotted paths are subterm paths. Multiplication is serving as a paradigm case,)

Lemma 5. 3b, Any split can be resolved into a loop ·

Lemma 5, 3 is an analogue to the <llurch­ Rosser theorem for the Lamda Calculus, The proof of this and other results is by an induction argument on the rank rk(t) of a term, where rk is an integer valued fu~tion (primi ti \·e recur-;rve) defined so that a) if sis a subterm oft then rk(s) < rk(t) and b) if s- t then rk(t) < rk(s). The existence of such a function-shows~ that any computation path from t has less than or equal to rk(t) steps, H we were using all primitive recur­ sive functions then such a rank function could be general recursive but not primitive recursive, e. g. like Ackerman's function. The organization of the proof is to dovetail 5. 3a and 5. 3b, first proving 5. 3a for rk(t) ~ nand then 5. 3b for rk(t) ~ n. The proof"i; somewhat more complicilid than the usual one because we do not require substitution to be uniform, a condition which would considerably simplify the structure of T(t), namely any split of a major connective would al­ ways immediate! y resolve:

6. hlgredients.

Definition 6. 1. Let q1· ··· , qn denote the occur­ ence s of strokes in the term t. Ing (t) denotes the set of list expressions obtained from q1· ·.· qn· ·, and exp, according to the following rules.

1) ql, ··· , qn are in lng(t).

Z) H 2_ and .i_ are in Ing(t) and f is · or exp then <.~.d.! f) is in Ing (t ).

The members of lng(t) are called the abstract ingredients oft, and q 1 , ··· , q are call­ ed the simple ingredients oft. Ingo(t) aenotes the set of simple ingredients of t. In the express­ ion {2_, ,L f), i. is called the control element and i is called the raw material. To understand the ~otivation behind this definition let us once again consider the recursive definition of u· v : u· 1 = u and u· vl = u· v + u. Thus v act as a control ele­ ment and u as a fixed parameter. Corresponding­ ly, if ~and .i_ were ingredients in rands resp. then in the term t equal r· s, {i,j,f) would be an ingredient in t with .i_ as the-control element and!_ as the "raw material" to be recopied.

m the analysis of ingredients and how they change as we trace out the ids in a computation it soon becomes clear that these changes tend to respect the internal structure of ingredients and can be characterized as "homomorphisms" of this structure. So we make a definition.

Definition 6.2. A mapping H: Ing(t)-.Ing(s) is a homomorphism (hom) iff for all (~ .1..! f) in Ing (t) H({!_,i_, f)) - (H{!_), H!,i). f) ·

Facts about Homomorphisms. 6. 3a H H,G: lng(t)-Ing(s) are homomorphisms which agree on mg 0 (t) then H = G. 6. 3b Any map H : Ing 0 (t)-Ing(s) extends to a unique hom from Ing(t) into Ing(s ). 6. 3c Hom His 1-1 on Ing(t) iff His 1-1 on Ing 0 (t).

There are infinitely many abstract ingre­ dients in Ing (t) only some of which represent real computations. We now use the idea of homomorph­ ism to single these out in a precise manner.

We associate with a s imple reduction t-s the following hom H[t -oos]. Let ID(t _..s) be the set of ids accompanying t-s as defined in section 5. H[t -sJ is the unique hom from Ing (s) into Ing (t) determined by the following (here q denotes any simple ingredient in Ing 0 (s )).

H[t-+s] is 1-1 on Ing 0 (s) and hence is 1-1 on all of Ing(s). We can now define the computationally meaningful ingredients.

Definition 6. 4 . Let P = t 1 , ··· , t be an evalua­ tion path for t; thus ltl = t · Define the hom n HfPJ = Hrt 1 -t 2 1 o H[t 2 -+t 3 Jo ··· 0 H[tn_ 1 -tn]. The set of (real) ingredients of t w. r. t. P is the set H[P] (Ing 0 (tn)) and is denoteJ by mg(t;P).

Note that H[ PJ is a 1-1 map of mg 0 (1tl) into mg (t ). So the cardinality of mg (t; P) is equal to the integer denoted by the numeral ltl. We think of H[P] (q) as the unique "computational pattern" in t which is "responsible" for q via P.

7. Invariance of Ingredients.

How does H[P] depend on P? This is an­ swered in Theorem 7. 6, but first consider the following example.

Example 7. 1.

The basic difference bewtween !_ and ,L is the temporal order in which the control ele­ ments q 4 and q 7 are ope rating and not the ultimate control relationships.

The above relationship between !_and ,Lis made into a basic equivalence relation.

Definition 7. z. Let !_and ,j_ be ingredients in Ing(t). We define~~ .J. iff there is a sequence of pairs !!J_, 1 1), ..· , ~n' .J.nl of ingredients of Ing(t) such that.!_= .!.n· .J.::: .J.n· and fork= 1, .· , n either

1. .!.k=1k'

Z) there exists ingredients~· ':!..· ~and function symbols f, g such that {.!.k·lk\ equals { ((~·':!..·f),~,g), ((~,~,g);(':!..,~·g),f)}, or 3) there exists k', k" less thank such that ~k= ~k".!ku,f) and lk = !.i.k·· lk"· f)·

Our Example 7. 1 suggests that as we move from one computation path P to a simple variant P' of P we will find that H[ PJ (q) is changed into an equivalent ingredient H[P'] (q); this is the content of Theorem 7. 7 ·

7, 3 Facts about ~ ·

7. 3a) .~ is an equivalence relation on Ing(t). 7, 3b) H.!_ ~ 1 and ~ ~ j~ then ~ · .J.. f) is equi­ valent to(i',j',f),

7.3c) rr_Ik-~.J.kfork= l,Z,3thP.n <~I·.!.z·f),.!_3,g) ~ <~J.I · .J.3.g), <Jz·b·g),f).

Theorem 7,4,Let H: Ing(s)-+lng(t) be a hom. Then Hpreserves ~,i.e. if.!_and.J.are in Ing(s) and.!_ ~ .J. then H(.!_) ~ H(.J.).

Theorem 7. 5, Let G, H : Ing (s) ~Ing (t) be two horns and suppose that for all p in Ing (s ), G(p) ~ H(p ), Then G(..!_) ~ H(2_) for all..!_ in ° Ing (s ).

Lemma 7. 6. Let t be any term with rk (t) :5 n. L H P and Q are computation paths from t to t' forming a dia~ond and i is a real ingredient in Ing(t') then HCPJ(i) ~ HfQJ(i).

IL H P and Q a~ computation paths from t to t 1 and i is a real ingredient of Ing(t') then HCPJ (..!_) ;; HCQJ(..!_).

The Lemma is proved by induction on n and dovetailing I and II. Lemma 5, 3 plays a major role, As an immediate consequence of this Lemma we get the main result of this section.

Theorem 7. 7. (Invariance of Ingredients.) Let P and Q be two evaluation paths for t. Then for all pin Ing 0 (t), H[PJ(p) ~ H[QJ(p).

There is a natural direction of simplifica­ tion built into the equivalence relation ~ , namely we will say that ({..!_,~,f), (.J.. ~·f), g) reduces to ((2_,1, g),~. f) , We then define an ingredient to be in normal form if it can't be reduced nor does it contain any ingredients which can be so reduced. H one tries to make a cost estimate for various computation paths it appears that if H[P)(q) is in normal form then P is the least expensive com­ putation path. Such estimates are not so easy to make in a reliable way but the examples which have been studied are quite suggestive.

8. Final Remarks.

The ideas presented in this paper can straightfowardly be applied to other deductive­ computational systems such as the Lamda Cal­ culus and Curry's Combinatorial Logic.

The next step in this investigation ex­ tends our analysis to the full 1st Order Intui­ tionistic Theory of Peano Arithmetic. The semantics developed provides a means whereby with each theorem A we can associate a collect­ ion M(A) of procedures extracted from the proofs of A. This will be the subject of a second paper being prepared under an NSF grant through Boston University.

Two examples will give some idea of how this semantics works.

Suppose A is the sentence t = ltl . Then M(A) will contain the procedures which compute the isomorphisms H[P] : In~(lti)-Ing(t) de­ termined by each evaluation path P for t,

Suppose A is the sentence B :>C. Then a procedure in M(A) will be a method for convert­ int a procedure in M(B) into a procedure in M(B). H A is the sentence BvC then a procedure in M(A) would construct a sentence D (which is either B or C) and a procedure in M(D).

Negation is defined in terms of implication -A =:A ::) 1 = 11. This at first seems a little odd because it says th<~.t_ you have a procedure which will transform any procedure in M(A) into a procedure in M{l = 11 ), and, ofcourse, with the means that we allow there are no procedures in M(l = 11 ). H we look at a concrete example like 11 = 111 ::> 1=11, this becomes less mys­ terious since with a little thought we can see how a set of rules, proportedly establishing an iso­ morphism between Ing ( 11) and Ing (111) could be actually modified sg as to establ~sh an iso­ morphism between Ing 0 ( 1 ) and Ing 0 (11 ).

The Induction Schema works out very nicely. For if we have procedures M, M' in M(A(l)) and M( Vx (A(x) :J A(xl ))) respectively, then our procedure in M(Vx A(x)) starts with M and makes a recursive call to M'.

References.

1. Yessenin- Volpin, A.S., "Ultraintuitionism and the Antitraditional Program for the Foundations of Mathematics", Procedings of the Summer conference on Intuitionism and Proof Theory at Buffalo, New York, 1968, North Holland.
2. Sussman, G. , "A Computational Model of Skill Aquisition", Doctoral Thesis, MIT,l973.