Use of the expression function of Lambda calculus

I just found the following lambda calculus expression:

(((λ f . (λ x . (fx))) (λ a . a)) (λ b . b)) 

So, this is a function that takes an argument f and returns another function that takes an argument x and gives the result x applied to f. The result of the above expression will be (λ b. B).

This reminds me of a partial application and currying, however the application of the "out out" (fx) function is what aroused my interest.

Is there a deeper theoretical meaning for this expression?

+6
source share
1 answer

This expression is really pretty cool, although it's a pretty simple operation. After all, a function is just an application function, right?

Where things get interesting. In terms of lambda, an application is a syntax rule that simply says: "If f is an expression and x is an expression, then fx is an expression." The application is not a function. This is sad: since lambda calculus is all about functions, it would suck to rely heavily on what is not a function!

Your example is a means of doing this. Although we cannot get rid of the application, we can at least define an analogue of the application. This analogue is a lambda function (λ f . (λ x . (fx))) (or more idiomatically, λfx.fx ). This is a function, so we can reason about it and use it just like any other function. We can pass it as arguments to other functions or use it as the result of a function. Suddenly, the application-application has become much more convenient.

That's all I have before calculating lambda, but this function and others like it are also very useful in real life. In the functional programming language F #, this function even has a name, the “feedback operator”, and we write that it has the infix operator <| . Thus, as an alternative to writing f (x) , where x is some expression, we can write f <| x f <| x . This is good because it can often free us from writing a lot of annoying parentheses. The key point I'm trying to do here is that, although at first glance your example seems academic or perhaps just not very useful, it really found its way into several major programming languages.

+8
source

Source: https://habr.com/ru/post/907372/


All Articles