我试图在 lambda 演算的上下文中理解 xor。我将 xor（异或）理解为https://en.wikipedia.org/wiki/Exclusive_or中的布尔逻辑运算 和异或的真值表。
但是为什么它是来自http://safalra.com/lambda-calculus/boolean-logic/的 xor b=(a)((b)(false)(true))(b) 是真的期望在 lambda 演算中。当我看到 true=λab.a false=λab.b 时，我不得不将 true 和 false 视为 lambda calc true 和 false，因为它在 true 的情况下返回第一个元素。但是理解这里的异或也是一个名字但与布尔逻辑中的异或不同是否正确？
直观地，我们可以将 A XOR B 视为
....或在一些伪代码中：
func xor (a,b)
if a then
return not b
else
return b
让我们进行 lambda 计算
true := λa.λb.a
false := λa.λb.b
true a b
// a
false a b
// b
接下来我们会做not
not := λp.p false true
not true a b
// b
not false a b
// a
我们可以做if下一步（注意，这有点愚蠢，因为true并且false已经表现得像if）
if := λp.λa.λb.p a b
if true a b
// a
if false a b
// b
好的，最后写xor
xor := λa.λb.if a (not b) b
(xor true true) a b
// b
(xor true false) a b
// a
(xor false true) a b
// a
(xor false false) a b
// b
记住if这里有点笨，我们可以删除它
xor := λa.λb.a (not b) b
现在，如果我们想用纯 lambda 编写它，只需将其替换为not它的定义
xor := λa.λb.a (not b) b
->β [ not := λp.p false true ]
xor := λa.λb.a ((λp.p false true) b) b
->β [ p := b ]
xor := λa.λb.a (b false true) b
此时，您可以看到我们从您的问题中得到了定义
a xor b = (a)((b)(false)(true))(b)
但当然，这引入了额外的自由变量false，并且true您可以用一些额外的 beta 减少来替换这些变量
xor := λa.λb.a (b false true) b
->β [ false := (λa.λb.b) ]
xor := λa.λb.a (b (λa.λb.b) true) b
->β [ true := (λa.λb.a) ]
// pure lambda definition
xor := λa.λb.a (b (λa.λb.b) (λa.λb.a)) b
考虑 a(b FT)b，中间的表达式本质上是 (not b)，所以 a(not b)b 只有当 a 和 b 不同时才为真。