perm filename FINAL.F77[206,LSP] blob sn#361413
filedate 1978-06-13 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00007 PAGES
C REC PAGE DESCRIPTION
C00002 00002 .require "lspmac.pub[lsp,clt]" source
C00006 00003 .hd206 Fall 1977
C00009 00004 #. We will say that a list u is "intermittently contained" in
C00013 00005 #. (10pts) Let e be a LISP expression in internal notation. %2usecadr e%1 is
C00015 00006 #. (10pts) What is compexp[$$(CONS (CAR X) Y), 0, ((X.1)(Y.2))$] as compiled by
C00016 00007 #. (10pts) Write an abstract evaluator for Boolean expressions using the
.require "lspmac.pub[lsp,clt]" source;
.MACRO hd206 (TERM) ⊂
.BEGIN NOFILL TURNON "←→"
←COMPUTER SCIENCE DEPARTMENT
CS206 ←COMPUTING WITH SYMBOLIC EXPRESSIONS →TERM
.PAGE ← 1
.hd206 Fall 1977
.cb Solutions to Final Exam.
This examination is open book and notes.
Write LISP functions as follows except where something else is
requested. Either notation may be used.
When a requested proof requires induction, be sure and write down
the induction principle appealed to and the specific predicate to
which the induction is applied. There are a total of 60pts possible, distributed
#. %2rev x%1 is the "reverse" of the arbitrary S-expression ⊗x. Thus
%2rev%1 (A.(B.C)) = ((C.B).A). Note that ⊗rev applied to a list
does not give the usual reversal of the list.
(5pts)a. Write a recursive definition of ⊗rev.
(5pts)b. Prove that ⊗rev is total.
(5pts)c. Prove that ⊗rev satisfies %2∀x: rev rev x = x%1.
1a. ⊗⊗rev x ← qif qat x qthen x qelse rev qd x . rev qa x⊗
1b. We prove ⊗rev is total by S-expression induction using the induction predicate
⊗⊗qP[x] ≡ issexp rev x⊗
In the case ⊗⊗qat x⊗, ⊗⊗rev_x_=_x⊗ and we know ⊗⊗issexp_x⊗. In the case
⊗⊗¬qat x⊗, we have ⊗⊗rev_x_=_rev_qqd_x_._rev_qqa_x⊗. By the induction hypothesis
both arguments to ⊗cons satisfy ⊗issexp and we are done.
1c. We prove this using S-expression induction using the induction predicate
⊗⊗qP[x] ≡ rev rev x = x⊗
In the case ⊗⊗qat x⊗, ⊗⊗rev_rev_x_=_x⊗. In the case ⊗⊗¬qat x⊗ we have
⊗⊗rev rev x = rev[rev qd x . rev qa x]⊗ ...by definition of ⊗rev
⊗⊗= [rev rev qa x] . [rev rev qd x]⊗ ...by 1b,definition and LISP axioms
⊗⊗= qa x . qd x⊗ ...by induction hypothesis
#. We will say that a list ⊗u is "intermittently contained" in
a list ⊗v if the elements of ⊗u occur in ⊗v in the same order
as in ⊗u but possibly separated by other elements of ⊗v. We write
%2u_≤≤_v%1 for this relation. Thus we have (A_C_E)_≤≤_(X_A_B_C_A_F_D_E_G).
(5pts)a. Write a recursive definition of %2u ≤≤ v%1.
Assume, to make the problem easier, that your %2u ≤≤ v%1 is total, and
(5pts)b. %2∀u:u ≤≤ u%1.
(5pts)c. %2∀u v w:(u ≤≤ v ∧ v ≤≤ w ⊃ u ≤≤ w)%1.
2a. ⊗⊗u ≤≤ v ← qif qn u qthen $T ⊗
⊗⊗qelse qif qn v qthen qNIL ⊗
⊗⊗qelse qif qa u = qa v qthen qd u ≤≤ qd v⊗
⊗⊗qelse u ≤≤ qd ⊗
2b. This proved by list induction with ⊗⊗qP[u] = u ≤≤ u⊗. If ⊗⊗qn u⊗ then
it is true by definition of ≤≤. If ⊗⊗¬qn u⊗ then ⊗⊗u ≤≤ u ≡ qd u ≤≤ qd u⊗ which
is true by the induction hypothesis.
2c. This is proved by list induction on ⊗w with ⊗⊗qP[w] ≡ ∀u v: [u ≤≤ v ∧ v ≤≤ w ⊃ u ≤≤ w]⊗
In the case ⊗⊗qn w⊗ if ⊗⊗u ≤≤ v ∧ v ≤≤ w⊗ then from the definition we have ⊗⊗qn v⊗ and
⊗⊗qn u⊗ and thus ⊗⊗u ≤≤ w⊗ as desired. To do the induction step we will use a
lemma: ⊗⊗∀u w: ¬qn w ∧ u ≤≤ qd w ⊃ u ≤≤ w⊗.
In the case ⊗⊗¬qn w⊗ we observe that if ⊗⊗qn u⊗
then the result is trivial, so we may assume that ⊗⊗¬qn u⊗ and therefore ⊗⊗¬qn v⊗.
There are two possibilities. If ⊗⊗qa v ≠ qa w⊗ then ⊗⊗v ≤≤ qd w⊗ and
by the induction hypothesis ⊗⊗u ≤≤ qd w⊗ so by the lemma we are done.
If ⊗⊗qa v = qa w⊗ then ⊗⊗qd v ≤≤ qd w⊗ and we have two
further cases. If ⊗⊗qa u ≠ qa v⊗ then ⊗⊗u ≤≤ qd v⊗ and again by induction and
the lemma we are done.
Otherwise we have ⊗⊗qd u ≤≤ qd v⊗ so by induction ⊗⊗qd u ≤≤ qd w⊗. But also we
know that ⊗⊗qa u = qa v = qa w⊗ so by definition of ≤≤ we are done.
The lemma can be proved by induction on ⊗⊗size_u_+_size_w⊗ using the predicate
⊗⊗⊗qP[n] = ∀u w: [size u + size w = n ⊃ [¬qn w ∧ u ≤≤ qd w ⊃ u ≤≤ w] ∧ [¬qn u ∧ u ≤≤ w ⊃ qd u ≤≤ w]]⊗
#. (10pts) Let ⊗e be a LISP expression in internal notation. %2usecadr e%1 is
equivalent to ⊗e except that subexpressions of the form (CAR_(CDR_%2e%1)) are
replaced by (CADR_%2e%1). Thus
%2usecadr%1 (CONS (CAR (CDR (FOO X))) Y) = (CONS (CADR (FOO X)) Y).
We assume ⊗e is an expression which can be ⊗⊗eval⊗ed and hence is either an
atom or a list consisting of an operator expression followed by its operands.
⊗⊗usecadr x ← qif qat x qthen x⊗
⊗⊗qelse qif [qa x = $CAR ∧ ¬qat qad x ∧ qaad x = $$CDR$] qthen
$CADR . mapcar[qdad x, $$USECADR$]⊗
⊗⊗qelse usecadr qa x . mapcar[qd x, $$USECADR$]⊗
#. (10pts) What is ⊗⊗compexp[$$(CONS (CAR X) Y), 0, ((X.1)(Y.2))$]⊗ as compiled by
LCOM0 and LCOM4.
LCOM0: (MOVE 1 1 P)
(PUSH P 1)
(MOVE 1 0 P)
(SUB P (α% 0 0 1 1))
(CALL 1 (QUOTE CAR))
(PUSH P 1)
(MOVE 1 1 P)
(PUSH P 1)
(MOVE 1 -1 P)
(MOVE 2 0 P)
(SUB P (α% 0 0 2 2))
(CALL 2 (QUOTE CONS))
LCOM4: (HLRZ 1 @ 1 P)
(MOVE 2 2 P)
(CALL 2 (QUOTE CONS))
#. (10pts) Write an abstract evaluator for Boolean expressions using the
abstract syntactic functions
a. %2isand e%1 meaning that ⊗e has principal connective "and".
b. %2isor e%1 meaning that ⊗e has principal connective "or".
c. %2isnot e%1 meaning that ⊗e has principal connective "not".
d. In each of the three above cases, %2operands e%1 gives a list
of the operands of the expression. If ⊗e satisfies %2isnot%1, there is
exactly one operand, but in the other cases there may be any number. The
LISP functions and predicates qa, qd, qn are applicable to these lists.
e. %2isvar e%1 means that ⊗e is a Boolean variable, and in this
case the predicate %2true(e,%Ax%1) is true if ⊗e is true in the
Write a recursive definition of the predicate %2istrue(e,%Ax%1)
whose value is true or false according to whether the Boolean expression
⊗e is true in the state %Ax%1. Your program should
not look at more terms of "and"s and "or"s than necessary to
decide the truth value.
⊗⊗istrue[e,qr] ← ⊗
⊗⊗qif isvar e qthen true[e,qr]⊗
⊗⊗qelse qif isnot e qthen ¬istrue[qa operands e, qr]⊗
⊗⊗qelse qif isand e qthen istand[operands e, qr]⊗
⊗⊗qelse qif isor e qthen istor[operands e, qr]⊗
⊗⊗istand[u, qr] ← qif qn u qthen $T qelse qif ¬istrue[qa u, qr] qthen $F qelse istand[qd u, qr]⊗
⊗⊗istor[u, qr] ← qif qn u qthen $F qelse qif istrue[qa u, qr] qthen $T qelse istor[qd u, qr]⊗