CCS-R：可逆计算下的细胞语言与生物系统建模

理论计算机科学电子笔记180（2007）31-49www.elsevier.com/locate/entcs在CCS-R文森特·达诺斯1Universit'eParisVII，CNRSParis，FranceJean Krivine2INRIA法国罗康库尔摘要我们提出了CCS-R，一个可逆的米尔纳的CCS的变体，以形式化的生物系统满足CCS-R中的保留字：可逆计算。 CCS，回溯机制1细胞的语言一些人认为的生物学革命几年前就开始了。新的测量技术，如DNA微阵列，现在正在分子水平上产生大量的数据在生物学中，自上而下的方法第一次被证明是可能的，补充了通常的自下而上的方法。这些全基因组快照在再现和验证细胞分子机制的过程中可能具有巨大的价值。但是，这种新的可能性也带来了一个非常基本的问题，即一个人想要重建的东西首先应该如何表现。应该用哪种语言来描述、模拟和分析构成细胞的相互作用过程的密集网络？目前大部分的重建工作都是针对基因调控网络，即追踪基因相互影响的图形，到但迟早会有更深层次的细节，比如蛋白质之间的相互作用，1 电子邮件：Vincent. pps.jussieu.fr2 电子邮件：Jean. inria.fr1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.01.04032诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）31以及蛋白质与DNA的相互作用，将不得不在图片中找到它们的位置。各种静态图形符号在分子生物学中已经很常见，例如在KEGG途径数据库中[12]，但重建任务需要访问动态。人们需要一种语言来描述细胞过程的精细分子细节，可以说是可以想象，这个问题所有这些都提供了构建模型的方法，但我们注意到，它们1.1π-演算建模最近，Regev，Shapiro [17，15，16]和其他一些作者[1，3]提出了这样一个想法，即进程代数，为分散计算系统中的通信建模而开发的语言，可能是有用的。这个命题属于一个明显不同的范畴，因为在某种意义上，它试图在一个适当的理想化水平上解释什么是分子生物学例如，在π演算中，分子是π演算的主体，绑定是通信，连续的物理接触是私有名称共享，等等。尽管这种关于分子相互作用的观点可能很有诱惑力，但仅仅因为这些相互作用确实是异步和并发的，人们不得不承认，代表精确生物系统的实际代码（例如Regev形式化的EGF-MAPK级联）有时很难辨认，更糟糕的是，在代表给定生物现象的方式上有很大的自由度此外，这里我们越来越接近本文的主题，到目前为止给出的示例总是向前运行，很少让绑定或激活被撤销。虽然这在某些情况下可能是一个相当合理的假设，例如在描述信号转导途径时，但它肯定偏离了实际的生物化学，实际上所有反应都是可逆的。1.2可逆性和调节。不仅大多数反应是可逆的，而且可逆性实际上会影响系统的行为。图1用一个生物学上合理的例子说明了这一点：蛋白质A和B竞争与某些C（可能是DNA上的一个复合物或一组结合位点）结合。由于绑定是盲目的，而且是一种纯粹的局部操作，因此有时可能会达到一种无限状态，A和B都与C绑定。但系统现在，如果我们把这个系统看作一个分子开关，A打开系统，B阻止它，那么系统能从中间态逃逸是至关重要的，否则这个开关就永远关闭了因此，可逆性不仅仅是一种生物化学上的约束，它与细胞自我编程有关，它实际上是一种基本的调节机制，可以防止死锁。诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）3133B一C不稳定络合物一C并且有助于获得类似开关的行为。蛋白B抑制C初始解蛋白A抑制Fig. 1.两种蛋白质本文的贡献是介绍了一个进程代数与可逆性有线的语法。原则上，可逆性可以用π演算来表达，人们可能会想，可逆性是否是一个值得添加的内容。我们认为是的。首先，可逆性似乎是生物系统中的一条规则，它在微积分中，并带来这样做的建模语言更接近真实的东西。其次，虽然声明特定动作是不可逆的，因此是不可回溯的很容易，但这当然是可能的，但在时间，可读性方面有一定的成本，并在模型中引入了大量的非生物事件我们的可逆语言还依赖于比π简单得多的通信代数，即CCS，因此可以期望我们的模型在易读性和可分析性方面表现得更好。1.3纲要代数的发展过程和生物学的应用是分开的.对于有生物学背景的读者来说，这是一个生动的介绍，因为我们可以设法处理代数。注意在一些细节和许多例子中解释过程代数问题，但是对CCS的一些熟悉当然会使本文的理解变得容易。我们推荐米尔纳首先，我们定义了基本的语法，给出了一些例子，并证明了回溯是合理的，在这个意义上，CCS和CCS-R系统具有相同的可达状态。第3节讨论了生物分子相互作用的建模，并提出了一个对CCS-R进行轻微修改的案例，称为CCS-Rμ，通过引入多作用来纠正由扩展定律引起的虚假因果依赖关系。第4节说明了CCS-Rμ在“完美混合假设”下的建模能力一个互补的接口。最后，第5节讨论了当混合不完美时会发生什么B一BC一B34诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）31确认这项工作很大程度上要归功于2003年在UniversityParis7 byVincentScha？ha？hter举办的关于生物系统的讲座;该讲座旨在让FabienTaris an在CCS-R上进行富有成效的句法讨论。2CCS-R如前所述，我们的出发点是Milner在CCS系统中，当两个智能体同时做互补的动作时，就会发生一些事情，就像握手一样进程可以尝试一些不同的同步，这是一种编写为ai.Pi;然后，该总和表示该进程执行以下操作中的任何一个的意愿：动作ai和Pi是相应的后续行为。过程可以也分为并行组件，通常称为线程;这是书面的Pi是并发运行的子进程。2.1回溯的语法Pi在哪里实现回溯的计划是为每个线程分配一个标识符，然后分配一个单独的内存堆栈来跟踪过去的通信。在执行前向转换时，回滚所需的信息必须存储在内存堆栈上。两个限制因素决定了下面解释的实际语法解决方案。首先是可靠性：反向计算不应该让人访问以前无法到达的状态;其次是表达性：记忆方案不应该在反向动作序列上引入虚假的因果依赖关系。本节只讨论第一个问题，第二个问题将在后面讨论。 在报纸上。CCS-R的语法在图中给出2和定义行动，过程和分类。一个人在记忆中记录了两种类型的事件，沟通和链接（过程定义的展开）。标识符的集合，写为U，取为N，也就是说标识符是整数的字。我们还使用以下简写符号：Mi [Pi] ui ：= M1 [P1] u1 | ... | Mk [Pk] uk.在CCS中，每个常数K都伴随着一个定义，其中P是普通CCS过程。诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）3135行动：a **=x|x¯|..... . 你 好 。 .ACTIONACHANE L| τSilent action进程：P：：= 0进程结束Σ|ai.PiChoice|Mi [Pi] ui并发线程| KConstant| (νx) PRestrictionMemories：M：：=def： K（ u）.MLinking trace| ⟨ u,a,P ⟩.MCommunication trace| ⟨⟩Empty memory图二. CCS-R2.2从CCS-R到CCS再返回。我们的演算显然只是CCS的一个φ（0）= 0Σ Σφ（ai.Pi）=ai.φ（Pi）φ（Mi[Pi]ui）=φ（Pi）φ（K）=Kφ（（νx）P）=（νx）φ（P）相反，我们可以给CCS过程配备标识符和空存储器，并使用以下U-索引提升函数族l：U ×CCS−→ CCS-R：lu（0）= 0lu （ ai.Pi ） =ai.lu（ Pi） lu（ Pi） =[lu.i（Pi）]u.ilu（K）=Klu（（νx）P）=（νx）lu（P）36诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）31令CCS-Ri= CCS-R表示具有空存储器（或处于初始状态）的CCS-R项的集合。所有提升映射的余域都包含在CCS-Ri中，并且是遗忘映射φ的后逆，即对所有u∈ U，φ<$lu是单位元。不是完全相反！变形luφ正在清除所有记忆。2.3CCS-R结构同余我们现在要定义结构全等，记作。这在语法处理中提供了一些灵活性。第一个也是最重要的原则是内存可以在子线程之间分布或共享：M[Pi]ui]u[M[Pi]ui]u（份额）与这个确保记忆机制一致性的第一个方程一起，我们负责过程定义的展开。当K：=P时，我们设置（回想一下P是一个普通的CCS过程）：M[K]u连接定义：K（ u）连接.M[lu（P）]u（link）新的语法子线程必须被标记为“在上”，例如，如果K：=（x. K+y。0个）|x′。K，then：l1（（x. K+y。0个）|x′。K）=k[l11（x. K+y。0）] 11|[1]2（x）.（K）]12=100[x. K+ y。0]11|⟨⟩[x¯. K]12，⟨⟩[K]1≡⟨d e f：K(1)⟩[⟨⟩[x. K+y。0]11|⟨⟩[x¯. K]12]1为了总结定义，我们添加了通常的CCS方程：P1|P2-P2|P1（P1）|P2）|P1|（P2）|P3）P1+P2P2+P1（P1+P2）+P3=P1+（P2+P3）P+0P（νx）P1|P2π（νx）（P1|P2）如果x/∈ P2并将结构同余定义为在所有句法结构下闭合的项上的最小等价关系，并包含上述方程。2.4转换规则有了我们的结构一致性，我们现在可以为CCS-R定义一个标记转换系统（简称LTS）。这是描述所有可能的诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）3137计算痕迹一个过程可以通过两种变迁演化：内部变迁或τ-变迁，标签形式为（u，r，τ），其中τ是沉默的动作，u，r标识了进行通信的伙伴;或者外部变迁，标签形式为（u，r，a），a是普通的动作，u标识了负责a的过程，r是上下文提供的标识符2.4.1基本规则我们首先有两个基本的过渡：u，r，aM[a.Q+P]u−→R，a，P<$.M[Q]u（com）u，r，ar，a，P（背面）人们注意到，（背）是一种沟通，也是它与（com）正好相反。为了保持系统的一致性，当且仅当通信中的另一个前伙伴愿意回滚时，才允许回滚我们有时会使用不可逆或不可回溯的动作，写为。对于这样的行为，交流根本不是记忆，人们使用简化的（com）J：u，r，aM[a.Q+P]u−→M[Q]u（com）J2.4.2语境规则我们转向语境规则的定义，解释当在语境中完成时，基本转换会变成什么。下面，当我们不再想区分foward通信u，r，au，r，au，r，a和反向交流，我们写←→表示−→或←−。u，r，aJP←→P（P）u，r，a⟨⟩[P]u←→[P]uu，r，aJu，r，aJP←→PP←→Pa/=c，c<$（面值）u，r，a（P|Q）←→（P| Q)u，r，a（νc）P←→（νc）P（res）Ju，r，aJr，u，a'JPPJJu，r，aJ J（syn）P1←→P1P2←→P2P←→QQQ（）u，r，τJ Ju，r，a（P1）|P2）←→（P1|P2）P←→Q在这些规则中没有什么值得注意的，除了（x2）规则要求保护给定线程JJ38诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）31的内存堆栈在任何涉及其子线程的操作发生之前为空该规则与（份额）一致性规则一起使用，是CCS-R系统的核心（参见下面的示例1）。诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）31391我们将写P<$p→PJ，意思是有一系列的转变，可能包括零，从P开始并导致PJ。2.5因果关系和回溯我们的转换系统中的标签与[5，4]中用于标记CCS转换的“证明项”没有什么不同引入这些证明项的最初动机是为了获得足够的信息来分析动作之间的因果依赖关系并不是在动作a之后完成的每一个动作实际上都依赖于动作a。 例如，|b和a.b可以产生计算迹a·b，但只有在后一种情况下b依赖于a，在前一种情况下a和b是并发的。一个适当的回溯机制必须执行一些隐含的因果关系分析，否则一个人可以回溯某个行动a，而不先回溯a导致发生的b因此，这可能是不足为奇的，有一个家族相似性与cacability-oriented系统。2.6分享和链接从现在开始，我们将简单地写[P]u而不是[P]u，并使用Mu来表示标识符u所标识的进程的内存堆栈。例1：需要（分享）。考虑一下这个系统：S=[x. （[y. 0 +R]11|[y'。0]12） +Q]1假设暂时1，r，xS−→S1=r，x，Q[[y. 0 +R]11|[y'。0]12]111、12、τ−→S2=r，x，Q[12，y，R[0]11|11，y<$，01，r，xJ←−S1=[x. （2012，y，R）[0]11|11，y<$，0[ ] 1内部的归约导致S2是一个问题，因为在此之后，可以回溯M1并产生对应于φ（SJ）= x的过程。（0个|0）+Q，这是从φ（S）不可达的。 限制（S）规则的要点是禁止从S1到S2的直接跃迁。除了立即回溯，只有（share）可以应用于S1：S1[r，x，Q[y. 0 +R]11|r，x，Q0]12]111，12，τ−→[12，y，R. r，x，Q|11岁，0岁。r，x，Q但是随后存储器被正确地设置，并且所获得的过程必须在撤销x上的通信之前首先回溯y上的内部通信。40诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）31示例2：（链接）的规则。现在考虑系统[K]1，其中K：=x.K+Q;如果人们可以自由地展开一个常数，而不需要在相关的记忆中跟踪它，那么我们将得到：[K]11，r1，x−→r1，x，Q<$[K]11，r2，x←−<$r1，x，Q<$[x.K+Q]11，r2，x−→r2，x，Qr1，x，Q[K]11，r1，x←− [x. （x.K+Q）+Q]1结果的过程在结构上等同于原始的过程，但是当回滚时，人们希望强制重新折叠展开的定义，这就是为什么人们在内存中记录展开。在我们的例子中，我们得到：[K]1def：K（1）[x.K+Q]11，r1，x−→ r 1，x，Q。def： K（1）K（1）K（1）n = 1，x，Q = 0. K（1）[x.K+Q]11，r2，x−→π r 2，x，Q π。K（1）K（1）n = 1，x，Q = 0. def： K（1）1，r2，x（1）K（1）n = 1，x，Q = 0. K（1）[x.K+Q]11，x，Q = 0. K（1）K[K]11，r1，x←−kdef： K（1）k[x.K+Q]1[K]1和（链接）是恢复确切的原始过程。2.7健全性既然系统已经有了明确的定义和一些例子，现在是时候证明它确实像预期的那样工作了。引理2.1（可逆性）u，r，aP∈CCS-R，P −→P中国共产党u，r，a←−P这两种影响都显示了LTS结构上的归纳。从这个∗∗我们可以直接看到：P<$→PJi <$PJ<$→P，换句话说，可访问性是一个对称关系，这是一种严格的说法，我们的过渡系统是可逆的引理2.2（合理性）u，r，aJaJP∈CCS-R，P−→P φ（P）−→φ（P）一JJ诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）3141其中−→是CCS转换。再次证明是通过归纳的LTS。42诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）31引理2.3（完备性）<$P∈CCS-R，φ（P）−a→Qu，r，QJu，r，a：P−→Q φ（QJ）=Q证明是通过P上的归纳法。定理2.4（等价性）<$P∈CCS-Ri， P<$$> →PJ<$$> φ（P）−<$→φ（PJ）请注意，P必须在CCS-Ri中才能使这个定理为真，否则一些记忆可能隐藏在P中。一个明显的例子是P = r，a，Q [0] 1，它可以回滚到r [a]。0+Q]1而φ（P）= 0，根据定义，在CCS中没有跃迁。上面的所有证明都是例行的;定理直接从引理推导出来。3生物系统的让我们结束进程代数这一章，转向生物学问题。我们首先解释我们对生物相互作用的心理图景，在此过程中，我们对我们的基本语言进行了各种修改，以使其适应表示这种相互作用的特定任务。3.1弹塑性在溶液中，可以形成几种复合物有些蛋白质是稳定的，有些则不是，但蛋白质确实不知道什么是稳定的，什么是不稳定的。因此，在我们的思维模式中，蛋白质总是试图与溶液中存在的任何互补界面结合，而自然界则试图将反应物带回原始状态。蛋白质弹性的原理如图3所示。在蛋白质的空间构型没有任何限制的情况下，例如复合或活化（见下文），它总是会折叠回其原始构型。这完全符合我们的回溯机制。隐藏站点可见站点展开一B初始配置图三. 蛋白质弹性J诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）3143磷酸受体激酶活性区活性结合域隐藏结合域一也就是说，复合并不是蛋白质改变其相互作用能力的唯一方式。它也可以被磷酸化或以其他方式激活。[3]因此也存在一定的可塑性，图4给出了这一点的说明：Bβ代表B的磷酸化状态。由于活化改变了B的自然构型，因此在解络合后它不会恢复到原来的形式。激活是蛋白质天然构型的永久变化，因此使用不可逆或不可回溯的作用来模拟它似乎是很自然的初始溶液络合活化解络合B*见图4。 蛋白质可塑性3.2适应CCS-R所有这些都需要对系统进行一些调整。第四，这种简单的CCS持续地通过n个节点和节点来实现，并且被转换为结合位点之间的二元互补关系，记为C，如果x C x j，则两个结合位点x和xJ能够彼此连接。其次，我们观察到，有时生物蛋白质-蛋白质相互作用需要在几个位点上同时连接，然后才允许另一种反应物连接到复合物上，如图5所示。将C写成（l1|L2|l3）.l4似乎是显而易见的事情，但这样的表达式不是官方语法的一部分。通常不考虑进程语法的这种扩展，因为人们总是可以依靠扩展定律来转换进程C以普通的形式。在我们的例子中，C将被扩展为l1.l2.l3.l4+ l1.l3.l2.l4+. . 不幸的是，这引入了虚假的因果依赖性。第4、5项3在磷酸化或去磷酸化过程中，磷酸盐在反应物之间交换，导致共价结合或解结合。这可能会永久改变蛋白质的状态。4 [2]中也有类似的说法[5]另一种可能性是将C定义为（νt i）（l 1.t 1| l 2.t 2| l 3.t 3|t1. t2. t3. l4），但无生物学意义。一B一B一B44诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）31活性结合域非活性结合域一CB初始解络合激活络合图五. A结合B，然后B结合C。我们可以用一个更简单的例子来说明这一点：1，r，a[a. 0] 1|[b. 0] 2−→αr，α，0 α [0] 1|[b. 0]22，s，b−→Δ r，a，0 Δ[0]1|中国，b，0[0]21，r，a←− [a. 0] 1|中国，b，0 [0] 2但在扩展[a] 1之后，|[b] 2作为a.b+b. a，上面的跟踪不再有效。 在这个特定的意义上，当涉及回溯时，扩展定律是错误的。3.3多动作因此，我们通过让进程由多组动作或多个动作来保护来不同地做到这一通常情况下，这些多集只是单例。多个动作可以以任何顺序执行和回溯。多个动作由下式给出：6多动作：μ：：= μ|（μ|a）标记的动作：γ：：=|（（r，a）|γ）帧存储器：M：：=γ; P.M打开的存储器| ⟨ γ; P ⟩.MClosed memory其中，r代表空的多重集，r是一个标识符，γ是一个具有一个作用（不是多重作用！）的对（r，a）的多重集。 一个人看到记忆现在可以打开或关闭。属于同一个多动作的动作将存储在BB一C一C诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）31456我们的多动作与Join-calculus [6，7]的模式无关，因为它们是独立同步的。46诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）31我我打开的内存的同一帧，在堆栈的顶部。请注意，由于多动作是多集，多动作γ中的动作a可以自由地相互交换。（com）和（back）规则必须相应修改：u，r，aγ; P.M[（μ|a）.Q] u−→γ|（r，a）; P.M[μ.Q] u（μ-com）u，r，aγ|（r，a）; P.M[μ.Q] u<$−γ; P.M[（μ|a）.Q] u（μ-背面）框架的打开和关闭由附加的结构方程处理：M [μ.P + Q] u /g; Q .M [μ.P] u（打开）γ; Q.M[.P]u关闭 γ; Q.M[P]u（关闭）条件是M本身在（开）方程中是闭的。如上所述，CCS-R可以嵌入到这个扩展中，我们称之为CCS-Rμ，作为γs和μs始终是单例的片段。同样，新系统只是CCS的装饰。3.4回到示例现在，我们有了所有的材料，可以对图5中概括的情况作出令人满意的表示。定义：A：=（l1|L2|l3）。0B：= 1b。0 C：=（1J|LJ|lJ）。012 3对于所有i，liClJ和lbCl4。现在我们得到以下计算轨迹：S=[A] 1|[B] 2|[C] 31、3、τJJ J−→（3，l1）;0[{l2，l3}。0] 1|[B] 2|（1，l 1）;0[{l2，l3}.l4。0]31、3、τJ JJ−→（3，l 1）|（3，l 3）;0[{l2}。0]1 | [B]2 |（1，l 3）;0 [ { l 2 } .l 4.|(1,l 3 );0[{l2}.l4. 0]31、3、τJ J J−→n（3，l 1）|（3，l 3）|（3，l 2）;0[0]1 | [B]2 |（1，l 3）|（1，l 2）;0 [ l 4.|(1,l 2);0⟩[l4. 0]3如所期望的，可以以任何顺序执行和回溯L1到LJ特别是（1，l j）中的任何标记动作|（1，lJ）|（1，l，J）可以触发反向1 3 2过渡 最终络合通过以下获得：2、3、τJ J J诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）3147−→n（3，l 1）|（3，l 3）|（3，l 2）;0[0]1|（3，l b）;0|（2，l 4）;0. （1，l 1）|（1，l 3）|（1，l 2）;0[0]348诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）31I24CCS-R表现力更复杂的生物学情况可以被代表。在这里，我们形成了一个系统，其中蛋白质的转录是由不同的反应物之间的竞争控制回溯和多动作都是需要的。在基因转录开始之前，一个复杂的蛋白质机器，由A表示，必须在DNA链上的基因上游结合。在我们的例子中，有两种抑制剂：I2与A竞争结合DNA上的同一位点，I1阻止DNA链正确折叠。图6概括了这种情况。以下是CCS-Rμ中的表示：初始状态我比状态1Bx y zy x基因序列DNA链状态12我基因表达一比比I2基因未表达B'X'z'BI1A基因未表达状态2状态13见图6。 基因表达A：=（x|y|b. EXPDNA：=[（xJ|yJ|zJ）。0] 11|[（bJ. EXPJ+ iJ。0）] 12I 1 ：= i. 0I 2：= y。0其中EXP和EXPJ是处理基因表达阶段的常数，并且共域关系C使得（x，xJ）、（y，yJ）等在C中。假设初始解为：S=[DNA] 1|[A] 2|[I 1] 3|[I 2] 4，B一I1一诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）3149我们在这里有一个可能的计算轨迹：11，2，τJJ JJ J JS −→（2，x）;0[（y）|z）。0]11|[b.EXP|（1，x）;0[（y）|z）.b.EXP] 2| [I 1] 3| [I 2] 4+i . 0]1211、4、τJ JJJ J J−→（2，x）|（4，y）;0[z .0]11|[b.EXP|（1，x）;0[（y）|z）.b.EXP]2| [I 1] 3| ⟨(1,y);0⟩[0]4+i . 0]1211、2、τJ JJJ J J−→n（2，x）|（4，y）|（2，z）;0[0]11 |[b.EXP|（1，x）|（1，z）;0[y.b.EXP]2| [I 1] 3| ⟨(1,y);0⟩[0]4+i . 0]12为了清楚起见，在该运行中没有追踪连接，[ ]1支撑DNA也没有按照它应该的那样沿着运行重复在这个阶段，A和I2都与DNA结合，其中一个必须断开（回忆一下引言中的例子假设I2先放手，那么计算可以这样进行：11、4、τJ JJJ J J←−（2，x）|（2，z）;0[y .0]11|[b.EXP|（1，x）|（1，z）;0[y.b.EXP]2| [I 1] 3| ⟨⟩ [y. 0]4+i . 0]1211、2、τJ JJJ J J50诉Danos，J.Krivine/Electronic Notes in Theoretical Computer Science 180（2007）31−→n（2，x）|（2，y）|（2，z）;0[0]11 |[b.EXP|n（1，x）|（1，z）|（1，y）;0[b.EXP]2| [I 1] 3| ⟨⟩ [y. 0]4+i . 0]12