BERTINI YVES

 YVES BERTINI

Doctorant


Informations diverses

Thèmes de Recherche

La notion de non-défini en l-calcul

Le but de cette étude est d'essayer de décrire les termes du l-calcul qui n'ont pas de sens opératoire. Ce qu'on appelle les termes non-définis.

La caractérisation des non-définis qu'on adopte ici est celle des termes faciles. Elle a été introduite par G.Jacopini et M.Venturini Zilli. Elle s'énonce ainsi : un terme U est facile si, pour tout terme clos M, la l-théorie T=lb+ { U=M } (i.e la b-réduction plus l'équation U=M) conserve une consistance. Autrement dit, si on identifie un terme facile a un terme clos, on n'aboutira pas à la contradiction N1=N2 pour N1 et N2 deux termes normaux.

Ainsi définis, les termes faciles ont finalement comme propriétés opératoires celles de n'importe quel autre terme clos. Autant dire qu'ils n'en ont pas.

Dans son article [1] Alessandro Berarducci donne une classe assez large de termes faciles : celle des zéros-termes forts de degré fini. Pour les zéros-termes forts de degré infini, il n'y a pas de réponse générale. Et pour cause, on peut trouver des exemples qui sont faciles, et d'autres qui ne le sont pas.

L'étude des termes faciles s'oriente donc vers celle des zéros-termes forts de degré infini. Et parmi ces termes, le combinateur YtW3 est remarquable par sa capacité à se répliquer à la fois à gauche et à droite. Quant à sa facilité, la question reste ouverte [2]. Aussi j'espère que l'étude particulière de YtW3 permettra de mieux comprendre le comportement des termes de degré infini.

Références
[1]
Alessandro Berarducci : Infinite l-calculus and non-sensible models. ('94).
[2]
Alessandro Berarducci and Benedetto Intigrila : Church-Rosser Theories, infinite l-termes and consistency problems. ('95) 

Publications


Baladez-vous
dans la grande famille du LAMA











This document was translated from LATEX by HEVEA.