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