lambda calculus xor expression par vrai faux

Question

J'essaie de comprendre xor en contexte de lambda-calcul. Je comprends xor (Exclusive ou) comme opération logique booléenne dans https://en.wikipedia.org/wiki/Exclusive_or et la table de vérité de xor.

Mais comment pourquoi est-il vrai comme XOR b = (a) ((b) (false) (true)) (b) de http://safalra.com/lambda-calculus/boolean-logic/ il est en effet ce que vous attendez dans le calcul lambda. Quand j'ai vu true = λab.a false = λab.b J'ai un peu besoin de voir le vrai et le faux comme un lambda calc vrai et faux car il retourne le premier élément en cas de vrai. Mais est-ce correct de comprendre que le xor ici est aussi un nom mais pas le même que xor dans la logique booléenne?

Answer 1

Intuitivement, on peut penser à un XOR B comme

1. si A, B pas
2. autrement, B

.... ou dans un pseudo-code:

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

---

Obtenons lambda calculusing

true := λa.λb.a 
false := λa.λb.b 

true a b 
// a 

false a b 
// b 

prochaine, nous ferons not

not := λp.p false true 

not true a b 
// b 

not false a b 
// a 

nous pouvons faire if suivant (note, que ce genre de bête depuis true et false se comportent déjà comme if)

if := λp.λa.λb.p a b 

if true a b 
// a 

if false a b 
// b 

Ok, écrivez enfin 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 

Rappelez-vous if est un peu idiot ici, nous pouvons juste enlever

xor := λa.λb.a (not b) b 

Maintenant, si nous voulons écrire tout cela avec lambda pur, il suffit de remplacer la not avec sa définition

Au ce point, vous pouvez voir que nous avons la définition de votre question

a XOR b = (a) ((b) (false) (true)) (b)

Mais bien sûr, qui a introduit des variables libres supplémentaires false et true - vous pouvez remplacer ceux Deux ou trois réductions supplémentaires de bêta

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