教会数字:如何在lambda演算中编码零？

Question

我正在学习lambda演算,但我似乎无法理解数字0的编码.

" 函数接受函数和第二个值并将函数零次应用于参数 "为零？有没有其他方法来编码零？这里的任何人都可以帮我编码0吗？

Answer 1

见维基百科:

0 ? ?f.?x. x
1 ? ?f.?x. f x
2 ? ?f.?x. f (f x)
3 ? ?f.?x. f (f (f x))
...
n ? ?f.?x. fn x

Answer 2

"接受函数和第二个值并在函数上应用函数零次的函数"当然不是零.它的编码为零.当你处理普通的lambda演算时,你必须以某种方式编码数字(以及其他原始类型),并且每种类型都有一些要求.例如,对自然数的一个要求是能够将1添加到给定数字,而另一个要求能够区分零和更大的数字(如果您想了解更多,请查找"Peano算术").Dario引用的流行编码为您提供了这两个方面,并且它还通过函数表示整数N,该函数执行某些操作(编码为f参数)N次 - 这是一种使用自然的自然方式.

还有其他编码可能 - 例如,一旦您可以表示列表,您可以将N表示为N个项目的列表.这些编码有其优点和缺点,但上面的编码是迄今为止最受欢迎的编码.

Answer 3

如果你学会了演算,你可能已经知道,λxy.y ARG1*ARG2*将减少arg2的,因为x被换成什么,其余的(λy.y)是身份的功能.

你可以用许多其他方式写零(即提出不同的约定),但有充分的理由使用λxy.y. 例如,你希望零成为第一个自然数,所以如果你将后继函数应用于它,你得到1,2,3等等.使用函数λabc.b(abc),得到λxy.x(y ),λxy.x(x(y)),λxy.x(x(x(y)))等,换句话说,你得到一个整数系统.

此外,你想要零作为加法的中性元素.利用我们的后继函数S:=λabc.b(abc),我们可以将n +*m*定义为n S m,即将后继函数应用于m的n倍.我们的零λxy.y满足这一点,0 S m和m S 0都减小到m.