抽象 GSOS 规则与递归定义的模块化处理
计算机科学中的逻辑
2015-07-01 v2 范畴论
摘要
函子的终余代数充当各类基于状态系统的语义域。例如，CCS 进程的行为、流、无限树、形式语言和非良基集合都构成终余代数。我们通过结合两个思想，提出了对终余代数中递归定义语义的统一描述：(1) 抽象 GSOS 规则 指定了终余代数上的附加代数运算；(2) 终余代数也是初始完全迭代代数 (cias)。我们还表明，抽象 GSOS 规则会导致终余代数上产生新的扩展 cia 结构。随后，我们将涉及由 指定的给定运算的递归函数定义形式化为 的递归程序方案，并证明了在扩展 cias 中存在唯一解。从我们的结果可以得出，终余代数中递归（函数）定义的解可用于后续的递归定义，且这些后续定义仍具有唯一解。我们将此原则称为模块化。我们通过上述五个具体的终余代数实例说明了我们的结果，例如，一个有限流电路定义了一个唯一的流函数。
引用
@article{arxiv.1307.2538,
title = {Abstract GSOS Rules and a Modular Treatment of Recursive Definitions},
author = {Stefan Milius and Lawrence S Moss and Daniel Schwencke},
journal= {arXiv preprint arXiv:1307.2538},
year = {2015}
}