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表達式通過真假

回答

相關問題