Lambda calculus expression implementing function application

Question

I just found the following lambda calculus expression:

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

So that is a function that takes an argument f and returns another function that takes an argument x and yields the result of x applied to f. The result of the above expression would be (λ b . b).

This reminds me of partial application and currying, however the "inside out" function application (f x) is what piqued my interest.

Is there a deeper theoretical meaning to that expression?

Answer 1

This expression is actually pretty cool, even though it is a pretty simple operation. After all, the function is just function application, right?

That's where things get interesting. In the lambda calculus, application is a syntactic rule, which simply says "If f is an expression and x is an expression, then f x is an expression". Application is not a function of any sort. This is unfortunate: since the lambda calculus is all about functions, it would suck to have to rely heavily on something which isn't a function!

Your example is a sort of remedy to this. Although we can't get rid of application, we can at least define a counterpart to application. That counterpart is the lambda function (λ f . (λ x . (f x))) (or more idiomatically, λfx.f x). 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 it can be used as the result of a function. Suddenly, function application has become far more usable.

That's all I've got as far as lambda calculus goes, but this function, and others like it, are also quite helpful in real life. In the functional programming language F#, this function even has a name, the "pipe-backward operator", and we write it has the infix operator <|. So as an alternative to writing f (x) where x is some expression, we can write f <| x. This is nice since it can often free us from writing a lot of annoying parenthesis. The key point I'm trying to make here is that, although at a glance your example seems academic, or perhaps just not very helpful, it has actually found its way into several mainstream programming languages.