How to reduce lambda calculus

Question

I try to understand lambda calculus and read the wonderful article.

On the page 8, there is an expression:

(λy.(x(λx.xy)))

If I am going to substitute the left outer most(λy) with t,

(λy.(x(λx.xy))) t

then the result would be?

x(λx.xy)

prof1990 prof1990 · Accepted Answer · 2017-01-27T08:03:14

I took the liberty of rewriting it to haskell syntax

(\y -> x (\x-> x y))
(\y -> x (\x-> x y)) t

x (\x -> x t)

since the y is already bound to the input \y all y will be substituted by t.

Edit: As noted in the comment below if t where to contain a free x it would be important to rename the bound x in this scope to a "fresh" name. That is a name that has currently no meaning. If we say

let t = \t -> x t

Then the proper substitution would look like

x (\z -> z (\t -> x t))

Where as stated by pigworker some z is chosen for freshness as a fresh identifier to replace our bound x to prevent hiding the free x in t.

How to reduce lambda calculus

1 Answers