您只需要λ，第一部分：布尔值

近一个世纪前，阿隆佐·丘奇发明了简单、优雅但又难以捉摸的λ微积分。然后，他和艾伦·图灵一起证明了丘奇-图灵命题：任何可以用图灵机计算的东西都可以在λ微积分中计算。然而，几乎在我们有了数字计算机之后，我们就开始发明编程语言，随之而来的是大量的功能，既漂亮又可怕，其中许多似乎很难与可计算性的基本性质联系起来，更不用说具体的λ演算了。

虽然任何可以计算的东西，句号，都可以在lambda演算中计算，但您可能不想这样做：至少可以说，它很简朴，而且在设计时没有考虑到可读性方面的现代敏感性。我们开发所有这些语言和功能都是有原因的！尽管如此，丘奇不仅证明了用Lambda微积分计算任何可计算的东西都是可能的，而且还证明了人们可以如何做到这一点。

在本系列中，我们将研究一些使用lambda演算的极简工具来表示公共编程语言特性的方法。我们从可能最普遍的类型开始：布尔型。

Lambda演算的紧缩是极端的：你甚至没有布尔值。你所拥有的只有：

我们现在将详细回顾这些内容；如果您已经熟悉lambda演算，请随意跳过本部分。

Lambda抽象(“lambdas”、“Abstraction”和“Functions”也将可互换使用)引入单个变量的函数。

抽象写成λx。Y，表示变量x和表达式y，其中x现在作为主体中的绑定变量可用，并且x的任何封闭定义都被隐藏起来(即，λx。λx.。X=λx。λy.。Y≠λx.。λy.。x)。(我们暂时将严格假设词汇作用域。)。

在Haskell中，我们将改为\x->；y；在JavaScript中，函数(X){return y}或(X)=>；y。

应用程序(“函数应用程序”和“函数调用”将互换使用)将左边表达式的结果应用到右边的表达式。

对于表达式x和y，应用被写为xy，并且是左相关的，即a b c=(A B)c≠a(B C)。函数应用程序比λ抽象更紧密地绑定，即λx。λy.。Y x=λx。λy.。(Y X)≠λx。(λy.。Y)x。

在Haskell中，语法是相同的；在JavaScript中，我们会编写x(Y)或a(b，c)。但是请注意，由于lambda演算函数都是单参数函数，因此后者的一个更直接(虽然不太习惯)的等价函数是a(B)(C)。

变量写成或多或少的任意名称，通常是字母数字的(例如，Xx或Y0等)；但是，我们可以随意在名称中包含我们认为合适的非字母数字字符，因为语法的缺乏意味着几乎没有歧义的风险。

由于唯一可用的变量是那些被封闭的lambdas绑定的变量，我们还可以推断没有局部变量的let绑定，也没有任何类型的全局变量；lambda演算没有提供标准库。

最后，下表对lambda演算的语法与Haskell&；JavaScript中的相应语法进行了并排比较：

由于lambda演算的简洁性，我将免费使用几个记号上的便利：

正在写入λx y。Z是λx的缩写。λy.。老子。

写作？来代表我们还不知道的部分，就好像我们有一个支持洞的环境。

编写类型签名，就好像我们有一个类型系统，甚至是一个类型检查器，在任何特定时刻都具有尽可能多的多态性和推论。

忽略应用程序顺序、规范化、缩减、替换、值、引用、分配、复制、空间、时间、熵，以及任何和所有其他任何我想要的细节。

按照惯例，我将命名TitleCase中的类型，以及CamelCase中的Term和(局部)类型变量。

我会尽量避免太肆无忌惮地胡说八道，但现在，我会请你暂缓怀疑；我希望在以后的帖子中重新审视并证明其中一些是正确的。

Lambdas是引入值的唯一方式--它们是语言中唯一的“字面”语法。因此，我们可以推断唯一种类的运行时值一定是闭包。在lambda演算的解释器中，闭包可能由引入的变量的名称、lambda的主体和amp；一个映射组成，该映射将构造时关闭的任何变量的名称和值联系起来(同样，我们假定严格的词法作用域)。该语言的语义中没有位、字节、字、指针或对象；只有lambdas的运行时表示。

同样，lambdas也是引入变量的唯一方式-没有标准库、内置、原语、前奏或全局环境来提供公共定义。我们真的是从头开始烤苹果派。

