perm filename FINAL.F77[206,LSP]2 blob sn#325500 filedate 1977-12-29 generic text, type C, neo UTF8

COMMENT ⊗ VALID 00007 PAGES C REC PAGE DESCRIPTION C00001 00001 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 C00019 ENDMK C⊗; .require "lspmac.pub[lsp,clt]" source; .LSPFONT .allop .basicops .MACRO hd206 (TERM) ⊂ .BEGIN NOFILL TURNON "←→" ←COMPUTER SCIENCE DEPARTMENT ←STANFORD UNIVERSITY .SKIP CS206 ←COMPUTING WITH SYMBOLIC EXPRESSIONS →TERM .TURNOFF .END ⊃ . .itemmac .PORTION MAINPORTION .PAGE ← 1 .hd206 Fall 1977 .skip .cb Solutions to Final Exam. .skip 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 as indicated. .item←0 #. %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 .begin nofill ⊗⊗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 ⊗⊗= x⊗ .end .next page #. 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 prove (5pts)b. %2∀u:u ≤≤ u%1. (5pts)c. %2∀u v w:(u ≤≤ v ∧ v ≤≤ w ⊃ u ≤≤ w)%1. .begin nofill 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 ⊗ .end 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. Thus .begin nofill ⊗⊗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$]⊗ .end .next page #. (10pts) What is ⊗⊗compexp[$$(CONS (CAR X) Y), 0, ((X.1)(Y.2))$]⊗ as compiled by LCOM0 and LCOM4. .begin nofill 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)) .end #. (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 state %Ax%1. 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. .begin nofill ⊗⊗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]⊗ .end