arXiv · 0905.0574
Une réponse négative à la conjecture de E. Tronci pour les systèmes numériques typés
Abstract
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.
Explore related subjects
Keep this discovery
Karim Nour. 2009-05-05. Une réponse négative à la conjecture de E. Tronci pour les systèmes numériques typés. https://arxiv.org/abs/0905.0574
Cite the original work for its findings. Save a collection to share your selection of sources.