Lambda演算表达式实现函数应用
我刚刚找到了以下 lambda 演算表达式：
(((λ f . (λ x . (f x))) (λ a . a)) (λ b . b))
因此，这是一个接受参数 f 并返回另一个函数的函数，该函数接受参数 x 并产生 x 应用于 f 的结果。上述表达式的结果将是(λ b . b)。
这让我想起了部分应用和柯里化，但是“由内而外”的函数应用（fx）引起了我的兴趣。
这个表达有更深层次的理论意义吗？
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?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
这个表达式实际上非常酷，尽管它是一个非常简单的操作。毕竟，函数只是函数应用，对吧？
这就是事情变得有趣的地方。在 lambda 演算中，application 是一个语法规则，它简单地说“如果
f是一个表达式，x是一个表达式，那么f x是一个表达”。应用程序不是任何类型的函数。这是不幸的：由于 lambda 演算都是关于函数的，因此必须严重依赖非函数的东西会很糟糕！你的例子是对此的一种补救措施。虽然我们无法摆脱应用程序，但我们至少可以定义一个与应用程序相对应的应用程序。该对应项是 lambda 函数
(λ f . (λ x . (fx)))（或更惯用的是λfx.f x）。这是一个函数，因此我们可以像任何其他函数一样推理并使用它。我们可以将它作为参数传递给其他函数，也可以将其用作函数的结果。突然之间，函数应用程序变得更加可用。这就是我所了解的 lambda 演算的全部内容，但是这个函数以及其他类似的函数在现实生活中也非常有帮助。在函数式编程语言F#中，这个函数甚至还有一个名字，“向后管道运算符”，我们写它时带有中缀运算符
<|。因此，作为编写f (x)的替代方案，其中x是某个表达式，我们可以编写f <| x。这很好，因为它通常可以让我们免于编写大量烦人的括号。我在这里想说的关键点是，虽然乍一看你的例子似乎很学术，或者可能不是很有帮助，但它实际上已经进入了几种主流编程语言。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
fis an expression andxis an expression, thenf xis 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 writingf (x)wherexis some expression, we can writef <| 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.