Modality via Iterated Enrichment
Modality via Iterated Enrichment
复制标题
通过迭代丰富的方式
DOI：
10.1016/j.entcs.2018.11.015
复制
发表时间：
2018
影响因子：
--
通讯作者：
Murase Yuito
中科院分区：
文献类型：
--
作者：
Nishiwaki Yuichi;Kakutani Yoshihiko;Murase Yuito
本文用一种新的范畴语义——基变语义来研究模态类型理论。变换基语义是新颖的，因为它是基于（可能无限地）迭代的丰富和作为本源对象的情态的解释。在我们的语义中，多阶段计算中的元级和对象级之间的关系正好对应于富类和被富类之间的关系。因此，我们获得了元逻辑和对象逻辑可能完全不同的情况的分类解释。我们的范畴模型包括模态类型理论的常规模型（例如，具有单轴内函子的笛卡尔闭范畴）作为特殊情况，因此可以看作是对以前结果的自然改进。在类型理论方面，表明菲奇式模态类型理论可以直接解释为迭代丰富的范畴。有趣的是，这一解释表明，菲奇式模态类型理论是双语境演算的右伴随理论。此外，我们还介绍了如何根据基的变化语义描述线性时间、S4和线性指数模态。最后，我们证明了变换基语义可以自然地扩展到多阶段有效计算和广义上下文情态（la Nanevski等）。我们强调，本文回答了de Paiva和Ritter在2011年的调查论文中提出的问题，即菲氏类型理论的分类模型是什么样的。
This paper investigates modal type theories by using a new categorical semantics called change-of-base semantics. Change-of-base semantics is novel in that it is based on (possibly infinitely) iterated enrichment and interpretation of modality as hom objects. In our semantics, the relationship between meta and object levels in multi-staged computation exactly corresponds to the relationship between enriching and enriched categories. As a result, we obtain a categorical explanation of situations where meta and object logics may be completely different. Our categorical models include conventional models of modal type theory (e.g., cartesian closed categories with a monoidal endofunctor) as special cases and hence can be seen as a natural refinement of former results.On the type theoretical side, it is shown that Fitch-style modal type theory can be directly interpreted in iterated enrichment of categories. Interestingly, this interpretation suggests the fact that Fitch-style modal type theory is the right adjoint of dual-context calculus. In addition, we present how linear temporal, S4, and linear exponential modalities are described in terms of change-of-base semantics. Finally, we show that the change-of-base semantics can be naturally extended to multi-staged effectful computation and generalized contextual modality a la Nanevski et al. We emphasize that this paper answers the question raised in the survey paper by de Paiva and Ritter in 2011, what a categorical model for Fitch-style type theory is like.