CMSC 221/321
Homework set 5
Due: Friday, Nov 11, 2011 at midnight

5.0 [Reading] Lectures 8 and 9.

For 5.1 and 5.2, we will work with the following formalization of
typing derivations using the inference rules (1) through (6)
defined in Figure 4.3.

From any such derivation d of a typing judgement Γ ⊦ e : τ we can
derive three attribute values: the context Γ=context(d), the subject
expression e=subject(d), and the type τ=type(d).

Derivation terms:

   d ::= R1(Γ, c)
       | R2(Γ, x)
       | R3(c, d1, d2)
       | R4(x, d1, d2)
       | R5(x, τ, d)
       | R6(d1, d2)

Constraints:
Valid derivation terms have to satisfy the following constraints.

  R2(Γ,x)        RC2:  x ∈ domain(Γ)
  R3(d1,d2,d3)   RC3a: context(d1) = context(d2) = context(d3)
                 RC3b: type(d1) = Bool
                 RC3c: type(d2) = type(d3)
  R4(x,τ,d1,d2): RC4a: context(d2) = context(d1) ⋃ {x:type(d1)}
                 RC4b: type(d1) = τ
  R5(x,τ,d1)     RC5:  context(d1) = context(d) ⋃ {x: τ}
  R6(d1,d2) :    RC6a: context(d1) = context(d2)
                 RC6b: ∃τ. type(d1) = type(d2) → τ
 
Attribute functions:

  S1: subject(R1(Γ, c)) = Const c
  S2: subject(R2(Γ, x)) = Var x
  S3: subject(R3(d1,d2,d3)) = If(subject(d1),subject(d2),subject(d3))
  S4: subject(R4(x,d1,d2)) = Let(x,subject(d1),subject(d2))
  S5: subject(R5(x,τ,d)) = Fun(x,τ,subject(d))
  S6: subject(R6(d1,d2)) = App(subject(d1),subject(d2))

  C1: context(R1(Γ, c)) = Γ
  C2: context(R2(Γ, x)) = Γ
  C3: context(R3(d1,d2,d3)) = context(d2)
  C4: context(R4(x,d1,d2)) = context(d1)
  C5: context(R5(x,τ1,d1)) = context(d1)\{x}         
  C6: context(R6(d1,d2)) = context(d1)

  T1: type(R1(Γ, c)) = Σ(c) 
  T2: type(R2(Γ, x)) = Γ(x)
  T3: type(R3(d1,d2,d3)) = type(d2)
  T4: type(R4(x,d1,d2)) = type(d2)
  T5: type(R5(x,τ,d1)) = τ -> type(d1)
  T6: type(R6(d1,d2)) = τ2  where type(d1) = τ1 -> τ2


======================================================================
5.1 [35]. Give a full and rigorous proof of the Substitution Lemma
(Lemma 4.9, Lecture 8), using the proof of the Substitution Lemma for
the ok judgement (Lemma 4.4, Lecture 7) as the template.

Proof: By induction on the derivation d of Γ[x: τ] ⊦ e2 : τ', using the
rules of Fig. 4.3.

Let us assume we are given a Γ, e1, and τ such that Γ ⊦ e1 : τ, and a variable
x ∉ domain(Γ). We want to prove that ∀d∈D.P(d), where P is the property given
by:

(2)   P(d) == Γ ⊆ context(d)  ∧  context(d)(x) = τ  ==>
              context(d)\{x} ⊦ [e1/x]subject(d) : type(d)
 

