exercises.holbert

[{"contents":[0,"A Holbert PL Semantics Exercise"],"tag":"Heading"},{"contents":"This is a series of small exercises designed to help you get familiar with Holbert. So that you will not need to type cumbersome prefix notation, we define some syntax here.","tag":"Paragraph"},{"contents":[2,"_/\\_","LeftAssoc"],"tag":"SyntaxDecl"},{"contents":[1,"_\\/_","LeftAssoc"],"tag":"SyntaxDecl"},{"contents":[5,"not_","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_BExp","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_IExp","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[1,"if_then_else_","LeftAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_Bool","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_eval_","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_eval","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_|->_","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"_~=_","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[0,"let_in_","NonAssoc"],"tag":"SyntaxDecl"},{"contents":[1,"The Language I of Boolean Decisions"],"tag":"Heading"},{"contents":"First, we shall define a judgement $x:x Bool$ that says that $x:x$ is a boolean value, $True$ or $False$. Under \"derived rules\" you can see that Holbert generates elimination and cases rules for booleans automatically. This is because we used the \"Inductive Definition\" mechanism.","tag":"Paragraph"},{"contents":["Inductive",[["True F",[[],[],{"contents":[{"contents":"_Bool","tag":"Const"},{"contents":"True","tag":"Const"}],"tag":"Ap"}],null],["False F",[[],[],{"contents":[{"contents":"_Bool","tag":"Const"},{"contents":"False","tag":"Const"}],"tag":"Ap"}],null]],[[{"contents":["_Bool",1],"tag":"Cases"},[["§P","§0"],[[[],[],{"contents":[{"contents":"_Bool","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"True","tag":"Const"}],"tag":"Ap"}]],{"contents":1,"tag":"LocalVar"}],[[],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"False","tag":"Const"}],"tag":"Ap"}]],{"contents":1,"tag":"LocalVar"}]],{"contents":1,"tag":"LocalVar"}]],[{"contents":["_Bool",1],"tag":"Induction"},[["§P0","§0"],[[[],[],{"contents":[{"contents":"_Bool","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":"True","tag":"Const"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":"False","tag":"Const"}],"tag":"Ap"}]],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]]]],"tag":"Rule"},{"contents":"Next, we shall define the language judgement $A:A IExp$ that says that $A:A$ is a valid expression in the language $I$. Valid forms are $0$, $1$ and $if_then_else_$ expressions. ","tag":"Paragraph"},{"contents":["Inductive",[["0 F",[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":"0","tag":"Const"}],"tag":"Ap"}],null],["1 F",[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":"1","tag":"Const"}],"tag":"Ap"}],null],["if F",[["A","B","C"],[[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],null]],[[{"contents":["_IExp",1],"tag":"Cases"},[["§P","§0"],[[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"}]],{"contents":1,"tag":"LocalVar"}],[[],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"1","tag":"Const"}],"tag":"Ap"}]],{"contents":1,"tag":"LocalVar"}],[["A","B","C"],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":4,"tag":"LocalVar"}]],{"contents":1,"tag":"LocalVar"}]],[{"contents":["_IExp",1],"tag":"Induction"},[["§P0","§0"],[[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":"0","tag":"Const"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":"1","tag":"Const"}],"tag":"Ap"}],[["A","B","C"],[[[],[],{"contents":[{"contents":4,"tag":"LocalVar"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":4,"tag":"LocalVar"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":4,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":4,"tag":"LocalVar"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}]],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]]]],"tag":"Rule"},{"contents":"Next, we shall define some axioms that give a [big-step, operational] semantics to the language I.","tag":"Paragraph"},{"contents":["Axiom",[["eval 0",[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":"0","tag":"Const"}],"tag":"Ap"},{"contents":"False","tag":"Const"}],"tag":"Ap"}],null],["eval 1",[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":"1","tag":"Const"}],"tag":"Ap"},{"contents":"True","tag":"Const"}],"tag":"Ap"}],null],["eval if0",[["A","B","C","x"],[[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"False","tag":"Const"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],null],["eval if1",[["A","B","C","x"],[[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"True","tag":"Const"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],null]],[]],"tag":"Rule"},{"contents":"Because we didn't define an existential quantifier or anything, we just define a judgement $A:A eval$ which says that $A:A$ evaluates to a boolean value. Note that this is inductive so we get the elimination rule for free.","tag":"Paragraph"},{"contents":["Inductive",[["eval Bool",[["A","x"],[[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_Bool","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],null]],[[{"contents":["_eval",1],"tag":"Cases"},[["§P","A"],[[[],[],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[["x"],[[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_Bool","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":2,"tag":"LocalVar"}]],{"contents":1,"tag":"LocalVar"}]],[{"contents":["_eval",1],"tag":"Induction"},[["§P0","§0"],[[[],[],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[["A","x"],[[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_Bool","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":3,"tag":"LocalVar"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]]]],"tag":"Rule"},{"contents":"*Exercise* : Try proving that this involved expression evaluates!","tag":"Paragraph"},{"contents":["Theorem",[["eval-I-example",[[],[],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":"1","tag":"Const"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":"0","tag":"Const"}],"tag":"Ap"},{"contents":"1","tag":"Const"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":"0","tag":"Const"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"},{"contents":"1","tag":"Const"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":"0","tag":"Const"}],"tag":"Ap"},{"contents":"1","tag":"Const"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":"1","tag":"Const"}],"tag":"Ap"},{"contents":"1","tag":"Const"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Ap"}],[[null,[],[],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":"1","tag":"Const"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":"0","tag":"Const"}],"tag":"Ap"},{"contents":"1","tag":"Const"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":"0","tag":"Const"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"},{"contents":"1","tag":"Const"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":"0","tag":"Const"}],"tag":"Ap"},{"contents":"1","tag":"Const"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":"1","tag":"Const"}],"tag":"Ap"},{"contents":"1","tag":"Const"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"}],"tag":"Ap"}],"tag":"Ap"},null],38]]],[]],"tag":"Rule"},{"contents":"* Exercise* : Prove that all expressions in the language $I$ evaluates to a boolean value. One of the subgoals for $if$ has been done already.","tag":"Paragraph"},{"contents":["Theorem",[["IExp eval",[["P"],[[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[{"style":"Prose","subtitle":"Show:"},["P"],[[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},[{"contents":[{"contents":["_IExp",1],"tag":"Induction"},{"contents":0,"tag":"Local"}],"tag":"Elim"},[[{"style":"Abbr","subtitle":"Show:"},[],[],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":"0","tag":"Const"}],"tag":"Ap"},null],[{"style":"Abbr","subtitle":"Show:"},[],[],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":"1","tag":"Const"}],"tag":"Ap"},null],[{"style":"Prose","subtitle":"Show:"},["A","B","C"],[[[],[],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_IExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},[{"contents":[{"contents":["_eval",1],"tag":"Cases"},{"contents":1,"tag":"Local"}],"tag":"Elim"},[[{"style":"Prose","subtitle":"Show:"},["a"],[[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_Bool","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},[{"contents":[{"contents":["_Bool",1],"tag":"Cases"},{"contents":8,"tag":"Local"}],"tag":"Elim"},[[{"style":"Prose","subtitle":"Show:"},[],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"True","tag":"Const"}],"tag":"Ap"}]],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},[{"contents":[{"contents":["_eval",1],"tag":"Cases"},{"contents":2,"tag":"Local"}],"tag":"Elim"},[[null,["b"],[[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_Bool","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":4,"tag":"LocalVar"}],"tag":"Ap"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},[{"contents":"eval Bool","tag":"Defn"},[[null,[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":4,"tag":"LocalVar"}],"tag":"Ap"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},[{"contents":"eval if1","tag":"Defn"},[[null,[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":4,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"True","tag":"Const"}],"tag":"Ap"},[{"contents":[{"contents":9,"tag":"Local"},true,"RHS"],"tag":"Rewrite"},[[null,[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":4,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},[{"contents":7,"tag":"Local"},[]]]]]],[null,[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},null]]]],[null,[],[],{"contents":[{"contents":"_Bool","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},null]]]]]]],[{"style":"Prose","subtitle":"Show:"},[],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"False","tag":"Const"}],"tag":"Ap"}]],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},null]]]]]]]]]],37]]],[]],"tag":"Rule"},{"contents":[1,"The Language B of Boolean Expressions"],"tag":"Heading"},{"contents":"Here we define a new language $B$ of Boolean Expressions, consisting of $top$, $bot$, $_/\\_$, $_\\/_$ and $not_$.","tag":"Paragraph"},{"contents":["Inductive",[["top F",[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":"top","tag":"Const"}],"tag":"Ap"}],null],["bot F",[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":"bot","tag":"Const"}],"tag":"Ap"}],null],["/\\ F",[["A","B"],[[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":[{"contents":[{"contents":"_/\\_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],null],["\\/ F",[["A","B"],[[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":[{"contents":[{"contents":"_\\/_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],null],["not F",[["A"],[[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":[{"contents":"not_","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],null]],[[{"contents":["_BExp",1],"tag":"Cases"},[["§P","§0"],[[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"top","tag":"Const"}],"tag":"Ap"}]],{"contents":1,"tag":"LocalVar"}],[[],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"bot","tag":"Const"}],"tag":"Ap"}]],{"contents":1,"tag":"LocalVar"}],[["A","B"],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":"_/\\_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":3,"tag":"LocalVar"}],[["A","B"],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":"_\\/_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":3,"tag":"LocalVar"}],[["A"],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":"not_","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":2,"tag":"LocalVar"}]],{"contents":1,"tag":"LocalVar"}]],[{"contents":["_BExp",1],"tag":"Induction"},[["§P0","§0"],[[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":"top","tag":"Const"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":"bot","tag":"Const"}],"tag":"Ap"}],[["A","B"],[[[],[],{"contents":[{"contents":3,"tag":"LocalVar"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":3,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":3,"tag":"LocalVar"},{"contents":[{"contents":[{"contents":"_/\\_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],[["A","B"],[[[],[],{"contents":[{"contents":3,"tag":"LocalVar"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":3,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":3,"tag":"LocalVar"},{"contents":[{"contents":[{"contents":"_\\/_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],[["A"],[[[],[],{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":[{"contents":"not_","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}]],{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]]]],"tag":"Rule"},{"contents":"*Exercise*: Devise suitable semantic rules for each expression in $B$.","tag":"Paragraph"},{"contents":["Axiom",[["eval top B",[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":"top","tag":"Const"}],"tag":"Ap"},{"contents":"True","tag":"Const"}],"tag":"Ap"}],null],["eval bot B",[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":"bot","tag":"Const"}],"tag":"Ap"},{"contents":"False","tag":"Const"}],"tag":"Ap"}],null]],[]],"tag":"Rule"},{"contents":"*Exercise*: Prove that all $B$ expressions evaluate to a boolean value:","tag":"Paragraph"},{"contents":["Theorem",[["BExp eval",[["X"],[[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[{"style":"Prose","subtitle":"Show:"},["X"],[[[],[],{"contents":[{"contents":"_BExp","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":"_eval","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},null],149]]],[]],"tag":"Rule"},{"contents":[1,"Compilation"],"tag":"Heading"},{"contents":"Now, we define a relation $_|->_$ that describes a translation, or /compilation/, from $B$ expressions to $I$ expressions. \n\n*Exercise*: Complete this definition with rules for $_\\/_$ and $not_$","tag":"Paragraph"},{"contents":["Inductive",[["|-> top",[[],[],{"contents":[{"contents":[{"contents":"_|->_","tag":"Const"},{"contents":"top","tag":"Const"}],"tag":"Ap"},{"contents":"1","tag":"Const"}],"tag":"Ap"}],null],["|-> bot",[[],[],{"contents":[{"contents":[{"contents":"_|->_","tag":"Const"},{"contents":"bot","tag":"Const"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"}],null],["|-> /\\",[["A","B","A'","B'"],[[[],[],{"contents":[{"contents":[{"contents":"_|->_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":"_|->_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":"_|->_","tag":"Const"},{"contents":[{"contents":[{"contents":"_/\\_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"}],"tag":"Ap"}],null]],[[{"contents":["_|->_",2],"tag":"Cases"},[["§P","§0","§1"],[[[],[],{"contents":[{"contents":[{"contents":"_|->_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"top","tag":"Const"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"1","tag":"Const"}],"tag":"Ap"}]],{"contents":2,"tag":"LocalVar"}],[[],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"bot","tag":"Const"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"}]],{"contents":2,"tag":"LocalVar"}],[["A","B","A'","B'"],[[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":5,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":"_/\\_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":"_=_","tag":"Const"},{"contents":4,"tag":"LocalVar"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":"_|->_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":"_|->_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":6,"tag":"LocalVar"}]],{"contents":2,"tag":"LocalVar"}]],[{"contents":["_|->_",2],"tag":"Induction"},[["§P0","§0","§1"],[[[],[],{"contents":[{"contents":[{"contents":"_|->_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":"top","tag":"Const"}],"tag":"Ap"},{"contents":"1","tag":"Const"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":"bot","tag":"Const"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"}],[["A","B","A'","B'"],[[[],[],{"contents":[{"contents":[{"contents":6,"tag":"LocalVar"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":6,"tag":"LocalVar"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":"_|->_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":"_|->_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":6,"tag":"LocalVar"},{"contents":[{"contents":[{"contents":"_/\\_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":[{"contents":[{"contents":[{"contents":"if_then_else_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},{"contents":"0","tag":"Const"}],"tag":"Ap"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]]]],"tag":"Rule"},{"contents":"Next, we shall define a relation called /evaluation equivalence/, written $X Y:X ~= Y$, which states that $X:X$ and $Y:Y$ evaluate to the same boolean value:","tag":"Paragraph"},{"contents":["Inductive",[["~= eval",[["X","Y","x"],[[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_Bool","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":"_~=_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}],null]],[[{"contents":["_~=_",2],"tag":"Cases"},[["§P","X","Y"],[[[],[],{"contents":[{"contents":[{"contents":"_~=_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[["x"],[[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_Bool","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":3,"tag":"LocalVar"}]],{"contents":2,"tag":"LocalVar"}]],[{"contents":["_~=_",2],"tag":"Induction"},[["§P0","§0","§1"],[[[],[],{"contents":[{"contents":[{"contents":"_~=_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[["X","Y","x"],[[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[],[],{"contents":[{"contents":"_Bool","tag":"Const"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":5,"tag":"LocalVar"},{"contents":2,"tag":"LocalVar"}],"tag":"Ap"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]]]],"tag":"Rule"},{"contents":"*Exercise*: Prove that your compilation is correct, that is, that the translation relation preserves this equivalence:","tag":"Paragraph"},{"contents":["Theorem",[["|-> ~=",[["X","Y"],[[[],[],{"contents":[{"contents":[{"contents":"_|->_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":"_~=_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],[[{"style":"Prose","subtitle":"Show:"},["X","Y"],[[[],[],{"contents":[{"contents":[{"contents":"_|->_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":"_~=_","tag":"Const"},{"contents":1,"tag":"LocalVar"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"},null],412]]],[]],"tag":"Rule"},{"contents":[1,"Going Higher Order"],"tag":"Heading"},{"contents":"$lambda$-expressions in Holbert are written simply as $(x. P)$, describing a function that takes in an argument and returns $P$. When modelling variables in programming languages (or quantifiers in logic), it is common to re-use this lambda mechanism, by representing variable binding using a $lambda$-expression. Substitution therefore becomes mere function application. This technique is called /higher order abstract syntax/. ","tag":"Paragraph"},{"contents":"To add Let expressions to our languages, we just define an evaluation rule that says that a Let expression evaluates the same as replacing the bound variable with the bound expression in the body.","tag":"Paragraph"},{"contents":["Axiom",[["let eval",[["P","x","Q","y"],[[[],[],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":[{"contents":1,"tag":"LocalVar"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}]],{"contents":[{"contents":[{"contents":"_eval_","tag":"Const"},{"contents":[{"contents":[{"contents":"let_in_","tag":"Const"},{"contents":3,"tag":"LocalVar"}],"tag":"Ap"},{"contents":["x",{"contents":[{"contents":2,"tag":"LocalVar"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],"tag":"Lam"}],"tag":"Ap"}],"tag":"Ap"},{"contents":0,"tag":"LocalVar"}],"tag":"Ap"}],null]],[]],"tag":"Rule"},{"contents":"*Exercise*: First, add a rule to the compilation translation relation for $let_in_$ expressions. To define the rule in the most elegant way, you will need a /hypothetical derivation/.","tag":"Paragraph"},{"contents":"*Exercise*: Move the rule $.thm:let eval$ above the compilation correctness $.thm:|-> ~=$ theorem using the arrow buttons on the right. Then re-prove the compilation translation correctness theorem $.thm:|-> ~=$ . If you use a hypothetical derivation, you may find the following /forward reasoning/ rule helpful (move it up before the theorem if you want to use it).","tag":"Paragraph"},{"contents":["Theorem",[["forward",[["P","Q","R","S"],[[[],[],{"contents":3,"tag":"LocalVar"}],[[],[],{"contents":2,"tag":"LocalVar"}],[[],[[[],[],{"contents":3,"tag":"LocalVar"}],[[],[],{"contents":2,"tag":"LocalVar"}]],{"contents":1,"tag":"LocalVar"}],[[],[[[],[],{"contents":1,"tag":"LocalVar"}]],{"contents":0,"tag":"LocalVar"}]],{"contents":0,"tag":"LocalVar"}],[[{"style":"Tree","subtitle":"Show:"},["P","Q","R","S"],[[[],[],{"contents":3,"tag":"LocalVar"}],[[],[],{"contents":2,"tag":"LocalVar"}],[[],[[[],[],{"contents":3,"tag":"LocalVar"}],[[],[],{"contents":2,"tag":"LocalVar"}]],{"contents":1,"tag":"LocalVar"}],[[],[[[],[],{"contents":1,"tag":"LocalVar"}]],{"contents":0,"tag":"LocalVar"}]],{"contents":0,"tag":"LocalVar"},[{"contents":3,"tag":"Local"},[[null,[],[],{"contents":1,"tag":"LocalVar"},[{"contents":2,"tag":"Local"},[[null,[],[],{"contents":3,"tag":"LocalVar"},[{"contents":0,"tag":"Local"},[]]],[null,[],[],{"contents":2,"tag":"LocalVar"},[{"contents":1,"tag":"Local"},[]]]]]]]]],0]]],[]],"tag":"Rule"},{"contents":"*Exercise*: The above $.thm:let eval$ rule assumes /call by name/ evaluation. That is, the expression is substituted into the body as-is. How would you do /call by value/ evaluation instead, where the expression is fully evaluated to $top$ or $bot$ before being substituted?","tag":"Paragraph"}]