Variables d'après la logique combinatoire

$\newcommand{\s}{\mathbf S}
\newcommand{\k}{\mathbf K}
\newcommand{\o}[2]{\square #1 #2}
\newcommand{\i}{\o{\o {\s}{\k}}{\k}}
\newcommand{\r}[2]{#1 \rhd #2}
\newcommand{\l}[2]{\lambda #1 #2}
\newcommand{\sub}[3]{\left [#2 / #1 \right ] #3}
\newcommand{\subv}[3]{\left [\vec{#2} / \vec{#1} \right ] #3}
\newcommand{\b}{\o {\o {\s}{\o {\k}{\s}}}{\k}}
\newcommand{\a}[2]{\langle #1 \rangle \to #2}
\newcommand{\jt}[3]{#1 \vdash #2 : #3}
$L'emploi des lettres en mathématiques pose beaucoup de problèmes à beaucoup de monde. Le statut de la lettre $x$ dans "la fonction affine $t\mapsto xt+y$"et dans $\forall x\in \R, x^2\geq 0$ n'est pas le même. Comment exprimer clairement les rôles respectifs des lettres dans ces deux situations. Qu'est-ce, au fond, qu'une variable?
Le mathématicien russe Moses Schönfinkel a inventé dans les années 1920 la logique combinatoire pour répondre
précisément à cette question. Ce formalisme a été repris ensuite par Haskell Curry parallèlement au développement du lambda calcul par Alonzo Church. Puis il est tombé dans une sorte d'oubli (les traités de lambda calcul lui consacrent rarement plus de quelques pages à ma connaissance; hors des milieux spécialisés il y a de grandes chances que personne n'en ait entendu parler) et -ce n'est que mon avis- il n'a pas eu la postérité qu'il aurait dû avoir.

Bien sûr d'autres solutions sont disponibles pour parler intelligemment et précisément des variables: description explicite de l'apha-équivalence (les manuels de logique le font); indices de De Bruijn; méthode graphique (notations de Quine, reprises par Bourbaki: les variables liées sont un symbole dédié relié par un trait à un symbole lieur).
Mais seule la logique combinatoire permet de répondre de la bonne manière aux pires poncifs sur les variables (liées) en les remettant à leur vraie place: celle de pur sucre syntaxique au service d'une écriture plus compacte des formules.
De plus ce formalisme est tellement simple qu'il peut être maîtrisé en quelques heures.
Un très bon livre introductif sur ce sujet est le "Lambda-Calculus and Combinators: An Introduction" de R.Hindley et J.Seldin (il contient tous les développements techniques du présent fil).

I) Définition des combinateurs et de la relation de réduction.
On fixe deux constantes $\s,\k$ dans tout ce qui suit. On appelle combinateur (ils sont en notation polonaise ci-dessous):
-une des deux constantes $\s,\k$
-une lettre ou un symbole mathématique autre que $\s,\k$.
-$\o P Q$ où $P,Q$ sont des combinateurs (edit: ajout du tiret!).
On définit "$\r {\:}{\:}$" comme la plus petite relation binaire réflexive et transitive entre combinateurs telle que pour tous combinateurs $A,B,C$ et $D$:
1°) $\r{\o {\o {\k} A} B} A$
2°) $\r{\o {\o {\o{\s} A} B} C}{\o {\o A C}{\o B C}}$
3°) si $\r A B$ et $\r C D$ alors $\r{\o A C}{\o B D}$.

Par exemple, pour tout combinateur $E$, on a $\r{\o{\i} E} E$.
En effet, $\r{\r{\o{\i}{E}}{\o{\o{\k}{E}}{\o{\k}{E}}}}{E}$ via les axiomes ci-dessus.

II) Substitution d'une lettre par un terme.
Soit $\mathbf v$ une lettre et $T,P$ deux combinateurs. On désigne par $\sub {\mathbf v} T P$ le combinateur obtenu en remplaçant, dans $P$, toutes les occurrences de $\mathbf v$ par $T$ (édité).
Exemples:
1°) $\sub x {\o {\k} {\s}} {\o {\o {\s} x} x}$ est le combinateur $\o {\o {\s} {\o {\k} {\s}}} {\o {\k} {\s}}$
2°) $\sub y {\o x y} {\o y {\o y {\k}}}$ est le combinateur $\o {\o x y} {\o {\o x y} {\k}}$

NB:
3°) étant donné une lettre quelconque $\mathbf w$ et un combinateur $Q$, $\sub {\mathbf w} {\mathbf w} Q$ est bien évidemment $Q$ lui-même (en remplaçant $\mathbf w$ par $\mathbf w$ on ne change rien!).
4°) Etant donnés trois combinateurs $A,B,C$ et une lettre $\mathbf u$, si $\r A B$, alors $\r {\sub {\mathbf u} C A}
{\sub {\mathbf u} C B}$ Cela se voit par induction évidente sur la longueur de la suite de réductions élémentaires (étapes décrites au I) de ce paragraphe) appliquées pour obtenir $\r A B$: quand vous remplacez un terme $X$ par $\sub{\mathbf u} C X$ dans chacun des cas 1°, 2° ou 3° de I) vous obtenez une étape de réduction de même forme.
Par exemple: on prend les lettres $x,y,z$. On a $\r {\o {\o {\o {\b}x}y}z} {\o x {\o y z}}$: le détail est donné par
$$\r{\o {\o {\o {\b}x}y}z}{\r {\o {\o {\o {\o {\o {\k}{\s}}x}{\o {\k} x}}y}z} {\r {\o {\o {\o {\s} {\o {\k} x}} y}z} {\r {\o {\o {\o {\k} x} z}{\o y z}}{\o x {\o y z}}}}} \tag{$\dagger$}$$ Alors on a également $\r {\o {\o {\o {\b}{\o {\s}{\k}}}y}z} {\o {\o{\s}{\k}} {\o y z}}$ en appliquant $\sub x {\o {\s}{\k}} {\:}$ à chaque terme; la suite de réductions correspondante étant $$
\r{\o {\o {\o {\b}{\o {\s}{\k}}}y}z}{\r {\o {\o {\o {\o {\o {\k}{\s}}{\o {\s}{\k}}}{\o {\k} {\o {\s}{\k}}}}y}z} {\r {\o {\o {\o {\s} {\o {\k} {\o {\s}{\k}}}} y}z} {\r {\o {\o {\o {\k} {\o {\s}{\k}}} z}{\o y z}}{\o {\o {\s}{\k}} {\o y z}}}}} \tag{$\dagger \dagger$}$$
III) Elimination de l'abstraction.
A) Cas d'un argument:
étant donné une lettre $\mathbf x$ et un combinateur $P$, on définit par induction sur la taille de $P$ le combinateur $\l {\mathbf x} P$ de la façon suivante:
(i) $\l {\mathbf x} {\mathbf x} := \i$
(ii) $\l {\mathbf x} P := \o {\k} P$ lorsque $P$ ne contient aucune occurrence de la lettre $\mathbf x$
(iii) $\l {\mathbf x}{\o Q {\mathbf x}} := Q$ lorsque $Q$ ne contient aucune occurrence de la lettre $\mathbf x$.
(iv) dans tous les autres cas, $P$ est de la forme $\o M N$ avec $M,N$ combinateurs et on pose $\l {\mathbf x}{\o M N} := \o{\o{\s}{\l {\mathbf x}{M}}}{\l {\mathbf x} N}$

