Jouissance combinatoriale pour foys

J'essaie d'attirer foys vers le présent fil car il a parfois envie de parler de combinateurs, qui, il faut bien le reconnaitre, sont l'avenir de la science, mais ont eu un destin d'enfant non désiré et se sont fait massacrer par la recherche scientifique.

Depuis une trentaine d'années, ils reprennent de la vigueur, mais dans des cadres étriqués de typages qui les brident et découragent leurs utilisateurs.

Je fais rapidement une introduction au sujet (et désolé, je n'ai pas le temps, je vais utiliser MES lettres et pas celles qu'on trouve dans la littérature que je ne connais pas, qui est souvent "usine à gaz", à l'exception de $S,K,W$ (et surtout $K,W$))

1/ Soit $Z$ un ensemble doté d'un loi qu'on notera multiplicativement avec la convention que $abc$ veut dire $(ab)c$.

2/ Comme on est dans un fil ludique et que de toute façon on ne peut faire des bonnes maths que dans des théories contradictoires, je vais utiliser le signe $=$ dans un premier temps (il sera toujours temps de "pontifier" le sujet si besoin, ce sont les participants qui décideront)

3/ Il y a dans $Z$ 4 éléments désopilants. Je les ai choisis tels à cause de théorèmes de logique que j'ai prouvé qui trivialisent (j'utilise parfois un point virgule en lieu et place de "et" dans le latex) la notion de preuve. Les autres jeux (que je signalerai) n'ont pas l'efficacité des 4 que je présente.

4.1/ tout d'abord les célèbres $W,K,J$ qui sont tels que:

$$\forall u,v: (Wuv=uvv ; Kuv=u; Jx=x)$$

4.2/ Et mes deux stars, dont une est connue:

$$ \forall x,y,z: Dxyz = x(yz); Hxyz = yzx$$

5/ Pour info, je signale d'autres jeux complets de combinateurs:

5.1/ Le jeu $\{C;W;K\}$ avec $\forall a,b,c: Cabc=b(ac)$

5.2/ Le jeu $\{S;K\}$ avec $\forall a,b,c: Sabc = (ac)(bc)$, mais je n'aime pas du tout $S$, qui embouteille maladroitement $W, D,C,H,B$ qui sont de nature différente (profondément)

5.3/ Le jeu $\{D;B;K;W\}$ avec $\forall x,y: Bxy=yx$

5.4/ Le jeu $\{C;K;B_0;K;W\}$ avec $\forall x: B_0x = xJ$

5.5/ $\{M;G; K;W\}$ avec $\forall x,y,z: Mxyz=x(zy)$ et $Gxyz = xzy$

6/ Intérêt de ces groupes.

6.1/ Ils sont tous complets. Complet, ça veut dire que pour tout mot $m$ contenant une ou plusieurs fois la lettre $x$, vous pouvez grâce à eux, trouver (facilement) un mot $n$ ne contenant pas la lettre $x$, et appliquer les règles de calculs pour prouver (facilement) que $nx=m$

6.2/ Pourquoi je n'aime pas le groupe (pourtant historique) $\{S;K\}$? Parce qu'il ne permet pas de distinguer des opérations de la vie profondément différentes, que je vais décrire maintenant:

7.1/ Les combinateurs $M;C;D;H;G.B;B_0$ sont le développement durables et de nombreuses parties de leur ensemble sont complètes pour le DD. En effet, ils se contentent de déplacer ordre et parenthèses, mais ne jette rien ni ne duplique rien. C'est important quantiquement puisque les ressources quantiques ne peuvent pas être dupliquées sous peine de contradiction formelle et violente avec la relativité.

7.2/ Le combinateur $K$, très stable, offre directement un "jetage à la poubelle" d'une ressource. Mais il ne permet pas de dupliquer.

7.3/ Le dupliqueur est $W$. C'est lui qui offre sa puissance et son indécidabilité à la science (et sa contradiction).

