通过函子的交替不动点实现 Büchi 与奇偶性条件的范畴化
计算机科学中的逻辑
2018-03-20 v1
摘要
对递归数据结构及其相关推理原则的范畴研究大多集中于两个极端：初始代数与归纳，以及最终余代数与余归纳。本文研究其间的情形。我们利用类似于自由单子构造的方式形式化了函子的交替不动点概念。我们发现它们在 Büchi 与奇偶性接受条件下接受运行树的范畴建模中有用。该建模抽象掉了自动机的状态；因此可被视为具有 Büchi 或奇偶性条件的系统的“行为”，其方式遵循余代数系统行为建模的传统。
引用
@article{arxiv.1803.06811,
title = {Categorical Buechi and Parity Conditions via Alternating Fixed Points of Functors},
author = {Natsuki Urabe and Ichiro Hasuo},
journal= {arXiv preprint arXiv:1803.06811},
year = {2018}
}