On peut maintenant énoncer le théorème fondamental de la logique combinatoire:
Pour toute lettre $\mathbf y$ et tous combinateurs $F,Z$, la lettre $\mathbf y$ ne figure pas dans $\l {\mathbf y} F$, et toutes les autres lettres (les constantes $\s,\k$ ne sont pas considérées comme des lettres) apparaissant dans $\l {\mathbf y} F$ apparaissent dans $F$. De plus $$\r {\o {\l {\mathbf y} F} Z} {\sub {\mathbf y} Z F} \tag{*}$$.
Le fait que l'algorithme définissant $\lambda$ retire une par une toutes les occurences de $\mathbf y$ dans $F$ est évident.
Le deuxième point du théorème se démontre par induction sur le nombre de symboles de $F$ en examinant les 4 cas dans la définition de $\lambda$:
cas (i): découle de l'exemple du I)
cas (ii): découle du 1°) de la définition du I)
cas (iii): découle de ce que comme $\mathbf y$ n'apparaît pas dans $F$, $\sub {\mathbf y} Z F$
cas (iv): découle du 2°) de la définition du I) et de l'hypothèse de récurrence (l'initialisation étant couverte par les cas (i) et (ii) ci-dessus).

Remarque: on a en particulier compte tenu de II) 3°), $\r {\o {\l {\mathbf y} F} {\mathbf y}} F$ (puisque $ \sub {\mathbf y} {\mathbf y} F $ est identique à $F$).

