对E. Tronci关于类型化数字系统猜想的否定回答
逻辑
2009-05-06 v1
摘要
一个数字系统是一个由无穷多个不同的封闭正规λ项组成的序列，该序列具有用于后继和零测试的封闭λ项。一个数字系统被称为是充分的，当且仅当它有一个用于前驱的封闭λ项。一个数字系统的存储算子是一个封闭λ项，它在“按名调用”策略的上下文中模拟“按值调用”。E. Tronci猜想如下结果：如果一个数字系统有一个存储算子，那么它是充分的。本文对J.-Y. Girard类型系统F中可类型化的数字系统给出了该猜想的否定回答。E. Tronci的猜想在纯λ演算中仍然悬而未决。
引用
@article{arxiv.0905.0574,
title = {Une r\'eponse n\'egative \`a la conjecture de E. Tronci pour les syst\`emes num\'eriques typ\'es},
author = {Karim Nour},
journal= {arXiv preprint arXiv:0905.0574},
year = {2009}
}