logique combinatoire remixée

christophe c

Une théorie tellement riche et tellement économique, que je trouve qu'elle vaut la peine d'être un tout petit peu connue. De plus, GDN, si tu veux "décompresser" (encore que je ne sache pas si tu es "compressé") tu pourrais en faire un peu de la logique combinatoire: ça nettoie le cerveau à vitesse grand V et ya presque rien à comprendre pour y entrer.

De plus, c'est pour ça que j'y pense, c'est le seul domaine formel où tu as le droit "à volonté" en plus au définitions circulaires.

On se donne un ensemble $TOT$ muni d'une opération $.$, une relation transitive $<$, 5 objets: I;K;B;D;2 privilégiés

Attention, le "2" n'est pas le 2 courant. Mais c'est mnémotechnique de le nommer ainsi:

D est appelé le composeur
K le jeteur
B le dualeur
2 le cloneur

Par convention les parenthèse sont à gauche quand elles ne sont pas écrites et on omet l'écriture du point
exemple: $u.v$ est plutôt écrit $uv$ et $abc$ veut dire $(ab)c$

Voici les axiomes, valables pour tous éléments $a,b,c$ de $TOT$:

$Dabc>a(bc)$

$Bab>ba$

$2ab>abb$

$Kab>a$

$Ia>a$

$<$ est transitive

si $a>b$ alors $ac>bc$ et $ca>cb$

Une telle structure peut être enrichie de tout un tas de choses rigolotes. Elle sert à l'informatique en ce qu'à elle seule, elle permet de programmer.

Dans le cadre informatique, $K$ porte un autre nom: "le vrai"
Dans ce cadre informatique, $KI$ s'appelle "le faux"


Les éléments de $TOT$ peuvent être vus comme des "programmes" et $>$ comme une relation d'évolution. Les éléments $x\in T$ tels que $x>K$ ou $x>KI$ sont comparables à des phrases.
Pouruqoi? Bin, imaginez que vous fassiez un premier programme p que vous parvenez à mettre dans $TOT$ qui teste quelque chose "x" (qui après évolution va conclure K (vrai) ou KI (faux)), puis vous souhaitez que si x est ok, votre programme évolue comme "y", et sinon comme "z", et bien voilà ce qu'il suffit de faire (de regarder dans TOT):

l'élément: pxyz

En effet, si $px>K$ (autrement dit, si x répond au test du programme p) alors $pxyz>Kyz>y$
Par contre, si x ne répond pas au test, $pxyz>KIyz>Iz>z$

---

J'en arrive aux définitions circulaires, chères à GDN (décidément je suis victime du syndrome de Stockholm):

Les objets de TOT peuvent aussi être vu comme des "fonctions" particulières. Soit $f\in TOT$

but du jeu: faire un objet a tel que $a>fa$

(le $">"$ peut être vu comme une évolution dans une "égalité", en ce sens qu'on peut toujours considérer comme "vrai" objet final, le résultat à la fin de l'évolution)

Voici une astuce très simple: je voudrais juste m'arranger pour que $\forall x\in TOT: ax>f(xx)$

En effet, si j'y arrive alors, $aa>f(aa)$ et en prenant $b:=aa$, j'ai réussi $b>fb$

Remarquons que $2Ix>Ixx>xx$. (C'est là qu'on voie que le clonage...)

il me suffira donc de trouver $a$ de sorte que pour tout x: $ax>f(2Ix)$

Mais $Df(2I)x>f(2Ix)$ donc:

j'ai mon $a:=Df(2I)$ que je cherchais, vérifions:

$ax>Df(2I)x>f(2Ix)>f(xx)$ et avec $b:=aa$, on obtient $b>fb$

---

La possibilité ci-dessus montre la richesse de cette notion (informatiquement, ça donne récursivité et tests).

La cerise sur le gateau: on obtient à peu de frais la famille des théorème de Godel!

Soit $P\in TOT$ tel que $\forall x\in TOT: Px>K$ ou $Px>KI$

Je n'ai rien dit, mais sous-entendons qu'on espère de $P$ qu'il réussisse correctement la chose suivante:

