Extensional and Intensional Semantic Universes
Extensional and Intensional Semantic Universes
复制标题
外延和内涵语义宇宙
DOI：
10.1145/3209108.3209206
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Blot V
中科院分区：
文献类型：
--
作者：
Blot V
我们描述了一个依赖类型理论，以及它的一个外延模型，它同时包含了内涵和外延的语义宇宙。在前者中，术语和类型被解释为对某些图对策的策略，而后者则被解释为事件域上的稳定函数；具体数据结构本身形成了一个事件域，我们可以用它来解释(外延)宇宙类型的(内涵)类型。一个依赖游戏对应于这个领域中的一个稳定函数；我们使用它的迹来定义依赖积和结构，因为它准确地捕捉到展开的动作与依赖相结合是如何塑造游戏中可能的交互的。由于每个策略都在CDS状态上计算一个稳定的函数，我们可以将类型判断从内涵提升到外延，从而给出了一个递归定义的类型族和类型操作符的表达类型理论；我们定义了内涵术语的操作语义，给出了基于我们的类型理论的函数式编程语言，并证明了它的语义在计算上是充分的。通过在内涵项上推广一个简单的非局域控制算子，我们可以精确地刻画内涵模型中的行为。我们通过证明完全抽象和完全结果来证明这一点。
We describe a dependent type theory, and a denotational model for it, that incorporates both intensional and extensional semantic universes. In the former, terms and types are interpreted as strategies on certain graph games, which are concrete data structures of a generalized form, and in the latter as stable functions on event domains.The concrete data structures themselves form an event domain, with which we may interpret an (extensional) universe type of (intensional) types. A dependent game corresponds to a stable function into this domain; we use its trace to define dependent product and sum constructions as it captures precisely how unfolding moves combine with the dependency to shape the possible interaction in the game. Since each strategy computes a stable function on CDS states, we can lift typing judgements from the intensional to the extensional setting, giving an expressive type theory with recursively defined type families and type operators.We define an operational semantics for intensional terms, giving a functional programming language based on our type theory, and prove that our semantics for it is computationally adequate. By extending it with a simple non-local control operator on intensional terms, we can precisely characterize behaviour in the intensional model. We demonstrate this by proving full abstraction and full completeness results.