Massachusetts Institute of Technology Handout 5 6.044J/18.423J: Computability Theory of and with Scheme September 23, 1998 (revised Sept 28) Professor Albert R. Meyer

# Problems on Equational Proof Systems

For Friday, Sept 25, you should turn in written solutions to a selection among the eleven problems given in Handout 2 on Arithmetic Equations. I leave it to you to decide how many to write up and how thoroughly -- do enough to persuade me that you understand the Handout 2 material and that you have an idea how to write a careful mathematical proof. Samples of such writeups can be found on the Fall 96 webpage. (Solutions to about half the problems are available on the Fall 96 webpage. You are welcome to consult these, but if you do, be sure to include a citation to them in your own work. You might care to comment on or improve on some of those solutions instead of writing your own from scratch.) If there are any parts of Handout 2 you don't understand, indicate that in your writeup so we can discuss it later.

On Monday, Sept. 28, we discussed "substitution proofs." The problem that day had been to explain how to convert any equational proof as defined in Handout 2 into a substitution proof of the same equation. Nobody got very far on this, so we outlined in class how a recursive Scheme procedure might convert a proof in the system of Handout 2 into substitution proof of the same equation. For example, in Handout 2, Fig. 1, there was a ten* line proof of the equation ((f + g) + -g = f):

g + -g = 0 (inverse for +)
f = f (reflexivity)
f + (g + -g) = f + 0 (congruence for +)
(f + g) + -g = f + (g + -g) (associativity of +)
(f + g) + -g = f + 0 (transitivity)
f + 0 = 0 + f (symmetry)
(f + g) + -g = 0 + f (transitivity)
0 + f = f (identity for +)
(f + g) + -g = f (transitivity)
A different, attractive format for a proof would be to write
(f + g) + -g = f + (g + -g) = f + 0 = 0 + f = f.
In ordinary mathematics, we would justify these successive equalities by saying the first followed by (associativity), the second by (inverse for +), and the third and fourth by (symmetry) and (identity for +), respectively. Proofs in this format are easy to follow because each equality follows solely from the immediately previous equality by "substituting equals for equals" -- in contrast to the proofs in the formal system of Handout 2, where justification of an equation may require appeal to more than one antecedent. In Handout 2, we carefully defined "equational proofs" as a sequence of equations satisfying some constraints, namely, each equation had to follow by some inference from equations preceding it in the sequence. We can also give a careful definition of substitution proofs:
Define a sequence of ae's, e_i, separated by equality symbols:
e_1 = e_2 = e_3 = ...= e_n
to be a substitution proof of the aeq (e_1 = e_n), if, for 1 <= i < n, each ae e_(i+1) is obtained from e_i by "substituting equals for equals," viz., using the [x:=...] notation of Handout 2:
e_i can be described as h[x:=f_i], and e_(i+1) can be described as h[x:=g_i]
for some ae, h, with exactly one occurrence of some variable, x, and some ae's f_i and g_i such that one of the equations (f_i = g_i) or (g_i = f_i) is an axiom.
To design a recursive Scheme procedure for converting a proof in the system of Handout 2 into substitution proof of the same equation, assume for simplicity that the input to the Scheme procedure has already been converted from the sequence-of-equations form of Handout 2, into a tree-proof showing the antecedents of each equation. (We discussed in an earlier class how to transform sequence-of-equations proofs into tree proofs and vice-versa). For example, the sequence-of-equations proof above would be represented in tree form as:
```
reflexivity            inverse-for+
(f=f)              ((g + (- g)) = 0)
\                      /
\ congruence-for+  /
\              /
\            /                  commutativity-for+
((f + (g + (- g))) = (f + 0))       ((f + 0) = (0 + f))
\                            /
\       transitivity    /
\                  /
associativity                      \              /
(((f + g) + (- g)) = (f + (g + (- g))))    (((f + (g + (- g))) = (0 + f))
\                                           /
\                                        /
\                                     /
\        transitivity              /
\                               /
\                            /
\                         /                       identity-for+
(((f + g) + (- g)) = (0 + f))                         ((0 + f) = f)
\                                      /
\                                /
\      transitivity        /
\                      /
\                    /
(((f + g) + (- g)) = f)

```
This tree would then be represented as a Scheme list structure. Namely, a tree-proof is represented as a list of the equation proved, a token indicating the inference rule by which it was deduced, and, if the inference rule was not an axiom, the lists representing the tree-proofs of the antecedents of the inference rule. So the representation of the above tree-proof would be:
```(define Fig1-tree-proof
'((((f + g) + (- g)) = f)
transitivity
((((f + g) + (- g)) = (0 + f))
transitivity
((((f + g) + (- g)) = (f + (g + (- g)))) associativity-of+)
(((f + (g + (- g))) = (0 + f))
transitivity
(((f + (g + (- g))) = (f + 0))
congruence-for+
((f = f) reflexivity)
(((g + (- g)) = 0) inverse-for+))
(((f + 0) = (0 + f)) commutativity-for+)))
(((0 + f) = f) identity-for+)))
```
and procedure evaluation might result in:
```(tree-proof-->subst-proof Fig1-tree-proof)
;Value: (((f + g) + (- g)) = (f + (g + (- g))) = (f + 0) = (0 + f) = f)
```
(Actually, it's not likely any simple tree-proof-->subst-proof procedure would yield such a nice substitution proof, but it doesn't have to: any substitution proof of the target equation is OK as the result.)

The assignment for Friday, Oct. 2, is to

• actually define a Scheme procedure tree-proof-->subst-proof. Turn in your procedure definitions and some sample output indicating that the procedure works properly,
• be prepared to discuss how an inverse procedure subst-proof-->tree-proof might be defined (no need to actually write one), and also
• look over and be prepared to discuss sample rewrite rules (given out in class and available as Handout 6 on the course Handouts page) for putting arithmetic expressions into standard, sorted, sum-of-products form; simplifying quoted list expressions; and for the doctor program Eliza. Also take a look at the definitions of the Scheme procedures for pattern-matching and applying the rewrite rules.
Taken together, these proof transforming procedures show that the class of provable equations, i.e., the theorems, would remain the same whichever notion of proof we adopted. And since we've already argued that the system of Handout 2 is Complete, we can conclude that a proof system with substitution proofs is Complete too.
* "There are three kinds of mathematicians, though who can count and those who can't." -- attributed to the famous mathematician E. Bombieri.