Une r\'eponse n\'egative \`a la conjecture de E. Tronci pour les syst\`emes num\'eriques typ\'es

TL;DR

This paper demonstrates that within the Girard type system F, having a storage operator does not imply a numeral system is adequate, providing a negative answer to Tronci's conjecture in this context.

Contribution

It provides a counterexample to Tronci's conjecture for typable numeral systems in Girard's system F, showing the conjecture does not hold universally.

Findings

Counterexample to Tronci's conjecture in system F

Adequacy of numeral systems is not implied by storage operators in this setting

The conjecture remains open in pure λ-calculus

Abstract

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 F. The E. Tronci's conjecture remains open in pure $\lambda$-calculus.