A negative answer to Tronci’s conjecture for typed numerical systems. (Une réponse négative à la conjecture de E. Tronci pour les systèmes numériques typés.) (French) Zbl 0898.68010

Summary: A numeral system is a sequence of an infinite different closed normal \(\lambda\)-terms which has closed \(\lambda\)-terms for successor and zero test. A numeral system is said adequate iff it has a closed \(\lambda\)-term for predecessor. A storage operator for a numeral system is a closed \(\lambda\)-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 \({\mathcal F}\). The E. Tronci’s conjecture remains open in pure \(\lambda\)-calculus.


68N15 Theory of programming languages


numeral system
Full Text: DOI EuDML


[1] 1. H. BARENDREGT, The lambda calculus, its syntax and semantics, North Holland, 1984. Zbl0551.03007 MR774952 · Zbl 0551.03007
[2] 2. J.-Y. GIRARD, Y. LAFONT et P. TAYLOR, Proofs and types, Cambridge University Press, 1986. Zbl0671.68002 MR1003608 · Zbl 0671.68002
[3] 3. J.-L. KRIVINE, Lambda calcul, types et modèles, Masson, 1990. Zbl0697.03004 MR1162977 · Zbl 0697.03004
[4] 4. J.-L. KRIVINE, Opérateurs de mise en mémoire et traduction de Gödel, Archive for Mathematical Logic, 1990, 30, p. 241-267. Zbl0712.03009 MR1080590 · Zbl 0712.03009
[5] 5. K. NOUR, Opérateurs de mise en mémoire en lambda-calcul pure et typé, Thèse de Doctorat, Université de Chambéry, 1993.
[6] 6. K. NOUR, An example of a non adequate numeral system, CRAS. Paris, 1996, 323, Série I, p. 439-442. Zbl0864.03011 MR1408972 · Zbl 0864.03011
[7] 7. K. NOUR, A conjecture on numeral system, Notre Dame of Formal Logic, 1997, 38, p. 270-275. Zbl0918.03009 MR1489413 · Zbl 0918.03009
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.