多重代数的不等式演绎系统及其应用

理论计算机科学电子笔记72（2007）31-44www.elsevier.com/locate/entcs作为项图重写的不等式演绎1Andrea Corradini2 和法比奥·加杜奇2DipartimentodiInformatica，Universita`diPisa，ItalyWolfram Kahl3加拿大麦克马斯特大学计算机与软件系BarbaraKéonig4在德国慕尼黑大学，摘要多重代数允许在代数框架中通过将运算符解释为从单个参数到可能结果集的函数来建模非确定性。我们提出了一个简单的不等式演绎系统，根据长期图，推断包含衍生关系的多代数，我们表明，长期图重写提供了一个健全的和完整的实施。保留字：多重代数，不确定性，不等式演绎系统，项图重写1引言在过去的二十年里，代数规范技术在处理不确定性方面的扩展是众多文献的主题（参见[10]的概述）。人们认识到，非确定性不仅出现在本质上非确定性系统的具体化中，如并发系统，而且当系统是确定性的并且人们想要抽象时，1这项工作得到了意大利MIUR项目COMETA（计算元模型）的部分支持;并得到了欧盟在FET-流动性）。供资机构不负责对本文所列结果的任何使用。2 电子邮件：{andrea，gadducci}@ di.unipi.it3电子邮件：cas.mcmaster.ca4 电子邮件：in.tum.de1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2002.09.00432A. Corradini等人/理论计算机科学电子笔记72（2007）31远离实现细节，或者通常远离对于系统的完整描述所必需的信息（如定时考虑、状态的内部等）。许多非确定性的规范化技术的扩展都努力做到非侵入性或保守性，即它们试图不改变确定性规范的现有框架，特别是当只考虑确定性操作时，它们简化为标准理论[11]。这一事实可能解释了多重代数在其他代数方法中的成功，例如例如幂代数。推广标准部分代数，在多重代数中，签名的算子被解释为从单个参数到可能结果集的函数。然而，关于（在）等式规范的演绎系统的问题问题是句法性质的，它们与所谓的缺乏替代性密切相关。粗略地说，这意味着在自由变量的替换下，项等价性不被保持。这一事实表明，Gested寻找替代表示的衍生运营商在一个多重代数，以及发展特设推理系统。文[2]给出了多重代数的函子语义，推广了代数理论中的经典结果一个附带的结果是精确地描述了一个简单的语法设备，用于在多代数规范中表示导出算子，即通过项图。事实上，共享的概念，这是隐含在框架中，允许直接表示非决定论和域限制，从而获得一个有效的工具，在这种情况下的具体化。在本文中，我们更进一步，提出了使用不等式的基础上，长期图指定之间的包含派生关系的多代数。我们提出了一个演绎演算这样的不等式，证明其可靠性（而其完整性仍然是一个开放的问题）。 更有趣的是，我们证明了图重写[9]提供了不等式演绎的充分实现在这个意义上，F±G可以被推导出当且仅当F重写为G。 这提供了项图重写的原始应用，本文根据DAG2多重代数与关系将签名运算符解释为关系允许在代数框架中对某种非确定性行为进行建模[10]。对于多重代数，与运算符相关的关系是将每个输入值映射到一组（可能的）输出值的函数。很明显，这等价于通常把关系定义为直积的子集。定义2.1（关系）设A和B是两个集合。 A关系R：A参与B是一个函数R：A→ P（B），其中P是幂集算子。 关系是A. Corradini等人/理论计算机科学电子笔记72（2007）3133总计，如果|R（a）|对于所有a∈A ≥ 1;它是单叶（泛函）的，如果|R（a）|对所有a∈A ≤ 1。给定两个关系P，R：AParticipateB，P包含在R中（记为P<$R），如果对所有a ∈ A，P（a）<$R（a）。因此，一个单叶关系是一个部分函数R：A-B，而一个单叶和全关系只是一个函数R：A→B。我们将考虑下列关系运算。定义2.2（关于关系的并集和合成）对于一个集合A，设Ai表示A的i个副本的直积。给定两个关系P：AjParticipateAi和R：AlParticipateAk，它们的 并集是关系 P<$R： Aj+lParticipateAi+k，定 义为 P<$R（Aj1 ，. aj+lj）={kb1，. bi+k|1、... bi∈P（na1，. aj）bi+1，. bi+k <$∈R（kaj+1，. aj+l）}。给定两个关系P：A Participate B和R：B Participate C，它们的复合P;R：A Participate C表示由P与R +复合得到的关系：P（B）→ P（C），R的加法扩张。为了简单起见，在整个论文中，我们将我们的分析限制在一个排序的签名上，我们用一个任意固定的签名来表示。定义2.3（多重代数）一个（有限）签名上的多重代数A =i∈N <$i是一对|一|，ρA，其中载体|一|是一个集合，且ρA={fA|f∈ H}是一个关系族，使得对于每一个f∈ f i，fA：|一|参与|一|.此外，我们定义性（f）=i i <$f∈<$i，对所有的算子f∈<$。3术语图重写本节介绍了术语图和[1]中的一些操作，以及术语图的重写。为了避免可能的混淆，让我们设想我们将考虑三种不同类型的(i) 有向无环图（DAG 's）是最基本的图：我们将引入它们所在的范畴DAG，“项图重写”将根据该范畴中的双推出方法来定义。(ii) 排名DAG的是dag的配备有选定的根和变量节点。(iii) 项图是秩DAG虽然DAG事实上，它们将需要用于构造多代数规范的导出算子。定义3.1（有向无环图和态射）有向 无 环图（DAG）（在n上）是一个三元组d= nN（d），ld，sdn，其中N（d）是一组节点，ld：N（d）-n n是一个称为标记函数的部分函数，sd：N（d-N（d）n是一个称为后继函数的部分函数，满足以下条件：• dom（d）=dom（s）;34A. Corradini等人/理论计算机科学电子笔记72（2007）31RR=（dL（lGdKrK（d）HvdG（dV VdDb）dH图1. 重写步骤为双推出结构。• 对于每个节点n∈dom（ld），arity（ld（n））=length（sd（n））;• d没有圈（以期望的方式定义）。一个节点n∈N（d）称为空的，如果n ∈dom（ld）。我们让N（d）表示N（d）的空节点子集，并且N（d）= N（d）\N（d）。一个（DAG）态射f：d→dJ是一个保持标号和后继的函数f：N（d）→N（dJ）;它是一个同构，如果另外f是一个双射，并且它的反函数f−1：N（dJ）→N（d）是一个DAG态射。我们用DAG表示以dag's为对象、以dag态射为箭头的范畴。一个DAG态射f：d → DJ是n-内射的，如果它对N n（d）的限制是内射的;它是强非循环的，如果对所有a1∈Nn（d）和a2∈Nn（d）都没有从f（a1）到f（a2）;如果它是强非循环的，则它是简单的. 证明强内射态射和强非循环态射的合成是很容易的.重写形式主义，我们将使用的是标准的代数双推出方法[6]的范畴达格我们首先介绍重写的一般定义。接下来，在第5节中，我们将集中讨论规则的一种特殊形式，我们将考察它在不等式演绎表示方面的充分性。定义3.2（DPO在DAGL r重写）规则R =（dL<$dK→dR）是dag态射的一个跨距。DAG的d L、d K和d R分别称为R的左手边、界面和右手边。重写系统R是一组规则。给定DgG，则R=（dLlK→rdR），和dAM ATCH（即，的DAG←d态射）g：dL→dG，我们说dG重写为dH（使用R和g），如果图1中的图可以构造，其中两个正方形都是DAG范畴中的推出。在这种情况下，dD被称为上下文（DAG），我们写dGR，gdH，可能省略了下标。 我们写dGdH如果有可能空从G到H的重写步骤序列，使用R中的规则。和通常的DPO演示一样，也有重写机制的操作描述然而，它不同于标准建设控股，例如，在图的范畴中，更多的细节我们请读者参考[4]，以及引理5.4，稍后将介绍。定义3.3（rankedDAGA. Corradini等人/理论计算机科学电子笔记72（2007）313511H2122 1HG1 1 22F1K1是一个称为根映射的函数5，v：j→N（d）是一个称为变量映射的双射（在j和d的空节点之间）。 如果g= r，d，v和gJ=rJ，dJ，vJ是两个等秩的DAG，则秩DAG态射：G → G J是DAG态射：D → D J使得R = R J和V = V J。（j，i）-秩项图G是（j，i）-秩DAG的同构类.术语图上有两种自然操作，定义如下。定义3.4（项图的合成与并）设Gj，Hi为项王空军图表。它们的合成是秩为（k，i）的项图Gj; Hi，王空军取G和H下面的图的不相交并集，然后将G的根与H的相应变量。设Gi，Hk是项图. 它们的并集是术语图GiHk秩jl jl（j+l，i+k）通过首先取G和H，然后将G的根（变量）与H的根（变量）连接。6下图显示了四个术语图。空节点由与其在变量列表中的位置相对应的自然数表示，并在左侧被描绘为垂直序列;非空节点由其标签表示，指向后继节点的边从该标签离开;右侧的数字列表表示指向根的指针：从j到节点的虚线箭头表示它是第j个根。例如，第一项图G1具有例如rank（2，4），五个节点（两个空的，1和2，三个非空的，f，g和k），g的后继是变量2和1（按此顺序），f的后继是g和2，k的后继是2，四个根是g，f，k和f。12G11 12F11 1 3k324小时4分3 5254 6G1G2G3=G1;G2G4=G1<$G2这些约定有助于理解术语图上的两个基本操作。两个项图的合成是通过首先将第一项图的根与第二项图的变量匹配，然后消除这些变量来获得的。项图G3例如是G1和G2的合成。联合本质上是它们的不相交联合，其中变量和根的列表是连接的。项图G4是G1和G2的并集.5对于自然数k，我们假设k={1，. ......、 k}，因此0= k。6设G j= H [r，d，vj]，H i= H [rJ，dJ，vJ]. 然后，G;H=[rJJ，dJJ，vJJ] n，对于dJJ，d和王空军DJ，模等价于由r（x）=VJ（x）诱导的结点，且RJJ：dr→DJJ，VJJ：DVDJJ独特的诱导箭头。设Gi=<$[r，d，v]<$，Hk=<$[RJ，DJ，VJ]<$.则GH=[rJJ，dJJ，vJJ]，J LDJJ是d和DJ的不交并，RJJ：i + k→ DJJ，VJJ：j + l → DJJ是唯一诱导的箭头。1221 1 G12F1K2342236A. Corradini等人/理论计算机科学电子笔记72（2007）31v（k）r（ h）h33JJ⎪4项图不等式推导由于标准的一阶项表示全代数中的导出运算，因此项图特别适合表示多代数中的导出关系（参见[2]对此进行详细讨论。定义4.1（由项图表示的关系）给定一个环上的多重代数A和一个秩为（j，i）的项图G，我们用GA表示关系GA：|一|j参与者|一|我定义如下。 设r，d，v是G中的任意秩DAG，使得N（d）={n1，.，np};则1、... bi <$∈ GA（<$a1，. aj）优惠⎧ ⎫n ∈ N（d）. xn∈|一|∧⎪⎪⎪⎨∀k∈j. x=akN1 ... xnp.An ∈ N（d）. xm∈ ld（m）⎪⎩∀h∈i. X=b（m= 1，. ，xs d（m）↑arity（l d（m）⎪⎭其中sd（m）↑i表示序列sd（m）的第i个元素，对于每个节点m∈N∈ N（d）且i = 1，.，arity（ld（m））.换句话说，我们为项图的每个节点取多代数A的载体的一个元素。对应于G的根和变量的元素的元组是关系GA，如果对应于节点m的每个元素都属于fA（m1，.，mk），其中m1，.，m，k是的后继者M.很容易证明这个定义是很好的，因为它不依赖于为G选择的具体代表。作为一个例子，考虑上面的术语图G3。 它有秩（2，1），因此GA是一个函数，|一|2016年02月01日02：02：02（|一|），定义如下：b∈GA（a1，a2）惠.一x1，x2，xg，xf，xh，xk∈|一|.x1= a1<$x2= a2<$xg∈g（x2，x1）<$X∈fA（x，x）<$x∈hA（x，x）<$x∈kA（x）<$b=x<$fg2h gfk2h其中fA，gA，hA和kA是对应于多重代数A中签名算子的解释的基本关系.作为进一步的示例，现在让我们考虑两个（相当退化的）项图，它们将在一个实例中出现一些不确定性。 嘿！j（adischarger）是秩为（j，0）的唯一离散项图，因此具有j个变量节点并且没有根。通过<$j（一个复制器）我们将表示秩为（j，2j）的离散项图，使得变量k既是k次根又是（k+j）次根，其中k∈j。通过应用上面的通式，可以很容易地得到（表示|一|0）对于所有的a1，.，aj∈|一|、！A（a1，.，aj）={k}，并且A（a1，.，a，j）={a，1，..、aj、a1、.，aj}A. Corradini等人/理论计算机科学电子笔记72（2007）3137特别要注意的是，这两个关系都是完全的和单叶的，也就是说，它们只是函数。非常重要的是，从项图到A上的导出关系的映射（）A可以很容易地证明是关于定义2.2和定义3.4中介绍的运算的同态。引理4.2设A是一个多重代数，F，G是两项图。 则（F <$G）A=FA<$GA且（F; G）A= FA; GA.Q在选择了项图来表示多重代数中的导出关系之后，我们可以探索它们在具体化中的用途按照多重代数理论中的一个良好传统，我们将考虑不等式，它们自然地被解释为对应关系之间的包含。定义4.3（项图规范）环上的一个（项图）不等式是一对等秩项图<$F，G <$，通常写为F ± G。给定一个环上的多重代数A，我们说不等式F±G在A中成立（我们写A| =F±G），如果FA<$GA。给定一个多重代数类A，同样的不等式在A中成 立（记为A |= F ± G），如果它对所有A∈ A成立。一个（项图不等式）规范是一对项图不等式，其中Φ是一组项图不等式。给定一个规格参数φ ∈φ，其模型类为MAlgφ，Φ ={A∈MAlgφ|一|=对于所有<$∈ Φ}换句话说，如果关系FA包含在关系GA中，则不等式F±G在A中成立。下一步是尝试在语法上包含满足给定不等式集的多重代数中的导出关系定义4.4（项图不等式推导）设φ，Φ是项图不等式的具体化。然后，从该规范导出一个不等式F±G，记为Φ F ± G，如果该不等式可由下列公理和推理规则得到[公理]ϕ∈ΦΦ ►ϕ[结构公理]对于所有秩为（j，i）的项图G，你好！i±！jΦ G; i± j;（G G）[自反性与传递性]对所有秩为（j，i）的G，H，K，公司简介Φ1000±1000，Φ1000±1000公司简介[置换性]对于秩为（j，i）的所有G1，H1和秩为（i，k）的所有G2，H2，Φ1000±1000，Φ1000±1000Φ1;G2±H1;H238A. Corradini等人/理论计算机科学电子笔记72（2007）31J我J[同余]对所有秩为（j，i）的G1，H1和秩为（k，l）的G2，H2，Φ1000±1000，Φ1000±1000Φ1000mm±1000mm±1000mm让我们评论一下结构公理。如上所述，对于每个多重代数A，A是固定的，它是从|一|关于Singleton Set|一|0的情况。因此，无论关系G A是什么：|一|j参与者|一|i，组成GA;！A可能是单例集的部分函数，因此（G;！（一）A类！A是必然的。关于第二个结构公理，它形式化了这样一个事实，即如果我们两次（使用复制器）评估由G表示的非确定性表达式的结果，通常我们得到的结果比评估两次要少，因为两次评估可能会产生不同的结果（关于这一点的更多细节，请参见[3]还要注意的是，关于操作的闭包明确地确保了可替换性。给出了对结构公理和引理4.2的这种解释，上面的演算是合理的就不足为奇了。定理4.5（项图不等式推导的可靠性）设其中，Φ是一个不等式的具体化，F±G是一个关于 Φ的不等式：ΦF ± G=MAlg，Φ| = F± GQ我们无法证明微积分的完备性。我们猜想，只要对这些具体化施加适当的限制，情况确实如此（也见定义5.1）。我们通过展示一些不等式的例子来结束这一节，并描述相应的导出关系的诱导性质命题4.6（用项图不等式表示）设A是一个n-多重代数，G是秩为（j，i）的项图.然后• 一|- - j± G;！我i ∈ GA是一个全关系。• 一|=j;（G G）±G;ii-β GA是单价的。此外，让我们考虑秩为（j，k）的项图H。然后，导出的算子F = H_j;（G_j（H;！k））表示G wrt的域限制。H的定义域，也就是说，对于所有的多重代数A，FA<$GA和dom（FA）= dom（HA）<$dom（GA）都成立。然后，我们有• 一|=j;（G（H;！k））± G.• 一|= G ± j;（G（H;！k））i-dom（GA）-dom（HA）. Q5不等式推导在本节中，我们将展示如何将项图指定转换为项图重写系统，从而可以推导出不等式F±GA. Corradini等人/理论计算机科学电子笔记72（2007）3139FFFF使用定义4.4的系统，当且仅当F根据相关的重写系统重写为G我们将要描述的重写和逻辑演绎之间的关系遵循术语重写和重写逻辑之间的关系的相同模式，即我们将考虑具有限制格式的项图不等式.首先，根据定义4.3，不等式的两边必须具有相同的秩。其次，规则必须是适当的，这是一个条件，概括了一个规则不能有一个变量作为左手边的要求，通常在术语重写中。定义5.1（真不等式）项图F是真的，如果F中没有变量节点也 是根;不等式F± G是真的，如果F是。现在，我们可以描述我们的编码。定义5.2（从不等式到规则）给定一个项图F，我们将定义为：|F|一个任意选择的，未排名的DAG属于F。设F±G是一个proper。在等式1中，对于所述主机，具有k（j，i）的hot_hot_of_h。你的屁股像是被踢了Fl rRG=dL←dK→dR定义如下：• dL和dR是没有排名的达格|F|和|G|，分别;• 接口dK是包含i+j个节点的离散图;• 态射l和r将d K的i + j个节点一致地映射到d L =的i个根和j个变量。|F|DR= |G|，分别。7例5.3前一节的推导系统包括（结构）不等式F;！±！和F;±;（FF）。设F是一个项图，F的根由一个k元算子f∈N，且k是不同的变量，两个相应的规则，我们表示R！和R，分别，具有图2和图3所示的形状。左手边（中间，右手边）的DAG是dL（dK和dR，re-k）。 xi，yj表示空节点，并用于直观地描述dag态射的跨度：例如，在规则R中，由y f 1标识的节点和yf2，在dK中不同，合并成在dL中的f。注意左射l可能不是单射的：这发生在一个真不等式F ± G的编码中，当F中的两个根重合时（就像规则R）。7 非正式地，我们假设我们跟踪了 哪些节点，|F|（ 一）|G|）是F中的根或变量（G，分别）。40A. Corradini等人/理论计算机科学电子笔记72（2007）31，tcx2KFC，c，，Kc和kF→d→dx1，，1，fx1x1，2，cccKC... Ccc......xcJcxkxk图2.重写规则R！编码不等式Gf;！±！x1，，1，，fx1yf1x1，1，f，，2，cc，2，ccx2，t，ccx2KCx2，t1，kc2，c，... Cc...yf2...Ccc，fxcJcXKc，xk，tc图3. 重写规则R编码不等式Gf;<$± <$;（Gf <$Gf）.下一个引理总结了一些关于相关推出和推出补的存在性的结果，这些结果是使用上述格式的规则在DAG中执行DPO根据引理7.3，我们将只考虑普通态射作为匹配（见定义3.1）。引理5.4（DAG中的推出补）设l：dK→dL和r：dK→dR与定义5.2相同，设m：dL→dG是满足悬挂条件的普通匹配。8然后：(i) 如果l是单射的，则存在l的推出补格，m，由交换态射的存在性排序。如果dKkDDG是最小推出补数，9则推出k：dK→dD，r：dK→dR存在。(ii) 如果l不是内射的，则存在推出补格的非空族，并且这些格中的每一个都享有与前一点相同的性质。Q由于项图重写是在未排序的DAG第五章. 5（秩图的重写）对于k∈N，不可避免地，对于具有非可变节点的k（k，1），Gk是一种基于k（k，1）和k个可变节点的非可变节点映射。设F，H是秩为（j，k）的项图（环n）. 我们说F重写为Hˆ∗ˆEscherdef如果|F|EURR|H|，其中F=F;Gk= 0.8这是DPO方法的标准应用条件：形式上，对于每个节点n∈N（dL）\l（N（dK）），J J若m（n）∈sdG（n）则n ∈m（N（dL））. 熟悉DPO方法的读者可能会注意到识别条件由m的单内射性保证。[9]如果这个推出补数可以被表征为“自然”补数，即，如[5]中所示，是一个回调。X2X2A. Corradini等人/理论计算机科学电子笔记72（2007）3141RRFFR（Φ）不是这样的|F|⇒∗|国际和平协会|F|⇒∗ |⇒∗|，但反之则不成立，|, but theconverse does not hold,因为悬挂条件。 我们现在准备陈述主要结果。定理5.6（重写的不等式演绎）设R（Φ），Φ是一个不等式规范，R（Φ）是包含结构规则！对于所有的f∈φ，R∈ φ定义5.2。然后ΦF±Gi|F|⇒∗|Gˆ|Q证明的草图可以在附录中找到6结论和进一步工作我们的论文的主要目的是寻找证据来支持这样一个主张，即对于全代数，标准项起作用是一种类似的作用，因此，对于多个代数的特殊性来说，标准项是必不可少这一技术上的合理性来自于多重代数的函子表示，最初在[2]中提出，其中项图被证明是表示多重代数中导出算子的合适语法工具。我们的主张得到了证实，提出了一个演算的项图不等式推导，并证明其可靠性。特别是，演算充分利用了项图的使用，因为一个不受限制的替代性规则成立（这不适用于多重代数的其他演算）。更重要的是，我们证明了演算可以通过项图重写来实现，重写步骤模仿不等式演绎。作为未来的工作，我们要解决的第一个问题是微积分的完备性。与此同时，我们也想比较我们的演算与其他建议，从文学方面的复杂性的规则，和表达能力。我们预见的进一步扩展包括Horn子句逻辑，以及为了具有令人满意地指定的表达能力而需要的某种有限[11]）。引用[1] A. Corradini和F.嘎杜奇项图的代数表示，通过gs-monoidal范畴。应用范畴结构，7：299 -331，1999。[2] A. Corradini和F.嘎杜奇多重代数和部分代数的函子语义及其在句法上的应用。理论计算。Sci. ，2002年。地出现。可查阅http://www.di.unipi.it/ ~ gadducci/papers。[3] A. Corradini，F. Gadducci和W.卡尔多重代数的项图语法。技术报告TR-00-04，比萨大学信息学系，2000年。[4] A. Corradini和F.罗西用于术语重写系统和逻辑编程的超边缘替换丛林重写。理论计算。Sci. ，109：7R42A. Corradini等人/理论计算机科学电子笔记72（2007）31[5] H. 埃里希和H.- J. Kreowski.图形系统与图形文法的范畴方法。 在G. Marchesini和S.K. Mitter，editors，Mathematical Systems Theory，Volume 131 ofLecture Notes inEconomics and Mathematical Systems，pages 323-351.斯普林格，1976年。[6] H. Ehrig ， M. Pfender 和 H.J. Schneider 。 图 文 法 ： 代 数 方 法 。 在 R. V. Book ， 编 辑 ， Switching andAutomata Theory，第167-180页。IEEE Computer Society Press，1973.[7] F.嘎杜奇关于并发项重写的代数方法。比萨大学信息学系博士论文，1996年。[8] D.丰满。项图重写。In H. Ehrig，G.恩格斯，H. J. Kreowski和G. Rozenberg，编辑，Handbook ofGraph Grammars and Computing by Graph Transformation，第2卷，第3世界科学，1999年。[9] M.R.睡眠，M.J. Plasmeijer和M.C.J.D. van Eekelen，编辑。术语图重写：理论与实践。Wiley，1993年。[10] M. Walicki和S.梅铎非决定论的代数学方法：概述。ACM计算调查，29：30[11] M. Walicki和S.梅铎非决定论的多代数和函数语义学的完全演算。ACM翻译计划。Lang.系统，17：3667附录我们在这里提出一些证明草图的主要结果的文件。我们从一个技术引理开始。引理7.1（DAG中的推出）设f：d→dJ是一个DAG态射，并让它的相关替换为函数f：N（d）→T（N（dJ）），将每个变量节点n映射到通过“解开”f（n）获得的（N，N（dJ））上的项。jfgJJ给定跨度d←d →d在DAG中，当且仅当替换Beself和Beselg统一。Q关于证明，参见[4]的命题1.18，其中该陈述是针对范畴丛林图证明的，它等价于范畴DAG。我们现在可以提供引理5.4的一个证明。引理5.4的证明草图。对于点（i），非正式地，通过删除m（N（dL）\l（N（dK））中的所有节点，并通过使标记和后继函数未定义，从dG获得最小推出补对象dDkJJ在m（l（N（dK））\N（dL））中的节点上。 给定两个推出补数dK→dDKJJJJDKD，他们的加入是他们的推出，他们的相遇是由在推出过程中回撤注射。图1的最小推出补的右推出的存在性从前面的引理得出，通过观察dK的j+i个节点中，j被r映射到dR的不同变量（通过构造），并且其他i被k映射到dD的不同变量，因此相应的替换统一。对于点（ii），直观地，如果l（n）=l（nJ），则在推出补对象中，对dG中的节点m（l（n））的引用可以以任意方式分裂为对k（n）或k（nJ）的引用，并且每个这样的选择确定推出补的格。QA. Corradini等人/理论计算机科学电子笔记72（2007）3143HGRR（Φ）R（Φ）R（Φ）R（Φ）R（Φ）这一节的其余部分将用来概述我们的主要结果Theo-rem5.6的证明. 我们首先从一个辅助定义开始定义7.2（术语图上下文）（术语图）上下文C [j，i]是一个格式良好的、排名的术语图表达式（使用术语图作为常数，运算符为“和”;）含有1（ranked）占位符[j，i] （对于某些i，j∈N）。如果C [j，i]是上下文，G是秩为（j，i）的项图，则C[G]表示用G替换[ i，j ]后对表达式C求值得到的项图。现在，我们有两个技术引理。第一个关系到满足悬挂条件的普通匹配和上下文之间的联系;在此基础上，第二个基本引理指出，通过应用规则R获得的任何重写步骤都等价于将R嵌入上下文。引理7.3（普通态射和上下文）设F是秩（j，i），letdK→ldL是规则RF的左分量（定义5.2）和令dG= |G|是项图G中的一个选定的dag。 则存在上下文C [j，i]使得G = C [F]当且仅当存在满足关于l的悬挂条件的纯态射m：dL→dG。Q引理7.4（重写为语境化）设RF成为相关规则用适当的不等式F± G，设S，T是两项图.然后|F|⇒FG |如果且唯一地，如果x是一个C=C[F]的常数，且|ifandonlyifthereexistsacontextCs uchthatS=C[F]andT= C [G]。Q最后给出了主要结果的证明大纲定理5.6的证明简图。[演绎意味着重写]如果Φ <$F ± G，我们的生活|F|⇒∗|G|通过引入用于执行以下操作的路径，是的。对于结构公理，它们在演绎中的效果可以通过重复应用例5.3的辅助规则来模拟。 响应性和传递性规则以显而易见的方式处理。对于替换性和同余，我们利用最后一个引理。 如果Φ<$G1±H1和Φ<$G2±H2，通过诱导hy-potthesiswehave|G-1|⇒∗|and|G-2|⇒∗ |⇒∗|.|. 从这个地方流下来|⇒∗ |⇒∗|.|. 现在考虑上下文C=G1; [j，i]，其中（j，i）是秩或G2。7.我的超能力4，并通过在其左侧引入|G-2|⇒∗|H-2|，we乌布登塔塔|C[C2]|φR（Φ）|C[CH2OH2]|，thus|G1级;G2级|φR（Φ）|G1;H2|. 与上下文[k，j];H2对称地，其中（k，j）是G1的秩，人们获得期望的重写序列。同样的，对于？[重写意味着演绎]第一个表明，一个单一的重写步骤对应于一个演绎。 这对于对应于R（Φ）规则的步骤来说是微不足道的。对于一般的重写，通过引理7.4，这等价于将规则放在项图上下文中。证明然后去归纳的句法结构的情况下，观察到，长期图作为常数对应于rexexivity规则，而操作的contradictions和;对应于应用的同余和替代性规则。接下来，重写由更多44A. Corradini等人/理论计算机科学电子笔记72（2007）31一个以上的步骤对应于传递性规则的应用Q