所有这一切都提出了一个问题：在你甚至没有真假之分的情况下，你怎么做任何事情呢？Lambdas和变量做不到这一点，它们只是做了，所以这就离开了应用。当您拥有的只有应用程序时，一切看起来都像是lambda抽象，所以我们将使用lambdas表示布尔值。

当然，我们要找的不仅仅是布尔值；如果没有AND、OR、NOT、IF和其他所有东西，真和假就没有多大用处。因此，为了有用，我们对布尔值的表示也应该足以定义这些。但是，如果不使用if，您如何定义if呢？在像Haskell这样的懒惰语言中，我们可以将if定义为如下所示的函数：

If_：：Bool->；a->；a->；a If_cond Then_Else_=If Cond Then_Else_。

在像JavaScript这样的严格语言中，我们将取而代之的是备选方案的函数：

这两个定义都使用语言的原生布尔值和IF语法(一种用于实现嵌入式DSL的策略，称为“元循环”)，因此在lambda演算中是不可行的。但是，它们确实给了我们一个提示：在这两种情况下，我们都有一个函数接受条件、结果和替代，并使用第一个函数选择后两个中的一个。在lambda演算中，我们可以从以下内容开始：

(注意：lambda演算中没有任何关键字，所以没有什么可以阻止我为变量命名，比如if，这是我将免费利用的事实。)。

我们已经引入了if的定义，作为三个参数的函数；，现在我们该如何处理它们呢？Lambda演算鲜明的调色板使我们可以很容易地枚举我们可以用某个变量a做的所有事情：

忽略它，不管是干脆不提它(就像在λa中一样。λb.。B)，或者通过用绑定相同名称的另一个λ来隐藏它(如在λa中。λa.。a)。

提到它，不管是在λ的身体里(就像在λa.。A或λa.。λb.。A)，在应用程序的任一侧的某处(如在λa.。λb.。A b或λa。λb.。B a)，或两者的某种组合(如在λa.。(λb.。A)a)。

IF=λ条件，则为ELSE。Thenif=λ条件，然后是Else。其他。

但在这种情况下，条件根本不是条件的--值决不依赖于条件。显然，如果我们想让身体的行为像我们从其他语言中了解和喜爱的if一样，那么身体必须利用所有这三个变量。

让我们退后一步，让我们来看看if的参数的作用。Then和Else是被动的；我们只想根据cond的值使用或计算其中之一。因此，条件是关键：它扮演着积极的角色。

因此，与Haskell&；JavaScript中的if_function使用这些语言的功能来实现的方式相同，我们将IF cond Then Else定义为将条件应用于其他两个参数：

在λ演算的标准语义下，我们可以通过“η-Reducing”进一步简化这个定义，注意λx。F x的行为与单独使用f的行为相同。不过，为了清楚起见，我们将把这个定义和可能的其他定义保留为完整的、长于η的形式。

这感觉很奇怪，像是作弊：当然，我们只是把问题转移了。现在，我们没有决定返回哪个参数，而是将其推迟到cond。但是if和cond在语义上并不相同；if接受一个布尔值和另外两个参数，并返回后一个参数，而cond是一个布尔值-尽管很明显是一个表示为函数的布尔值。让我们写下if的类型，以使其更加精确：

尽管我们为条件的类型使用了尚未定义的名称Bool，但它与我们在Haskell中给出的if_类型相同；这是一个好兆头，表明我们在正确的道路上！它接受一个bool和两个a类型的参数，它必须返回其中的一个，因为这是它得到返回的a的唯一方法。但是布尔是什么呢？

从if的类型和定义向后看，我们看到cond应用于两个参数，因此必须是两个参数的函数。此外，它们都是a类型，并且它返回的值也必须是a类型，IF的类型才能保存。因此，我们可以这样定义Bool类型：

我在这里显式地使用for-all量词来阐明这一点，即任何特定的布尔值都必须能够应用于当时和其他任意类型a的值，无论是现在定义的还是将来定义的。

出于同样的原因，我们可以更明确地将if的类型编写为：

在这里和将来，可以假定局部类型变量以与Haskell相同的方式隐式泛化，如果没有以其他方式量化的话。

如果给定的Bool是返回相同类型的任意类型的两个参数的函数，则它必须选择其中一个参数返回。Bool只有两个可区分的居民，真和假，因此我们可以推断，既然将结果的选择推迟到Bool，真和假要真正不同，他们必须做出相反的选择。换句话说，TRUE必须返回THEN参数，而FALSE必须返回另一个参数：

