Une response négative à la conjecture de E. Tronci pour les systèmes numériques typés
Une réponse négative à la conjecture de E. Tronci pour les systèmes numériques typés
摘要:
一个数制是一个无穷多个不同的闭正规$λ$ -项的序列,它具有用于后继和零检验的闭$λ$ -项。称一个数制是适当的,当且仅当它有一个用于前趋的闭$λ$ -项。数制的存储算子是一个封闭的$λ$项,它在“按名调用”策略的上下文中模拟“按值调用”。E. Tronci证明了下面的结果:一个数字系统是足够的,如果它有一个存储算子。本文对J. Y. Girard型系统F.急诊Tronci猜想在纯$λ$ -演算中仍然是开放的。
英文摘要:
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分析而来,可能存在错误,请以论文正文为准。