Pour Church, la fonctionnelle qui, à deux fonctions a et b, associe la première des deux, est vraie. La fonctionnelle qui, à deux fonctions a et b, associe la seconde, est fausse. On les note respectivement
L'affichage montre la fonction vrai, compilée en JavaScript. En effet, il s'agit bien d'une fonction...
On a donc besoin d'un affichage plus performant. Pas besoin de Churcher trop loin, l'image du couple ("vrai","faux") par chacune des
fonctions donne le résultat affiché. On construit une fonction affichage (qui n'est donc pas une λ-fonction puisqu'elle porte un
nom) et il suffit de l'invoquer pour afficher un booléen de Church:
La curryfication consiste à écrire une fonctionnelle portant sur deux fonctions, en une fonctionnelle de fonctionnelle:
Du coup les notations deviennent, dans l'ordre
La seule fonction booléenne portant sur une seule variable (à part l'identité) est la négation, définie pour une proposition p
par λpab.p b a ou λp.λab.p b a ou λp.λa.λb.p b a. C'est la deuxième version qu'on va adopter ici:
En fait puisqu'une proposition est une fonction des deux variables "vrai" et "faux", sa négation est une fonction des deux mêmes variables
mais en inversant leurs positions. Géométriquement, la fonction "vrai" est l'abscisse (première coordonnée d'un point du plan) et la
fonction "faux" est l'ordonnée (seconde coordonnée). La négation ayant pour effet d'échanger l'abscisse et l'ordonnée, est la symétrie
axiale par rapport à la droite d'équation y=x. Et le tiers exclu correspond au fait que le plan est
de dimension 2.
Un booléen étant construit comme une fonction qui choisit entre deux élements, la variante de la négation consistant à ne pas inverser
les deux entrées du booléen fait un test. C'est donc la base de la construction d'algorithmes en λ-calcul. Alors que la négation était
λp.λa.λb.p b a, le test est λp.λa.λb.p a b. Mais ce n'est pas une opération sur les propositions, on va donc le
décurryfier en λpab.p a b plutôt qu'en λp.λab.p a b:
On peut donc choisir entre les deux fonctions cos et sin selon la valeur de vérité de la proposition. Comme dans
le λ-calcul, tout est fonction, on peut choisir entre deux fonctions quelconques, et donc, entre deux objets quelconques du λ-calcul.
La conjonction, comme toute opération logique (binaire), est une fonctionnelle portant sur deux booléens a et b. On constate que
λab.b a b qu'on peut curryfier en λa.λb.b a b. Mais ici on utilise la version curryfiée:
Pour la disjonction, ce sont les tautologies qui sont absorbantes (a∨b est vrai dès que b est vrai) et les antilogies qui sont neutres (a∨b a la même valeur de vérité que a si b est vrai). Donc
λab.b b a:
La curryfication de cette disjonction donne λa.λb.b a b.
Remarque: Une opération logique étant définie par trois choix de a ou b comme ci-dessus, il y a 23=8 opérations possibles:
| λ-expression | Opération |
|---|---|
λab.a a a | premier terme (a) |
λab.a a b | Ou inclusif |
λab.a b a | Et |
λab.a b b | Second terme (b) |
λab.b a a | Premier terme |
λab.b a b | Et |
λab.b b a | Ou inclusif |
λab.b b b | Second terme |
On constate que cela ne permet pas de définir l'opérateur de Sheffer ni l'implication ni même le "ou exclusif". Mais en rajoutant une négation, on peut définir ce dernier:
Cette expression s'écrit, sans curryfication, λab. a leContraireDe(b) b ou λab. a (b (λc.λd d c) (λc.λd c d)) b
Avec la comparaison géométrique ci-dessus, la logique ternaire de
Łukasiewicz
revient à rajouter une troisième dimension, et la symétrie représentant la négation se fait maintenant par rapport au plan d'équation
x=z: