使用教会数字的公式

Question

关于lambda微积分的wikipedia条目定义了一些与教会数字一起工作的公式，如

SUCC := λn.λf.λx.f (n f x)

在教会的论文中，他首先定义了他的λ微积分，他说

两个变量的..a函数，其值取格式良好的公式F和X，是formaula {F}(X)，是递归的.

在后面的文章中，他称这个函数为B(m,n)。

如何使用所有这些信息来描述像B这样的函数如何在SUCC 1上工作

我知道，我们必须把输入和输出作为素数的力量，就像他在整个论文中使用Gódel的编号系统一样，但是我发现很难把它们拼凑在一起。

Answer 1

我使用lambda微积分和javascript。我将尝试展示一些小的例子，SUCC和函数B，也就是蓝知更鸟/构图是如何工作的，如何组合。

首先用Church-Numerals (在JS中)提醒一下：

const n0 = f => x => x       
const n1 = f => x => f(x) 
const n2 = f => x => f(f(x))     
const n3 = f => x => f(f(f(x)))

和继承SUCC := λnfx.f(nfx)的教会-数字在JS：const succ = n => f => x => f( n(f)(x) )。我们可以看到，succ-Function只是在前面使用了一个教堂数字，并添加了一个f，这样带有body f(x)的succ(n1)就会是f(f(x))。因此，它最终完成了f的1+n组合。

// example creating new Church-Numbers with the Succesor-Function
const n4 = succ(n3)
const n5 = succ(n4)

// or do Addition with Church-Numbers
const n7  = n2(succ)(n5)
const n10 = n5(succ)(n5)

//to test if it works, us the helper-function churchtoJsNum
const churchtoJsNum = n => n(x => x + 1)(0)

churchtoJsNum(n10) // 10

还有另一种编写后继的方法，因为我们正在做n重组合:编写函数。Smullyan以咖喱的B组合器命名蓝鸟。

B := λfgx.f(gx)

在JS：const B = f => g => x => f(g(x))

现在可以将succ和B-Function结合起来。

const succ = n => f => x => B(f) (n(f)) (x)  

既然我们有了一个实际的组合函数，我们就可以定义后继函数，而无需提及最后的x值参数。

const succ = n => f => B(f)(n(f));