加载中…
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.

生成讲解博客的中文版本

生成AI智能校验的中文版本