Abstract FR:

On donne un eclairage theorique nouveau sur un systeme de preuves de totalite de fonctions developpe par p. Manoury et m. Simonot. Ce systeme s'inscrit dans le cadre de la theorie des types recursifs qui a pour principe l'isomorphisme de curry-howard. On associe a chacune des fonctions donnees par des ensembles equationnels une mesure ordinale verifiant la propriete de decroissance stricte pour tout appel inductif. Ces mesures sont definies sur des uplets de termes clos et leur famille admet comme borne superieure omega puissance omega. On montre que les mesures peuvent s'obtenir a l'aide de la trace constituee par les lambda-termes. On montre egalement que cette famille de mesure, caracterisant la terminaison, peut s'etendre a d'autres ensembles equationnels. A titre d'application on etablit un lien avec le systeme de boyer-moore. Pour cela, on definit de nouvelles mesures ordinales a valeurs dans epsilon zero dont la famille est en bijection avec la premiere. On prouve alors que si une fonction est totale dans le systeme de manoury et simonot elle l'est egalement dans le systeme de boyer-moore muni de la nouvelle mesure.