Cas de plusieurs arguments.
Soient $d$ un entier et $\vec {\mathbf x} = (\mathbf x_1,\mathbf x_2,...,\mathbf x_d)$ une liste de lettres distinctes deux à deux.
Etant donnés un combinateur $C$, et une liste $\vec T := (T_1,...,T_d)$ de combinateurs, on désigne par $\subv {\mathbf x} {T} C$ le combinateur obtenu en remplaçant, pour tout $i=1,...,d$, toutes les occurrences de la lettre $\mathbf x_i$ par $T_i$ dans $C$. La substitution décrite au II) est un cas particulier de cette opération avec des listes d'une seule lettre et un seul combinateur.
$(\clubsuit)$ On a à nouveau, pour les mêmes raisons, $\r {\subv {\mathbf x} T M} {\subv {\mathbf x} T N}$ pour tous combinateurs $M,N$ tels que $\r M N$. A nouveau il suffit de regarder ce qui se passe sur les étapes élémentaires d'une réduction.

Lemme: pour tout combinateur $P$, $$
\r {\o {\ldots \o {\o {\l {\mathbf x_1} {\l {\mathbf x_2} {\ldots {\l {\mathbf x_d} P}}}} {\mathbf x_1}} {\mathbf x_2}} {\ldots \mathbf x_d}} P \tag{**}$$Ce lemme se montre par récurrence immédiate sur $d$ en exploitant la remarque à la fin de II)A)
On en déduit une généralisation à $d$ arguments du résultat fondamental du même paragraphe:
Pour tout combinateur $Q$,$$
\r {\o {\ldots \o {\o {\l {\mathbf x_1} {\l {\mathbf x_2} {\ldots {\l {\mathbf x_d} Q}}}} T_1} T_2} {\ldots T_d}} {\subv {\mathbf x} T Q} \tag{***}$$
Cela découle de $(**)$ ci-dessus et de la remarque $(\clubsuit)$ plus haut vu que comme $\l {\mathbf x_1} {\l {\mathbf x_2} {\ldots {\l {\mathbf x_d} P}}}$ ne contient aucune occurrence des lettres $\mathbf x_1, \mathbf x_2,...,\mathbf x_d$, $\subv {\mathbf x} T {\o {\ldots \o {\o {\l {\mathbf x_1} {\l {\mathbf x_2} {\ldots {\l {\mathbf x_d} Q}}}} {\mathbf x_1}} {\mathbf x_2}} {\ldots \mathbf x_d}}$ est identique à $\o {\ldots \o {\o {\l {\mathbf x_1} {\l {\mathbf x_2} {\ldots {\l {\mathbf x_d} Q}}}} T_1} T_2} {\ldots T_d}$.

