Les types non finiment engendrés du Λ-Calcul

Thierry Joly

On résout une question soulevée par R. Statman concernant le λ-calcul simplement typé (doté d’un unique type atomique o) : peut-on trouver un ensemble fini de λ-termes clos engendrant par applications tous les termes clos d’un type donné à βη-équivalence près ? On montre que les seuls types pour lesquels cela est possible sont les types de rang au plus deux, les types de rang trois dont tous les sous-types de rang deux sont de la forme : T → o et, bien sûr, les types ne possédant pas de λ-termes clos.

Ces faits sont déduits d’un théorème d’indécidabilité dû à R. Loader à l’aide de divers codages des λ-termes purs dans le calcul typé permettant d’y représenter un grand nombre de surjections entre types.

Address: Equipe P.P.S., Université Paris 7, Paris, France. Personal address: 84, rue du Mont Cenis, 75018 Paris, France

E-mail: joly@logique.jussieu.fr