INTRODUCTION
(André Brouty)
Cet exposé est sous licence libre
LLDD.
Le but de ce petit travail est de faire le point sur l'état actuel des
connaissances concernant l'existence et la caractérisation des termes
inversibles dans le lambda calcul et en logique combinatoire.
Pour pouvoir parler de termes inversibles il faut disposer d'une structure
algébrique adéquate dans laquelle la notion d'inversibilité peut
être définie.
C'est précisement le but du premier chapitre que d'introduire le cadre formel
de cette étude et de rappeler ou préciser les outils mathématiques
qui seront
nécessaires pour aborder les chapitres suivants. nous rappelons brièvement
les différentes théories utilisées:
L,
L0,
CL,
CL0 en mettant en évidence les
différences les caractérisant.
Dans le second chapitre nous abordons l'étude des combinateurs inversibles
en logique combinatoire avec extensionalité,c'est-à-dire du plus grand groupe
contenu dans le monoïde (
CL0+ext,B,I).
Ayant ainsi caractérisé les termes inversibles on aborde dans le troisième
chapitre l'étude des termes inversibles à gauche ou inversibles à droite dans
le monoïde (
L,B,I) sans extensionalité.
Enfin le quatrième chapitre est consacré à l'étude d'un algorithme permet-
tant de repérer quand ils existent les termes inversibles que nous avons
traités dans le
second chapitre et de donner leurs inverses ou bien,en cas de terminaison de
l'algorithme,de donner une des raisons pour laquelle un tel inverse n'existe pas.
Pour terminer je tiens à remercier tout particulièrement Emmanuel Saint-James pour l'aide
précieuse qu'il m'a apportée dans la mise au point de ce délicat programme.