我如何在λ演算中证明XOR true true = false？

问题描述

我知道XOR =（a）（（b）（false）（true））（b） 但是如何减少[xor true true]并从该表达式中得到错误的结果？

解决方法

您忘记了XOR定义前面的λ。另外，您还必须将true和false定义为标准Church布尔值：

true = λab.a
false = λab.b
XOR = λab.a(b false true)b

然后

    XOR true true
--> (λab.a(b false true)b) true true
--> true (true false true) true
--> true false true
--> false