Requête sur booléens dans Lambda Calcul

Question

Ceci est la représentation du lambda-calcul pour l'opérateur:

lambda(m).lambda(n).lambda (a).lambda (b). m(n a b) b 

Quelqu'un peut-il me aider à comprendre cette représentation?

Answer 1

Pour comprendre comment représenter les booléens dans le calcul lambda, il aide à penser à une expression IF, « si alors b autre c ». C'est une expression qui choisit la première branche, b, si elle est vraie, et la seconde, c, si elle est fausse. Les expressions lambda peuvent faire très facilement:

lambda(x).lambda(y).x 

vous donnera la première de ses arguments, et

lambda(x).lambda(y).y 

vous donne la seconde. Donc, si un est l'une de ces expressions, puis

a b c 

donne soit b ou c, ce qui est exactement ce que nous voulons que le SI faire. Donc, définir

true = lambda(x).lambda(y).x 
false = lambda(x).lambda(y).y 

et a b c se comportera comme if a then b else c.

regardant à l'intérieur de votre expression à (n a b), cela signifie if n then a else b. Ensuite m (n a b) b signifie

if m then (if n then a else b) else b 

Cette expression évalue à a si les deux m et n sont true, et b autrement. Puisque a est le premier argument de votre fonction et b est le deuxième, et true a été défini comme une fonction qui donne le premier de ses deux arguments, alors si m et n sont tous les deux true, ainsi est l'expression entière. Sinon, il s'agit de false. Et c'est juste la définition de and!

Tout cela a été inventé par Alonzo Church, qui a inventé le lambda-calcul.

Answer 2

En fait, c'est un peu plus que l'opérateur AND. C'est la version du lambda-calcul de if m and n then a else b. Voici l'explication:

Dans le calcul lambda vrai est représenté en fonction prenant deux arguments * et en retournant la première. Faux est représenté comme une fonction prenant deux arguments * et retournant le second.

La fonction que vous avez montrée ci-dessus prend quatre arguments *. D'après son apparence, m et n sont censés être des booléens et a et b d'autres valeurs. Si m est vrai, il va évaluer son premier argument qui est n a b. Ceci à son tour évaluera à un si n est vrai et b si n est faux. Si m est faux, il sera évalué à son deuxième argument b.

Donc, fondamentalement, la fonction retourne un si m et n sont vraies et b autrement.

(*) Où « prendre deux arguments » signifie « prendre un argument et en retournant une fonction qui prend un autre argument ».

Modifier en réponse à votre commentaire:

and true false vu sur la page wiki fonctionne comme ceci:

La première étape consiste simplement à remplacer chaque identifiant par sa définition, à savoir (λm.λn. m n m) (λa.λb. a) (λa.λb. b). Maintenant, la fonction (λm.λn. m n m) est appliquée. Cela signifie que chaque occurrence de m dans m n m est remplacée par le premier argument ((λa.λb. a)) et chaque occurrence de n est remplacée par le second argument ((λa.λb. b)). Nous obtenons donc (λa.λb. a) (λa.λb. b) (λa.λb. a). Maintenant, nous appliquons simplement la fonction (λa.λb. a). Etant donné que le corps de cette fonction est tout simplement un, à savoir le premier argument, ce évaluée à (λa.λb. b), à savoir false (comme λx.λy. y signifie false).

Answer 3

Dans le lambda-calcul, un booléen est représenté par une fonction qui prend deux arguments, l'un pour le succès et l'autre pour l'échec. Les arguments sont appelés continuations, car ils continuent avec le reste du calcul; le booléen Vrai appelle la continuation du succès et le Faux Booléen appelle la continuation de l'échec. Ce codage est appelé l'encodage de l'Église, et l'idée est qu'un booléen ressemble beaucoup à une «fonction d'if-then-else».

On peut donc dire

true = \s.\f.s 
false = \s.\f.f 

où s représente le succès, f représente l'échec, et la barre oblique inverse est un lambda ASCII. Maintenant, j'espère que vous pouvez voir où cela se passe. Comment codons-nous and? Eh bien, en C, nous pourrions l'étendre à

n && m = n ? m : false 

Seules ces sont des fonctions, donc

(n && m) s f = (n ? m : false) s f = n ? (m s f) : (false s f) = n ? (m s f) : f 

MAIS, la construction ternaire, lorsqu'il est codé dans le calcul lambda, est fonctionner simplement l'application, nous avons donc

(n && m) s f = (n m false) s f = n (m s f) (false s f) = n (m s f) f 

donc finalement on arrive à

&& = \n . \m . \s . \f . n (m s f) f 

Et si on renomme le succès et continuations échec à a et b nous revenons à votre original

&& = \n . \m . \a . \b . n (m a b) b 

Comme avec d'autres calculs dans le calcul lambda, en particulier lors de l'utilisation encodages Eglise, il est souvent plus facile de travailler les choses avec les lois algébriques et le raisonnement équationnel, puis convertir en lambdas à la fin.