lambda-calculus - 在 lambda 演算中，当输入是恒等函数时，我将如何编写一个返回 true 的函数？

Question

在 lambda 演算中，当输入是恒等函数时，我将如何编写一个返回 true 的函数？

假设 true 是一些教堂编码的 true 值。

看起来这应该是一个容易编写的函数。但是对于我想到的每一个测试，一个棘手的输入都可以胜过它。这是不可能的吗？

Answer 1

I := λx.x
0 := λf.λx.x
1 := λf.λx.f x
TRUE := λx.λy.x
FALSE := λx.λy.y
PRED := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
ISZERO := λn.n (λx.FALSE) TRUE

恒等函数λx.x是 Eta 等价于教堂数字 1 λf.λx.f x。下面的 Fn 将返回任何在通过谓词函数后FALSE计算结果不为教堂数字零 ( ) 的函数。λf.λx.x

λx.(ISZERO (PRED x)) TRUE FALSE

可能存在一个行为如下的函数 BAD：

λx.(ISZERO (PRED x)) TRUE FALSE BAD := TRUE
BAD != I