lambda calculus xor表达式为true false

Question

我试图在lambda演算的上下文中理解xor.我理解xor(Exclusive或)作为https://en.wikipedia.org/wiki/Exclusive_or中的布尔逻辑运算 和xor的真值表.

但是为什么它作为一个xor b =(a)((b)(false)(true))(b)来自http://safalra.com/lambda-calculus/boolean-logic/ 它究竟是什么呢期待lambda演算.当我看到true =λab.afalse =λab.b时,我必须看到真和假为lambda calc true和false,因为它返回第一个元素,如果是真的话.但是理解这里的xor也是一个名称但与布尔逻辑中的xor不同是否正确？

Answer 1

直觉上,我们可以将A XOR B视为

1. 如果A,那么不是 B.
2. 否则,B

....或某些伪代码:

func xor (a,b)
  if a then
    return not b
  else
    return b

让我们得到lambda calculusing

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-你可以取代那些有一对夫妇的额外削减公测

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