8/ Pour simplifier, je suppose connue ou plutôt donnée la notion de phrase et un mot que je nomme "garantir". En outre, je suppose que pour toutes phrases $A,B$ et tout élément $u$ de $Z$:

$u$ garantir $A\to B$ ssi $(\forall v\in Z: v$ garantit $A$ implique $uv$ garantit $B)$.

C'est une version simplifiée mais peu importe (c'est la définition du forcing qui a permis à Cohen en 1963 de prouver l'indépendance de HC et de recevoir la médaille Field)


9/ Voici ce que garantissent nos célébrités ci-dessus (je vous laisse l'établir en exercice), et ce pour toutes phrases:

$M$ garantit $(B\to C)\to (A\to ((A\to \to C))$

$C$ garantit $(A\to \to ((B\to C)\to (A\to C))$

$D$ garantit $(B\to C)\to ((A\to \to (A\to C))$

$B$ garantit $A\to ((A\to \to $

$J$ garantit $A\to A$

$W$ garantit $(A\to (A\to )\to (A\to $

$K$ garantit $A\to (B\to A)$

$B_0$ garantit $((A\to A)\to \to B$

$S$ garantit $(A\to (B\to C))\to ((A\to \to (A\to C))$

$G$ garantit $(A\to (B\to C))\to (B\to (A\to C))$

Je vous laisse en exercice écrire la garantie offerte par $H$ (j'ai mal à la main)

10/ Dès lors qu'un jeu est complet, vous disposez d'une logique de fond correspondante. Cela est dû au fait qu'un jeu complet permet de se passer de l'usine à gaz des séquents et des déchargement d'hypothèses, tout se fait à coup de LA SEULE règle du modus ponens.

11/ En effet, le point "action" (6.1) correspond au point "déduction" suivant:

Dès lors qu'on prend comme axiomes les phrases garanties par un jeu complet, on obtient que l'ensemble des théorèmes prouvés avec juste le modus ponens a la qualité suivante: "si en faisant des hypothèses $X$ auxquelles j'ajoute $A$, je peux prouver $B$ alors je peux prouver $(A\to $ à partir des seules hypothèses de $X$.

11.1/ La logique engendrée par les combinateurs du développement durable s'appelle "logique linéaire"

11.2/ La logique engendrée par les combinateurs du développement durable auxquels on ajoute $K$ s'appelle "logique affine"

11.3/ La logique engendrée par tous les combinateurs s'appelle "logique intuitionniste".

11.4/ En outre tout jeu complet est pour la linéaire (en termes d'actions les DevDur) est suffisant, il suffit d'ajoute rà la demande $K, W$ ou les deux selon ce qu'on veut mais "le coeur" du raisonnement reste intact.

12/ Mon système préféré (que je n'utilise pourtant presque jamais) est évidemment $\{D;H\}$. En voici les raisons:

12.1/ Il est Dev.Dur complet**

12.2/ il a un avantage vraiment impressionnant (qu'a aussi le jeu $\{C;D;B\}$):



Par superstition j'arrête là.

Enfin non,

13/ Le thème s'appelle "logique combinatoire". Les mots fabriqués s'appellent "termes du lambda calcul"

14/ ** pour tout mont $m$ contenant n fois la lettre $x$, il existe un mot $t$ tel que les règles de calcul permettent de prouver $m = txxxx\dots x$ où la lettre $x$ apparait $n$ fois, mais n'apparait dans $t$.

15/ Les contradictions célèbres s'expriment en termes: par exemple le théorème de Cantor est le terme $(WJ)(WJ)$. Le terme $B$ est le célèbre plongement Espace vers Bidual.

16/ $W(Cu(Cv)) =Suv$

17/ $[x\mapsto (uv)] := S(x\mapsto u)(x\mapsto v)$, c'est cette propriété célèbrissime qui a fait décoller l'importance de ce paradigme, puisque $[x\mapsto blabla]$ (qui est l'unique et puissant outil des maths) se retrouve programmé "bêtement" en algèbre.