非确定性迭代与测试的统一范畴视角
计算机科学中的逻辑
2024-07-19 v2
摘要
我们研究了范畴语境下的克莱因迭代。克莱因代数(带测试)的一个著名完备结果引入了克莱因代数作为轻量级推理程序等价性的通用工具,然而随后随着对更精细语义需求的响应,诸多该变量的变体陆续涌现,以应对包括状态、并发、异常、混合、分支时间等在内的各种语义特征。我们将克莱因迭代从克莱因代数中分离出来,从范畴学视角进行分析。我们抵达的概念是具有(无限小)范畴(带余积和测试),我们展示其在编程语言特征兼容性方面具有广泛和稳健的意义,例如异常、存储、并发行为等。我们通过各种 yardstick 验证提出的概念,最重要的是,通过表征其自由模型为某类(非确定性)有理树来实现。
引用
@article{arxiv.2407.08688,
title = {A Unifying Categorical View of Nondeterministic Iteration and Tests},
author = {Sergey Goncharov and Tarmo Uustalu},
journal= {arXiv preprint arXiv:2407.08688},
year = {2024}
}
备注
Full version of the CONCUR 2024 paper