lambda - Lambda微积分将如何加数字？

Question

我一直在阅读关于lambda演算的文章，并且喜欢它提出的想法，但是有些事情我无法解释。

Lambda演算如何进行加法运算？

我明白那个

(\x . + x x) 3

与 3 + 3相同，即 6，但是首先要如何实现加法功能？

是编译器/语言必须内置的东西，还是可以仅由lambda微积分定义？

Answer 1

是的，您可以在lambda演算中定义数字（实际上是任意数据类型）。这是主意。

首先，让我们选择要定义的数字。最简单的数字是自然数：0、1、2、3，依此类推。我们如何定义这些？通常的方法是使用Peano axioms：


0是自然数。
如果n是自然数，则Sn是自然数。


在此，S表示n或n + 1的后继。因此，前几个Peano自然数为0，S0，SS0，SSS0，依此类推-这是一元表示形式。

现在，在lambda演算中，我们可以表示函数应用程序，因此可以表示Sn，但是我们不知道如何表示0和S本身。但是幸运的是，lambda演算为我们提供了一种推迟选择的方式：我们可以将它们作为参数，让其他人来决定！让我们将z表示为0，将s表示为S。然后，我们可以如下表示前几个数字，为​​“自然数n的lambda微积分表示形式”写⟦n⟧：


⟦0⟧=λz s。 ž
⟦1⟧=λz s。设
⟦2⟧=λz s。 s（s z）
⟦3⟧＝λzs。 s（s（s z））


就像自然数n是S的n个应用到0一样，n的lambda微积分表示是将任何后继函数s的n个副本应用到任何零z。我们也可以定义后继者：


⟦0⟧=λz s。 ž
⟦S⟧=λn。 λz s。 s（n z s）


在这里，我们确保后继者在确保n使用相同的z和s之后将s的一个额外副本应用于n。我们可以看到，这给了我们相同的表示形式，使用⇝表示“求值”：


⟦0⟧=λz s。 ž
⟦1⟧=⟦S0⟧
=（λn。λz s。s（n z s））（λz's'。z'）
λλz s。 s（（（λz's'。z'）z s）
λλz s。设
⟦2⟧=⟦SS0⟧
=（（λn。λz s。s（n z s））（（（λn'。λz's'。s'（n'z's'））（λz''s''。z''））
⇝（λn。λz s。s（n z s））（λz's'。s'（（λz“ s”。z“）z's'））
⇝（λn。λz s。s（n z s））（λz's'。s'z'）
λλz s。 s（（（λz's'。s'z'）z s）
λλz s。 s（s z）
⟦3⟧=⟦SSS0⟧
=（（λn。λzs。s（nzs））（（（λn'。λz's'。s'（n'z's'））（（（λn''。λz''s''。s'' （n''z''s''））（λz‴s‴。z‴）））
⇝（λn。λzs。s（nzs））（（（λn'。λz's'。s'（n'z's'））（λz''s''。s''（（λz‴ s‴。z‴）z” s”）））
⇝（λn。λz s。s（n z s））（（（λn'。λz's'。s'（n'z's'））（λz''s''。s''z''）
⇝（λn。λz s。s（n z s））（λz's'。s'（（（λz“ s”。s“ z”）z's'）））
⇝（λn。λz s。s（n z s））（λz's'。s'（s'z'））
λλz s。 s（（（λz's'。s'（s'z'））z s）
λλz s。 s（s（s z））


（是的，这变得很密集并且很难快速阅读。如果您觉得自己需要更多的练习，那么进行此练习是非常不错的练习–它导致我在最初编写的内容中发现了一个错误！）

现在，我们定义了0和S，这是一个好的开始，但是我们也需要归纳原理。毕竟，这就是使自然数成为实际数字的原因！那么，这将如何工作？好吧，事实证明我们已经基本设置好了。在以编程方式考虑归纳原理时，我们需要一个函数，该函数以基本情况和归纳情况为输入，并产生从自然数到某种输出的函数。我将输出称为“ n的证明”。那么我们的输入应该是：


一个基本情况，这是我们对0的证明。
归纳案例，它是将n的证明作为输入并产生Sn的证明的函数。


