移动环境和图灵完备性的研究

理论计算机科学电子札记96（2004）29-49www.elsevier.com/locate/entcs纯环境演算塞尔吉奥·马·马塞雷斯和伊恩·菲利普斯1，2，3伦敦帝国理工学院计算机系摘要Cardelli和Gordon的Mobile Ambients演算作为移动计算的一个模型引起了广泛的兴趣。标准演算相当丰富，有各种各样的运算符，以及进入、离开和消除环境的能力。问题是什么是最小图灵完备集的结构。以前的工作已经确定，图灵完备性可以在不使用通信或限制的情况下实现。我们表明，它可以实现仅仅使用运动能力（而不是溶解）。我们还表明，某些较小的构造集是终止的或具有可判定的终止。关键词：环境演算，移动环境，图灵完备性，计数器，终止性，可判定性。1介绍自1998年引入以来，Cardelli和Gordon环境是一个包含运行过程的容器。环境可以移动，携带他们的内容。标准演算相当丰富，有各种各样的运算符，以及进入、离开和消除环境的能力。随后的研究人员增加了这种品种1我们要感谢Cristiano Calcagno、Philippa Gardner、Maria Grazia Vigliotti和NobukoYoshida的有益讨论和鼓励。2电子邮件：{ma eis，iccp} @ doc.imperial.ac.uk3马德里斯的研究得到了剑桥微软研究院的资助。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.02030S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-通过提出替代移动能力。我们可能会提到移动安全环境（SA）[13，14]，鲁棒环境（ROAM）[10]，安全环境与密码（SAP）[16]，推拉环境演算（PAC）[20]，受控环境（CA）[23]和盒装环境版本[2]与密码（NBA）[3]。我们将使用术语Ambient Calculus（AC）来指代所有这些变体。问题是什么是一个最小的一组结构，使图灵机的计算能力，即图灵完备。解决这个问题的一种方法是将其他一些已知是图灵完备的进程演算编码到环境演算Cardelli和Gordon展示了如何将异步π演算编码到Mobile Ambients中[6]。编码利用环境演算中的通信原语然而，Cardelli和Gordon还将图灵机直接编码到纯AC中，其中没有通信。（顺便说一句，Zimmer [24]随后将同步pi演算编码为纯Mobile Safe Ambients [13，14]。Busi和Zavattaro [4]展示了如何将计数器机器编码为纯粹的移动环境而不受限制。Hirschko、Lozes和Sangiorgi [11]独立地将图灵机编码到相同的子演算中。在本文中，我们跟进这项工作，并调查是否更小的片段AC可以图灵完整。我们专注于纯AC。我们的工作很大程度上受到Busi和Zavattaro的启发;我们遵循他们使用而不是图灵机。以前的工作留下的主要问题是，纯AC是否具有溶解环境的开放能力可以是图灵完备的。鉴于Bugliesi，Castagna和Crafa在提出他们的Boxed Ambients演算时决定免除环境开放，这个问题特别有趣[2，17，3，7]。他们提倡一个环境包含在另一个环境中的环境之间的通信，而不是移动环境的相同环境通信。在[19]中采用了类似的通信模型。我们给出了一个编码的计数器机器到纯MA没有限制，没有开放的能力（定理3.6），表明这个片段是图灵完备的。编码还表明，无论是终止和观察弱倒钩是不可判定的问题。据我们所知，图灵完备性以前没有被证明用于任何没有溶解环境的能力的纯环境演算（尽管我们注意到在[2]中给出了将pi演算编码为带通信的Boxed Ambients）。Cardelli和Gordon [6]确定了两种不同的环境运动：主观和客观。主观运动是一种-S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-31ent本身移动;objective移动是指它被另一个环境移动的地方例如，如果m[P]（一个包含进程P的名为m的环境）要进入另一个环境n[Q]，那么控制可以驻留在P或Q中。标准微积分MA选择主观运动，而客观运动（所谓的我们将表明，计数器机器可以编码到纯粹的推拉演算（PAC）没有开放的能力。许多演算是主观和客观运动的混合体;当处理m[P]进入n[Q]时，它们需要P和Q同步。在移动安全环境（SA）[13，14]中，环境必须明确允许自己通过协同能力进入。通过为每个环境配备必要的协同能力，可以直接将标准MA编码为SA。因此，MA的图灵完备性结果，例如上面提到的，将扩展到SA，而不是相反。鲁棒环境（ROAM）[10]是另一种演算，其中环境必须同步才能执行进入。m[P]要进入n[Q]，P必须命名n，Q必须命名m，这是一种主观和客观运动的对称混合。MA或PAC的图灵完备性结果将扩展到ROAM（因为我们的编码只使用有限的名称集）。如上所述，MA和PAC在环境之间的同步性不如SA或ROAM。如果我们要求运动能力没有延续，那么在环境中运动可以变得不那么同步，这样如果m[P]进入n[Q]，那么P和Q都不能依赖于这在其代码的其余部分中何时发生。这可以称为异步运动。我们表明，主观和客观的结石与异步运动（没有限制）是图灵完成有足够的权力，在进程中能够同步溶解的氛围。我们感兴趣的是找到AC的最小图灵完全片段。这需要证明较小的碎片太弱而不能成为图灵完备的。Busi和Zavattaro已经证明，在具有开放能力但没有移动能力或限制的MA片段中，可以确定给定过程是否具有非终止计算[4]。我们展示了相同的可判定性属性的片段的能力，只允许在一个方向上移动（无论是进入或退出）。我们还表明，在某些较小的片段（复制只允许的能力），每一个计算终止。该文件的组织如下。在第2节中，我们回顾了环境演算的各种运算符和功能，以及它们相关的归约概念。在第3节中，我们讨论了各种图灵完备语言，有和没有开放能力。在第4节中，我们表明，某些碎片-32S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-具有复制的AC段实际上正在终止。在第5节中，我们证明了AC的某些其他片段具有可判定的终止性。最后得出一些结论。1.1相关工作自从进行这项工作以来，我们最近才知道Boneva和Talbot的一篇独立论文[1]。他们提出了一个编码的两个计数器的机器（图灵完备的形式主义）到纯粹的移动Ambients没有限制，没有开放的能力。我们在定理3.6中考虑的AC片段与他们的相似，但是他们允许在任意进程上复制，而我们只允许在能力上复制。他们表明，可达性和名称收敛（弱倒钩的观察）都是不可判定的问题。由于他们的编码可以采取我们的工作重点与Boneva和Talbot的不同之处在于，我们专注于图灵完备性和终止性，而他们专注于环境逻辑中的可达性和模型检查。2运营商和能力我们将调查各种运营商和纯移动环境的能力[6]及其变体。我们让P，Q，. 在进程和M上的范围，. 而不是周围环境所能发挥的能力。我们假设一个集合N的名字，由m，n，..。和一组过程变量（用于递归），范围为X，.。。首先，我们陈述一个我们将考虑的运营商P：：= 0|n [P] |P|Q| M.P|文波|！P|X|记录X.P通常，0表示非活动进程。我们可以随意省略尾随的0，并将空的环境符写为n[ ]而不是n[0]。进程n[P]是一个名为n的环境，包含进程P。过程P|Q是P和Q的平行合成。 进程M.P执行能力M，然后继续P。 过程νn P是名称n受限的过程P。 通常，restriction是一个变量绑定操作符。我们用fn（P）表示过程P的自由名集合。过程！P是一个复制进程，它可以根据需要旋转P的任意副本。过程recX.P是一个递归，其中X是一个绑定的过程变量。我们将只考虑所有过程变量都被约束的过程。 如果在recX.P中，S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-33X在P中的出现不是在环境中。我们将只需要非装箱递归。如果递归是可用的，那么！P可以用recX模拟。（X）|P），所以我们永远不需要复制和递归。下面是我们要考虑的所有能力的集合M：：=打开n|在n|外出;外 出 |在n|外出;外 出 |推送n|拉;拉第一个功能openn用于溶解一个名为n的环境。其余的能力都与运动有关。我们可以区分主观移动和客观移动：inn和outn的能力使环境能够进入或离开名为n的环境。这是主观的运动。有时我们考虑能力的相比之下，客观运动是指环境被其他环境所移动我们考虑[ 20 ]的所谓包含另一个名为n的ambient的ambient可以使用pushn功能将另一个ambient推出。类似地，pulln可以用来拉入一个名为n的环境。结构一致性将相同的过程等同于结构一致性，结构重排 它由以下规则定义：0 |PP n00P|QQ |Pνm νn P ν n νm P（P|Q）|RP|（Q |R）！PP|！Pνn（P|Q）（νnP）|Q如果n∈/fn（Q） recX. PP{recX. P/X}νn m[P]<$m[νn P] ifm/ =n过程之间的归约关系我们首先定义与能力相关的减少。（Open）开放的|n [Q] →P|Q(In)以英里/小时计|Q] |m [R] → m [n [P |Q] |R]（外）m [n][外] m.P|Q] |R] →n [P|Q] |m [R]（安全）n [在m.P |Q] |m [m.R |S] → m [n [P |Q] |R|安全出口，安全出口|Q]|外磁共振|S] → n [P |Q] |m [R|拉，拉，拉|Q] |m [R] → n [P |Q |m [R]]（推）n [m [P]|推压m.Q |R] → n [Q |R] |m [P]我们将考虑只拥有完整语言的一个子集的语言。34S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-一套能力。 当我们考虑在中具有能力的语言时，我们将也总是有能力，我们将采用规则（SafeIn）而不是规则（In）。显然，如果一种语言具有in、in和复制这些能力的能力，那么规则（In）的结果就可以被模拟;通过将n[P]转换为n[！在n|P]。类似的考虑也适用于各种能力。其余的减少规则是P→PJn[P]→n[PJ]P→PJνn P→νn PJP→PJP|Q → PJ|QP<$PjPJ→QJQJ<$QP→Q我们把→的自反和传递闭包写为。语言是由一组过程L和一个归约关系→组成的对（L，→）。我们将（L，→）简写为L。 我们让L，... 范围跨越语言。我们将通过给出过程的集合来定义一种语言语言的归约关系（和结构一致性）将被默认为由本节中适用于可用运算符和功能的所有规则的集合给出，除了上面提到的一Computation是一个关于P0→P1→· ··的极大值方程。可以对过程进行的最基本的观察是顶层环境的存在（即不受能力保护或包含在其他环境中的环境）[6]。我们称n是P（P↓n）的强倒钩我不知道，... mk（n [Q] |R）（其中nP（P<$n）i< $P<$PJ↓n.m1，. mk），n是弱倒钩3AC的图灵完全片段过程语言的计算强度的一个基本衡量标准是图灵机或其他图灵完备形式是否可以用语言编码Cardelli和Gordon [6]建立了纯Mobile Ambients可以编码图灵机。Busi和Zavattaro [4]通过证明计数器机器（CM）可以在没有限制的情况下在纯MA中编码来改进这个结果。他们还表明，没有运动能力（但有限制）的纯MA片段可以编码CM。我们将表明，CM可以编码在纯MA没有限制，没有开放。我们还将在具有异步运动的MA版本中编码CM（即，在能力之后没有延续），但是具有开放能力。S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-35计数器机（CM）是一组有限的寄存器R0，...，Rb（b∈N）.每个Rj都包含一个自然数。我们把Rj和它的内容k一起写成Rj（k）。最初，寄存器保存输入值。CM执行指令I0，.，Ia（a∈ N），其中Ii具有两种形式：• i：Inc（j）将R j的内容加1，之后控制移动到Ii+1。• i：DecJump（j，iJ）从R j的内容中减去1，之后控制移动到Ii+1，除非内容为零，在这种情况下，Rj不变并且CM跳转到指令iJ。CM从指令I0开始，并无限地按顺序执行指令，直到控制移动到无效的指令编号（我们可以将其视为a + 1），此时CM终止，输出保存在第一个寄存器中。上面定义的CM基本上是[22]的无限寄存器机器。他们使用一组指令，这是最小的，同时保持图灵完整性[18]。(In事实上，只有两个寄存器的CM已经是图灵完备的了。）3.1图灵完备性最好弄清楚在本文中我们将使用什么样的图灵完备性标准。设CM是一个CM（程序加上寄存器及其内容）。令[[[CM]]为AC的目标片段中的CM的编码我们将要求：如果CM终止，则[[CM]]的每个计算都成功完成，这意味着它以某种方式发出完成信号，获得正确的结果并使计算结果（即，第一寄存器的内容）以可用的形式可用于由其它处理执行的潜在• 如果CM不终止，则[[CM]]信号的计算不会完成。在我们的编码中，完成将通过在顶层出现特定环境来因此，我们可以从CM的停机问题的不可判定性推断出，对于目标片段，对于进程P和命名n是否P≠n，它通常是不可判定的。此外，我们的编码实际上将满足标准3.1和以下附加属性：准则3.2·如果CM终止，则[[CM]]的每个计算都终止。36S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-ν• 如果CM不终止，则[[CM]]的计算不会终止。因此，我们可以推断，一个过程是否具有无限计算是不可判定的。(In事实上，如果第二项被削弱为：如果CM不终止，则[[[CM]]]具有无限计算。然而，由于标准3.2不是图灵完备性所必需的，我们不能仅仅因为终结是可判定的而推断出一种语言不是图灵完备的。仍然可以将CM编码为目标语言，其中编码CM的所有计算都是无限的。当CM终止时，编码的CM在发散之前的有限时间内报告结果。然而，通过显示一个片段的标准3.2和另一个片段的终止的可判定性，许多编码满足以下一步保存属性：如果CM在一步中移动到CMJ，则[[[CM]][[CMJ]]]。虽然一步保留是有用的，但我们认为它对图灵完备性来说是不必要的强大奈斯考虑例如图灵机（TM），其在以下意义上是非擦除的：在每一步，其将磁带内容复制到磁带的下一个未使用部分，然后进行指令所需的改变。这样的机器显然和普通的TM一样强大。然而，我们不能将TM编码成非擦除TM并满足一步保存原则，因为非擦除TM具有额外的信息。(Note对于非擦除TM，配置的可达性是可判定的，因为磁带内容的大小不断增加，因此图灵完备性并不意味着可达性是不可判定的。这与我们的关注有关，因为在我们的编码中，我们积累了惰性垃圾。就像非擦除TM一样，这对图灵完备性没有障碍。备注3.3Hirschko，Lozes和Sangiorgi [11]给出了将TM编码为AC片段的编码，该编码满足一步保存，但编码可能会发生这种错误的转向是严格限制的，因为该过程将立即停止在成功终止不能错过的状态。这对于他们声称图灵完备性是足够的，但我们将要求计算不能采取非预期的路径。3.2现有工作Busi和Zavattaro将CM编码为纯AC的两个片段。第一个片段，我们称之为Lop，定义如下：P：：= 0 |n [ ] |P |Q|开放式|文波|X|记录X.PS.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-37ioioioPPAPPAPPA令人惊讶的是，没有运动能力的空环境就足够了。有一个基本的使用限制，以获得相互递归的效果然而，这个结果显示了开放能力的强度。 我们希望研究一下，在不开的情况下，我们是否能达到图灵完备性。Busi和ZavattaroP：：= 0|n [P] |P|Q|开放式|在N.P中|输出|！请注意，Lop不需要限制，并且使用复制而不是递归。Hirschko、Lozes和Sangiorgi [11]独立地将图灵机编码为Lop，并附加了语法约束，即能力的延续必须是有限的，也就是说，不能涉及复制。3.3“Asynchronous” Languages with在本小节中，我们证明了即使在不允许移动能力后的延续时，也存在图灵完备的AC语言。我们对客观运动（定理3.4）和主观运动（定理3.5）都证明了这一点。让Lop是下面的语言（一个片段的推和拉上午-[20]第二十话P：：= 0|n [P] |P|Q|开放式|推动;推动;推动0 |拉，拉; 0 |！注意push和pull没有连续性。我们可以称之为异步运动。此外，复制仅与打开一起使用。定理3.4Lop图灵完备。证据（草图）我们描述了CM到L op的编码。CM将被编码为一个系统，该系统由对寄存器进行编码的进程与每个指令的进程并行组成。我们考虑一个特定的CM，称为CM，指令为I0，.，Ia和寄存器R0，..，Rb.令CM（i：k0，.，kb）表示CM，并将kj存入寄存器j（j ≤ b）。 设CM= CM 0的（唯一）有限或无限计算为CM0，CM1，..、CM1、..。，其中CM_l= CM（i_l：k_0_l，.，kbl）。首先，我们描述了这些规则。Rj（k）被编码为Rj[k]，其中，整数过程k由下式定义：0=dfz[]k+ 1=dfs[k]因此，寄存器通过其最外层的环境来区分。在描述指令的编码时，我们必须考虑这样一个事实，即递减/跳转指令将在每个38S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-Lli i j j ij iji我ii i i i ii i i i0 0时间，他们被使用，因为无论是递减或跳转的代码是留下未使用。因此，我们通过我们在计算中已经达到的阶段的索引l来参数化我们的编码。令dec（i，l）（resp. jump（i，l））是递减的数量（分别为跳转）在CM的计算期间由指令i执行，直到但不包括阶段l。我们用[[[Ii]]l表示指令Ii的编码，定义如下：[[i：Inc（j）]]=df！ 奥佩恩斯蒂岛拉，拉，拉|s[pulll rj|n. sti+1[]|pushsti+1]|pushsti+1][[i：DecJump（j，iJ）]]=df！ O PENST。c[pulll r|奥普恩河（S|ZJ） ]|！ 奥佩恩迪|！ 人民日报|（ci[Zi jiJ]）dec（i，l）|（ci[Sij]）jump（i，l）S=dfd[pulll s|r[pulll s|O PENS. （e[]|pushe） ]|普赫埃|st[]]|奥普内岛pushdiZJ=dfo penz。（dJ[r[0]|stJ[]]|pushdJ）伊治ij i ii我们使用Pk并行地复制P的k个请注意，所有open出现的连续性都是有限的（与[11]中使用的和上一小节中提到的条件相同）。我们定义：[[CM（i：k， . 。 ， k）]]=dfst[]|[[I]]|·· ·|[[I]]|r[k]|·· ·|r[k]0bli0 la l00bbCM的编码是[[[CM]]=df[[CM]]。 说明开始时没有任何垃圾编码的CM将经历连续的阶段[[[CM1]]1。我们证明了对于非线性最小值l，[[CMl]]l=[[CMl+1]]l+1，且[CMl]l保证为[CMl+1]]l+1.一个指令进程[[[Ii]]l由sti在顶层的出现触发;该指令从消耗sti开始。[[[Ii]]l的执行通过释放对应于下一个指令的sti在整个计算过程中，最多存在一个第一如果环境sta+1出现在最高级别，则编码机器终止。根据指令Ii的性质，存在各种情况。形式[[[i：Inc（j）]]的一个转换过程创建了一个新的寄存器rj[s[]]，它可以是一个成功的过程，也可以是一个不需要为增量而进行的过程。新的寄存器将现有的寄存器拉入其核心，并剥去外壳。然后，该指令通过推出下一条指令的触发器来发出完成信号。计算是完全确定的。我们拥有：. .。sti[]|[[i ： Inc （ j ） ]]l|rj[k]. .。你 . . .。sti+1[]|[[i ： Inc（j）]]l+1|rj[k+ 1]. . 。S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-39IOAIOA形式为[[[i：DecJump（j，iJ）]]l的指令处理创建新的环境ci，拉入寄存器rj并剥离其外层，留下数字。这个数字的最外层环境是s或z，这取决于数字是零还是后继数字。• 如果该数字是后继的，则将其拉入环境di内，然后拉入新的寄存器环境rj内，在此将其递减。然后，将包含新的递增寄存器以及触发器sti+1的环境di推出ci，并打开以释放触发器。我们拥有：. . 。 sti|[[i：DecJump（j，iJ）]]l|rj[k+ 1]. . 。你. . . 。 sti+1[]|[[i：DecJump（j，iJ）]]l|[Zi jiJ]|rj[k]. . 。你. . . 。 sti+1[]|[[i：DecJump（j，iJ）]]l+1|rj[k]. . 。递减的执行将ci[ZijiJ]作为垃圾留在后面，这不会在计算中进一步参与。同样，计算是完全确定性的。• 如果数字为零，则这通过打开z来检测，并且新的环境di（包含rj[0]）与触发器一起被打开以释放触发器。我们拥有：. . 。 sti[]|[[i：DecJump（j，iJ）]]l|rj[0]. . 。你. . . 。 stiJ[]|[[i：DecJump（j，iJ）]]l|ci[Sij]|rj[0]. . 。你. . . 。 stiJ[]|[[i：DecJump（j，iJ）]]l+1|rj[0]. . 。同样，计算是完全确定性的。最后，我们看到如果CML是终结的（所以iL=a+ 1），那么[[[CML]] L没有约简。 [[[CML]] L显示倒钩sta+1以指示终止。计算结果存储在寄存器0中，可供后续计算使用。另一方面，如果CM不终止，那么[[[CM]]也不终止，倒钩sta+1将永远不会出现。没有“坏”的计算，即。那些在非最终状态下停止、发散或产生非预期行为的人。我们有一个编码，它显示了图灵完备性，以及终止和弱倒钩的不可判定性。Q我们可以对主观运动达到完全相同的效果尽管编码更加精细。 让Lop请使用以下语言：P：：= 0|n [P] |P|Q|开放式|在n. 0 |出去; 0 |！开放式定理3.5Lop图灵完备。（见全文[15]）40S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-io3.4没有开放的语言到目前为止，所有被考虑的语言都具有开放能力。我们将通过将CM编码成一种仅具有标准运动能力（即in和out）的语言来证明这对于图灵完备性并不重要。让Lio成为以下语言：P：：= 0|n [P] |P|Q|在N.P中|输出|！在N.P中|！outn.P显然，Lio是前面定义的Lop主要区别是Lio没有开放能力。此外，复制仅适用于to the capabilities能力.我们将在第4节和第5节中看到，语言的强度取决于复制是应用于能力还是应用于环境。定理3.6 Lio是图灵完备的。证据（草图）我们遇到的一个问题是处理指令。由于每个指令Ii必须无限多次使用，因此可以将其编码为！pi[Pi]，其中每次需要指令时，旋转pi[Pi]的新副本。但是之前使用的副本可能会干扰与当前副本一起，从而例如，复制可能被错误地定向到仍然存在的旧P1如果我们可以使用开放功能来销毁不需要的环境，则不会出现此问题。寄存器由一系列的双层皮组成。[]]，z[ ]为核心。我们使用双皮肤，而不是更明显的s[s[z[]样式。这是为了帮助减少，这是通过剥离最外面的s，然后在一个单独的操作中剥离现在暴露的t我们遵循Busi和Zavattaro的方法，通过在中央核心z[ ]周围添加新的s[t[ ] ]来执行寄存器的递增。这似乎比在外部添加一个新的双层皮肤更可取，因为它可以防止增量代码和减量代码相互干扰。基本思想是每个指令Ii都是通过输入一个STi环境来触发的。 所有其他指令和所有寄存器也都进入-监视器进程在Ii被允许执行之前检查是否发生了这一情况。因此，每次执行一条指令时，计算都会下降一级。当一条指令结束时，它释放stiambient来触发下一条指令。如果计算完成，第一个寄存器被发送到顶层，在那里它可以作为可能的进一步计算的输入。所以我们有图灵完备性。我们的编码进一步建立了弱barb关系是不可判定的，并且具有非确定性。最终计算是不可判定的。S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-41随着计算的进行，惰性垃圾在指令和寄存器中累积。我们处理这一点就像在Theo- rem3.4的证明中一样，让指令和寄存器的编码与计算中的当前步骤参数化。计算在很大程度上是确定性的;例外是在指令执行之间，指令和寄存器以不确定的顺序向下移动，并且在增量中也有一些有限的并发性。详情请参阅完整版本[15]Q注释3.7在独立的工作中，Boneva和Talbot [1]已经将双计数器机器编码成以下语言：P：：= 0|n [P] |P|Q|在N.P中|输出|！P（请注意，这种语言与Lio略有不同，因为它允许复制任意过程，包括环境。）然而，它们的编码可能会发散并错误地进入错误状态，这意味着它们不要求图灵完备性。然而，因为他们建立了一步保存，他们可以表明，这是不可决定的，是从另一个可达的，以及对于任意过程P，P是否是名字n。Lio中任意进程的可达性是否可判定是一个悬而未决的问题。即使可达性对于Lio是可判定的，这也不会与图灵完备性相矛盾（见3.1节）。我们刚刚将CM编码为具有标准主观运动能力的语言Lio（并且没有开放）。我们也可以用以下语言Lpp对CM进行编码，其中包含目标移动：P：：= 0|n [P] |P|Q|推动;推动|拉;拉|！P定理3.8 Lpp是图灵完备的。（见全文[15]）4AC的终止片段我们想知道3.4小节的语言Lio是否是最小图灵完备语言。作为对这个问题的部分回答，我们将在本节中展示，如果我们移除其中一个移动能力（无论是in还是out），那么结果语言实际上是终止的，即每个计算都终止。定义4.1语言（L，→）是终止的，如果每个计算都是有限的。42S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-LetLièibethefollowinglanguage：P：：= 0|n [P] |P|Q|在N.P中|在N.P中|！在N.P中|！在N.P中|文波请注意，Li<$i是从Lio通过取出能力和（为了使下一个定理更清晰）添加[ 13 ]中的协同能力和限制而得到的。Theorem4.2Lii正在终止。我的律师。（Sketch）首先，如果Lii的一个P有一个无限计算，那么如果我们确定P的所有名称并删除所有限制，我们仍然有一个无限计算，因为所有现有的约简仍然可以发生（也可能是一些新的）。类似地，我们可以用复制的能力替换所有的能力。因此，它表面上显示的子语言的定理P：：= 0|m [P] |P|Q|！以m. p.计|！以m.p.计其中m是一个固定的名字。我们首先定义一个进程的复制嵌套深度（replication nesting depth，rnd）rn d（0）=df0rn d（P|Q）=dfm a x（rn d（P），rn d（Q））rn d（m[P]）=dfrn d（P）rn d（ ！ in m. P）=dfrnd（P） +1rn d（ ！ inm. P）=dfrnd（P） +1我们接下来定义的复制度（缩写为rd，或简单的度）环境温度m[P]。这是P的能力成分的第二个，定义如下。任何过程P在结构上全等于！在m.Pi|！单位：m.Pj|m [Pk]1≤i≤I1≤j≤J1≤k≤K其中I，J，K≥0，且I= 0表示平行组合为空（类似于J，K）。P的能力成分是Pcap=df1≤i≤I！在m.Pi|1≤j≤J！单位：m.Pj并且weletrd（m[P]）=dfrn d（Pc ap）。这是我们定义的，它具有结构一致性。请注意，环境光的度数在整个计算过程中是不变的。它不受任何程度的其他环境因素的影响。而且，任何能力都不会消失。在计算期间，环境可以产生“子”。 例如m[！在m.m[ ]中，当它进入其他环境时，可以产生一系列新的m[ ]环境。这些孩子将有严格较低的复制度。对于一个给定的环境m[P]，一个单一反应可以产生的子元素的数量有一个固定的有限S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-43我们可以假设所有的环境都配备了这两个！在和！在能力的 因此，所有环境的度都≥1。我们简述了终止的两个证明;第一个证明依赖于假设一个最小的无限计算，然后证明必须有一个更小的计算，而在第二个证明中，我们将注意力限制在一个“顶层”的归约策略上，将多集分配给计算中的过程，并证明它们在一个特定的方式1.假设P0→···是一个无限计算。设D0是P0中（无保护的）环境的最大度.在计算期间，新的环境被创建为现有环境的子环境。他们的学位都比他们的父母低， D。其中至少有一个必须是无限生产性的，也就是说，生产无限多的孩子。现在让c >0表示度> D的无限生产环境的数量。我们已经展示了如何将一对（D，c）（D≥1，c≥1）分配给每个无限计算。 现在让P0→···→ Pi→. 是一个无限计算，在字典序中具有最小值（D，c）（D，c）<（DJ，cJ）i ≠ D< DJ或（D = DJand c D的无限生产环境。 我们可以假设它在计算开始时可用，如果需要的话，通过删除计算的有限初始段（这不会改变D和c的值）。Each表示形式为Ci{m[Qi]}的计算is的Pi，其中我们显示所选环境的外部上下文和内部内容。约简要么只涉及上下文，要么只涉及内容，要么涉及所选的环境作为主体-进入或被进入。既然环境是无限生产性的，那么必然有无限多的这第三种还原。现在让我们通过使所选择的环境完全无效来改变计算-简单地移除环境所行使的能力的延续。我们仍然有一个无限的计算，这是比以前更少的如果D的值没有减少，那么c的值必须至少减少1。因此，我们的新计算在字典序中更低，这是一个矛盾。方法2.设→J为标准→还原（第2节）的修正，其中在环境中禁止还原让你的朋友成为你的朋友44S.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-的传递闭包。假设有一个无限计算，PP帽|m [Pk]1≤k≤K那么我们必须使K≥1，使P有约化。 如果K= 1，我们写P\P1.显然，P1有一个无限的计算。如果K >1，则可以表明存在P的无限计算，其开始于由所有其他顶层环境输入的一个特定顶层环境。 因此，P JP J，其中PJ有\约化。把所有这些放在一起，我们看到，如果P有一个无限→计算，那么P也有一个ni无限→J\计算。为了表明无限的可预测假设是不可能的，我们假设多个-tisets的过程，并定义了这些多集的顺序，这是良好的基础和严格减少 与hrespec t toNUMERJ\。LetP0， . . 。 ，Pi，. . 。 这是一个无限次的计算。我们分配给每个chPi是多重集Si.它的元素将是由一个自然数和一个自然数的多集组成的有序对。这些数字都是Pi中的（无保护）环境的度。我们创建S0如下：对于度为d的每个无保护环境m[PJ]，包含在P0中，我们将有序对（d，n）添加到S0。在计算中有两种约简：→J和\。设Pi→JPi+1。A→J约简由度为d的环境m[Q]进入度为dJ的环境m[QJ]组成。与这些氛围相对应的是元素（d，T）和（dJ，TJ）在Si中。（由于我们正在进行顶层约简，因此两个环境在Si对的第一个元素中表示。→J约化将产生m[Q]的d次子元素;我们将它们的度加到T上。<约简也会产生m[QJ]的DJ次的孩子;我们把他们的度加到TJ上。<这样我们就得到了Si+1。现在假设Pi\Pi+1。一个\减少基本上放弃了一个顶部-保持环境水平，同时保持其内容。假设这个环境是d，并且对应于Si的元素（d，T）。我们从Si中去掉（d，T），对于每个DJ∈T，我们将（DJ，）加到Si上。注意，每个dJd。<这样我们就得到了Si+1。我们可以在良基序上定义一个多重集的序，通过这个序，S>Sj，如果SJ是从S通过用一个更小元素的有限集合替换S的任何元素而得到的这是一个很好的选择[8]。现在如果我们只考虑对于多重集合Si中的第一对元素，我们可以看到a →J约简使集合保持不变，而a\约简删除了一个元素，并将it替换为smallerelements的有限集合。在排序中使用了简单的简化。由于>的成立性，没有无限的计算，因此也没有无限的计算。QS.马菲伊斯岛Phillips / Electronic Notes in Theoretical Computer Science 96（2004）29-45OOO如果一个语言没有out作为其唯一的能力，那么它就是终结性的。设Lo为下列语言：P：：= 0|n [P] |P|Q|输出|！输出|文波请注意，Lo是从Lio通过移除能力和（为了使下一个定理更清晰）添加限制而得到的。定理4.3 Lo是终止的.（见全文[15]）请注意，在我们将co-capability out添加到L o的语言中，情况并非如此，因为反例n [n [outn]|！出，出，出当协同能力位于上层时，情况也是如此[16]：n [n [out n]]|！n.出，出有 了“推”作为唯一的能力，我们可以在有限的计算，例如n [ n []|！推;推动备注4.4如果我们将复制与开放功能结合起来，我们可以创建非终止进程，例如n [ ]|！打开的;打开的;打开的Busi和Zavattaro [4]表明，对于使用复制构建的流程，终止是可判定的，开（见第5节定理5.2）。5具有可决定终止性定义5.1如果给定L的任何过程P，P是否具有无限次计算是可判定的，则我们将说终止在语言（L，→）中是可判定的。Busi和Zavattaro证明了终止在语言中是可判定的，没有限制，并且具有开放但没有移动的能力。它们能够允许非装箱递归，而不仅仅是复制。他们的证明依赖于这样一个事实，