Lambda演算和教堂数字混乱

Question

我正在努力理解lambda演算和教会数字的基础知识.我一直在做很多阅读和练习,但我似乎一直在试图看看一些功能是如何工作的.

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

1号教堂的数字可以表示为:

?f. ?x. f x

教会数字(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,我没有回来.我哪里错了？

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