function - Lambda 演算和教会数字混淆

Question

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

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

1 的 Church 数可以表示为:

λf. λx. f x

教会数字 (mn) 的幂函数可以表示为:

λm. λn. n m

我想要做的就是表明，通过将幂函数应用于 1 和 1，我得到 1，因为 11 = 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

Where am I going wrong?

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

λf. λx. f x

你有

λx2. (λx1. x2 x1)

重命名 x2至 f和 x1至 x瞧!你有

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