CODEWITHSUNDEEP
haskelllambda-calculus
softshipper
softshipper

Reputation: 34061

How to reduce lambda calculus

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)

Upvotes: 0

Views: 192

Answers (1)

prof1990
prof1990

Reputation: 480

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.

Upvotes: 1

Related Questions