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 |

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)`:

A different, attractive format for a proof would be to writeg + -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)

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:(f + g) + -g = f + (g + -g) = f + 0 = 0 + f = f.

Define a sequence of ae's, e_i, separated by equality symbols: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:e_1 = e_2 = e_3 = ...= e_n to be asubstitution proofof 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 anaxiom.

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: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)

and procedure evaluation might result in:(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+)))

(Actually, it's not likely any simple(tree-proof-->subst-proof Fig1-tree-proof) ;Value: (((f + g) + (- g)) = (f + (g + (- g))) = (f + 0) = (0 + f) = f)

**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.

* "There are three kinds of mathematicians, though who can count and those who can't." -- attributed to the famous mathematician E. Bombieri.

Copyright © 1998. All rights reserved. | Last updated 10/18/98 |