Base Case: d = R1(Γ',c). Then let e2 = subject(d) = Const(c) and τ' =
type(d) = Σ(c), note that context(d) = Γ'.  Then [e1/x]e2 = Const(c)
by the definition of subsitution. By Rule (1), Γ'' ⊦
Const(c) : τ' for any context Γ'', so Γ'' ⊦ [e1/x]e2 : τ' for any
context Γ'', and in particuular for the context Γ'\{x}.

Base Case: d = R2(Γ',y). Then let e2 = subject(d) = y and τ' = type(d)
= Γ'(y), where Γ' = context(d). We can assume the hypotheses Γ ⊆ Γ',
and Γ'(x) = τ. There are two subcases.

(a) y = x: In this case, [e1/x]e2 = e1. We know that Γ ⊦ e1:τ, and
hence Γ'\{x} ⊦ e1 :τ , by the Weakening Lemma (Lemma 4.8) since Γ ⊆ Γ'\{x}.
Hence Γ'\{x} ⊦ [e1/x]e2 : τ. But τ = Γ'(x) = Γ'(y), so Γ'\{x} ⊦ [e1/x]e2 : τ'.

(b) y ≠ x: In this case, [e1/x]e2 = e2 = Var(y). It must be the case
that y ∈ domain(Γ') by the constraint C2, and since y ≠ x, y ∈ domain(Γ'\{x}).
Hence Γ'\{x} ⊦ Var(y):τ' by R2. So Γ'\{x} ⊦ [e1/x]e2 : τ' . [X] 
   
   
Ind Case: d = R3(d1,d2,d3).
Then let e2 = subject(d) = If(e3,e4,e5) where e3 = subject(d1) and
e4 =subject(d2) and e5 = subject(d3).  Let Γ' = context(d) =
context(d1) = context(d2) = context(d3) (by C3 and RC3a). 
By constraints RC3b and RC3c, we know type(d1) = BOOL and type(d2) = type(d3).
Let τ' = type(d2) = type(d3).

We can assume the hypotheses:
(hyp1) Γ ⊆ Γ'
(hyp2) Γ'(x) = τ 

IH1: P(d1)  ==  Γ ⊆ Γ' ∧ Γ'(x) = τ  =>  Γ'\{x} ⊦ [e1/x]e3 : Bool
IH2: P(d2)  ==  Γ ⊆ Γ' ∧ Γ'(x) = τ  =>  Γ'\{x} ⊦ [e1/x]e4 : τ'
IH3: P(d3)  ==  Γ ⊆ Γ' ∧ Γ'(x) = τ  =>  Γ'\{x} ⊦ [e1/x]e5 : τ'

From these induction hypotheses and (hyp1) and (hyp2), we can
conclude

(2) Γ'\{x} ⊦ [e1\x]e3 : Bool.
(3) Γ'\{x} ⊦ [e1\x]e4 : τ'
(4) Γ'\{x} ⊦ [e1\x]e5 : τ'.

Then by rule (3) we have we have:

    Γ'\{x} ⊦ If([e1\x]e3, [e1/x]e4, [e1/x]e5) : τ',

hence
  
    Γ'\{x} ⊦ [e1\x]If(e3,e4,e5) : τ'

by the defn of substituion. Thus Γ'\{x} ⊦ [e1\x]e2 : τ'.  [X]

Ind Case: d = R4(y,τ1,d1,d2).
Then let e2 = subject(d) = Let(y,τ1,e3,e4), where e3 = subject(d1) and
e4 = subject(d2). Let Γ' = context(d) = context(d1), by the defn of context
for R4. Let Γ'' = context(d2) and τ2 = type(d2). Then Γ'' = Γ'[y:τ1]
by the R4 constraint for context, and type(d1) = τ1 by the R4 constraint 
for type. We can assume that the let-bound variable y is chosen so that y ≠ x
and y ∉ FV(e1). We can also assume 

(1)  Γ ⊆ Γ'

since otherwise P(d) is true vacuously. Then since Γ' ⊆ Γ'', we also have

(2)  Γ ⊆ Γ''

IH1: P(d1)  ==  Γ ⊆ Γ'  =>  Γ'\{x} ⊦ [e1/x]e3 : τ1
IH2: P(d2)  ==  Γ ⊆ Γ'' =>  Γ''\{x} ⊦ [e1/x]e4 : τ2

By IH1 and (1):

(3)  Γ'\{x} ⊦ [e1/x]e3 : τ1

By IH2 and (2):

(4) Γ''\{x} ⊦ [e1/x]e4 : τ2

Since Γ''\{x} = (Γ'\{x:τ})[y:τ1], we can conclude from (3), (4)
and typing R4 that:

(5) Γ'\{x} ⊦ Let(y,[e1/x]e3,[e1/x]e4) : τ2

But by the definition of substitution and the assumption 
that y ≠ x and y ∉ FV(e1),

(6)  Let(y,[e1/x]e3,[e1/x]e4) = [e1/x](Let(y,e3,e4)) = [e1/x]e2

Hence by (5) and (6), we have

(7)  Γ'\{x} ⊦ [e1/x]e2 : τ2.      [X]


Ind Case: d = R5(y,τ1,d1).
Then let e2 = subject(d) = Fun(y,τ1,e3), where e3 = subject(d1),
and let Γ' = context(d1) and τ2 = type(d1).

Let Γ'' = context(d1) = Γ'[y:τ] by the R5 constraint for
context.

We can assume that the local let-bound variable y is chosen 
so that y ≠ x and y ∉ FV(e1). We can also assume the hypotheses

(hyp1)  Γ ⊆ Γ'
(hyp2)  Γ'(x) = τ

Since Γ' ⊆ Γ'', we also have

(1)  Γ ⊆ Γ''
(2)  Γ''(x) = Γ'(x) = τ

IH1: P(d1)  ==  Γ ⊆ Γ'' ∧ Γ''(x) = τ  =>  Γ''\{x} ⊦ [e1/x]e3 : τ2

By IH1, (1), and (2), 

(3)  Γ''\{x} ⊦ [e1/x]e3 : τ2

Since Γ''\{x} = (Γ\{x})[y:τ1], we can conclude from (3),
and rule (5),

(4)  Γ''\{x} ⊦ Fun(y,τ1,[e1/x]e3) : τ1 -> τ2

But by the definition of substitution and the assumption 
that y ≠ x and y ∉ FV(e1),

(5)  Fun(y,τ1,[e1/x]e3) = [e1/x]Fun(y,τ1,e3) = [e1/x]e2
	  
Hence by (4) and (5),

     Γ''\{x} ⊦ [e1/x]e2 : τ1 -> τ'  [X]
       
       
Ind Case: d = R6(d1,d2).
Let e2 = App(e3,e4) where e3 = subject(d1) and e4 = subject(d2).  Let
Γ' = context(d) = context(d1) = context(d2), by C6 and constraint
RC6a.  Let τ2 = type(d) and τ1 = type(d3).  By T6 and R6b,
type(d2) = τ1 → τ2.

We assume the hypotheses

(hyp1) Γ ⊆ Γ'
(hyp2) Γ'(x) = τ

IH1: P(d2)  ==  Γ ⊆ Γ' ∧ Γ'(x) = τ  =>  Γ'\{x} ⊦ [e1/x]e3 : τ1 → τ2
IH2: P(d3)  ==  Γ ⊆ Γ' ∧ Γ'(x) = τ    =>  Γ'\{x} ⊦ [e1/x]e4 : τ1

By IH1, IH2 and (hyp1), (hyp2):

(3) Γ'\{x} ⊦ [e1\x]e3 : τ1 → τ2
(4) Γ'\{x} ⊦ [e1\x]e4 : τ1

Then by rule (6):

(5) Γ'\{x} ⊦ App([e1\x]e3, [e1\x]e4) :τ2

and so, by the definition of substitution,

(6) Γ'\{x} ⊦ [e1\x]App(e3,e4) : τ2

Hence,

(7) Γ'\{x} ⊦ [e1\x]e2 : τ2    [XX]


======================================================================
5.2 [25]. Prove Lemma 4.11 (Lecture 8), showing that an expression
(in a given type context) has a unique type.

Lemma 4.11 [Unique types] If Γ ⊦ e : τ and Γ ⊦ e : τ', then τ = τ'

Proof: Straightforward induction on the derivation of Γ ⊦ e: τ.


We want to prove that ∀d∈D.P(d), where P is the property given
by:

(0) P(d) == ∀d'. context(d) = context(d') ∧ subject(d) = subject(d')  
                 => type(d) = type(d')              [defn]
(1) ∀d. P(d)                                        [TBS]
(2) induction on structure of d
  (3) case: d = R1(Γ, c)                            [case hyp] 
    (4) subject(d) = Const c                        [S1] 
    (5) type(d) = Σ(c)                              [T1] 
    (6) context(d) = Γ                              [C1]
    (6) Let d' ∈ Deriv                              [decl]
    (7) subject(d') = subject(d) 
       ∧ context(d') = context(d)                   [hyp]
    (8) subject(d') = Const(c)                      [7,4]
    (9) context(d') = Γ                             [7,6]
    (10) d' = R1(Γ',c)                              [8, 9, Invert S1, C1]
    (11) type(d') = Σ(c)                            [T1]
    (12) type(d') = type(d)                         [11,5]
    (13) P(d)                                       [7,12, => Intro; 6, ∀ Intro; QED case] 

  (20) case: d = R2(Γ, x)                           [case hyp]
    (21) subject(d) = Var x                         [S2] 
    (22) context(d) = Γ                             [C2]
    (23) type(d) = Γ(x)                             [T2]
    (24) Let d' ∈ Deriv                             [decl]
    (25) context(d') = context(d) ∧ 
         subject(d') = subject(d)                   [hyp]
    (26) subject(d') = Var x                        [21,25]
    (27) context(d') = Γ                            [22,25]
    (28) d' = R2(Γ, x)                              [26,27, Invert S2, C2] 
    (29) type(d') = Γ(x)                            [T2]
    (30) type(d) = type(d')                         [23,29] 
    (31) P(d)                                       [25,30, => Intro; 24, ∀ Intro; QED case]

  (40) case: d = R3(d1, d2, d3)                     [case hyp]
    (41) subject(d) = If(subject(d1), 
                         subject(d2), 
                         subject(d3))               [S3] 
    (42) context(d) = context(d1)                   [C3]  
    (43) context(d1) = context(d2)                  [RC3a]
    (44) type(d) = type(d2)                         [T3]
    (45) Let d' ∈ Deriv                             [decl]
    (46) subject(d) = subject(d') ∧
         context(d) = context(d')                   [hyp]
    (47) subject(d') = If(subject(d1),              
                          subject(d2), 
                          subject(d3))              [46,41]
    (48) d' = R3(d1',d2',d3')                       [47, invert subject]
    (49) subject(d') = If(subject(d1'),
                          subject(d2'),
			  subject(d3'))             [48,S3]
    (50) subject(d2') = subject(d2)                 [46,41,49]
    (51) context(d') = context(d2')                 [48,C3]
    (52) context(d2') = context(d2)                 [42,43,46,51]
    (53) P(d2)                                      [I.H.]
    (54) type(d2') = type(d2)                       [50,52,53]
    (55) type(d') = type(d2')                       [48,T3]
    (56) type(d') = type(d)                         [44,55]
    (57) P(d)                                       [46,56, => Intro;
                                                     45, ∀ Intro;
                                                     QED case]

  (60) case: d = R4(x,τ,d1,d2)                      [case hyp] 
    (61) subject(d) = Let(x, τ, 
                          subject(d1), 
                          subject(d2))              [S4] 
    (62) context(d) = context(d1)                   [C4]
    (63) context(d2) = context(d1) ⋃ {x:τ}          [RC4a] 
    (64) type(d) = type(d2)                         [T4]
    (65) Let d' ∈ Deriv                             [decl]
    (66) subject(d) = subject(d') ∧
         context(d) = context(d')                   [hyp]
    (67) d' = R4(v,τ,d1',d2')                       [61,66, Invert S4]
    (68) subject(d') = Let(x, τ,
                           subject(d1'),
			   subject(d2'))            [67,S4]
    (69) subject(d2') = subject(d2)                 [61,68]
    (70) type(d') = type(d2')                       [67,T4]
    (71) context(d2') = context(d1') ⋃ {x:τ}        [67,RC4a]
    (72) context(d') = context(d1')                 [67,C4]
    (73) context(d1') = context(d1)                 [2,66]
    (74) context(d2') = context(d2)                 [63,71,73]
    (75) P(d2)                                      [I.H.]
    (76) type(d2') = type(d2)                       [69,74,75]
    (77) type(d') = type(d)                         [64,70,77]
    (78) P(d)                                       [69,74, => Intro;
                                                     65, ∀ Intro;
						     QED case] 


 (80) case: d = R5(x,τ,d1)                          [case hyp]
    (81) subject(d) = Fun(x, τ, subject(d1))        [S5]
    (82) context(d1) = context(d) ⋃ {x:τ}           [RC5] 
    (83) type(d) = τ → type(d1)                     [T5] 
    (85) Let d' ∈ Deriv                             [decl] 
    (86) subject(d) = subject(d') ∧
         context(d) = context(d')                   [hyp]
    (87) d' = R5(x,τ,d1')                           [81,86, Invert S5]
    (88) type(d') = τ → type(d1')                   [T5]
    (89) subject(d') = Fun(x,τ,subject(d1'))        [87,S5]
    (90) subject(d1') = subject(d1)                 [81,86,89]
    (91) context(d1') = context(d') ⋃ {x:τ}         [87,RC5]
    (92) context(d1') = context(d1)                 [82,86,91]
    (93) P(d1)                                      [I.H.]
    (94) type(d1') = type(d1)                       [90,92,93]
    (95) type(d') = type(d)                         [83,88,94]
    (96) P(d)                                       [86,95, => Intro;
                                                     85, ∀ Intro;
						     QED case]                                

 (100) case: d = R6(d1,d2)                          [case hyp]
    (101) subject(d) = App(subject(d1),
                           subject(d2))             [S6]
    (102) context(d) = context(d1)                  [C6]
    (103) type(d1) = type(d2) → τ                   [RC6b]
    (104) type(d) = τ                               [103,T6]
    (104) Let d' ∈ Deriv                            [decl]
    (105) subject(d) = subject(d') ∧
          context(d) = context(d')                  [hyp]
    (106) d' = R6(d1',d2')                          [101,105, Invert S6]
    (107) subject(d') = App(subject(d1'),
                            subject(d2'))           [106,S6]
    (107) subject(d1') = subject(d1)                [101,105,107]
    (108) context(d') = context(d1')                [106,C6]
    (109) context(d1') = context(d1)                [102,105,108]
    (110) P(d1)                                     [I.H.]
    (111) type(d1') = type(d1)                      [107,109,110]
    (112) type(d') = type(d)                        [104,111,RC6b]
    (113) P(d)                                      [105,112, => Intro;
                                                     104, ∀ Intro;
						     QED case]

(120) ∀d. P(d)                                      [cases, I.P.; QED]

 
5.2 [10]. Prove part (5) of the Inversion Lemma (Lemma 4.8, Lecture
8). Solution by: Carsen Berger

 (5) Γ ⊦ Fun(x,τ1,e) : τ  ==>  ∃τ2. τ = τ1 → τ2 and Γ[x:τ'] ⊦ e : τ2

A derivation of Γ ⊦ Fun(x,τ1,e) : τ must have rule Typ(5) as its final rule, because that is the
only rule that matches the expresion Fun(x,τ1,e). Hence the premise of that rule, namely
Γ[x:τ1] ⊦ e : τ2, must be the conclusion of the subderivation. But in order for Γ ⊦ Fun(x,τ1,e) : τ
to match the conclusion of Typ(5), we must have τ = τ1 → τ2.
Therefore ∃τ2. τ = τ1 → τ2 & Γ[x:τ1] ⊦ e : τ2.


5.3 [10] Give an informal proof of Lemma 4.10(3) (cannonical forms
for function types). Solution by: Matt Lee

Lemma 4.10 [Canonical Forms]:
(3) v a value and ⊦ v : τ1 → τ2  =>
    v = Fun(x, τ, e) (for some x, τ, e), or
    v = Const(primop), where primop ∈ PrimFun, or
    v = App(Const(primop), v),  where primop ∈ PrimFun and v is a value
        (assuming primop is always binary)
        
We have the following definitions of values:

Num = {Num(n) | n ∈ Nat}                        
Bool = {Bool(b) | b ∈ {True, False}}            
PrimFun = {Plus, Times, Minus, Eq, Lt, ...}    
PrimPA = {App(op,Num(n)) | v ∈ Value, op ∈ PrimFun}
Fun = {Fun(x,τ,e) | Fun(x,τ,e) closed}         

Thus a value v is one of these 5.
Suppose v a value and ⊦ v : τ1 → τ2.  Then we can have 5 cases:
(1) if v = Num(n), then as Int ≠ τ1 → τ2, the claim holds vacuously.
(2) if v ∈ Bool(b), then Bool ≠ τ1 → τ2, and again the claim holds vacuously
(3) if v ∈ PrimFun, then v = Const(primop), where primop ∈ PrimFun.
(4) if v ∈ PrimPA, then v = App(primop,v') for some v' ∈ Value
    and primop ∈ PrimFun
(5) if v ∈ Fun, then v = Fun(x,τ1,e), a closed fun expr for some x,τ1,e