14/06/2001: Thierry Joly (Univ. Nijmegen)
Les types simples finiment engendrés.
Résumé
On reprend une vieille question concernant le lambda-calcul simplement typé de Church :
"Quels sont les types finiment engendrés, c'est-à-dire les types dont les habitants clos sont tous
bêta-êta-équivalents à une combinaison applicative d'éléments d'un même ensemble fini G de
lambda-termes clos (de types quelconques) ?"
(Exemple : le type Nat = (o->o)->(o->o) des entiers de Church est finiment engendré par
l'ensemble G = {Succ : Nat->Nat, Zero : Nat}, où : Succ = \x : Nat \s : o->o \z : o . s(xsz) et
Zero = \s : Nat \z : o->o . z.)
On répond à cette question en la rapprochant d'un autre vieux problème sur les types simples :
DP (Definability Problem) : "Etant donné une fonctionnelle quelconque phi de n'importe quel modèle
plein fini M, existe-t-il un lambda-terme clos dont l'interprétation dans M soit précisément phi ?"
(Rappelons qu'un modèle plein fini M est une famille d'ensembles finis M^T tels que pour tous
types A et B, M^{A->B} soit l'ensemble de toutes les applications de M^A dans M^B.)
R. Loader (1995) a établi l'indécidabilité de DP et même celle de sa restriction DP_M aux
fonctionnelles d'un seul modèle M dont l'un des ensembles M^a (a atomique) possède au moins
7 éléments.
On considère ici pour chaque type T, la restriction orthogonale DP_T de DP aux seules fonctionnelles
de type T et l'on montre que les hypothèses suivantes sont équivalentes :
1. T est finiment engendré,
2. DP_T est décidable,
3. Tous les termes normaux clos de type T se laissent écrire à l'aide d'une même ressource finie de
variables typées.
Enfin, en adaptant l'algorithme de Ben-Yelles (qui décide si un type T donné est habité ou vide), on
décide facilement à l'aide de la clause 3. plus haut si un type T donné est finiment engendré ou non.