守护你的 Daggers 与 Traces：守卫式(共)递归的性质
计算机科学中的逻辑
2018-08-21 v1
摘要
受近期对守卫式(共)递归模型兴趣的推动，我们研究了它们的等式性质。我们为守卫式不动点算子公式化了公理，推广了Bloom和Ésik的迭代理论公理。这些公理的模型既包括标准的（例如基于cpo的）迭代理论模型，也包括守卫式递归模型，如完备度量空间或Birkedal等人研究的树拓扑斯。我们证明了由唯一dagger操作满足所有Conway公理的标准结果推广到了守卫式设定。我们还引入了范畴上的守卫式迹算子的概念，并证明守卫式迹与守卫式不动点算子之间存在一一对应。我们的结果旨在作为迈向未来描述守卫式递归分类理论的第一步，希望如此。
引用
@article{arxiv.1603.05214,
title = {Guard Your Daggers and Traces: Properties of Guarded (Co-)recursion},
author = {Stefan Milius and Tadeusz Litak},
journal= {arXiv preprint arXiv:1603.05214},
year = {2018}
}
备注
invited to a special issue of Fundamenta Informaticae (FiCS'13). arXiv admin note: text overlap with arXiv:1309.0895