定理证明器中实数的机械化对实时系统验证具有实际意义

266理论计算机科学电子笔记42（2001）网址：http://www.elsevier.nl/locate/entcs/volume42.html16页使用理论解释来机械化定理证明器杰米盾牌1澳大利亚昆士兰大学软件验证研究中心4072伊恩·海耶斯2和大卫·卡林顿3澳大利亚昆士兰大学计算机科学与电气工程学院4072摘要定理证明器中实数的机械化对于实时系统的验证具有实际实数为经典数学分析（如微分和积分）提供了定理证明器我们已经采取的方法，使广泛使用的理论解释设施的互动定理证明Ergo最大限度地提高理论重用，从而减少定理冗余。开发的理论与哈里森的HOL版本进行了比较1介绍本文描述了在Ergo定理证明器[5]中使用理论实例化和解释来支持实数的发展和后续分析虽然选择Ergo是因为我们熟悉它，但这里报告的工作应该适用于任何为理论实例化和解释提供便利的定理证明器。Ergo可以定制为支持任何逻辑，并支持窗口推理证明范式[6]。窗口推理被设计为支持层次化的、目标导向的证明，并为子项的上下文提供支持Ergo使用Qu-Prolog [7]作为高级策略的元语言它为记录、浏览和回放样张提供了重要支持，1电子邮件地址：jims@csee.uq.edu.au2电子邮件地址：ianh@csee.uq.edu.au3电子邮件地址：davec@csee.uq.edu.au2001年由ElsevierScien ceB出版。 诉 操作访问和C CB Y-NC-ND许可证。希尔德，海斯和卡林顿267理论的无环图和一个强大的查询语言，与搜索的理论。这个项目的动机源于一个更大的项目，为实时精化演算提供工具支持[4，9]。实数是连续的，正是这个性质使得它们在处理实时系统时是可取的（如果不是必要的话）。例如，在涉及温度传感器的系统中，为了指定温度变化率的限制，可以使用标准微分演算（基于实数）如果实数不可用，则只能形式化地陈述离散模型的较弱性质2代表现实构造实数有两种方法：公理化和定义延拓。实数的公理化涉及到一个新类型的声明，使用新类型的运算符，以及实数的公理另一种方法，定义延拓，涉及根据现有的构造来定义实数。这涉及到最初创建一个模型的现实。例如，实数可以用柯西序列（有理数的收敛序列）来模拟实数的标准公理可以证明为模型的定理。数学家们已经发展出了丰富多样的代数结构，如幺半群、群、环和场。数学家通过定义它们的公理来识别代数结构，并且所开发的定理是许多数学结构之间共享的属性例如，实数与有理数、整数和自然数有许多相同的性质一旦一个模型被证明保持了代数结构的公理，代数结构的定理就可以用来推理这个模型。例如，整数形成一个阿贝尔群，加法作为运算符，零作为单位元，否定作为逆。引入更一般的代数结构的好处包括增加理论的重用和增加对系统有效性的信心作为许多以前的实数构造的结果，出现了三种对实数建模的技术[3]。表示实数是位置展开。这些是任意基数的无限数列（位置序列），例如，十进制或二进制。不支持优雅的算法，使用这种方法时，形式分析是繁琐的[3，pp.13-16]。Dedekind cutsDedekind [1]用所有小于它的有理数的集合来表示一个实数。这个集合被称为cut。切割必须满足几个属性。也就是说，割可能不是空的;它一定不是所有有理数的集合，Q;它一定是向下封闭的，也就是说，给定希尔德，海斯和卡林顿268割中的任何元素，所有小于该元素的有理数也必须在割中。最后，在割中必须不存在最大的元素，也就是说，对于割中的每一个元素，都有另一个更大的元素，也在割中算术运算的构造相当简单.例如，对于割集（有理数集）X和Y，X + Y ={x + y|x∈X<$y∈Y}然而，实数乘法的定义确实使证明复杂化了。如果一个割包含的有理数小于它所表示的实数，那么其中一些元素是负数。结果集，天真地使用以下实数乘法的错误定义，包含任意大的正数，因为两个负有理数的乘积是正数。因此，所得到的集合不是切割。XY ={x y |x ∈ X <$y ∈ Y}柯西序列这个方法用一组收敛到它的有理序列来表示一个实数Harrison [3]观察到通常归因于Cantor的Cauchy序列方法也由Meray探索在我们的工作中采取的方法是基于柯西序列。它们比位置展开式更容易处理，也比戴德金割更熟悉。本文的结构如下：第三节回顾了阐释理论和例证实施细节见第4节。在第5节中，该项目与HOL [3]中柯西序列方法第6节总结了项目的成果在[8]的附录A中可以找到发展中的每个理论的总结3解释和实例化实数的传统发展产生了一个定义良好的代数结构层次。这种幺半群、场等的层次结构是相当模块化的，并为理论重用提供了机会。Ergo通过以下机制为理论重用提供了实例化理论实例化用于句法包含。当一个理论被实例化时，就好像实例化命令在文本上被被实例化的理论所取代，除了理论符号被重命名。理论属性在重命名下被复制注意，来自被实例化的理论的公理仍然是实例化理论中的公理。例如，给定一个半群理论和一个恒等式理论，可以通过将它们实例化为一个新的理论来创建一个幺半群理论。希尔德，海斯和卡林顿269∗∗当一个理论M的定理需要在另一个理论N中使用时，使用理论解释。M的定理在N中是有效的，只要M的公理可以用N的性质证明成立。像实例化一样，因果解释将一个理论的性质复制到另一个理论中，除非公理映射到公设，否则必须在新的上下文中证明如果理论（例如，加法下的整数）被认为是另一理论的模型或具有另一理论的性质a组）。更正式地说，理论表示是一对P=L，G>，由一阶语言L和L中的句子集合G组成。<翻译I：L1→L2是从一种语言L1到另一种语言L2的映射，该映射将L1的每个符号重命名为具有相同语法声明的L2的符号（例如， Ari ty）。GivenP1=L1 ， G1>和 P2=L2 ， G2>，I： L1→L2是一个解释，如果当σ∈G1时I（σ）∈G2[2].理论层次更复杂的理论可以通过实例化和/或解释来组合理论。作为一个例子，一个环可以通过结合阿贝尔群的公理化（用环的“+”算子实例化群的算子）和半群的公理化（用环的“”算子实例化半群的算子）来公理化因此，环的理论包含了半群理论的两个实例，但由于算子的名称和它们的单位元是不同的，因此不会产生混淆。为了证明带运算符“+”和“”的整数Z为了使解释有效，环公理必须被证明为使用整数、整数加法和整数乘法的性质的定理。 一旦环公理被证明对整数成立，环定理就可以用来推理整数。Hamilton等人在Ergo [2]中对解释进行了更深入的讨论。理论解释和实例化的实际好处是：理论重用新的理论可以从现有的（在某些情况下是众所周知的）理论中建立起来，而不是重新公理化。这既减少了所需的工作，也减少了在公理化中引入错误的可能性例如，在命令式编程语言中，以顺序组合作为操作符的命令和以null命令作为标识符的命令形成了一个幺半群。通过引入理论来构建新理论的发展，人们提供了可能在未来应用中有用的新理论理论越一般，就越有可能被重用。实际上希尔德，海斯和卡林顿270只有在不同语境中使用的两套公理之间的相似性得到承认之后，才能承认一般理论在这种情况下，提取类似的公理来形成一个新的理论并将其实例化到不同的上下文中可能是有益的。定理重用所有为一个理论证明的（抽象）定理都可以直接用于该理论的实例化，也可以用于该理论的解释，如果在后一种情况下，解释定理的公理已经被证明成立。这为模块化证明提供了一个强大的机制，多年来4设计与实现4.1框架我们发展实数R理论的第一步是对场和有序场代数结构进行公理化。支持理论的层次结构如图1所示这个数字使用了继承这个术语继承是一种简单的实例化形式，其中不发生重命名在这种自下而上的发展中，有序场的公理化始于半群、交换性、逆和恒等式理论。紧接着是幺半群理论，然后是群、阿贝尔群等。到有序场理论这种理论层次结构增加了理论重用的机会，同时仍然限制了理论开发所需的数量。有几种方法可以建立代数结构的公理化虽然第3节提倡理论解释/实例化，但需要考虑其他替代方案，以确保做出最佳决策。公理化有序场的最简单方法是创建一个包含所有有序场公理、定义和定理的单一理论（没有缺乏模块性，缺乏定理可追溯性，以及重复许多类似定理是这种方法的问题一个稍微复杂一点的方法是为每个代数结构创建一个理论，并产生一个继承理论的线性链 这种方法解决了模型问题，但重复了理论。为公理化有序场而选择的替代方案涉及理论解释和实例化的使用。在理论解释方面，15个理论取代了估计的48个理论（其中4个是构造有理数的有序对的场性质，17个是有理数的有序场性质，17个是实数的有序场性质）。具体数字并不重要。许多理论的发展，但是，已被避免和使用理论解释增加了理论和定理重用的机会。在有序场理论的公理化之后，希尔德，海斯和卡林顿271Cauchy（柯西序列和实数）序列有序字段集合论无穷序列领域秩序古典Zermelo Fraenkel集合论古典Id（整环）Cringwid（有单位元的交换环谓词逻辑有序对算术类型理论Ringwid（有单位元的环）环阿贝尔群幺半群逆交换性半群身份解释实例化继承Fig. 1. 支持的理论有理数和实数。几个标准的Ergo理论直接用于模型的创建。对于有理数，Zermelo Frænkel集合论（zfc）是继承的。这有几个子理论。直接用于构建有理数模型的是有序对理论（o pair），经典算术理论（carith）：基于皮亚诺算术的整数理论，经典谓词逻辑（或一阶逻辑：FOL）理论（cpred）和类型理论（types）。为了构造实数的模型，使用了集合论无限序列的标准理论（seq）。该理论继承了零电流控制理论。有理数被建模为有序对S的等价类，其中每个对的第二个元素是非零的。希尔德，海斯和卡林顿272定义4.1（有序对）有序对集合的定义S=^Z×（Z\{0}）这些有序对并不能给出有理数的唯一表示因此我们引入了等价关系ρs和对应于S的一个元素的等价类。定义4.2（ρs）S上的等价关系ρs定义为：（a，b）∈S<$（c，d）∈S（（a，b）ρs（c，d））<$（a<$d=c<$b）定义4.3（equivclass）给定A，S的一个元素，A[A]ρs=^{w：S|（A ρsw）}定义4.4（有理数集）有理数是由ρ s确定的所有等价类的集合。Q=^{w：P（S）|Z：S·w=[z]ρs}虽然有理数的模型已经被定义，但典型的公理和定理还没有。然而，通过将有序场理论解释为有理数理论，使用Q作为集合，并在这个集合的元素上适当地定义场算子，所需要的只是证明有序场的公理对有理数成立，然后所有有序场的定理都可以用来推理有理数。接下来，使用有理数和无穷序列对实数进行建模。无限柯西序列是根据收敛的有理数序列定义的。有限柯西序列，当需要时，由递归序列建模，即，通过重复最后的理性广告。定义4.5（有理数以下）有理数序列的集合被定义为：seq（Q）=^N→Q定义4.6（cauchy seq）给定正有理数Q+、<有理数的排序运算Q、有理数的减法运算− Q和有理数的绝对值运算，| ·|Q，柯西方程定义为：Qω=^{v：seq（Q）|e：Q+·n：N·m>ne·n>ne·m|v[m]−Qv[n]|Q ne|v[n]|Q id op X =X。公理identity2 = X：set => X op id =X。%最后理论被关闭。这使得任何%更新到理论的公理%理论开发仍然是可能的。关闭理论下面列出了半群理论的公理化%建立了半群理论加法理论（半群）%其他理论是继承的。包括理论（[types，undef]，all）。%运算符和集合已声明。declare声明set。add operator（500，leftaserv给出了闭包和结合性公理公理闭包X：set和Y：set =>（X op Y）：set。公理assumption =X：set和Y：set和Z：set =>（Xop Y）op Z = X op（Y opZ）。关闭理论幺半群是包含单位元的半群。因此，半群和恒等式理论都需要被实例化。幺半群理论的Ergo来源如下所示%创建幺半群理论并继承其他理论。Monoid（monoid）包括理论（[types，undef]，all）。希尔德，海斯和卡林顿275% deconstruct幺半群声明set。declareadd operator（500，leftaserv，'op'）. 声明ID。%接下来，将半群理论实例化为%子理论么半群sg. 实例化（半群，么半群sg，[’set’ --->T[]）.%最后，恒等式理论被实例化为% subtheory monoid id.instantiate（identity，monoid id，[’set’ --->T’id’ --->[]）.关闭理论幺半群理论中的第一个实例化命令将半群理论中的闭包和结合性公理复制到幺半群理论中。该命令的第一个论点是更一般的理论，专门的定理是从那里创建的。第二个参数是给当前理论的子理论的名称，其中半群理论的公理和定理被复制。也就是说，实例化创建了当前理论的一个子理论，其中包含了重新映射的公理和定理。 第三个参数包含操作符和常数更名，用于将一般理论的公理和定理转换为更专门的公理和定理。第四个论证将一般理论的祖先理论映射到专门理论或当前理论的现有解释祖先。本文不要求使用这一论点。第五论证将在一般理论中解释的理论重新映射到当前理论的子理论。虽然这个映射在上面的例子中是空的，但它在下面被用来解释有序场论到有理数。公理化的过程，提供定理和实例化继续下去，直到有序域理论已经发展。在这个阶段，有理数被建模，有序场理论被解释为有理理论，以获得有序场的性质。有序域理论的所有公理必须在有理模型的上下文中得到证明，然后有序域的定理才对有理有效希尔德，海斯和卡林顿276由于Ergo模型中使用的有序对用场的性质来解释，有理数用有序场的性质来解释也就是说，给定整数有序对的类型定义s和等价关系s=（即定义4.2中的ρs），等价类被定义。定义equivclass（A）=set_of w：s（A s=w）。接下来，给定Ergo权力，理性的模型形成了define rationals_set =set_of w：power（s）（ex z：s（w=equivclass（z）。有理数是一个有序场。因此，我们从有序场理论解释到有理数理论，并表明有序场公理对有理数成立有理数的运算符和常数都以“q”为前缀，interpret（ofield，rationals_ofield，[’set’ --->T’zero’’one’’-’(S)’inverse’(S) ---><<’abs’(T)T[ofield_sg1-> rationals_sg1，ofield_sg2-> rationals_sg2，ofield_m->有理数_m，ofield_g->有理数_g，ofield_c1-> rationals_c1，ofield_c2-> rationals_c2，ofield_id1-> rationals_id1，ofield_id2-> rationals_id2，ofield_inv1-> rationals_inv1，ofield_inv2-> rationals_inv2，ofield_ring->有理数环，ofield_ringwid->有理数环，希尔德，海斯和卡林顿277ofield_cringwid-> rationals_cringwid，ofield_ag-> rationals_ag，ofield_id-> rationals_id，ofield_field-> rationals_field，ofield_order-> rationals_order]）。最后的论证把已经被解释为奥菲尔德的理论复制到理性奥菲尔德的子理论中，并根据提供的命名。例如，ofield有一个解释的半群子理论ofieldsg1。一个新的子理论，有理数sg1，通过复制ofield sg1并重新命名其符号来创建，如第一个参数所示正如一位匿名的评论者所指出的那样，这种子理论命名的列表打破了理论的模块性，因为ofield理论的理性必须知道ofield理论的子理论。这种解释形成了场理论中的29个公设，所有这些公设都必须被证明以确保解释是有效的。所述程序在复杂性方面不同，也有简单的程序，例如，1Q：Q（其中1Q是有理数），可能需要大量的证明步骤。在有理数被创建之后，实数被建模为柯西序列的等价类给定有理数序列、有理数序列、其他标准有理数算子和常数、序列索引定义cauchy_seq =set_ofw：rationals_seq所有e：有理数_set（e q> qzero =>ex ne：nats所有m：nats所有n：nats（m> ne和n> ne =>qabs（（w at m）q-（w at n））q e））。在定义了等价类“ceequivclass”定义实数=set_of w：power（cauchy_seq）(exan：cauchy_seq w = cequivclass（an））。有序场的性质然后被解释到实数理论中，其方式与上面用于有理数的方式相同。解释有效的理由遵循标准柯西序列发展证明。为了完成构造，通过证明上确界性质成立，实数被证明形成一个完备的有序场。最后，由于Ergo是一个基于窗口推理的定理证明器，因此需要每个新算子的子项的开放规则通常，增加的开放规则允许在等价关系下改变子项希尔德，海斯和卡林顿278因此，只要增加一个适当的开定则，就可以用对应于另一个柯西序列r2的等价类来代替对应于柯西序列r1的等价类，只要r1与r2byρQω相关。4.3工具设计注意事项Ergo的许多方面都影响了实数理论的设计所有工具面临的一些考虑因素是：当处理多个理论解释时，如果同一个算子在多个理论中使用，那么问题就出现了，这个算子属于哪一个理论。因此，可以通过用理论名称前缀算子来解决因此，为了使用有序场Ofield.+相比之下，为了使用实数加法，运算符的前缀是实数理论的名称真实+该解决方案被认为是次优的。最好能够提供一个默认值，在操作符未被预置时使用Ergo然而，这需要重新组织标准的Ergo理论，以避免名称冲突。在理论发展的某个阶段，有必要使用理论标识符重新映射，从标识符“op”指示的通用性改变'+'. 可以说，这种重新映射应该尽可能晚地进行也就是说，使用专门的语法可能会导致不正确的假设，即实数算术的语义是唯一适用的域。这应该与理论的可读性相权衡。也就是说，在这个级别上，定理的复杂性增加，使得维护者很难将它们解码到一个众所周知的和理解的领域，以便完成证明。人们赞成这样一种观点，即众所周知的实数域增强了理论的可读性。宏观解释Ergo的宏观（缩写）工具的一个缺点因此，当一个带有缩写的理论被实例化时，每个缩写都必须手动复制并使用重映射进行更改例如，ofield理论包含一个二进制减法运算符的缩写。T−R=^T+−R希尔德，海斯和卡林顿279当外场理论被实例化为理性理论时，抽象性并没有转移。因此，在理性理论中必须重复这种缩略语T−QR=^T+Q−QR为了帮助理论的易用性，提供了从整数到有理数的映射。此外，还提供了从有理数到实数的映射。这些映射简化了字面有理数和实数的构造。另一种方法是定义实数的一个子集对应于有理数，而这些有理数的一个子集对应于整数。这需要证明有理数子集满足有理数公理，或者它与前面给出的有理数模型同构。对于整数也需要类似的证明。因此，也可以定制的设施称为神谕。神谕使涉及文字有理数和实数的表达式的推理更容易。例如，一个合适的预言机可以用来将有理表达式[（1，2）]ρs+Q[（1，2）]ρs自动地转换为[（1，1）]ρs。神谕也可以用来构造无限长的文字有理数，实数（的子集）自动使用位置展开5与以往工作的比较哈里森开发了一种该技术的目的是通过跳过理性的构建来后来，作为real的一个子集，创建了real实际上，Harrison遵循柯西序列方法，但他的发展等价于使用柯西序列，在这种情况下，指数从1开始，以O（1/n）的速度收敛到实数R，即柯西序列w，满足：B：N·|w [n] −R|

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