COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "book.pub[let,jmc]" source_file
C00009 ENDMK
C⊗;
.require "book.pub[let,jmc]" source_file;
.font B "ms25";
.font C "grfx25"
.font D "grfx35"
.TURN OFF "{}∂[]"
.cb	CS206	Computing with Symbolic Expressions	Spring 1977
.cb	Answer Sheet for Problem Set Three
.cb	June 2  1977
.skip 2
Given	(1)	%2xεu ← ¬%1n%2 u ∧ (x= %1a%2u ∨ xε%1d%2u)%1

Prove	(2)	%2∀xuv: [xε(u*v) ≡ xεu ∨ xεv]%1

.fill
We can prove assertion (2) if we can change the function definition for member
into a universally quantified statement about member. What we want is the following
theorem.

.nofill
Theorem	(3)	%2∀xu: [xεu ≡ ¬%1n%2u ∧ (x=%1a%2u ∨ xε%1d%2u)]%1

.fill
Since definition (1) could lead to contradictions in the event that its calculation
is undefined, we cannot simply copy the definition, making syntactic changes to yield
theorem (3). We must prove that definition (1) is total; to do so we resort to the
fake predicates mentioned in class as a tool for proving totality of other predicates.

We must create a fake version of member, defined by the following assertion.
.nofill

Definition (4)	%2∀xu: [memberA[x,u] ≡ NOT NULL u AND (x EQUALS %1a%2u OR memberA[x,%1d%2u])]%1

We will define our original member predicate as follows.

Definition (5)	%2∀xu: [x ε u ≡ (memberA[x,u]=T)]%1

.fill
Since memberA is a fake predicate, its result can be true, false, or undefined.
Since the result "undefined" is not an s-expression, we need only show that for
all cases where x and u are s-expressions, memberA[x,u] is also an s-expression.
.nofill

Theorem	(6)	%2∀xu: issexpr[memberA[x,u]]%1

.fill
Since %2u%1 is list, we will use the induction schema for lists, proving our hypothesis
for the case where u is null and proving that P[du] implies P[u].

.nofill
Schema	(7)	%2∀u: [ P(%1nil%2) ∧ ( P(%1d%2u)→P(u) )] → ∀u: P(u)%1

In our case, P(u) must be that our fake predicate yields an s-expression.

Lemma	(8) 	%2P(u)= issexpr [memberA[x,u]]%1

Considering the cases we have the following two results.

Case 	(9)	%2u=%1nil:%2	P(%1nil%2)= issexpr [NOT NULL %1nil%2 AND ....]%1

From theorem B9 of the Representation paper we know that F AND anything is F.

		%2P(%1nil%2) = issexpr [F]
		P(%1nil%2) = T%1

Case(10) %2u≠%1nil%2	P(u) = issexpr[[NOT NULL u] AND [x EQUALS %1a%2u OR memberA[x,%1d%2u]]]%1

Distributing the predicate we have the following.

	%2P(u) = issexpr[T] AND issexpr[[x EQUALS %1a%2u] OR memberA[x,%1d%2u]]%1

By our induction schema we can assume that the cdr case is true, so we have the following.

	%2P(u) = issexpr[T] AND issexpr[T∨F]
	P(u) = T%1

.fill
With cases (8) and (9) proven, we can now use our schema (7) to claim that lemma
(8) is proven true, and that as a consequence, memberA is defined for all
s-expressions, that is that memberA is total. By the magic of our definition
(5), we can also claim that member (ε) is total and the transformation of the 
definition into the quantified expression (3) is now legal.

Our hypothesis to be proven is as follows.

.nofill
Hypothesis (11)	%2P(u)=[∀xuv: [xε u*v ≡ xεu ∨ xεv]]%1

P(u) for the case where u is nil can be easily demonstrated by substitution.

	%2xε(%1nil%2*v) =?= xε %1nil%2 ∨ xεv
	xεv =?= F ∨ xεv%1			by def's of append and member
	%2xεv = xεv%1			by def of ∨

.fill
For the case where u≠nil, we will substitute our definition for member into the
left side of the iff in the hypothesis, and struggle to produce the right side.

.nofill
%2 xε u*v = ¬%1n%2(u*v)∧(x=%1a%2(u*v) ∨ xε %1d%2(u*v))%1		by theorem (3)
%2 xε u*v = ¬%1n%2(%1a%2u.[%1d%2u*v]) ∧ (x=%1a%2[%1a%2u.[%1d%2u*v]] ∨ xε %1d%2(%1a%2u.[%1d%2u*v]))%1	by def of append

.fill
The axioms for lisp in the Representation paper include a number of theorems that we
now need.
.nofill

L6	at nil
L13%2	∀xy: %1a%2(x.y)=x%1
L14	%2∀xy: %1d%2(x.y)=y%1
L15	%2∀xy: ¬%1at%2(x.y)%1

.fill
Using L6 and L15, we can prove that %2∀xy: ¬%1n%2(x.y)%1 by contradiction. Making this 
substitution and those for the car and cdr, we have a cleaner expression.

%2xε u*v = T ∧ (x=%1a%2u ∨ xε(%1d%2u*v) )%1

Since we are following the induction schema (7), we can assume hypothesis (11) for 
the cdr case, so we can replace part of our expression as follows.

%2xε u*v = (x=%1a%2u ∨ xε%1d%2u) ∨ xεv%1

Finally, we can apply theorem (3) backwards, substituting the expression for 
its expansion.

%2xε u*v = xεu ∨ xεv%1