# 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 ⟶`

and _{v}* t"`t' ⟶`

, and prove both, showing each βᵥ-reduction step with the redex underlined._{v}* t"

For example:

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

`(λx. λx. x) (λy. λz. y) (λy. λz. z) ⟶* λy. λz. z`

`(λx. λy. y x) (y y) z ⟶* z (y y)`

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

`(λ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`

.

Write λ-terms

`leaf`

and`node`

that satisfy the following:`leaf n l = l node t`

_{1}t_{2}n l = n (t_{1}n l) (t_{2}n l)(There’s almost nothing to do here.) The term

`leaf`

is a tree consisting of just one leaf; the term`node t`

is a tree consisting of a root node with_{1}t_{2}`t`

and_{1}`t`

as its child subtrees. Added: For example, the tree above can be constructed by_{2}`node (node leaf leaf) leaf`

.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`

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) = c`

._{3}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 t`

_{1}t_{2}) = t_{1}left leaf = leaf right (node t_{1}t_{2}) = t_{2}right leaf = leaf

## 3. Hailstone sequences

The hailstone sequence starting with *n* is defined as follows:

*a*_{0}=*n*.- If
*a*_{n}is even,*a*_{n + 1}=*n*/2. - If
*a*_{n}is odd,*a*_{n + 1}= 3*n*+ 1.

The Collatz conjecture is that for all *n* > 0, the hailstone sequence starting with *n* eventually reaches 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`

.Challenge (0 points): Write

`divmod`

too.