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
C00002 00002 .REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file
C00003 00003 .hd206 SPRING 1978
.REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file;
.PAGE FRAME 56 HIGH 80 WIDE;
.evenleftborder ← oddleftborder ← 1000;
.area text lines 1 to 56;
.MACRO hd206 (TERM) ⊂
.BEGIN NOFILL TURNON "←→"
←COMPUTER SCIENCE DEPARTMENT
CS206 ←COMPUTING WITH SYMBOLIC EXPRESSIONS →TERM
.MACRO hw (NUMBER, DUEDATE) ⊂
. BEGIN TURNON "←" NOFILL
←PROBLEM SET NUMBER
. TURNOFF END ⊃
.hd206 SPRING 1978
.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.
.begin indent 0,6
#. 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.