the*_*sti 6 lambda functional-programming lambda-calculus
我一直在读关于lambda演算,并喜欢它提出的想法,但有一些我无法解释的事情;
lambda演算如何增加数字呢？
我明白那个
(\x . + x x) 3
是一样的3 + 3,它是6,但如何将相加功能已经在第一时间得到落实？
这是编译器/语言必须内置的东西,还是只能由lambda演算定义？
Ant*_*sky 13
是的,您可以在lambda演算中定义数字(实际上是任意数据类型).这是个主意.
首先,让我们选择我们要定义的数字.最简单的数字是自然数:0,1,2,3等.我们如何定义这些？通常的方法是使用Peano公理:
这里,S表示n或n + 1 的后继.因此,前几个Peano自然数是0,S0,SS0,SSS0等等 - 它是一元表示.
现在,在lambda演算中,我们可以表示函数应用,因此我们可以表示S n,但我们不知道如何自己表示0和S. 但幸运的是,lambda演算为我们提供了一种推迟选择的方法:我们可以将它们作为参数,让其他人决定!让我们为我们给出的0 写z,为我们给出的S 写s.然后,我们可以表示如下,写⟦第几号ñ ⟧为"自然数的演算表示ñ ":
正如一个自然数Ñ是Ñ至0 S的应用中,一个拉姆达演算表示Ñ是一个应用程序Ñ拷贝任何后继函数小号到任何零ž.我们也可以定义继任者:
在这里,我们看到的是,继任者适用的一个额外副本小号到ň,确保后ñ使用相同ž和小号.我们可以看到这给了我们相同的表示,使用⇝进行"评估":
(是的,这会变得很密集,很难快速阅读.如果你觉得你需要更多的练习,那么通过它是一个非常好的练习 - 它导致我在我最初编写的内容中发现错误!)
现在,我们已经定义了0和S,所以这是一个好的开始,但我们也想要一个归纳原理.毕竟,这就是使自然数字成为现实的原因!那么,这将如何运作？好吧,事实证明我们基本上已经确定了.在以编程方式考虑我们的归纳原理时,我们需要一个函数,它将基本案例和归纳案例作为输入,并生成从自然数到某种输出的函数.我将输出称为" n的证明".然后我们的输入应该是:
换句话说,我们需要某种零值,以及某种后继函数.但这些只是我们的z和s论点!事实证明,我们将自然数表示为其归纳原理,我认为这很酷.
这意味着我们可以定义基本操作.我将在这里定义添加,并将其余部分作为练习.在我们的归纳公式中,我们可以定义如下:
这是在第二个论点上归纳定义的.那么我们如何翻译呢？它成为了:
这是从哪里来的？好吧,我们将我们的归纳原理应用于n.在基本情况下,我们返回m(使用环境s和z),如上所述.在归纳案例中,我们将后继(环境s)应用于我们得到的东西.所以这一定是对的!
看看这另一种方式是,由于ñ 小号 ž适用ň的副本小号到ž,我们有ñ(米 小号 ž)小号适用ñ副本小号来米 小号 ž,共计ñ + 米的副本s到z.再次,这是正确的答案!
(如果你仍然不相信,我鼓励你制定一个像⟦1+2⟧这样的小例子;它应该足够小,易于处理,但足够大,至少有点有趣.)
所以现在我们看到如何在纯无类型lambda演算中定义自然数的加法.如果你愿意,还有一些额外的想法可供进一步阅读; 这些更精简,更少解释.
这种表示技术更普遍适用; 它不仅仅适用于自然数字.它被称为教会编码,可以适用于表示任意代数数据类型.正如我们通过它们的归纳原理来表示自然数,我们通过它们的结构递归原理(它们的折叠)来表示所有数据类型:数据类型的表示是为每个构造函数接受一个参数的函数,然后应用该构造函数"对所有必要的论点.所以:
data Either a b = Left a | Right b):
data List a = Nil | Cons a (List a)):
请注意,在最后一种情况下,l本身就是一个编码列表.
此技术也适用于类型设置,我们可以在其中讨论数据类型的折叠(或catamorphisms).(我大多提到这个,因为我个人觉得它真的很酷.) data Nat = Z | S Nat然后是同构的forall a. a -> (a -> a) -> a,并且es的列表是同构的forall a. e -> (e -> a -> a) -> a,这只是公共类型签名的一部分foldr :: (e -> a -> a) -> a -> [e] -> a.普遍量化的as表示自然数或列表本身的类型; 它们需要进行普遍量化,因此传递这些需要更高级别的类型.同构性是由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,单个1).然后编码自然数就像这样简单
data Nat = Zero | PosNat Pos
但是我们的功能,比如加法,会变得更复杂(但速度更快).