CODEWITHSUNDEEP
lambda-calculus
user4260853
user4260853

Reputation:

Beta reduction Lambda calculus

I am trying to reduce the following using beta reduction:

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

I am getting stuck after the first substitution since it seems to be giving (λx. λy.x x)(λx. λy.x x) which would end in kind of a loop. What am I doing wrong?

Upvotes: 0

Views: 2266

Answers (2)

Mulan
Mulan

Reputation: 135217

Here's an illustration of the evaluation

beta reduction 1
(λx.x x) (λx.λy.x x)              →β x [x := (λx.λy.x x)]
(λx.(λx.λy.x x) (λx.λy.x x))

beta reduction 2
(λx.λy.x x) (λx.λy.x x)           →β x [x := (λx.λy.x x)]
(λx.λy.(λx.λy.x x) (λx.λy.x x))

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

Now we have reached Weak Head Normal Form – ie, we have a lambda λy without any arguments to apply it to.

To get to Head Normal Form, we can attempt to reduce under the lambda ...

reduction 1
λy.(λx.λy.x x) (λx.λy.x x)       →β x [x := (λx.λy.x x)]
λy.(λx.λy.(λx.λy.x x) (λx.λy.x x))

reduction 2 ...
λy.λy.(λx.λy.x x) (λx.λy.x x)

Ok, we can immediately see that this pattern will repeat itself. Each time we try to reduce under the lambda, the result gets wrapped in another λy.

So, this particular lambda expression does not have a Head Normal Form – ie, the evaluation of this expression (when applied to an argument) will never terminate; it will never reach Normal Form.

Upvotes: 2

Euge
Euge

Reputation: 749

You are doing nothing wrong.

The expression (λx.x x) (λx. λy.x x) beta-reduces in one step to (λx. λy.x x)(λx. λy.x x), which beta-reduces to λy.(λx. λy.x x)(λx. λy.x x) and then to λy.λy.(λx. λy.x x)(λx. λy.x x).
In every step, each new expression is the same as before, but contained in a new abstraction.

In Lambda Calculus, the reduction process may not terminate. In other words, programs may not terminate (like in any turing-complete programming language).

Another example of this is the term Ω = (λx.x x)(λx.x x)

Upvotes: 1

Related Questions