作为CCS的预置层和交互等效的无辜策略（扩展版）
Innocent strategies as presheaves and interactive equivalences for CCS (expanded version)
摘要：
寻求一个一般的框架推理和比较程序设计语言，我们得出一个新的米尔纳的CCS的看法。我们构造了一个“游戏”的范畴E和一个“观点”的子范畴V。我们认为，V上的预层充分代表了“无辜”的策略，在游戏语义的意义上。我们用一个简单的互动概念来装备无辜的策略。然后，我们证明无辜的战略分解结果，并限制到有限序数的预层，证明无辜的战略是一个最终的余代数多项式函子来自游戏。这导致了CCS的递归方程的转换。最后，我们提出了一个概念的“互动等效”无辜的战略，这是接近的精神Beffara的解释测试等价的并发理论。在这个框架中，我们考虑公平测试和必须测试的类似物。我们表明，必须测试是严格精细的，在我们的模型比CCS，因为它避免了我们所谓的“空间不公平”。尽管如此，它不同于公平测试，我们表明，它符合一个宽松的形式的公平测试。
英文摘要：
Seeking a general framework for reasoning about and comparing programming languages, we derive a new view of Milner's CCS. We construct a category E of 'plays', and a subcategory V of 'views'. We argue that presheaves on V adequately represent 'innocent' strategies, in the sense of game semantics. We equip innocent strategies with a simple notion of interaction. We then prove decomposition results for innocent strategies, and, restricting to presheaves of finite ordinals, prove that innocent strategies are a final coalgebra for a polynomial functor derived from the game. This leads to a translation of CCS with recursive equations. Finally, we propose a notion of 'interactive equivalence' for innocent strategies, which is close in spirit to Beffara's interpretation of testing equivalences in concurrency theory. In this framework, we consider analogues of fair testing and must testing. We show that must testing is strictly finer in our model than in CCS, since it avoids what we call 'spatial unfairness'. Still, it differs from fair testing, and we show that it coincides with a relaxed form of fair testing.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
