局部通信域的分布式π演算

1《理论计算机科学电子札记》41卷第2期（2001年）网址：http://www.elsevier.nl/locate/entcs/volume41.html16页一个具有局部通信域的分布式π演算汤姆·乔西亚和伊恩·斯塔克计算机科学基础实验室信息学系，爱丁堡大学梅菲尔德路，爱丁堡EH9 3JZ，苏格兰，英国{stark，tpcc}@ dcs.ed.ac.uk摘要本文介绍了一个进程演算，旨在捕捉的现象，名称是众所周知的，但总是指本地信息。我们的系统扩展了π演算，使一个通道名称可以在其范围内有几个不相交的局部区域。这种信道名可以用于区域内的通信，也可以在区域之间发送，但它本身不能用于从一个区域向另一个区域发送信息。区域按层次结构排列，例如区分单个应用程序、机器或整个网络。我们给出了一个演算的操作语义，并开发了一个类型系统，保证正确使用的通道在其本地区域。我们举例说明与模型的互联网服务协议和一对分布式代理。1介绍大多数计算机程序都对它们运行的环境做出假设：可用的设施以及如何使用它们。一个C程序员可以自由地使用printf函数，并期望无论在哪里执行他们编译的代码，都会加载一个适当的库来打印格式化的文本。在Web上运行的轻量级小程序的Java模型依赖于每个浏览器支持到大量已知库的标准接口。甚至更动态地，“移动代理”的概念这里的共同主题是使用全球知名的名称来访问本地资源。但是，名字是如何成为全球知名的，什么是当地的？通常，这是一个非常静态和非计算性的问题：用户手册列出了库调用，或者服务在“众所周知”的地址上运行。在本文中，我们提供了一个演算，开始调查的范围之间的相互作用，其中一个名字是已知的和它的运作的局部地区2001年由ElsevierScienceB出版。 V. 操作访问和C CB Y-NC-ND许可证。2我们的系统是基于π演算，它提供了一个既定的框架推理的名称和通信。具体来说，我们使用一个多元的变体（通道携带元组而不是单个值[10]）和异步（输出动作总是成功[3]）。为此，我们添加了几个新的扩展，我们在这里用一个简短的例子来激励它们。π演算背后的一个原始观察结果是，与移动代码相关的许多问题可以通过简单地查看移动名称来研究这里就是这样，我们的例子是指导互联网的服务协议的操作。当一个浏览器连接一个网络服务器来获取一个页面，或者一个人操作手指来列出机器上的用户时，两者都连接到一个编号的“port”在上市当然，这只有在双方都同意的情况下才能起作用;当足够多的系统同意时，端口号就成为在Unix下，文件/etc/services保存一个将数字映射到服务1的列表。还有一个更深层次的间接性：大多数机器只运行一个通用的元服务器inetd，即Internet守护进程，它监听所有端口。当inetd接收到一个连接时，它在/etc/services中查找端口，然后查询第二个文件，该文件标识提供该服务的程序。inetd启动程序并将连接交给调用方。这个过程的π演算模型可能看起来像这样。客户鲤鱼= νc。（派克·芬格，C.|c（x）. printx）我是你的儿子！pik e（s，r）. 四月|！finger（y）. 你好PikeUsers| ! daytim e（z）. zPikeDate系统（鲤鱼|派克）在这里，客户机Carp希望用手指请求联系服务器Pike。客户端有两个组件：第一个传输请求，第二个准备打印结果。ServerPike包括三个复制进程：一个通用Internet守护进程、一个Finger守护进程和一个time-of-day守护进程。Channelpike是服务器计算机的互联网地址，而免费名称finger和daytime则表示众所周知的端口号。在操作中，Carp将其请求发送给Pike，命名为finger服务和应答通道c。Pike上的Internet守护进程通过名为finger的通道重新传输联系人c来处理此问题。Finger守护进程收集这些信息，并将PikeUsers上的信息传递回Carp上的等待进程。这是一个公平的模型，非常符合π演算的风格，但它有一些缺点。因为finger和daytime这两个名字随处可见，即使Pike上的Internet守护进程已经收集了请求，也没有任何保护措施来防止实际处理它的不同服务器上的Finger守护进程-甚至可能是如果我们限制1这通常包括大量的端口号，这些端口号从未变得足够重要。“众所周知”。3如果将finger的作用域设置为主机Pike，那么Carp就无法制定请求，因为它必须知道服务的名称。我们通过扩展π演算的局部区域并为每个通道分配一个操作级别来打破这种Catch-22。我们的系统现在网[宿主[鲤鱼]|主机[派克]]这表示Carp和Pike是驻留在单个网络上的独立主机的事实。系统中的每个名称都被识别为在网络或主机级别运行：c @ net、pike @ net、finger @ host、daytime @ host、print @ host。因此，在手指、白天或印刷信道上的通信只能跨越单个主机，而信道c和pike在整个网络上操作这与v-binding给出的名字的作用域特别是，本例中的finger名称具有很大的作用域，但是不同主机上的相同Finger守护进程永远不会相互干扰。引入级别可以区分单个系统中并发和通信的不同用途。例如，在一个主机内可能有几个应用程序，由应用程序级别的区域表示;或者在主机和网络之间可能有一个子网级别。应用程序中两个线程之间的通信概述在第2节中，我们开发了一个正式的描述，这种局部区域π-演算。我们给出了一个操作语义，并证明它正确地限制通信到适当的局部区域。我们扩大互联网服务的例子，并提出了一个基于代理的编程演算的说明这个操作语义结合了几个动态检查，以确保正确使用通道。在第3节中，我们提出了一个静态捕获这些信息的类型系统。例如，我们的finger通道具有type（string@net）@host;这表明它是一个主机级通道，携带的值本身命名了用于通信字符串的网络级通道我们证明了“良好类型的进程不会出错”，并推断我们可以省略大部分的动态检查的操作语义。论文第四节结束。4\相关工作在早期的工作中，Vivas和Dam [15]研究了π演算中阻塞算子的行为：本质上是CCS限制P a，它阻塞了单个通道a上的通信而没有绑定它。 他们的具体观察是，这打破了桑吉奥吉我们地方和各级的贡献之一是为这种静态限制提供了一个系统的框架。有一系列的项目解决π演算中的位置，与我们当地的一些相似之处。总的来说，他们的目标是复杂的：例如，Sangiorgi研究了使用位置的非交织语义和因果关系[11]，Amadio在分布式中对局部故障进行了系统[1]。 这两者都没有限制通信的范围。为移动代理提出的系统通常使用位置来非常严格地限制通信：代理只能与同一位置的代理交互，并且必须移动才能与其他代理交谈。这是Cardelli和Gordon的移动环境[4]以及Hennessy和Riely [7，6]的系统Dπ的情况分布式系统的方法有时会选择特定的学科进行本地和全球通信。Sewell提出了一个类型系统来区分这些，其中通道要么具有普遍的范围，要么仅限于单个局部区域[14]。Join演算需要定位所有通道：虽然任何人都可以传输数据，但只有单个站点上的选定进程可以接收数据[5]。Sangiorgi使用类型来构造π演算通道的2具有局部面积的π2.1语法微积分是围绕两类标识符构建的：通道a，b，c，x，y，查询，回复，. ∈ Chan以及级别l、m、app、host、net. ∈ Level。频道名称是从一个可数的无限供应，陈。在句法上，它们的行为与π演算完全相同。水平是相当多的约束：我们假设一些有限的和完全有序的集合水平的先验选择。本文中的例子都是用应用程序主机网实现的。在微积分的形式描述中，我们把l和m作为这些层次的元变量。进程由以下语法给出，基于异步5≡|--≡−多元π-演算进程P，Q：：= 0个非活动进程|Q平行合成|Qparallel composition|a¯⟨→b⟩outputtuple|a(→b).Pinput|! a（→b）.P复制输入|l [P]local area at level l|νa@ l.Pfresh channel a at level l大多数都是标准的。最后两个构造是局部区域演算所特有的：因此l[P]表示在局部区域中运行的进程P，其级别为l，而名称绑定νa@l.P指定通道a在哪个级别运行。区域和进程一样，是匿名的;这与位置系统相反，位置系统通常用标识符标记定义2.1施事是任何形式l[P]的过程：即单个封闭区域。通道名称可以在任何进程中绑定或释放。绑定前缀通常是输入的前缀a（→b），！a（→b）和限制νa@l. 我们写fn （P）为进程P的自由名的集合。我们识别直到结构同余a（→b）.Pa（→c）.P{→c/→b}P|0元！a（→b）.P！a（→c）.P{→c/→b}P|QQ|Pνa@l.Pνb@l.P{b/a}（P|Q）|RP|（Q|（R）νa@l.00νa@ l.νb @ m.P ν b@ m.νa @ l.P a/= bl[νa@m.P]νa@m. （l[P]）（νa@l.P）|你好。（P|Q）a∈fn（Q）这里P→c/→b代表捕获-避免同时替换。 这种一致性允许绑定名称的alpha转换、并行组合"“的代数属性以及通道名称的灵活范围。这最后一点意味着我们可以自由地扩展和收缩任何v-绑定的作用域，当然前提是它总是包括它绑定的名称的每一次使用2.2范围和领域上面的结构同余式的一个有趣之处是方程l[νa@m.P]是的。（1[P]）、交换名称绑定和区域边界。这样做的结果是，由v-绑定确定的通道名的作用域与由l[ ]给出的区域布局完全无关。作用域决定了一个名字在哪里被知道，这将随着过程的发展而改变：区域决定了一个名字如何被使用，这些区域有一个固定的结构。6||对于有意义的过程描述，嵌套区域的固定结构必须符合预定的层次顺序。例如，一个网络可以包含一个主机，但反之亦然;同样，一个主机不能包含另一个主机。在总的层次顺序中为一步关系写1，我们要求每个嵌套区域必须是1-低于上面的区域定义2.2过程P的顶层动因是所有子项m [Q]，它们本身不包含在任何中间区域l[-]中。例如，在过程a<$bm[Q]a（b）中。m[R]thetop-levelagentsarem[Q]和m[R]。定义2.3一个进程P在层l上是良构的，如果对于每个顶层主体m[Q]，层m<1l，并且Q本身递归地在层m上是良构的。 一个施事l [P]是良构的，如果P在层l是良构的。我们现在可以正式区分名称的作用域和它的作用域。考虑绑定通道名a在一个well-formed过程P，作为某个动作的对象：一个（-），一个（-），或！a（−）。a的作用域是封闭的ν-绑定νa@l。（−）。a的这种出现的局部区域是封闭的水平l区域l[-]。一个名字在其作用域内可能有几个不相交的局部区域。 它也有可能一个名字出现在正确级别的任何局部区域之外;在这种情况下，它只能被视为数据，而不能用于通信。我们将看到操作语义以及后来提出的类型系统如何强制执行这种行为。2.3操作语义我们给局域演算一个后期绑定的，小步操作语义。其中大部分是常规π演算的标准;唯一的改进是确保任何信道上的通信都包含在适当的局部区域内。哪个区域是合适的取决于每个通道的操作级别，我们在一个级别上下文Λ中捕获该信息：从通道名称到级别的有限部分映射。我们使用名称绑定中的a@l表示法写下级别上下文。举例来说Λ ={pike@net，finger@host，daytime@host，print@host}，或者更简单：Λ= pike@net; finger，daytime，print @host。这表明pike是一种用于网络远程通信的通道，而finger、daytime和print，即使是全球已知的，也仅限于主机级交互。7⟨ ⟩−→⊆►≡l−→l−→出a→ba<$→b⟩−→ 0l≤Λ（a）a（→b）INΛla（→b）.PPl≤Λ（a）→bdom（Λ）=πa（→b）进去！啊！a（→b）.PP|！a（→b）. Pl≤Λ（a） →b≠m（Λ）=πPARαP−→PJαP|Q−→PJ|QPa→cPJΛa（→b）Q QJΛ►l P|Q−τ→PJ|QJ{→c/→b}结合αΛ，a@m<$lP−→PJa∈/fn（α）αΛlνa@m.P−→νa@m.PJ区域αP−→PJ如果α是a<$n→b<$n或a（→b），αΛml[P]−→l[PJ]则m≤Λ（a）图1.一、 局部区域演算的操作语义给定某个层次上下文Λ，我们写ΛlP表示过程P在水平l处是良构的，其中fn（P）dom（Λ）。 当这个过程实际上一个单一的代理，我们可以省略旋转栅门上的注释，并将其写成Λl[P]我们的操作语义是作为一个在良构过程上的归纳定义的关系给出的，由它们的级别l和上下文Λ索引过渡的形式是αP−→Q其中Λ∈P，α是下列之一。转换α：：=a<$→b<$输出|a(→b)input|τsilent internal action跃迁本身有自由和束缚的名字，分别由函数fn（α）和bn（α）给出，其中通常fn（a<$n→b<$n）={a}<$n→bfn（a（→b））=fn（！a（→b））={a}b n（a<$n→bn）=n=f n（τ）=b n（τ）b n（a（→b））=b n（！a（→b））=→b .使用图1的规则导出有效的转换。我们对这些规则和附加于它们的附加条件• 积极使用结构一致性−→Comm8≤∩∅--Ll1k它可以取得进展。例如，PAR规则没有对称形式（也不需要）。• 为了应用COMM规则，可能有必要使用结构一致性来扩展通信名称的范围，以涵盖发送者和接收者。• 后期绑定由输入规则上的副条件→bdom（Λ）=强制执行;这确保了输入名称被选择为新鲜的，准备好在COMM规则中替换Q→c/→b。同样，我们可以通过各种方法来实现这一点。所有这些评论都是对标准的π-演算 以下是当地的具体情况。• 关于OUT、IN和IN的边条件lΛ（a）！规则防止以太高的电平读取或写入通道。例如，尝试在主机级进程中传输应用程序级名称。任何试图这样做的进程都会被卡住。• AREA规则上的边条件m≤Λ（a）防止通信从其本地区域逃逸。注意，这里必须是l<1m，因为要求左手边l[P]在水平m处是良构的。下面的结果表明，这种操作语义确实成功地捕捉到了区域和级别背后的直觉：区域在转换过程中保持其结构，并且通道上的操作从未在其操作级别之上被观察到。α命题2.4如果我们可以导出变换Λ<$lP−→Q，则• 过程Q在l级是良构的，其中fn（Q）是n（Λ）n（α）;• 若变换α是a<$n→b<$n或a（→b），则l≤Λ（a）.我的律师。 关于Λ<$P−α→Q导出的结构归纳。特别是如果Λ进一步跃迁。P−τ→PJ则ΛτPJ和PJ本身可能使推论2.5如果我们能导出跃迁序列Λ<$P−τ→P−τ→···−τ→P−α→Q则Q的性质与命题2.4证明中的性质相同。 重复前面的命题。2.4示例在介绍中，我们遇到了一个互联网服务提供的小模型。图2将该系统公式化为局部区域演算的项，L►LτττCarp= host [vc@net. （派克·芬格，C.|c（x）. printx）]Pike=主机[Inet|手指|白天]Inet=！pik e（s，r）. 四月Finger=！finger（y）. 你好PikeUsers白天=！daytim e（z）. zPikeDateΛ =pike@net;finger，daytime，print@host鲤鱼（Carp|派克）图二、使用本地区域的进程示例：Internet服务器守护进程以下结构：鲤鱼（Carp|Pike）。回想一下，主机Carp希望通过一个通用Inet守护进程联系运行在主机Pike上的Finger守护进程我们现在可以应用我们的操作语义来查看这一点。鲤鱼（Carp |Pike）（host [vc@net. （派克·芬格，C.|c（x）. printx）]|手指|白天]）|Daytime])扩大范围vc@net是什么意思（主持人[派克·芬格，c|c（x）. printx]|手指|白天]）|Daytime])展开Inetv c@net。（主持人[派克·芬格，c|c（x）. printx]|host[! pik e（s，r）. 四月|手指|Daytim e]）pike@net上的通信−→νc@net。（host[c（x）.print]|Inet|手指|白天]）|Daytime])展开Finger网络。（host [c（x）.print]|Inet|！|! finger（y）. 你好PikeUser s|Daytime]）finger@host上的通信−→νc@net。（host[c（x）.print]|cPikeUsers|芬厄河|Daytime ]）|Daytim e])通信关于C@net−→νc@net。（host [print PikeUsers]|手指|白天]）|Daytime])在网络和主机级的一系列内部通信之后，第一个主机Carp准备打印信息PikeUsers，主机Pike恢复到其原始配置。即使这个小例子也展示了有趣的可伸缩性。• Pike可以支持多个同时的手指或白天请求，因为910τ⟨ ⟩Main= app [v c@host. （load）|c（y）.link（z）.print（y/z）]Probe= app [v c@host. （load）|c（w）.linkw）]Load=ap p[！l oad（x）. [LocalLoad]Λ =load@host，link@net，print@host主机[Main|负载]|主机[探针|负载]图3.第三章。使用局部区域的进程示例：负载管理代理新创建的信道（如C）提供专用通信链路。• 该系统可以在多个主机上支持Finger和Daytime服务器，使用完全相同的代理代码和协议，因为finger和Daytime名称是全局已知的，但在本地起作用。图3展示了另一个示例，这一次是一个非常简单的代理风格编程模型两台主机都带有负载监视代理Load，它将向同一主机上的任何其他代理报告当前系统负载。一台主机上的主程序想要比较两台机器上的负载，并使用与它共享专用通道链路的Probe代理来完成这一任务。执行这些过程会产生以下结果：主机[Main|负载]|主机[探针|负载]−→主机[print k]|负载]|主机[加载]其中k是两台主机上负载的数值比。 输出打印k是主剂的残留物，探测器被完全释放。像这样安排的系统的一个目的是它允许在加载代理中进行简化：• 这两个加载代理实际上是相同的：没有参数，没有区别标识符。• 两者都使用相同的全局已知通道名load进行寻址。• 它们只需要主机级的通信能力，并且可以独立于防火墙或身份验证进行操作。这些都是基于代理的编程提出的优点：例子显示了如何局部区域演算可以表示它们。当然，当智能体变得可移动时，它们确实会受到影响，但即使在这样的静态系统中，我们也可以开始评估它们的属性3区域类型第2.3节结尾处的结果表明，本地通信确实保持本地性：在信道上的动作从未在其水平之上被观察到。11≤►操作然而，这依赖于图1的操作语义中的几个副条件，其形式为IΛ（a），其本质上是运行时级别检查。在本节中，我们将展示一个合适的类型系统可以提供足够的静态信息，使这些检查变得不必要。图1中的规则AREA处理的是一旦动作发生就进行传播，它的副条件仍然是必不可少的。电平测试伴随OUT、IN和IN！是不同的：它们检查是否应该尝试一个动作。例如，如果过程a（→b）.P高于a的操作级别，则不应进行该过程。可以说，这样的进程永远不应该被编写;消除它们并非完全无关紧要的原因是，它们可能在执行过程中作为替换的结果出现。例如，考虑以下系统：a@hos t，b@app主机[ap p[a<$b]|a（x）。[x]−τ→宿主[]−→在这里，应用程序将名称b发送到主机级进程;这是作为数据的，但主机随后尝试在其上传输，并且进程停止，因为b仅用于应用程序内的通信我们提出的类型系统不仅通过指定通道的操作级别来处理这个问题，而且还通过递归方式指定通道名的级别。3.1类型系统类型由以下相当简单的语法给出。Typeσ：：=→σ@l形式a：→σ@l的类型声明a是一个携带其类型由向量→σ给出的向量元组的左向量通道。基本类型是那些具有空元组的类型：类型（）@ l的通道用于l区域内的同步。在具体的例子中，我们将假设额外的基本数据类型，如int或string，以便方便;这些可以毫无困难地合并到正式表示中。将类型引入进程所需的唯一语法更改是ν-结合：工艺P、Q：：= ··· |νa：σ.Pσ型新河道A。另一个绑定操作，输入前缀a（→b）.P，d不需要显式的类型注释，因为→b的类型由通道a的类型固定。我们还将级别上下文Λ替换为类型上下文Γ，限定从通道名称到类型的部分映射。通过这些改变，图4呈现了用于派生形式为ΓIP的类型断言的规则，其声明亲-cessP在上下文Γ中的级别l处是良好类型的12[2014 -05-23][2014-05-23]L►Γ0ΓlPΓlQΓ►lP|QΓ，→b：→σlPΓla（→b）.PΓ（a）=→σ@m且l≤mrlPl mr，a：σlPΓ，→b：→σlPΓ（a）=→σ@mΓ►m l[P]1Γ►l νa：σ.P你好！a（→b）.Pl≤mΓ<$la<$$>n→b<$r（a）=→σ@m，r（→b）=→σ且l≤m图四、局部区域演算中的过程类型为了将类型化演算与非类型化演算联系起来，我们使用e rasur e的概念。 如果σ=→σ@l是一个y pe，那么它的解σ就是水平。 如果P是一个类型化的过程，那么它的擦除P是同一个过程，所有的类型都被它们的擦除版本替换了：特别是名称绑定νa：→σ@l.Q被替换为νy a@ l.Q。这样就丢弃了类型信息的细节，但保留了基本级别的声明。最后，擦除类型上下文Γ给出级别上下文[Γ]。命题3.1如果P在类型上下文Γ中的级别l是良型进程，则它的擦除[P]在级别上下文[Γ]中的级别l是良构的。rlP=[rl[P我的律师。 关于T型导数ΓlP的结构归纳。3.2示例我们可以给2.4节中的两个例子都赋予类型，它们合理地反映了它们的操作。首先，对于图2的互联网守护进程c：string@netpike：（service，response）@netfinger：service白天：服务服务=响应@主机打印：字符串@主机响应=字符串@网络finger和daytime的类型服务扩展为（string@net）@host。这意味着通道只能用于主机级通信， 所携带的值本身将是网络级名称。主机级通信是在Inet和Finger或Daytime之间进行的;网络级通信是发送给原始查询者的响应，在本例中是机器Carp。通道派克有一个网络级别的类型，作为网关，读取服务的名称和服务应该发送其应答的通道第二个示例是代理比较两个主机上的负载，其类型如下。c：int@hostload：（int@host）@hostlink：int@net print：int@host13≤LL这里最有趣的类型是load：它捕获了这样一个事实，即加载请求不仅必须来自同一主机上的代理，而且响应也是受主机限制的。这是在更大的分布式环境中使用的纯本地过程调用的特征。3.3正确性在图1的所有规则中，良好类型进程的操作语义用Γ替换Λ，并从OUT、IN和IN中省略副条件lΛ（a）。进去！我们在本节中所展示的是，进行这些遗漏是安全的。第一步是证明这种操作语义保留了类型。命题3.2如果P在上下文Γ中是在水平l上的良型过程，并且我们αc可以导出变换ΓlP−→Q，则Q是线性的：• 若α=a<$n→b<$n或τ则Γ<$lQ• 若α=a（→b），则当rrer（a）=→σ@m时，我的律师。关于跃迁Γ-1的结构归纳P−α→Q。正如预期的那样，在类型化进程项的行为和它们的非类型化擦除之间有着极其紧密的联系。命题3.3证明了Γ_P是一个线性p_p。αα(i) 如果Γ。(ii) 若[Γ∈[P∈−α→Q，对于某个单位元Q，则re是一个单位元PJα使得Q=[Pj]且Γ<$lP−→PJ。证据 关 于 转换推导的结构归纳。结合命题3.2和3.3（i）与推论2.5，我们得到了一个证明，即定理3.4对于任何良型过程P，如果我们能导出转移序列，τ ταΓlP−→. . . −→−→Q当reα为a<$n→b <$n或a（→b）且Γ（a）=→σ@m时，则水平l≤m.这就确定了一个良好类型的进程永远不会尝试使用高于其操作级别的通道，而不需要在操作语义中进行显式检查。4结论和进一步的工作局部区域演算提供了一个合理的设置来探索使用全局已知但在局部起作用的名称。我们已经给出了一个操作语义，并证明它正确地捕捉到了这种直觉。说明性示例包括互联网服务协议和一对分布式代理。14我们提出了一个类型系统的通道中的演算，并证明它消除了一些运行时局部性检查的需要。我们正在探索的另一个应用领域是分层网络协议：每一层都以本地名称与下一层通信，只有最外层参与实际的长距离通信。例如，TCP/IP通常与作为应用传输网络链路的等级排序一起使用。我们将局部区域编码到纯π演算中，使用控制器进程的显式装置来执行级别约束：每个通信都通过路由器进行编组，每个局部区域一个我们还在MLj [2]中构建了一个实现的组件，这为微积分的各种设计选择提供了有用的见解通道在不同级别（网络、主机、应用程序）运行- 出现了调整过程的观察以检查单个感兴趣级别的可能性。我们正在研究一个相应的互模拟概念，它在某些层面上过滤了行动，并将注意力集中在其他层面上。局部区域也为它捕获空间信息提供了机会演算中的通信可能被限制在某些区域的事实提供了一种形式的安全性，尽管是相当弱的一种，并且可能在这里与π演算的相关版本建立联系。例如，如果消息的加密和解密由私钥命名的通道上的通信表示小的“沙箱”区域防止窃听。参见Vivas和Dam [15]，了解使用阻塞的说明。级别的顺序直接暗示了通道上的子类型的概念：例如，可以使用网络级别的名称来代替主机级别的名称。然而，即使这是可取的，它打破了，只要我们传递的名称本身。 构造函 数 ' @ ' in → σ @ l 在 其 左参数中变为不变式，本质上是因为通道用于输入和输出两者。当然值得追求的一个方向是从静态代理到适当的移动代理的步骤，我们正在寻找各种方法将这些纳入微积分，同时保留范围和区域的单独处理。上面提到的π演算编码提供了一些提示：在经典的π演算风格中，它可以通过动态地重新布线伴随的路由器进程来模拟移动区域。15引用[1] 罗伯托·阿玛迪奥关于流动性的模型。理论计算机科学，240：147[2] P. 尼克·本顿安德鲁·肯尼迪和乔治·罗素将标准ML编译为Java字节码。ICFPACM Press，1998.[3] 杰拉尔·布多尔。 异步时钟和π-演算。Rapportderecherche1702，INRIA，Sophia Antipolis，1992.[4] 卢卡 卡尔代利 和 安德鲁 D. 戈登 移动环境。 在软件科学和计算结构的基础：FoSSaCS '98的会议记录Springer-Verlag，1998.[5] C'edricFournet和GeorgesGo nthier.返回CHAM和连接演算. POPL '96会议记录：第23届ACM程序ACM Press，1996.[6] 马修·亨尼西和詹姆斯·莱利移动代理系统中的资源访问控制。在HLCL '98会议录Elsevier，1998年。[7] 马修·亨尼西和詹姆斯·莱利一种用于分布式移动进程的类型化语言。POPL'98：第25届ACM Symposium on Principles of Programming Languages会议记录ACM Press，1998.[8] IANA ， 互 联 网 号 码 管 理 局 。 协 议 号 和 分 配 服 务 ： 端 口 号 。http://www.iana.org/numbers.html#P。[9] 丹尼湾兰格和大岛充。移动代理的七个好理由Communications of the ACM，42（3）：88[10] 罗宾·米尔纳多元π演算-教程。技术报告ECS-LFCS-91-180，计算机科学基础实验室，爱丁堡大学，1991年。[11] 大卫·桑吉奥吉。移动处理演算中的局部性和非交错语义。理论计算机科学，155：39[12] 大卫·桑吉奥吉。接受的名义纪律。在自动机，语言和编程：第24届国际学术讨论会ICALP '97会议记录Springer-Verlag，1997.[13] 大卫·桑吉奥吉。使用类型推理并发系统。在软件科学和计算结构的基础：FoSSaCS '99的会议记录Springer-Verlag，1999年3月。16[14] 彼得·休厄尔。分布式π演算的全局/局部子类型和能力推断。在自动机，语言和编程：第25届国际学术讨论会ICALP '98会议记录Springer-Verlag，1998.[15] Jos'e-LuisVi vas和MadsDam。从高阶π-演算到静态算子存在下的π-演算CONCUR'98：Concurrency Theory。第九届国际会议论文集，计算机科学讲义1466。Springer-Verlag，1998.