Nous étudions les isomorphismes de types dans un lambda-calcul simplement typé avec types indcutifs et opérateurs de récursion. Nous montrons que, dans certains cas (produits n-aires, copies de types), on peut ajouter de nouvelles règles de réduction de telle sorte que:
Ces travaux s'inscrivent dans un mouvement initié à la fin des années 70 par S. Soloviev [1], puis relancé dans les années 90, notamment par G. Longo et R. Di Cosmo [2], qui s'est (entre autres) interessé successivement aux isomorphismes de types simples (flèche, produit, unit) [2,3], du second ordre [3], puis aux types somme [4].
[1] S. Soloviev (1981) The category of finite sets and Cartesian closed categories
[2] K. Bruce, R. Di Cosmo, G. Longo (1992) Provable isomorphisms of types
[3] R. Di Cosmo (1995) Isomorphisms of types: from lambda-calculus to information retrieval
[4] V. Balat (2002) Une étude des sommes fortes : isomorphismes et formes normales