perm filename HW3.SOL[206,LSP] blob sn#251563 filedate 1976-12-07 generic text, type C, neo UTF8

COMMENT ⊗ VALID 00003 PAGES C REC PAGE DESCRIPTION C00001 00001 C00002 00002 C00007 00003 C00008 ENDMK C⊗; SOLUTIONS TO HW#3 CS216 DEC 7,1976 I assume the facts, proved in class, that (1) u*[v*w]=[u*v]*w and (1) u*NIL=u. The following propositions correspond to the LISP definitions of the functions which concern us here: (2) u*v = if n u then v else a u.[[d u] * v] (3) rev(u) = rev1(u,NIL)[Note: to save writing, I've renamed "reverse" to "rev"] (4) rev1(u,v) = if n u then v else rev1(d u,a u . v) (5) u % x = if n u then NIL else [[a u].x].[d u % x] (6) u ⊗ v = if n v then NIL else [ u % a v] * [ u ⊗ d v ] I wish to prove: rev(u*v)=rev(v)*rev(u), rev(rev(u))=u, and u⊗[v*w]=[u⊗v]*[u⊗w] First I prove a lemma, (7) rev1(u,v)=rev(u)*v Proof: By induction on u. The Induction hypothesis P(u) is ∀v.(rev1(u,v)=rev(u)*v) Base case: Assume u=NIL. Then rev1(u,v) = if n u then v else rev1(d u,au .v) = v = NIL*v = rev1(NIL,NIL)*v = rev(u)*v Induction step: Assume ¬(n u) and that for all w, rev1(d u,w)=rev(d u)*w Then rev1(u,v) = if n u then v else rev1(d u,a u . v) = rev1(d u, a u .v) = rev(d u)*[a u . v] (by the induction hypothesis) = rev(d u)* [[a u . NIL] * v] (by definition of * ) = [rev(d u) * [a u . NIL]] * v (by 1) = rev1[d u,a u . NIL] * v (by the induction hypothesis) = rev1[u,NIL] * v (by the definition of rev1) = rev(u) * v (by the definition of rev) (8) rev(u*v)=rev(v)*rev(u) Proof: By induction on u. Base case: If u=NIL then rev(u*v) = rev(NIL*v) = rev(v) = rev(v) * NIL = rev(v) * rev(NIL) = rev(v) * rev(u), since rev(NIL) = NIL (immediate from (3),(4)) Induction step: Assume ¬(n u), and that for all w, rev(d u * w)=rev(w) * rev(d u) Then rev(u*v) = rev1(u*v,NIL) = if n u*v then NIL else rev1(d [u*v],[a [u*v]].NIL) Now u*v = if n u then v else a u.[[d u]*v] =a u.[[d u]*v] which is not NIL, thus rev(u*v) = rev1(d [u*v],[a [u*v]].NIL) = rev(d [u*v])*[[a [u*v]]. NIL] (by (7)) = rev(d [u*v]) * [a u . NIL] (by definition of *) = rev([d u]*v) * [a u . NIL] (by definition of *) = [rev(v)*rev(d u)]*[a u . NIL] (by induction hypothesis] = rev(v)* [rev(d u)*[a u.NIL]] (by 1) = rev(v) * [rev1(d u,a u . NIL)] (by 7) = rev(v) * rev(u) (by definition of rev,rev1) (9) rev(rev(u))=u Proof: By induction on u. Base case: rev(rev(NIL))=NIL is immediate from the defintions of rev,rev1. Induction step: Assume ¬(n u) and rev(rev(d u))=d u. Then rev(rev(u))=rev(rev1(u,NIL)) = rev(if n u then NIL else rev1(d u,a u . NIL)) = rev(rev1(d u,a u . NIL)) = rev(rev(d u)*[a u . NIL]) (by 7) = rev(a u .NIL) * rev(rev(d u)) (by 8) = rev(a u . NIL) * d u (by the induction hypothesis) = [a u . NIL] * d u (by the definition of rev,rev1) = u (by definition of *) (10) u⊗[v*w]=[u⊗v]*[u⊗w] Proof: By indution on v. Base case: if v=NIL then u⊗[v*w]=u⊗[NIL*w]=u⊗w=NIL*[u⊗w]=[u⊗v]*[u⊗w] Induction step: Assume ¬(n v) and u⊗[d v * w] = [u ⊗ d v] * [u ⊗ w] Then u⊗[v*w] = if n v then NIL else [u % [a [v*w]]] * [u ⊗ d [v * w]] = [u % [a [v*w]]] * [u ⊗ d [v *w]] = [u % [a v]]*[u ⊗ [[d v]*w]] (by definition of *) = [u % [a v]]*[[u ⊗ [d v]]*[u⊗w]] (by the induction hypothesis) = [[u % [a v]] * [u ⊗ [d v]] ⊗ [u ⊗ w] (by 1) = [u ⊗ v]*[u ⊗ w] (by definitition of ⊗) Notice that in this last proof, we used no property of the function % !