Chapitre 5 QUELQUES REMARQUES ET RÉFLEXIONS EN GUISE DE CONCLUSION
(André Brouty)
Cet exposé est sous licence libre
LLDD.
5.1 SUR LA DÉCIDABILITÉ DES ALGORITHMES.
Pour revenir sur l'algorithme décrit au chapitre précédent, on peut se
demander si celui-ci est décidable. C'est-à-dire s'arrète-t-il toujours et
quand il s'arrète donne-t-il une réponse satisfaisante ?
Nous savons qu'une λ-expression sans forme normale n'admet pas
d'inverse. Si nous donnons une telle expression à notre algorithme qu'en fait-
il? Étant donné que les expressions sont systématiquement mises sous forme
normale de tête avant d'être analysées, si cette forme normale de tête
n'existe
pas (cas des termes non résolubles) l'algorithme ne s'arrètera pas. C'est
le cas par exemple du combinateur (
W W W). Tout combinateur non résoluble fait
boucler l'algorithme.
Mais un combinateur résoluble sans forme normale ne fera pas nécessairement
boucler le programme. Par exemple le combinateur (
C(
B C(
C I))(
W W W)) qui
n'a pas de forme normale puisqu'il contient un sous terme non résoluble qui
n'est pas amené à disparaitre, sera mis sous forme normale de tête pour donner
(1 0 (
W W W)) et l'algorithme s'arrètera en décrétant que ce combinateur
n'est pas régulier. Par contre avec le combinateur (
C(
B C(
B B))(
W W W)) on
obtiendra une forme normale de tête (0 1 (
W W W 2)) dont le début
correspond bien à une permutation réguliere et donc l'algorithme ira analyser le sous
terme (
W W W) qui n'est pas résoluble et bouclera.
Cet algorithme est donc semi-décidable. On a une réponse en cas d'arret
du programme seulement.
Le chapitre 3 décrit la recherche d'inverses à gauche et à droite de manière
très algorithmique. Ici aussi on peut se demander si les algorithmes
correspondants sont décidables. Ils ont en effet une grande apparence de
décidabilité, mais il ne faut pas oublier que ces algorithmes
s'appliquent aux arbres de Bohm des λ-expressions pour lesquelles
les sous termes non résolubles ont ete remplacés par un symbole particulier:
Ω. Si on part d'une λ-expression il nous faudra élaborer
un algorithme qui donne l'arbre de Bohm
associé, c'est-à-dire un algorithme qui repère les expressions non
résolubles et on sait qu'un tel algorithme n'est pas décidable.
La reconnaissance des termes inversibles se heurte donc au délicat
problème de l'arret des programmes correspondants.
5.2 SUR LA GÉNÉRALISATION DES TERMES INVERSIBLES A GAUCHE OU A DROITE AVEC L'EXTENSIONALITÉ.
Le chapitre 3 détermine la classe des termes inversibles à gauche ou
inversibles à droite dans le monoïde (
L,
B,
I).
Que se passe-t-il si l'on ajoute la règle d'extensionalité?
Augmente-t-on la classe des termes
inversibles à gauche et la classe des termes inversibles à droite?
Évidemment oui puisqu'on ajoute alors tous les termes inversibles,
c'est-à-dire les permutateurs héréditairement finis, qui, à part
I,
n'admettent pas d'inverse ni à gauche ni à droite dans (
L,
B,
I).
Y en a-t-il d'autres? Examinons cela de manière informelle.
Commençons par nous placer dans le monoïde le plus simple:
(
CL0+ext,
B,
I) et examinons un petit exemple que
l'on va généraliser. On a
| B W K x0 x1 |
= |
W (K x0) x1 |
| |
= |
K x0 x1 x1 |
| |
= |
x0 x1 |
Ainsi
B W K =
I et
W est un inverse à gauche de
K et
K est un
inverse à droite de
W.
Le combinateur
K a dejà une infinité d'inverses à gauche dans les théories
sans extensionalité (voir chapitre 3 page 23), et dans ces théories
W
n'admet pas d'inverse ni à gauche ni à droite.
Sur ce petit exemple nous constatons que
W duplique une variable que
K
vient ensuite supprimer. On peut aisément généraliser cette situation.
Soient donc
W' et
K' deux combinateurs vérifiant
| B W' K' x0 x1 … xn |
= |
W'(K' x0)x1 … xn |
| |
= |
x0 x1 … xn |
W' est donc d'ordre
n+1 et doit de plus être régulier puisqu'inversible
à droite.
W' est donc autorisé à dupliquer les variables qu'il veut
un nombre arbitraire de fois et ceci à partir de n'importe quelle
position dans la liste des variables; le combinateur
K' aura alors
pour rôle de supprimer toutes les variables ainsi dupliquées.
Mais
W' peut faire mieux encore: rien ne l'empèche de permuter
les variables avant de se livrer à la duplication,
K' ayant pour
charge de les remettre dans l'ordre et de supprimer les variables dupliquées.
On pourrait ainsi nommer
W' un permutateur-duplicateur,
K' étant alors un
permutateur-projecteur.
Il est aisé d'imaginer que chaque permutateur-duplicateur admet aussi un
permutateur-projecteur comme inverse à droite, et moins facile de
le formaliser.
Pour un permutateur-duplicateur
W' d'ordre
n+1 notons
J l'ensemble des
n+1 indices. On peut alors associer à
W' la fonction suivante:
| F : |
J —→ J× N |
| |
i ⊢→ (f(i),g(i)) |
la fonction
f :
J —→
J caractérise la permutation des
variables, et
la fonction
g :
J —→
N représente les duplications,
g(
i) est le nombre de variables dupliquées entre
xi et la variable
permutée suivante avec la
convention que les variables permutées sont celles rencontrées en premier
en lisant la liste des variables de gauche à droite.
Une telle fonction ne caractérise pas entièrement
W' puisque plusieurs
combinateurs l'admettent comme fonction associée, mais cela suffit pour donner
un inverse à droite de
W'.
Par exemple
W'=λ(x0 x1 x2 x3) (x0 x0 x2 x0 x2 x3 x0 x0 x2 x0 x1 x1)
les variables soulignées sont les variables permutées.
On a alors
f(0)=0, f(1)=2, f(2)=3, f(3)=1
g(0)=1, g(1)=1, g(2)=2, g(3)=4
et ainsi
K'=λ(x0 x1 … x11) (x0 x10 x2 x5)
est un inverse à droite de
W'.
De manière générale soient
et la fonction
G :
J —→
J' vérifiant
alors en posant
p=
MAX(
J')
K'=λ(x0 x1 … xp) (x0 xG(1) … xG(n))
est un inverse à droite
de
W' auquel est associée la fonction
F; ainsi:
Théorème 1
Tout permutateur-duplicateur régulier admet un inverse à droite.
A-t-on ainsi caracterisé la classe des termes inversibles à droite ?
Hélas non comme le montre l'exemple suivant:
W'=λ(x0 x1 x2) (x0 x2(x0 x2)x1)
qui admet pour inverse à droite
K'=λ(x0 x1 x2 x3) (x0 x3 x1).
C'est-à-dire que
W' peut se permettre de parenthéser, mais de
ne parenthéser que des termes dupliqués bien entendu, que
K'
supprimera en bloc. La classe s'élargit donc aux
permutateurs-duplicateurs-parenthéseurs.
Les a-t-on tous maintenant? Hélas non! L'exemple suivant va élargir
considérablement la classe:
W'=λ(x0 x1 x2) (x0 x2 X1 x1 x0 X2 X3 … Xp)
où
Xi est un terme quelconque admet comme inverse à droite:
K'=λ(x0 x1 … xp+4) (x0 x3 x1)
On voit qu'une telle expression peut contenir des variables libres, ce qui
élargit l'étude au monoïde (
CL+ext,
B,
I).
On voit se préciser la classe des termes
inversibles à droite. Il suffit de glisser dans
les permutateurs-duplicateurs-parenthéseurs précédents
des termes quelconques en nombre quelconque. A-t-on la
classe maintenant? Encore hélas non! Deux petits exemples
vont nous éclairer. Une remarque d'abord: il suffit qu'il y ait parmi la
liste des termes de
W' une permutation des variables pour être assurés de
l'inversibilité à droite, les deux exemples suivants n'entrent pas dans cette
catégorie.
W'=λ(x0 x1) (x0 (K x1))
a pour inverse à droite
K'=λ(x0 x1) (x0 (W x1))
En effet on a:
| W'(K' x0)x1 |
= |
K' x0 (K x1) |
| |
= |
x0 (W (K x1)) |
| |
= |
x0 (B W K x1) |
| |
= |
x0 (I x1) |
| |
= |
x0 x1 |
puisque
B W K =
I dans ce contexte.
Cet exemple n'entre pas dans la classe précédente puisque
K' n'est ni un
projecteur ni un permutateur.
Le second exemple est de même nature mais fait intervenir un projecteur:
W'=λ(x0 x1 x2 x3) (x0 x0 x1 x1 (K x2) x3 x1)
a pour inverse
K'=λ(x0x1x2x3x4x5x6)(x0x3(Wx4)x5)
De manière plus générale soit:
W'=λ(x0 … xn) (x0∗∗(K1 xf(1))∗∗(K2 xf(2))∗∗ … ∗∗(Kn xf(n))∗∗)
où ∗∗ représente des termes quelconques ou des variables dupliquées
et où les
Ki sont des termes inversibles à gauche admet comme
inverse à droite:
K'=λ(x0 x1 … xp) (x0(WG(1) xG(1)) (WG(2) xG(2))…(WG(n) xG(n)))
où
p est le nombre total de termes de
W',
Wi un inverse à droite
de
Ki et où
G désigne la fonction définie précédemment.
On constate donc que la recherche des termes inversibles à droite suppose
connus les termes inversibles à gauche. Or l'exemple
K' ci-dessus est
inversible à gauche et utilise des termes inversibles à droite.
Il apparait ainsi que la caractérisation de ces termes ne peut se
faire indépendamment les uns des autres dans ce contexte .
L'étude des termes inversibles à gauche est plus délicate.
Il est cependant facile d'établir que:
Tout permutateur-projecteur régulier admet un inverse à gauche.
Tous les exemples d'inverses à gauche qu'on a donnés dans ce chapitre sont
réguliers et n'admettent pas d'inverse à gauche sans l'extensionalité.
Dans les théories sans extensionalité les termes inversibles à gauche
ne sont pas réguliers à part
I.
On peut se demander s'il existe des termes inversibles à
gauche avec usage de la règle d'extensionalité et qui ne sont pas
réguliers. En voici un exemple:
K'=λ(x0 x1 x2) (x1 (x0 x2))
qui n'est pas régulier et pas
inversible à gauche sans l'extensionalité admet ici comme inverse à gauche
W'=λ(x0 x1) (x0 I x1)
On peut donner maintenant une classe assez
grosse de termes inversibles.
Soit
D0 l'ensemble des expressions de la forme
λ(x0 x1 … xn) (x0 X1 X2 … Xp)
où les
Xi sont des termes ou
des variables quelconques tels que
n d'entr'eux représentent
une permutation des variables
x1 …
xn.
D0 est
une classe de termes inversibles à droite.
Soit
G0 l'ensemble des expressions inversibles à gauche sans
l'extensionalité.
Définissons deux suites d'ensembles (
Di)
i∈ N et
(
Gi)
i∈ N.
L'ensemble
Di+1 contient les termes de la forme:
λ(x0 x1 … xp) (x0∗∗(K1 xf(1))∗∗(K2 xf(2))∗∗ … ∗∗(Kp xf(p))∗∗)
sachant que
f est une permutation de {1,2,…,
p} et que
Kj
est élément de
Gi.
L'ensemble
Gi+1 contient les termes de la forme:
λ(x0 x1 … xq) (x0 (W1 xg(1)) (W2 xg(2)) … (Wk xg(k)))
sachant que
g est une injection de {1,2,…,
q} dans lui-même et
que
Wj est élément de
Di. Alors:
est une classe de termes
inversibles à droite et
est une classe de termes inversibles à gauche.
Malheureusement ces classes ne caractérisent pas complètement les termes
inversibles qui nous intéressent puisque l'exemple précédent n'en fait pas
partie ainsi que l'exemple suivant:
K'=λ(x0 x1 x2) (x1 (x0 (W x2)))
a pour inverse à gauche
W'=λ(x0 x1) (x0 I (K x1))
car
| W'(K' x0) x1 |
= |
K' x0 I (K x1) |
| |
= |
I (x0 (W (K x1))) |
| |
= |
x0 (B W K x1) |
| |
= |
x0 (I x1) |
| |
= |
x0 x1 |
A l'heure où nous mettons sous presse nous n'avons pas
suffisamment avancé notre étude pour en dire beaucoup plus
sur la question.
Ce chapitre de débroussaillage, un peu flou, montre que la
difficulté pour clarifier la question tient dans la mise au point d'un
formalisme simple permettant de décrire parfaitement les termes qui ont été
introduits dans ce chapitre de manière informelle. Nous ne désesperons pas
d'y arriver un jour.