Assignment #4: Typed Lambda Calculus

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):



(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]





----------------- (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) =
               (fun bar (y: bool) = if y then (x false) else (foo x true)))

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.  

a) Assume D is a set of variables.  ie:

D ::= . | D,x

Define a collection of interference rules for the judgement D |- e that determines when the free variables of expression e are subset of the variables in D.  (you may put simple set-theoretic expressions like "x D" in the premises of your judgements where necessary).  An expression is closed if and only if:

 . |- e

b) Prove that if . |- e and e --> e' then . |- e'.