Lambda 演算和教会数字混淆答案

【问题标题】：Lambda calculus and church numerals confusionLambda 演算和教会数字混淆
【发布时间】：2010-11-06 06:24:36
【问题描述】：

我正在尝试了解 lambda 演算和 Church 数字的基础知识。我一直在做大量的阅读和练习，但我似乎一直在尝试了解某些功能是如何工作的。

我坚持的例子如下。也许有人可以解释我哪里出错了。

1 的教堂数字可以表示为：

λf. λx. f x

Church 数字 (mⁿ) 的幂函数可以表示为：

λm. λn. n m

我想要做的就是表明，通过将幂函数应用于 1 和 1，我得到了 1，因为 1¹ = 1。我正在这样做，所以我更好地理解了这些功能起作用。我的工作如下，每次都卡住了：

// Exp (1 1)
(λm. λn. n m) (λf1. λx1. f1 x1) (λf2. λx2. f2 x2)
// Substitute for m
(λn. n (λf1. λx1. f1 x1)) (λf2. λx2. f2 x2)
// Substitute for n
(λf2. λx2. f2 x2) (λf1. λx1. f1 x1)
// Substitute for f2
(λx2. (λf1. λx1. f1 x1) x2)
// Substitute for f1
λx2. (λx1. x2 x1)

我被卡住了。我已经失去了两个f，只剩下x，我还没有得到1。我哪里错了？

【问题讨论】：

标签： function lambda-calculus

【解决方案1】：

我哪里错了？

无处可去！你完成了。请记住，变量名并不重要；重要的是结构。名称 f 或 x2 没有意义。重要的是如何使用它们。 1 的教会数字是

λf. λx. f x

你有

λx2. (λx1. x2 x1)

将x2 重命名为f，将x1 重命名为x，瞧！你有

λf. (λx. f x)
= λf. λx. f x

【讨论】：

非常感谢。在我得到你的洞察力之前，你不知道我已经填写（并诅咒）了多少张废纸，试图让这个和类似的问题“起作用”！