Lambda calculus expression reduction

Question

I'm trying to learn and understand how lambda calculus reduction works. I've been reducing some expression and I've run into this one:

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

I have reduce it to this:

(λ x . λ y . x)

But, I don't know if it's in normal form or it can be reduced more.

If this Python language question, you should add Pyton tag to the question. — Jarosław Kończak
It's a general lambda expression reduction question, not only for Python. — Saturnino

jwodder jwodder · Accepted Answer · 2015-01-16T14:23:36

The first expression cannot be reduced further, as the only term being applied to another term is a bound (and thus undefined) variable. Your reduction is invalid, as x could be anything, and thus we do not know what it will do to (λ x . λ y . x).

Lambda calculus expression reduction

1 Answers