使用教堂数字的公式答案

【问题标题】：Formulas that work with Church numerals使用教堂数字的公式
【发布时间】：2017-04-04 19:53:31
【问题描述】：

wikipedia entry on lambda calculus 定义了一些适用于教堂数字的公式，例如

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

在他首次定义 lambda 演算的 Churches 论文中，他说

.. 两个变量的函数公式F和X，是公式{F}(X)，是递归的..

后来在他的论文中，他将此函数称为B(m,n)。

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

我知道我们必须将输入和输出计算为素数的幂，因为他在整篇论文中都使用了哥德尔的编号系统，但是我发现很难将它们拼凑在一起。

【问题讨论】：

标签： lambda lambda-calculus church-encoding

【解决方案1】：

我在 javascript 中使用 lambda 演算。我将尝试展示一些小例子，SUCC 和函数 B aka Bluebird/Compose 是如何工作的并且可以组合使用。

首先用 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)))

以及 JS 中教会数字的继承者 SUCC := λnfx.f(nfx)： const succ = n => f => x => f( n(f)(x) )。我们可以看到succ-Function 只接受一个教会数字并在前面添加一个f，因此带有主体f(x) 的succ(n1) 将是f(f(x))。因此，它最终总共做了 1 + n 个f 的合成。

// 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-fold 组合：一个 compose 函数。 Smullyan 以 Curry 的 B 组合器将其命名为 Bluebird。

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));

【讨论】：