组合逻辑

组合逻辑是一种符号，用于消除数理逻辑中对量化变量的需求。它是由摩西-舍芬克尔和哈斯克-库里提出的，最近在计算机科学中被用作计算的理论模型，也被用作函数式编程语言设计的基础。它以组合器为基础，组合器是由Schönfinkel在1920年引入的，其想法是提供一种类似的方式来建立函数，并消除对变量的任何提及，特别是在谓词逻辑中。组合器是一个高阶函数，它只使用函数应用和早期定义的组合器，从其参数中定义一个结果。在数学中，组合逻辑最初是作为一种"前逻辑"，它将澄清量化变量在逻辑中的作用，基本上是通过消除它们。消除量化变量的另一种方式是奎因的谓词漏斗逻辑。虽然组合逻辑的表达能力通常超过一阶逻辑，但谓词漏斗逻辑的表达能力与一阶逻辑的表达能力相同（Quine1960,1966,1976）。

哈斯克尔-库里在1927年底在普林斯顿大学担任讲师时重新发现了组合逻辑。

在计算机科学中，组合逻辑被用作计算的简化模型，用于可计算性理论和证明理论。尽管它很简单，但组合逻辑抓住了计算的许多基本特征。组合逻辑可以被看作是λ微积分的一个变体，其中λ表达式(代表函数抽象)被一组有限的组合器所取代，即没有自由变量的原始函数。将lambda表达式转化为组合器表达式很容易，而且组合器还原比lambda还原要简单得多。因此，组合逻辑已经被用来为一些非严格的函数式编程语言和硬件建模。这种观点最纯粹的形式是编程语言Unlambda，其xxx的基元是用字符输入/输出增强的S和K组合器。虽然不是一种实用的编程语言，但乌兰巴达具有一定的理论意义。组合逻辑可以被赋予各种解释。Curry的许多早期论文展示了如何将传统逻辑的公理集转化为组合逻辑方程（HindleyandMeredith1990）。DanaScott在20世纪60年代和70年代展示了如何将模型理论和组合逻辑结合起来。

兰姆达微积分关注的是被称为兰姆达术语的对象，它可以用以下三种形式的字符串表示。