Abstract GSOS Rules and a Modular Treatment of Recursive Definitions
Abstract GSOS Rules and a Modular Treatment of Recursive Definitions
复制标题
抽象 GSOS 规则和递归定义的模块化处理
DOI：
10.2168/lmcs-9(3:28)2013
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
D. Schwencke
中科院分区：
文献类型：
--
作者：
Stefan Milius;L. Moss;D. Schwencke
函子的末端膜膜充当各种类型的州基系统的语义域。例如，CCS过程，流，无限的树，形式语言和非孔子基景的行为形成了终端结构。我们通过结合两个想法来介绍终端山地递归定义语义的统一说明：（1）摘要GSOS规则l指定终端山地上的其他代数操作； （2）末端结构也是最初完全迭代的代数（CIAS）。我们还表明，一项抽象的GSO规则会导致末端山地上的新扩展中央情报局结构。然后，我们将涉及L指定为L的递归程序方案给定的操作的递归函数定义形式化，我们证明了扩展的CIA中存在独特的解决方案。从我们的结果中可以得出结论，在终端结构膜中的递归（功能）定义的解决方案可用于随后具有独特解决方案的递归定义。我们称此原理模块化。我们通过上述五个混凝土终端煤层（例如，有限的流电路定义了独特的流函数）来说明我们的结果。
Terminal coalgebras for a functor serve as semantic domains for state-based systems of various types. For example, behaviors of CCS processes, streams, infinite trees, formal languages and non-well-founded sets form terminal coalgebras. We present a uniform account of the semantics of recursive definitions in terminal coalgebras by combining two ideas: (1) abstract GSOS rules l specify additional algebraic operations on a terminal coalgebra; (2) terminal coalgebras are also initial completely iterative algebras (cias). We also show that an abstract GSOS rule leads to new extended cia structures on the terminal coalgebra. Then we formalize recursive function definitions involving given operations specified by l as recursive program schemes for l, and we prove that unique solutions exist in the extended cias. From our results it follows that the solutions of recursive (function) definitions in terminal coalgebras may be used in subsequent recursive definitions which still have unique solutions. We call this principle modularity. We illustrate our results by the five concrete terminal coalgebras mentioned above, e.\,g., a finite stream circuit defines a unique stream function.