Written Assignment - Solutions

Arithmetic Expressions

Task 1) Arithmetic Expressions with plus

Evaluation gets stuck for ill-typed terms (anti-progress?:-).

We sketch the proof by induction on the structure of a stuck term (the typing rules should be clear). We do this only for equal and plus at the toplevel, other cases being similar. If evaluation gets stuck there are always two cases to consider: either both arguments are values or at least one of them is not a value. If both are values, then a case distinction yields "ill-typedness" , because there are rules for all well-typed cases. If at least one of them is not a value, then evaluation got stuck in the argument, and we can apply the induction hypothesis.

Task 2) Termination

Here is a function "weight" that maps expressions to naturals:

    weight( t )                   = 0 for t ∈ {zero, true, false}
    weight( f(t) )                = weight(t) + 1 for f ∈ {isZero, succ, pred}
    weight( if c then t else e  ) = weight(c)+weight(t)+weight(e) + 1 
    weight( plus a b  )           = 2*weight(a)+weight(b) + 1 
  

Then we just need to observe these facts:

Proposition: If t → t', then weight(t) > weight(t')

This is proved by induction on the structure of t.

Proposition: There is no nonterminating chain of reductions. (Obviously, no expression can have a negative weight.)

Please note that "normal form" is not the same as "value": A normal form is just an expression that cannot be reduced (it might just be an expression that is stuck). Of course the safety property (progress+preservation) tells us that a well-typed term will not reduce to an ill-typed term, but this is irrelevant for the question at hand.

Task 3) Lists and lambda calculus

