为何定义教会的数字

zer*_*ing 4 lambda-calculus

我想明白,为什么教会定义数字如下:

0 = ? f . ? x . x
1 = ? f . ? x . f x
2 = ? f . ? x . f f x
3 = ? f . ? x . f f f x
4 = ? f . ? x . f f f f x
Run Code Online (Sandbox Code Playgroud)

背后的逻辑是什么?

为什么0表示如下:

0 = ? f . ? x . x
Run Code Online (Sandbox Code Playgroud)

Joh*_*man 9

教会并没有努力实践.他试图证明关于lambda演算的表达能力的结果 - 原则上任何可能的计算都可以在lambda演算中完成,因此lambda演算可以作为可计算性研究的理论基础.为了做到这一点,有必要将数字编码为lambda表达式,以便像后继函数这样的东西很容易定义.这是显示lambda演算和Gödel的递归函数理论(它是关于自然数的可计算函数)的等价性的关键步骤.教堂数字基本上是方便的,虽然不是非常可读的数字编码.从某种意义上说,它没有任何非常深刻的逻辑.的权利要求不是1在其本质 ? f . ? x . f x,但后者是前者的可维修的编码.

这并不意味着它是一种任意编码.它有一个明确的逻辑.编码数字最自然的方式n是涉及到的n.教会数字使用n功能应用.自然数n由高阶函数表示,该函数将函数n时间应用于输入.1由应用一次2的函数,应用两次的函数等编码.这是一种非常自然的编码,特别是在lambda演算的背景下.此外,很容易在它们上定义算术的事实简化了lambda演算相当于递归函数的证明.

要在实践中看到这一点,您可以运行以下Python3脚本:

#some Church numerals:

ZERO = lambda f: lambda x: x
ONE = lambda f: lambda x: f(x)
TWO = lambda f: lambda x: f(f(x))
THREE = lambda f: lambda x: f(f(f(x)))

#function to apply these numerals to:

def square(x): return x**2

#so ZERO(square), ONE(square), etc. are functions
#apply these to 2 and print the results:

print(ZERO(square)(2), ONE(square)(2), TWO(square)(2),THREE(square)(2))
Run Code Online (Sandbox Code Playgroud)

输出:

2 4 16 256
Run Code Online (Sandbox Code Playgroud)

注意,这些数字是通过将数字2分别平方0次,1次,2次和3次获得的.


Rob*_*let 7

根据Peano公理,对于另一个自然数n,自然数是0或S(n):

0 = 0
1 = S(0)
2 = S(S(0))
...
Run Code Online (Sandbox Code Playgroud)

你可以看到教会数字作为Peano数字的推广,你提供自己的0和S:

0 = ?s.?z. z
1 = ?s.?z. s(z)
2 = ?s.?z. s(s(z))
...
Run Code Online (Sandbox Code Playgroud)

由于这是一个编程论坛,让我们在EcmaScript 6中创建一些教会数字:

const ZERO = s => z => z;
const ONE  = s => z => s(z);
const TWO  = s => z => s(s(z));
...
Run Code Online (Sandbox Code Playgroud)

您可以通过提供适当的零和后继来将这些Church数字转换为JavaScript数字:

function toInt(n) {
    return n(i => i + 1)(0);
}
Run Code Online (Sandbox Code Playgroud)

然后:

> toInt(TWO)
2
Run Code Online (Sandbox Code Playgroud)

您可以使用教堂数字来做一些实际的事情:

function shout(text) {
    return text + "!";
}

> shout("hi")
"hi!"
> NINE(shout)("hi")
"hi!!!!!!!!!"
Run Code Online (Sandbox Code Playgroud)

你可以在这里试试:https://es6console.com/iyoim5y8/