λxyz.xz(yz) 是 Lambda 演算中的抽象还是应用程序？答案

【问题标题】：Is λxyz.xz(yz) an abstraction or an application in Lambda Calculus?λxyz.xz(yz) 是 Lambda 演算中的抽象还是应用程序？
【发布时间】：2019-04-15 11:24:25
【问题描述】：

根据 lambda 演算，应将 λxyz.xz(yz) 视为 λxyz.xz 到 (yz) 的应用，还是将 xz(yz) 中的括号简单地表示操作应该像 (xz)(yz) 而不是 ((xz)y)z 和xz(yz) 的全部内容是在函数“body”中吗？

我认为这是一个抽象，应用程序必须写成 (λxyz.xz)yz，但我的理解很差，所以我想检查一下。

【问题讨论】：

fyi 这也正是 S combinator，形成最小的图灵完备编程语言所需的组合器之一 :-)

标签： lambda-calculus

【解决方案1】：

正确。准确地说，它取决于 lambda 项语法的确切定义，更准确地说是括号省略的规则，但这些规则是有约定的。特别是，通常

application has precedence over abstraction，所以你先尝试形成xz到yz的应用，然后 x、y 和 z 上的抽象，而不是首先形成抽象 λxyz.xz，然后将生成的术语嵌入到 yz 的应用程序中（如果抽象优先于应用程序，你会得到） ;
应用程序术语中的括号是左关联的，因此xzyz（yz 周围没有括号）将被读取为((xz)y)z，并表示xz 应用于yz，您需要括号术语yz。

正如你所怀疑的，λxyz.xz(yz) 是对xz(yz) 的三重抽象，xz(yz) 本身是xz 到yz 的应用，这又是x 到z 和@ 的应用分别为 987654341@ 至 z。

所有括号都存在，术语是λx.(λy.(λz.(xz(yz))))。
因此，该术语的语法树如下所示：

λxyz.xz(yz): abstraction
|- x: variable
|- λyz.xz(yz): abstraction
  |- y: variable
  |- λz.xz(yz): abstraction
     |- z: variable
     |- xz(yz): application
        |- xz: application
        |  |- x: variable
        |  |- z: variable
        |- yz: application
           |- y: variable
           |- z: variable

正如您也正确怀疑的那样，λxyz.xz 到 yz 的应用程序将写为 (λxyz.xz)yz。

【讨论】：

谢谢您，非常感谢您的帮助！ :)