lambda - 适用于教会数字的公式

Question

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

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

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

..a function of two variables whose value, when taken of the well-formed formulas F and X, is the formaula {F}(X), is recursive..

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

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

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

Answer 1

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

首先用教会数字(在 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 只是接受一个 Church-Numeral 并在前面添加一个 f，这样一个 succ(n1)主体 f(x) 将是 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 次组合: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));