A Fully Abstract Bidomain Model of Unary FPC
A Fully Abstract Bidomain Model of Unary FPC
复制标题
一元FPC的完全抽象双域模型
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
J. Laird
中科院分区：
文献类型：
--
作者：
J. Laird
我们提出了一个完全抽象和有效的一元FPC模型（一种带提升和而不是提升和的FPC版本），它属于二元函数和连续稳定函数的范畴。首先证明了一元FPC相应模型的通用性，然后证明了这意味着一元FPC的完全抽象。我们使用翻译到这种元语言来证明惰性λ-微积分的“规范”双域模型（具有顺序收敛性测试）是完全抽象的。
We present a fully abstract and effectively presentable model of unary FPC (a version of FPC with lifting rather than lifted sums) in a category of bicpos and continuous and stable functions. We show universality for the corresponding model of unary PCF, and then show that this implies full abstraction for unary FPC. We use a translation into this metalanguage to show that the "canonical" bidomain model of the lazy λ-calculus (with seqential convergence testing) is fully abstract.