理论计算机科学电子笔记174（2007）125-142www.elsevier.com/locate/entcs英文名称：Step by Step Tactical克劳迪奥·萨塞尔多蒂·科恩1恩里科·塔西2斯特凡诺·扎奇罗利3博洛尼亚大学计算机科学系Mura Anteo Zamboni，7 - 40127Bologna，ITALY摘要大多数最先进的证明助手都基于过程证明语言、脚本，并依赖于LCF战术作为战术组合的主要工具。 在本文中，我们讨论了这些成分如何不能很好地与用户界面交互的基础上，相同的交互范例的一般证明（事实上的标准，在这个领域），识别在粗粒度的战术评估的关键问题。我们提出Tinycals作为LCF战术子集的替代方案，表明如果以更细粒度的方式评估战术，用户不会遇到同样的问题。我们提出了正式的操作语义tinycals以及他们的实现在Matita证明助手。保留字：交互式定理证明，小步语义，策略1引言一些最先进的交互式定理证明器基于过程证明语言;用户主要通过记录执行命令的文本脚本与系统交互在证明过程中允许进展的命令被称为策略，并以原子方式执行。NuPRL [10]，Isabelle [6]，Coq [13]和Matita4（我们在博洛尼亚大学的团队正在开发的证明助手）是这些系统的几个例子。最著名的证明助手只提供声明性证明语言是Mizar [8]，而其他一些则将声明性证明语言叠加在过程核心之上。这一类中最著名的系统是Isabelle，它在Isabelle/Isar变体中向用户提供声明性的Isar证明语言[14]。除了Mizar之外，这两种系统共享相同的用户界面范例，灵感来自CtCoq的开创性工作[2]，现在体现在1sacerdot@cs.unibo.it2tassi@cs.unibo.it3zacchiro@cs.unibo.it4http://matita.cs.unibo.it1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.026126C.S. Coen等人理论计算机科学电子笔记174（2007）125定理lt_O_defactorize_aux：\forall f：nat_fact.\for all i：nat.O< defactorize_aux f i.介绍。埃利姆湾简化。展开l.rewrite>times_n_SO。应用le_times。改变（O<\pi_i）。应用lt_O_nth_prime_n。时间复杂度为O（\pi _ i）^n应用lt_O_exp.应用lt_O_nth_prime_n。simplify.unfoldlt.rewrite> times_n_SO.应用le_times。时间复杂度为O（\pi _ i）^n应用lt_O_exp.应用lt_O_nth_prime_n。变化（O< defact n1（Si））。应用H.定理lt_O_defactorize_aux：\forall f：nat_fact.\for all i：nat.Otimes_n_SO;应用le_times;[用（O\pi_ i）改变;应用lt_O_nth_prime_n|二、三：时间复杂度：O（\pi _ i）^n应用lt_O_nth_prime_n| 变化（O< defact n1（Si））;应用H]]。Fig. 1. 同样的证明有（在右边）和没有（在左边）战术。一般证明[1]。在这种范式中，可以原子地执行的最小数量的代码是语句，在证明过程中，它要么是一种策略（在过程世界中），要么是一个证明步骤（在声明世界中）。只有通过一步一步的执行，从系统中获得关于证明状态的反馈，才能理解证明。由于反馈只在原子步骤之间（在所谓的执行点）给出，因此为了理解，而且为了调试和证明维护，尽可能小的原子步骤是很重要的。这与战术相反，更高阶的结构可以用来将战术组合在一起。在本文中，我们提出了一个替代战术，以获得更小的原子执行步骤。我们的工作在声明性证明语言的上下文中不相关。然而，那些可以在声明性证明步骤中嵌入过程脚本的少数系统可能已经提供了我们建议的功能。战术最早出现在1979年的LCF定理证明器[5]中。战术的典型例子是顺序组合和分支。[5]前者，通常写为后者，“t ;[ t1| ··· |tn]"，采用n + 1策略，将t应用于当前猜想，并且要求t返回正好n个猜想，将t 1 应用于第一个返回的猜想，将t 2 应用于第二个，等等。Tactical改进了过程证明语言，提供了具体的优势，我们用图1来说明。图中使用的具体语法是Matita证明助手的语法。证明结构。使用分支，证明的脚本表示可以模仿证明树的结构（该树具有作为节点和策略标记的弧的结构）。由于证明树分支通常反映5在本文中，术语C.S. Coen等人理论计算机科学电子笔记174（2007）125127笔和纸证明，分支策略有助于提高脚本的可读性（平均来说非常差，如果与声明性证明语言相比）。甚至证明脚本的可维护性也可以通过使用分支来提高，例如当假设被添加、删除或置换时。例如，在图1的右边，现在可以清楚地看到elim f将证明分成两个分支;这两个分支（由“[1，2：“选择）都以相同的策略开始，直到每个分支通过应用le times引理再次分裂。 在四个分支中，第二和第三个分支（由“|2，3：“）是用同样的策略来证明，证明同样的事实。所有不遵循分支的策略都不会在证明中引入分支。在实践中，左手边的证明将通过使用指示符和空白行来理解分支的开始和结束。这种方式提高了可读性，但对证据维护的影响较小。此外，系统不会以任何方式验证证明的布局，并且在脚本更改时不保证一致性。我们预计，一旦出现一种没有缺点的替代方案（而不是LCF战术），用户就会放弃这种行为。请注意，我们在本文中提出的一次选择多个分支是对标准分支策略的改进简洁。代码分解是编程中的一个很好的实践，证明分解是定理证明。使用像顺序组合这样的策略减少了在证明脚本中复制和粘贴的需要，有助于在证明中分解在图1中简洁性是明显的。在我们所知道的所有证明助手中，战术是原子地评估的，并且不允许将执行点放置在复杂战术的中间（例如在图1中，这意味着在证明的开始处具有执行点并要求系统向前移动它（即执行下一条语句），用户将导致用户检查这些状态的唯一方法是手动解构复杂的战术，这是一种常见的需求，例如脚本维护或证明演示。tacticals的大步骤评估在证明作者如何开发他们的证明方面也有缺点。由于不可能总是预测复杂战术的结果，以下是常见的做法：(i) 评估脚本的下一个策略;(ii) 检查返回的一套照片;(iii) 决定使用(iv) 如果是：撤回最后一个语句，添加策略，转到步骤（i）。最后，但同样重要的是，战术的大步评估的不精确的错误报告。考虑脚本中断的常见情况，128C.S. Coen等人理论计算机科学电子笔记174（2007）125系统返回的错误信息可能涉及用户未知的内部状态，因为整个战术是立即评估的此外，错误消息可能涉及脚本中没有逐字出现的术语。找到需要修正的陈述通常是用由外向内的恒等策略替换策略，直到找到唯一失败的策略。这种技术不仅容易出错，而且在存在边项（除了应用它们的边项之外的策略关闭语句）的情况下甚至不可靠，因为恒等策略没有边项，并且证明的分支可能会因为它们的缺失而被删除。我们声称，战术和一般证明之间的紧张关系，如接口可以被打破。在本文中，我们提出了一个微小的语言的战术-所谓的tinycals-解决了这个问题。Tinycals可以在很小的步骤中进行评估，使执行点能够放置在复杂的结构中，如管道或分支结构。这一目标是通过解构战术的语法并将语义描述为评估状态上的转换系统来实现的，评估状态是比证明状态战术作用的结构更丰富的结构。注意，解构并不一定意味着改变战术的具体语法，而是允许解析和立即评估战术片段，如本文的结构如下。第2节描述了tinycal的抽象语法及其小步操作语义。tinycals相对于LCF战术的其他优点也在那里讨论第3节介绍了tinycals在Matita中的实现。第4节涉及tactical不包括tinycals。第5节讨论了相关工作，第6节总结了本文。2 Tinycals：语法和语义tinycal的语法在表1中报告，其中，tinycal是生成脚本语言的顶级非参数。L每个语句要么是一个原子的tactical语句（标记为“tactical“），要么是一个tinycal语句。注意，与tinycals本身相关的语法部分是完全去结构化的。在tinycals的语法中嵌入LCF tac-ticals（非终结符的语法）的结构化语法的需要将在第4节中讨论。目前，读者可以假设语法仅限于这种情况B我们现在将描述tinycals的语义，它在证明状态策略作用时以及它们的语义中是参数化的（参见表2）。校样状态是当前校样的逻辑状态。 它可以被看作是当前的证明树，但它实际上不需要是一棵树。 例如，Matita只是保留了一组要证明的结构，以及一个证明项，其中元变量出现在缺失的组件中。从语义的角度来看，证明状态是一种抽象数据类型。直觉上，它必须至少描述一组尚未证明的命题。Goal是另一种用于索引结构的抽象数据类型。apply tac函数实现策略应用。 它作为输入C.S. Coen等人理论计算机科学电子笔记174（2007）125129表1tinycals的抽象语法和核心LCF策略。S简体中文（zh_cn）S|SB联系我们（tactical）|“（恢复期）|“（循环）|B（composition）|B（分支）B|“我...... “ 的|“B”]“T（战术）表2语义参数。证明状态：证明目标：目标战术运用：运用战术：T→目标→目标×目标列表×目标列表一个策略、一个证明状态和一个目标（策略应该作用的推测），并返回一个证明状态和两个目标列表作为输出：新打开的目标集合这种选择使我们的语义能够解释副作用，即：策略可以关闭目标，而不是它们所应用的目标，这是通过存在或元变量在几个证明助手中实现的功能[4，9]。在低成本竞争中，由于缺乏元变量和副效应，策略不能直接操纵证据状态。在本节的其余部分，我们将把tinycal的语义定义为求值状态的转换（用−→表示）。评价状态定义见表3。状态（代码）的第一个组成部分是tinycals语法的语句列表。每次转换都会使用该列表，每次使用一条语句。这种选择是由我们语法的非结构化形式所指导的，tinycals的细粒度执行第二个组件是证明状态，我们用上下文堆栈来丰富它(the第三部分）。上下文堆栈，一个证明历史的表示，|“.”（点）|“;”（张文）|“[”（分支机构）|“|“（轮班）|i1，.. .， in“：“（预测）|“(wild卡）|“接受”（确认）|“]”（合并）|“（选择）|“完成”（取消选择）130C.S. Coen等人理论计算机科学电子笔记174（2007）125表3评价状况。task = int×（Opengoal）|关闭目标） （任务）r =任务列表（上下文）τ=任务列表（κ=任务列表（点ctxt tag=B |F（栈级标记）ctxt栈=（Γ×τ×κ×ctxt标签）列表（上下文栈）code=Slist（statements）status=code×code×ctxt stack（评估状态）far，被处理为堆栈：当分支tinycal“[“被求值时，或者当“focus“被求值时，级别被推到它的顶部; 由于语法是非结构化的，我们不能确保静态正确的tinycal嵌套，因此，每个堆栈级别都配备有一个标记，该标记用创建tinycal对其进行注释（B表示除了标签之外，每个栈层还具有三个分量Γ、τ和κ，分别用于活动任务、推迟到分支结束的任务和由““响应的任务。“.这些组件的作用将在对作用于它们的tinycals的描述中解释。 每个组件是一系列编号的任务。一个任务是一个处理器，要么是一个尚未证明的猜想，要么是一个已经被一个副作用关闭的猜想在后一种情况下，用户必须使用“accept“来确认实例化每个评估状态对用户来说都是有意义的，并且可以通过修改已经存在的用户界面。我们的展示选择在第3节中描述。不耐烦的读者可以偷偷预览图2，其中证明状态的有趣部分被呈现为要证明的假设的笔记本，并且推测标签通过以下方式表示来自上下文栈的相关信息：1）粗体文本（对于当前选择的分支中的假设，下一个策略应用的目标;它们被保持在栈顶部的I分量中）; 2）下标（对于兄弟分支中尚未选择的假设;它们被保持在栈顶部以下的级别的I分量中）。堆栈中保存的其余信息不需要显示给用户，因为它不影响用户的即时操作。我们首先描述tinycals的语义，它不涉及在堆栈上创建新的级别。语义如表4所示，其中使用了一些效用函数（在附录A中描述）。战术运用考虑表4中tinycals语义的第一种情况。它使用堆栈级别的第一个组件（表示为Γ），表示C.S. Coen等人理论计算机科学电子笔记174（2007）125131nnnn表4基本tinycals语义。⟨wherere[g1;· ··;gn]=获取任务列表（r）中的所有⎧⎪⟨ξ0,Go,Gc⟩=⟨ξ,[],[]⟩⎪0 0⎪oo o c c和⎨⟨ξi+1,Gi+1,Gi+1⟩=⟨ξi,Gi,Gi⟩gi+1∈Gi⎪⎪⟨ξi+1,Go ，Gc<$=<$$>J，（Go\Gc）<$Go，Gc<$Gc<$gi+1/∈Gc简体中文⎪i+1i i i i当ererJ，Go，Gcr j=applytac（T，g， g）时，i i+1且SJ=<$rJ，τJ，κJ，t：：封闭任务（Gc，S）和ΓJ =标记为已处理（Go）和τJ=移除任务（Gc，τ）和κJ=移除任务（Gc，κ）““当r rr r=[nj1，Closedg1n;·· ·;njn，Closedgnn n]n≥1且dGc=[g1;· ··;gn]和SJ=[]，移除任务（Gc，τ），移除任务（Gc，κ），t*结束任务 （Gc、S）“嗯”。”“嗯”。”其中get open tasks（Γ）=[ ]这是下一个被评估的策略将被应用于的目标集合当评估一个策略时，检查当前目标的集合Γ（期望至少找到其中一个），然后依次将该策略应用于每个目标，以获得最终证明状态。在每一步i，两个集合Co和Gc我我更新到目前为止打开和关闭的目标这个过程对于用户来说是原子性的(i.e.当该策略被应用于每个当前的132C.S. Coen等人理论计算机科学电子笔记174（2007）125applytrans_eq;[apply H|应用H1|接受]tac1;[ tac2. tac3。|tac4;[tac5 |tac6]]目标），但她可以自由地使用分支来铸造原子性。在将该策略应用于所有目标之后，将创建新的当前目标集，其中包含在应用期间已打开但尚未关闭的所有目标。它们被标记（使用标记为已处理实用程序），以便它们不满足未处理的谓词，这表明已经对它们应用了某种策略。由边线球关闭的球门将从τ和κ中移除，并在S中标记为关闭。的读者可以在附录A中找到该程序的详细说明。顺序组合由于排序是由Γ处理的，所以“;“的语义我们将其保留在tinycal的语法中，以保持与LCF tacticals的并行性。侧面碰撞处理“例如，考虑存在用户分支的两个当前目标的情况。对第一个目标采取策略可能会关闭第二个目标，删除脚本中第二个分支的需要。使用tinycals，用户永远不会看到她意识到的分支在没有通知的情况下消失因此，像上面这样的情况被处理，在堆栈上将分支标记为Closed（使用close tasks示例2.1考虑以下脚本：其中的应用程序的传递性性质的平等的猜想L=R打开了三个命题？1：L=？3，？2：？3=R和？3：nat.应用假设H实例化？3，隐含地关闭第三个猜想，因此必须承认。局部解构只要脚本结构模仿证明背后的直觉结构，证明脚本的结构化就可以增强其可读性出于这个原因，作者并不总是希望将证明脚本结构化到证明树的最远叶。示例2.2考虑以下脚本片段模板：在这里，作者试图模拟证明的结构（两个主要分支，在第二个分支中还有两个分支），而不关心第一个分支的结构。C.S. Coen等人理论计算机科学电子笔记174（2007）125133tac1;[tac2 |tac3]; tac4Tacticals不允许将非结构化脚本嵌套在分支中。在这个例子中，他们只允许用身份策略替换第一个分支，继续非结构化的片段“tac2”。 tac3。” 在代码片段的末尾，但是这样脚本结构和证明树之间的对应关系将完全丢失。tinycal的语义“。”当“。“应用于当前目标的非空集合，第一个被选择并成为新的单例当前目标集合Γ。剩余的目标在当前堆栈级别的第三个组件（点的延续，表示为κ）中被重新记录，以便当“。“再次应用于一组空的目标，它们可以依次被召回。的地方”。” is inherited by the locality of dot’s continuation表5描述了需要堆栈规程的tinycal的语义。分支对分支的支持由“[“实现剩余的目标（当前分支上下文）存储在新创建的目标之下。有三种不同的选择方法。重复使用“|“按顺序使用分支上下文。i1，.. 、.、in“：“启用目标的多个位置选择从分支上下文中。作为新的当前目标。所有这些分支策略的语义如表5的前五种情况所示。每次用户完成对当前目标的工作并从分支上下文中选择新目标时，她的工作的结果（即，r）需要被保存以便在分支构造结束时恢复。这是实现LCF语义所必需的，该语义为如下代码段提供支持：实施例2.3其中由应用TAC2和TAC3产生的目标被重新组合在一起以创建为TAC4设置的目标。我们存储它们的地方是堆栈级别的第二个组件（todo list，表示为τ）。每次使用分支选择tinycal时，当前目标集（可能为空）都会被附加到当前堆栈级别的todo列表当134C.S. Coen等人理论计算机科学电子笔记174（2007）125表5分支tinycals语义。<其中，重新编号分支（[l1;·· ·;ln]）=[lJ;···;lJ]1N并且SJ=k[LJ]，[]，[]，Bj：：k[LJ;···;LJ]，τ，κ，τ=：S1 2N“|“：：c，，r，τ，κ，B：：[ l 1 ; · · · ; l n ]，τ j，κ j，t j：：S − → c，，S j n ≥ 1当SJ=π[l1]， τj得到任务s（r）πκ，[]，Bπ：：π[l2;· ··;ln]， τJ，κJ，tJπ：：S时，i1，.. 、.、 in“：“：：C，，[ L ]，Τ，[ ]，B：：R J，Τ J，Κ J，T J：：S − → C，，Sj如果未处理（l）andj=1.. . n，nlj=nj，sjn，lj∈l：：ΓJandSJ=k[l1;·· ·;ln]，τ，[]，Bn：：k（l：：rJ）\[l1; ···; l n ]，τ j，k j，t j j = k [ l1 ;·· ·;ln]， τ ， [] ， B n ： ： k （ l ： ： r j ） \ [ l 1 ; ·· · ; l n ] ， τJ，kJ，tJ=：：S“如果未处理（l）和SJ=l：：ΓJ，τ， []，B：：[]，τj得到开放任务（Γ）κ，κJ，tJ：：S“其中SJ=<$τ<$get open tasks（Γ）<$τj <$κ，τJ，κJ，tJ< $：：S⟨wheeregi∈getopengolsinstatus（S）andSJ=kashandled（[g1;·· ·;gn]），[]，[]，Fn：：关闭任务（r，τ，κ，t：：S）“done“：：c，聚焦两个小家伙. . ““使用在这一点上，用户可以自由地按照她喜欢的方式工作，例如分支，但C.S. Coen等人理论计算机科学电子笔记174（2007）125135在调用“完成”之前，需要关闭所有这些“焦点”的预期用途“对结论或假设中含有元变量的猜想应用策略可以实例化元变量，从而使其他猜想为假。换句话说，在元变量的存在下，代数不再是独立的，并且考虑并关闭一堆或相关的代数变得至关重要，即使在证明的遥远分支中。在这种情况下，. .“或者，. . “请注意，使用“因为用户知道的所有目标，如果关闭，将被标记为关闭，要求她稍后在证明中手动3执行问题Tinycals已在Matita校对助手中实现。本节阐述了在执行这些建议时所面临的问题。战术编码战术人员在证明助手中扮演两个不同的角色。 它们可以在脚本和策略实现中使用。事实上，在每个派生策略的实现中，至少使用了顺序组合和分支中的一种在本文中，我们提出用tinycals代替tacticals。Tactical在证明状态下操作，而tinycals在评估状态下操作。当脚本中使用tinycals时，这是很好的，因为保存在评估状态中的附加信息是我们想要呈现给用户的丰富的中间状态。相反 ， 这 种 数 据 类 型 的 变 化 不 允 许 在 派 生 战 术 的 实 现 中 用 tinycals 替 换tacticals。因此，我们立即考虑是否有可能用tinycals来表示tacticals，以避免相关操作的独立重新实现。在对证明状态的抽象数据类型的附加假设下，答案是肯定的。直观地说，我们需要定义两个一旦实现了这两个函数，我们就可以将顺序组合和分支表示为：（t1; t2）（n，g）= proj（eval（embed（[t1;“;“;t 2 ]，n，g））（1）（t ; [ t1|... . . . 你 好 。 . |tn]）（n，g） =proj（eval（embed（[t;“[“;t1;“|“; . ;“|“; tn ;“]“]，n，g））（2）其中eval是−→的传递闭包。对于每个状态S，eval（S）为空。136C.S. Coen等人理论计算机科学电子笔记174（2007）125ξ嵌入函数很容易定义为：embed（c，n，g）=nc，n，[ng，[]，[]，Fn]n然而，为了定义proj函数，我们需要能够计算eval（embed（c，c，g））对任何给定代码c、证明状态c和选定目标g打开和关闭的目标集。前者很容易通过附录A的状态实用程序中的get open goals来计算。然而，要计算后者，存储在评估上下文中的信息是不够的。我们说，每当关闭的目标不能重新打开时，策略就不会重用目标具体地说，通过保持一个代表已使用的最高目标索引的全局计数器，可以在实现中尊重这一属性。当一个战术打开一个新的目标时，它会选择计数器的后继者，也会增加。当战术不重复使用目标时，可以通过比较序列两端的开放目标集来确定由一系列评估步骤为了进行这种比较，可以向证明状态抽象数据类型添加一个返回打开的目标集的方法设di_j为函数，给定两个证明状态，返回在_j中打开，在_J中关闭的目标集。对于每个证明状态，投影函数定义为：proj（[ ]，J，S）=（J，get open goals in status（S），di（，J））函数proj*必须在等式（1）和等式（2）中使用，以代替项目Tinycals用户界面Tinycals如果没有向用户呈现评估状态的方法，将毫无价值。我们当前的Matita用户界面解决方案如图2所示。我们已经有了一个类似Proof General的用户界面，其中包含脚本和执行点（图2的左侧），以及一组开放猜想（右侧）的序列表示，使用元变量索引作为标签。用户在使用tinycals时缺少的是堆栈的可视化表示我们的选择是将当前分支上下文表示为选项卡标签注释：当前目标集中的所有目标都有粗体的标签，当前没有带来任何变化，因为这些变化是由|n（其中r是位置索引），并且已经由旁项关闭的目标具有删除线标签，如：？n.例如，在图2中，下一个策略将被应用到的唯一目标（粗体）是20（即，r= [101，打开20圈]），而目标21将被下一个“|“tinycal。这种选择使用户知道哪些目标将被执行点评估的策略所影响，以及她可能需要的所有索引信息。她确实可以看到当前分支上下文中的所有元变量索引（如果她想要"聚焦"）和目标的所有位置索引C.S. Coen等人理论计算机科学电子笔记174（2007）125137图二. Matita用户界面中的评估状态表示。(for i1，.. .，in“：“和“：“）。然而，这种用户界面选择最大限度地减少了与使用Proof General之类界面的通常工作方式的偏差。4关于剩余战术的在基本的LCF策略中，到目前为止，我们只考虑了顺序组合和分支。值得讨论的是其余的，特别是尝试，|| (or-else) and repeat.尝试T策略，永远不会失败，应用策略T，如果T失败，则表现为身份。这是一个特殊的情况下，否则战术：T1||如果T1没有失败，则T2的行为与T1相同，否则与T2相同.因此，try T等价于T||ID.try和or-else策略出现在脚本中，有两种不同的用法。最常见的是在顺序合成之后：T1;尝试T2或T1; T2||T3。这里的想法是，用户知道T2可以应用于T1生成的一些目标（在第二种情况下，T3可以应用于其他因此，她面临两种可能性：要么使用分支并在每个分支中重复T2（或T3），要么使用顺序组合和回溯（封装在两个策略中）。 Tinycals或通过投影和通配符tinycals来更好地解决任何一种选择：T1; [i1，.，in：T2|T3]。后一种表达方式对读者来说也不是更有信息量，但它在计算上也更有效，因为它避免了将T2应用于多个目标（可能代价高昂）try和or-else的第二种用法是在重复策略中。重复T策略应用T一次，如果T失败则失败;否则，该策略递归地将T再次应用于T打开的每个目标，直到T失败，在这种情况下，它表现为138C.S. Coen等人理论计算机科学电子笔记174（2007）125身份策略有没有可能提供一个非结构化版本的try T，T||TJ，并按照tinycals的精神重复T，以便允许用户编写和执行T步骤通过逐步检查中间评估状态？答案是否定的，正如我们在最简单的情况下可以很容易地看到的那样，即尝试T。考虑声明T;try（T1;T2）其中顺序组合应该由相应的tinycal提供。让T打开两个目标，并假设当用户执行T1时，T1可以按预期顺序应用于两个目标。设T为应用T后的证明状态，设T1和T2分别为应用T1现在让用户执行标识tinycal为了尊重战术的预期语义，应该部分地回溯状态1002以撤销从1001到1001的更改，保留从1001到1002的更改。如果系统有副作用，则后一个操作是未定义的，因为应用于T1的T1可以实例化控制应用于T1的T1的行为的元变量。因此，撤销对第一个目标的T1应用也会使之前对第二个目标的T1即使系统没有副作用，证明状态可以部分回溯的要求也对证明状态的可能实现具有相当大的限制。例如，一个证明状态不能是一个简单的证明项，其中元变量的出现代替了假设，因为回溯一个策略将需要用元变量替换一个精确的子项，但是没有信息来检测哪个子项。作为最后的评论，最简单的解决方案是通过对第二个目标的完全回溯来实现部分回溯，然后将T1应用于第二个目标，这不符合tinycals的精神。通过这种实现，将T1应用于第二个目标将被执行两次，从而将计算资源的浪费扫到地毯下。唯一诚实的解决方案包括保持所有的战术，除了分支和顺序组合，完全结构化，因为他们现在。想要在T;try（T1;T2）之前检查T;tryT1的行为的用户必须通过原子地执行tryT1、手动回溯并从头执行try（T1;T2）来这样做。对于其余的战术，也得出了类似的结论。出于这个原因，在表1中给出的语法中，生产环境中的tagicalB列出了所有不包含在tinycal中的传统战术。注意，原子顺序组合和原子分支（如前一节所实现的）也被列出，因为tinycal不能作为tactical的参数出现。5相关工作过去对战术的语义有不同的表述。第一个介绍是由戈登等人在[5]中给出的。虽然更大的一套在他们的工作中描述了比这里考虑的战术，C.S. Coen等人理论计算机科学电子笔记174（2007）125139没有考虑内部证明状态的检查。证明当时没有类似将军的界面，以及带有副作用的元变量和战术在[7]中，Kirchner描述了Coq策略的一个小步骤语义。尽管tinycals比相应的Coq tactical具有较小的表达优势，(like“focus“，“focus：“，i 1，.. .，在“：“中，“[“的使用限制较少，以及由“实现的结构化工具。” and “在特别地，我们的语义仅假设抽象的证明状态和用于战术应用的非常一般的类型，而在[7]中，假设了用于证明树的非常详细的API。Delahaye在[3]中描述了Ltac，一种功能强大的元语言，用户和策略实现者都可以使用它Ltac比tinycals强大得多，它具有高级编程的典型结构，并定义了它们的归约语义。然而，由于它的目标是不同的，Ltac未能解决tinycals解决的交互问题。在[11]和[12]中提出了两种用于创作结构化HOL脚本的替代方法第一种方法，在Syme的TkHOL中实现此外，与HOL不同，我们考虑一个逻辑的元变量，可以关闭的侧效应。因此，战术关闭分支的顺序是相关的，必须在脚本中明确出于这个原因，我们支持tinycals，如i1，.. .，in“：“，这在TkHOL中是不需要的。第二种方法，由高桥例如，通过自动声明由最后执行的策略打开的每个目标的词元来实现语法指导的编辑。这种技术在元变量上失败了，因为它们在引理的语句中是不允许的6结论在本文中，我们介绍了tinycals的语法和语义，tinycals是一种战术语言，能够模仿一些在最先进的证明工具中广泛使用的LCF战术Tinycals相对于LCF策略的优势在于，它们的语法是非结构化的，并且它们的评估是逐步进行的，使用户能够在完成之前开始执行结构化脚本。可以检查中间证明状态，并支持带有侧面效果的策略。整洁的结果是更好地与基于CtCoq/Proof General范式的用户界面集成。还讨论了一些实施问题，并考虑将该方法扩展到其他战术，但结果不佳Tinycals已经实现，并用于Matita证明助理继续开发其标准库。使用过其他证明助手的用户，特别是Coq，认为它们是证明创作界面的重大改进。这不是一个很大的数字（在撰写本文时，我们的用户只是我们研究团队的成员），但足以激励我们的工作，希望看到他们很快在其他系统中被采用140C.S. Coen等人理论计算机科学电子笔记174（2007）125引用[1] 阿斯皮纳尔，D.，Proof General：A generic tool for proof development，in：Tools and Algorithmsfor the Construction and Analysis of Systems ， TACAS 2000 ， Lecture Notes in ComputerScience1785（2000）.[2] Bertot，Y.，CtCoq系统：设计和架构，计算的形式方面11（1999），pp。225-243[3] Delahaye，D.，“Concept i o n d e langage s pour r d'ecri re le e s p r eu v e s et l e s auto m a t i on s d an les out i l s d ' a id e ` a p r e u v e：un e' etud e dan s l e cad r e d u s y s t ` e m e C o q，”Ph. D. 她的妹妹，《居里夫人》（巴黎6号）（2001年）。URLhttp://cedric.cnam.fr/http：//www.example.com[4] Geuvers，H.和G.I. Jojgov，Open Proofs and Open Terms：A Basis for Interactive Logic，J。布拉德菲尔德，编辑，计算机科学逻辑：第16届国际研讨会，CLS 2002，计算机科学讲义2471（2002），页。537-552[5] 戈 登 ， M 。 J. C. 的 方 法 ， R. Milner和 C.P. Wadsworth ， Edinburgh LCF ： A Mechanical Logic ofComputation，Lecture Notes in Computer Science78（1979）.[6] 伊莎贝尔的校对助理http://www.cl.cam.ac.uk/Research/HVG/Isabelle/.[7] Kirchner ， F. ， Coq Tacticals and PVS Strategies ： A Small-Step Semantics ， in ： Design andApplication of Strategies/Tactics in Higher Order Logics，2003.[8] 开阳星的校对助理http://mizar.uwb.edu.pl/.[9] 穆尼奥斯角，“A C a l cul u s of Sub s t i tut i on s for Inco m p l e - P r o o o f R e p re s e n tat i o n inT y p e Theo r y“，Ph. D. 论文，INRIA（1997）。[10] NuPRL证明助理，http：//www. cs. cornell. edu/Info/Projects/NuPrl/nuprl. 赫特湖[11] Syme，D.，一个新的接口的持有-想法，问题和实现，在：高阶逻辑定理证明及其应用程序，第8届国际研讨会，TPHOLs 1995年，讲义在计算机科学971（1995年），页。第324-339页。[12] 高桥K.和M.Hagiya，作为编辑HOL策略的证明，计算的形式方面11（1999），pp.343-357[13] Coq开发团队，Coq证明辅助参考手册，http://coq.inria.fr/doc/main.html（2005年）。[14] Wenzel，M.，Isar-一个通用的解释性方法可读的形式证明文件，在：定理证明高阶逻辑，1999年，页。167-184。A效用函数由“[“或“自动选择的目标|“被称为未处理的，直到对其应用策略。未处理的目标只是被推迟（不移动到todo列表τ中）i1，. .，in“：“。由战术打开的目标被标记为已处理，以将其与未处理的目标区分开来。函数renumber branches被⎧trueifl =unhandled（l）=否则为falsemarkashandedled（[g1;·· ·;gn]）=[0，Openg1<$;·· ·;0，Opengn<$]renumberbranches（[i1，s1;·· ·;in，sn]）=[1，s1;·· ·;n，sn]C.S. Coen等人理论计算机科学电子笔记174（2007）125141⎪接下来的三个函数返回打开的目标或任务的状态或部分。打开的目标是那些对应于仍待证明的结构的获取打开的任务（l）=⎧如果l=[]，⎨i，Openg⎪如果l=hd：：tl，则禁用获取打开的任务（tl）获取任务列表中的未完成目标（l）=⎧如果l=[]，⎨g：：get open goals in tasks list（tl）ifl=0，打开g目标：：tl⎪在任务列表（tl）如果l=0，则关闭gl：：tl获取状态（S）中的未完成目标=⎧如果S=[]，⎨在任务列表（Γ@τ@κ）⎪⎪@get open goals in status（tl）ifS = r，τ，κ，：：tl为了保持脚本中的分支和证明中的分支之间的对应关系，如果目标在Γ中（跟踪打开的分支），则将由侧项关闭的目标标记为关闭否则，它们将被默默地从推迟的目标中删除（在todo listτ或dot continuation
我的内容管理
展开
