lambda-calculus - 无法推导出 lambda 表达式 λx.λy.x(xy) 的数字表示(教会编码)

Question

我有一个 lambda 表达式:λx.λy.x(xy)，我应该推断它的整数表示。我已经阅读了很多关于教会编码和教会数字的内容，但我找不到数字是什么。你能用 3 岁的 child 能理解的方式向我解释一下吗？或者可以向我推荐比维基百科更好的资源吗？

Answer 1

整数的教会编码如下:

• "0"≡ (λf.(λx.x)):将 (λf.(λx.x)) 视为含义:给定一个函数 f 和一个元素 x，结果是 x:这就像将函数 f 零次应用到 x 。
• "1"≡ (λf.(λx.(fx))):将 (λf.(λx.(fx))) 视为含义:给定一个函数 f 和一个元素 x，结果是 (fx):应该被认为是 apply f 到 x 或更标准的数学符号，如 f(x)。
• "2"≡ (λf.(λx.(f(fx)))):想想 (λf.(λx.(f(fx)))) 的含义:给定一个函数f和一个元素x，结果是(f(fx)):应该这样想将 f 应用于 x 两次 或者，在更标准的数学符号中，如 f(f(x)) .
• "3"≡ (λf.(λx.(f(f(fx))))):想想 (λf.(λx.(f(f(fx) )))) 的含义:给定一个函数 f 和一个元素 x，结果是 (f(f(fx))):应该被认为是将 f 应用于 x 三次，或者用更标准的数学符号，如 f (f(f(x)))。

我希望您能看到这种模式(以及背后的逻辑)。在您的情况下， (λx.(λy.(x(xy)))) 是数字 2 的 Church 编码(当然使用 alpha-equivalence)。

wikiped article其实很清楚。你有什么不明白的？