We use x,y,z for elements, xs, ys, zs for lists, f for functions. The example applications do not follow any evaluation strategy like call-by-name or call-by-value strictly, instead we apply beta reduction freely wherever we can, and sometimes use numbers 1,2,3 and lists [1,2,3] as abbreviations (this keeps the examples reasonably small).

        sum [1,2,3] = sum (\c.\n.c 1 (c 2 (c 3 n)))
        →  (\c.\n.c 1 (c 2 (c 3 n))) (\x.\y.plus x y) zero
        →* (\n.plus 1 (plus 2 (plus 3 n) zero
        →  plus 1 (plus 2 (plus 3 zero) 
        →* 6
        

        length [1,2,3] = length (\c.\n.c 1 (c 2 (c 3 n)))
        →  (\c.\n.c 1 (c 2 (c 3 n)))  (\x.\y.succ y) zero
        →* (\n. (\x.\y.succ y) 1 ((\x.\y.succ y) 2 ((\x.\y.succ y) 3 n) zero
        →  (\x.\y.succ y) 1 ((\x.\y.succ y) 2 ((\x.\y.succ y) 3 zero)
        →* (\y. succ y) ((\y.succ y) ((\y.succ y) zero))
        →* succ succ succ zero
        

        append [1] [2,3] = append (\c.\n. c 1 n) (\c.\n.c 1 (c 2 n))
        →  (\c.\n. [1] c ([2,3] c n))

        length(append [1] [2,3]) 
        →* length (\c.\n. [1] c ([2,3] c n))
        →  (\c.\n. [1] c ([2,3] c n)) (\x.\y.succ y) zero
        →  [1] (\x.\y.succ y) ([2,3] (\x.\y.succ y) zero)
        =  (\c.\n. c 1 n) (\x.\y.succ y) ([2,3] (\x.\y.succ y) zero)
        →* (\x.\y.succ y) 1 ([2,3] (\x.\y.succ y) zero)
        →* (\x.\y.succ y) 1 ((\x.\y.succ y) 2 ((\x.\y.succ y) 3 zero))
        →* succ succ succ zero
        

        map (\x.(plus x 1)) [1,2] = map (\x.(plus x 1)) (\c.\n. c 1 (c 2 n))
        →  (\xs. \c \n. xs (\y.\ys. c (\x.(plus y 1)) n)) (\c.\n. c 1 (c 2 n))
        →  \c \n. (\c'.\n'. c' 1 (c' 2 n')) (\y.\ys. c (\x.(plus y 1)) n
        →  \c \n. (\n'. (\y.\ys. c (\x.(plus y 1)) 1 ((\y.\ys. c (\x.(plus y 1)) 2 n')) n
        →  \c \n. (\y.\ys. c (\x.(plus y 1)) 1 ((\y.\ys. c (\x.(plus y 1)) 2 n)
        →* \c \n. c 2 (c 3 n)
        = [2,3]
        

          [z] stands for (\c''.\n''. c'' h n''))

        reverse [1,2,3] = reverse (\c'.\n'. c' 1 (c' 2 (c' 3 n')))
        = (\xs. \c.\n. (xs (\z.\zs. append zs [z]) n) c n) [1,2,3]
        → \c.\n. ([1,2,3] (\z.\zs. append zs [z]) n) c n
        = \c.\n. (\c'.\n'. c' 1 (c' 2 (c' 3 n'))) (\z.\zs. append zs [z]) n) c n
        →  \c.\n. (\c'.\n'. c' 1 (c' 2 (c' 3 n'))) (\z.\zs. append zs [z]) c n
        →* \c.\n. ((\z.\zs. append zs [z]) 1 ((\z.\zs. append zs [z]) 2 ((\z.\zs. append zs [z]) 3 n) c n
        →* \c.\n. (append (append (append n [3]) [2]) [1]) c n
        →* \c.\n. [3,2,1] c n
        =  [3,2,1]
        

Typing Rules

Task 4) T-Eta Rules

The T-Eta rule is admissible, because every derivation that ends with T-Eta has the following structure:

                             Γ |- t: T1 → T2 
      _______________     ____________________
T-Var                                           (weakening) (x ∉ fv(t))
      Γ,  x:T1 |- x: T1    Γ, x:T1 |- t: T1 → T2 
      ________________________________________
                                                T-App 
             Γ, x:T1 |- t x: T2
         _________________________
                                    T-Abs 
          Γ |- \x:T1. t x: T1 → T2
         _________________________
                                    T-Eta (x ∉ fv(t))
              Γ |- t: T1 → T2

( The weakening rule is a rule that lets you add new assumptions to a proof, provided they don't interfere with it. For example, weakening lets you infer that if the moon is made of green cheese then 1+1=2. )

If we arrive at Γ |- t: T₁ → T₂ with T-Eta, we must already have had a proof of Γ |- t: T₁ → T₂! The smallest derivation of Γ |- t: T₁ → T₂ does not use T-Eta.

Propositions 9.3.1 holds, because the admissible T-Eta rule does not have an effect on the form and number of typings we can derive.

9.3.3 also holds, but the "moreover, there is just one derivation of this typing" part does obviously not hold, because there can be infinitely many derivations for a type T₁ → T₂. There is however exactly one smallest derivation in that infinite set of derivations.

Task 5) T-Eta and subtyping

Here are the rules next to each other:

    Γ |- \x:T1. t x: T1 → T2
 _________________________    
                           T-Eta (x ∉ fv(t))
       Γ |- t: T1 → T2

  T1 <: S1 S2 <: T2
 _______________________
                         S-Arrow
  S1 → S2 <: T1 → T2

We show the '⇒' direction: If Γ ⊢ t: T with T-Eta then Γ ⊢ t: T with S-Arrow

We are only interested in derivation that use T-Eta and that make use of subtyping, the other ones can be removed as seen above. A proof with T-Eta and subtyping axioms will look as follows

      _______________
T-Var
      Γ,  x:T1 |- x: T1   T1 <: S1                Γ |- t: S1 → S2 
      ______________________________          ____________________
T-Sub                                                             (weakening) (x ∉ fv(t))
      Γ,  x:T1 |- x: S1                         Γ, x:S1 |- t: S1 → S2 
      __________________________________________________________
                                                T-App 
             Γ, x:T1 |- t x: S2                                     S2 < T2
         ____________________________________________________________________
                                                                              T-Sub
             Γ, x:T1 |- t x: T2
         _________________________
                                    T-Abs 
          Γ |- \x:T1. t x: T1 → T2
         _________________________
                                    T-Eta (x ∉ fv(t))
              Γ |- t: T1 → T2

So to prove Γ |- t: T₁ → T₂, we needed Γ |- t: S₁ → S₂, T₁ <: S₁ and S₂ < T₂. But these are just what we need to apply S-Arrow. Every use of T-Eta can be replaced in this way.

Now the other direction: If Γ |- t: T with S-Arrow then Γ |- t: T with T-Eta

This is simple now, replace every occurrence of S-Arrow with the derivation tree fragment above. The resulting derivation is a well-formed derivation of Γ |- t: T that uses only T-Eta and no S-Arrow.

Task 6) Progress in FJ[optional]

Task 7) Exercise 22.3.9 (pp. 325-326 of TAPL) [optional]

These solutions will be provided later.