TRUE，FALSE：booltrue=λ，然后是ELSE。ThenFalse=λ，然后为Else。其他。

我们终究没有解决这个问题，我们解决了它。我们注意到一个更深层次的见解：布尔值的这种编码使得If是多余的，因为如果我们可以将If应用于一个Bool和两个参数，我们就可以同样地将Bool直接应用于这些参数。

我们选择将Bool按接收到的相同顺序定义为将Bool应用于其他参数，但我们也可以很容易地交换它们：

在这种情况下，IF会更有用，因为它可以保持我们熟悉的参数顺序。作为读者的练习，考虑这种差异还会有什么其他影响。在句法和语义上有什么权衡呢？什么时候其中一个定义更方便，或者更不方便？

将布尔值与位(它们的最小表示形式)混为一谈通常很方便，但实际上它们完全不同。实际上，一些编程语言将布尔值定义为内存中的一个字节，可能将其值限制为0和1；另一些编程语言将它们定义为某个布尔类的实例或代数数据类型的构造函数。有些代码根本没有提供true和false之间的正式关系，只是提供了一个公共接口-鸭子类型。

从数学上讲，布尔值是命题逻辑中的值；格的上界和下界；半环的零和一；基数为2的集合的成员；以及许多不同上下文中的许多其他东西。

在操作上，布尔值代表选择，这是我们将重复看到的模式：用lambdas编码数据类型意味着将数据类型表示为支持其所有操作的函数。对布尔值的所有操作都可以通过在两个备选方案中进行选择来定义，这正是我们的编码所做的。

我们可以使用到目前为止构建的编码，通过定义布尔值上的一些其他操作(例如，逻辑运算符)来演示这一点。

在定义if时，我们可以对Bool执行的所有操作都是对其进行分支：

正如前面所讨论的，IF在操作上是冗余的-即，如果xyz在操作上等价于xyz-给定我们前面选择的bools的参数顺序。然而，它令人愉快地唤起了人们的回忆，因此它被用来澄清，所以我们可以停止谈论排序决定。

但是，如果我们希望返回具有相反值的Bool，我们应该传递哪些参数呢？回想一下上面对Bool的定义：

因此，要返回布尔值，每个参数也必须同样是布尔值。如果x为TRUE，将选择第一个参数，如果x为FALSE，将选择第二个参数，因此，如果我们想要与x相反的值，只需将其应用于任意位置的相反值：

因此，如果x为TRUE，NOT x将返回FALSE，如果x为FALSE，则返回TRUE；等于：

Not的类型是bool->bool，相当于(∀a.。A->；a->；a)->；∀a.。A->；a->；a因此，我们也可以通过获取结果Bool将应用到的额外参数并直接使用它们(尽管顺序相反)来定义Not：

如果您不习惯例如在Haskell中常用的所谓“咖喱函数”，这种定义风格可能会令人惊讶，但它在操作上等同于上面开发的定义。作为练习，试着找出为什么等价性成立。

或者和和彼此密切相关，所以我们将同时定义它们。两者都取两个布尔值并返回一个布尔值：

OR，AND：Bool->；Bool->；Boolor=λx y。？和=λx y。？

OR=λx y。如果x？？and=λx y。如果x？？

或者，如果x为TRUE，我们可以立即返回TRUE(“短路”)。对于和来说，情况正好相反：

OR=λx y。如果x为真？并且=λx y。如果x呢？错误

如果x为假，或者需要测试y是否为真；同样，如果x为真，则需要测试y是否也为真。再说一次，我们对bools所能做的只有BRANCH：

OR=λx y。如果x为真(如果y？？)并且=λx y。如果x(如果y？？)。错误。

OR=λx y。如果x为真(如果y为假)并且=λx y。如果x(如果y为true，则为false)为false。

令人愉快的是，如果y true false(以及同样y true false)在运算上与y等价。使用这种等价，我们可以简化这些定义，从而得到：

OR=λx y。如果x为真，yand=λx y。如果x y为false。

在这篇文章中，我们探索了如何定义一种无处不在的编程语言特性--布尔值--只不过是使用lambda演算的简朴装饰品。我们已经出现了一种语言，它不仅可以表达函数及其应用，还可以表达基本的形而上学概念，如真理。

在下一篇文章中，我们将介绍美丽的lambda编码：ML/Haskell样式的代数数据类型。