基于高阶逻辑λ演算的假设交互式定理证明器的策略演算：类型化操作语义的战术演算

理论计算机科学电子笔记93（2004）118-137www.elsevier.com/locate/entcs一种策略演算及其操作语义G.I. Jojgov1荷兰埃因霍温理工大学H. Geuvers2荷兰奈梅亨大学摘要本文介绍了基于高阶逻辑λ演算（λHOL）的假设交互式定理证明器的策略演算的进展情况。战术演算是一种扩展 一个关于λHOL的开项演算。在其他系统中，策略的语义是由它们在通用编程语言（例如OCAML）中的实现的语义给出的，与此相反，我们能够根据定理证明器的状态来定义策略的作用，一个开放项，它对迄今为止在给定状态下创建的不完整证明进行编码。我们提出了类型化的操作语义的战术演算，并表明它是健全的和完整的演算的开放条款。可靠性定理进一步建立了策略执行前后证明者状态之间的关系保留字：交互式定理证明 类型理论，策略，操作语义学1介绍和动机证明助手是一种计算机程序，它可以促进复杂证明的形式化和发展，以及它们所需的理论。在证明开发中，就像在计算机编程中一样，我们可以区分声明式和过程式方法。在陈述式的证明1 电子邮件：G.I. tue.nl2电子邮件地址：herman@cs.kun.nl1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.12.031G.I. Jojgov，H. Geuvers / Electronic Notes in Theoretical Computer Science 93（2004）118-119构造一记录助理可以检查的从先前语句跟随的基于策略的证明助手采用过程方法，其中发出操纵证明的命令，直到构造出所需目标的证明这些命令，通常被称为战术，可以被看作是在证明器的当前状态下找到开放目标的实例的策略的复杂性可能会有所不同，从一个单一的推导规则的应用程序复杂的（半）决策程序（半）决策类的问题。通常，助手提供一种元语言，允许用户通过组合、迭代等方式从现有策略中定义更复杂的策略。这种语言的操作符被称为策略。这些战术和战术是在证明助手中微观层面上管理数学内容的构建块。其他的工具也可以用来处理文档和文件，但是要真正重要的是要获得一个更抽象的-数学，而不是证明-辅助导向-对战术的看法，并充分理解基本的微观步骤是什么，以及如何组成它们。在这方面，我们认为目前的工作正在为MKM社区做出贡献本文在高阶逻辑的开项λ-演算的基础上提出了一种演算，其开项被解释为策略。开放项演算和策略演算形成了高阶逻辑的基于假设策略的交互式定理证明模型的第三层-战术层-也是一个主题但它不属于本文的范围。在提出这个模型并描述了策略语言之后，我们为策略演算定义了一个类型化的操作语义，并证明了它相对于开放项演算为什么我们需要战术演算，为它定义语义学有什么好处？首先，它提供了一种独立于证明器实现语言的专用语言。这允许用户编写可移植的战术，而不需要在每个新版本中重新编译。从理论的角度来看，兴趣甚至更大，因为策略演算的语义在策略的定义和它所描述的证明器的证明状态的操作之间提供了直接的联系。这提供了增加的可靠性相比的情况下，当策略是书面的实现语言的证明。此外，战术语言的语义学将允许我们对战术进行推理。例如，在定义了一种策略之后，人们可以证明它总是终止的，或者它解决了某些类别的目标。120G.I. Jojgov，H. Geuvers / Electronic Notes in Theoretical Computer Science 93（2004）118-策略演算的引入及其语义的定义比开放术语的底层系统的句法包装更进一步，因为它们允许我们将证明搜索过程定义为策略演算中的术语在这些搜索过程中，我们可以使用基础演算中不可用的构造我们的想法是，这样的程序的结果应该与开放项的演算相关，以保证交互式证明构造的过程是合理的。除了说明成功的策略评估会产生一个良好的结果之外，可靠性定理还给出了策略执行前后证明者状态之间的关系。这意味着，例如，当我们执行一个旨在解决一个目标的策略时，这不仅仅是通过引入一个新的公理来实现的。关于策略语言的早期工作，如定理证明器Coq的策略语言LTac[2]，本文可以被视为补充。在LTAC的Coq提供的基本策略作为原语，可以建立新的策略，而我们的目的是解释这些原语通过编纂的证明状态的操作。当然，与Coq的关系只是概念上的，我们并不要求为Coq的原始策略提供语义，因为Coq是基于归纳构造演算（CIC）的，而我们使用λHOL，我们甚至不尝试处理归纳类型。本文的组织如下：第2节介绍了模型的定理证明，我们的工作，通过描述其三层。在2.3节讨论策略层时，我们介绍了策略演算的语法。然后在第3节中，我们将展示一些常见的策略是如何在其中定义的。第四节介绍了策略演算的语义，并展示了它的适足性 我们在第5节中对相关和未来的工作进行了总结。2交互式证明器建模看看交互式证明助手，它们采用程序化的方法来进行证明构造（例如Coq [10]和Lego [8]），我们可以清楚地识别出三个抽象层次-表示证明对象的下面，我们将简要地评论每一层，以便正式介绍它们并确定术语。G.I. Jojgov，H. Geuvers / Electronic Notes in Theoretical Computer Science 93（2004）118-121nt不state？？st a teta ctic alrtancstfi. Cs？什么？ ？Min staioabtjieocnterFig. 1.在对象层中表示的状态通过策略进行转换。 战术人员使用战术来找到目标在各州的实例。2.1对象层在我们的模型中的对象层是一个λ演算高阶逻辑（λHOL）扩展与开放条款。λHOL的选择并不重要，我们可以用另一个λ-演算来建立模型，它允许带有开放项的扩展开放术语是包含我们试图查找的未知术语的占位符的术语一个开放的术语通常代表一个不完整的证明，正在开发的证明。我们采用[3]的方法来处理开项，其中λHOL的开项扩展是通过添加特殊的参数化变量（元变量），输入它们的规则和允许我们填充未知值的实例化操作来完成的。关于开放项演算的细节，我们请读者参考[3]3。这里我们将只注意到一个元数据有一个描述？m[x1：A1. . . xn：An] ：A（典型的是，所有的人都可以在一个字符串中输入），并输入一个字符串[t1] 。 .我不知道该怎么办。读者可能会问为什么我们需要引入Meta变量而不仅仅是使用自由变量来表示未知数。如果一个逻辑公式所涉及的对象是对象级的，那么逻辑推理是在元级上完成的。当在开放项演算中进行交互式证明构造时，证明是我们的对象，我们实际上是在元-元级别上工作。区分源自对象级别的依赖性和来自元级别的依赖性是有充分理由的。例如，证明A→A的目标和在假设A下证明A的目标可能在逻辑上是等价的（如果我们想要证明构造的可靠性，它们应该是等价的），但是从元-元的观点来看，它们是不同的，因为证明A→A的一种方法可以通过→的引入规则得到它，并且通过执行这个证明构造步骤，我们达到了在假设A下证明A的目标。但我们本可以3 为方便参考，文中还包括了开放项演算的类型规则附录A中？M122G.I. Jojgov，H. Geuvers / Electronic Notes in Theoretical Computer Science 93（2004）118-我们也应用了另一个逻辑规则，构造了一个不同的证明，如果我们从第二个目标开始，就无法获得这个证明。通过引入Meta变量，我们可以区分对象级依赖（即函数变量f：σ→σ）和元级依赖（m[x：σ]：σ）。在我们的例子中，这种区分是必要的，因为战术术语定义了公开条件下的操纵，即。战术演算甚至更高一个元级别除了需要区分对象级依赖和元级依赖之外，使用元变量还有一些实际的优点。例如，在一阶设置中，高阶函数的引入可能是不可取的;某些类型系统的一致性对它们的函数空间的扩展很敏感，等等。2.2States.国与国之间的转变在给定时刻，证明器的状态可以由开放项演算中的类型判断来表示。一个判断Γ<$M：A断言不完全项M在上下文Γ中是A型的。术语M是我们正在开发的不完整证明，而Γ包含我们所使用的语言的所有声明，全局假设和表示证明未知部分的元变量。 事实上，判决 在开项演算中是可导出的，保证了状态的一般来说，验证施工过程将开始与判断的fr0，？m0[ ]：Am0[ ]：A，其中rr0是我们想要找到A型居民的坐标xt。通过对目标m 0应用一种策略，我们为它找到了一个实例化M0，它可能包含新的Meta变量m1：A1. mn [n]：An.在策略应用之后，代表证明者的这种状态的判断是你呢？m1 [1]：A1.. . ？mn[n]：AnM0：A该策略给出的状态转换可以用以下方式来理解：从初始判 决 开 始，？m0[ ] ：Am0[ ]：Aween i t w e k en t w e ni t w e n i t i t w e n itwenititwenititwenititwenititwen itite nititen itenititeniten ititenitit m1[m1] ：A1. . . ？mn[n] ：An，？m0[ ]：Am0[ ]：A. 然后我们检查由策略产生的初始项M0在新目标的背景下是正确的类型，即我们确保Γ0，？m1 [1]：A1.. . ？mn[n]：AnM0：A.如果是这种情况，我们可以使用开项演算的割引理4来实例化m0并获得4 见附录aG.I. Jojgov，H. Geuvers / Electronic Notes in Theoretical Computer Science 93（2004）118-123最后的审判。因此，我们可以把策略应用所引起的状态转换步骤看作是组合元变量弱化和切割所得到的判断之间的映射开项演算的基本性质保证了这种转换将可导出的判断映射为可导出的判断。 所以如果我们从对f的判断开始，？0：变量，那么我们已经在上下文Γ0中找到了类型A的居民。2.3战术层策略层是一个演算，允许我们定义合理的转换步骤。更准确地说，在我们的设置中，策略是一个术语，当在目标的上下文中进行评估时，它会为该目标生成一个实例，并可能在此实例中使用新的目标请注意，战术术语只计算实例化术语和新目标。它不会改变它想要解决的目标。将策略应用于目标是实际转换证明状态的操作。这个元操作是一个战术的例子（参见下面的战术层）。策略演算是对象层演算的扩展，并添加了以下证明搜索结构：• 引入新目标。这是通过？-粘合剂。术语？m：A.T直观上意味着 使用绑定器是在通常的绑定变量约定中引入新名称的一种干净方法。• 显式统一约束。统一化约束具有以下形状：[M<$N].T其中M和N是开放项，N是元变量列表，T是策略项。这个构造的想法是，我们试图统一M和N，如果这是成功的，我们继续与T。如果统一成功，将提供一些元变量的实例化。这个实例化在对T求值之前应用于T。它指定了需要在本地专门引入的元变量，用于统一约束。例如，如果我们想检查是否是一个蕴涵，我们需要引入新的元变量A和B，并为它们找到实例，使得A→B[提案A，B：提案A→B].T124G.I. Jojgov，H. Geuvers / Electronic Notes in Theoretical Computer Science 93（2004）118-排序S：：= Prop|类型|种对象项B：：= x|m [B.] B] |BB| λx：B. B|B. B|S参数列表：：= ε|x：B元变量列表：：= ε|什么？m[]：B策略项策略语境T：：= x|m [B.] B] |t [B]. B] |T T| λx：B. 不|B. 不|| ? m [m]：B. 不|[B B]. 不|（T，T）|失败t：：= t [x：B. x：B]：= TC：：= ε| C，x：B| C，？m []：B| C，！m[]：=B：B‘Matching variables’ like• 失败的策略。 特殊策略Fail代表总是失败的策略。• 案例区分。区分情况的操作符允许我们通过指定策略失败时的替代操作来处理失败的策略。为了计算（MelseN），我们首先计算M。如果成功，则其值变为（MelseN）的值。否则取N• 非终止递归。我们将允许通过递归来定义策略，而不施加保证终止的语法约束。允许非限制形式的递归有两个原因。第一个原因是，一个终止系统必然是不完整的;第二个原因是，在存在统一约束的情况下，保证终止的句法标准的制定似乎是一个困难的问题，我们还没有找到满意的解决方案（即，一个覆盖我们打算赋予语义的例子的可判定的句法标准）。图2总结了对象层和策略层演算的语法。由于技术原因，我们还允许引入全局定义，图二. 语法上下文中的选项（例如，m[j]：=N：A，rJ），因为它们提供了一种方便的实例化元变量的方法。当我们想用N来初始化m[m]时，我们只需更改声明即可？A：！m[m]：=N：A。这为我们节省了通过上下文的其余部分传播实例化的时间，并允许更清晰地表达语义的特性。G.I. Jojgov，H. Geuvers / Electronic Notes in Theoretical Computer Science 93（2004）118-1252.4示例：策略应用。策略Apply试图通过用证明M专门化一个定理来解决一个目标。例如，如果P（t）是P（t），而P（t）是P（x），则策略产生实例化（M t），它是P（t）的证明。在更复杂的情况下，它可能会引入新的元变量，用于实例化XML所需的未知项。 例如，设a、b和c为项 类型U和R是U上的二元关系。设M是R是传递的证明。然后，对目标R（a，c）应用具有参数M的应用将产生新的元变量y[]：U、p[]：R（a，y）和q[]：R（y，c）以及可以用于求解原始目标的实例化项（M a y[]cp[]q[]）为了进一步说明Apply所需的复杂行为，让我们假设也有一个项N表示证明R（x，b）。 如果 我们在目标p上使用ApplywithN，我们观察到两件事第二，在通过统一a找到的实例化之后，目标y被删除。因此根据一方选择一种战术可能会迫使其他目标被解决。使用上面介绍的策略演算，我们可以将Apply定义为：应用[：Prop，：Prop，M：]：=[].M其他[？A，？B：提案：A.B]。？m：A. 应用[μ，B，（μ m）]其他[？U：类型，？B[x：U]：Prop[x：U.B [x]]。？m：A. 应用[μ，B[m]，（Mm）]我们去掉了else周围的括号，将其定义为左结合的。在第二行中，我们检验目标和定理是否可以统一。如果是的话，我们可以从M得到一个证明，通过将由unification找到的unifier应用于它。如果统一失败，我们在第四行测试是否将蕴涵A→B。如果是这种情况，我们引入一个新的A类型的证明元变量m，并使用它来构造进行递归调用所需的B的证明（M m）。 在最后一种情况下，我们检查这是一个普遍量化的公式。如果是，我们再次引入一个新的Meta变量，用于消除递归调用中的通用量化器。请注意，在这种情况下，元变量可能出现在类型B[m]中。回到传递关系R，我们可以预期，当126G.I. Jojgov，H. Geuvers / Electronic Notes in Theoretical Computer Science 93（2004）118-评估术语应用[R（a，c），nx，y，z：U.R（x，y）→R（y，z）→R（x，z），M]我们必须大致执行以下步骤（参见第4节的精确表述）：？x：U应用[R（a，c），m，y，z：U.R（x，y）→R（y，z）→R（x，z），（M x）]？x，y：U应用[R（a，c），m，z：U.R（x，y）→R（y，z）→R（x，z），（M x y）]？x，y，z：U应用[R（a，c），R（x，y）→R（y，z）→R（x，z），（M x y z）]？x，y，z：U. ？p：R（x，y）应用[R（a，c），R（y，z）→R（x，z），（M x y z p）]？x，y，z：U. ？p：R（x，y）。？q：R（y，z）应用[R（a，c），R（x，z），（M x y z p q）]？x，y，z：U. ？p：R（x，y）。？q：R（y，z）[R（a，c）<$R（x，z）]（M x y z p q）？y：U。？p：R（a，y）. ？q：R（y，c）（M a y c p q）在最后一步，我们看到了另一个潜在的问题一般来说，对一个策略术语的一个子术语的评估可能会影响另一个子术语是否评估以及评估什么例如，在上下文A：Prop，g：A→A，？m[]：Prop项（[A<$A].λf：A→A.f）（λx：m[ ].gx）不能被评估为良好类型的项，而项（[m[]<$ A ].λf：A→A.f）（λx：m[].gx）的计算结果为（λf：A→A.f）（λx：A.gx）（定义展开因此，我们应该确保语义学正确地捕捉到策略术语评估的副作用2.5战术层策略通常可以被描述为通过求解和引入由策略项生成的元变量来转换证明状态的映射。最基本的战术是战术运用战术。 它将一个策略术语作为参数，在当前目标的上下文中对其进行评估，并根据策略的规定实例化和引入元变量。其他策略包括不同类型的组合、故障处理、处理命名的策略等。不幸的是，由于篇幅限制，我们不能详细讨论战术及其语义。在第4.1节中，我们将对策略应用tactical的语义意图进行描述，因为这对于我们讨论策略术语的语义是必不可少的G.I. Jojgov，H. Geuvers / Electronic Notes in Theoretical Computer Science 93（2004）118-127应用[：Prop，：Prop，M：]：=[].M其他[？A，？B：提案：A.B]。？m：A. 应用[，B，（Mm）] else[？A：类型，？B[x：A]：Prop[x：A.B [x]]。？m：A. 应用[μ，B[m]，（Mm）]3定义一些基本策略下面我们用我们的语言给出（递归）定义，这些定义代表了基于策略的交互式定理证明器中的一些常见策略。按照惯例，战术的第一个参数总是该战术所解决的目标。策略Cut和Assert通过引入一个语句并证明→和来解决目标。两者之间的区别在于新目标产生的顺序。介绍[：Prop]：=[A，B：Prop_x：A.B].λx：A.Intros[B]else【类型A：类型，B[x：A]：属性x：A.B [x]】。λx：A。Intros[B[x]]else？m：m介绍战术需要一个目标，并尽可能长时间地尝试应用介绍规则。例如，Intros[xU.P（x）→Q（x）]得到项λx：U.λp：P（x）.m[x，p]，其中m是一个新的元变量，带有声明m[x：U，p：P（x）]：Q（x）我们已经在第2.4节中看到了该策略的应用。它试图通过用证明M专门化定理M来产生一个类型为M的项。切[：道具，：道具]：=？p：n → n。？q：（p q）断言[：Prop，：Prop]：=？q：？p：n → n。（p q）128G.I. Jojgov，H. Geuvers / Electronic Notes in Theoretical Computer Science 93（2004）118-泛化[B：Prop，U：Type，t：U]：= [B[t]？B[x：U]：Prop[x：U]。？m：U.B.[x].mt策略概括在某种意义上是应用的对立面。给定目标和项t，它产生一个新的目标x.B[x]，使得是它被t特化的（即使得B[t]）。这种策略用于证明一个变量的所有值的陈述比证明一个特定的值更容易的情况。它的有效性在很大程度上受到一个人使用的统一机制的力量的影响。4操作语义到目前为止，我们已经介绍了交互式定理证明器的抽象模型在本节中，我们将介绍允许我们“执行”策略术语的规则如前所述，一个成功的战术评估应该产生一个旨在实例化给定目标的术语。评估可以具有副作用，其形式为引入新目标和/或实例化预先存在的目标以及甚至新引入的目标。给定一个状态Γ，？m[m]：A，rJ=M：B，上下文r表示目标m的状态上下文。上下文m将被称为m的局部上下文。当我们将一个战术项t应用于目标时，我们将得到一个项N，它在目标的上下文中应该是A型的。使问题复杂化的是统一约束可能具有的非局部效应。这意味着在我们评估策略项之后，目标的上下文Γ可能会改变，因为它的一些元变量已经被求解或引入了新的元变量。因此，我们将使用如下判断：|= ⟨Γ; ∆⟩ D t ⇒ ⟨ Γ J; ∆ J⟩ D N : A这个判断应该被理解为：正如它的名字所暗示的那样，MySQL只包含变量声明。元变量在状态上下文中声明。例如，考虑以下判断：|=⟨A: Prop; ε⟩DIntros [A → A] ⇒ ⟨A: Prop,? n[x：A]：A;ε<$Dλx：A.n[x]：A→AG.I. Jojgov，H. Geuvers / Electronic Notes in Theoretical Computer Science 93（2004）118-12911111在状态上下文A：Prop和空局部上下文中，我们评估策略Intros[A→A]。结果，我们得到了一个新的状态上下文，其中有一个新的Meta变量n[x：A]：A和类型为A→A的项λx：A.n[x]。4.1战术运用在定义语义评估关系之前|=我们将展示我们打算如何在实际将策略应用于证明状态的策略应用程序中使用它。设Γ1，？m[m]：A，Γ2<$M：B是当前状态。假设我们想把策略项t应用到m上。首先，我们在状态上下文Γ1和局部上下文Γ 2中评估t的 定义|=是这样的，本地上下文被保留：|= ⟨Γ1; ∆ ⟩ D t ⇒ ⟨ Γ J; ∆ ⟩ D N : C接下来，我们检查在上下文ΓJ，Γ j中，期望类型A是否βδ-等于实际类型C。如果是这样的话，那么我们构造一个新的状态：rJ，m [m]：=N：A，r2<$M：B请注意，语义必须确保在上下文ΓJ，中，项N实际上是类型C的，并且ΓJ包含Γ1的所有元变量（一些元变量），变量可以转换为定义，并可以添加新的定义）和确切的变量Γ1。这些要求一起构成了我们语义的可靠性标准（见定理4.8）。4.2战术术语有两种判断。 判决|= r;Dt rJ; DFail表示评估失败，判断|= r;d t rJ; d N：A表示在新状态下成功地将t求值为类型A的项N上下文ΓJ和局部上下文Γ j。语义由统一的oracle参数化。这个预言是一个外部函数uni（Γ， r，M，N），它将用于解决类型化的统一问题。我们假设uni（）是一个全递归函数，它要么为M和N在上下文中产生一个unifier，要么产生一个值Fail，表明没有找到unifier。我们注意到，由于高阶unifier的不可判定性，找不到unifier并不一定意味着它不存在由于在2.3节中给出的原因，我们分离了表示“匹配变量”的Meta变量上下文，130G.I. Jojgov，H. Geuvers / Electronic Notes in Theoretical Computer Science 93（2004）118-|= ⟨Γ; ∆⟩ D M ⇒ ⟨ Γ J; ∆ ⟩ D P :A|= ⟨Γ; ∆⟩ D (M else N) ⇒ ⟨ Γ J; ∆ ⟩ D P :A（ele+）|=⟨Γ;∆⟩D M ⇒ ⟨ΓJ; ∆⟩D Fail|=⟨Γ;∆⟩D N ⇒ ⟨ΓJJ; ∆⟩D Q : A|= ⟨Γ; ∆⟩ D (M else N) ⇒ ⟨ Γ JJ; ∆ ⟩ D Q :A（else−）|=⟨Γ;∆⟩D Prop ⇒ ⟨Γ;∆⟩D Prop: Typeuni（（r， n），n，M，N）=σ|（P）|Σ (P) ⇒ ⟨ΓJ; ∆⟩D Q: A|= ⟨Γ; ∆⟩ D [M ∼ΣN].P ⇒ ⟨ Γ J; ∆ ⟩ D Q :A（uni+）|=⟨Γ;∆⟩D Prop ⇒ ⟨Γ;∆⟩D Prop: Typeuni（（r， n），n，M，N）=未通过|=⟨Γ;∆⟩D [M ∼ΣN].P ⇒ ⟨Γ;∆⟩D Fail（uni−）|=⟨Γ,? m1[]：A;DM [m1[]/m]rJ;DN：B|=⟨Γ;∆⟩D? m：A.MrJ;DN：B（MV介绍）m1是新鲜的|=⟨Γ;∆⟩Dti⇒⟨Γ;∆⟩Dti:Ai[tj/xj]j

下载后可阅读完整内容，剩余1页未读，立即下载