演算和教会的数字混乱(Lambda calculus and church numerals con

我想了解演算和Church数的基础知识。 我一直在做大量的阅读和练习，但我似乎保持卡住，试图看到一些功能是如何工作的。

我被困在示例如下。 也许有人可以解释，我也出了问题。

1教会标号可以表示为：

λf. λx. f x

上Church数^（m×n个 ）的幂函数可给出如下：

λ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回。 我要去哪里错了？

Answer 1:

我要去哪里错了？

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

λf. λx. f x

你有

λx2. (λx1. x2 x1)

重命名x2到f和x1到x和瞧！ 你有

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

文章来源: Lambda calculus and church numerals confusion