pour tout $x\in TOT$: $Px>K$ si et seulement si "il est prouvé, en un sens ou un autre que "x>K"

En notant $f:=DPN$, et en faisant comme au dessus, en contruisant un b tel que $b>fb$, on obtient que $b>DPNb>P(Nb)$. Il reste alors à remplacer "N" par un objet qui exprime "non". Ainsi, on obtiendra:

que $b$ évalue vers $K$ si et seulement si il est prouvé que non(b) évolue vers $K$

Intuitivement, ce qu'on veut c'est que $Nx>x(KI)K$ pour tout $x$. Ainsi, si $x$ évolue vers "le vrai", alors $Nx$ évolue vers "le faux". En effet $Nx>x(KI)K>K(KI)K>KI$

posons $c:=KI$. On veut $Nx>xcK$ or $Bcx>xc$ donc $BK(BCx)>xcK$.

Ainsi, en prenant $N:=D(BK)(BC)$ on obtient ce qu'on veut...

Qui s'amuse à fabriquer P??? -D

deufeufeu

Pourquoi ne pas présenter cela avec juste le nécessaire ? K et S, où S a b c > a c (b c)
A ce propos connais tu le livre de Smullyan sur les combinateurs ? To mock a mocking bird. Si oui, qu'en pense-tu ? cela fait un moment que j'hésite à l'acheter.

christophe c

Pour le livre de Smullyan, non

Pour $S$ je ne l'aime pas parce qu'il contient de manière intégré la puissance du cloneur. Je trouve plus sympa d'avoir la partie "non clonable" à part (lol Girardisme?)

Par ailleurs, j'aime bien $D$ et $B$ qui sont naturels et montrent la minimum vital:

D c'est la composition (comme tu sais): $Dfgx>f(gx)$ alors que $S$ c'est pas marrant de dire aux gens ce qu'il fait

$B$ est aussi très naturel: $Bxf>fx$ et ainsi $Bx$ représente la dualité. De plus, je n'y connais pas gd chose à la LL, mais je pense que $D,B$ suffisent à la représenter, et $D,B,K,I$ suffisent à représenter la logique affine (en rajoutant un truc non combinatoire (mais inoffensif sans "2") pour représenter le "(non non A) --- > A"

christophe c

De plus, d'une certaine manière, on obtient gratuitement le produit sur les entiers: c'est tout simplement "D"

Je continue la petite histoire: "le faux" informatique (en fait, plus précisément la "place 2 après le else") peut aussi être vu comme l'entier 0.

Définitions:

dans $TOT$, on appelle $0$ l'objet $KI$

on appelle $1$ l'objet $I$

on appelle $2$ l'objet $2D$

voyons ce qu'il font: $2Dfx>Dffx>f(fx)$

$1fx>fx$

$0fx>KIfx>Ix>x$

Cette notation est mystérieuse, mais elle est bcp plus intuitive si vous exprimer $nf$ par $f^n$

Evidemment, en informatique, $n$ va avoir la même utilité que "for i:=1 to n do..."

on va donc "naturellement" appeler $3$ l'objet "successeur de 2", encore faut-il définir ce qu'on entend par "successeur".

On veut (je le note S): $Snfx>nf(fx)$ pour tous $n,f,x$ des objets quelconques de $TOT$

avec $S:=D2(DD)$

$nf(fx)<D(nf)fx<DDnffx<2(DDn)fx<D2(DD)nfx<Snfx$

Et on a un successeur tout à faite respectable...

Ainsi les entiers de $TOT$ seront les éléments du plus petit sous-ensemble de $TOT$ qui contient $0$ et stable par $S$: ie si x est dedans alors Sx aussi

Je ne parlerai pas de l'entier 2, mais seulement du cloneur 2. Sinon, je serai explicite.

La multiplication: Et bien c'est D! Pas mal non? Et tout ça ça marche exactement comme dans la géométrie arguésienne de Emil Artin... ou dans les matrices...

deufeufeu

