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.
| Copyright © 1998. All rights reserved. |
Last updated 10/18/98
|
