perm filename SOLNS3.S77[206,LSP] blob sn#287042 filedate 1977-06-02 generic text, type C, neo UTF8

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