lambda微积分xor表达式通过真假

我想了解xor在lambda微积分中的上下文。我了解异或（异或）作为布尔逻辑运算https://en.wikipedia.org/wiki/Exclusive_or 和xor的真值表。lambda微积分xor表达式通过真假

但是，如何，为什么这是真的为XOR B =（A）（（B）（假）（真））（B）从http://safalra.com/lambda-calculus/boolean-logic/ 它确实是期望在演算什么。当我看到 true =λab.a false =λab.b 我不得不看到true和false作为lambda计算true和false，因为它返回true的情况下的第一个元素。但是，理解xor在这里是否也是一个名称，但与布尔逻辑中的xor不同？

来源

2017-10-17 echo

顺便说一下，我认为真正=λab.a 假=λab.b是同样的事情，真=（λa.b.）一假=（λa.b。）b后者更具教科书风格 – echo

lambda微积分逻辑与布尔逻辑中的逻辑相同。在lamba微积分中，没有值，只有符号（名称）。 TRUE不仅是函数，而且是一个描述它的名字。当评估结果为λab.a时，它是一个函数并不重要，更重要的是它是由符号TRUE描述的函数。 – rsm

另请参阅：[*教会编码*]（https://en.wikipedia.org/wiki/Church_encoding） - 所有值均为函数，偶数为零：=λf.λx.x'，one：=λf。 λx.fx'，'two：=λf.λx.f（fx）'等 – naomik

直观地说，我们可以认为A XOR B作为

如果A，那么不乙
否则，B

....或一些伪代码：

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

让我们拉姆达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

现在，如果我们想将它全部用纯朗母写的，只是它的定义更换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

在这个点，你可以看到我们有你的问题的定义

一个XOR B =（A）（（B）（假）（真））（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

来源

2017-10-17 17:54:39 naomik

相关：https://stackoverflow.com/questions/37119381/can-xor-be-expressed-using-ski-combinators - cool显示来自[SKI组合器]的XOR的回答（https://en.wikipedia.org/wiki/SKI_combinator_calculus） – naomik

lambda微积分xor表达式通过真假

回答

相关问题