UNE RÉPONSE NÉGATIVE À LA CONJECTURE DE E. TRONCI POUR LES SYSTÈMES NUMÉRIQUES TYPÉS

摘要

A numeral system is a sequence of an infinite different closed normal λ-terms which has closed λ-terms for successor and zero test. A numeral system is said adequate iff it has a closed λ-term for predecessor. A storage operator for a numeral system is a closed λ-term which simulate "call-by-value" in the context of a "call-by-name" strategy. E. Tronci conjectured the following result : a numeral system is adequate if it has a storage operator. This paper gives a negative answer to this conjecture for the numeral systems typable in the J.-Y. Girard type system F. The E. Tronci's conjecture remains open in pure λ-calculus.%Un système numérique est une suite de λ-termes normaux clos distincts pour laquelle il existe des λ-termes clos pour les fonctions successeur et test à zéro. Un système numérique est dit adéquat ssi il existe un λ-terme clos pour la fonction prédécesseur. Un opérateur de mise en mémoire pour un système numérique est un λ-terme clos qui simule "l'appel-par-valeur" dans le cadre de "l'appel-par-nom". E. Tronci a conjecturé le résultat suivant : un système numérique est adéquat s'il possède un opérateur de mise en mémoire. Nous donnons, dans cet article, une réponse négative à la conjecture de E. Tronci mais uniquement pour les systèmes numériques typable dans le système F. La conjecture de E. Tronci reste sans solution en λ-calcul pur.