Week 14: Exercises

1. Free Variables

  1. Write a Haskell datatype Term that represents a λ-calculus term.

  2. Write a function isFree :: String -> Term -> Bool that determines whether a variable occurs free in a term.

  3. Write a function freeVars :: Term -> [String] that computes the set of free variables in a term.

2. Substitution

Evaluate the following lambda-calculus substitutions:

  1. ((xyz)[x := y])[y := z]

  2. ((λx.xyz)[x := y])[y := z]

  3. (λy.yyz)[x := yz]

  4. (λy.x(λx.x))[x := λy.xy]

  5. (y(λv.xv))[x := λy.vy]

3. Substitution in Haskell

Write a Haskell function subst :: Term -> String -> Term -> Term that performs substitution in a lambda-calculus term.

4. Substitution Properties

True or false? If false, provide a counterexample.

  1. M[x := P][y := Q] ≡ M[y := Q][x := P]

  2. FV(M[x := N]) = FV(M) ∪ FV(N)

  3. M[x := v][v := P] ≡ M[x := P]

5. α-Equivalence

Which of the following terms are α-equivalent to (λz.zxz)((λy.xy)x) ?

  1. (λy.yxy)((λz.xz)x)

  2. (λx.xyx)((λz.yz)y)

  3. (λy.yxy)((λy.xy)x)

  4. (λv.(vx)v)((λu.uv)x)

6. Testing α-Equivalence

Write a function alphaEq :: Term -> Term -> Bool that determines whether two terms are α-equivalent.

7. β-Normal Form

Reduce the following terms to β-normal form:

  1. (λz.zxz)((λy.xy)x)

  2. (λx.x(x(yz))x)(λu.uv)

  3. (λxy.xyy)(λu.uyx)

8. β-Redexes

Recall that normal-order reduction always reduces the leftmost outermost β-redex in a term. An outermost redex is one that is not contained in any other redex.

Write a Haskell function leftmost :: Term -> Maybe Term that finds and returns the leftmost outermost β-redex in a term, or Nothing if there is none.

9. Call By Name

Call-by-name reduction is like normal-order reduction, but does not perform reductions inside an abstraction. For example, this evaluation strategy will perform no more reductions on the term λx.(λy.y)z. The normal-order strategy will reduce this term to λx.z.

Write a Haskell function evalByName :: Term -> Term that evaluates a term using call by name. (If the term has no normal form, your function may not terminate.)

10. Call By Value

Call-by-value reduction is like call-by-name reduction, but is strict: it evaluates a function's argument before calling the function.

Write a Haskell function evalByValue :: Term -> Term that evaluates a term using call by value.

11. Church Booleans

In the lambda calculus, the Church booleans are defined as follows:

true = λx.λy.x

false = λx.λy.y


We can now define a function


if = λb.λx.λy.bxy


that works like if/then/else in Haskell. For example,


if false (aa) (bb) → bb


Define functions for logical and, or, and not.


12. Pairs

In the lambda calculus, we may represent the pair (x, y) by the function

λb.if b x y


  1. Define a function pair that takes two values x and y and returns a pair.

  2. Define functions fst and snd that return the first and second elements of a pair.

13. Church Numerals

The Church numerals are one possible way to encode the integers in the lambda calculus:

0 = λf.λx.x

1 = λf.λx.fx

2 = λf.λx.f(fx)

…


  1. Write a Haskell function makeNum :: Int -> Term that constructs a Church numeral.

  2. Write a Haskell function decode :: Term -> Maybe Int that converts a Church numeral to a Haskell integer. If the term is not a Church numeral, return Nothing.

14. Numeric Functions

In the lambda calculus, define the following functions on the Church numerals:

  1. succ – given n, computes (n + 1)

  2. plus – given m and n, computes (m + 1)

  3. times – given m and n, computes (m · n)

  4. exp – given m and n, computes mn

  5. iszero – given m, returns true if m = 0