论文标题
在合成守卫领域理论中对Topoi进行分类
Classifying topoi in synthetic guarded domain theory
论文作者
论文摘要
几种不同的Topoi在合成保护领域理论（SGDT）的开发和应用中发挥了重要作用，这是一种新型的合成领域理论，该理论抽象了在编程语言语言语义中经常采用的保护递归的概念。为了统一守护的递归和共同引导的帐户，一些作者用多个“时钟”参数化了不同的时间流，从而使SGDT更加复杂且难以理解TOPOS模型。到目前为止，这些拓扑topoi已被理解为预示的类别，以及这些Topoi分类的理论的逻辑地面问题仍然开放。我们表明，SGDT的几种重要的Topos模型对非常简单的几何理论进行了分类，并且可以根据约翰斯通（Johnstone）引起的较低的bagtopos构造维克斯（Vickers and vickers）的较低形式的多种形式的多形的守卫递归。我们通过将多锁守卫递归的通用性能作为一种模块化结构来促进SGDT的合并，该模块化构造适用于任何单盘守卫递归的TOPOS模型。
Several different topoi have played an important role in the development and applications of synthetic guarded domain theory (SGDT), a new kind of synthetic domain theory that abstracts the concept of guarded recursion frequently employed in the semantics of programming languages. In order to unify the accounts of guarded recursion and coinduction, several authors have enriched SGDT with multiple "clocks" parameterizing different time-streams, leading to more complex and difficult to understand topos models. Until now these topoi have been understood very concretely qua categories of presheaves, and the logico-geometrical question of what theories these topoi classify has remained open. We show that several important topos models of SGDT classify very simple geometric theories, and that the passage to various forms of multi-clock guarded recursion can be rephrased more compositionally in terms of the lower bagtopos construction of Vickers and variations thereon due to Johnstone. We contribute to the consolidation of SGDT by isolating the universal property of multi-clock guarded recursion as a modular construction that applies to any topos model of single-clock guarded recursion.
