Homework 5: Simply-typed λ

• Due: 03/22 at 11:55pm
• Points: 15 (each question 5 points)

Please prepare your solutions as a PDF file (scanned handwriting is okay, but no .doc or .docx, please). Submit your PDF file in Sakai.

1. Practice with simply-typed λ

Consider the following function of type Nat→Nat in PCF:

double ≡ fix (λf:___. λx:Nat. if iszero x then 0 else succ (succ (f (pred x))))

1. What should the type of f be (fill in the ___)?

2. Write the typing derivation for double : Nat→Nat. To avoid repeating yourself, feel free to define new names like t1 ≡ pred x or Γ1 ≡ x:Nat.

2. letpair

In Python, we can write things like (a, b) = p, which is equivalent to a = p[0]; b = p[1] if p is a pair. Let’s add a similar construct to our extended λ-calculus:

t ::= ...
      letpair {x1, x2} = t3 in t4

We could define this as syntactic sugar in terms of .1 and .2:

(letpair {x1, x2} = t3 in t4) ≡ (let x1 = t3.1 in let x2 = t3.2 in t4)

For example,

letpair {x, y} = {0, true} in if y then succ x else x ⟶ succ 0

But suppose that we want to get rid of .1 and .2 and make letpair the only way to un-pair pairs.

1. Write .1 and .2 as syntactic sugar in terms of letpair (fill in the ___):

   t.1 ≡ ___
   t.2 ≡ ___

2. Write evaluation and typing rules for letpair.

3. Redefining NB

For this question, we’ll use the simply-typed λ-calculus with sum types (<·>, inl, inr, case), the unit type (Unit, unit), and recursive types (μ). Don’t use fix or built-in Bool or Nat.

We don’t need Booleans or numbers to be built in; we can define them ourselves.

1. Write a definition for Bool, and then use it to define

    tru : Bool
    fls : Bool
   test : Bool → Nat → Nat → Nat

   Recall that test is like if but always evaluates all its arguments; here, the “then” and “else” parts are (arbitrarily) restricted to be of type Nat. Your definitions should satisfy:

   test tru x y = x
   test fls x y = y

2. Write a definition for Nat, and then use it to define

     zro : Nat
     scc : Nat → Nat
   iszro : Nat → Bool
     prd : Nat → Nat

   Please use isorecursive types, so do use fold and unfold where needed. Since I neglected to talk about fold and unfold, you don’t need to use them if you don’t want to. Your definitions should satisfy:

       iszro zro = tru
   iszro (scc x) = fls
         prd zro = zro
     prd (scc x) = x