名义逻辑中A和AC函数的α-等价形式化及可靠性验证

可在www.sciencedirect.com在线获取理论计算机科学电子笔记332（2017）21-38www.elsevier.com/locate/entcsA和AC函数符号的名义α等价形式化1MauricioAyala-Rinc'on<$，Washington deCarvalho-Segundo<$，MaribelFernandez和Daniele Nantes-Sobrinho<$2Dep artamentosde<$Matem'aticaeCidadaComputacaoDepartmentofInformaticsUniversidadedeBras'ılia，Brazil King摘要名词抽象句法模结合中α-等价概念可靠性的形式化（A）和结合-交换（AC）方程理论。 最初，α等价的概念根据Urban在其名词发展中提出的所谓“弱”名词关系，在伊莎贝尔/霍尔。然后，在Coq中形式化了这个等式确实是一个等价关系。 后给出了与A和AC函数符号的广义α-等价关系，并形式证明了它是一个等价关系.作为推论，得到了模A和模AC的可靠性α-等价.最后，给出了模A和模AC的α等价性检验算法.一般的α-等价问题是对数线性求解的，而AC以及A和AC的组合α-等价问题是对数线性求解的。与标准一阶方法相同的复杂性。这一发展是朝着验证名义匹配，统一和缩小算法模一般方程理 论迈 出的 第一 步。关键词：名义逻辑;阿尔法等价;模A等价; AC。1介绍匹配、统一，以及更一般地说，检查涉及存在性和泛量化的等式问题的有效性，粗略地说，两个术语s和t在句法上是等价的（分别是）。如果s=t，则可匹配，可统一）。如果有一个置换σ使得sσ=t，或者同时代入s和t使它们相等：sσ=tσ）。这些概念可以扩展到等式理论，如α-等价性，交换性，结合性，恒等式等更一般地说，我们考虑等价，匹配和unification模E，其中E是一组等式公理。特别是，α-等价在λ-演算[ 5 ]中起着基础性的作用，它捕捉了用作绑定变量的名称的不相关性的概念。1由CNPq普遍赠款476952/2013-1部分支持2电子邮件：ayala@unb.br，wtonribeiro@gmail.com，maribel. kcl.ac.uk，dnantes@mat.unb.brhttp://dx.doi.org/10.1016/j.entcs.2017.04.0031571-0661/© 2017作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。22M. Ayala-Rincón等人/理论计算机科学电子笔记332（2017）21对约束变量的适当操作是名义逻辑[20]和其他形式发展的主要动机，包括名义统一[2，9，19，25，26]，即模α的统一，名义重写[16，17，18]，演绎系统[11]，编程语言[8，22，23]和推理框架[3，24]。在名义语法中，人们使用原子而不是变量，原子由它们的名称区分并用于构建抽象。此外，新鲜度的概念是通过推理规则来明确的，这些规则定义了原子在名义上是否是自由的。变量的重命名是通过原子的交换来定义的，原子是作用于项的排列的基本组成部分。最后，α-等价的概念通过推理规则具体化，这些规则指定在某些新鲜度约束下，项是否是α-等价的。这与λ演算等框架中的通常处理不同，其中α等价是通过Barendregt变量约定等假设隐式抽象的最著名和最完整的名词语法的形式发展是由Urban等人在Isabelle/HOL中具体化的（[25，26]）：首先，一个关系α被具体化并被证明是合理的，也就是说，被证明是一个等价关系;其次，一个名词统一算法被具体化，它使用α-等价，并被验证是正确和完整的。 在[25]中，Urban详细描述了 证明名义上的α关系实际上是一个等价关系，使用一个中间弱α关系表示为ωω。贡献 在Coq形式化的可靠性的α-等价的名义语法的描述。这一发展的显著特点是，据我们所知，我们第一次进一步推进，并且还检查了A和AC算子的名义α等价性。这一发展可以用其它方程理论加以推广。正式化的主要步骤如下所述。• 最初，α-等价性<$α和弱等价性<$ω的概念是按照Urban的证明风格来具体化的[25]。然后形式化地证明了<$ω是一个等价关系。然后，利用ω证明了α -等价的特定概念是合理的。虽然这个属性通常被认为是理所当然的，但它的形式化并不简单，因为它依赖于一个非平凡的归纳法对于不能直接建立归纳假设的项，为了方便（α）重新命名应用归纳的项的适当子项。其他重要的，非平凡的性质需要：保存新鲜度，equivariance的α，保存置换作用。• 本文给出了具有A和AC算子的项的α- 等价关系，记为<${A，AC}，并证明了它是合理的.由α { A，AC }的可靠性导出α-等价模A（αα，A）和模AC（αα，AC）的可靠性.这些关系是以参数化的方式指定的，这将简化α-等价与其他方程理论的处理和组合。功能符号被注释以指示它们是A还是AC。关系<${A，AC}使用α-等价规则，证明了将其限制为α-等价对应于<$α。因此，使用<$α的正确性，通过应用A和AC算子的代数性质来检查关系<$A{A，AC}，此外，M. Ayala-Rincón等人/理论计算机科学电子笔记332（2017）2123保鲜性和等方差性。• 本文给出了一种基于Coq规范的确定n{A，AC}的算法当检查等价性时，是否应用专门用于A或AC符号的标称推理规则的决定是使用功能符号注释以自然的方式完成的。假设预先计算以函数符号为首的项的近似形式，证明了仅确定模A的α-等价的代价与问题的大小是对数线性的，而模AC的α-等价的行为与Benanav，Kapur和Narendran[6]提出的纯AC-等价的算法相同相关工作。自从现代抽象代数的早期发展以来，方程问题已经被广泛地探索过（参见，例如，Baader等人的E-unification调查[4]）。具体而言，关于AC统一，根据Boudet，Contejan和Devie[7]在通常的一阶语法中，对决定AC相等问题的处理归结为在二分图中搜索完美匹配的问题，如[6]所示。除了Isabelle/HOL 形式化，C oq 和PVS 也有正式的名词性发展。Ayala-Rinc′on，Fern′andezandRocha-Oliveira[2]根据[16]中提出的证明草图，在不使用辅助关系<$ω的情况下，形式化了PVS中的<$α-等价，并提供了标称统一算法正确性的形式化。Aydemir，Bohannon和Weirich在Coq中开发了名义推理技术[3]。与目前的发展相反，这种方法没有考虑名义相等的正式验证，因为它通过根据约束变量在项中的位置将约束变量的出现确定为自然数来识别α最近，Copello等人[12]提出了一种名义方法，基本上基于名义交换和新鲜度，用于以具体的方式处理λ演算中的α这是用来形式化的阿格达原则的α-结构归纳和递归通过这个名义上的具体实施巴伦德雷特此外，Schmidt-Schauss et al.[21]介绍使用递归let指令的λ-表达式的标称统一和匹配算法。他们证明了这两个问题都是NP-完全的，并转移了方法，他们证明了名义交换统一也是NP-完全的。 纲要第二节介绍了名词性抽象语法的必要背景。第三节和第四节分别给出了α-等价及其A算子和AC算子形式的可靠性的形式化在结束之前，第5节讨论了从Coqs规范中提取的用于确定{A，AC}的算法，在https://github.com/wtonribeiro/nominal-ac。2标称值本节介绍了名词语法[25，16]。给定一个函数符号的签名，并且在有限集合V和A中可数，变量和原子，则生成名义项的集合T（A，A，V24M. Ayala-Rincón等人/理论计算机科学电子笔记332（2017）21KKKK通过以下语法：s，t：：=0 | 一| [a] t| 阿斯特尔 | fEt| π.X原子只是名字不同，所以对于原子a和b，表达式a/=b是多余的。一个置换是A上具有有限域的双射。交换被定义为一对原子（a b），置换π由形式为（a1b1）：：.. 的交 换 的 有 限 列 表 表 示 。 . ：：（anbn）：：nil，其中nil表示相同的置换。表示π的交换的逆列表对应于π−1，π的逆。排列π和πJ的合成记作πJ<$π。一元排列（ab）：：nil将缩写为（a b）。一个变量X∈ V作为一个项对象应该总是被挂在X上的某个置换π修饰，π.X。 为了简洁起见，形式为nil.X的项将被写为X。置换作用于名义项，但挂起于变量。空元组或单元表示为空元组，非空元组使用形式为s，t的项对来构建，其中s和t也可以是对。请注意，此语法不允许构造一元元组。符号a表示原子a作为术语对象。[a]t是项t中原子a的抽象。记法fEt表示fE∈F对t的应用。函数符号fE中的脚本E和k是分别用于区分函数符号的等式性质和具有相同等式性质的算子类之间函数符号的不可分性。如果没有混淆，这些脚本将被省略。感应原子：设置：=感应无功：设置：=atom：nat→Atom。var：nat→ Var.定义Perm：=list（Atom×Atom）.归纳项：设置：=| At : Atom → term| Ut : term| Fc : nat → nat → term →term| Pr : term → term → term| Ab : Atom → term → term| Su : Perm → Var → term在规范中，语法如上所述运算符Ut、At、Ab、Pr、Fc和Su分别指定单元、原子作为术语对象、抽象、对、函数应用和挂起变量。对于Fc构造函数，第一个和第二个nat参数表示所应用的函数符号在规范中，函数符号fA和fAC表示为：JK分别由Fc 0j和Fc 1 k表示，都具有类型term→term。所有其他上标表示空的等式理论。一个原子作为一个对象项a，在Coq中写为（Ata）。必要时，此语法用于描述规范的伪代码中，否则将采用标准标称语法。请注意，虽然在名义语法中，两个原子a和d是由定义区分的，但（Ata）和（Atd）可以是同一个原子，因为在Coq规范中，a和d被用作原子范围内的元变量定义2.1置换对项的作用被指定为交换列表对单个原子的作用的同胚扩张M. Ayala-Rincón等人/理论计算机科学电子笔记332（2017）2125π·a→（Atπ·a）⎪阿罗拉#[#-ut]埃塞俄比亚a#b[#-at]数据库#t[#-fc]∇ ► a#ftEK∇ ►a#t1∇ ►a#t2[#-pr]∇ ►a#⟨t1,t2⟩中国a#t∇ ►a#[b]t[#-ab2][#-ab1]图中所示为图#[a]tπ−1·a#X∈ ππ.X[#-su]nil·a：=a如果c=a，则πJ·d⎧⎪π·⟨⟩→⟨⟩π·fEt→fE（π·t）π·t：=（（c d）：：πJ）·a：=如果d=a，则πJ·cπ·u，v→ ππ·u，π·v⎪其他⎩⎩否则πJ·aπ·（[a]t）→[π·a]（π·t）⎪⎩π·(πJ. X）→（πJ <$π）。X对原子术语对象a的置换的动作，例如，nil·a，作为结果给出一个项。这被指定为nil·（Ata），它给出结果a，即（Ata），而不是原子a。置换π在悬置变量πJ.X上的作用作为结果给出项π·（πJ.X）=（πJ<$π）.X。请注意，排列组合的工作方向相反置换（a b）：：π作用于项[a]<$b，πJ.X<$将具有结果[π·b]<$At（π·a），（πJ<$（（a b）：：π））.X<$。名义上的相等的原生概念是α等价，它是使用交换和新鲜度的概念来定义的新鲜度约束是原子和名义项t的对a#t。直觉上，a#t意味着a在t中是新鲜的，也就是说，如果a出现在t中，那么它必须在抽象器[a]下这样做。α-等式约束是由两个项s和t组成的一对s<$αt。新鲜度上下文是新鲜度约束的集合。将在新鲜度上下文中进行排序。新鲜度判断是以下形式的元组：而一个α-等价判断是一个形式为sαt的元组。表1新鲜度关系可推导的新鲜度和α等价性判断由表1和表2中的规则定义。我们将ds（π，πJ）#X写为{a #X}的缩写|a ∈ds（π，πJ）}，其中ds（π，πJ）={a |π·a = πJ·a}是其中π和πJ不同的原子的集合（差异集）。一个约束集合P称为一个问题。当对每个P ∈ P都存在判断的证明时，我们用表1和表2的规则写为判断的证明。抽象和暂停的规则是有趣的。比如说，<$<$a #<$[a]（<$a，b<$），π.X<$<$只能在π−1·a#X在<$中时导出。表2中⎪KK26M. Ayala-Rincón等人/理论计算机科学电子笔记332（2017）21有两个抽象规则：[α-ab1]和[α-ab2]。后者，对于用不同原子构建的抽象，交换其中一个抽象中的原子，只要原子是新鲜的。M. Ayala-Rincón等人/理论计算机科学电子笔记332（2017）2127∇ ► ⟨⟩ ≈ ⟨⟩α[α-ut]黑腹[α-at]∇ ►你好，α TJαFt ftEE[α-fc]KαKJ∇ ►t1≈αtJ1∇ ► ⟨t1,t2 ⟩≈α ⟨tJ1,tJ2⟩∇ ►t2≈αtJ2[-pr]α∇ ►[a]t≈α[a]tJ∇ ►t≈αtJ[-ab]α1∇ ►t≈α(a b)·tJ∇ ►a#t J∇ ►[a]t≈α[b]tJ[-ab]α2ds（π，π）#Xπ∇ ►π.X≈απJ.XJ[-su]α⟨⟩ ∼ ⟨⟩ω[-ut]ω一个ω a[ω-at]ft ftEtωtJKωEKJ [ω-fc]t1<$ωtJ1T1，T2t2<$ωtJ2[-pr]ω[a]tω[a]tJtωtJ[-ab]ωds（π，πJ）=ππ·X<$ωπJ·XJ[-su]ω表2α等价规则3α关系可靠性的形式化使用Coq规范，alpha equiv（即表2中的α）被正式证明是一个等价关系。本节描述了形式化。标准证明使用项上的测度来证明α是对称的，然后证明α是传递的[2，16，19，26]。 我们使用Urban在[25]中提出的另一种证明：首先定义一个所谓的“弱”等价关系<$ω，如表3所示。然后，证明了<$ω是一个等价关系，它是直接的，并给出了<$α的一个中间传递性结果：<$<$t1<$αt2和t2<$ωt3蕴涵<$<$t1<$αt3.最后，结合一些辅助引理证明了该结果的传递性和对称性，是的。形 式 化 的最后部分依赖于三个主要的辅助引理：•α的保鲜性：α=α#t，α=α t，α= αt， α=αT;• <$α的等方差：<$$>t<$αtJ蕴涵<$$>π·t<$απ·tJ;• 在置换作用下的不变性：（∇ ►π·t≈απJ·t.表3弱α等价为了检验模A和AC的α -等价性，可以使用<$α的可靠性。因此，可以采用任何方法来检查α，保持用于检查α{A，AC}的方法。 更具体地说，我们指定一个归纳关系equiv（S），其中S是一组指数，每个指数与一个不同的方程理论y相关联。特别地，关系equiv（equiv）从equiv的具体化中排除了任何方程理论的所有特殊推理规则。形式上证明了关系equiv（）与关系<$α：<$t <$αtJ惠equiv（）（，t，tJ）是等价的.28M. Ayala-Rincón等人/理论计算机科学电子笔记332（2017）21引理3.1（带<$ω的<$α的中间传递性）如果<$αt1<$αt2，t2 <$ωt3那么<$1 <$αt3。这个证明是通过对α的归纳法得到的。 它使用了名义项的基本性质和在定义α时推理规则的扩展，除了规则[α-ab2]，其分析需要应用α ω的等方差性质和αω下的新鲜度保持。也就是说，在这种情况下的归纳步骤中，我们有作为前提的t1<$α（a b）t2，[a]t1<$α[b]t2，[b]t2<$ωt3，a#t2，并且作为IH：对于所有的t0，（a b）t2<$ωt0意味着<$t1<$αt0;我们需要得出结论，<$[a]t1<$αt3（省略了一些不相关的前提）。 按性质<$ω，[b]t2<$ωt3，t3应该是[b]TJ3的形式。 因此，人们需要得出结论，∇ ►[a]t1≈α[b]tJ3.此外，有t2<$ωtJ3，通过<$ω的等方差，可以得出（a b）t2 <$ω（ab）tJ3。此外，通过在低温下保鲜，3.第三次约会用（a b）tJ3来例示IH，则有该IH1<$α（a b）tJ3。由此，应用规则[α-ab2]，最终得出结论：α[a]t1α[b]tJ3。引理3.2（α的保鲜）如果α#t和αt≥αtJ，则∇ ►a #tJ.这个证明是通过对α的归纳法得到的。有趣的情况是对[α-ab2 ]规则的分析，其假设是a0/=b0，tα（a0b0）tJ，ta0#tJ，[a0]t. 由IHa#ta#（a0b0）tJ。 我们应该证明[b0]tJ. 为此，应分析三种情况：a=a0、b0=a/=a0和b0/=a/=a0。困难的情况是最后一个，这是通过应用[#ab2]规则并使用关于 新鲜度关系引理3.3（<$α的等方差）如果<$$> t<$αtJ，则<$$>π·t <$απ·tJ。形式化是通过对α的归纳。棘手的情况是当假设a/=b，tα（a b）tJ和a#tJ时。IH为<$$> π·t<$απ·（（a b）tJ）。应证明<$$>π·（[a] t）<$απ·（[b] tJ）。应用的定义置换作用和[α-ab2]规则，必须证明三个子目标：π·a/=π·b，πα（（π·a）（π·b））（π·tJ）和π α（π·a）#（π·tJ）。第一个和最后一个问题可以通过技术引理简单地解决。对于第二个子目标，Lem。3.1用π·（（a b）tJ）实例化t2那么新的子目标之一是IH，另一个是（π·（（a b）t））<$ω（（π·a）（π·b））（π·tJ）。后者是关于置换在交换中的分布的技术引理的一个下一个结果将应用于Lem的证明3.5以及在与对称性有关的证明中，如交换下的α∇ ►(a b)·t≈α(c d)·t with∇ ►a, b, c, d#t.引理3.4（项在α下的不变性和置换的作用）（na ∈ ds（π，πJ），n a #t）i n这个引理是通过在任意排列下对t的引理3.5（第二中间传递性引理）如果t1<$αt2且∇ ►t2≈απ·t2then∇ ►t1≈απ·t2.M. Ayala-Rincón等人/理论计算机科学电子笔记332（2017）2129这个证明是通过在假设t1αt2中对α的归纳而得到的。有趣的情况是对于抽象，即t1=[a]TJ1和t2= [b]TJ2。根据a和b、a和π·a、b和π·b以及a和π·b是否相等，可以考虑几种情况。引理3.6（α的回归性）这个引理是通过在t的结构上的常规归纳法证明的。引理3.7（α的传递性）如果αt1αt2且αt2αt3，则α tt 1 αt 3.形式化是由归纳法在t1αt2与推广的t3。的当t1= [a]TJ1，t2= [b]TJ2，t3= [c]TJ3时，a/=b=c/=a，出现了困难的情况。IH被给出为Δt0，ΔtJ2Δt0ΔtJ1Δt0，以及其他假设分别为：tJ1α（a b）tJ2，a#tJ2，tJ2α（b c）tJ3和b#tJ3。应该得出结论，即，[a]tJ1<$α[c]tJ3。将规则[α-ab2 ]应用于目标1，得到子目标αtJ3，∇ ►tJ1≈α(a c)tJ3.Lem证明了前者。3.2.将IH应用于后一个子目标，还需要证明<$$>（ a b ） tJ2<$α （ a c ） tJ3 。 因 此 ， 需 要 证 明 中 间 状 态 t∈[ （ bc ） ： ：（ab）]·TJ3<$α[（bc）：：（ab）：：（bc）]·t3J，这是应用Lem的可能性三点四 操纵交换和利用莱姆 3.5我们可以推 断出 <$$> （ab）tJ2<$α[（ bc）：：（ab）：：（bc）]·t3J。最后，一个应用程序。3.1其中t2：=[（b c）：：（a b）：：（bc）]·tJ3只剩下证明[（b c）：：（a b）：：（b c）]·tJ3<$ω（a c）tJ3，这可以使用<$ω的性质，例如它的等价性和等方差性来完成。引理3.8（α的对称性）如果αtαtJ，则αtjαt。证明是通过归纳法在上的<$α在上。非平凡的情况是，a b和假设是：t0<$α（a b）tJ0，a#tJ0和（a b）tJ0<$αt0，其中子目标为[b]tJ0<$α[a]t0。这是通过应用规则[α-ab2]和Lem的双重应用来提供的。3.7使用t2：=（a b）t0和t2：= [（a b）：：（a b）]·t0实例化。其余子目标使用Lem处理。三点三4 <${A，AC}，<$α，A和<$α，AC的正规可靠性类属关系equiv（S）在第二节末尾提到。3分别考虑了A和AC函数符号，如果0∈S和1∈Sequiv（{0}）、equiv（{1}）和equiv（{0，1}）是定义关系式αmodoA，AC和A分别与AC功能符号组合。这样就建立了关系式<$α，A，<$α，AC和<${A，AC}。只有当参数S包含0或/和1时，上标为0和1的函数符号才分别被解释为A和AC运算符。利用参数S={0}和带任意上标（包括0）的函数符号以及仅带上标0的函数符号，分别表示了一般的和初等的模A α -方程问题（[4]）. AC问题也是如此。这里给出的形式化是为了30M. Ayala-Rincón等人/理论计算机科学电子笔记332（2017）21ff⎪⎪⎪⎩⎩⎪⎪⎪⎪⎪⎨⎩⎪→⎨⎪⎨⎩一般α-等价问题为了简单起见，我们将在续集中使用A和AC来代替0和1。4.1元组上的运算在定义关系A{A，AC}时，A和AC算子的归纳规则使用了三个辅助算子来处理函数符号的参数。函数符号f的参数是使用pairs的构造函数构建的项或元组，以及以相同函数符号f开头的项的参数。这些运营商，如图所示 1，提取应用（n A或AC）符号f的参数的相关信息，并分别指定参数的长度或数量，t [i]f，以及第i个参数的选择和删除，t（i）和t[i]。⎧⎪⟨s,u⟩→ǁsǁf+ǁuǁf⎧⎪⟨s,u⟩→⎧ ⎨ifi≤ǁsǁ fthens(i)f如果g=felseu（i−sf）ft其他1⎩⎪→1t（i）f：=g sifg=fthens（i）f否则gs⎩⎪→t⎪⎧⎧⎪ 如果i≤s然后，如果f= 1，则u否则，，u[2001年]fs，ut[i]f：=其他⎧⎩⎩如果f= 1，则selses，u[（i−sf）]f⎪gs→⎩⎪→⟨⟩如果gsf= 1，则elseg（s[i]f）Fig. 1. 指定元组或参数的长度操作符，选择和删除第i关于函数符号f的为了简化符号，当从上下文中清楚时，f这些操作员的行为如下所示例 4.1 对 于 参 数 的 数 量 ·ff=f= 1 。 ·fa ， bf=a ， bf= 2 ， 但 ga ， bf= 1;·f[a]（π·X），fb，ga，fa，bf=[a]（π·X）f+ bf+ga，fa，bf= 3。例4.2对于第i个参数的选择. ·t（0）=t（1）f并且，如果i>t=f，则t（i）f=t（i）f。 ·如果f= 1，且t不是以f为头，则t（1）f = t，但（fft）（1）f= t; ·（f）（3）f =（f）（2）f =（g）（1）f = g。FFM. Ayala-Rincón等人/理论计算机科学电子笔记332（2017）2131K例4.3删除第i个 参数.·t[0]=t[1]f如果i>tf则t[i]f =t[tf]f.·如果tf=1thent[1]f =;·（f[a]（π·X）， f<$b， g<$a， f<$a，b<$<$）[<$2]f=f<$[a]（π·X），（f<$b， g<$a， f<$a，b<$$>）[<$1]f<$= f<$[a]（π·X），f（g<$a，f<$a，b<$$>）<$.读者应该清楚的是，这种规范遵循了函数符号没有固定参数的名义语法。因此，对于任何A或AC符号，都应该将其应用于单位（单位）和单个参数的含义分开解释，例如，使用通常的算子符号解释，∧⟨⟩, ∨⟨⟩, +⟨⟩and×⟨⟩ might be specified as使用这些运算符有两个优点：第一，不需要额外的数据结构（例如列表，序列，数组）或非线性运算符来表达结合性;第二，这种方法是通用的：语法和给定的规则可以扩展到以自然的方式操作各种方程理论的运算符。如果在一个项中出现具有不同等式性质的函数符号，则使用处理其等式性质的专门推理规则。这简化了对模A和AC的α-等价以及其他方程理论的处理在表4中列出了一些形式化的结果，这些结果来自与这些算子相关的形式化引理的更长列表。这些结果将在与E-等价相关的引理的描述中引用，为了简洁起见，它们没有泛量化器。表4经营者的基本特征：（）f 和[s]fn tn ≥1，t（0）= t（1），t[s0]= t[s1]i≥t t（i）= t（t），t[si]= t[st]tt0i j或02：在应用辅助引理后，f t和ftJ有两种可能性，即对某个i 0，ftt（1）f<${A，AC}tJ（i0）f和ftt[1]f<${A，AC}tJ[i0]f.如果i= 1，则结果是平凡的。 对于i> 1，归纳法适用于项t0=ft[t1]f 和tJ0=ftJ[i0]f其中nti1=i−1。注意t帽IH为Given，G i v en为（t0ftf，t′0，0j1. 分别将j实例化为j1+ 1或j1，并使用运算符t [i]f、t（i）f和t[i]f的性质得出结论。引理4.10（T{A，AC}的传递性）如果T{A，AC} t1 T{A，A C}t2且T{A，AC}t3，则{ A，AC}t1<${A，AC}t3。形式化是通过对t1的大小的归纳，其中指定的名义项的大小由其组件根据所构建的数据结构给出34M. Ayala-Rincón等人/理论计算机科学电子笔记332（2017）21KKKKKJK−1KfE[2016-01 - 22]{A，AC}J0从他们的语法归纳。对t2和t3项进行了推广，并将等式推理规则的反演应用于两个等式t1{A，AC}t2和∇► t2≈{A,AC} t3. 困难的情况是规则[α-ab 2]和[等价物A]或[等效AC]。 对于[α-ab 2]，一个有趣的子情形是当a = aJ/= aJ0/= a时：两个符号是t {A，AC}（a aJ）tJa #tJ和tJ{A，AC}（aJaJ0）tJ0 a J0#tJ0，IH被给出为（s1，s2，s3），|S1|<|不|（应用[α-ab 2]，我们还需要证明：α t ∈ { A，AC }（aaj0）TJ0，αt∈{A，AC}. 前者通过保鲜获得，后者通过IH与应用获得关于Lem4.5、等方差和保鲜。对于规则[equiv A]或[equiv AC]，在形式化的某个点达到以下上下文，其中对于[equiv A]的情况，i=i0= 1：宾馆（1）{A，AC}tJ[1]第一次世界大战F{A，AC}fEtJ，andn=J（1）F{A，AC}fE㈠EKKkfEKK[2001年] Ef EKKtJ0（i0）fEKEkfEKfEtk[i0]fEK，IH由（s1，s2，s3）给出，|S1|<|（| ∧ (∇ ► s1≈{A,AC} s2∧ ∇ ► s2≈{A,AC} s3) ⇒ ∇ ► s1≈{A,AC} s3, and one shouldconclude that ∇ ► f Et ≈{A,AC} f EtJ0. 应用[equiv A]和IH在这种情况下，E=A是很容易证明的。当E=AC时，使用Lem。4.9以及上述第二个前提，得到第三个前提：{A，AC}tJ0（i1）fEtJ[i]fE{A，AC}t0J[i1]fE. 然后，应用[等同于AC]，kkki1，得到的子目标为：{A，AC}tJ0 （i1）fEK[1][2][3][4]K{A，AC}fEtj[2001年1月1日]fEK从第一个和第三个前提，两个子目标都得到了解决。引理4.11（A，A C}的对称性）如果A，A C}tJ，则A，A C}t。形式化是通过应用引理4.5，4.8和4.10，新鲜度保持和等方差对λ{A，AC}进行特别是使用LEM。4.10 是至关重要的： 在 [Aα-ab2] 的 情况下，一 个 人 应 该 po 的 ， 该po[b]tJ{A，AC}[a]t具有sypotheses其中，IH_（a b）tJ<${A，AC} t。那么莱姆4.10被应用两次，将t2实例化为（a，b）t和（a b）（a b）t，这允许使用引理4.5（具有α的性质）和等方差来得出结论。为了检验α，A和α，AC使用以下推论。记住，α，A，α，AC和推论4.12对于S<${0，1}，equiv（S）也是等价关系。形式化是通过操纵S−1={0，1} −S。对于一般等价问题equiv（S）（n，t1，t2），用既不属于{0，1}也不出现在t1和t2中的新算子替换集合S中t1和t2项中的所有上标算子，分别得到TJ1和TJ2.然后，通过对equiv的推理规则的归纳，容易地证明了equiv（S）（n，t1，t2）惠equiv（S）（n，TJ1，TJ2）惠equiv（{0，1}）（n，TJ1，TJ2）.因此，使用equiv（{0，1}）是一个等价关系的结论。M. Ayala-Rincón等人/理论计算机科学电子笔记332（2017）2135≈∇≈KK5一般<$α，A，<$α，AC，<${A，AC}问题的算法本节关注的是在A和AC符号存在的情况下，通过应用简化规则来检查α例如，使用[26]中给出的简化规则，形式为[a]X<$α[b]X的约束简化为约束集a#X，b#X;因此，a#X，b#X<$[a]X<$α[b]X。类似地，假设+是AC函数符号，等式当新鲜度约束满足时，a#X，b #X属于X。方程问题被写成对（pairs，P），其