滴答作为依赖的右伴随：基于时钟类型论的指称语义
摘要：Clocked Type Theory (CloTT)的一种类型理论被用于受限递归，对于使用共归类型进行编程是有用的，允许将生产率编码到类型中，并且使用一种抽象的步骤索引来推理关于高级编程语言功能的问题。先前已经证明CloTT具有许多句法属性，包括强规范性、规范性和等式理论的可决定性。在本文中，我们提出了CloTT的一种指称语义，用于研究CloTT的未来扩展，如路径类型的构造。 构建该模型的主要挑战是对在CloTT中用于关于共归类型的共归推理的时钟上的勾记概念进行建模。我们借鉴了先前用于多个时钟模型受限递归的范畴。在这个范畴中，有一个时钟对象，但没有勾记对象，因此上下文中的勾记假设无法使用标准工具建模。相反，我们使用依赖右伴随函子来建模勾记，这是类别论概念伴随推广到具有家族的范畴的一种方式。依赖右伴随已知可以建模Fitch风格的模态类型，但在CloTT的情况下，模态运算符构成由时钟在类型理论中内部索引的一个家族。我们使用在时钟对象上的切片范畴上的依赖右伴随来建模这个家族。最后，我们展示了如何使用语义替代项来建模CloTT的勾记常量。 这项工作改进了首次两位命名作者的先前模型，这个模型不仅有缺陷，而且更加复杂。
作者：Bassel Mannaa, Rasmus Ejlers M{o}gelberg, Niccol`o Veltri
论文ID：2004.01709
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22