代数处理进程理论的新视角与应用

理论计算机科学电子笔记162（2006）227-231www.elsevier.com/locate/entcs什么是进程理论中的代数？Bas Luttik1荷兰埃因霍温理工大学数学与计算机科学系CWI，阿姆斯特丹，荷兰摘要过程理论开始于20世纪70年代，重点是对其基本概念进行代数处理。在20世纪90年代，随着高级特征（数据、时间、移动性、概率、随机性）的迅速引入，代数线基本上被抛弃了。我相信一个彻底的抽象代数处理为理论增加了一定程度的数学成熟度和优雅性。 在这篇笔记中，我讨论了什么是代数的过程理论，什么不是（尚未）。保留字：进程理论，进程代数，抽象代数。1序言在数学中，有时可以区分两种代数：初等代数和抽象代数。初等代数记录了实数系统的性质，主要是以方程的形式使用符号来表示常数（特定实数）和变量（所有实数）。初等代数是具体的，因为它是关于一种特殊的对象：实数。抽象代数（也被称为现代代数）涉及更一般性的算术基本运算（性质）的研究没有不再只讨论实数的加法，而是讨论任何可能值得加法的一般性通常通过公理化地定义基本运算来实现作为一个公理化定义的例子，考虑一个二元运算理论，它通过假设第一个运算是可交换的、结合的和幂等的，第二个运算从右边分布在第一个运算上，也是结合的来定义。 一个环理论家可能会告诉你，幂等半环理论的一个定义，除了几个公理是1电子邮件：s. p. tue.nl1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.086228B. Luttik/Electronic Notes in Theoretical Computer Science 162（2006）227肯定是失踪了。最值得注意的是，环理论家评论说，应该包括一个公理，该公理表示第二个操作也从第一个操作的左边开始分布。然而，一个过程理论家会认识到，这个公理被故意遗漏了，因为我们在这里所拥有的是过程的交替和顺序组合理论的定义。这个理论的特殊版本是由Bergstra和Klop在1982年提出的（见[4，6]）;他们把它作为一组形式方程。2代数过程论代数过程理论开始于20世纪70什么是CSP和CCS的代数？事实上，重点是研究过程的基本操作CSP和CCS在很大程度上同意这些基本操作是什么，都包括排序，不确定性选择和平行组合。此外，这些构造被证明满足非常相似的性质。CSP和CCS之间的主要区别在于被视为过程概念的适当数学表示：在CSP中，过程在数学上表示为一组故障2，而在CCS中，CCS它是一个元素的集合标记的转换系统模观察等价性定义过程域上的一阶运算语言并证明这些运算的性质是代数的基本含义。通过他们的开创性论文[10]，Hennessy和Milner在一个更抽象的方法的方向，提供了一个地面完整的3方程axiomatisation的观察等价的情况下，递归免费CCS。他们的公理原则上可以被看作是一种抽象的代数定义。一个真正抽象代数方法首先由Bergstra和Klop [4，6]明确提出在引入ACP时，他们的方法论关注之一是“首先提出然后研究其模型[6，p. 112]）。让我尽量避免误解，为什么伯格斯特拉和克洛普的理论是代数意义上的抽象代数。这并不是（至少不仅仅是）它使用等式公理来定义运算的事实。这些方程只是实现抽象代数真正需要的一种手段，抽象代数的真正需要是从所考虑的对象的性质中抽象出来。就像环的数学理论是关于算术而不依赖于数的数学定义一样，Bergstra和Klop[2]失败是一系列事件，在这些事件中，一个过程可能参与其中，但随后拒绝参与其中。3我们称公理化为地完备的，如果任何两个行为等价的闭过程表达式可证明相等。B. Luttik/Electronic Notes in Theoretical Computer Science 162（2006）227229代数学成就在20世纪80年代后半期，过程论中的代数方法受到了相当多的关注。我们简要地提到三类代数结果（见Aceto表达性：获得的几个结果表明，基本过程理论运算的某些组合比其他组合更具表达性。例如，它表明堆栈的行为可以通过使用交替组合和顺序组合的有限递归指定来指定，而如果顺序组合被前缀乘法取代，则这是不可能的[5]。公理性：大量的工作是为过程论运算的某些组合提供令人满意的等式公理系统，并表明对于其他组合不存在令人满意的等式公理系统在这里，“令人满意”通常意味着在某种行为一致性的概念方面是有限的和完全的唯一分解：对于并行组合的几个版本，已经确定每个过程可以唯一地表示为并行素数过程的并行组合，直到某个行为等价。第一个这样的Milner和Moller在[17]中得到了这个结果上面提到的大多数结果都是代数的，就像初等代数是代数的一样：它们记录了定义为基于过程的预定数学模型（通常，标记为转换系统模行为等价）。Moller [18]在他优秀的博士论文中提出的ω-完备性结果可以被认为是一个例外;它们是更抽象的代数，因为它们是关于公理系统本身的质量，不依赖于特定的预定数学模型的过程。在最近的一篇论文[14]中，作者与Vincent van Oostrom一起证明了唯一分解结果的故事可以在交换幺半群的抽象代数设置中重述主要的技术，发现米勒，以证明独特的分解结果在过程理论是一般化沿抽象代数线的抽象代数设置的交换monoid，产生一个完整的axiomatisation类的交换monoid与独特的分解。最大的优点是，为了证明关于某种形式的并行复合的唯一分解，直到某种行为等价，现在可以建立诱导幺半群满足使一般证明通过的公理。尚未代数在20世纪90（一个值得注意的例外是递归操作的工作，见最近的调查[3]）。大部分工艺230B. Luttik/Electronic Notes in Theoretical Computer Science 162（2006）227这些特征的理论处理涉及变量绑定操作的使用。例如，形式化的过程规范语言μCRL[8]将ACP的过程理论操作与抽象数据类型相结合，Σ量化器. 直觉是，如果p（d）是一个形式μCRL表达式，Σ自由变量d在某些数据类型的值范围内，则dp（d）表示对于数据类型的每个值v都有一个被加数p（v这种结构可以用来表示值传递。μCRL的选择量化器和一般的绑定操作不是代数的。 原因是它们依赖于句法性质的定义它们所作用的对象，因为它们应该绑定一个变量，对象回想一下抽象代数的要求：对象的内在本质不应该是重要的。因此，说μCRL是代数的就等于说进程是表达式，当然它在[13]中，有可能提供一种选择量化的抽象代数处理，其方式与代数逻辑中处理存在量化的方式大致相同[9]。3最后我相信，彻底的抽象代数处理将为过程论领域增加一定程度的数学成熟性和优雅性。因此，我认为我们应该进一步发展过程理论的抽象代数方面，通过对高级过程理论概念进行抽象代数处理（例如，流动性，时间，随机），并考虑基本过程理论的结果和结构从代数的角度。引用[1] 阿塞托湖，经典进程代数中我最喜欢的一些结果，金砖国家报告NS-03-2，金砖国家，奥尔堡大学计算机科学系（2003年）。[2] Baeten，J.C. M.，进程代数简史，Theory。Comput. Sci. 335（2005），pp.131-146。[3] Bergstra，J. A.，W. Fokkink和A.庞斯，递归操作的过程代数 ，在：J.A. Bergstra， A. Ponse和S. A.Smolka，编辑，过程代数手册，Elsevier Science Inc.，2001年，pp. 333-389.[4] 伯 格 斯 特 拉 ， J. A. 和 J. W. 郭 文 贵 ， 进 程 代 数 中 的 不 动 点 语 义 ， 技 术 报 告 IW 280 ， 数 学 中 心（1982）。[5] 伯格斯特拉，J. A.和J. W. Klop，递归定义过程的代数和正则过程的代数，在：J. Paredaens，编辑，ICALP82比95[6] 伯格斯特拉，J. A.和J. W. Klop，Process algebra for synchronous communication，Information andControl60（1984），pp. 109-137[7] Brookes，S. D、C. A. R. Hoare和A. W. Roscoe，A theory of communicating sequential processes，J. ACM31（1984），pp. 560-599.[8] Groote，J. F.和A. Ponse，μCRL的语法和语义，在：A.庞斯角Verhoef和S. F. M. van Vlijmen，editors，Algebra of Communicating Processes，Workshops in Computing（1994），pp. 26比62[9] 哈尔莫斯，公共关系，代数逻辑的基本概念，美国数学月刊63（1956），页。363-387.DB. Luttik/Electronic Notes in Theoretical Computer Science 162（2006）227231[10] Hennessy，M.和R. Milner，Algebrafts for nondeterminism and concurrency，J. ACM32（1985），pp.137-161。[11]霍尔角A. R.，通信顺序进程，Commun。ACM21（1978），pp. 666-677。[12] 霍尔角A. R.，“Communicating Sequential Processes,” Series in Computer Science, Prentice-HallInternational, London,[13] Luttik，B.， 论文，阿姆斯特丹大学（2002年），可查阅http://www.win.tue.nl/~luttik。[14] 卢蒂克湾和V. van Oostrom，Decomposition orders-another generalisation of the fundamental theoremof arithmetic，Theoret. Comput. Sci. 335（2005），pp. 147-186[15] 米尔纳河，“A Calculus of Communicating Systems,” LNCS 92, Springer-Verlag, Berlin,[16] 米尔纳河，[17] 米尔纳河和F. Moller，过程的唯一分解，理论计算。 Sci. 107（1993），pp. 357-363.[18] Moller，F.，“并发公理”，博士。毕业论文，爱丁堡大学（1989年）。