# Homework 2: Untyped λ-calculus

• Due: 02/08 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). If you prefer, you can write your solutions to problems 2-3 as plain text files. Submit all files in Sakai.

## 1. Lambda calculations

Prove each of the following statements. If the statement is of the form `t ⟶* t'`, show each call-by-value β-reduction step with the redex underlined. If the statement is of the form `t = t'`, find a third term `t"` such that `t ⟶v* t"` and `t' ⟶v* t"`, and prove both, showing each βᵥ-reduction step with the redex underlined.

For example:

``````    (λx. x) (λy. y) (λz. z)
―――――――――――――――

⟶ (λy. y) (λz. z)
―――――――――――――――

⟶ (λz. z)``````
1. `(λx. λx. x) (λy. λz. y) (λy. λz. z) ⟶* λy. λz. z`
2. `(λx. λy. y x) (y y) z ⟶* z (y y)`
3. `(λx. λy. λz. x z (y z)) (λx. λy. x) (λx. λy. x) = λz. z`
4. `(λm. λn. λs. λz. m s (n s z)) x (λs. λz. z) = (λm. λn. λs. λz. m s (n s z)) (λs. λz. z) x`

## 2. Church trees

Added explanation: In this problem, we’ll explore how to represent binary trees (without labels) as λ-terms. Just as the Church numeral for a number is a function of two arguments, `s` and `z`, that applies `s` to `z` that number of times, we want to represent a tree as a function of two arguments, `n` and `l`, that applies `n` to `l` in the same “shape” as the tree. For example, the tree below is represented by `λn. λl. n (n l l) l`.

1. Write λ-terms `leaf` and `node` that satisfy the following:

``````      leaf n l = l
node t1 t2 n l = n (t1 n l) (t2 n l)``````

(There’s almost nothing to do here.) The term `leaf` is a tree consisting of just one leaf; the term `node t1 t2` is a tree consisting of a root node with `t1` and `t2` as its child subtrees. Added: For example, the tree above can be constructed by `node (node leaf leaf) leaf`.

2. Write a λ-term `isleaf` that tells whether a tree’s root is a leaf node. For example,

``````            isleaf leaf = true
isleaf (node leaf leaf) = false``````
3. Write a λ-term `size` that counts the number of nodes (including leaves) in a tree (as a Church numeral). For example, `node leaf leaf` has three nodes, so `size (node leaf leaf) = c3`.

4. Challenge (0 points): Write λ-terms `left` and `right` that return the left and right child subtrees, respectively, of a tree’s root. That is, they should satisfy:

`````` left (node t1 t2) = t1
left  leaf        = leaf
right (node t1 t2) = t2
right  leaf        = leaf``````

## 3. Hailstone sequences

The hailstone sequence starting with n is defined as follows:

• a0 = n.
• If an is even, an + 1 = n/2.
• If an is odd, an + 1 = 3n + 1.

The Collatz conjecture is that for all n > 0, the hailstone sequence starting with n eventually reaches 1.

1. Write a λ-term that, given the Church numeral for n > 0, returns `tru` if the hailstone sequence starting with n eventually reaches 1; otherwise, it diverges.

You may assume that you have a function `divmod` such that for any Church numerals `x` and `y`, `divmod x y` is a pair containing the quotient and remainder of `x` divided by `y`.

2. Challenge (0 points): Write `divmod` too.