Je trouve que l'on voit assez bien ce qu'il font si on écrit leur type, pour le Kroqueur, il prend un A et un B et il renvoie le premier A, il a Kroqué le B :
$$\lambda x y . x : A \rightarrow B \rightarrow A$$
Pour le Serpent, il prend une foncton $f(x,y)$, une fonction $g(x)$ et un x, et il calcule $f(x,g(x))$ :
$$\lambda x y z . x z (y z) : (A \rightarrow B \rightarrow C) \rightarrow (A \rightarrow \rightarrow A \rightarrow C$$
C'est assez naturel vue comme cela, le serpent permet de "replier" l'expression sur B.

christophe c

Je vous laisse faire l'addition...

christophe c

Je n'avais pas vu ton msg: oui, en un certain sens, tu as raison, sauf qu'il faut être habitué à la Cor CU HO qui n'est peut-être pas le truc de tlm ici.

Et puis, j'ai surtout envie de ne pas parler de types car ce serait pour moi un travail interminable que de dessiner les flêches avec latex... De plus c'est les def circulaires qui m'ont inspiré ce fil, donc je l'aborde dans son volet hors-type (points fixes, récursivité bien représentée à peu de frais, etc)

S pour serpent, à bin oui, fallait y penser;)

christophe c

Par ailleurs pour l'expert que tu es, la différence, en différenciant bien le cloneur du reste c'est que si on n'utilise pas "2", alors TOUS LES TERMES HABITUELS TERMINENT*. C'est quand-même intéressant...

En effet, ya un symbole qui disparait à chaque fois.. Donc tout est "normalisable" ce qui est joussif, puisque ça permet des phrases définies à partir d'elles-mêmes sans contradiction...

