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.
(λ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,
z, that applies
z that number of times, we want to represent a tree as a function of two arguments,
l, that applies
l in the same “shape” as the tree. For example, the tree below is represented by
λn. λl. n (n l l) l.
nodethat 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
leafis a tree consisting of just one leaf; the term
node t1 t2is a tree consisting of a root node with
t2as its child subtrees. Added: For example, the tree above can be constructed by
node (node leaf leaf) leaf.
Write a λ-term
isleafthat tells whether a tree’s root is a leaf node. For example,
isleaf leaf = true isleaf (node leaf leaf) = false
Write a λ-term
sizethat counts the number of nodes (including leaves) in a tree (as a Church numeral). For example,
node leaf leafhas three nodes, so
size (node leaf leaf) = c3.
Challenge (0 points): Write λ-terms
rightthat 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.
Write a λ-term that, given the Church numeral for n > 0, returns
truif the hailstone sequence starting with n eventually reaches 1; otherwise, it diverges.
You may assume that you have a function
divmodsuch that for any Church numerals
divmod x yis a pair containing the quotient and remainder of
Challenge (0 points): Write