我一直在阅读关于λ演算的内容,并且喜欢其中提出的思想,但有些问题我无法解释;
λ演算怎样处理加法?
我知道
(\x . + x x) 3
这与3 + 3
相同,即6
,但是加法函数最初是如何实现的呢?
这是编译器/语言必须内置的内容吗,还是仅可以由λ演算定义?
我一直在阅读关于λ演算的内容,并且喜欢其中提出的思想,但有些问题我无法解释;
λ演算怎样处理加法?
我知道
(\x . + x x) 3
这与3 + 3
相同,即6
,但是加法函数最初是如何实现的呢?
这是编译器/语言必须内置的内容吗,还是仅可以由λ演算定义?
是的,您可以在λ演算中定义数字(以及任意数据类型)。 这是想法。
首先,让我们选择要定义的数字。 最简单的数字是自然数:0、1、2、3等。 我们如何定义这些数字? 通常的方法是使用Peano公理:
这里,S表示n的后继,或n+1。 因此,Peano自然数的前几个数字是0、S0、SS0、SSS0等——这是一种一元表示。
现在,在λ演算中,我们可以表示函数应用,因此我们可以表示Sn,但我们不知道如何表示0和S本身。但幸运的是,λ演算为我们提供了一种推迟这个选择的方法:我们可以将它们作为参数,并让其他人决定! 让我们用z表示我们得到的0,用s表示我们得到的S。然后我们可以按照以下方式表示前几个数字,写⟦n⟧表示“自然数n的λ演算表示”:
自然数n可以通过对0进行n次S应用来表示,lambda演算中的n也是将任意继承函数s应用n次于任何0z的结果。我们也可以定义继承函数:
在这里,我们可以看到后继函数会在确保n使用相同的z和s之后,向n应用一个额外的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:
data Either a b = Left a | Right b
):
data List a = Nil | Cons a (List a)
):
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 e
s 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 a
s 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).
\x \y . (\z . x(y(z)))