29/06/2000: Vincent Padovani, PPS---
Retractions et Types Simples
Résumé
Je presenterai la solution d'un probleme jusqu'ici ouvert, celui de la
caracterisation des retractions valides entre types simples: il s'agit,
etant donne deux types A, B, de determiner s'il existe u : A -> B,
v: B -> A tels que (u o v) = I : A -> A a beta/eta equivalence pres.
On sait, depuis 1985 (Bruce, Longo) caracteriser les couples A,B
isomorphes (u o v = I, v o u = I) et, depuis 1992 (Piperno, de'Liguoro,
Statman), les retractions definissables par des termes lineaires, dans
les deux cas via un systeme de types permettant de deriver de tels
couples. La methode presentee ici est differente: je montrerai que la
relation "A est retractible en B" est corollaire (inattendu) de la
decidabilite du modele minimal du lambda-calcul simplement type.