通过迭代富集的模态
Modality via Iterated Enrichment
摘要：
本文利用一种新的范畴语义学--基变语义学来研究模态类型论。基变语义是一种新颖的语义，它是基于（可能是无限的）迭代丰富和解释的模态作为homobject。在我们的语义中，多阶段计算中的Meta和对象级别之间的关系正好对应于丰富和丰富类别之间的关系。其结果是，我们获得了Meta和对象逻辑可能完全不同的情况下的分类解释。我们的分类模型包括模态类型论的传统模型（例如，Carnival闭范畴与monoidal endofunctor）作为特殊情况，因此可以看作是一个自然的改进以前的结果。在类型理论方面，它表明，菲奇风格的模态类型论可以直接解释在迭代丰富的类别。有趣的是，这种解释表明，Fitch风格的模态类型论是双上下文演算的右伴随。此外，我们提出了如何线性时间，S4和线性指数形式的变化的基础语义方面的描述。最后，我们表明，基的变化语义可以自然地扩展到多阶段的有效计算和广义上下文模态一la Nanevski et al.我们强调，本文回答了在2011年的调查报告中提出的问题，由德派瓦和Ritter，什么是一个分类模型的Fitch风格的类型论是什么样的。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
