Sur requête booléens en calcul Lambda

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, s'il est vrai, et le second, 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. définir Alors

 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.

Recherche dans votre expression à (n a b), cela signifie if n then a else b. Ensuite moyens m (n a b) b

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. Depuis a est le premier argument de votre fonction et b est le deuxième, et true a été définie comme une fonction qui donne la première de ses deux arguments, alors si m et n sont à la fois true, est donc l'expression entière. Dans le cas contraire, il est false. Et c'est juste la définition de and!

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

Answer 2

Dans le calcul de lambda, un opérateur booléen est représentée par une fonction qui prend deux arguments, l'un pour le succès et un échec. Les arguments sont appelés continuations , parce qu'ils continuent avec le reste du calcul; le booléen vrai appelle la poursuite du succès et les faux appels booléennes La continuation de l'échec. Ce codage est appelé codage Eglise, et l'idée est qu'une booléenne est très semblable à une « fonction if-then-else ».

On peut donc dire

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

où s signifie succès, f signifie l'échec, et la barre oblique inverse est un lambda ASCII.

Maintenant, je l'espère, vous pouvez voir où cela va. Comment le code-nous and? Eh bien, en C, nous pourrions l'étendre à

n && m = n ? m : false

Seules ces fonctions sont, donc

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

, la construction ternaire, lorsqu'il est codé dans le calcul lambda, est juste application de la fonction, nous avons donc

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

Enfin, nous arrivons à

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

Et si on renomme le succès et l'échec de continuations 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 de l'Église, il est souvent plus facile de travailler les choses avec les lois algébriques et raisonnement équationnel, puis convertir en lambdas à la fin.

Answer 3

En fait, il est un peu plus que l'opérateur. Il 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é en fonction prenant deux arguments * et en retournant la seconde.

La fonction prend montriez quatre arguments ci-dessus *. Des regards de ce m et n sont censés être booléens et a et b d'autres valeurs. Si m est vrai, il évaluera à son premier argument qui est n a b. Cela évaluera à un si n est vrai et b si n est faux. Si m est faux, il évaluera à 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 comme on le voit sur la page wiki fonctionne comme ceci:

La première étape consiste simplement à remplacer chaque identifiant à sa définition, à savoir (λm.λn. m n m) (λa.λb. a) (λa.λb. b). Maintenant, est appliquée la fonction (λm.λn. m n m). Cela signifie que chaque occurrence de m dans m n m est remplacé par le premier argument ((λa.λb. a)) et chaque occurrence de n est remplacé 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).