CODEWITHSUNDEEP
lambda-calculus
Pradeep
Pradeep

Reputation: 637

Lambda calculus reduction of functions

I'm very new to lambda calculus and while I was reading a tutorial , came across with this. Here is my equation.

Y = ƛf.( ƛx.f(xx)) ( ƛx.f(xx))

Now if we apply another term, let's say F (YF), then how can we reduce this.If I'm correct according to beta reduction , we can replace all the f in ( ƛx.f(xx)) by ( ƛx.f(xx)), is this correct and if so how can we do that.

Thanks

Upvotes: 1

Views: 368

Answers (1)

Nir Alfasi
Nir Alfasi

Reputation: 53525

Reuction steps:

Y = ƛf.( ƛx.f(xx)) ( ƛx.f(xx)) = ƛf.( f ( ƛx.f(xx) ƛx.f(xx) ) ) 
  = ƛf.( f ( f (ƛx.f(xx) ƛx.f(xx)))) 
  = ƛf.( f ( f ( f (ƛx.f(xx) ƛx.f(xx)))) 
  = ƛf.( f ( f ( f ( f (ƛx.f(xx) ƛx.f(xx))))) = ...

So this Lambda term goes into an infinite loop...

Explanation:
Let's look on the term ( ƛx.f(xx) ƛx.f(xx) ) we substitute ƛx.f(xx) with f'
which means (f' f') => activating the term f' on itself.
It might be easier to look at like this:
( ƛy.f(yy) ƛx.f(xx) ) now when you activate the ƛy.f(yy) and provide the input (which substitutes y with ƛx.f(xx) ) the outcome is: f(ƛx.f(xx) ƛx.f(xx)) which in turn, can go over the same process again and again and the lambda-expression will only expend...


Remark:
It's wrong to write:
Y = ƛf.( ƛx.f(xx)) ( ƛx.f(xx)) it should actually be: Y = ƛf.(ƛx.f(xx) ƛx.f(xx))
The difference between ƛx.f(xx) and (ƛx.f(xx)) is that the latter is an activation of ƛx.f(xx) - it's meaningless to activate it like this (ƛx.f(xx)) since we need an x (input) to activate it on.

Finally:
Y = ƛf.( ƛx.f(xx)) ( ƛx.f(xx)) = ƛf.( f ( ƛx.f(xx) ƛx.f(xx) ) )
meaning:
YF = ( ƛx.F(xx)) ( ƛx.F(xx)) = F(ƛx.F(xx)) ( ƛx.F(xx)) = F(YF)

Upvotes: 0

Related Questions