The Austalian National University Semester 1, 2020 Research School of Computer Science
Dr. Ranald Clouston
COMP1130: Lambda Calculus
• Scope and Associativity
For the following expressions, remove as many redundant brackets as possible using the scoping laws and the property of left associativity. (Hopefully this exercise motivates why we avoid brackets where possible!)
1. (λx.(λy.(λz.(zy)x)))
2. (v((w(xy))z))
3. (λx.(λy.(((λz.xy)z)w)))
4. (λx.(y((λz.z)w)(λz.z)))
5. λx.(λy.((λz.z)((xy)λx.(xy)))w)
• Free Variables and Alpha Equivalence
For the following expressions, identify which variables are bound, and which are free. Afterwards, rewrite each expression using alpha conversion where necessary, such that the names of variables do not conflict.
1. x
2. λx.x
3. λy.x
4. λx.xy
5. λx.λx.x
6. x(λx.λx.x)
7. (λx.x)(λx.x)
8. λx.xλx.x
9. zλx.λy.λz.λx.xyzx
10. y(λx.λz.xz)z
11. λx.λy.yz(λx.x)x
• Substitution
Apply the following substitutions. If alpha converting is required for the substitution, indicate
as such.
1. x[y\x]
2. y[λz.z\x]
3. λx.x[y\x]
4. y(λy.y)[λz.zx\y]
5. x(λx.y)[z\y]
6. (λx.xyx)[λx.xx\y]
7. (λx.x(λy.z)x)[λz.λy.z\x]
1
8. λx.λy.z[zx\y]
9. (λx.λy.w(λy.zwy))[λx.λy.w(λy.zwy)\z]
• Beta Reduction
Perform a single beta reduction on the following expressions. Make it explicit where you’ve had
to perform an alpha conversion, if required. For example,
1. (λx.x)y
2. (λx.x)x
3. (λx.λy.xy)xy 4. (λx.yx)(λx.x) 5. (λx.xx)(λx.xx)
(λx.xx)x = (λy.yy)x → xx αβ
2