Mail/M'écrire


Chapitre 2  CARACTERISATION DES TERMES INVERSIBLES EN LOGIQUE COMBINATOIRE.

(André Brouty)
Cet exposé est sous licence libre LLDD.
Dans ce chapitre nous nous plaçons exclusivement dans le système CL0+ext.

2.1  INVERSE DANS UN MONOÏDE.

Pour pouvoir parler d'inverse il nous faut disposer d'une structure algébrique; c'est-à-dire d'un ensemble non vide muni d'une loi d'opération binaire et d'un élément neutre associé à cette loi. L'associativité de l'opération binaire est souvent exigée car cette propriété permet de montrer Nous prendrons comme ensemble CL0, comme opération binaire B et comme élément neutre I. Il est bien connu que l'opération B est associative. Nous obtenons ainsi le monoïde (CL0,B,I). Rappelons que B et I vérifient:
BXYZ=X(YZ)
IX=X
X Y et Z représentent des combinateurs quelconques.
Un terme X de CL0 est dit inversible s'il existe un terme X' de CL0 tel que
BXX'=I et BX'X=I.
Étant dans un monoïde nous sommes assurés de l'unicité de l'inverse quand il existe.
Une remarque: contrairement aux monoïdes classiques le monoïde (CL0,B,I) a la particularité de contenir son opération comme élément.

2.2  INTÉRET.

Une équation entre termes combinatoires de la forme NX=Y où N et Y sont suposés être en forme normale admet une solution précisément si N admet un inverse N'. En effet on a alors:
N'(NX)=N'Y
BN'NX=N'Y
IX=N'Y
X=N'Y
En analogie avec l'algèbre classique.

Remarquons tout d'abord que dans CL0+ext un combinateur U d'ordre n qui vérifie
UX1X2… Xn=X1X2… Xn
est équivalent à I qui, lui, est d'ordre 1 par définition; U peut être representé par le combinateur
B(B(B...(B(n−1) foisI)...))
qui est bien d'ordre n on le notera BnI. Pour apporter un peu plus de précision dans l'écriture on posera In=BnI; on aura donc In=Ip pour tout n et p positifs non nuls.

2.3  DÉFINITION.

Un permutateur P d'ordre n+1 est un combinateur d'ordre n+1 tel que:
PX0X1X2… Xn=Xf(0)Xf(1)Xf(2)… Xf(n)
où f est une bijection de {0 1 2 … n} dans {0 1 2 … n} (permutation).

2.4  RÉSULTATS.

En 1958 Curry ([3] pp 167-168) établit que les seuls combinateurs réguliers et propres ayant un inverse sont les permutateurs réguliers.

Soit donc P un combinateur d'ordre n+1; il doit vérifier: PX0X1… Xn=A0A1… Ap; P étant supposé propre, Ai, qui est un terme comme Xi est écrit exclusivement en termes de Xi. Supposons l'existence d'un inverse noté P−1. Commençons par remarquer que l'inversibilité à droite impose la régularité. En effet on doit avoir
BPP−1X0X1… Xn=X0X1… Xn
Or
BPP−1X0X1… Xn=P(P−1X0)X1… Xn=A'0A'1… A'p
où A'i= S(Ai)[X0 ←— P−1X0].
Supposons qu'il existe j ≠ 0 le plus petit entier tel que A'j contienne le terme P−1X0, alors aucune réduction n'est possible sur un tel terme qui doit se réduire à X0X1… Xn sauf si P−1=I et A'i=Xi et alors P=I. Donc P est régulier ainsi que P−1 puisque P est aussi l'inverse à droite de P−1. Donc A0=X0.
Soit donc maintenant P−1 un inverse de P; il doit vérifier:
P−1X0X1… Xp=X0C1… Cq
On a
BPP−1X0X1… Xn = P(P−1X0)X1… Xn
  = P−1X0A'1… A'p
  = X0C'1… C'q
  = X0X1… Xn
Avec
A'i= S(Ai)[X0 ←— P−1X0]
C'i= S(Ci)[X1 ←— A'1… Xp ←— A'p]
On en déduit que q=n et que C'i=Xi puisque les deux dernières lignes représentent des expressions en forme normale équivalentes. De plus on ne saurait avoir p<n car il n'y a évidemment pas de combinateur qui ajoute des variables à la demande; donc p≥ n. Par définition de l'inverse on a aussi:
BP−1PX0X1… Xp = P−1(PX0)X1… Xp
  = PX0B1… Bn
  = X0B'1… B'p
  = X0X1… Xp
Avec
Bi= S(Ci)[X0 ←— PX0]
B'i= S(Ai)[X1 ←— B1… Xn ←— Bn]
On en déduit de même que n=p et B'i=Xi. Il s'ensuit alors que Ai est réduit à un atome ainsi que Ci. Comme n=p=q on a le résultat de Curry: P et P−1 sont des permutateurs réguliers.

