π-演算的开放性与名称理论的关系

理论计算机科学电子笔记141（2005）49-67www.elsevier.com/locate/entcs一个相应的高阶微积分L.G.梅雷迪思1首席技术官，DjinnisysCorporation 505 N72nd St，Seattle，WA 98103Matthias Radestock2LShift有限公司6 Rufus St，London N1 6PE摘要π-演算不是一个封闭的理论，而是一个依赖于名称理论的理论。从操作的角度来看，人们可以把π演算看作是一个过程，当交给一个名称理论时，它提供了一个通过这些名称进行通信的过程理论。这种理论的开放性已经在π演算实现中得到了利用，其中辅助机制提供了一种解释名称的方法，例如作为tcp/ip端口。 但是，从根本上说，人们可能会问，是否存在一种封闭的过程理论，即名称理论产生于过程理论并完全由过程理论决定的过程理论。在这里，我们提出了这样一个理论的异步消息传递演算的形式上的引用的概念。名称是被引用的进程，因此代表了进程的代码，是作为进程操作对象的进程语法结构的具体化。在此设置中，名称传递成为将进程代码作为消息传递的一种方式。在存在解引用操作的情况下，将流程的代码转换为运行实例，这种机制在不引入流程变量的情况下产生高阶特征。作为高阶演算的标准，复制和/或递归不再需要作为原始操作。更有趣的是，引入一个进程构造器来动态地将进程转换为它的代码，这对于获得计算完整性是必不可少的，同时也取代了ν运算符的功能。事实上，我们可以将ν运算符的复合编码到一个以动态引用和反引用为特征的演算中保留字： 并发，消息传递，进程演算，反射1lgreg. gmail.com2matthias@lshift.net1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.05.01650L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）1介绍π-演算（[10]）不是一个封闭的理论，而是一个依赖于名称理论的理论。从操作的角度来看，人们可以把π演算看作是一个过程，当交给一个名称理论时，它提供了一个通过这些名称进行通信的过程理论的这种开放性已经在π演算实现中得到了利用，例如Microsoft的Biztalk [8 ]中的执行名称可以是TCP/IP端口或URL或对象引用等。但是，从根本上说，人们可能会问，是否存在一个封闭的过程理论，即：在这种理论中，名称理论产生于过程理论，并完全由过程理论决定在这个问题的背后，还隐藏着一大堆其他令人兴奋的、可能具有启发性的问题，这些问题涉及名称与结构在相互作用演算中的作用，以及名称的结构与过程的结构之间的换句话说，在计算机科学家可用的工具中，没有一个地方存在可数无限的原子实体集。所有这样的集合，例如自然数，某些字母表上有限长的字符串的集合，等等，从有限的表示中生成，因此这些集合的元素从生成过程中继承结构作为一个专注于从这样一个集合构建的过程理论的某些方面的理论家，人们可能会暂时忘记这个结构，但它仍然存在，并且在人们试图构建这些演算的可执行为了说明这一点，当名称具有结构时，名称相等就变成了一种计算。但是，如果我们的相互作用理论要为计算理论提供基础，那么这种计算当然也必须考虑在内此外，这些基于名字的、可移动的相互作用演算的任何实现都必须掌握具有结构的名字，这一事实回避了一个问题：如果相互作用的理论解释包括对名字结构和过程结构之间关系的解释，那么它作为理论本身和实施指南是否会更1.1概述和贡献在这里，我们提出了一个理论的异步消息传递演算建立在引用的概念。名字是被引用的过程，因此代表了一个过程的代码，一个过程的句法结构的具体化（直到某种等价）。名称传递，然后成为一种传递进程代码作为消息的方式在存在反引号操作的情况下，将流程的代码转换为运行实例，这种机制产生更高阶的L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）51特性，而不引入过程变量。作为高阶演算的标准，复制和/或递归不再需要作为原始操作。更有趣的是，引入一个进程构造器来动态地将进程转换为它的代码，这对于获得计算完整性是必不可少的，同时也取代了ν运算符的功能。事实上，我们在演算中给出了ν算子的复合编码，基本上使用了动态引用和反引用。遵循Smith和des Rivieres开创的传统，[3]我们将这种将运行代码转换为数据并再次返回的能力称为反射;因此，名称为反射，高-阶演算，或rho-calculus，简称为ρ-演算当然，本文提出了一个具体的演算，可用于模拟各种计算，并强调了一些有趣的phenemona在这些计算。我们认为，然而，主要的贡献是，微积分提供了一种工具，使生活中的一系列问题的作用，名称的相互作用演算这些问题包括名称相等的计算作为一个计算中考虑的框架内的互动和角色的名称相等的替代与同步。然而，如果没有手中的仪器，这些问题就不会真正出现。所以，我们立即转向微积分的介绍。2微积分2.0.1符号我们让P、Q、R在进程上进行范围划分，让x、y、z在名称上进行范围划分ρ-演算P，Q：：= 0零过程|x（y）.P输入|P|升降机|⟩lift||P|Q个并行x，y：：=P52L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）2.0.2引用我们以自下而上的方式工作，从名字开始。在名称理论中，对应于π演算我们从异步移动进程演算的更标准表示出发的第一个出发点是这里。语言术语的语法将包括语法中名称的产生式名字是一个事实，P2.0.3平行此构造函数是通常的并行组合，表示组合进程的并发2.0.4升降尽管名称是由进程（的代码）构建的，但我们仍然在进程和名称之间保持谨慎的区分;因此，名称构造不是进程构造。因此，如果希望能够从给定的进程中生成一个名称，则必须有一个用于从进程中创建名称的术语的进程构造器 这就是生产的动机x|P|他在这里被称为电梯操作员。该术语的直观含义是，过程P将被打包为它的代码P '，并引入这个操作符的更正式的动机将在后续中变得清晰。但是，现在可以说P在ρ-演算中，替换并不会在引号之间替换进程 另一方面，x|P|引用容易被替换，因此构成了一种动态的引用形式，因为最终引用的过程主体将根据x引用的上下文而不同。|P|出现错误表达式。当然，当一个名称是一个引用的过程时，使用一个验证字符串是非常方便的。这样，x操作员我们说“最终”是因为只有当引用的过程被替换到这个表达式中时，这种提取才会发生。这一点的一个后果是，必须在输入前缀下确定一种说法是，如果你想完成某件事，有时你需要说出一个名字，但它应该是你认识的代理人的名字。L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）53注2.1电梯操作员所起的作用类似于（ν x）P。正如在介绍中提到的，它是必不可少的计算的完整性的演算，在实现复制的关键作用它也为ν算子的复合编码提供了一个基本成分注2.2众所周知，在高阶进程代数中不需要复制[13]。虽然我们的代数不是传统意义上的高阶（没有与名称不同类型的正式过程变量），但它具有高阶过程代数的所有特征因此，事实证明，不需要递归术语。为了说明这一点，我们在下面提出了一个编码！在微积分中直观地说，这将相当于接收一个过程的引用形式，评估它，同时使引用形式再次可用。熟悉λ-演算的读者会注意到编码中的关键项和悖论组合子之间的形式相似性[1]。2.0.5输入和输出输入构造函数是异步名称传递演算的标准。输入阻止它的继续执行，直到它收到一个通信。Lift是一种输出形式，因为演算是异步的，所以不允许继续。它也是一种方便的语法糖，我们在这里定义。x[y] x|'y|⟩2.0.6null进程正如我们将在下面看到的，空过程在这个演算中有一个更突出的角色。它提供了唯一的原子，所有其他过程（以及它们使用的名称）都是以同样的方式出现的，数字0是构造自然数的唯一数字;或者空集是ZF集合论中所有集合的唯一集合;或者空博弈是康威博弈与数字理论中所有博弈的唯一博弈在我们看来，与这些其他理论的类比引起了对引言中提出的关于相互作用演算设计的基本问题的2.1名称游戏在介绍移动进程演算的一些更标准的特性，自由名称的计算，结构等价等之前，我们希望考虑一些过程和名称的例子。特别是，如果进程54L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）名字是由名字组成的，而名字又是由过程组成的，那么有没有可能取得成功呢？幸运的是，有一个进程的构造不涉及名称，即空进程0。因为我们至少有一个进程，所以我们可以在1' 3处创建信任 使用一个名称，我们现在可以构造至少两个新进程，它们在语法上明显不同于0，即0' [ 0 ' ]和0 '（0'）。0的情况。正如我们所理解的，这些过程的直观操作解释也不同于完整的过程。假设第一步在通道10 '上输出名称0'，则普通π演算过程x [ x ]在通道x上输出名称x，并且在通道10 '上输出经编码的输入，就像普通π演算过程x（x）一样。通道x上的0个输入。当然，现在我们有了两个进程，我们有了两个名字，0“[0”]“和0”（0“）。0将这三个名称作为我们的disposa，我们可以构建一个全新的进程供应，这些进程生成一个新的名称供应，我们但是，应该指出的是，一旦我们有了空进程，我们也有了0 |0和0 |0 |0，因此，我们的名称为0|0'，和d0|0|0'，和但是，自从我们开始你希望把这些组合看作是写空进程的其他方式，而不是与它区分开，我们是否应该承认这些进程的代码与0'不同？这个问题引出了几个有趣的、显然是基本的问题。首先，如果名称具有结构，不管这是来自过程的结构还是其他什么，什么是名称的合理平等概念为了确定名字上的平等，应该进行多少计算此外，在过程演算中，名称平等应该扮演什么角色？在构造这个演算的过程中，我们意识到替换和同步确定了名字相等在名字传递演算中扮演的两个潜在的非常在一个可行的和有效的理论中，它们可能通过非常不同的机制我们有一个选择，但这只是无限多的设计选择之一。最有可能的是，这个建议的主要价值是提出这个问题。同样，我们提出了一个关于计算名字相等的建议，这只是许多建议之一，其真正目的是使问题生动起来。我们希望带着这些问题转向微积分的核心力学。3pun gratefully accepted;-）L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）552.2自由名和绑定名语法的选择使得名称的绑定实例夹在圆括号（·）之间。因此，进程P的自由名的计算，记为FN（P），递归地给出如下：FN（0）=0FN（x（y）.P）={x}<$（FN（P）\{y}）FN（x）|P|）={x}FN（P|Q）= FN（P）FN（在一个过程P中x的出现是有界的，如果它不是自由的。在一个进程中出现的名称集合（绑定或自由）用N（P）表示。2.3结构叠合过程的结构全等，记为α，是满足下列定律的包含α-等价的最小全等P|0 P 0 |PP |QQ|P（P|Q）|RP|（Q|右）2.4名称等价现在我们来谈谈这种微积分的第一个真正微妙之处。进程自由名的计算和进程间结构一致性的确定都关键地依赖于能否确定两个进程名是否相等。例如，在计算输入保护进程的自由名的情况下，为了删除绑定名，我们必须确定它是否在延续的自由名集合中同样地，结构全等也包括α-等价。但是，建立过程x（z）之间的α-等价。 w|y[z]|和x（v）。 w|y[v]|例如，求x（v）需要计算一个替换，例如x（v）。 w|y[v]|{z/v}。但是这种计算反过来又要求能够确定两个名称是否相等，在这种情况下，输出的对象位置中的名称和被替换的名称如将看到的，名称上的相等涉及过程上的结构相等，这又涉及字母相等，这涉及名称相等。这是一个微妙的相互递归，但结果证明是有根据的。在介绍技术细节之前，读者可能会注意到，上面的语法强制在引号和过程之间进行严格的交替56L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）^{z/y}建筑师。每一个关于过程的问题，如果涉及到一个关于名称的问题，可能又会涉及到一个关于过程的问题，但是下一级过程中的名称，换句话说，每一次让我们假设我们有一个关于（句法）替代和α-等价的说明，我们可以依赖于它来表述名称等价的概念，然后从那里引导我们的替代和α-等价的概念我们取名字等价，写作N，是由以下规则生成的最小等价’（QUOTE-DROP）PQP（结构-E qUIV）2.5句法替换现在我们建立α-等价所使用的替换我们用Proc来表示过程的集合，用Proc'来表示名称的集合，通过以下等式，可以使等式：Proc→Proc(0){Q^（R）|S）{Q^' / P ' } =（R）{ Q ^ ' / P '}|（S）{Q^' / P '}（x（y）. R）{Q'/P'}=（x）{Q'/P'}（z）。（（R^）{Q^' / P ' }）（x =0|R|（X）{Q^' / P ' } =（X）{ Q ' / P '}|R{Q^' / P '}|⟩（"哪里（x）{Q我也⎧⎨Q否则，z是P'，Q '，Q中的自由名和R中的所有名字的区别我们的α-等价将通过这个替换以标准的方式建立。L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）57^^联系我们但是，给定这些相互递归，问题是是否计算<$N（分别是，<$N，<$α）终止。为了回答这个问题，我们需要将我们关于名称x的引用级别或引用深度#（x）的直觉形式化如下。#（P#（P）=max{#（x）：x∈N（P）}N（P）/=0.00否则该算法保证了t#（P'）是有界的. 然后，N（分别为2.6动态报价：示例对即将发生的事情有所预期{u/z}，为了遵循流程的持续性，|y[z]|n和w[y[z]' ]。w|y[z]|{u/z}=w|y[u]| ⟩w[y[z]由于引号之间的过程主体不受submitting的影响，因此我们得到了完全不同的答案。事实上，通过检查输入上下文中的第一个过程，例如x（z）。w|y[z]|因此，我们可以看到，在提升操作符下的进程可能是由在其中绑定名称的前缀输入来塑造的。从这个意义上说，提升操作符将被视为一种在将进程具体化为名称之前动态构造进程的方法。2.7语义替代在α等价中使用的替换实际上只是一种形式上承认绑定出现不依赖于具体名称的手段。它不是计算的引擎这里的建议是，虽然同步是该引擎的驱动程序，但真正的计算引擎是一个语义上的替换概念，它将删除的名称识别为运行进程的请求。哪个过程？为什么那个代码被绑定到名字上的人被删除了。从形式上讲，这相当于一个替代的概念，从应用中的语法替代到删除的名称。（QxNP我也在本文的其余部分，我们将参考语义和句法58L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）{y/x}替换仅仅是替换，并且依赖于上下文来区分哪个是意思。类似地，我们将滥用记号，将^ 写成{y/x}。最后配备这些标准功能，我们可以提出的动力学的演算。2.8操作语义ρ-演算的归约规则是x0Nx1x0|Q|⟩|x1（y）。 P→P{Q（COMM）此外，我们还有以下上下文规则：P→PJP|Q → P J|Q（PAR）P<$PjPJ→QJQJ<$Q P→Q（方程式UIV）上下文规则是完全标准的，我们在这里不多说。通信规则做了承诺的事情，即使代理可以同步和通信打包为名称的进程。例如，使用命名规则和名称等价，我们现在可以证明输出的语法糖是正确的。x [z]|x（y）.P=x|'z|⟩|x（y）。 P→P{P{z/y}但是，它也提供了一个方案，可以识别名称相等在同步中的作用。名称与结构之间还有其他关系例如，考虑一个与上面介绍的微积分相同的微积分，但是具有另一种控制通信的规则。L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）59你好[P通道|Q通道→R] R→ 0Qch anne l'ches|Q|⟩|PCH ANNE L'（Y）. P→P{Q（COMM-湮灭）直观地说，一对过程，P通道，Q通道的代码，在通道/共通道关系中，当过程的组成最终总是减少到0时，也就是说，当过程相互湮灭时这条规则是有根据的，因为观察到，|0，0个|0→100。 因此，0的存在是因为它本身的共同渠道。类似于从0开始的名称的生成，使用一个这样的通道/共通道对，我们可以找到许多这样的对。关于这一规则，我们希望指出的是，我们可以精确地看到从相互作用理论导出的信道/同信道关系的计算我们不知道名字相等的计算是否也有类似的表现，这就揭示了这两个角色在相互作用演算中的潜在差异我们提到，作为一个简短的旁白，没有理由为什么0在上面的方案我们构造了一个由一组过程索引的演算族{Sα}，并且仅在它们的通信规则中进行区分，每个通信规则都符合下面的方案。你好[P通道|Q通道→R] R →RJ<$SαQch anne l'ches|Q|⟩|PCH ANNE L'（Y）. P→P{Q（COMM-湮没-S）我们探讨这个家庭的结石在即将举行的文件。然而，对于本文的其余部分，我们将注意力限制在具有较少外来通信规则的微积分上，根据该系统使用→进行归约，并使用kr进行→kr。3复制如前所述，复制（以及递归）可以在高阶进程代数中实现。作为我们用迄今为止所介绍的机器进行计算的第一个例子，我们在ρ演算中明确地给出了D（x）x（y）。 （x[y]|'y）！P（x）x|D（x）|P |⟩ |D（x）60L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）！P（x）=x|（x（y）. （x[y]|（y））|P|⟩|x（y）。 （x[y]|'y）→（x[y]|'y）{（x（y）. （'y|x[y]））|P' / y}=x[（x（y）. （x[y]|（y））|P'] |（x（y）. （x[y]|（y））|P→……→ BVP|P|. . . ...这是什么？当然，这种编码，作为一种实现，会失控，展开！P急。一个更懒惰和更可实现的复制操作符，仅限于输入保护进程，可以如下获得。！u（v）.Px|u（v）. （D（x））|P）|⟩ |D（x）值得注意的是，提升算子是获得计算完备性的必要条件。一个类似的演算只配备了一个静态的报价享有的计算表示至少相当于上下文无关的语法，但缺乏上下文敏感。这一事实在即将发表的关于ρ演算的类型系统的论文4互模拟在将限制的概念从语言中移除之后，我们小心地将其放回观察的概念中，从而放回程序平等的概念也就是说，我们通过一组名称来参数化倒钩互模拟的概念，我们可以在这些名称上设置倒钩。这种选择的动机实际上是与其他结石进行比较。ρ-演算的名字集合是全局的。在过程语法中，不可能防止术语被置于可能观察到通信的上下文中因此，我们提供了一个地方，推理这种限制的观察范围的互模拟理论。定义4.1在一组名称N上的观察关系↓N是满足以下规则的最小关系。y∈ N，x<$Nyx[v] ↓Nx（OUT-倒钩）P↓Nx或Q↓NxP|Q↓Nx（PAR-倒钩）我们写P<$Nx，如果存在Q使得P<$Q和Q↓Nx。L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）61注意x（y）.P没有倒钩。事实上，在ρ演算和其他异步演算中，观察者没有直接的方法来检测发送的消息是否被接收到。定义4.2在一组名称N上的N倒钩互模拟是主体之间的对称二元关系SN，使得PSNQ意味着：(i) 如果P→PJ，则Q<$QJ且PJSNQJ。(ii) 若P↓Nx，则Q<$Nx。.P是与Q的N-倒钩双相似，记为P<$NQ，如果PSNQ对某个N-倒钩互模拟5解释π演算在这里，我们提供了一个编码的纯异步π演算到ρ演算。由于在ρ演算中所有的名字都是全局的，我们在开始处理自由名字时遇到了一个有几种方法可以处理这个问题。一种是坚持把翻译交给一个封闭的程序（在这个程序中，所有的名字要么被输入，要么被限制）。这种选择感觉并不优雅。另一种方法是提供一个环境r：Nπ→Proc然而，维护对环境的更新掩盖了翻译的简单性我们采用第三种选择。为了说明π演算在名称理论中是参数化的，我们建立了一个π演算，其中名称是ρ演算的名称这与使用自然数或URL集作为名称集来构建π演算没有什么不同正如π演算中这类名称的结构与过程的结构之间没有联系一样，理论所用名称中引用的过程与理论所产生的过程之间也没有联系，我们利用了这一事实。62L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）5.1π演算更正式地说，π-演算P，Q：：= 0|x[y]|x（y）.P|（ν x）P|P|Q|！Px，y：：=x，y∈Proc注意：名字是引用的ρ-演算过程。5.2结构叠合定义5.1进程之间的结构同余，，是相对于α-重命名封闭的最小同余，满足平行的阿贝尔幺半群定律（结合性，交换性和0作为单位元），以及以下公理：(i) 范围法：（ν x）0< $0，（ν x）（ν x）P<$（ν x）P，（ν x）（ν y）P（ν y）（ν x）P，P|（ν x）Q（ν x）P| Q，如果x/∈ FN（P）(ii) 递归法则：！PP|！P(iii) 名称等价定律：P<$P{x/y}，如果x<$Ny5.3操作语义操作语义是标准的。x [z]|x（y）.P→P {z/y}（COMM）L.G. 梅雷迪思，M。Radestock/Electronic Notes in Theoretical Computer Science 141（2005）63此外，我们还有以下上下文规则：P→PJP|Q → P J|Q（PAR）P→PJ（ν x）P→（νx）PJ（新）P<$PjPJ→QJQJ<$Q P→Q（方程式UIV）同样，我们将→写成，并依靠上下文来区分→在π演算中何时意味着归约，在ρ演算中何时意味着归约。π演算过程的集合将用Procπ表示。5.4翻译该转换将由函数给出，[−]]（−，−） ：Procπ×ProcProc指导思想是，我们沿着一个分布式内存分配器的边创建，进程对它的访问是通过函数的第二个参数进行调解的第一个参数决定给定分配器的内存形状给定一个过程P，我们选择n和p，使得n p和不同于以P的名字命名。F或example，n=<$m∈FN （P）m[0' ] '且p =

下载后可阅读完整内容，剩余1页未读，立即下载