Lambda is back!

COMP1130 PAL Week 4: Lambda Calc (continued)

Lambda Intro

λ-calculus is essentially very high level mathematics.

Last week we focused on (mostly) single argument functions. This week’s time to shake it up a little.

Remember your basic λ syntax: let x = e1 in e2 is short for (λx.e2) e1

EXERCISE: Write lambdas that will represent multi-argument functions.

f(x,y)=(x*y)/x
f(x,y,z)=(x*y)/x*z
f(x,y)=(x^(y*z)
f(x,y,z)=((x*z)*z)
f(Tina,Jay)=(Tina cos(Tina)*Jay)

EXERCISE: Write functions that represent lambdas.

λx.λy(x+y)
λx.λy.λz.((x*x*y)/ z / x) 6  8  1
λTina.λJay.λz.((Tina*Tina*Jay)/ z / Tina)  6  1

Free Variables

For each of the following lambda expressions, name the free and bound variables. If someone doesn’t understand why one is free and one is bound, explain it to them.

λx.x
(λx.x)(λy.yx)
(λx.x)x
x
y
λx.((λx.x)x)
(λJay.Jay)(λ(Tina).(Tina)y)

Alpha reduction

(Another name for Alpha-Conversion is Alpha-Renaming - It’s basically variable renaming) For each of these, convert the variable on the left of the curly brackets with that on the right, if possible. If multiple conversions are possible then list them all. For example λx.x {x → y} becomes λy.y

λy.y {y → z}
λx.y {x → z}
λx.y {x → y}
y {y → z}
λx.y {y → z}
λx.λy.x {x → y}
λx.λy.x {x → z}
λ(hosking).λ(hosking).(hosking) {(hosking) → y}

Beta reduction

Beta reduction is the use of a lambda application to convert a lambda expression into a simpler form. Recall Tony’s lectures to beta reduce the following functions. If in doubt, ask a pal!

(λx.λy x)(λz.u)
(λx.x x)(λz.u)
(λy.y a)((λx.x)(λz.(λu.u) z)) (There are three solutions to this expression)
(λc.λy.c y)
(λx.x (λx.x) (hosking))
(λp.p (λp.p)) z

Challenge Question

What does this expression evaluate to?

λ(assignments).assignments assignments (λ(assignments).assignments assignments)