On peut se demander s'il existe des combinateurs réguliers non propres qui sont inversibles. La réponse est positive comme le montre Dezani en 1975. On va pour cela généraliser les permutateurs précédents à une classe particulière qu'on appellera permutateurs héréditairement finis. Soit donc l'ensemble P construit récursivement comme suit: f étant toujours une permutation de {1 2 … n}.

2.5  EXEMPLES

C=λ(x0 x1 x2)(x0 x2 x1)
λ(x0 x1 x2)(x0 (C x2) (I x1))
λ(x0 x1 x2 x3)(x0 (C x3) (I x1) (C x2))
sont des éléments de P. On a alors le résultat suivant:
Théorème 1   Les combinateurs en forme normale qui ont un inverse sont exactement les éléments de P.
Autrement dit ( P B I) est un groupe et c'est le plus grand groupe contenu dans le monoïde (CL0 B I).

Pour être plus précis on peut donner l'inverse d'un élément de P. Soient donc M et N deux éléments de P définis par:
M=λ(x0 x1 … xn)(x0 (M1 xf(1)) (M2 xf(2)) … (Mn xf(n)))
N=λ(x0 x1 … xn)(x0 (N1 xg(1)) (N2 xg(2)) … (Nn xg(n)))
Ces deux éléments sont inverses l'un de l'autre si l'on a
g=f−1 et Ni=Mf−1(i)−1
où Mj−1 désigne l'inverse du combinateur Mj et f−1 la permutation réciproque de f. En effet si nous calculons BMN nous avons:
BMNX0X1… Xn=M(NX0)X1… Xn
=NX0 (M1 Xf(1))(M2 Xf(2)) … (Mi Xf(i)) … (Mn Xf(n))
=X0(N1(Mg(1) Xf(g(1)))) … (Ni(Mg(i) Xf(g(i)))) … (Nn(Mg(n) Xf(g(n))))
=X0 (B N1 Mg(1) Xf(g(1))) … (B Ni Mg(i) Xf(g(i))) … (B Nn Mg(n) Xf(g(n)))
Or f(g(i))=i puisque g=f−1 et Ni=Mg(i)−1 d'où
B Ni Mg(i) Xf(g(i)) = B Mg(i)−1 Mg(i) Xi = Xi
puisque B Mg(i)−1 Mg(i) = I par définition.

Il est maintenant facile de montrer qu'un terme de P est inversible. Cela se fait par récurrence sur le nombre k d'utilisations de la définition récursive qui représente aussi la profondeur d'un élément P de P.
Si k=0 (profondeur zéro) alors P=I et P est inversible. Supposons alors l'inversibilité vérifiée pour chaque terme de profondeur k=m et montrons l'inversibilité pour un terme de profondeur k=m+1.
Une λ-expression P à cette profondeur a la forme
P=λ(x0 x1 … xn)(x0 (P1 xf(1)) … (Pn xf(n)))
où Pi est une expression de profondeur m pour laquelle s'applique l'hypothèse de récurrence; Pi a donc un inverse. Le calcul fait plus haut montre que P a aussi un inverse d'où le résultat.

On vient ainsi d'établir la condition suffisante du théorème; pour la condition nécessaire on pourra consulter [6] ou [1] pp 633-639.

Exemple

M=λ(x0 x1 x2 x3) (x0 (I x3) (C x1) (I x2))
a pour inverse
M−1=λ(x0 x1 x2 x3) (x0 (C x2)(I x3) (I x1))
D'autres exemples seront donnés dans le chapitre 4 où de plus un algorithme de reconnaissance d'inverses sera examiné.

Il est établi depuis 1980 qu'un combinateur sans forme normale n'admet pas d'inverse dans CL0+ext. On pourra à ce sujet consulter [7] où l'on verra que la preuve,très technique,de ce résultat fait largement intervenir les arbres de Bohm ainsi que le modèle de Scott dont nous n'avons pas parlé dans le chapitre 1.

Pour terminer ce chapitre disons un mot sur une éventuelle généralisation au monoïde (CL+ext,B,I). Que se passe-t-il si on accepte les variables libres? Modifie-t-on l'ensemble des expressions inversibles? Outre qu'il parait difficile de concevoir un permutateur contenant des variables libres, si on introduit une telle variable, elle doit disparaître lors du calcul de P−1(P x0)x1 x2 … xn. Cela n'est possible que si P ou P−1 a un effet cachant. Or tout combinateur à effet cachant ne saurait avoir un inverse puisqu'il n'y a pas d'expression qui ajoute des variables à la demande. On peut donc conclure que le plus grand groupe contenu dans (CL+ext,B,I) est toujours P.

Termes inversibles a gauche ou a droite dans le Lambda calcul