lambda - 以下是 lambda 演算的合法后继函数吗？（教会数字）

Question

我从书中读到，Church Numerals 的后继形式为： (\lambda nf x. f (nfx) )

昨晚我想出了这个： (\lambda ab c. (ab) (bc) )

我相信它也执行后继功能的功能。但是，我不是 100% 肯定我的减少是正确的。有人可以检查它并告诉我吗？

以下是我的简化：设一个教堂数字为 (\lambda f x. f^nx)，其中 f^nx 实际上是 (f(f(f(f...(x)))..它代表数字n，期望的结果应该是n+1，即(\lambda f x. f^{n+1} x)

(\lambda ab c. (ab) (bc) )(\lambda f x. f^nx)

= (\lambda b c. ( (\lambda f x. f^nx) b) (bc) ) // a 替换

= (\lambda b c. ( (\lambda x. b^nx) (bc) ) // f 替换

= (\lambda b c. ( (\lambda x. b^nx) (bc) ) // 不是 100% 确定，我可以用 (bc) 替换 x 吗？

= (\lambda b c. ( b^n (bc) )

= (\lambda b c. ( b^(n+1) c )

这种减少是否正确，尤其是从第 3 步到第 4 步？谢谢！

score 1 · Accepted Answer

是的，这是正确的。代替没有b c问题x。请参阅替换规则。虽然b和c受约束，但它们在所讨论的两个术语之上都有约束，因此它们在两个地方具有相同的含义。

score 0 · Accepted Answer

理解后继函数的两个定义的一种方法是从总和开始：

plus = \n,m,x,y. n x (m x y)

那么我们可以定义

succ1 = \n. plus one n 
succ2 = \n. plus n one

在哪里one = \x,y.x y

简化这两项，我们得到

succ1 = \n,x,y. one x (n x y) 
      = \n,x,y. x (n x y)
succ2 = \n,x,y. n x (one x y) 
      = \n,x,y. n x (x y)

2 回答 2