Par exemple, dans un "monde magique" où une phrase A serait vraiment EGALE à A-->B et bé on ne peut pas pour autant "prouver" B avec uniquement les droits logiques issus de "D,B,K,I" (C'est "2", le cloneur qui fait le boulot essentiel)

christophe c

Pour toi, les types:

$D: (A\to \to ((X\to A)\to (X\to )$

$K:..$ tu connais et tu l'as dit

$I: X\to X$

$2: (A\to (A\to X))\to (A\to X)$ (le vilain)

$B:A\to ((A\to X)\to X)$ (avec X=faux, ça donne A implique non non A)

christophe c

Maintenant, pour donner libre cours aux calculs, je décris une astuce bien connue (de Deufeufeu et des spécialistes de ça) pour fabriquer des objets intéressants:

D,B,K,I suffisent en fait à simuler le "lambda" du lambda calcul...

Mais il faut procéder occurence par occurence (ce qui est bien plus marrant, mais utile, car on voit ainsi où on clone)

Admettons que vous disposiez d'une expression et qui vous souhaitiez "abstraire" une lettre qui n'a qu'une seule occurence dans l'expression

si votre expression est de la forme u.v et que c'est u qui contient l'occurence de x, et bien vous "descendez" (donc par récurrence...) dans u, vous fabriquez une expression m sans la lettre x, dont vous pouvez prouver avec les axiomes que
mx>u. donc vous aurez prouvé aussi que mxv>uv et donc Bv(mx)>uv et donc que (D(Bv)m)x>uv

Ainsi, vous aurez récupérer une expression w sans la lettre x telle que wx>uv

Admettons que ce soit v et non pas u qui contienne l'occurence de x. De même vous fabriquez une expression h (sans x) telle que vous pouvez prouver que hx>v. donc u(hx)>uv et donc Duhx>uv et vous avez aussi une expression w sans "x" telle que vous pouvez prouver que wx>uv

Mais peut-être n'y a t il nulle part x dans uv et que vous voulez quand même une expression w telle que wx>uv. Dans ce cas, K(uv) est l'idéal

Pour initialiser: Ix>x

Avec les tests et la récursivité, on voit que l'étude de cette structure offre aussi la possibilité de faire comme en C ou en pascal, à savoir de "définir" des objets qu'on peut voir comme des procédures qu'on écrit à part.

christophe c

Reste à voir ce qui se passe quand il y a "x" dans u et dans v.

d'abord vous fabriquez m et n de sorte que mx>u et nx>v (avec m,n qui ne contiennent pas x) et ensuite:

Puis vous fabriquez $G$ de facon que pour tous $a,b,x: Gabx>axb$

avec lequel:

$(mx)(nx)<Gm(nx)x<[D(Gm)n]xx<2[D(Gm)n]x$ vous obtenez ainsi votre w tel que wx>uv avec w qui ne contient pas "x".

Fabrication de $G$:

$axb<Bb(ax)<D(Bb)ax$ (précision pour ci-dessous: ici, on gagne aussi $DDBbax>axb$, donc $DDBHHa>HaH$, pour tout H)

Want $Gab>D(Bb)a$

$D(Bb)a<DDBba<Hba$ en posant $H:=DDB$

$Hba<Ba(Hb)<D(Ba)Hb<DDBaHb<HaHb<HHHab$


Et voilà: $G:=(DDB)(DDB)(DDB)$

lol ya peut-être plus simple...

deufeufeu

je lirais tous tes posts demain matin avec mon café au boulot, là il est tard
mais juste un mot sur le livre de Smullyan, je l'avais cité car justement il me semble qu'il effectue le même genre de construction : partir de manières élémentaires des combinateurs et arriver à présenter une version *concrète* du théorème d'incomplétude de Godel.

christophe c

A propos des S et K proposés par Deufeufeu, je signale le dernier post de

http://www.les-mathematiques.net/phorum/read.php?16,358198,page=9

où justement je les utilise pour montrer qu'on peut faire toutes les maths avec le modus ponens (je me sers de S contrairement à ce fil)

---

Sinon, amusons-nous à entrer dans la "folie" des logiciens du début du 20ième (ils l'ont payé cher...)

Revoyons sous l'angle présent, certaines idées.

Définition (je crois que je l'ai déjà dit): on appelle phrase un élément de $TOT$ qui évolue soit vers $K$ soit vers $KI$ (ie qui évolue vers le vrai ou vers le faux... )

Formellement, c'est donc un élément $p\in TOT$ tel que $p\geq K$ ou $p\geq KI$

Rappel: $u>v$ peut être vu par l'intuition comme "u évolue vers v"

Dorénavant je dirais que $(TOT;K;D;B;2;I)$ s'appelle une "civilisation" et, abus de langage courant, je dirai "Soit TOT une civilation", plutôt que "soit $(TOT;K;D;B;2;I)$ une civilisation".

Définition: une civilisation $TOT$ est dite "divine" ssi: pour toute application $f:TOT\to TOT$, il existe $a\in TOT$ tel que $\forall x\in TOT$:

$ax>f(x)$

L'élément $a$ sera dit associé à $f$.

Définition: on appelle un "dieu" dans une civilisation un élément $d\in TOT$ tel que $\forall x\in TOT: d>x$

Théorème: toute civilisation divine contient un dieu.

Preuve: on utilise l'axiome du choix; à chaque $x\in TOT$ on associe $f(x)\in TOT$ telle que non$x>f(x)$. Soit a un élément associé à $f$ et soit b tel que $b>ab$ (voir posts précédent pour l'existence de b). Alors $b>ab>f(b)$ contradiction.

Remarque: dans les civilisations divines, les dieux évoluent donc vers tout le monde...

Définition: une phrase $p$ est dite vivante quand $p\geq K$ et $p\geq KI$.

Définition: une civilisation est dite fataliste quand il existe $v\in TOT$ tel que pour tout $x\in TOT$ si $x$ n'est pas $\geq K$ alors $vx>KI$ et sinon $vx>K$

Théorème: dans toute civilisation fataliste, il existe une phrase vivante.

Soit effet, $a$ tel que pour tout $x$: $ax>v(x(KI)K)$ et soit $p$ tel que $p>ap$. Montrons que $p$ est une phrase:

$p>$ à un truc de la forme $vq$ qui évolue forcément vers $K$ ou vers $KI$. Ainsi $p$ évolue vers $K$ ou vers $KI$. Si $v(p(KI)K)>K$ alors $p>K$ et donc $v(...)>v(K(KI)K)>v(KI)>KI$ (sauf si $KI>K$, auquel cas CQFD, car la phrase (KI serait vivante)) et donc $p$ est vivante.

Si $v(...)>KI$ alors $p>KI$, et donc $v(...)>v(KI(KI)K)>K$ donc $p>K$