演算和教会的数字混乱

Question

我想了解演算和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回。我在哪里去了？

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