perm filename PROBS2.S78[206,LSP] blob sn#351111 filedate 1978-04-24 generic text, type C, neo UTF8

COMMENT ⊗ VALID 00003 PAGES C REC PAGE DESCRIPTION C00001 00001 C00002 00002 .REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file C00003 00003 .hd206 SPRING 1978 C00006 ENDMK C⊗; .REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file; .PAGE FRAME 56 HIGH 80 WIDE; .evenleftborder ← oddleftborder ← 1000; .area text lines 1 to 56; .place text; . .MACRO hd206 (TERM) ⊂ .BEGIN NOFILL TURNON "←→" ←COMPUTER SCIENCE DEPARTMENT ←STANFORD UNIVERSITY .SKIP CS206 ←COMPUTING WITH SYMBOLIC EXPRESSIONS →TERM .TURNOFF .END ⊃ . . .MACRO hw (NUMBER, DUEDATE) ⊂ . BEGIN TURNON "←" NOFILL ←PROBLEM SET NUMBER ←Due DUEDATE . TURNOFF END ⊃ . .itemmac 1 . .PORTION MAINPORTION . .hd206 SPRING 1978 .skip .hw 2, |May 16| . .bb General comments. This assignment involves proving properties of LISP functions. Unless otherwise noted your proofs should be fairly formal. The level of detail should be approximately that of Chapter_III section_7 of the notes. For each step of your proof, make sure that you list all of the facts (axioms, earlier steps or previously proved properties) that are necessary to make that step. You may use any facts already proved in the notes or in class. .item←0 .begin indent 0,6 .bb Assignment. #. Chapter III. Exercise 1. ii-v. #. Chapter III. Exercise 2. #. EXTRA (for practice with extended truth values, not required). Let ⊗andlist be as defined in Chapter I and assume ⊗p is a suitably well-behaved predicate. Prove the following: ##. ⊗⊗∀u v: [andlis[u*v, p] = andlis[u, p] ∧ andlis[v, p]]⊗ ##. ⊗⊗∀u: [andlis[reverse u, p] = andlis[u, p]]⊗ Hint: define ⊗aandlis, which returns an extended truth value corresponding to the truth value of ⊗andlis on corresponding arguments. Show that ⊗andlis as defined in terms of ⊗aandlis satisfies the desired equivalence. Then you may use this result to prove other facts about ⊗andlis. The statement that "⊗p is suitably well-behaved" is rather vague. You will need to make it more precise in order to make your proof clear. State this in your proof. .end