CODEWITHSUNDEEP
lambdalambda-calculus
softshipper
softshipper

Reputation: 34061

Beta reduction of some lambda

I have following lambda calculus and want to know to beta reduction of it.

The lambda is:

λxy.xy

I suppose, that it can't do beta reduce because there is no substitution and the x is bound to the body.

Is my assumption right?

Upvotes: 2

Views: 191

Answers (1)

user1544337
user1544337

Reputation:

You cannot apply beta-reduction (which is probably what you are looking for). Beta-reduction can only be applied on function applications (and even then not in all cases).

You can apply eta conversion, which transforms λx.fx to f when x does not appear freely in f. Then you can convert your expression:

λxy.xy = λx.λy.xy →η λx.x (= I).

Upvotes: 4

Related Questions