Lambda演算如何实现加法？

Question

Lambda演算如何实现加法？

lambdafunctional-programminglambda-calculus

10

我一直在阅读关于λ演算的内容，并且喜欢其中提出的思想，但有些问题我无法解释；

λ演算怎样处理加法？

我知道

(\x . + x x) 3

这与3 + 3相同，即6，但是加法函数最初是如何实现的呢？

这是编译器/语言必须内置的内容吗，还是仅可以由λ演算定义？

- theonlygusti

2个回答

4

假设您正在使用 Church数，而不是一些原始的数字类型，加法就是组合：

\x \y . (\z . x(y(z)))

如果您已经在λ演算中添加了某种原始数字类型，那么加法将必须成为原语或者必须根据类似于后继操作的某些东西来定义。

- user2357112

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Antal Spector-Zabusky · Accepted Answer

是的，您可以在λ演算中定义数字（以及任意数据类型）。这是想法。

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

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

这里，S表示n的后继，或n+1。因此，Peano自然数的前几个数字是0、S0、SS0、SSS0等——这是一种一元表示。

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

⟦0⟧ = λ z s . z
⟦1⟧ = λ z s . s z
⟦2⟧ = λ z s . s (s z)
⟦3⟧ = λ z s . s (s (s z))

自然数n可以通过对0进行n次S应用来表示，lambda演算中的n也是将任意继承函数s应用n次于任何0z的结果。我们也可以定义继承函数：

⟦0⟧ = λ z s . z
⟦S⟧ = λ n . λ z s . s (n z s)

在这里，我们可以看到后继函数会在确保n使用相同的z和s之后，向n应用一个额外的s。我们可以使用⇝表示"评估为"来看到这给我们相同的表示：

⟦0⟧ = λ z s . z
⟦1⟧ = ⟦S0⟧
= (λ n . λ z s . s (n z s))(λ z′ s′ . z′)
⇝ λ z s . s ((λ z′ s′ . z′) z s)
⇝ λ z s . s z
⟦2⟧ = ⟦SS0⟧
= (λ n . λ z s . s (n z s))((λ n′ . λ z′ s′ . s′ (n′ z′ s′))(λ z″ s″ . z″))
⇝ λ z s . s (s z)
⟦3⟧ = ⟦SSS0⟧
= (λ n . λ z s . s (n z s))((λ n′ . λ z′ s′ . s′ (n′ z′ s′))((λ n″ . λ z″ s″ . s″ (n″ z″ s″))(λ z‴ s‴ . z‴)))
⇝ λ z s . s (s (s z))

(是的，这变得密集而且很快难以阅读。如果你觉得需要更多练习，通过它进行工作是一个相当好的练习 - 这导致我在我最初编写的内容中发现了一个错误！)

现在，我们已经定义了0和S，这是一个好的开始，但我们也想要归纳原理。毕竟，这就是自然数的本质！那么，这将如何工作？嗯，事实证明我们基本上已经准备好了。在考虑我们的归纳原理时，我们希望一个函数，该函数将基础案例和归纳案例作为输入，并生成从自然数到某种输出的函数。我将输出称为“n的证明”。那么我们的输入应该是：

1.一个基础案例，即我们对0的证明。 2.一个归纳案例，即一个函数，该函数以n的证明作为输入，并产生Sn的证明。

换句话说，我们需要某种零值和某种后继函数。但这些只是我们的z和s参数！因此，事实证明我们正在用归纳原理来表示自然数，我觉得这很酷。

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

1. m + 0 = m 2. m + Sn = S(m + n)

这在第二个参数上进行归纳定义。那么我们该如何翻译它？变成了：

[+]= λm n. λ z s. n (m z s) s

这是从哪里来的？我们将归纳原则应用于n。在基本情况下，我们返回m（使用环境中的z和s），就像上面一样。在归纳情况下，我们对得到的内容应用后继（环境中的s）。因此这一定是正确的！

另一种看待这个问题的方法是，由于n z s将n个s副本应用于z，因此n（m z s）s将n个s副本应用于m z s，总共为n+m个s副本应用于z。同样，这是正确的答案！

如果您仍然不确定，我鼓励您进行一个小实例的练习，例如⟦1+2⟧; 这应该足够简单以便于操作，但又足够有趣。

现在我们看到如何在纯无类型λ演算中定义自然数的加法。如果您愿意，这里有一些进一步阅读的思考；这些更为简洁，解释较少。

This representation technique is more generally applicable; it's not just for natural numbers. It's called Church encoding, and can be adapted to represent arbitrary algebraic data types. Just as we represented the natural numbers by their induction principle, we represent all data types by their structural recursion principle (their fold): the representation of a data type is a function that takes one argument for each constructor, and then applies that "constructor" to all the necessary arguments. So:
- Booleans:
  - ⟦False⟧ = λ f t . f
  - ⟦True⟧ = λ f t . t
- Tuples:
  - ⟦(x,y)⟧ = λ p . p x y
- Sum types (data Either a b = Left a | Right b):
  - ⟦Left x⟧ = λ l r . l x
  - ⟦Right y⟧ = λ l r . r y
- Lists (data List a = Nil | Cons a (List a)):
  - ⟦Nil⟧ = λ n c . n
  - ⟦Cons x l⟧ = λ n c . c x l
Note that in the last case, l will be itself an encoded list.
This technique also works in a typed setting, where we can talk about folds (or catamorphisms) for data types. (I mostly mention this because I personally think it's really cool.) data Nat = Z | S Nat is then isomorphic to forall a. a -> (a -> a) -> a, and lists of es are isomorphic to forall a. e -> (e -> a -> a) -> a, which is just part of the type signature of the common foldr :: (e -> a -> a) -> a -> [e] -> a. The universally quantified as represent the type of the natural number or list itself; they need to be universally quantified, so passing these around requires higher-rank types. The isomorphism is witnessed by the fact that foldr Cons Nil is the identity function; for a natural number encoded as n, we similarly have n Z S recovering our original list.
If you're bothered by the fact that we only used natural numbers, we can define a representation for integers; for instance, a common unary-style representation is
```
 data Int = NonNeg Nat | NegSucc Nat
```
Here, NonNeg n represents n, and NegSucc n represents -(n+1); the extra +1 in the negative case ensures that there's a unique 0. It should be straightforward to convince yourself that you could, if you so desired, implement the various arithmetic functions on Int in a programming language with real data types; these functions could then be encoded in the untyped lambda calculus via Church encoding, and so we're set. Fractions are also representable as pairs, although I don't know of a representation that ensures all fractions are uniquely representable. Representing real numbers gets tricky, but IEEE 754 floating point numbers can be represented as 32-, 64-, or 128-tuples of booleans, which is horribly inefficient and bulky, but encodable.
More efficient representations of natural numbers (and integers, and so on) are also available; for example,
```
 data Pos = One
          | Twice     Pos
          | TwiceSucc Pos
```
encodes positive binary numbers (Twice n is 2*n, or adding a 0 to the end; TwiceSucc is 2*n + 1, or adding a 1 to the end; the base case is One, a single 1). Encoding the natural numbers is then as simple as
```
 data Nat = Zero | PosNat Pos
```
but then our functions, such as addition, get more complicated (but faster).