一句话：为 CloTT 给出指称语义，用依赖右伴随在切片范畴中建模时钟滴答，并修复此前有缺陷的模型。
CloTT 是一种用于守卫递归的类型理论，可把共归纳类型的生产率编码进类型，并支持抽象步进索引推理；此前已有强规范化、典范性与等式可判定性等语法结果。本文为其建立指称语义，核心难点是解释用于共归纳推理的时钟滴答。作者在现有多时钟守卫递归范畴上工作，该范畴有时钟对象却无滴答对象，因此标准工具无法建模 tick 假设。他们使用 categories with families 中的依赖右伴随，并在时钟对象上的切片范畴中建模按时钟内部索引的模态算子族，最后用语义替换解释 tick 常量。该模型修复了前两位作者此前有缺陷且更复杂的模型。
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to enjoy a number of syntactic properties including strong normalisation, canonicity and decidability of the equational theory. In this paper we present a denotational semantics for CloTT useful, e.g., for studying future extensions of CloTT with constructions such as path types. The main challenge for constructing this model is to model the notion of ticks on a clock used in CloTT for coinductive reasoning about coinductive types. We build on a category previously used to model guarded recursion with multiple clocks. In this category there is an object of clocks but no object of ticks, and so tick-assumptions in a context can not be modelled using standard tools. Instead we model ticks using dependent right adjoint functors, a generalisation of the category theoretic notion of adjunction to the setting of categories with families. Dependent right adjoints are known to model Fitch-style modal types, but in the case of CloTT, the modal operators constitute a family indexed internally in the type theory by clocks. We model this family using a dependent right adjoint on the slice category over the object of clocks. Finally we show how to model the tick constant of CloTT using a semantic substitution. This work improves on a previous model by the first two named authors which not only had a flaw but was also considerably more complicated.Comment: 31 pages. Second version is a minor revision. arXiv admin note: text overlap with arXiv:1804.06687
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{MannaaMV20,
title = {Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory},
author = {Bassel Mannaa and Rasmus Ejlers Møgelberg and Niccolò Veltri},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 4},
year = {2020},
doi = {10.23638/lmcs-16(4:17)2020}
}