La logique combinatoire, via $(*)$ et $(***)$ ci-dessus, donne donc un sens précis à la notion de "définition d'une fonction par une expression avec des variables".
Exemple: prenons à nouveau les lettres $x,y,z$. Un calcul montre que $\l x {\l y {\l z {\o x {\o y z}}}}$ est le combinateur $\b$. Si $F,G,H$ sont trois autres combinateurs, on a $\r {\o {\o {\o {\l x {\l y {\l z {\o x {\o y z}}}}}F}G}H} {\o F {\o G H}}$, autrement dit: $\r {\o {\o {\o {\b}F}G}H} {\o F {\o G H}}$. L'exemple $(\dagger \dagger)$ du II) plus haut est un cas particulier de cette relation.

IV) Introduction au typage.
Il est impossible de résumer la totalité des systèmes de typages qui existent en maths ou en informatique. Celui qui est présenté ci-dessous est le plus simple que je connaisse (c'est un début!).
On introduit un nouvel alphabet (on utilisera des lettres grecques ci-dessous). On appelle sorte (ou pour faire court: type) une expression obtenue de la façon suivante:
-une lettre est une sorte
-si $\Phi,\Psi$ sont des sortes, $\a {\Phi}{\Psi}$ est une sorte.

Un contexte est un ensemble de couples $(\mathbf a_1:\Theta_1),...,(\mathbf a_n:\Theta_n)$ de couples où pour tout $i=1...n$, $\mathbf a_i$ est une lettre et $\Theta_i$ un type.

Etant donné un contexte $\mathcal C$, on définit une relation binaire entre combinateurs
On introduit une nouvelle relation binaire entre combinateurs $T$ et types $\Xi$, notée $\jt {\mathcal C}{T}{\Xi}$ (on dira que "$T$ est de type $\Xi$ dans $\mathcal C$" ou même simplement "$T$ est de type $\Xi$" si aucune confusion n'est à craindre), définie par induction de la façon suivante:
-si $(T:\Xi) \in \mathcal C$ alors $\jt {\mathcal C}{T}{\Xi}$
-pour toutes sortes $\Gamma,\Delta$, on a $\jt {\mathcal C}{\k}{\a {\Gamma} {\a {\Delta}{\Gamma}}}$
-pour toutes sortes $\Phi,\Psi,\Sigma$, on a $\jt {\mathcal C}{\s}{\a {\a {\Phi}{\a{\Psi}{\Sigma}}}{\a{\a{\Phi}{\Psi}}{\a{\Phi}{\Sigma}}}}$
-pour toutes sortes $\Upsilon,\Omega$ et tous combinateurs $P,Q$, si $\jt {\mathcal C} P {\a{\Upsilon}{\Omega}}$ et $\jt {\mathcal C} Q {\Upsilon}$ alors $\jt {\mathcal C} {\o P Q} {\Omega}$

Citons deux résultats exprimant le bon comportement de cette notion vis-à-vis de celles que nous avons définies au points précédents. Soit $\mathcal D$ un contexte.
1°) Pour tous combinateurs $V,W$ tels que $\r V W$ et toute sorte $\Xi$, si $\jt {\mathcal D} V \Xi$ alors $\jt {\mathcal D} W \Xi$
2°) Pour toute lettre $\mathbf x$ ne figurant pas dans $\mathcal D$, toutes sortes $\Delta,\Sigma$ et tout combinateur $F$ tel que $\jt{\mathcal D \cup \{(\mathbf x : \Delta)\}} F {\Sigma}$, on a également $\jt {\mathcal D} {\l {\mathbf x} F} {\a {\Delta}{\Sigma}}$
Ces résultats se montrent par induction respectivement sur la taille de la preuve de la relation de réduction dans le premier cas et sur la taille du combinateur dans le second.
Noter que si un terme $X$ est typable dans un contexte $\mathcal E$ (i.e. il existe une sorte $\Omega$ telle que $\jt {\mathcal E} T {\Omega}$), alors toutes les lettres apparaissant dans $X$ apparaissent dans $\mathcal E$ (examiner les étapes de la preuve de ce que le terme est typable).

D'autres exemples seront introduits plus loin.