This assignment has 10 points.
When answering questions, refer to the following definition of the lambda calculus with booleans and recursive functions (LBR from now on):
Syntax:
(types) t ::= bool | t1 -> t2
(expressions) e ::= x | true | false | if e1 then e2 else e3 | fun f (x:t1):t2 = e | e1 e2
(values) v ::= true | false | fun f (x:t1):t2 = e
(contexts) G ::= . | G,x:t
Call-by-value Evaluation:
e --> e'
------------------------------------------------------- (E-if0)
if e then e1 else e2 --> if e' then e1 else e2
------------------------------------- (E-if1)
if true then e1 else e2 --> e1
------------------------------------- (E-if2)
if false then e1 else e2 --> e2
e1 --> e1'
-------------------- (E-app1)
e1 e2 --> e1' e2
e2 --> e2'
-------------------- (E-app2)
v e2 --> v e2'
------------------------------------------------------------------- (E-app3)
(fun f(x:t1):t2 = e) v --> e[v/x][(fun f(x:t1):t2 = e)/f]
Typing:
----------------- (T-var)
G |-- x : G(x)
--------------------- (T-true)
G |-- true : bool
---------------------- (T-false)
G |-- false : bool
G |-- e : bool G |-- e1 : t G |-- e2 : t
----------------------------------------------------- (T-if)
G |-- if e then e1 else e2 : t
G, f:t1->t2, x:t1 |-- e : t2
----------------------------------------- (T-fun)
G |-- fun f (x:t1):t2 = e : t1 -> t2
G |-- e1 : t1 -> t2 G |-- e2 : t1
------------------------------------------ (T-app)
G |-- e1 e2 : t2
| 1. [1 point] Let the
expression e be the following: (fun
foo (x:bool -> bool) = Give a complete typing derivation for the judgement below. Mark each level of the derivation with the name of the rule (T-var, T-if, etc.) that you used to make the corresponding inference. . |- e : (bool -> bool) -> bool -> bool 3. [2 points] Conjecture: In LBR, if G |- e : t and e' --> e then G |- e' : t. Prove it or give a counterexample. 4. [1 point] Conjecture: For any LBR expression e and any type t1 there is at most one type t2 such that (fun f(x:t1):t2 = e) is well typed. Prove it or give a counter example. 5. [6 points] Consider adding trees with leaf node elements of type t (a "t tree") to the simple language above. The additional types, expressions, and values are as follows: t ::= ... (as above) ... | t tree e ::= ... (as above) ... | Leaf(e) | Node(e1,e2) | treecase e of (Leaf x => e1 | Node(x,y) => e2) v ::= ... (as above) ... | Leaf(v) | Node(v1,v2) Here are the operational rules:
e --> e' e1 --> e1' e2 --> e2'
------------------------ (L)
------------------------------------- (N1)
------------------------------------- (N2)
e --> e' --------------------------------------------------------------------------------------------------------------------------- (T1) treecase e of (Leaf x => e1 | Node(x,y) => e2) --> treecase e' of (Leaf x => e1 | Node(x,y) => e2)
--------------------------------------------------------------------------------- (T2) treecase Leaf(v) of (Leaf x => e1 | Node(x,y) => e2) --> e1[v/x]
------------------------------------------------------------------------------------------------ (T3) treecase Node(v1,v2) of (Leaf x => e1 | Node(x,y) => e2) --> e2[v1/x][v2/y]
Part (a). [2 points] Give typing rules for for the Leaf, Node and treecase expressions.
Part (b). [4 points] Prove the cases of the Preservation Theorem that pertain to the Leaf, Node and treecase expressions. You may assume that the Exchange, Weakening and Substitution Lemmas have been proven for you.
Exchange: If G1,x1:t1,x2:t2,G2 |- e : t then G1,x2:t2,x1:t1,G2 |- e : t.
Weakening: If G |- e : t and x not in Dom(G) then G,x1:t1 |- e : t.
Substitution: If G,x1:t1 |- e : t and |- v1 : t1 then G |- e[v1/x1] : t.
|