初始代数上的纤维化初始代数-最终余代数重合：将验证见证上下颠倒
计算机科学中的逻辑
2021-08-25 v3 计算与语言
摘要
初始代数(IA)与最终余代数(FC)之间的重合是一种支撑理论计算机科学中各种重要结果的现象。在本文中，我们识别了IA-FC重合的一个一般纤维化条件，即基础范畴中初始代数之上的纤维中的条件。将纤维中的(余)代数识别为(余)归纳谓词，我们的纤维化IA-FC重合允许人们使用余归纳见证(如不变式)来验证归纳性质(如活性)。我们的一般纤维化理论以链余极限稳定性的技术条件为特征；我们也将框架扩展到单调子效应存在的情况，限制为完全格值谓词的纤维化。我们范畴理论的实用益处通过针对三个验证问题的新“上下颠倒”见证概念得以例证：概率活性，以及关于自底向上树自动机的接受和模型检测。
引用
@article{arxiv.2105.04817,
title = {Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down},
author = {Mayuko Kori and Ichiro Hasuo and Shin-ya Katsumata},
journal= {arXiv preprint arXiv:2105.04817},
year = {2021}
}
备注
38 pages