项图重写：X演算的实现模型与Curry-Howard对应

理论计算机科学电子笔记127（2005）171-195www.elsevier.com/locate/entcs执行XSte Escheren van Bakel和Jayshan Raghunandan伦敦帝国理工学院计算机系摘要本文提出了一个术语图重写系统作为X演算的实现，X演算是一种无替换语言，可用于在非常低的粒度级别上描述函数式编程语言的行为，并且在[10，1]中首次定义。 由于演算有绑定的概念，因此在共享的上下文中引入了重新绑定的概念， 避免名字的双重绑定。保留字：项图重写，X-演算，lambda演算，Curry Howard对应介绍本文将提出一个项图重写的概念，作为（无类型）演算X的实现模型，该演算首先在[10]中定义，后来在[1]中得到了广泛的研究。X的起源在于寻求一种语言，旨在为经典逻辑的微积分提供Curry-Howard对应，特别是在[12]中。X被定义为一种无替代的编程语言，也许令人惊讶的是，它非常适合在非常低的层次上描述函数式编程语言的行为，并且在[10]中被定义。文[1]详细研究了它与λ演算和显式代换演算λxCurry-Howard性质将可类型程序和可证明定理紧密联系在一起，可以理解为：1 电邮地址：svb@doc.ic.ac.uk，jr200@doc.ic.ac.uk1571-0661 © 2005由Elsevier B. V.出版 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.025172S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171（C rury-HOWARDISOMORPHISM）设M是项，A是类型，则M是类型A当且仅当读作逻辑公式的A在相应的逻辑中可证明，使用一个结构对应于M的证明。一个典型的蕴涵经典逻辑可以定义为：rα：A，r，A（Ax）：Γ，Aα：A，（cut）：rα：A，r r，BΓ►∆Γ，Aα：B，（LI）：Γ，A→B（RI）： ΓA→B，在这种同构中，在项的演算中的归约和证明的规范化之间存在着很强的关系，也被称为割消。就Curry-Howard同构而言，X的突出之处在于它是第一个完全实现经典逻辑的演算。例如，在λµµ中，所有可提供的命题都可以被占据，但不是所有的项都对应于证明，并且在λµ中，不是所有的证明都可以被表示，因为那里的归约是连续的。与此相反，在蕴涵经典中，逻辑不是。从该领域的不同方法出发[9，12]，在[10]中引入了微积分X，并表明在表达性方面与[9]的λµµ-c计算是等价的。使用这种对应关系，可以为λμ μ π ι显示强归一化结果。 在fact[1 0]中，以及[1 2]，没有研究无类型X的任何propery，但只关注与微积分有关的类型方面; [12]开始研究证明的结构，因此那里的术语携带类型并对应于证明。在X中，我们研究没有类型的项，并且放弃了项应该完全表示逻辑证明的条件：我们研究纯演算。当把X作为一种非类型化语言来研究时，一些意想不到的特殊属性浮出水面：很明显，X提供了一种优秀的通用机器，非常适合编码各种演算（详细信息，参见[1]）。在该论文研究的演算中，显式替换演算λx脱颖而出，X通过将显式替换分解为更小的分量提供了“亚原子”水平。而且，微积分是可解的[3];由（Pα^fx^Q）表示的“cut”在某种意义上表示P对Q中x的显式替换，也表示Q对P中α的显式替换。也许X的主要特征是它构成了一种变量和无替换的计算方法. 在X中，符号x代表一个套接字，一个项可以通过一个插头α连接到该套接字上，而不是像x这样的变量代表可以插入项的位置。的定义S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171173对X的约简很好地显示了两者之间的相互作用是如何微妙而温和地通过项进行简化的。此外，虽然X的起源是一个逻辑，并且人们可以期望它接近LC，但它实际上是通过重写规则指定的条件项重写系统，这些重写规则指定如何使用特定结构的项来构造新项。这一观察结果是编写本文件的原因。在X的重写规则中，唯一的非标准方面是绑定的概念，它处理三种不同类别的开放节点（插头、插座和电路）。从这个观察开始，我们决定使用术语图重写技术为X构建一个解释器;我们开始为X构建一个通用的归约工具，针对编程语言的感兴趣的研究人员该工具允许用户不仅输入X中的术语，还可以输入LC中的术语，使用后者到X中的解释，如[1]所述。本文件报告了该分类的初步发现。口译员可在http://www.doc.ic.ac.uk/~jr200/XTool并且实际上是高度复杂的工具的一部分，其允许用户几乎绝对控制还原引擎，选择子系统、策略和切割以随意还原。在测试解释器的初始实现时，发生了非法的reduction行为。分析了归约引擎产生连接符“双重绑定”的问题。根据术语图重写的性质，在引擎中不仅在所涉及的电路上，而且在它们的连接器上引入共享，其中将“绑定”边从绑定出现添加到绑定出现。虽然共享初始项的图形解释仅限于此“绑定”链接，但在约简后不再需要这种情况。不仅电路可以共享，连接器也可以以更多的方式共享;归约引擎实际上生成了“双”绑定，即多个绑定边以单个连接器节点结束。连接器的绑定在共享的上下文中是有问题的，就像在lambda图的上下文中共享对于抽象是有问题的一样[13]。为了解决这个问题，本文提出的解决方案将在X项图中引入辅助结构，并在约简系统中加入重绑定的概念。这个想法是“剥离或复制”的图形，这可能会得到一个连接器的双重绑定的干扰。这种方法的原理类似于[13]，但是，正如此后许多论文所指出的那样，这种方法限制性太强，可以改进。在本文中，我们将介绍一个解决方案，只需要剥离或剥离“位于再次使用的连接器上方”的结构所有其他共享可以174S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171y）Pβ α）保持完整1X演算在本节中，我们将给出X-演算的定义，正如[1]中详细研究的那样它具有两个独立的“连接器”类别定义1.1 [1] X-演算的回路由以下语法定义，其中x，y，. 在无限组插座上的范围，以及在无限组插头上的α，β。P，Q：：= 1x。α⟩|y^Pβ^·α|Pβ^[y]x^Q|Pα^<$x^Q在这个定义中，“·”象征着下面的插座或插头被束缚在电路中。这自然导致了以下关于电路P中自由插座fs（P）和自由插头fp（P）的定义。定义1.2电路中的自由插座和自由插头定义为：fs（fs）α= {x}fs（x^Pβ^·α） =fs（P）\{x}fs（Pα^[y]x^Q）=fs（P）<${y} <$fs（Q）\{x}fs（Pα^^x^Q）=fs（P）<$fs（Q）\{x}fp（fax. α）={α}fp（x^Pβ^·α） =（fp（P）\{β}）<${α}fp（Pα^[y]x^Q）=（fp（P）\{α}）fp（Q）fp（Pα^fx^Q） =（fp（P）\{α}）自由连接线的集合是这些连接线的并集：fc（P）=fs（P）<$fp（P）。非自由的连接器（插座或插头）称为绑定。像往常一样，我们将识别仅在绑定连接符（α-转换）的名称中不同的过程我们在电路中使用以下术语：fixx。αn称为胶囊，（y^Pβ^·α）称为出口电路，（Pβ^[y]x^Q）称为介质，（Pα^fx^Q）称为切口。我们用图表表示这些电路：x）的α）y）Pβx）[]）QP α）xQS. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171175X的电路可以看作是一组导线，每一条导线都有一个输入和一个输出。当两个回路交互时，它们只通过一个输入和一个输出名称来进行交互 ， 这 些 名 称 在 交 互 中 绑 定 。 这 种 相 互 作 用 可 以 通 过 一 个 回 路（Pα^fx^Q）来表示，它将试图将称为P的回路中以α结尾的线路连接到称为Q的回路中以x开头的线路。 另一方面，他们可以beboundasin（Pβ^[y]x^Q），其中x表示两个试图连接的电路以β结尾、以x开头的连线，但这需要另一个回路在它们之间进行调解;这个新回路将需要通过输入名称y（也可能出现在P和Q中）进行交互。而且，可以使愿意经由连接器y和β交互的电路P本身可用（导出）通过名称α，asin（y^Pβ^·α）.在任何给定的时刻，电路中所有未连接的输入和输出组成了在计算步骤中不活动的自由连接器的集合;绑定连接器都参与了一些相互作用。由下面的归约规则定义的微积分，详细解释了切割如何通过电路分布，最终在胶囊级进行评估。约简是通过给出良好连接的基本语法结构如何相互作用来定义的，并指定如何处理将计算中的活动节点传播到它们可以相互作用的点定 义 1.3[ 归 约 ： 逻 辑 规 则 ] （ cap ） ：归 约 。 αα^<$x^x 。ββ→βγ。β⟩（ex p）：（y^Pβ^·α）α^fx^fx. γε→γ^Pβ^·γ，α/∈fp（P）（m ed）：darry.α<$α^<$x^（Qβ^[x]z^P）→Qβ^[y]z^P，x/∈fs（Q，P）（单位s）：（y^Pβ^·α）α^†x^（Q^γ[x]z^R）→.Qγ^<$y^（Pβ^<$z^R）（Qγ^<$y^P）β^<$z^R.α/∈fp（P）x/∈fs（Q，R）这些规则的图解表示如图1所示。上面的前三个逻辑规则指定了重命名（重新连接）过程，而最后一个规则指定了基本的计算步骤： 通过唯一插头α可获得的功能，连接到连接唯一插座x的中介器电路中的开放相邻位置。注意，这些规则被指定为条件项重写系统;非标准方面是连接器的绑定，它处理三个不同类的开放节点（插头，插座和电路）。该语法扩展了两个标记的或活动的cut：P：：=. . .|P1α^x^P2|P1α^x^P2从限制语法中构造的没有这些标记削减的术语是176S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171►年）的 β）γ）yβz年）的 α）α）xx）Qβ）[]z）P► ）Q）[]）P⎧⎪⎨► ⎪⎩Fig. 1. 逻辑规则的数学表示被称为纯的（标记的切割的数学表示与未标记的切割的数学表示相同）。当上述逻辑规则不适用时，会产生这些标记的切割，并且在处理胶囊时会减少到正常切割，或者通过电路传播定义1.4[还原：激活切割]我们定义了以下两个激活规则。（act-1）：Pα^fx^Q→Pα^（act-R）：Pα^fx^Q→Pα^x^QifPdoesnotintroducex^QifQdoesnotintroducex其中：Pint tr=Qα^[x]y^R且x f ∈fs（Q，R），或P=∞x. δ0。P_i=x^Qβ^·δ且δf ∈fp（Q），或P=f ∈x. δ0。引入激活的割（注意，激活只可能是逻辑规则不能应用的割）以获得微调的归约系统。一个被激活的切割是通过系统地“推”它来处理的，然后，切割被停用，使得可以应用逻辑规则，否则，年）的α）α）xx）β）y）P））α）x ）的β αXγy）Pβy）P β）α）α x）X）Q））Rγ[ ]zQγ y）P βzR）QγyP）β）zR⎪►⎪S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171177定义1.5[约简：传播规则]左传播（dL）：不规则的。α⟩α^（L1）：不确定性。β⟩α^x^P→y。αα^<$x^Px^P→y。ββ/=α（L2）：（y^Qβ^·α）α^（13）：（y^Qβ^·γ）α^x^P→（y^（Qα^x^P→y^（Qα^x^P）β^·γ）γ^^x^P， γfreshx^P）β^·γ，γi=α（14）：（Qβ^[z]y^P）α^x^R→（Qα^ x^R）β^[z]y^（Pα^x（R）（15）：（Qβ^fy^P）α^右传播x^R→（Qα^ x^R）β^<$y^（Pα^x（R）（dR）：Pα^（R1）：Pα^x^x。β→Pα^<$x^<$x。β⟩x^y。ββ→βγ。β=y=x（R2）：Pα^x^（y^Qβ^·γ） →y^（Pα^x^Q）β^·γ（R3）：Pα^x^（Qβ^[x]y^R）→Pα^<$z^（（Pα^x^Q）β^[z]y^（Pα^x^R））zfresh（R4）：Pα^x^（Qβ^[z]y^R）→（Pα^x^Q）β^[z]y^（Pα^x^R）zx（R5）：Pα^x^（Qβ^<$y^R） →（Pα^x^Q）β^<$y^（Pα^x（R）对于由这些规则（16）导出的（自反、传递、相容）归约关系，我们写作→直觉上，X的减少将连接插座和插头。在这种观点下，计算Pα^fx^Q表示α在P中的所有出现和x在Q中的所有出现之间的必然联系。在某些情况下，这些事件是唯一的，并且在顶部（即被引入），并且连接这很简单，逻辑规则处理这些问题。如果不是这种情况，则必须“查找"连接器带着这个 左前降支，即运行Pα^ x^Q，将产生所有178S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171P中的α的出现将连接到Q中的x;类似地，右propa-gation，即运行Pα^ x^Q，将使x的所有发生都在Q将连接到P中的α;注意这两个运算不需要有相同的结果，特别是如果P中没有α或Q中没有x。繁殖行为可分为两个阶段.首先，切割在一个方向上传播，直到遇到它可以连接的电路，即在最外层显示连接器的电路。这是规则（l2）和（r3）正式描述的情况如果这个回路是非平凡的（有子回路），需要发生两件事：首先，需要处理所展示的连接器的所有（可能）事件，这是通过传播到所有子回路来完成的;其次，新的切割将处理剩下的一个事件。由于最后S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171179现在可以假设出现是唯一的（所有其他的都将由传播处理），所得到的结构现在可能是逻辑切割;由于这个原因，附加切割是不活动的。在某种意义上，在传播的该第二阶段中，新剪切重新评估其在规则（L2）和（R3）中，我们重命名以避免α（x）同时出现束缚和自由;但事实上，不可能混淆，因此这里的α转换几乎是装饰性的。由于X上的归约关系→模仿逻辑割消（完全），所以它不是连续的;这实际上来自于在两个时间段内作用于割Pα^fx^Q的临界对，如果Pdoe不是在割α中，并且Qdoee不是引入x。当根据第一个标准激活时，归约将把P中的所有α与Q中的连接符x连接起来;如果α没有出现在P中，这将返回P。当使用第二个时，归约将把Q中的所有x与P中的连接符α连接起来;如果x没有出现在Q中，这将返回Q。作为示例，考虑（当β γ，且yi=z时）⎧^（x）^（x）α<$α^·γ）β^z^hey. δα→δγ。δ⟩（x^x. α<$α^·γ）β<$z^y。δ⟩→⎩（x^x.α<$α^·γ）β^z^hey. δ0→x^<$x。αα^·γ因此，如果两个方向的激活都是可能的，那么还原的最终结果可能是不同的。在[1]中，引入了两种策略，只要出现上述关键对，它们就明确支持一种激活：定义1.6[按名称调用和按值调用]• CBV策略只允许在有两种激活方式的情况下激活切割via（act-L）;在这种情况下，我们写P→VQ• CBN策略只允许通过（act-R）激活这样的切割;然后我们写P→NQ。定理2.3给出了术语的定义。在[1]中，给出了一些基本性质，这些性质基本上表明该演算是行为良好的，以及X与许多其他演算之间的关系。这些结果促使制定新的规则：180S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171引理1.7（[1]）下列归约规则是可容许的：（gc-1）：Pα^（GC-R）：Pα^x^Q→P若α/∈fp（P）， P为x^Q→Q如果x/∈fs（Q）， Qpure（ren-1）：Pδ^tz^tz. αβ→P[α/δ]Ppurere（ren-R）：z. α<$α^<$x^P→P[z/x]Ppure后两者可以作为重命名规则引入X的归约引擎。其结果类似于α-转换，因为我们必须在整个术语中重命名绑定连接符的所有出现，尽管绑定出现本身消失了。然而，这些规则也有危险，因为它们实际上对表示P的图执行了破坏性的更新。只有当我们能够保证没有其他的对P的引用时，这才是合理的。这个问题与lambda图的情况非常相似，其中涉及两个应用程序的抽象必须复制。 这个问题也许可以通过在减少引用时跟踪引用计数来避免，或者通过抽象的编译时分析来避免。这是一种独特的精神类型[7]。然而，鉴于这种困难，重命名规则暂时从工具中省略2与Lambda演算在本节中，我们将简要强调LC和X之间的关系。我们假设读者熟悉LC[4];我们只记得lambda项和β-压缩的定义。定义2.1[λ项和β-收缩[4]](i) lambda项的集合Λ由语法定义：M：：= x| λx.M|M1M2(ii) 约简关系→β被定义为规则的上下文（即兼容[4]）闭包：（λx.M）N→βM[N/x]n→→β是→β的反交闭包，=β是y→→β生成的等价关系我们现在定义λ-项到X的直接编码。2.2定义[[1]]通过插塞α将λ-项解释为X，S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171181[[（λx.xx）（λy.y）α=[[λx. xx {\displaystylex}{\displaystylex}}{\displaystyle x}{\displaystylex}}{\displaystyle x}{\displaystyle x}}{\displaystylex}{\displaystyle x}}{\displaystyle x}{\displaystylex}{ yγ^γ[z]v^v. α）=（x^[[x^·β）β^<$z^（[[λy. yγ^γ[z]^vv. απ） →（ins）[[λy. y<$$>γ^<$x^（[[xx<$$><$$>v^<$v. α） =[[λy. yγ^<$x^（（x. γγ^<$z^（λx. δδ^[z]w^w。^. α）→（REN-L），（REN-R），（ACT-R）[[λy. yγ^γx^（？x. δδ^[x]w^w。αα）→（R3）[[λy. y<$$>γ^<$z^（（[[λy. yγ^γx^x。δ）δ^[z]w^（[[λy. yγ^γx^w. α））→（dR），（REN-R），（r1）[[λy. y<$γ^γ <$z^（[[λy. yδ^[z]w^w. α）=（y^y.µµ^·γ）γ^<$z^（[[λy. yδ^[z]w^w. απ）→（ins）[[λy. yδ^<$y^（y. 你好。αα）→（cap），（ren-R）[[λy.y]图 二、 （Symbol i caly）reucing[[（λx. xx）（λ y. y）α到[[λ y. yα。[1][2][3][4][5][6][7][8][9][10][11][12][12][13][14][15][16][17][18][19][19][10][19][10][10][19][10][10][11][10][10][11][10][10][11][10][11][10][10][11][10][11][11[[x]α=x。α⟩[[λx.Mα=x^[[Mβ^·α，βfresh[[MNα=[[Mγ^<$x^（[[Nβ^[x]y^<$y. αα），x，y，β， γfresh注意，[[Mα]的每个子项都有一个自由插塞。在图2中，我们展示了过程[[（λx.xx）（λy.y）α如何使用上面给出在[1]中，在LC和X中的（按名称调用，按值调用）减少之间示出了以下关系：定理2.3（[1]）（i）若M →βN，则[[Mα→ [[N α.(ii) 如果M → VN，则[[Mγ→ V[[N γ。(iii) 如果M → NN，则[[Mγ→ N[[N γ。最后两个结果将“名”和“值”的概念很好地与X联系起来一个插头，一个名字是一个引入插座的电路。然而，请注意，与LC相反，在X中CBV182S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171约化不是CBN约化的子系统;对于后者，也许应该使用另一个概念而不是注意，对于X上的r→V的概念，在计算Pα^fx^Q时，S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171183如果Q不引入x，且P是一个值，则cut是右激活的。 所以，P只 有 当Q是一个值时，它才被“插入”到Q中，这使得这种归约被合理地称为“按值调用”。定理2.3的结果的逆命题不先验地成立：这主要是因为X中的归约关系远比λ项（的解释）之间的那些归约复杂得多，并且它可能是在[[M<$N <$N α]和[[M <$N <$N α]之间存在一条路径，它不对应于M和N之间的LC-归约路径。3X语言的项图重写系统X的解释器的实现当然可以用传统的方式完成，通过字符串归约机。选择使用术语图重写的动机主要是观察到X的归约规则形成了一个条件术语重写系统;对于一般的术语重写系统，术语图技术提供了最佳的实现平台。这就产生了一个封装解释器的工具，http://www.doc.ic.ac.uk/~jr200/XTool。这个工具实际上是非常复杂的，允许的不仅仅是减少电路;它允许用户几乎绝对控制减少引擎，扩展规则集，选择子系统，策略和削减来随意减少。它提供了一种探索X的优雅方法，完全绕过了“手动”运行电路的需要。最终产品的优雅不仅是通过彻底的工程实现的，而且还通过TGRS形式主义的美丽，它允许对运行X所需的还原引擎进行高层次的规范和理解。应用的技术是[11，5，6]的标准匹配，构建，链接，重定向和垃圾收集方法，其中术语和重写规则被提升到图形。通过提升的过程，连接器在生成的图中只出现一次，这立即引入了共享。重写规则也变成了具有两个子图的图，每个子图都有一个根，并且通过共享的叶子联合起来。定义3.1[项图]X项图由以下语法定义G：：= Cap（x，α）|切割（G1，α，x，G2）|Exp（y，G，α，β）|中位（G1，α，y，x，G2）184S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171[[x]G= x|∅⟩[[α♩♩G=⟨α|∅⟩[[100]αG=r |{r = Cap（r1，r2）}<$G1<$G2<$，其中，|G1=[[xG，第二次世界大战|G2=[[αg，[[Mα^<$x^N]][G= r]|{r= Cut（r1，r2，r3，r4）} <$G1<$G2<$G3<$G4<$whe r er1|G1=[[M G第二次世界大战|G2=[[αG第三章|G3=[[xG第四章|G4=[[N G[[y^Mα^·β]G= βr|{r= Exp（r1，r2，r3，r4）} <$G1<$G2<$G3<$G4<$其中，|G1=[[yG第二次世界大战|G2=[[M G第三章|G3=[[βG第四章|G4=[[αG[[Mα^[y]x^N]\^G=\\r|{r=Med（r1，r2，r3，r4，r5）} <$G1<$G2<$G3<$G4<$G5<$whe r er1|G1=[[M G第二次世界大战|G2=[[αG第三章|G3=[[yG第四章|G4=[[xG第五章|G5=[[N G图三. X项的图形解释它对应于（有序）图帽xα切割G1G2α x实验βy αGMedG1G2αyx（请注意，我们不需要使用帽子，因为可以立即清楚哪些连接器是绑定事件）定义3.2 [图形解释]对于每个项M，M的图形解释[ [ M]]，（使用[8]的符号）在图3中定义。定义3.3将X归约规则提升到项图重写S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171185（L2）：（y^Pβ^·α）α^x^Q→（y^（Pα^x^Q）β^·γ）γ^fx^Q，γfresh阿尔布尔河|{r 1= CutL（1，2，3，4）1 =Exp（5， 6， 7， 2）2=α3=x4 =Q5 =y6 =P7 =βyrr=Cut（8， 9， 3，4）8 =Exp（5， 10，7， 9）9 =γ10 =CutL（6， 2，3，4）rlrrCutL切割CutL（Exp（5：y，6：P，7：β，2：α），2， 3：x，4：Q）→切割（Exp（5，CutL（6， 2， 3， 4），7， 9：γ），9， 3， 4）γ新鲜见图4。 规则（l2）的各种项图表示。规则现在表示为：[[left → right]左→右|Gl Gr其中，|G l =[[左G布雷尔河|G r=[[右G使用这种解释，对应于（L2）和（R3）的术语图规则如图4和图5所示（写作n而不是rn）。当然，在我们的（扩展的）tgr中解释术语和归约规则的为此，我们需要定义一个解开的概念：定义3.4Unrav（G），X项图G的解开是通过自上而下遍历图（注意我们没有循环结构），并复制所有共享图中所有不是自由连接器的节点来获得的。这个定义显然取决于入度，即进入节点的弧的数量。这个概念没有包含在我们这里使用的图的定义中，但是可以很容易地修改。使用这个概念，我们现在可以证明以下充分性结果：定理3.5设G1，G2是X-项图，P1，P2是X-圈，使得Unrav（Gi）=[[Pi] ∈[g]，其中i = 1，2.如果使用项图规则G1→G2，则P1→ P2. 而 且 ，如果G2是正规形式，那么P2也是正规形式.实验αX Q实验γPβCutL186S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171证据很容易证明存在一个G3使得[[P2]G= Unrav（G3）且[[P1]G→G3.这种减少导致从P1到P2的减少。如果G2不包含割，则[[P2]]也不包含割，P2也不包含割。 Q事实上，上面定义的术语图重写系统就是为了满足这个性质而建立的。反之则不成立，因为在术语图重写引擎中共享的本质。然而，以下部分可靠性结果应该成立：推论3.6若P → Q，则存在R使得Q → R且[[P]→ [[R]] → [R]]。4执行问题X的功能策略被发现可以通过TGRS中规则的有序列表上的严格第一匹配策略如定义1.6所建议的，按名称调用策略（CBN）是通过规则的排序来实现的，其中（act-R）出现在（act-L）之前，而按值调用策略（CBV）是通过优先（act-L）来实现的。在可以以任何方式激活切割的情况下，此策略确保应用遇到的第一个规则。在TGRS重写引擎中实现共享几乎不需要额外的关注，因为节点重定向只涉及指针更新和引用计数的增加/减少;字符串归约机将涉及术语的内部复制机制的实现。另外，从来不需要在术语图中搜索绑定连接器的位置，因为节点的任何绑定都是共享的。TGRS方法被证明是微积分的一个很好的学习工具，允许用户可视化每个简化步骤。用户可以清楚地看到切割被传播到子图，并且阿尔法转换通过重新绑定节点发生。在这个实现中需要解决的主要问题是X知道绑定连接器。与LC[13]的情况类似，在共享的上下文中，绑定被认为是有问题的因此，在解释术语和将规则重写为图表时，必须要注意一些。示例4.1以下列电路为例（y^hey. µµ^·γ）γ^<$x^（µx. δδ^[x]w^w。α）S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171187帽切割Med帽Xδ（R3）：Pα^x^（Qβ^[x]y^R）→Pα^<$z^（（Pα^阿尔布尔河|{r 1= CutR（1，2，3，4）1 = P2 =αx^Q）β^[z]y^（Pα^7 =y8 =R9 =zx^R）），xfresh3 =x4 =中（5、 6、3、 7、 8）5 =Q6 =βrr=Cut（1， 2， 9， 10）10 =中（11， 6， 7， 9， 12）11 =CutR（1， 2， 3， 5）12 =CutR（1， 2， 3，8）rlrrCUTR切割PMedMedα x Q R zCutRCutRβ yCutR（1：P，2：α，3：x，Med（5：Q，6：β，3， 7：y，8：R））→切割（1， 2， 9：z，中位（CutR（1， 2， 3， 5），6，9， 7，CutR（1， 2， 3， 8）图五. 规则（r3）的各种项图表示。表示该电路的图形为Expγ帽W αy µ应用术语图规则（act-R）和（R3）将生成188S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171（y^hey. µµ^·γ）γ^<$z^（（y^<$y. µµ^·γ）γ^x^x。δ）δ^[z]w^（（y^y.µµ^·γ）γ^x^w.α））S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171189Expδ帽帽α应用项图规则（dr）、（exp）和（r1）将生成（y^y）。µµ^·γ）γ^<$z^（（y^<$y. µµ^·δ）δ^[z]w^w。α）帽α从这个图中可以清楚地看到，左边的胶囊现在是共享的，并且有两个绑定到y和µ的绑定器，来自两个导出节点。继续执行此图（通过规则的第一个变体（ins）），（y^hey. µµ^·δ）δ^<$y^（y. 你好。α）切割切割y µ帽W α注意，在这个图中引入了δ，而y没有，所以这个图简化为（（y^y。µµ^·δ）δ^y^y。µ⟩) µ^†w^⟨w. α⟩切割Exp Medγ zCutRCutRCap帽x δ wy µ切割ExpMedγ zExpCapδ wy µ190S. van Bakel，J.Raghunandan/Electron.注意Theor。Comput. Sci. 127（2005）171切割Expδ帽Exp帽实验σ切割帽帽切割帽W αy µ顺便说一下，如果我们应用规则（ins）的第二种变体，这就是我们从上图中得到的结果注意，现在有两个嵌套的绑定到µ。我们可以假设最里面的束缚力最强，所以左边的自由μ被最里面的束缚，右边的自由μ被最外面的束缚，但这并不能解决这里的矛盾。如果我们现在首先使用（exp）减少内部切割，我们得到（y^hey. µ⟩µ ^·µ) µ^†w^⟨w. α⟩切割帽W αy µ请注意，最右边的自由µ被最外面的绑定器绑定，但重写规则将生成错误的图形。为了减少切割，我们首先检查是否引入了μ;这不是这样的，因为μ∈fp（Cap（y，μ）），从而否定了规则（exp）的预期应用。相反，我们传播切割并使用规则（act-1）、（L2）和（dL）获得，（y^（y. 你好。α）μ^·σ）σ^<$w^w. α⟩切割y µ w α