This assignment has 5 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. [1 point] The Curry-Howard Isomorphism suggests that the typed lambda calculus (with non-recursive functions and pairs, for instance) can be thought of as a logic instead of a programming language (intuitionistic propositional logic to be precise). What happens if you add recursive functions to the programming language like in LBR? Will the result still serve as a useful logic (ie: can LBR be interpreted as a useful logic)? Explain your answer. Hint: think about the various components of the isomorphism (programs = proofs, types = propositions/conjectures, inhabited types = true theorems, ...). Which one is useful answering this question? Where did I put the italics??? ************************************************************************ Ungraded Practice Question: A closed term (expression) is a term that has no free variables. Call-by-value evaluation of LBR preserves the closure property on terms. In other words, if you start with a closed term and evaluate for any number of steps, the result will also be a closed term.
|