G6021 Comparative Programming λ-calculus
1 Reduction and reduction graphs
• Reduction in the λ-calculus is defined in terms of substitution: (λx.M)N → M{x → N}
• A redex is a term of the form: (λx.M)N. When reducing a term, we need to find sub-terms of this form. We have to be careful sometimes, because remember that application associates to the left, so P(λx.M)N = (P(λx.M))N, so here (λx.M)N is not a sub-term, and therefore not a redex of the original term.
• If you prefer, you can also use the Haskell notation: \x -> M is the same as λx.M, so a redex is (\x -> M)N.
• A reduction graph simply shows all the different ways that a λ-term can be reduced.
Let I = λx.x, B = λxyz.x(yz), W = λxy.xyy and T = λfx.f(fx). Reduce the following terms to normal form, showing all alternative reductions with a reduction graph.
For each of the following λ-terms, draw the reduction graph: 1. WI
2. WII
3. WI(II)
4. WB
5. III
6. (λfx.fx)(II)
7. (λxy.x)I(II)
8. (λfx.f(fx))(λx.x) 9. BII
10. B(II)I
11. I(I(II))
12. If you are feeling adventurous, here’s a larger one to look at:
(λx.(xI))(λy.(λz.zz)(yI)) 13. If you are feeling brave, try this one: TTII.
1