基于能力的类型系统和共归纳行为理论在DPI中的应用

理论计算机科学电子笔记156（2006）115-133www.elsevier.com/locate/entcs将递归添加到DPI（延伸摘要）Samuel Hym1PPS，巴黎大学7CNRS马修·轩尼诗2苏塞克斯大学信息学系摘要D PI是pi演算的分布式版本，其中进程被显式地定位，并且可以使用迁移构造来在位置之间移动。我们认为，在语言中添加递归运算符会显著增加其描述能力。但是输入递归过程需要使用潜在的无限类型。我们表明，DPI的基于能力的类型系统可以扩展到共归纳类型，使递归过程可以成功地支持。我们还表明，在Π演算，递归可以通过迭代实现。 这个翻译比标准的翻译有以下改进：是组合的，但在我们的分布式环境中仍然会带来显著的迁移开销保留字：类型微积分，递归，使用复制实现，递归和共归纳1介绍Π演算[7，8]是一种著名的形式演算，用于描述，推理，并发进程的行为，通过双向沟通渠道。Dpi [4]是一个扩展，其中进程位于其中，并且可以在位置或站点之间迁移通过执行显式的migrate命令;代理转到k.P，在1Samuel. pps.jussieu.fr2M. sussex.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.029116S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115站点l将继续在站点k处执行P。这个扩展配备了一个复杂的基于能力的类型系统，以及一个考虑到这些类型所施加的约束的共归纳行为理论，[3，4]。类型非正式地对应于能力集，并且流程可以对实体（例如位置或通道）的使用取决于流程拥有实体的当前类型。此外，这种类型可能会随着时间的推移而变化，反映了过程可能会逐渐积累实体的能力。最常见的PI演算公式使用迭代（写为P）的迭代，以描述重复的过程。因此什么？（x）d！表示在通道C上重复输入值并在D处输出该值的过程。另一种方法是使用显式的递归运算符，从而得到如下定义：recZ. c？（x）d！x但有人认为显式递归是不必要的，因为它不会给迭代带来额外的方便;事实上，众所周知，这样的递归运算符可以很容易地使用迭代实现;参见[ 8 ]中的第132-138页然而，当我们进入DΠ的分布式世界时，情况发生了变化。在第2节中，我们证明了显式递归的增加导致强大的编程技术，特别是它导致简单的自然描述的过程中搜索底层网络的网站具有特定的属性。不幸的是，这种描述能力的提高是有代价的。为了使这些递归过程 能 够 容 纳 在 DPI 的 类 型 化 框 架 中 ， 我 们 需 要 用 共 归 纳 类 型 （ co-inductive types）来扩展类型系统，即潜在无限深度的类型本文的目的是• 演示递归在添加到DPI时的描述能力;• 开发一个支持递归过程的共归纳类型系统;• 证明在没有网络故障的情况下，以显著的迁移成本为代价，DPI中的递归仍然可以在第2节中，我们描述了对DPI的扩展，称为RECDPI，并通过一系列原型示例演示了递归的强大功能。第3节将概述如何定义共归纳类型，以及如何轻松扩展DPI的类型系统以处理S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115117（Ⅲ）这些新类型。递归过程到迭代过程的转换在第4节中解释，我们在第5节中概述了正确性的证明。这需要使用类型化互模拟等价来适应RECDPI的类型化标记转换系统。该文件在很大程度上依赖于现有的工作DΠ，读者被称为文件，如[3，4]的详细解释的语义DΠ和它的类型系统。2recDpi语言RECDPI的语法如图1所示，是它的简单扩展新的构造以粗体突出显示。像往常一样，它假设一组名称，由字母组成，如a，b，c，k，l，. . 和一组单独的变量，其范围为x，y，z，.. . . 为了处理递归过程，我们使用另一组递归变量，范围为X，Y，Z，. 语言中的值包括标识符，即名称或变量，以及地址，其中，W代表位于那里的一个位置和一个通道。在本文中，我们只考虑封闭项，其中所有变量（包括递归）都有界。最重要的新构造是对于类型化递归进程，rec（Z：R）。正如我们将看到的，R类型规定了希望托管此过程的任何站点的要求。我们在这里还有一个新的构造[x]P，它允许进程知道它的当前位置。例2.1[搜索一个网络]考虑下面的递归过程，它在一个网络中搜索满足某个未指定的predicatep的某些值：搜索rec Z：S. 测试？（x）如果p（x），那么回家。报告！否则会叫？（y）gotoy.Z当放置在一个特定的位置，如k，给系统k搜索，该过程首先从信道测试获得本地值。如果它满足测试，搜索结束;过程返回主页，并报告值。否则，它使用本地通道neigh找到当前站点的邻居，迁移到那里并在这个新站点上启动递归调用Q我们避免给读者带来RECDPI的正式归约语义的负担，因为它是DPI的一个小扩展。 第4节我们118S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115（Ⅲ）||∗⟨ ⟩（2）τ（Ⅲ）（Ⅲ）∗（LTS-REC）Kτrec（Z：R）。 P图1RECDPIM，N：：=系统l P定位过程M NComposition（newe：E）M Name Creation0终止P，Q：：=过程u！V POutput你呢？（X：T）PInputgotov.PMigration如果u1=u2则PelseQ匹配（newcc：C）P通道创建（newregn：N）P全局名称创建（newlockk：K）P位置创建P Q组成停止终止P迭代这里[x]P位置查找rec（Z：R）.P递归Z递归变量给出语言的类型化标记转换系统，其τ-移动提供了我们的归约语义（参见图3）。 对于目前的讨论，我们可以集中在以下规则：（LTS-此处）kτk这里[x]P−→k P[/x]（LTS-ITER）k<$P）−→ k<$P）|（k<$P）<$rec（Z：R）. P）−→ k<$P {/Z}）第一个简单地实现了由这里的构造体捕获当前位置。第二个声明在k，kP处的迭代过程可以产生新的副本k P，同时保留迭代过程。这意味这个过程的每个新副本都位于k中。最后一个（LTS-REC），以标准的方式通过展开主体来实现递归，这是通过将递归变量Z在P中的每个自由出现替换为递归过程本身来完成的。这需要一个显式的τ-约简来匹配规则（LTS-ITER）。S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115119（Ⅲ）（Ⅲ）（Ⅲ）（2）（Ⅲ）（2）例2.2[自定位过程]我们给出一个例子来说明为什么这里的构造对于递归过程特别有趣。考虑系统kQuest，其中任务记录Z：R。 Here [x]（newc ans）neigh？（y：R）（ans？（新闻）. . |gotoy req！数据，一个s@xZ）在确定其当前位置x之后，该过程在当前站点k处生成新的本地频道ans，并且在该频道上设置监听器以等待新闻。同时，它通过本地信道neigh找到一个邻居。然后，它迁移到这个邻居，并通过channelreq在那里提出一个问题，并发出一个新的递归调用，这次是在相邻的站点。邻居的请求信道req需要一些数据、data和返回地址，在这种情况下，返回地址经由值ans @ x给出。请注意，在运行时，在提供给信道请求的值中出现的x由始发站点k代替。在简化系统kQuest的前三个步骤之后，我们得到（新ans）kneigh？（y：R） （gotoy. req！数据，ans@k|ans？（新闻）. . ）的方式如果k（新闻）. .|L Q| (newansJ)lneigh?（y：R） （gotoy. req！数据，ansJ@l数据探索|还有J？（新闻）. . ）的方式用Q在l运行一些代码来回答Quest带来的请求。这里的结构也可以用来写一个进程，从一个简单的链表开始初始化一个双向链表。为此，我们假设单元格是包含两个特定通道的位置：n用于获取列表中下一个单元格的名称，p用于前一个我们系统的初始状态是l0n！100万美元 | l1n！2012年2月 |......这是什么？我们在这个网络的第一个单元中运行以下代码来初始化列表：recZ：R. n？（nJ）这里[pJ]（n！金日成|转到nJ。（p！⟨pJ⟩|Z））Q现在我们需要更仔细地研究递归构造中涉及的类型，如R120S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115⟨⟩ |⟨ ⟩ |⟨⟩||⟨ ⟩ ⟨⟩⟨ ⟩图2递归预类型基本类型：B：：=intbool单位... 本地信道类型：A：：= RU WTRWU，T能力类型：C：：= u：A位置类型：K：：= LOC [C 1，...，Cn]，n≥ 0 |μY。K|Y注册名称类型：G：：=RCAV值Types：V：：=B|一|（A）@u|（A）@K传输类型：T，U：：=（V 1，...，Vn），n≥ 03recDpi的共感应类型DPI有一个完善的基于能力的类型系统，[4]，我们可以适应RECDPI。3.1的类型在这种类型系统中，局部通道具有形式为RU，WT或RWU，T的读/写类型（意味着在该类型的通道上，值以类型T写入，并以类型U读取），假设对象类型U和T位置具有记录类型，格式如下LOC [u1：A 1，.，n：An]指示本地信道u，i可以在对应的类型A，i处使用。然而，对于递归过程，我们需要考虑无限位置类型。要看到这一点，请再次考虑例2.1中的搜索过程Search。任何可以支持这个过程的站点，比如k，都需要有一个名为neigh的本地通道，从中可以读取值。这些值必须是位置，让我们考虑它们的类型，即neigh的对象类型。这些位置必须有一个叫做test的本地通道，具有适当的类型，还有一个叫做neigh的本地通道;这个本地通道的对象类型必须与我们试图描述的类型相同使用递归运算符μ，这种类型可以描述为μY。LOC [test：RTt，[neigh：rY]在搜索的定义中，它将被用作类型S;它精确地描述了希望托管此过程的任何站点的要求图2给出了递归预类型的集合，通过添加运算符μY获得。K作为一个构造函数，以DPI的类型形成规则。S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115121LOC嘶鸣R·⟨ ⟨⟩⟩在[8]之后，我们可以将每个递归预类型T与一个共归纳预类型相关联，表示为Tree（T），它采用有限分支但可能无限的树的形式，其节点由类型构造器标记。例如，Tree（S）是由下图表示的无限树测试R·Tt定义3.1 [压缩和树预类型]我们称递归预类型S为压缩的，如果对于每个μY。它包含，Y只能在出现LOC的情况下出现在SJ中。在本文中，我们将只考虑压缩前类型。对于每个压缩S，我们可以定义Tree（S），唯一的树满足通过以下等式：• 非缠绕递归预紧类型Tree（μY. SJ）=Tre e（SJ{|μY。SJ/Y|）的文件• 不修改任何其他构造;例如Tree（R<$U <$）=R<$Tree（U）<$我们称Tree（S）为与递归预类型S相关联的树预类型。Q请注意，当递归前类型S不是压缩的时，Tree（S为了从预类型到类型，我们需要摆脱无意义的预类型，如RWR，int，这将是一个通道的类型，在该通道上写入整数，但读取通道。这是通过使用子类型的概念来实现的，并且要求在RW<$U，T <$，T的形式中必须是U的子类型。在图A.1（附录中）中，我们给出了标准规则集，定义子类型关系（SUB-CHAN），采用以下形式D Π; 一个典型的规则， 的实例T：U：UJRWU，T：RUJ然而，在这里我们解释这些规则共归纳，[2]。形式上，它们引起了树前类型上的关系的转换如果R是这样的关系，122S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115˜˜⟨⟩则Sub（R）是由下式给出的关系Sub（R）={（base，base）}{（u：A，u：B）if（A，B）is inR}<${（（C），（CJ））if（Ci，CJi）is inR for alli}我...直观地说，如果图A.1的任何规则的假设在R中，则结论在Sub（R）中。定义3.2[子类型和类型]我们将树预类型之间的子类型关系定义为函数Sub的最大定点，写作νSub。为了方便起见，我们经常写T：TJ来表示（T，TJ）在νSub中。然后树预类型被称为树类型，如果每个出现RWU，T它包含满足T：U。最后，这被提升到递归前类型。如果Tree（T）是树类型，则图2中的预类型T称为递归类型Q子类型的共归纳定义产生了一种自然的共归纳证明方法，这是DPI中用于子类型的通常归纳证明方法的对偶。这可以用来导出RECDPI中子类型化的许多所需属性。 这是一个典型的例子。 让我们把T1↓T2写成这意味着存在某个T，使得T：T1和T：T2，即T1和T2是兼容的。引理3.3树类型的集合，按<：排序，有部分交。即T1↓ T2意味着T1和T2相交，记为T1H T2。在论文的完整版本[5]中，我们继续证明这个结果也适用于递归类型，并且给出了计算任何两个兼容递归类型的交的过程。3.2分型系统有了这些类型，我们现在可以调整DPI的打字系统来记录DPI。在系统一级，判决采取以下形式：ΓMS. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115123（Ⅲ）并且所使用的规则与DΠ的规则相同，参见本文完整版中的图11，[5]，其中它们被重述。这里的主要规则是（T-PROC）伊萨克山口伊萨克山口这反过来又需要一套推理规则来判断伊萨克山口这表明进程P是良好类型的，可以在位置k处运行。再一次，这些规则中的大多数都是从DPI继承的，参见[5]中的图12，我们在这里集中解释递归和here构造所需的三个新规则。后者很简单：（T-这里）rwP[w/x]r=e[x]P然而，为了得到关于递归过程的判断，例如R=（Z：R）。 P（1）我们需要用递归变量的条目来扩充DPI中使用的类型环境。回想一下，这里的类型R是一个位置类型，比如LOC [u1：A 1，. un：An]，表示对希望承载对递归过程的调用的任何位置的最低要求。所以在某种程度上，我们想以与位置相同的方式来考虑递归变量。但是我们必须小心，因为子类型不能被允许在这些变量上，不像位置。因此，在类型环境中，我们只允许Z：K形式的唯一条目，其中K是位置类型。然后，对递归调用进行类型检查的自然规则，即递归变量的出现，由下式给出（T-RECVAR）rw：r（Z）rwZ为了对递归定义进行类型检查，例如上面的（1），我们需要• 检查k至少具有R中所需的能力，即r=k：R;• 确保主体P只使用R中给定的资源。124S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115►⟨⟨⟩⟩►⟨ ⟩ ⟨⟩为了检查第二点，我们再次将递归变量视为位置，并检查P是否在“位置Z”中运行最后的规则是（T-REC）R：RΓ，Z：RZPr=rec（Z：R）.P其中r，Z：R是一个符号，用Z具有R中的所有能力的信息扩展了Γ。例3.4回到例2.1，让我们看看如何使用这些规则来推断Γ k搜索，假设Γ知道home、k等位置及其信道。因此，通过（T-REC），这将等于：Γ，Z：SZ检验？（x）ifp（x）thengotohom e. 回复！否则会叫？（y）gotoy.Z这反过来将主要包括证明：r，rZ：St检验：RTt@ZΓ，τZ：Sτ，x：Ttτneigh：RSτ@ZΓ，TZ：S，x：Tt，y：SyZ这些陈述是可证明的，因为S是μY。LOC[test：RTt，neigh：RY];第一个是显而易见的，而第二个将通过展开递归类型一次而为真，这意味着第三个也将为真。Q将递归变量看作位置的部分观点使构造有效环境的形式规则变得有点复杂。在这个扩展的摘要中，我们不进入细节。但为了完整起见，我们在附录中给出了图A.2中的构成规则，以及图A.3中的值类型化规则。请注意，值类型规则允许使用形式为ΓZ：LOC的语句，这是在“at Z“输入进程时所必需的类型推理系统的主要新技术特性由下式给出引理3.5（递归变量替换）L假设Γ是recZ：R. P. 则r∈wP{recZ：R. P/Z}。这反过来又导致：S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115125►−→（Ⅲ）（Ⅲ）∗⟨ ⟩引理3.6（主语归约）ΓM和MτM. J.MJ意味着，4使用迭代在D pi中使用迭代实现递归的问题，与pi演算相反，是任何形式为k P的代码将强制P的每个实例在原始站点k启动;这与krec（Z：R）相反。其中主体P的初始实例在k处启动，但后续实例可以在任意位置启动，只要它们被适当地类型化。尽管如此，以重复迁移为代价，我们可以通过指定一个在启动新实例之前进程必须返回的主基地，使用迭代来模拟递归进程例如，如果家庭被认为是家庭基地，那么我们可以使用哪里首页搜索）|k<$FireOne）IterSearchping？（l）gotol.test？（x）如果p（x），那么回家。报告！X否则会叫？（y）goto y.FireOneFireOne这里[l]转到home.ping！⟨l⟩通过这个例子，我们可以很容易地看到翻译是如何一步一步地模仿原始过程的：过程的主体没有修改，只有递归部分被改变，通过实现递归调用和一些减少。FireOne是递归调用的“翻译”，这意味着转到主基地并激发一个新实例。这说明了为什么这里的构造是必要的：递归调用的转换需要检测它的当前位置，以确实在“适当”的上下文中触发新实例。然后，复制的IterSearch通过迁移到它将运行的实际位置来启动。这种方法是递归过程到迭代过程的一般转换的基础，我们现在解释。由于我们希望确保我们的翻译是组合的，因此我们必须动态地为迭代过程生成主库，在示例IterSearch中，主库和复制过程已经设置好了。我们还将动态生成注册的通道ping，用于向进程的新实例提供位置的名称，126S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115►递归调用发生。当递归第一次展开时，要做的最后一件事是开始迭代过程，这意味着两件事：将将要复制的代码移动到其母库，并启动第一个实例。正如我们在示例中所解释的，当递归被展开时，复制的代码将只需要等待一个位置的名称，转到那里并表现为递归过程。我们的翻译是这样的：UNREC（recZ：R. P）=（newreg pingZ：RC_rw_RW_R_rw）（newlochome Z：LOC [pingZ：rcRWR]）（UNREC（Z）|回家Z。 你是说Z吗（l：R）goto l. UNEC（P））UNEC（Z）= here [x] goto home Z.pingZ！当然，除了递归之外的任何构造都不会被这种转换修改;例如UNREC（u！VV我们强调这样一个事实，即这种翻译严重依赖于迁移来模仿原始过程。我们推测，在位置或链接可能失败的DPI设置中，如[1]，将不可能获得递归到迭代的合理我们也可以给出另一种翻译，它更接近于[8]中为Π演算提出的翻译：• 关闭递归进程的自由名，然后通过通道ping传递它们的实际值，同时传递位置;• 在这个过程的最高层建立所有的基地，一劳永逸。但这样的方法不会是组合性的。现在我们已经描述了我们的翻译，我们想证明，从某种意义上说，翻译与原文的过程是“对等的”。由于我们在一个类型化的设置中，我们需要检查的第一个属性如下。引理4.1ΓM当且仅当ΓUNREC（M）我们还可以证明M的行为和它的平移UNREC（M）的行为是密切相关的。直觉上，我们想表明，无论何时，则任何观察者，或其他系统，其使用的名称符合类型的限制，在Γ中不能区分之间的M和UNREC（M）。这个想法已经正式在[3]作为一个类型化版本的减少倒钩同余，从而产生的判断Γ|=M=rbcN读者可参阅[3]以了解正式细节。S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115127（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）−−−−−−→˜˜CC−→C）（LTS-L-cREATE）τ图3标记的转换语义。 内部行动。（LTS-GO）我的天啊！P−→τ（LTS-ITER）βrDl<$P）（LTS-拆分）ΓDkP|Q−→τ（LTS-此处）βΓ D k<$P）|k<$Q）ΓDk<$P−→τ（LTS-REC）βr D k<$P）|（k<$P）这里[x]P−→τβΓDk<$P [k/x]）ΓDkrec（Z：R）。 P−→βΓ D k<$P {rec（Z：R）. P/Z}）ΓDk（newlocl：L）P−→τ（LTS-N-CREATE）ΓDk（newregn：N）P−→τ（LTS-C。创建）βΓ D（新l：L）k<$P）|lC）βΓD（新n：N）k<$P）ΓDk（newcc：C）P−→τ（LTS-Eq）βΓD（新c：C@k）k<$P）ΓDkifu=uthenPelseQ−→τ（LTS-NEq）ΓDkifu=vthenPelseQ−→τ（LTS-）MβΓDk<$P）βΓDk<$Q）当u vΓDM（n∈：T∈）k.一个！V（n）k. 是吗？VΓJMDMJ<$NDN−→<$JNDNJnfn（N）=ΓDM|N−→τΓDN|M−→τΓD（new n：T）M J|N JΓD（newnn：T）NJ|MJ定理4.2Sup poseΓM. 然后，|=M=rbcUNRE C（M）.该证明使用该关系的表征作为标记转换系统中的互模拟等价，其中：• 态是形式为ΓDM的构形;• 作用的形式为ΓDM−→μΓJDMJ;这些作用基于标记的图3和图4中给出的转换系统。定义4.3[动作]对于形式为（ΓDM）的构形，我们说它们可以做以下动作：• C−→τCJ或C−（−n：−T−）k−。a−？→V如果我们可以用LTS中的推导证明这一点• C−（n−k）−k。-a！→V如果存在某个推导证明128S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115（m：TJ）k. 一个！VLTS中的J（五）以“名”和“名”命名。QS. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115129（Ⅲ）（Ⅲ）eeee图4标记的转换语义。 外部行动。（LTS-OUT）中文（简体）a：R<$T<$@k∈Γr，nV：T@kenvIDka！Va-！→V（LTS-IN）中文（简体）a：W<$U<$@k∈Γr，V：T@kDk<$P）V：U@k你好吗？（X：T）P-k-。a−？→V（LTS-新）Dk<$P{|V/X|）的文件M−→μ DMJΓD（newn：T）M−→μ（LTS-打开）ΓJD（新n：T）MJn/∈μΓDM−（−n<$−：T<$−）k−。a-！→VDMJn∈ {a，k}ΓD（newn：T）M−（−n n−：T-T−）−k.-a！→V（LTS-弱）DMJn∈fn（V）<$n（T<$）r，n：T<$DM−（−n<$：−T<$−）k−. a−？→VDMJΓDM−（−n：−T−，n−：T−）k−.a−？→V（LTS-PAR）ΓJDMJn/∈ {a，k}M−→μ DMJΓDM|N−→μDMJ|Nbn（μ）fn（N）=我们再次请读者参考[3]以获得进一步的动机;本文还包含以下结果：（ΓDM）双（ΓDN）蕴涵Γ|=M=rbcN当r∈M和r∈N. 因此，我们建立定理4.2，Γ<$M蕴涵（ΓDM）<$bis（ΓDUNREC（M））（2）5递归可实现性130S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115让我们看看在试图证明方程（2）的例子中遇到的问题。为此，让我们考虑搜索的参数化服务器版本S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115131（Ⅲ）¢）112¢） 112（三）这将是一个探索二叉树而不是列表的过程PSearch搜索请求？（x，客户端）gotok0. recZ：S. 测试？（y）if p（x，y）then gotoclient.report！否则会叫？（n1，n2）goto n1.Z |goton2.z在系统服务器PSearch中使用。所以这就建立了一个搜索服务器，在Server;但是与例2.1中的Search不同的是，在网络中要搜索的数据是在search request onsearch req中给出的，并且随后被测试谓词p用作参数。我们将这个过程翻译为以下DPI代码：IPSearch搜索请求？（x，客户端）gotok0. （newreg ping）（newloc base）F|转到基地。电子邮件Instping？（k）gotok.test？（y）if p（x，y）then gotoclient.report！否则会叫？（n1，n2）转到n1。F|goton2. FF这里[l] goto base.ping！⟨l⟩其中Inst是迭代过程的实例，F是触发过程，编写FireOne是上一节中的示例。由于IPSearch是复制的，它将为每个搜索请求生成一个新的Inst主基地。这意味着，在满足了一些这样的请求之后，我们最终将得到一个如下形式的系统（new ping1）（new base1）（new ping2）（new base2）.服务器...|基础1分.. . ）的方式|k1¢. F1）|k2... F1）|......这是什么？ |二进制. ）的方式|k1¢. F 2）.当然，这将对应于RECDPI系统：服务器... |k1¢. rec Z. P）|k2... rec Z. P）|......这是什么？ |k1¢. rec Z.P）.132S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115在这个例子中，我们可以很清楚地看到我们的翻译和标准之间的主要区别，但是非组合的，我们之前提到的pi演算中使用的一个（见[8]），这是由于rec Z的复制而产生的。P.按照[8]中的翻译，S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115133（Ⅲ）（Ⅲ）1JPP112产生以下状态，对应于上述（3）（newping）（newbase）服务器搜索请求？（x，client）goto k0. F（x，client）|base ∗ ping?（k，x，client）gotok.test？（y）. .| k1¢... F（x1，客户端1））|k2... F（x1，客户端1））|......这是什么？|k1¢. F（x2，client2））.F（x，client）here [l] goto base.ping！l，x，客户端注意，这里递归过程中使用的所有自由名称都是封闭的通过ping调用实例时获取实际参数。但更重要的是，只有一个家庭基地是有史以来创建的。因此，组合性的丧失使得等价性的证明更容易，因为每个递归变量只有一个基回到我们的翻译讨论，我们在这里有一个RECDΠ一个包含许多递归结构的过程，但它们的方式是得到的DPI系统（3）取决于系统的历史。 的这就是为什么我们的证明（2）是基于一个扩展版本的翻译其中我们指定recZ. P已经被认为是一个家庭基地。如果没有，它应该生成一个新的;如果有，那么需要记录实际的基地。在本例中，我们需要将同一个home base属性赋予rec Z。在每个k i中的P，以及对于其他K岛让我们写UNRECP（M），用于M的平移，由下式参数化，并指定每个recZ. P应该翻译成M。 然后为了证明等式（2），我们想要展示包含对的互模拟（rDM， rDUNRECP（M））对任意项M，任意环境Γ使得ΓDM是良构构形，任意参数P.但是，在试图展示这种互模拟时，我们仍然有一个主要问题：由于我们引入了许多额外的约简，因此在原始过程中只有一个状态对应于翻译中的许多可能状态。为了处理这些额外的步骤，我们将求助于[6]中给出的证明技术，即直到β的互模拟。这是基于这样的评论，即在通过转换添加的减少中，只有通道ping上的通信是每隔一步就是所谓的β移动在图3的LTS中写为−→τβ。感谢您对最多βwe的二进制运算可以只专注于通信移动，通过使用翻译的新变体，写作UNRECβ（M），这意味着每个β移动所需的 P互模拟已经完成。然后考虑到ping通信134S. 海姆Hennessy/Electronic Notes in Theoretical Computer Science 156（2006）115（这是一个τ-移动）在平移对应于递归展开在RECDΠ，我们可以证明，（ΓDM， ΓDUNRECβ（M））P是一个上至β的双模拟。6结论本文给出了具有递归过程的DΠ-演算的一个推广.特别是，我们描述了为什么这个结构更适合在分布式环境中编程，允许通过网络迁移，访问和询问不同位置的代理的描述。我们还给出了一个类型系统，这个扩展的演算，其中涉及递归类型，处理使用共归纳证明技术，并表明主题减少仍然有效。最后，我们展示了如何通过在网络中添加额外的迁移来将我们的递归过程编码为使用迭代的标准DPI。编码被证明是健全的和完整的，在这个意义上，原来的和翻译的过程是不可区分的类型化版本的减少倒钩同余。现在，研究递归过程在网络某些部分可能发生故障（位置或链路）的情况下的行为将是有趣的，因为故障在分布式计算的研究中非常重要。我们猜想，在这样的设置有没有翻译的递归过程到迭代的，保持其行为。引用[1] Francalanza ， A. 和 M.Hennessy ， Location and link failure in a distributed pi-calculus ，Computer Science Report 2005：01，University of Sussex（2005）。[2] Gapeyev，V.，M. Levin和B. Pierce ，Recursive subtyping revealed ，Journal of FunctionalProgramming12（2003），pp. 511也出现在Benjamin C的《类型和编程语言》Pierce（MITPress，2002）.[3] Hennessy，M.，M. Merro和J. Rathke，分布式系统中访问和移动性控制的行为理论，理论计算机科学322（2003），pp.615-669[4] Hennessy，M.和j.Riely，移动代理系统中的资源访问控制，信息和计算173（2002），pp.82比120[5] Hym，S.和M. Hennessy，Adding recursion to DPI，Computer Science Report 2005：06，University of Sussex（2005）.[6] Je Escherey，A.和J.Rathke，A theory of bisimulation for a fragment of concurrent ml withlocal names，Theoretical Computer Science323（2004），pp.1-48号。