普适过程演算：不同层次上的进程模型与普适计算的理论基础

理论计算机科学电子笔记162（2006）255-259www.elsevier.com/locate/entcs普适过程演算罗宾·米尔纳英国剑桥大学计算机摘要具有不同签名和反应规则的进程演算可以为普适计算提供理论基础。保留字：二图，图重写，移动代理，普适计算，进程演算。如果我们想对普适计算建模，进程演算需要分支吗？我相信是这样的;我们不能期望一个固定的小原语集可以为所有事情工作。这已经在局部性和移动性（例如卢卡·卡德利和安迪·戈登的移动环境）以及连续动态（例如比尔·朗兹的Φ-演算）中表现出来。一般来说，当我们试图决定哪种行为是原始的时，它就会出现;这取决于我们的目的。在生物学中应用过程演算的研究人员发现，他们需要的原语取决于所需的动作粒度;例如，在一个水平上，细胞对一种分子的摄取是一个单一的离散行为，但在较低水平上，它是一个连续的过程。同样的事情也发生在普适计算中。例如，在有感知的建筑物中，移动代理进入房间在一个级别上是单个动作，但在较低级别上它是复杂的（涉及钥匙，行走等）;并且房间中的计算机然后可以在单个宏动作中感知和登录代理，涉及较低级别的详细因此，我们需要一个建模框架，它包含不同层次上的过程演算;较低层次演算的实现（或实现）应该是演算的一种态射。这就是双图形框架的目的.我希望这些态射将与由托尼·霍尔（Tony Hoare）和他在牛津的同事们多年来发展的精化概念相协调。然后一个重要的结果可能是一种在不同层次上除了这种1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.112256R. Milner/Electronic Notes in Theoretical Computer Science 162（2006）255B一一一一CCCRRRGyzHxFig. 1. 有感觉的建筑物：结构。偶图G是一个大系统的一个子系统，它有两个部分，这两个部分在整个系统中可能是分离的。 H是一个宿主系统;一个上下文，它的洞（灰色矩形）可以被G的部分占据，形成一个更大的系统。 复合系统H G如图2所示。在我们熟悉的协调语言中。我正在与哥本哈根国际电联的一个团队合作，该团队由Lars Birkedal和Thomas领导希尔德布兰特， http://www.itu.dk/research/theory/bpl。 我们我希望能从bigraph模型中衍生出一种Bigraphical Programming Language（BPL）。然后，普适系统的工程师可能会发现自己用一种易于分析的语言编程，因为它在理论上是可以理解的，尽管他们需要不知道理论。这就是ALGOL 60、逻辑编程和函数式编程所追求的;在普适计算的无政府主义世界里，没有理由不追求它。在现实世界的信息系统中，特别是在普适系统中，越来越需要以移动环境的风格来处理局部，并且同样地以CSP，CCS或π演算的通道的风格来处理系统的连接性，因此产生了双图模型此外，（1）连接性和地点可能是真实的或虚拟的，（2）它们应该彼此独立地对待（你在哪里并不影响你可以与谁交谈），（3）流动性只是对这两种结构的重新配置。区分双图的不是这两种结构的细节，而是它们的正交处理。本文的其余部分展示了双图如何捕捉渗透计算的现象，以及它们如何直接表示熟悉的进程演算首先，考虑一种包含房间R的有知觉的建筑物B。每个房间都包含一台计算机C，它也是一个传感器，所有这些计算机都连接在建筑物的基础设施上。代理A可以占据建筑物，在房间内或房间外;他们携带设备-例如电话-允许他们彼此通信;在这些设备的帮助下，他们也可以被房间中的任何计算机感测和登录。图1显示了一个代表这样的实体系统的偶图G;G的左边部分有一个带有房间和代理的建筑物，而右边部分有一个单独的房间，它可能完全在其他地方，和一个单独的代理。节点的嵌套表示局部性，而细长的链接表示连通性。G的一B一RCyzR. Milner/Electronic Notes in Theoretical Computer Science 162（2006）255257一R一C一C一RF =HGxxxxx图二. 有感觉的建筑：动力学。F=HG表示图1中插入宿主H的偶图G。 注意G的“外部”名称是如何与H的“内部”名称联系起来的。 上图显示了F变成F J的反应;代理A进入房间R，然后它被感知并登录到位于那里的计算机C。 下面显示了诱导这种反应的两个简单反应规则;一个代表进入房间，另一个代表感知和登录。另一个链接连接大楼G的区域的数目这些接口是对称monoidal范畴中的对象，其箭头是双图。一般来说，箭头是一个上下文;它不仅有一个外面，就像G一样，而且还有一个非平凡的内部面，决定了它可以与之组成的双图（即，那些可以占据上下文的因此H：J→K是这样一个上下文，其中K=101，{x} 102。G的内面是平凡面I=100，100;这样的偶图称为基。 以形成组合物 F=H<$G，如图2的上图所示，我们将G的部分插入H的孔中，然后连接同名链接（一个用于y，一个用于z）并删除它们的名称。动力学是由一个反应关系的基础双图，产生了一套反应规则，这可能会有所不同，从一个应用到另一个。的确，BB一一一R一一CCCCRRRFJXBB一一一一CCR一CCRRR258R. Milner/Electronic Notes in Theoretical Computer Science 162（2006）255双图的每个应用，称为双图反应系统（BRS），由指定一组控制（如B，R，.. .），每个都具有一些属性，以及这些属性控制的一组反应规则。图2的下半部分显示了两个非常简单的感知建筑反应规则;第一个允许智能体进入房间（保持其链接），而第二个允许房间 请注意，规则可以是参数化的;第一个规则中的灰洞代表具有适当接口的任意基偶图。另请注意，第二条规则要求座席和计算机位于同一位置;它不能应用于走廊中的座席和房间中的计算机之间。从一个角度来看，这些规则所表示的动作是非常基本的;在更高的层次上，我们可以认为像“一个代理A在房间R中找到代理B并移动到那里”这样的动作是原始的从另一个角度来看，这两个规则本身就很复杂;例如，进入一个房间可能需要钥匙和步行，而感知和登录可能需要详细的软件。因此，其他BRS可能会将更复杂或不太复杂的活动视为原始活动。例如，如果建筑物的操作系统是用基于π演算的语言编写的，那么我们希望将建筑物的BRS与表示该演算的BRS相Joachim Parrow和其他人使用各种图形模型揭示了π演算背后的地形直觉。用双图表示π-演算也很容易。特别地，并行组合由可链接的节点的位置（表示名称共享）表示。图3给出了编码的概念，其中显示了两个反应规则。第一个代表π演算规则（xz.P+···）|（x（y）.Q+···）dP|Q;它的两个参数（孔）表示P和Q，而另外两个表示被丢弃的被加数（（像y这样的绑定名在双图中有一个自然的处理方法;它们的作用域是位置。）大多数结构同余的公理在双图中成为恒等式，这表明双图忠实于微积分的直觉然而，复制-有时在π演算中用公理表示！PP|！结构全等的P-在双图中最好作为动态规则处理，如图3所示。我和Ole Jensen已经解决了这个编码和原始演算之间的对应关系;详细的故事将出现在他即将发表的博士论文中。这篇笔记只给出了一个关于双图如何工作的粗略概念。它表明，该模型表示的流动性的放置和链接，这些地方和链接可以是物理和虚拟的，以及各种不同的系统（不同的签名和反应）可以协调的双图演算。更细节可以在我的网页www.example.com上找到http://www.cl.cam.ac.uk/users/rm135，它提供了关于双图的论文的链接。到目前为止，这些文章集中在尽可能多地恢复双图中已知演算的理论理论已恢复为π演算，移动环境，CCS，Petri网R. Milner/Electronic Notes in Theoretical Computer Science 162（2006）255259y02！00分！0Zx图三.π演算的两个反应规则。 第一个代表通信;控件send、get和alt代表发送、接收和求和。孔的标签显示哪些参数被丢弃。 在双图中，复制最好用一个动态规则来表示，使用控件'！';这里的标签显示参数是重复的。和λ演算;这些工作的大部分都是从反应规则中统一推导这一推导是与杰米·莱弗（Jamey Leifer）一起完成的，它以一种新颖的方式利用了范畴论这类工作的另外两种方法值得一提。一个是基于Hartmut Ehrig及其同事在20世纪70年代提出的双推出构造的长期存在的图重写理论这项工作是基于以图形为对象、以嵌入为箭头的类别。在双图中，我们更喜欢图作为箭头，接口作为对象，因为它严格遵循进程演算的代数传统。但这两种方法之间有着密切的联系。同样，也有密切的联系，与方法的弗拉迪Sassone和帕维尔Sobocinski，基于2类。这两种方法是相辅相成的;目前正在研究哪种方法最适合不同的目的。在实践方面，我们将尝试在应用程序中使用双图，特别是在编程语言中。如果发现一种基于这种拓扑模型的语言便于指定和编程普适计算系统，那么它可以极大地促进它们的科学解释。考虑到这些系统的复杂性，以及它们将渗透到我们生活中的亲密性，这种严格的理解是最重要的。zXalt0发送1得到alty23