换句话说，我们需要某种零值和某种后继函数。但这只是我们的z和s参数！事实证明，我们将自然数表示为它们的归纳原理，我认为这很酷。

这意味着我们可以定义基本操作。我将在这里定义加法，其余的作为练习。在归纳公式中，我们可以定义加法如下：


m + 0 = m
m +锡= S（m + n）


这是第二个参数的归纳定义。那么我们该如何翻译呢？它成为了：


⟦+⟧＝λm n。 λz s。 n（m s z）s


这是从哪里来的？好吧，我们将归纳原理应用于n。在基本情况下，我们返回m（使用环境s和z），就像上面一样。在归纳的情况下，我们将继承者（环境）应用于获得的结果。所以这一定是对的！

另一种看待这种情况的方式是，由于n s z将s的n个副本应用于z，因此我们有n（m s z）s将s的n个副本应用于m s z，总共有n + m s的s到z。再次，这是正确的答案！

（如果您仍然不相信，我鼓励您提出一个小的示例，例如⟦1+2⟧；该示例应足够小以使其易于处理，但又应足够大以至于至少有点有趣。）



现在，我们来看看如何为纯无类型lambda演算中的自然数定义加法。如果您愿意，这里还有一些其他的想法供您进一步阅读；这些内容更简洁，解释也更少。


这种表示技术更普遍适用。这不仅是自然数。它称为Church encoding，并且可以适应于表示任意algebraic data types。正如我们用归纳原理表示自然数一样，我们也用结构递归原理（它们的折叠）来表示所有数据类型：数据类型的表示是一个对每个构造函数采用一个参数，然后应用“构造函数”的函数。所有必要的论点。所以：


布尔值：

⟦假⟧＝λf t。 F
“真” ＝λf t。 Ť

元组：

⟦（x，y）⟧=λp。 x

总和类型（data Either a b = Left a | Right b）：

⟦左x⟧=λl r。 x
⟦右y⟧=λl r。 RŸ

列表（data List a = Nil | Cons a (List a)）：

⟦Nil⟧=λn c。 ñ
⟦Consxl⟧=λn c。 ×



请注意，在最后一种情况下，l本身就是一个编码列表。
此技术也适用于类型化设置，在这里我们可以讨论数据类型的折叠（或同构）。 （我之所以这样提，是因为我个人认为它真的很酷。）data Nat = Z | S Nat然后与forall a. a -> (a -> a) -> a同构，而e的列表与forall a. e -> (e -> a -> a) -> a同构，这只是常见类型签名的一部分。 foldr :: (e -> a -> a) -> a -> [e] -> a。通用量化的a代表自然数或列表本身的类型；它们需要被普遍量化，因此传递这些参数需要higher-rank types。同构性由foldr Cons Nil是恒等函数来证明。对于编码为n的自然数，我们同样会n Z S恢复原始列表。
如果您对我们只使用自然数感到困扰，则可以定义整数的表示形式。例如，常见的一元样式表示形式是

data Int = NonNeg Nat | NegSucc Nat

这里， NonNeg n代表 n， NegSucc n代表 -(n+1)；否定情况下的多余 +1确保存在唯一的 0。要说服自己，如果您愿意，可以用一种具有真实数据类型的编程语言在 Int上实现各种算术函数，这应该很简单。这些函数然后可以通过Church编码在未类型化的lambda演算中进行编码，因此开始工作。分数也可以成对表示，尽管我不知道可以确保所有分数都是唯一可表示的表示形式。表示实数会很棘手，但是IEEE 754浮点数可以表示为32、64或128个元组的布尔值，这虽然效率低下而且笨重，但是可以编码。
还可以使用更有效的自然数表示法（以及整数等）。例如，

data Pos = One
         | Twice     Pos
         | TwiceSucc Pos

编码正二进制数（ Twice n是 2*n，或者在末尾添加 0； TwiceSucc是 2*n + 1，或者在末尾添加 1；基本情况是 One，a单个 1）。编码自然数就这么简单

data Nat = Zero | PosNat Pos

但随后我们的功能（例如加法）变得更加复杂（但速度更快）。