题
我想了解演算和Church数的基础知识。我一直在做大量的阅读和练习,但我似乎保持卡住,试图看到一些功能是如何工作的。
我停留上的例子如下。也许有人可以解释,我也出了问题。
1教会标号可以表示为:
λf. λx. f x
在Church数的幂函数(M 名词)可以被给定为:
λm. λn. n m
所有我想要做的是表明,通过应用幂函数1和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回。我在哪里去了?
解决方案
我在哪里去了?
无处!你完成了。请记住,变量名称并不重要;它是非常重要的结构。名称f
或x2
是没有意义的。唯一要紧如何使用它们。教会标号1是
λf. λx. f x
和你有
λx2. (λx1. x2 x1)
重命名x2
到f
和x1
到x
和瞧!您有
λf. (λx. f x)
= λf. λx. f x
不隶属于 StackOverflow