λ 演算 lambda calculus, the (Jesse Alama and Johannes Korbmacher)
首次发布于 2012 年 12 月 12 日星期三；实质性修订于 2023 年 7 月 25 日星期二
λ 演算在本质上是一种简单的函数和应用符号。其主要思想是将函数应用于参数，并通过抽象形成函数。基本 λ 演算的语法非常简洁，使其成为表示函数的优雅而专注的符号。函数和参数处于同等地位。结果是一种非外延的函数理论，将函数视为计算规则，与将函数视为有序对集合的外延函数理论形成对比。尽管其语法简洁，但 λ 演算的表达能力和灵活性使其成为逻辑和数学的宝库。本文介绍了该领域的一些核心亮点，并为读者进一步研究该主题及其在哲学、语言学、计算机科学和逻辑学中的应用做准备。
1. 简介
λ 演算是一种优雅的符号表示法，用于处理函数对参数的应用。以数学为例，假设我们给出一个简单的多项式，如 x2−2⋅x+5。当 x=2 时，这个表达式的值是多少？我们通过在表达式中将 2 替换为 x 来计算：我们得到 22−2⋅2+5，进一步简化得到答案 5。为了使用 λ 演算来表示这种情况，我们从 λ 项开始
λx [x2−2⋅x+5]。
λ 运算符允许我们对 x 进行抽象。直观地说，‘λx [x2−2⋅x+5]’可以理解为一个等待变量 x 的值 a 的表达式。当给定这样的值 a（如数字 2）时，表达式的值是 a2−2⋅a+5。‘λ’本身没有意义；它只是绑定变量 x，保护它免受外部干扰。λ 演算中的术语是我们想要将这个表达式应用到一个参数上，并得到一个值。我们用‘Ma’表示将函数 M 应用于参数 a。继续上面的例子，我们得到：
(λx [x2−2⋅x+5])2⊳22−2⋅2+5⟨ 将 2 代入 x⟩=4−4+5⟨ 算术 ⟩=5⟨ 算术 ⟩
这个计算的第一步是将表达式‘x2−2⋅x+5’中的 x 替换为‘2’，这是从抽象术语到另一个术语的过程，通过替换操作实现。其余的等式通过自然数计算来证明。
这个例子揭示了 λ 演算的核心原理，称为 β-还原，有时也称为 β-转换：
(β)(λx [M])N⊳M [x:=N]
理解是我们可以通过简单地将 N 插入 M 内部的 x 的出现（这就是符号‘M [x:=N]’所表示的）来将一个抽象项（左侧的 λxM）的应用（λxM）N 缩减或约简（⊳）为某个东西（右侧的 N）。β-缩减或 β-转换是 λ 演算的核心。当实际应用 β-缩减来缩减一个项时，必须遵守一个重要的条件。但这将在第 2.1 节中描述，当我们讨论绑定变量和自由变量时。
1.1 多参数操作
多个参数的函数怎么办？λ 演算能否表示诸如计算直角三角形斜边长度的操作：
直角三角形的斜边长度为 x 和 y 的两条直角边 ⇒√x2+y2。
斜边长度操作将两个正实数 x 和 y 映射到另一个正实数。可以使用 λ 演算的装置来表示这样的多元操作，将操作视为逐个输入。因此，可以将该操作视为接受一个输入 x（正实数）并产生一个值，而不是一个数字，而是一个操作：即，将正实数 y 作为输入并产生正实数 √x2+y2 作为输出的操作。可以通过说，计算直角三角形斜边长度的操作 hypotenuse-length，给定直角边 a 和 b 的长度，是：
λ 演算定义：斜边长度 :=λa [λb[√a2+b2]]
根据 β-还原原理，例如，斜边长度 3，即将斜边长度应用于 3，得到 λb [√32+b2]，这是一个“等待”另一个参数的函数。λ 项斜边长度 3 可以看作是一个函数，计算一个直角三角形的斜边长度，其中一条腿的长度为 3。最后我们发现，(斜边长度 3)4——将斜边长度应用于 3，然后再应用于 4——结果为 5，与预期相符。
理解将多元函数还原为一元函数的另一种方法是想象一个机器 M，初始时将多个参数 a、b、... 中的第一个参数 a 加载到内存中。如果在将第一个参数加载到内存后暂停机器，可以将结果视为另一个机器 Ma，它等待更少的输入；第一个参数现在是固定的。
1.2 非外延性
λ 演算中一个重要的哲学问题是其函数概念的基础。在集合论中，函数通常被理解为一组参数-值对的集合。更具体地说，函数被理解为一个满足性质(x,y)∈f 且(x,z)∈f 蕴含 y=z 的有序对集合 f。如果 f 是一个函数且(x,y)∈f，这意味着函数 f 将值 y 分配给参数 x。这就是函数作为集合的概念。因此，函数作为集合的相等概念是集合的相等，根据外延性原则，这意味着当两个函数包含相同的有序对时它们是相等的。换句话说，当两个函数对相同的参数分配相同的值时，它们是相同的。从这个意义上说，函数作为集合是外延性对象。
相反，在 λ 演算中，函数的概念是基于规则的：函数由一条规则给出，规定了如何根据参数确定其值。更具体地说，我们可以将 λ 项 λx [M] 视为一个操作的描述，给定 x，它产生 M；抽象项的主体 M 本质上是关于如何处理 x 的规则。这就是函数作为规则的概念。直观地说，给定规则 M 和 N，我们通常无法确定 λx [M] 是否等于 λx [N]。这两个项可能在相同的参数下“行为”相同（给定相同的参数具有相同的值），但可能不清楚为了证明这些项的相等性需要什么资源。从这个意义上说，函数作为规则是非外延性对象。
为了区分函数作为集合的外延概念和函数作为规则的非外延概念，后者通常被称为“内涵”函数概念，部分原因是涉及到的规则概念表面上是内涵的。这个术语在数理逻辑学家和数学哲学家的社区中特别流行，他们致力于数学基础的研究。但从语言哲学的角度来看，这个术语可能有些误导，因为在这个背景下，外延-内涵的区别有着稍微不同的意义。
在哲学语义学的标准可能世界框架中，我们将区分外延函数概念和内涵函数概念如下。我们说，如果两个函数在一个世界上对相同的参数赋予相同的值，那么它们在该世界上是外延等价的。我们说，如果两个函数在每个可能的世界上对相同的参数赋予相同的值，那么它们在内涵上是等价的。举个例子，考虑函数 highest-mountain-on-earth 和 highest-mountain-in-the-Himalayas，其中 highest-mountain-on-earth 将地球上最高的山作为每个参数的值，而 highest-mountain-in-the-Himalayas 将喜马拉雅山脉上最高的山作为每个参数的值。这两个函数在外延上是等价的（在实际世界上），但在内涵上不是等价的。在实际世界上，这两个函数对每个参数都赋予相同的值，即珠穆朗玛峰。现在考虑一个世界，在这个世界上珠穆朗玛峰不是地球上最高的山，而是说，拉什莫尔山是。进一步假设这是因为拉什莫尔山比实际世界上高出 30,000 英尺/9,100 米，而珠穆朗玛峰，以其大约 29,000 英尺/8,800 米的高度，仍然是喜马拉雅山脉最高的山。在那个世界中，highest-mountain-on-earth 现在将拉什莫尔山作为每个参数的值，而 highest-mountain-in-the-Himalayas 仍然将珠穆朗玛峰赋予每个参数。换句话说，highest-mountain-on-earth 和 highest-mountain-in-the-Himalayas 在外延上是等价的（在实际世界上），但在内涵上不等价。
如果且仅当在实际世界上需要在外延上等价的函数是相同的时，函数概念现在可以被称为外延的。如果且仅当需要在内涵上等价的函数是相同的时，函数概念可以被归类为内涵的。请注意，这些分类在数学基础中通常使用的区分概念上是有概念上的不同的。在数学基础中使用的术语上，函数作为集合被归类为外延，因为它们使用外延性公理作为它们的同一性标准，而函数作为规则被归类为内涵，因为它们依赖于表面上内涵的规则概念。在当前的可能世界术语中，函数概念被归类为外延或内涵，基于它们在可能世界上的行为。
可能会导致概念混淆的一个问题是，两种术语可能对 λ 演算中的函数概念产生不同的判断。为了看清楚这一点，考虑以下两个函数：
ADD-ONE:=λx [x+1] ADD-TWO-SUBTRACT-ONE:=λx [[x+2] −1]
这两个函数在外延上是等价的：它们在实际世界中为相同的输入赋予相同的值。此外，根据可能世界语义中的标准假设，这两个函数在内涵上也是等价的。如果我们假设数学事实（如加法和减法等事实）在每个可能世界中都是必然的，那么我们可以得出这两个函数在每个可能世界中对参数给出相同的值。因此，内涵函数概念要求这两个函数是相同的。然而，在 λ 演算中，我们并不能清楚地认为这两个函数是相同的。从形式上讲，如果没有其他原则的帮助，我们无法证明这两个 λ 项表示相同的函数。此外，从非正式的角度来看，在函数作为规则的概念中，我们甚至不能确定我们是否应该将它们视为相同的：这两个项涉及真正不同的规则，因此我们可能会说它们表示不同的函数。
允许内涵等价函数是不同的函数概念被称为超内涵。关键在于，在可能世界术语中，λ 演算中使用的函数概念可能被视为超内涵的，而不是意向的——与数学基础中常见的术语相反。请注意，不清楚一个内涵语义框架（如可能世界框架）如何在原则上解释非内涵函数概念。关于 λ 演算的语义，请参见第 7 节。这里的重点只是为了澄清在哲学讨论中使用不同术语可能引起的概念混淆。
λ 演算的超内涵性在其作为函数理论以及更一般的 n 元关系理论中尤为重要。关于此，请参见第 9.3 节。正是 λ 演算的超内涵性使其成为这一背景下的有吸引力的工具。然而需要注意的是，通过假设关于 λ 项相等性的附加定律，λ 演算可以被扩展（以及内涵）。关于此，请参见第 5 节。
2. 语法
λ 演算的官方语法非常简单；它包含在下一个定义中。
λ 演算的语言字母表的定义采用左括号、右括号、左方括号、右方括号、符号‘λ’和无限集合的变量。λ 项的类别按如下方式归纳定义：
每个变量都是一个 λ 项。
如果 M 和 N 是 λ 项，则(MN)也是 λ 项。
如果 M 是一个 λ 项，x 是一个变量，那么(λx [M])是一个 λ 项。
通过“项”我们总是指“λ 项”。根据规则(2)形成的项称为应用项。根据规则(3)形成的项称为抽象项。
在处理具有分组符号（在我们的情况下是左右括号）的形式语言时，通常会省略一些括号，只有在安全的情况下才会重新引入（即只有一种合理的方式）。严格来说，连续放置超过两个 λ 项是非法的。为了避免总是写入所有必需的括号而产生的乏味，我们采用以下约定：
约定（左结合）：当超过两个项 M1M2M3...Mn 并列时，我们可以通过左结合来恢复缺失的括号：从左到右读取，将 M1 和 M2 组合在一起，得到(M1M2)M3...Mn；然后将(M1M2)与 M3 组合：((M1M2)M3)...Mn，依此类推。
因此，该约定为长度大于 2 的任何 λ-项序列提供了唯一的解读。
2.1 变量，绑定和自由
λ 在抽象项（λx [M]）中的作用是将紧随其后的变量绑定到项 M 中。因此，λ 类似于一阶逻辑中的全称量词 ∀ 和存在量词 ∃。可以类似地定义自由变量和约束变量的概念，如下所示。
定义 语法函数 FV 和 BV（分别表示“自由变量”和“约束变量”）通过结构归纳在 λ-项集上定义如下：
对于每个变量 x、项 M 和项 N：
FreeBound(1)FV(x)={x}BV(x)=∅(2)FV(MN)=FV(M)∪FV(N)BV(MN)=BV(M)∪BV(N)(3)FV(λx [M])=FV(M)−{x}BV(λx [M])=BV(M)∪{x}
如果 FV(M)=∅ ，那么 M 被称为组合子。
两个定义中的第三条支持 λ 绑定变量（确保它们不是自由的）的意图。注意变量的 BV 和 FV 之间的区别。
如同其他学科中出现的概念一样，比如一阶逻辑，我们需要对这个问题保持谨慎；对替换的随意态度可能导致语法上的困难。[1] 我们可以通过采用一个约定来捍卫这种随意态度，即我们关注的不是项本身，而是一定等价类的项。现在我们来定义替换，然后制定一个约定，以避免这样的困难。
定义（替换）我们用‘M [x:=N]’表示将 N 替换为 M 中自由出现的 x。根据 λ-项集的递归，一个精确的定义 [2] 如下：对于所有的项 A、B 和 M，以及所有的变量 x 和 y，我们定义
x [x:=M] ≡M
y [x:=M] ≡y（y 与 x 不同）
(AB)[x:=M] ≡A [x:=M] B [x:=M]
(λx [A])[x:=M] ≡λx [A]
(λy [A])[x:=M] ≡λy [A[x:=M]] (y 与 x 不同)
定义的第一条款简单地说明，如果我们要将 M 替换为 x，并且我们只处理 x，那么结果就是 M。第二条款说明，当我们只处理与 x 不同的变量，但要替换 x 时，不会发生任何变化。第三条款告诉我们，替换无条件地分布在应用中。第四条和第五条涉及抽象项和并列的第一条款和第二条款（或者说，第二条款和第一条款，顺序相反）：如果抽象项 λz [A] 的绑定变量 z 与我们要进行替换的变量 x 相同，则我们不执行任何替换（即替换“停止”）。这与 M [x:=N] 表示用 N 替换 M 中的自由出现的 x 的意图一致。如果 M 是一个绑定变量为 x 的抽象项 λx [A]，则 x 在 M 中没有自由出现，所以没有任何操作要做。这解释了第四条款。最后，第五条款表示，如果抽象项的绑定变量与 x 不同，则 x 至少有“机会”在抽象项的主体中自由出现，并且替换会继续进行。
定义（绑定变量的更改，α-可转换性）。如果粗略地说，任何在 M 中的抽象项 λx [A] 都被替换为 λy [A[x:=y]]，那么项 N 是从项 M 中通过绑定变量的更改获得的。
假设 M 和 N 是 α-可转换的，如果从 M 到 N 存在一系列绑定变量的更改。
公理。β-转换（陈述了无捕获条件）：
(λx [M])N⊳M [x:=N]， 在将其替换为 M 之后，不会有任何自由出现在 N 中的变量变为绑定变量。
粗略地说，我们需要遵循自由变量应保持自由的原则；当一个变量的出现受到替换的威胁时，只需执行足够的 α-转换来规避这个问题。如果我们记住这一点，就可以在不担心这些棘手的语法困难的情况下使用 λ 演算。例如，我们不能将函数 λx [λy[x(y−5)]]应用于参数 2y，因为在将“2y”替换为“x”之后，“2y”中的“y”将被变量绑定运算符“λy”所捕获。这样的替换将产生与预期不同的函数。然而，我们可以先通过 α-转换将 λx [λy[x(y−5)]]转换为 λx [λz[x(z−5)]]，然后将后者应用于参数 2y。因此，虽然以下不是 β-转换的有效用法：(λx [λy[x(y−5)]])2y⊳λy [2y(y−5)]，但我们可以有效地使用 β-转换得出结论：(λx [λz[x(z−5)]])2y⊳λz [2y(z−5)]。这个例子帮助我们理解为什么 β-转换的条件如此重要。这个条件与谓词演算公理陈述中使用的条件没有什么不同，即：∀xϕ→ϕτx，前提是在替换之前，术语 τ 中的自由变量在替换之后不会变为绑定变量。
λ-演算的语法非常灵活。人们可以构造各种各样的术语，甚至包括自应用，例如 xx。这样的术语乍一看似乎可疑；人们可能会怀疑使用这样的术语可能导致不一致性，并且在任何情况下，人们可能会发现自己需要一种工具来禁止这样的术语。如果将函数和某种类型的有序对集合视为函数和有序对的集合，则 xx 中的 x 将是一个包含一个元素(x,y)的函数（有序对集合），其中第一个元素将是 x 本身。但是，没有集合可以以这种方式包含自身，否则将违反基础公理（或正则性）。因此，从集合论的角度来看，这样的术语显然是可疑的。下面是对一种这样的工具——类型理论的简要概述。但实际上，这样的术语并不会导致不一致性，并且在 λ-演算的上下文中具有有用的目的。此外，禁止这样的术语，如类型理论中所做的，是有代价的（例如，失去了无类型 λ-演算的某些表达能力）。
2.2 组合子
如前所述，组合子是没有自由变量的 λ-术语。人们可以直观地理解组合子为“完全指定”的操作，因为它们没有自由变量。在 λ-演算的历史中，有一些组合子被证明是有用的；下表突出显示了其中一些特殊的组合子。还可以给出更多的组合子（显然有无限多个组合子），但以下组合子具有简明的定义并证明了它们的实用性。下面是一些标准的 λ-术语和组合子的表格。
下面是本条目中使用的符号约定表。
3. λ-演算的简要历史
λ 演算起源于对函数作为规则的研究。这个学科的基本要素已经可以在弗雷格的开创性工作中找到（Frege, 1893）。正如我们之前所做的观察，弗雷格观察到，在研究函数时，只需要关注一元函数（即只接受一个参数的函数）就足够了。（将多元操作视为一系列抽象的过程，从而得到等效的一元操作的方法被称为柯里化操作。也许从历史角度来看，将这个操作称为弗雷格操作更准确，但在数学思想的命名中经常出现冤案。）在 20 世纪 20 年代，数学家莫西斯·舍恩菲克尔进一步研究了所谓的组合子。正如在学科的早期阶段很常见的那样，舍恩菲克尔对形式逻辑中出现的变换感兴趣，他的组合子旨在为形式逻辑的基础做出贡献。类似于在经典命题逻辑中看到的约翰逊符号的简化，舍恩菲克尔建立了一个令人惊讶的结果，即所有函数（在变换的意义上）都可以用组合子 K 和 S 来表示；稍后我们将看到这些组合子的定义。
定理 对于由 K 和 S 以及变量 x 构成的每个项 M，存在一个仅由 K 和 S 构建的项 F，使得我们可以推导出 Fx=M。
（证明这两个组合子足以表示所有函数超出了本条目的范围。有关进一步讨论，请参阅组合逻辑的条目。）可以构造性地证明这个定理：存在一个算法，给定 M，可以产生所需的 F。丘奇将这个 F 称为‘λx [M]’（Church, 1932）[3]。从这个角度来看，β 规则是合理的：如果‘λx [M]’是一个满足 Fx=M 的函数 F，那么 λx [M] x 应该转换为 M。这只是更一般原理的特例，对于所有 N，（λx [M]）N 应该转换为 M [x:=N]。
尽管今天我们有更明确的抽象和重写系统，但在早期的 λ 演算和组合逻辑（如 Schönfinkel 所述）中，它们与数学基础的研究紧密相连。在 Curry、Church、Kleene 和 Rosser（这些学科的先驱者之一）的手中，重点是定义数学对象并在这些新系统中进行逻辑推理。结果证明，这些早期的所谓推理 λ 演算和组合逻辑是不一致的。Curry 分离并修正了这个不一致性，结果现在被称为 Curry 的悖论。请参阅 Curry 的悖论和（Barendregt，1985）附录 B 的条目。
λ 演算在逻辑史上占据了特殊的地位，因为它是第一个不可判定问题的源头。这个问题是：给定 λ 项 M 和 N，确定 M=N 是否成立。（关于 λ 项的等式推理理论尚未定义；定义将在后面给出。）这个问题被证明是不可判定的。
λ 演算的另一个早期问题是它是否一致。在这个背景下，不一致意味着所有的项都是相等的：一个 λ 项 M 可以被规约为任何其他 λ 项 N。这不是 λ 演算的情况。最初，人们得到了一些结果，表明某些项是不可互换的（例如 K 和 S）；后来，一个更强大的结果，即所谓的 Church-Rosser 定理，帮助更深入地了解 β 转换，并可用于快速证明整个 λ 项类别的不可互换性。有关一致性的更详细讨论，请参阅下文。
λ 演算在 20 世纪 60 年代之前是一个相对晦涩的形式化方法，直到最后才找到了一个“数学”语义。它与编程语言的关系也得到了澄清。在那之前，λ 演算的唯一模型是“句法”的，即按照 Henkin 的风格生成的 λ 项的等价类（对于适当的等价概念）。由于 Montague 和其他语言学家的发展，它在自然语言语义学中的应用有助于“传播这个概念”。从那时起，λ 演算在数学逻辑、计算机科学、语言学（例如，Heim 和 Kratzer 1998）以及相关领域中享有崇高的地位。
4. 简化
有各种各样的 λ 项简化概念可供选择，但主要的是 β 简化，我们之前已经见过了。之前我们使用了符号“⊳”；我们可以更加精确地表示。在本节中，我们讨论 β 简化及其一些扩展。
定义（一步 β-还原 ⊳β,1）对于 λ-项 A 和 B，我们说 A 一步 β 还原为 B，记作 A⊳β,1B，只要存在 A 的子项 C（的一个出现），一个变量 x 和 λ-项 M 和 N，使得 C≡(λx [M])N，并且 B 是 A 的除了 A 中 C 的出现被 M [x:=N] 替换的部分。
这里有一些 β 还原的例子：
变量 x 不会 β 还原为任何东西。（它没有正确的形式：它只是一个变量，不是一个左手边是抽象项的应用项。）
(λx [x])a⊳β,1a.
如果 x 和 y 是不同的变量，则 (λx [y])a⊳β,1y.
λ-项 (λx [(λy[xy])a])b] 在一步内被 β-还原为两个不同的 λ-项:
(λx [(λy[xy])a])b⊳β,1(λy [by])a
和
(λx [(λy[xy])a])b⊳β,1(λx [xa])b
此外，我们可以检查这两个术语在一步中 β-规约为一个公共术语：ba。因此我们有：
与任何二元关系一样，我们可以对 λ-术语之间的关系 ⊳β,1 提出许多问题，并且可以根据 ⊳β,1 定义各种派生概念。
从 λ 项 A 到 λ 项 B 的 β-还原序列是以 A 开头、以 B 结尾的有限序列 s1,…sn，其中相邻的项(sk,sk+1)满足 sk⊳β,1sk+1 的性质。
更一般地，任何以 λ 项 A 开头的序列 s（有限或无限）被称为以 A 开头的 β-还原序列，前提是序列 s 的相邻项(sk,sk+1)满足 sk⊳β,1sk+1 的性质。
继续 β-还原示例 1，没有以变量 x 开头的 β-还原序列。
继续进行 β-还原 示例 2，这个两项序列
(λx [x])a,a
是从 (λx [x])a 到 a 的 β-还原序列。如果 a 是一个变量，那么这个 β-还原序列不能被延长，也没有其他以 (λx [x])a 开始的 β-还原序列；因此，以 (λx [x])a 开始的 β-还原序列是有限的，并且不包含无限序列。
组合子 Ω 具有奇特的性质，即 Ω⊳β,1Ω。以 Ω 为起始的每个 β-还原序列的每个术语（有限或无限）都等于 Ω。
考虑术语 KaΩ。有无限多个以该术语为起始的还原序列：
KaΩ⊳β,1a
KaΩ⊳β,1KaΩ⊳β,1a
KaΩ⊳β,1KaΩ⊳β,1KaΩ⊳β,1a
KaΩ⊳β,1KaΩ⊳β,1KaΩ…
如果 a 是一个变量，可以看到以 KaΩ 开头的所有有限规约序列都以 a 结束，并且存在唯一的无限规约序列。
定义 λ 项 M 的 β-可约项是 M 的形式为 (λx [P])Q 的子项。（'redex' 源自 'reducible expression'）。β-可约项只是 β-规约的一个候选项。通过进行 β-规约，可以缩减 β-可约项。如果一个项没有 β-可约项，则称其为 β-正规形式。
（一个项是否可以有多个 β-正规形式？答案字面上是 '是'，但实质上答案是 '否'：如果 M 和 M' 是某个项的 β-正规形式，则 M 可以 α-转换为 M'。因此，β-正规形式在绑定变量的改变上是唯一的。）
到目前为止，我们只关注了 β-还原的一个步骤。可以通过取关系 ⊳β,1 的传递闭包将多个 β-还原步骤合并为一个。
对于 λ-项 A 和 B，如果 A≡B 或者存在一个有限的 β-还原序列从 A 到 B，则称 A β-还原为 B，记作 A⊳βB。
如果存在一个项 N 使得 N 是 β-正常形式且 M⊳βN，则项 M 具有 β-正常形式。
按照定义，可约性是一种单向关系：如果 A⊳βB，则通常不成立 B⊳βA。然而，根据个人的目的，如果 A 减少到 B 或者 B 减少到 A，可以将 A 和 B 视为等价。这相当于考虑关系 ⊳β 的自反、对称和传递闭包。
对于 λ-项 A 和 B，如果 A≡B 或者存在一个以 A 开头、以 B 结尾的序列 s1,…sn，并且其相邻项(sk,sk+1)满足 sk⊳β,1sk+1 或者 sk+1⊳β,1sk，则我们说 A=βB。
4.1 减少的其他概念
到目前为止，我们已经发展了 β-还原的理论。这绝不是 λ 演算中唯一可用的还原概念。除了 β-还原之外，λ 项之间的标准关系还有 η-还原：
定义（一步 η-还原）对于 λ 项 A 和 B，我们说 A 可以在一步中 βη-还原为 B，记作 A⊳βη,1B，当且仅当存在 A 的子项 C（的一个出现）、变量 x 和 λ 项 M 和 N，满足以下条件之一：
C≡(λx [M])N，并且 A 中的 C 的出现被 M [x:=N] 替换后得到 B，A 中的其他部分保持不变。
或者
C≡(λx [Mx])，B 是 A 的一个例外，A 中的 C 的出现被 M 替换。
在 ⊳βη,1 的定义中，第一个子句确保了该关系扩展了一步 β-还原的关系。就像我们对一步 β-还原的关系所做的那样，我们可以重复发展 η-还原的过程。因此，我们有了 η-还原的概念，并且从 ⊳η,1 可以定义 λ-项之间的关系 ⊳η，它是 ⊳η,1 的自反传递闭包，捕捉了零个或多个 η-还原的步骤。然后，我们定义=η 为 ⊳η 的对称传递闭包。
如果 A⊳η,1B，则 B 的长度严格小于 A 的长度。因此，不存在无限的 η-规约。这在 β-规约中并非如上所见的 β-规约序列示例 3 和 4 的情况。
可以结合规约的概念。一个有用的组合是将 β-规约和 η-规约混合在一起。
定义（一步 βη-规约）λx [Mx] ⊳βη,1M 和（λx [M] N))⊳βη,1M [x:=N]。λ 项 A 在一步中 βη-规约到 λ 项 B，当且仅当 A 在一步中 β-规约到 B 或 A 在一步中 η-规约到 B。
再次，我们可以重温基本的约简概念，就像我们对于 β-约简所做的那样，对于这个新的约简概念 βη。
4.2 约简策略
回想一下，如果一个术语没有 β-约约束，也就是说，没有形如(λx [M])N 的子术语，那么它被称为 β-正规形式。如果一个术语可以被约简为 β-正规形式的术语，那么它就有一个 β-正规形式。直观上来说，如果一个术语有一个 β-正规形式，那么我们可以通过穷尽地缩减术语的所有 β-约约束，然后穷尽地缩减所有结果术语的 β-约约束，依此类推，找到一个 β-正规形式。说一个术语有一个 β-正规形式，意味着这种盲目搜索最终会终止。
盲目搜索 β-正规形式并不令人满意。除了审美上不舒服外，它可能非常低效：没有必要穷尽地缩减所有的 β-约束。我们需要的是一种策略，最好是可计算的策略，用于找到 β-正规形式。问题是如何有效地决定，如果一个表达式有多个 β-约束，应该缩减哪一个。
定义 β-约简策略是一个函数，其定义域是所有 λ-表达式的集合，对于一个不在 β-正规形式中的表达式 M，其值是 M 的一个约简子表达式，对于所有在 β-正规形式中的表达式 M，其值就是 M 本身。
换句话说，β-约简策略在一个表达式有多个 β-约束时选择应该缩减的那个。如果一个表达式已经是 β-正规形式，那么就不需要进行任何操作，这就是为什么在 β-约简策略的定义中要求它不改变任何 β-正规形式的表达式。可以将策略 S 表示为 λ-表达式上的关系 ⊳S，理解为如果通过遵循策略 S，从 M 经过一步得到 N，则 M⊳SN。从关系的角度来看，策略构成了 ⊳β,1 的子关系。
一个 β-约简策略可能具有或不具有遵循该策略将确保我们（最终）达到 β-正规形式（如果存在）的属性。
定义 β-约简策略 S 是正规化的，如果对于所有 λ-项 M，如果 M 有 β-正规形式 N，则序列 M，S(M)，S(S(M))，… 在 N 处终止。
一些 β-约简策略是正规化的，但其他一些则不是。
最右策略，即我们总是选择减少最右边的 β-约简式（如果有任何 β-约简式），是不规范的。例如，考虑术语 KIΩ。这个术语有两个 β-约简式：它本身和 Ω（回想一下，Ω 是术语 ωω≡(λx [xx])(λx [xx])）。通过使用左手边的 β-约简式，我们可以在两步中将 KIΩ β-约简为 I。如果我们坚持使用最右边的 β-约简式 Ω，我们将 KI(Ω) 减少为 KI(Ω)，然后是 KI(Ω)，……。
最左策略，即我们总是选择减少最左边的 β-约简式（如果有任何 β-约简式），是规范的。这个事实的证明超出了本条目的范围；有关详细信息，请参见（Barendregt，1985 年，第 13.2 节）。
一旦我们定义了一个约简策略，自然会问是否可以改进它。如果一个术语有一个 β-正规形式，那么一个策略将发现一个正规形式；但是是否可能存在一个更短的 β-约简序列，达到相同的正规形式（或者是与该正规形式 α-可转换的术语）？这就是最优性的问题。定义最优策略并证明它们是最优的通常比仅仅定义一个策略要困难得多。有关更多讨论，请参见（Barendregt，1984 年第 10 章）。
为了具体起见，我们仅讨论了 β-还原策略。但在上述定义中，还原 β 的概念只是一种可能性。对于还原的任何概念 R，我们都有与之相关的 R 还原策略理论，并且可以针对 R 重新进行可归约性、最优性等问题的处理。
5. λ 理论
我们之前讨论了 λ 演算是一个非外延的函数理论。如果按照非外延的精神，我们将 λ 项理解为描述，那么我们应该如何处理 λ 项的相等性？有各种方法可供选择。在本节中，让我们将等号关系=视为原始的、未定义的关系，它在两个 λ 项之间成立，并尝试公理化等号应具备的性质。任务是确定公理并制定适当的关于 λ 项相等性的推理规则。
一些与 λ 演算无关的明显的等式性质如下：
（自反性）X=X（对称性）X=YY=X（传递性）X=YY=ZX=Z
在证明理论中，按照标准的方式阅读这些推理规则，水平线上方是规则的前提（即等式），水平线下方的等式是推理规则的结论。在自反性规则的情况下，水平线上方没有写任何内容。我们理解这种情况是说，对于所有的项 X，我们可以从没有前提的情况下推导出等式 X=X。
5.1 λ 演算的基本理论
在前一节中列出的三条关于相等性的推理规则与 λ 演算无关。以下列出了与 λ 演算的两个术语构建操作（应用和抽象）以及未定义的相等性概念相关的推理规则。
M=NAM=ANM=NMA=NA(ξ)M=Nλx [M]=λx [N]
这些推理规则表明 = 是 λ-terms 集合上的一个同余关系：它“保持”应用和抽象的构建操作
推理的最后一个规则，β-转换，是最重要的：
(β)(λx [M])A=M [x:=A]
与前面的自反性规则一样，规则 β 没有前提条件：对于任何变量 x 和任何项 M 和 A，可以在 λ 理论的任何推导过程中推导出等式 (λx [M])A=M [x:=A]。
5.2 扩展基本理论 λ
λ 有许多扩展可用。例如，考虑规则 (η)，它将 η-约简原则表达为推理规则：
(η)λx [Mx]=M 前提是 x∉FV(M)
规则 η 告诉我们某种抽象是多余的：可以安全地将 M 与给定参数 x 应用 M 的函数进行等同。通过这个规则，我们也可以看到所有的术语实际上都是函数。可以用 β-还原原则直观地证明这个规则。
(Ext)Mx=NxM=N 前提是 x∉FV(M)∪FV(N)
人们可以将规则 Ext 视为一种泛化原则。如果我们已经推导出 Mx=Nx，但 x 既不在 M 中也不在 N 中，那么我们实际上已经证明了 M 和 N 是相似的。将这个原则与一阶逻辑中的普遍泛化原则进行比较：如果我们从一组假设 Γ 中推导出 ϕ(x)，其中 x 不是自由的，那么我们可以得出结论 Γ 推导出 ∀xϕ。
λ 演算中的另一个有生产力的原则允许我们识别“行为”相同的项：
（ω）对于所有的项 x，Mx=NxM=N
规则 ω 有无限多个假设：在假设 Mx=Nx 成立的情况下，无论 x 是什么，我们都可以得出 M=N 的结论。ω 规则是 λ 演算中与同名的形式数论推理规则的类比，根据该规则，可以得出全称公式 ∀xϕ，前提是对于 ϕ(x:=0),ϕ(x:=1),…都有证明。请注意，与规则 Ext 不同，不需要考虑 x 在 M 或 N 中是否自由出现的条件。
6. λ 演算的一致性
λ 演算是否一致？这个问题可能没有明确定义。λ 演算不是用于推理命题的逻辑；它没有明显的矛盾（⊥）的概念，也没有形成荒谬命题（例如，p∧¬p）的方法。因此，λ 演算的“不一致”不能意味着可以推导出 ⊥ 或等同于 ⊥ 的公式。然而，有一个合适的“一致性”概念可用。直观地说，如果一个逻辑允许我们推导出太多的东西，那么它就是不一致的。λ 理论是一个关于方程的理论。因此，我们可以将 λ 的不一致性理解为：所有方程都是可推导的。如果 λ 具有这样的性质，那么显然它作为一个形式理论的用途很小。
早期的 λ-演算理念由 A. Church 提出的确是不一致的；参见（Barendregt，1985，附录 2）或（Rosser，1985）进行讨论。以一个具体的问题为例：我们如何知道方程 K=I 不是 λ 的一个定理？这两个术语显然是直观上不同的。K 是一个具有两个参数的函数，而 I 是一个具有一个参数的函数。如果我们能够证明 K=I，那么我们就能够证明 KK=IK，从而 KK=K 将成为 λ 的一个定理，以及许多其他我们直观上不可接受的方程。但是，当我们研究 λ 这样的形式理论时，直观上的不可接受并不意味着不可推导。缺少的是对 β-还原的更深入理解。
一个早期给出这样理解的结果被称为 Church-Rosser 定理：
定理（Church-Rosser）如果 P⊳βQ 且 P⊳βR，则存在一个术语 S，使得 Q⊳βS 和 R⊳βS 都成立。
（这个定理的证明相当复杂，超出了本条目的范围。）这个结果是关于 β-还原的一个深刻事实。它表明，无论我们通过 β-还原如何偏离 P，我们总是可以再次收敛到一个公共术语。
Church-Rosser 定理告诉我们，除其他事项外，纯 λ-演算——即 λ-项之间的方程理论——是一致的，也就是说，并非所有方程都是可导出的。
作为一个例证，我们可以使用 Church-Rosser 定理来解决早期的问题，即证明两个术语 K 和 I 不被 λ 所识别。这两个术语处于 β-正规形式，因此它们之间根本没有 β-还原序列。如果 K=I 是 λ 的一个定理，那么就会有一个术语 M，从中可以通过 β-还原路径同时到达 I 和 K。然后，Church-Rosser 定理暗示着从 M 分开的两条路径可以合并。但这是不可能的，因为 K 和 I 是不同的 β-正规形式。
Church-Rosser 定理意味着从 K 和从 I 开始的 β-还原序列以相同的术语结束。但是，从 I 开始的 β-还原序列根本不存在，因为它处于 β-正规形式，K 也是如此。
定理 λ 是一致的，也就是说，并非每个方程都是定理。
要证明这个定理，只需产生一个不可推导的方程即可。我们已经通过一个例子进行了工作：我们使用了 Church-Rosser 定理来证明方程 K=I 不是 λ 的定理。当然，这两个术语并没有什么特别之处。这个结果的一个重要的推广是可用的：如果 M 和 N 是 β-正规形式，但 M 不等于 N，则方程 M=N 不是 λ 的定理。（如果我们向 λ 添加额外的推理规则，这个简单的不可推导条件通常不成立。）
λη 和 λω 理论同样是一致的。可以通过将 Church-Rosser 定理扩展到这些理论的更广义可导性的方式来证明这些一致性结果。
7. λ 演算的语义
正如我们在开始时所说，λ 演算的本质是关于函数及其应用的。但是，将这个想法用语义术语来解释却出奇地困难。一个自然的方法是尝试将每个 λ 项 M 关联到某个域 D 上的函数 fM，并使用函数应用 fM(fN)来解释应用项(MN)。但是这个想法很快遇到了困难。首先，很容易看出，在这个上下文中，我们不能使用标准的集合论概念将函数视为集合（参见本条目的第 1.2 节）。根据这个概念，记住，一个函数 f 是一个参数-值对的集合，其中每个参数被分配一个唯一的值。问题出现在自应用的上下文中。回想一下第 2.1 节中提到的无类型 λ 演算允许像(xx)这样的 λ 项，直观地将 x 应用于自身。在我们正在探索的语义图景中，我们可以通过将 x 的函数 fx 应用于自身来获得项(xx)的关联函数 f(xx)：
f(xx)=fx(fx)
但是根据函数作为集合的观点，这意味着集合 fx 需要包含一个以 fx 为第一个组成部分，以 f(xx) 为第二个组成部分的参数-值对：
fx={…,(fx,f(xx))),…}
但这将使 fx 成为一个非良基对象：定义 fx 将涉及 fx 本身。实际上，标准公理化集合论通过基础公理（也称为正则性公理）排除了这样的集合。-这进一步证明了 λ 演算的基础概念不能是外延函数作为集合的概念。
但问题甚至比这更深。即使我们使用非外延函数的概念，例如函数作为规则的概念（再次参见第 1.2 节），我们也会遇到困难。在无类型的 λ 演算中，一切都可以是函数，也可以是函数的参数。相应地，我们应该希望我们的域 D 在某种意义上包括函数空间 DD，其中只包含从 D 中的参数和值都是函数的函数。为了看到这一点：
D 的每个元素都可以是应用于 D 的元素的函数，然后返回的结果又可以作为 D 的元素的参数。因此，D 的每个元素直观上对应于 DD 的成员。
如果我们依次取一个属于 DD 的成员，即一个带有来自 D 的参数和值的函数，这正是我们想要包含在我们的域 D 中的东西。因此，直观上，我们希望 DD 的每个成员对应于 D 的一个成员。
简而言之，我们希望我们的域和它自己的函数空间之间存在一一对应的关系，即我们希望它们满足“等式”X≅XX。但这是不可能的，因为它与康托尔的定理相矛盾。
面对这些困难，问题出现了：是否有可能首先给出 λ 演算的集合论模型？事实证明是可以的。D. Scott 是第一个在 1969 年的一篇未发表的手稿中描述这样一个模型的人。这个模型 D∞ 通过适当限制函数空间 DD，只让一些 DD 的成员对应于 D 的成员，解决了前面提到的与康托尔的定理相关的问题。涉及到 Scott 的构造超出了本条目的范围，因为它涉及到代数和拓扑的高级工具；有关详细信息，请参阅（Meyer 1982），（Barendregt，1985，第 18.2 章）或（Hindley 和 Seldin，2008，第 16 章）。相反，我们将讨论一个更一般的问题：什么是 λ 演算的模型？也就是说，暂时不考虑集合是函数、规则还是完全不同的东西，我们问的是，λ 演算的模型在数学结构上是什么样的。
7.1 λ-模型
事实证明，对于 λ 演算的模型概念有多种本质上等价的定义方式；参见（Barendregt，1985 年，第 5 章）或（Hindley 和 Seldin，2008 年，第 15 章）。在接下来的内容中，我们将讨论我们认为对于熟悉一阶逻辑标准语义的哲学家来说最可接受的概念，即所谓的句法 λ 模型。这些模型最早出现在（Hindley 和 Longo，1980 年），（Koymans，1982 年）和（Meyer 1982 年）的工作中。它们得名于它们的子句与 λ 演算的句法规则密切对应。这在某种程度上是不令人满意的，并激发了“无语法”定义（见下文）。与此同时，句法 λ 模型为进入 λ 模型的世界提供了一个相当透明和易于理解的途径。此外，尽管存在概念上的缺陷，句法模型在 λ 演算的语义研究中已被证明是一个技术上有用的工具。
为了避免上述提到的集合论问题，大多数 λ 模型的定义使用所谓的应用结构。其思想是将 λ 项的指称视为未经分析的一阶“函数对象”，而不是集合论函数。相应地，我们将函数应用视为这些函数对象上的未经分析的二元操作：
定义 应用结构是一个二元组(D,⋅)，其中 D 是某个集合，⋅ 是 D 上的二元运算。为了避免平凡模型，我们通常假设 D 至少有两个元素。
应用结构在某种意义上是函数空间的一阶模型，满足问题方程 X≅XX。λ-模型则是在其上定义的。
对于我们的 λ-模型的定义，我们使用赋值——这是一种在一阶语义中常见的概念。赋值将变量赋予指称，并主要用于 λ-运算符的语义子句中。此外，它们还可以用于以一阶量词 ∃x 和 ∀x 的语义方式表达领域上的一般性断言。
在一个应用结构（D,⋅）中，一个赋值是一个函数 ρ，它将一个元素 ρ(x)∈D 分配给每个变量 x。
作为一个有用的符号表示，对于一个应用结构（D,⋅）中的赋值 ρ，一个变量 x 和一个对象 d∈D，我们定义赋值 ρ [x↦d] 如下：ρ x↦d={d 如果 y=xρ(y)否则换句话说，ρ [x↦d] 是将 x 的值改为 d，同时保持 ρ 下的所有其他值不变的结果。
语法 λ-模型是一个三元组 M=(D,⋅,[[ ]])，其中 (D,⋅) 是一个应用结构，[[ ]] 是一个函数，它将每个 λ-项 M 和赋值 ρ 分配给一个表示 [[M]]ρ∈D，满足以下约束条件：
[[x]]ρ=ρ(x)
[[MN]]ρ=[[M]]ρ⋅ [[N]]ρ
[[λxM]]ρ⋅d=[[M]]ρ [x↦d]，对于所有的 d∈D
[[λxM]]ρ=[[λxN]]ρ，只要对于所有的 d∈D，我们有 [[M]]ρ [x↦d]=[[N]]ρ [x↦d]
[[M]]ρ=[[M]]σ，只要对于所有的 x∈FV(M)，我们有 ρ(x)=σ(x)
直观地说，在模型 M 中，[[M]]ρ 是由 λ 项 M 在估值 ρ 下表示的函数对象。
现在很容易定义一个 λ-模型 M 满足方程 M=N 的含义，符号化表示为 M⊨M=N：
定义（满足性）。
当且仅当对于所有的 ρ，我们有 [[M]]ρ=[[N]]ρ。
用文字表达：在模型 M 中，只有当 λ-项 M 和 N 在底层应用结构的每个赋值下具有相同的指称时，方程 M=N 才成立。
注意，在语法 λ 模型的定义中，第 3 和第 4 条直接对应于 λ 规则 β 和 ξ（参见上面的第 5.1 节）。这是我们模型的“语法”性质。虽然这可能在语义上不令人满意（见下文），但它相对容易证明由语法 λ 模型提供的语义的完备性定理；参见（Barendregt，1985，定理 5.3.4）和（Hindley 和 Seldin，2008，定理 15.12）：
定理 对于所有的项 M、N，如果在 λ 中可导出 M=N，则对于所有的语法 λ 模型 M，我们有 M⊨M=N。
这个定理为语义提供了第一个“理智检查”。但请注意，到目前为止，我们还没有证明存在任何语法 λ 模型。
这个担忧通过构建所谓的“术语模型”得到解决，这些模型与一阶语义中的著名亨金构造类似。为了定义这些模型，我们首先需要给定 λ 项 M 的 λ 等价类的概念。这个类别包含了与 M 在 λ 下证明相同的项：
[M] λ={N:λ 证明 M=N}
然后我们通过以下方式定义 λ 的术语模型 T：
D={[M] λ:M 是一个 λ 术语}
[M] λ⋅ [N] λ=[MN] λ
[[M]]ρ=[M[x1:=N1]…[xn:=Nn]]λ，其中 FV(M)={x1,…,xn} 和 ρ(x1)=N1,…,ρ(xn)=Nn
很容易看出这确实定义了一个语法 λ 模型。实际上，很容易验证在 λ 的项模型中，我们有：
T⊨M=N 当且仅当 λ 推导出 M=N。
这为 λ 与语法 λ 模型类之间的完备性证明提供了一条非常简单的途径；参见（Meyer, 1982, 98–99）中对这种结果的少数明确提及之一：
定理 对于所有的项 M,N，如果对于所有的语法 λ 模型 M，我们有 M⊨M=N，则在 λ 中可导出 M=N。
该证明是一个简单的反证法证明，它使用术语模型 T 作为 λ 中任何不可导出的等式的反例。
但是有理由对作为 λ 演算的语法 λ 模型作为语义学的不满。首先，通过第 3 和第 4 条款反映了 β 和 ξ 规则，完备性结果“内置”在语义学中。从语义学的角度来看，这是不令人满意的，因为这意味着通过语法 λ 模型，我们实际上并没有直接了解到应用结构需要满足什么条件才能充分地模拟 λ 演算。
相关的担忧是第 3 和第 4 条款不具有递归性质。也就是说，它们不允许我们通过部分的指示和关于用于组合它们的语法操作的信息来计算复杂 λ 项的指示。在我们的语法中（参见第 2 节），有两种构建复杂 λ 项的方式：形式为 MN 的应用项和形式为（λx [M]）的抽象项。我们的语法 λ 模型的第 1 条款是用于语法应用操作的递归条款，但我们没有用于语法 λ 抽象操作的递归条款。第 3 和第 4 条款只是对指示函数 [[ ]]的条件，而不是递归条款。这是不令人满意的，因为这意味着通过语法 λ 模型，我们并没有真正为 λ 运算符提供一个组合语义学。
这些担忧在无语法 λ 模型的发展中得到了解决。对无语法模型的全面讨论超出了本条目的范围；但是请参阅（Barendregt，1985 年，第 5.2 章）和（Hinley 和 Seldin，2008 年，第 15B 章）了解详细信息。可以说，无语法 λ 模型的定义涉及确定在哪些条件下适合解释 λ 演算的应用结构。然后，得到的 λ 模型确实提供了（更接近）递归的组合语义，其中 λ 抽象的句法操作由应用结构上的相应语义操作来解释。
然而，值得注意的是，句法 λ 模型和无语法 λ 模型在某种意义上是等价的：每个句法 λ 模型都定义了一个无语法 λ 模型，反之亦然；请参阅（Barendregt，1985 年，定理 5.3.6）和（Hinley 和 Seldin，2008 年，定理 15.20）了解详细信息。从技术角度来看，这个结果使我们可以自由地在不同的 λ 模型表达之间切换，并在给定的上下文中使用最方便的模型概念。同时，可能有哲学上的原因使我们更喜欢一种表达方式而不是另一种，比如上述关于句法 λ 模型的语义担忧。
在进入模型构建之前，让我们简要提到有多种方法可以处理 λ 模型。到目前为止，我们忽略了一种特别有趣的方法，即从范畴论和范畴逻辑的角度来看。有一些著名的模型描述使用所谓的“笛卡尔闭范畴”；参见（Koymans，1982）。涵盖这些模型描述超出了本条目的范围，因为它需要熟悉范畴论中的各种概念；请参阅条目“范畴论”以了解所涉及的机制。而这些模型描述的详细信息，请参见（Barendregt，1985，第 5.4-6 节）。近年来，对于 λ 演算的范畴论方法重新引起了人们的兴趣，主要集中在 λ 演算的类型化版本上（请参见下面的第 8.2 节和第 9.1.2 节），但也包括本文讨论的无类型 λ 演算。例如，请参见（Hyland，2017）进行最新讨论。
7.2 模型构建
我们在第 7.1 节中看到的术语模型相当平凡：它直接反映了 λ 项的句法结构，通过模拟 λ 可证等价来精确建模。这使得术语模型在数学和哲学上相当无趣。构建和研究更有趣的具体 λ 模型是 λ 演算模型理论的主要目标之一。
我们已经提到了可能是最重要的，但肯定是第一个非平凡的 λ 演算模型：Scott 的 D∞。但还有其他有趣的模型构造，比如 Plotkin 和 Scott 的图模型 Pω，首次在（Plotkin 1972）和（Scott，1974）中描述。然而，这些模型构造通常依赖于相当复杂的数学方法，无论是对它们的定义还是对它们确实是 λ 模型的验证。因此，涵盖这些构造超出了本条目的范围；有关各种模型构造的概述，请参阅（Hinley 和 Seldin，2008，第 16F 章），有关许多形式细节，请参阅（Barendregt，1985，第 18 章）。
拥有不同模型的优势之一是可以从不同的角度看待 λ 演算中的相等性：每个不同的模型对 λ 项的等同性有不同的观点。在这个背景下，一个有趣的问题是：给定一类模型的 λ 理论是什么？在这个背景下，我们称一个 λ 模型类 C 是完备的，只要每个（一致的）λ 理论都被 C 中的某个模型满足。有关各种 λ 模型类的完备性和不完备性结果的概述，请参阅（Salibra，2003）。
8. 扩展和变体
8.1 组合逻辑
作为 λ 演算的姊妹形式，组合逻辑稍早发展，处理无变量的组合。组合逻辑确实比 λ 演算更简单，因为它缺乏变量绑定的概念。
组合逻辑的语言由组合子和变量构建。在选择基本组合子方面有一定的灵活性，但一些标准的组合子有 I、K、S、B 和 C。（这些名称并非随意选择。）
与 λ 演算一样，组合逻辑也关注可简化性和可证明性。主要的简化关系有：
通过翻译，可以从 λ 演算到组合逻辑。事实证明，尽管组合逻辑缺乏抽象的概念，但可以定义这样的概念，并在组合逻辑中模拟 λ 演算。这是一种翻译方法；它是递归定义的。
这个翻译是从内到外进行的，而不是从外到内。为了说明：
术语 λy [y] 的翻译，作为恒等函数的代表，根据此翻译被映射到恒等组合子 I（根据规则 4），如预期的那样。
我们一直称之为'K'的 λ 项 λx [λy[x]]，根据此翻译被映射到：
λx [λy[x]]≡λx [Kx] ⟨ 规则 1⟩≡K⟨ 规则 3⟩
这个翻译将其映射到切换其两个参数的 λ 演算 λx [λy[yx]]：
λx [λy[yx]]≡λx [C(λy[y])∗x]⟨ 规则 8⟩≡λx [CIx] ⟨λy [y] ≡I，根据规则 4⟩≡BCI)(λx [x])∗⟨ 规则 7⟩≡B(CI)I⟨(λx [x])∗≡I，根据规则 4⟩
我们可以确认 λ 演算 λx [λy[yx]]和翻译后的组合逻辑项 B(CI)I 具有类似的应用行为：对于所有的 λ 演算 P 和 Q，我们有
(λx [λy[yx]])PQ⊳(λy [yP])⊳QP;
同样地，对于所有的组合逻辑术语 P 和 Q，我们有
B(CI)IPQ⊳(CI)(IP)Q⊳IQ(IP)⊳Q(IP)⊳QP
我们只能对组合逻辑给予一瞥；有关该主题的更多信息，请参阅组合逻辑条目。在 λ 演算中讨论的许多问题在组合逻辑中有类似的对应物，反之亦然。
8.2 添加类型
在推理和计算的许多情境中，区分不同类型的对象是很自然的。引入这种区分的方式是要求某些公式、函数或关系只接受某些类型的对象作为参数或允许替换，而不是其他类型的对象。例如，我们可能要求加法+只接受数字作为参数。这种限制的效果是禁止将 5 和恒等函数 λx.x 相加。将对象分类为类型也是从（未排序的或一排序的）一阶逻辑到多排序一阶逻辑的思想背后的原理。（有关多排序一阶逻辑的更多信息，请参阅（Enderton，2001）和（Manzano，2005）。）目前，λ 演算不支持这种区分；任何项都可以应用于任何其他项。
扩展无类型的 λ 演算以区分不同类型的对象是很直观的。本条目仅限于无类型的 λ 演算。有关我们在添加类型时得到的 λ 演算扩展的详细讨论，请参阅类型理论和 Church 的类型理论的条目，并参阅（Barendregt，Dekkers，Statman，2013）以获取有关该主题的书籍长度的处理。
从模型论的角度来看，有趣的是（Scott，1980）使用无类型 λ 演算的范畴模型（参见第 7.1 节）从有类型 λ 演算的范畴模型推导出来，以论证有类型演算在概念上优先于无类型演算。
9. 应用
9.1 逻辑 à la λ
λ 演算与逻辑有两种联系。
9.1.1 逻辑常量的术语
在上面的组合子表中，我们定义了组合子 T 和 F，并说它们分别作为 λ 演算中真值 true 和 false 的表示。这些术语如何作为真值起作用？
结果发现，当将 λ 演算视为一种编程语言时，可以将条件语句“如果 P 则 A 否则 B”简单地写为 PAB，其中当然 P、A 和 B 被理解为 λ 项。如果 P⊳T，即 P 为'true'，那么我们有
if-P-then-A-else-B:=PAB⊳TAB⊳A,
（回想一下，根据定义，T≡K）如果 P⊳F，即 P 是“假”，那么
如果-P-那么-A-否则-B:=PAB⊳FAB⊳B，
（回想一下，根据定义，F≡KI）这正是我们对 if-then-else 的期望。如果 P 既不缩减为 T 也不缩减为 F，那么我们通常无法确定 if-P-then-A-else-B 的结果。
我们刚刚勾勒出的对经典真值表逻辑中一些熟悉的真值和逻辑连接词的编码，并没有显示出 λ 演算和经典逻辑之间的密切关系。这种编码只能显示出经典真值表逻辑的计算规则在 λ 演算中的嵌入性。如果对于所讨论的逻辑有足够的可计算成分（例如，如果逻辑蕴含关系是可计算的，或者如果可计算的可导出关系等），那么除了经典真值表逻辑之外的其他逻辑也可以在 λ 演算中表示出来。有关使用 λ 演算进行计算的更多信息，请参见下面的第 9.2 节。逻辑和 λ 演算之间更本质的关系在下一节中讨论。
9.1.2 类型化 λ 演算和 Curry-Howard-de Bruijn 对应关系
在这里描述的逻辑和 λ 演算之间的对应关系是通过一种称为类型的工具来实现的。本节概述了类型理论这一学科的初步发展。我们只对发展类型理论感兴趣，以使所谓的 Curry-Howard-de Bruijn 对应关系可见。有关更详细的处理，请参见类型理论条目；另请参阅（Hindley，1997）和（Barendregt，Dekkers，Statman，2013）。
类型理论通过要求给术语赋予类型来丰富无类型的 λ 演算。在无类型的 λ 演算中，无论 M 和 N 是什么，应用 MN 都是合法的术语。这种自由使人们能够形成诸如 xx 这样可疑的术语，从而形成诸如悖论组合子 Y 的术语。人们可能希望基于以下理由排除诸如 xx 这样的术语：x 既作为函数（在应用的左侧）又作为参数（在应用的右侧）。类型理论为我们提供了使这种直观论证更加精确的资源。
为术语分配类型 类型理论的语言始于一组（无限）的类型变量（假定与 λ 演算的变量集合和符号‘λ’本身不相交）。类型集由类型变量和操作 σ→τ 组成。类型理论中的变量现在带有类型注释（与无类型 λ 演算的未装饰术语变量不同）。已标记的变量呈现为‘x:σ’；直观解读是‘变量 x 具有类型 σ’。判断‘t:σ→τ’的直观解读是术语 t 是一个将类型为 σ 的参数转换为类型为 τ 的参数的函数。给术语变量分配类型后，有以下类型规则：
(M:σ→τ)(N:σ):τ
和
(λx:σ [M:τ]):σ→τ
上述两个规则定义了类型分配给应用和抽象项的方式。类型理论的术语集是根据这些形成规则构建的术语集合。
类型理论中术语集合的上述定义足以排除诸如 xx 之类的术语。当然，'xx'根本不是一个带类型的术语，原因很简单，它没有被分配任何类型。所指的是，没有类型 σ 可以被分配给 x，以使'xx'能够以合法的方式进行注释，从而成为一个带类型的术语。我们不能给 x 分配一个类型变量，因为这样左侧的 x 的类型将不是一个函数类型（即形状为'σ→τ'的类型）。此外，我们也不能给 x 分配一个函数类型 σ→τ，因为这样 σ 将等于 σ→τ，这是不可能的。
以 I、K 和 S 为例，考虑分配给它们的类型：
（请参阅 Hindley（1997）的主要类型表以获取更详尽的列表。）如果我们将“→”解读为蕴涵，将类型变量解读为命题变量，则我们可以在表的右侧列中识别出三个熟悉的重言式。所使用的语言很简单：只有命题变量和蕴涵；没有其他连接词。
这个表格暗示了类型化 λ 演算和形式逻辑之间的有趣对应关系。难道真的可以将分配给公式的类型，当作逻辑公式时是有效的吗？是的，尽管“有效性”需要理解为非经典有效性：
定理 如果 τ 是某个 λ 项的类型，则 τ 在直觉上是有效的。
这个定理的逆命题也成立：
定理 如果 ϕ 是一个直觉上有效的逻辑公式，其唯一的联结词是蕴含 (→)，那么 ϕ 是某个 λ-项的类型。
当一个人将直觉有效性与某种自然演绎形式中的可导性等同起来时，可以看到这种对应关系。关于这两个定理的证明，请参见 (Hindley, 1997, 第 6 章)。
前两个定理之间表达的直觉有效性和可类型化之间的对应关系被称为 Curry-Howard-de Bruijn 对应关系，这是三位独立注意到的逻辑学家的名字。所述的对应关系仅适用于命题直觉逻辑，限制在仅包含蕴含连接词→的片段中。人们也可以将对应关系扩展到其他连接词和量词，但最清晰的对应关系是在仅限于蕴含的片段层面上。有关详细信息，请参见（Howard，1980）。
9.2 计算
人们可以用简单的方式表示自然数，如下所示：
定义（有序元组，自然数）λ-项的有序元组 ⟨a0,…an⟩ 被定义为 λx [xa0…an]。然后，将自然数 n 对应的 λ-项 ┌n┐ 定义为：┌0┐=I，对于每个 k，┌k+1┐=⟨F,┌k┐⟩。
在这个表示中，对应于数字 1 的 λ-项是：
┌1┐≡⟨F,┌0┐⟩≡⟨F,I⟩≡λx [xFI]
对应于数字 2 的 λ 项，在这个表示中是：
┌2┐≡⟨F,┌1┐⟩≡λx [xFλx[xFI]]
类似地，┌3┐ 是 λx [xFλx[xFλx[xFI]]]。
可以使用各种自然数的表示方法；这种表示方法只是其中之一。[6]
使用 λ 演算提供的元素，可以表示所有递归函数。这表明该模型与图灵机和寄存器机等其他计算模型具有相同的表达能力。有关这些不同计算模型之间关系的更详细讨论，请参阅有关图灵和教堂方法比较的部分，该部分在教堂-图灵论文中。
定理：对于每个具有 n 个参数的递归函数 f，存在一个 λ 项 f∗，使得
对于所有自然数 a1,…an: f(a1,…an)=y 当且仅当 λ⊢f∗⟨¯a1,…,¯an⟩=¯y
证明见附录。
由于递归函数类是所有可计算（数论）函数的充分表示，根据上述工作，我们发现所有可计算（数论）函数可以在 λ 演算中忠实地表示。
9.3 关系
λ 演算在入口开始处给出的动机是基于将 λ 表达式解读为函数的描述。因此，我们理解'λx [M]'是一个（或者是）函数，给定 x，给出 M（通常情况下，尽管不一定，涉及 x）。但是，并不一定要将 λ 项解读为函数。可以将 λ 项理解为表示关系，并将抽象项'λx [M]'解读为一元关系（或属性）R，当且仅当 M 满足参数 x 时，关系 R 成立（参见 Carnap 1947，第 3 页）。在关系解读中，我们可以将应用项 MN 理解为一种断言形式。可以使用 β 转换原则理解这些项：
(λx [M])a=M [x:=A],
它说，对于谓词 A，抽象关系 λx [M] 是通过将 A 插入 M 中所有自由出现的 x 来获得的关系。
作为对 λ 演算这种方法的具体例子，考虑一个扩展了一阶逻辑的系统，其中可以使用 λ 项来形成新的原子公式，具体如下：
语法：对于任意公式 ϕ 和任意有限序列 x1,…,xn 的变量，表达式‘λx1…xn [ϕ]’是一个元数为 n 的谓词符号。以这种方式扩展自由变量和约束变量的概念（使用函数 FV 和 BV）。
FV(λx1…xn [ϕ])=FV(ϕ)−{x1,…xn}
和
BV(λx1…xn [ϕ])=BV(ϕ)∪{x1,…xn}
假设推导为所有等价式的全称闭包
λx1…xn ϕ ↔ϕ [x1,…xn:=t1,…tn]
其中 ϕ [x1,…xn:=t1,…tn] 表示将术语 tk 替换为变量 xk (1≤k≤n) 的同时替换。
对于一个一阶结构 A 和一个将 A 的元素分配给变量的赋值 s，定义
A⊨λx1…xn ϕ [s] 当且仅当 A⊨ϕ [x1,…xn:=t1,…tn][s]
根据这种方法，我们可以使用 λ 来处理几乎任何公式，甚至复杂的公式，就好像它们是原子的一样。我们在推导和语义部分中看到了 β-还原的原则。这种方法遵循 λ 项的关系解读可以在语义中清楚地看到：根据一阶逻辑的标准 Tarski 风格语义，一个公式（可能带有自由变量）的解释表示一组元素结构的元组，当我们改变将元素结构分配给变量的变量赋值时。
人们可以“内化”这种函数式方法。这在各种属性理论的情况下都是如此，这些理论是用于推理关于属性作为形而上学对象的形式理论（Bealer 1982，Zalta 1983，Menzel 1986，1993 和 Turner 1987）。这种理论在某些形而上学研究中被使用，其中属性是要进行研究的形而上学实体。在这些理论中，形而上学关系是感兴趣的对象（或其中之一）；就像我们在算术的形式理论中添加构建符号+和 × 来构建数字一样，在属性理论中使用 λ 来构建关系。这种方法与上述方法相反。在上述方法中，通过将其作为构建原子公式的配方来将 λ 添加到一阶逻辑的语法中；它是一个新的公式构建运算符，类似于 ∨ 或→或其他连接词。在属性理论的情况下，λ 的作用更像是算术的形式理论中的+和 ×：它用于构建关系（在这种情况下，关系被理解为一种形而上学对象）。不过，与+和 × 不同，λ 会绑定变量。
为了说明在这种情况下如何使用 λ，让我们检查一个典型应用的语法（McMichael 和 Zalta，1980）。通常会有一个谓词运算符（或更准确地说，一族谓词运算符）pk（k≥0）。在一个语言中，我们有术语 MARY 和 JOHN 以及二元关系 loves，我们可以形式上表示：
约翰爱玛丽：loves(JOHN,MARY)
约翰爱玛丽的属性：λ [loves(JOHN,MARY)]（注意 λ 不绑定任何变量；我们可以称之为“空绑定”。这样的属性可以理解为命题。）
约翰爱某个对象 x 的属性：λx [loves(JOHN,x)]。
玛丽被某物所爱的属性：λ [∃x(loves(x,MARY))]（另一个空绑定的实例，即命题）。
John 爱 Mary 的属性的预测：p1(λx [loves(JOHN,x)],MARY)。
John 爱 Mary 的属性（0 元）的预测：p0(λx [loves(JOHN,MARY)])。
对象 x 和 y 的属性，x 爱 y：λxy [loves(x,y)]。
对于一个对象 x，它爱自己的属性：λx [loves(x,x)]。
对于对象 x 和 y，x 爱 y 的属性应用于 John 和 Mary（按顺序）：p2(λxy [loves(x,y)],JOHN,MARY)。
我们使用 β 转换原则对这些 λ 项进行推理，例如：
pn(λx1,…xn [A],t1,…,tn)↔A [x1,…xn:=t1,…,tn]
形式上，谓词操作符 pk 是一个(k+1)-元谓词符号。第一个参数应该是一个具有 k 个参数的 λ 项，其余的参数应该是 λ 项主体的参数。上面的 β 原则表明，当 n 个 λ 项 L 的主体对这些项成立时，n 元 λ 项 L 到 n 个项的谓词成立。
事实证明，在这些理论中，我们可能或可能无法完全致力于 β 转换原则。实际上，在某些属性理论中，完全的 β 转换原则会导致悖论，因为当完全的 β 转换原则到位时，可以重演罗素式的论证。在这种情况下，通过要求 λ 项的主体不包含进一步的 λ 项或量词来限制 λ 公式的形成。有关进一步讨论，请参见（Orilia，2000）。
λ 演算中以 λ 演算形式化的属性理论之所以具有特殊的哲学重要性，其中一个原因是演算的超内涵性质（见第 1.2 节）。如果一个属性概念不仅仅是在每个可能的世界中由完全相同的对象实例化，即不确定地共指属性，则可以称之为“超内涵的”。Bealer、Zalta、Menzel 和 Turner 理论描述的属性和关系正好具有这种特征。换句话说，这些理论是超内涵属性理论。近年来，在形而上学中对超内涵属性概念的兴趣显著增加（Nolan 2014），相应地，以 λ 演算形式化的属性理论也将可能受到更多的关注。
在数学基础的背景下，Zalta 和 Oppenheimer（2011）主张将 λ-项的关系解释置于功能解释之上，具有概念上的优先性。
Bibliography
Baader, Franz and Tobias Nipkow, 1999, Term Rewriting and All That, Cambridge: Cambridge University Press.
Barendregt, Henk, 1985, The Lambda Calculus: Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics 103), 2nd edition, Amsterdam: North-Holland.
Barendregt, Henk, 1993, “Lambda calculi with types”, in S. Abramsky, D. Gabbay, T. Maibaum, and H. Barendregt (eds.), Handbook of Logic in Computer Science (Volume 2), New York: Oxford University Press, pp. 117–309.
Barendregt, Henk, Wil Dekkers, and Richard Statman., 2013, Lambda Calculus With Types, Cambridge: Cambridge University Press.
Bealer, George, 1982, Quality and Concept, Oxford: Clarendon Press.
van Benthem, Johan, 1998, A Manual of Intensional Logic, Stanford: CSLI Publications.
Carnap, Rudolf, 1947, Meaning and Necessity, Chicago: University of Chicago Press.
Church, Alonzo, 1932, “A set of postulates for the foundation of logic”, Annals of Mathematics (2nd Series), 33(2): 346–366.
Cutland, Nigel J., 1980, Computability, Cambridge: Cambridge University Press.
Doets, Kees and Jan van Eijk, 2004, The Haskell Road to Logic, Maths and Programming, London: College Publications.
Enderton, Herbert B., 2001, A Mathematical Introduction to Logic, 2nd edition, San Diego: Harcourt/Academic Press.
Frege, Gottlob, 1893, Grundgesetze der Arithmetik, Jena: Verlag Hermann Pohle, Band I; partial translation as The Basic Laws of Arithmetic, M. Furth (trans.), Berkeley: University of California Press, 1964.
Kleene, Stephen C., 1981, “Origins of recursive function theory”, Annals of the History of Computing, 3(1): 52–67.
Heim, Irene and Angelika Kratzer, 1998, Semantics in Generative Grammar, Malden, MA: Blackwell.
Hindley, J. Roger, 1997, Basic Simple Type Theory (Cambridge Tracts in Theoretical Computer Science 42), New York: Cambridge University Press.
Hindley, J. Roger and G. Longo, 1980, “Lambda-calculus Models and Extensionality.” Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 26: 289–310.
Hindley, J. Roger and Jonathan P. Seldin, 2008, Lambda-Calculus and Combinators: An Introduction, 2nd edition, Cambridge: Cambridge University Press.
Howard, William A., 1980, “The formula-as-types notion of construction”, in J. Hindley and J. Seldin (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus, and Formalism, London: Academic Press, pp. 479–490.
Hyland, J. Martin E., 2017, “Classical Lambda Calculus in Modern Dress”, Mathematical Structures in Computer Science, 27(5): 762–781.
Koymans, C.P.J., 1982, “Models of the Lambda Calculus”, Information and Control, 52: 306–332.
Manzano, Maria, 2005, Extensions of First-order Logic (Cambridge Tracts in Theoretical Computer Science 19), Cambridge: Cambridge University Press.
McCarthy, John, 1960, “Recursive functions of symbolic expressions and their computation by machine (Part I)”, Communications of the ACM, 3(4): 184–195.
McMichael, Alan and Edward N. Zalta, 1980, “An alternative theory of nonexistent objects”, Journal of Philosophical Logic, 9: 297–313.
Menzel, Christopher, 1986, “A complete, type-free second order logic of properties, relations, and propositions”, Technical Report #CSLI-86-40, Stanford: CSLI Publications.
Menzel, Christopher, 1993, “The proper treatment of predication in fine-grained intensional logic”, Philosophical Perspectives 7: 61–86.
Meyer, Albert R., 1982, “What is a model of the lambda calculus?”, In Information and Control, 52(1): 87–122.
Nederpelt, Rob, with Herman Geuvers and Roel de Vriejer (eds.), 1994, Selected Papers on Automath (Studies in Logic and the Foundations of Mathematics 133), Amsterdam: North-Holland.
Nolan, Daniel, 2014, “Hyperintensional metaphysics”, Philosophical Studies, 171(1); 149–160.
Orilia, Francesco, 2000, “Property theory and the revision theory of definitions”, Journal of Symbolic Logic, 65(1): 212–246.
Partee, Barbara H., with Alice ter Meulen and Robert E. Wall, 1990, Mathematical Methods in Linguistics, Berlin: Springer.
Plotkin, G.D., 1972, A Set-Theoretical Definition of Application, School of Artificial Intelligence, Memo MIP-R-95, University of Edinburgh.
Revesz, George E., 1988, Lambda-Calculus, Combinators, and Functional Programming, Cambridge: Cambridge University Press; reprinted 2008.
Rosser, J. Barkley, 1984, “Highlights of the History of the Lambda-Calculus”, Annals of the History of Computing, 6(4): 337–349.
Salibra, Antonio, 2003, “Lambda calculus: models and theories”, in Proceedings of the Third AMAST Workshop on Algebraic Methods in Language Processing (AMiLP-2003), No. 21, University of Twente, pp. 39–54.
Schönfinkel, Moses, 1924, “On the building blocks of mathematical logic”, in J. van Heijenoort (ed.), From Frege to Gödel: A Source Book in Mathematical Logic, Cambridge, MA: Harvard University Press, 1967, pp. 355–366.
Scott, Dana, 1974, “The LAMBDA language”, Journal of Symbolic Logic, 39: 425–427.
–––, 1980, “Lambda Calculus: Some Models, Some Philosophy”, in J. Barwise, H.J. Keisler, and K. Kunen (eds.), The Kleene Symposium, Amsterdam: North-Holland, pp. 223–265.
Troelstra, Anne and Helmut Schwichtenberg, 2000, Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science 43), 2nd edition, Cambridge: Cambridge University Press.
Turing, Alan M., 1937, “Computability and λ-definability”, Journal of Symbolic Logic, 2(4): 153–163.
Turner, Richard, 1987, “A theory of properties”, Journal of Symbolic Logic, 52(2): 455–472.
Zalta, Edward N., 1983, Abstract Objects: An Introduction to Axiomatic Metaphysics, Dordrecht: D. Reidel.
Zalta, Edward N. and Paul Oppenheimer, 2011, “Relations versus functions at the foundations of logic: type-theoretic considerations”, Journal of Logic and Computation 21: 351–374.
Zerpa, L., 2021, “The Teaching and Learning of the Untyped Lambda Calculus Through Web-Based e-Learning Tools”, in K. Arai Intelligent Computing (Lecture Notes in Networks and Systems: Volume 285), Cham: Springer, pp. 419–436.
Academic Tools
Other Internet Resources
The Lambda Calculator, a tool for working with λ-terms with an eye toward their use in formal semantics of natural language.
Lambda Evaluator, for visualizing reductions. Standard combinators and Church numerals are predefined.
Lambda calculus reduction workbench, for visualizing reduction strategies.
“λ-Calculus: Then and Now,” useful handout on the milestones in, contributors to, and bibliography on the λ-calculus, presented at the several Turing Centennial conferences. There also exists a video recording of the lecture given on the occasion of Princeton University’s celebration of the Turing Centennial in 2012.
In addition, see the very helpful discussion in (Zerpa 2021) on the use of e-learning tools for teaching and learning the untyped λ-calculus.
Related Entries
computer science, philosophy of | Curry’s paradox | logic: combinatory | logic: intensional | logic: intuitionistic | logic: second-order and higher-order | properties | semantics: Montague | type theory | type theory: Church’s type theory
Acknowledgments
The first author wishes to acknowledge the contributions of Henk Barendregt, Elizabeth Coppock, Reinhard Kahle, Martin Sørensen, and Ed Zalta in helping to craft this entry. He also thanks Nic McPhee for introducing him to the λ-calculus.
The second author would like to acknowledge the useful comments and suggestions of Fabrizio Cariani, Cameron Moy, Peter Percival, and Ed Zalta.
Copyright © 2023 by Jesse Alama Johannes Korbmacher <j.korbmacher@uu.nl>
最后更新于
