存在高阶引用时的类型同构
Isomorphisms of types in the presence of higher-order references
摘要：
我们研究了具有高阶引用的程序设计语言中的类型同构问题。我们首先回顾了Abramsky，Honda和McCusker的高阶参考的博弈论模型。解决一个公开的问题，劳伦特，我们表明，两个分支的竞技场是同构的当且仅当它们是几何相同的，到更名的动作（劳伦特的森林同构）。我们由此推导出一个等式理论，它描述了具有高阶引用的有限语言中类型的同构。然而，我们表明，洛朗的猜想并不持有无限分支的舞台上，产生一个非平凡的类型同构的扩展，这种语言与自然数。
英文摘要：
We investigate the problem of type isomorphisms in a programming language with higher-order references. We first recall the game-theoretic model of higher-order references by Abramsky, Honda and McCusker. Solving an open problem by Laurent, we show that two finitely branching arenas are isomorphic if and only if they are geometrically the same, up to renaming of moves (Laurent's forest isomorphism). We deduce from this an equational theory characterizing isomorphisms of types in a finitary language with higher order references. We show however that Laurent's conjecture does not hold on infinitely branching arenas, yielding a non-trivial type isomorphism in the extension of this language with natural numbers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
