perm filename SOLNS3.S77[206,LSP] blob sn#287042 filedate 1977-06-02 generic text, type C, neo UTF8
C00001 00001
C00002 00002	.require "[let,jmc]" source_file
C00009 ENDMK
.require "[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

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	(3)	%2∀xu: [xεu ≡ ¬%1n%2u ∧ (x=%1a%2u ∨ xε%1d%2u)]%1

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.

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

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.

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

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

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

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.

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 ∨

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.

%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

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

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

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