perm filename HOMEW3[206,LSP] blob sn#482120 filedate 1979-10-18 generic text, type C, neo UTF8

COMMENT ⊗ VALID 00003 PAGES C REC PAGE DESCRIPTION C00001 00001 C00002 00002 .REQUIRE "206MAC.PUB[206,LSP]" source_file C00003 00003 .hd206 FALL 1979 C00012 ENDMK C⊗; .REQUIRE "206MAC.PUB[206,LSP]" source_file; . .odd heading(,,{page}) ; .even heading({page}, , ) ; . .LSPFONT .basicops . .allops .itemmac 1; . .PORTION MAINPORTION .hd206 FALL 1979 .PAGE ← 1 .hw 3, |Nov. 12?| .begin .indent 0,3 .item ← 0 #. Consider the program ⊗flatagain[x] defined as follows: .begin nofill indent 0,0 ⊗⊗flatagain_x ← flata[<x>,qNIL]⊗ ⊗⊗flata[u,v] ← qif qn u qthen v qelse qif qat qa u qthen flata[qd u,qa u_._v] qelse flata[qda u_._[qaa u_._qd u],v]⊗ .end Prove that ⊗flatagain is total on S-expressions (⊗⊗∀x:SEXP_flatagain_x⊗) and that it computes the same function as ⊗fringe (⊗⊗∀x:flatagain_x=fringe_x⊗). The actual solution to this problem should be quite short, but it will require inventing a suitable intermediate theorem to prove, and figuring out a rank function to use for the induction. #. This problem is designed to lead you through the development of a theory about an inductively defined domain, ⊗BOOL, of boolean expressions. We then represent elements of this domain as S-expressions, and prove the representation correct. We can then write LISP programs to compute functions or predicates on the ⊗BOOL and use the theory of ⊗BOOL to reason about these programs. The domain of boolean expressions, ⊗BOOL, is defined inductively as follows. .begin nofill (i) ⊗BT boolean expression satisfying ⊗BOOLT (ii) ⊗BF boolean expression satisfying ⊗BOOLF (iii) A boolean variable is a boolean expression satisfying ⊗BOOLV (iv) If ⊗be is boolean expression then the negation ⊗mknot[be] is a boolean expression satisfying ⊗BOOLN (v) If ⊗be1 and ⊗be2 are boolean expressions then the conjuction ⊗mkand[be1,be2] is a boolean expression satisfying ⊗BOOLA. (vi) The only boolean expressions are those that are required by (i)-(v). Each boolean expression is uniquely determined by its construction via successive applications of (i)-(v) .end We have the function ⊗pn defined on the subdomain ⊗BOOLN which returns the component expression, the functions ⊗pa1, ⊗pa2 defined on the subdomain ⊗BOOLA which select the first and second components, respectively. ##. Give domain specifications, domain range mappings and axioms characterizing the domain of boolean expressions. In particular you should .skip .begin preface 0 (i) You should express the appropriate domain/range specifications for the functions ⊗mknot, ⊗mkand, ⊗mkor, ⊗pn, ⊗pa1, ⊗pa2, ⊗po1 and ⊗po2. (ii) The domain relations should express the fact that each boolean expression belongs to exactly one of the subdomains ⊗BOOLT, ⊗BOOLF, ⊗BOOLV, ⊗BOOLN or ⊗BOOLA. (iii) Provide for variables ⊗be, ⊗be1, ... ranging over boolean expressions, ⊗bv, ⊗bv1, ... ranging over boolean variables, ⊗bn, ⊗bn1, ... ranging over negations, and ⊗ba, ⊗ba1, ... ranging over conjunctions. (iv) The axioms should express the algebraic relations for the selector and constructor functions for negations and conjuctions. Also give the axiom schema for structural induction on boolean expressions. .end ##. Decide on a representation of boolean expressions as S-expressions and write programs implementing this representation. You will need a program to decide whether an arbitrary S-expression represents a boolean expression. You will also need programs for each subdomain, to decide whether a boolean expression (e.g. an S-expression representing a boolean expression) is a member of that subdomain, and programs implementing the constructor and selector functions. ##. Prove that your representation is correct. E.g. give the axioms characterizing your programs as functions on S-expressions and show that the computed domain predicates satisfy the domain relations and that the selector and constructor functions obey the domain/range specifications and satisfy the algebraic axioms. ##. Write an interpreter ⊗beval[be,alist] which computes the value (a boolean constant) of the expression ⊗be using to the assignment of values to variables given by ⊗alist and the following rules: .begin nofill indent 8,8 ⊗⊗BT → BT⊗ ⊗⊗BF → BF⊗ ⊗⊗mknot BT → BF⊗ ⊗⊗mknot BF → BT⊗ ⊗⊗mkand[BT,BT] → BT⊗ ⊗⊗mkand[BT,BF] → BF⊗ ⊗⊗mkand[BF,BT] → BF⊗ ⊗⊗mkand[BF,BF] → BF⊗ .end ##. Notice that according to the above rules we have the following property: .begin nofill indent 8,8 ⊗⊗∀be alist.beval[mknot[BT],alist]=BF]⊗ ⊗⊗∀be alist.beval[mknot[BF],alist]=BT]⊗ ⊗⊗∀be alist.beval[mkand[BT,be],alist]=beval[be,alist]]⊗ ⊗⊗∀be alist.beval[mkand[be,BT],alist]=beval[be,alist]]⊗ ⊗⊗∀be alist.beval[mkand[BF,be],alist]=BF⊗ ⊗⊗∀be alist.beval[mkand[be,BF],alist]=BF⊗ .end Write a program ⊗bsimplify[be] which reduces ⊗be to a constant is possible and other wise removes all occurrences of constants in the expression by applying the above facts as simplification rules. ##. Prove that your program is sound with respect to the interpreter. That is prove ⊗⊗⊗∀be alist.[binds[be,alist]⊃beval[bsimplify[be],alist]=beval[be,alist]]]⊗ ##. Prove that your program returns a maximally simplified expression. Namely, prove that .begin nofill ⊗⊗∀be: bsimplest[bsimplify[be]]⊗ where ⊗⊗∀be: bsimplest[be]≡BOOLT be ∨ BOOLF be ∨ bsimpv[be]⊗ ⊗⊗∀be:[[bsimplv[be]≡BOOLV be ∨ ⊗ ⊗⊗_______________[BOOLN be ∧ bsimpv[pn be]] ∨ ⊗ ⊗⊗_______________[BOOLA be ∧ bsimpv[pa1 be] ∧ bsimpv[pa1 be]] ]⊗ .end .END