CASL中的间隔库实现与区间算术错误估计 - 理论计算机科学笔记 2007

理论计算机科学电子笔记184（2007）133-149www.elsevier.com/locate/entcsCASL中局部区间的实现Regivan H.N. 阿纳玛丽亚·圣地亚哥莫雷拉1DepartamentoodeInform'ticaMaticaAplicadaUniversidade Federal do Rio Grande do Norte天气-纳塔尔，巴西卡蒂安河洛佩斯2Instituto Tocantinense Presidente AntonioCarlosAragua'ına，Tocantins，Brazil摘要本文定义了在CASL（通用代数规范语言）中实现区间库的基础，使得区间表现为具有错误信息的实数。为了实现这一点，我们重新定义了[15]中定义的区间局部集的概念，以便它可以在CASL的底层逻辑中实现。有了这些结果，就有可能在CASL中操纵区间，就好像它们是实数一样，用等式推理，并免费获得对所得结果的误差估计（从所得区间的宽度）。本文介绍了CASL定义的间隔库，并提出了一个简单的例子，需要处理的数据与“公差”的裕度的案例研究保留字：代数规范语言，实数规范，区间算术。1介绍对（连续）数值数据进行操作的系统的严格规范和开发其中一些在形式规范语言中包含实数[13]和有理数[2]。这样的系统与近似值和错误信息一起工作，并且通过使用指定该数据的数据类型和函数的库来实现所选择的解决方案这些方法的优点在于代数定律与实数（或有理数）相同。因此，它足以赋予任何代数规范语言与这些库，并应用方程逻辑程序来验证系统。然而，这些解决方案缺乏处理1电子邮件：regivan，anamaria@dimap.ufrn.br2电子邮件地址：katianelopes@hotmail.com1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.03.019134R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133在系统使用基本上不可表示（通过有理数）的数字进行计算的情况下-例如，计算圆面积S=π·r2的简单系统，或需要公差信息的系统。此外，在许多情况下，错误信息的处理留给了实现阶段，当规范或设计者细化这些规范时，问题就会出现，因为必须处理错误。另一种方法，我们在这里处理的方法，是使用实数的区间表示。这种方法的优点是能够从一开始就表示任何实数和误差信息，即，从规格。然而，代价是完全失去了对实数数据有效的定理，因为（非退化）区间不满足实数的一些重要代数性质。下面我们给出了这个问题的解决方案：区间被视为带有错误信息的实数，而不仅仅是一组实数。这意味着一个实数（例如π）可以用包含它的任何区间来表示（例如[3，4]）。为此，有两种方法：（1）将区间算术改变为尽可能接近实数算术的行为[6];或者（2）我们改变等式的概念和区间代数的定律[14]。在第二种方法中，我们定义了一个称为区间局部等式的辅助等式来处理区间，以验证（仅）等式属性。这项工作扩展了[14，15]中的工作，因为它现在可以直接在代数规范语言（CASL）中实现，并且已经提供了执行有限局部方程推理的规则。然后，我们想将这些结果应用到一种形式化的规范语言中，这样它们就可以在软件开发过程中实际使用。CASL [2]是一种代数规范语言，在学术界已经很有名，它提供了一些对这项工作至关重要的特性特别是，它的强等式和存在等式，分别实现了Scott区间库是建立在CASL的基本有理函数库上的，可以在[5]中找到。第二节介绍了区间算术，并指出它不像实数那样构成一个域;第三节指出区间可以看作是实数的信息，并与一致性和相等性有关;第四节介绍了Scott的简单相等和Ω-集的理论，并将这些概念与CASL联系起来;第5节定义了局部相等和局部集合的理论;第6节定义了一个在CASL中实现的布尔区间局部集合;第7节介绍了指定所需的一些公理并证明了它们的可靠性;第8节展示了指定的一部分并使公理工作;第9节提供了一个示例应用程序，最后，第10节包含一些最终备注。R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133135∈2区间运算区间算术的思想是由摩尔在五十年代左右提出的，我们在这里称之为摩尔算术。一些其他的算术提案也随之出现，但它们都是基于以下含义的正确性(1)x∈[a，b]<$f（x）∈F（[a，b]）其中x，f（x），[a，b]是一个区间，f是一个实算术函数，F是f3的区间算术表示。正确性的概念是，如果你用区间计算，期望的结果总是在得到的区间结果之内此外，最大误差是该结果区间的宽度。换句话说，如果你使用区间来表示和计算实数，结果误差总是在结果区间F（[a，b]）中描述从具体化的角度来看，如果你用区间而不是准时表示（例如有理表示）来描述一个系统，那么对任何方程性质的验证都会导致对所涉及的误差的立即估计。下面简要介绍摩尔算法。2.1摩尔算法摩尔区间算法基于定义中给出的区间定义2.1 在定义2.2中定义的间隔相等。定义2.1给定x1，x2∈使得x1≤x2，：x1≤x≤x2}称为闭区间或这里只是区间，并表示为X=[x1，x2]。形式为[x，x]的区间是退化的，其中[x，x]是实数x∈的对应区间。所有区间的集合用（）表示。 如果x1和x2被限制为有理数，那么，我们定义所有具有有理数端点的区间的集合，并将其表示为（）。虽然这里提出的理论首先被定义为（），（）对于这项工作特别重要，因为它可以定义2.2[区间相等]间隔上的相等是基于它们的集合性质;即。如果两个间隔是同一集合，则它们被认为是不可分的因此，给定A= [a1，a2]和B= [b1，b2]，(2)A=B惠a1=b1惠a2=b2给定A，B∈ （）、和、减、乘、除的运算-在表1中定义，并遵守以下属性：(3)A<$B={a<$b：a∈A<$b∈B}3 区间正确性和最优性的完整形式化可以在[17，18，19]中找到。136R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133操作定义OBSA+ B=[a1+b1，a2+b2][minK，maxK][−a2，−a1]1 1[， ]a2 a1A+（− B）A×（1）BA× B=K={a1×b1，a1×b2，a2×b1，a2×b2}−A=1一=0/∈AA-B=A/B=0/∈B表1对A= [a1，a2]，B= [b1，b2]∈（）其中，n ∈ {+，−，×，/}是四种算术运算之一。注意，（3）简单地满足了上面（1）中描述的正确性。对于除法，Mor e ri th emest0 ∈/B。在这种定义下，intervalarititi c是通过将实数算术应用于区间的端点来定义的，并且在有理端点的情况下是平凡的计算。例2.3[3， 4]+[1， 3]=[3 + 1， 4+ 3]=[4， 7]，−[3，4]=[−4，−3]，等等。2.2Moore算法的代数性质在摩尔区间算术中，我们知道加法和乘法是结合和交换的，并且有一个单位元，加法是[0， 0]，乘法是[1，然而，加法和乘法都没有逆运算。实际上，对于非退化区间，A+（−A）= [0，0]。相反，它们具有伪逆运算，其中X−X<$[0， 0]和X/X<$[1， 1]。最后，乘法在加法上的分布被次分布性所取代：A×（B+C）<$A×B+A×C。这种代数性质的弱化给我们的实数表示目标带来了严重的后果，如例2.4所示。例2.4假设你想解方程X+[3，4]=[1，2]。 应用等式逻辑，你最多可以得到X+[−1，1]=[−3，−1]（根据摩尔算术），而不是X =[1，2] −[3，4]或X =[−3，−1]。在这个例子中，从等式的两边减去[3，4]应该在左边给我们X+[0， 0]，这反过来又会导致X，因为[0， 0]是+的恒等式，但是我们只得到[-1，1]<$[0， 0]，因为伪逆属性。在本文中，我们展示了一种方法来克服这个问题。3摩尔区间作为实数的信息上面所示的问题来自于所使用的间隔相等的性质，其中两个间隔被认为是相等的，如果它们是同一个集合。本节R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133137引入了另一种观点，它允许定义一个较弱的区间相等的概念，其中两个区间被认为是相等的，如果它们可以表示一些公共的实数集。这种方法同时将区间作为关于实数和相应误差的信息来处理在这种方法中，区间的宽度越小，所表示的实数的信息越好，并且相应的误差的质量越好。 Moore算法[9]的包含单调性是这种方法的基础。包含单调性是这个算法的一个非常重要的性质，因为它声明它保留了错误的质量;例如，如果A<$C和B<$D，即如果A中存在的错误质量优于C，并且B和D相同，则A+B<$C+D，即，A+B的误差优于C+D。Moore算法的这个性质产生了区间分析的域方法[1，14]。在下文中，我们引用一些定义和命题来证明这一点。定义3.1给定A，B∈（），A±B当且仅当B<$A。其中A±B读作命题3.2偏序（），±是有向完全偏序（dcpo）-参见[14]-。因此，考虑退化区间[a，a]为实数，这种方法将set（）视为实数上的Scott-Strachey [ 21 ]意义上的信息空间。有很多有趣的后果。 其中之一是，这种方法从区域理论的角度为通常的区间算法提供了基础。另一个结果是，它将区间的观点从集合扩展到信息，最后一个观点是我们开始我们的方法的地方3.1一致性和平等领域理论中的一个概念是一致性，形式上：定义3.3给定一个偏序<$A，≤ <$A和x，y∈A，x与y相容，x=y，如果存在z∈A使得x≤z和y≤z。换句话说，x和y是一致的信息，如果它们提供了相同的在区间A，B∈（）的情况下，A=B当且仅当A<$B∈（）。表2建立了区间相等性和一致性之间的关系。你应该注意到，尽管实数的某些代数性质在区间上失效，但它们在一致性方面因此，即使经典的等式逻辑不能应用于使区间表现为具有错误信息的实数，我们也可以开发一种使我们能够做到这一点的一致性的等式逻辑。这种逻辑及其应用CASL是我们目前在这项工作。138R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133平等一致性x+（ y+ z）=（ x+y）+ z x+[ 0，0]= xx+ y= y+ xx− x<$[0，0]x×（ y× z）=（ x×y）× z x×[1，1]=xx× y= y× xx/x[1，1]x×（ y+ z）<$（ x× y）+（ x× z）x+（ y+ z）=（ x+y）+ z x+[ 0，0]= xx+ y= y+ xx− x=[0，0]x×（ y× z）=（ x×y）× z x×[1，1]=xx× y= y× xx/x=[1，1]x×（ y+ z）=（ x× y）+（ x× z）表2等式与一致性-x，y，z∈（）4CASL和Scott等式在本节中，我们将介绍由Dana Scott [20]引入的简单等式和等价的概念以及由Dana Scott和Michael Fourman [4]引入的称为Ω-集的相关模型我们还涉及到CASL中的等式。CASL [2，10]是由IFIP WG1.3发起的“代数规范和发展共同框架倡议”（COFI）提出的一阶代数规范语言从这个分类中产生的中心语言是CASL（通用代数规范语言），从中可以定义子语言和扩展。正确处理表示实数的区间和误差估计的能力可以被视为核心CASL语言的一个扩展。然而，核心语言中已经存在的功能足以指定我们在本文中提出的解决方案。 因此，我们的解决方案是通过包含一个CASL库，包含区间、局部相等和其他相关概念的定义。CASL的基本特征允许我们做到这一点，这两个等式如下所示。CASL中的偏性是用两个等式实现的：ex=y和存在性，用x=y表示。潜在的平等使下面的情况：这种等式适合于表示半群的结合律等定律e(i.e.x+（y+z）=（x+y）+z，其中x+（y+z）和（x+y）+z都是项它总是被定义的）。 第二种相等（强相等）使这些项能够被定义，并形式化以下情况：R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133139=他们是平等的形式上，强相等可以用存在相等的形式表示，公式如下：（四）x=y参与[（def（x）→ex=y）def（y）→ey=x）在平等的意义上，所有未定义的术语都是平等的。可以用CASL的第二个等式表示的理论的一个例子是范畴论。例如，对于可合成的态射x，y和z，对于未定义项x ∈（y ∈ z）和（x ∈ y）∈ z，我们有等式。因此，在CASL中，平等有两种含义：一种需要定义（存在这两种解释，以及其他允许它们被定义的解释。这些平等意义的理论和模型在[4，20]中得到了形式化e其中，CASL中的存在简单的相等和等价。简单（存在）等式的理论由以下公理给出（简单等式公理）e（1）Re：x x参与ef（x）;e e(2) 对称性：x=y→y=x;以及e e e(3) 传递性：x=y→y=z→x =z。CASL等式的第二个含义，在Scott的著作中称为等价（五）x=yParticipate（def（x）<$def（y）→ex=y）在这项工作中，遵循CASL约定，我们使用符号=表示强equality和equivalence（Scott4.1模型e”简单等式的模型，以及因此由CASL基本规范指定的集合，都是通常集合的推广。在下面我们提出这样的模型，称为Ω-集。它们是基于一些经典的代数概念，如偏序，格和Heyting代数[4，12，11]。完全海廷代数（英语：Complete Heyting algebra，cHa）可以被视为代数结构，并且经常被用来解释一些逻辑，如一阶直觉逻辑。它们用于谓词（关系）的赋值。在下文中，简单的等式、等价和可定义性被解释为上域是cHa的关系。由此产生的模型称为Ω-集[4]。定义4.1[Ω-集]给定 a cHa Ω， Ω-集 是 一 数学 结构 的 形式140R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133x=yx=x;e=.ΣeA，. =. ：A×A→Ω使得4：(1) 对称性：e ee e e(2) 传递性：x=y≤y=z≤ x=z。在任何Ω-集上，我们可以定义可定义性和等价性的关系e(1) 返回：def（x） =x=x;(2) equiv：x=y=def（x） def（y）x=y五、观察到Ω-集推广了经典集，其中cHa是众所周知的布尔代数{0， 1}。如3.1节所示，我们希望将一致性用作一种等价关系，它使我们能够像处理实数一样处理区间。然而，一致性不是区间上的传递关系。 例如，[1， 3]=[2， 5]和[2， 5]=[4， 6]，但是[1， 3]/=[4， 6]。由于简单的等式是传递的，它不足以形式化一致性。 接下来，我们将介绍 局部相等和局部集合的概念，在[16，15]中引入，以克服这个问题。局部等式不是原始等式，它是辅助关系（像任何其他关系一样，例如，（2）用简单的等式来定义5局部相等和局部集合假设简单等式（或CASL术语中的存在等式）为原语，局部等式是一个在传递公理上有先决条件的关系。这个想法是控制传递律的应用，使得它不是对所有元素x，y和z的三元组都需要，而是只对那些一致性是传递的。公理5.1（局部相等公理）假设一阶语言，其中定义了简单等式（CASL中的存在等式(1) 幂等性：xHx=x;(2) 交换性：xHY=yHX;(3) 结合性：xH（y H z）=（x H y）H z。Localequality=lc，由以下等式定义：(1) f（x）=f（x）=f（x）=f（x(2) 对称：x=lcy→ylcx;andd =(3) 局部传递性：def（xHz）→LC（x=yLCy=zLCx= z）。4e e那个 符号=. 表示解释谓词符号“="的函数。这同样适用于其他谓词符号。5 因此，我们可以把Ω-集看作是一个4元组ΩA，e=，def，=0。∧→R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133141H（x=yHLC==地方平等和简单平等。观察到，如果我们假设局部相等公理并引入额外公理：“x "。很好def（xHy）"，局部相等的前提条件总是成立，传递性定律又可以自由地适用。定义5.2[局部集合]局部相等的模型称为局部集合，lcanΩ-setAedwedwi th arelation.. ：A×A→Ω和partia函数H：A×A→A6，使得对所有x，y，z∈A：(1) xHx=x(2) xHy=y Hx;(3) xH（y Hz）=（x Hy） Hz;lc（4）x x=def（x）lc lc（5） x=y =y=x（六） def（xHz）≤Santiago [14，16，15]以这样一种方式定义了一个cHa，即区间上的一致性变成了一个简单的等式。然而，在这些著作中，这个cHa不是布尔代数，因此，这些定义不能在CASL中直接指定。换句话说，对于区间的可定义性和简单相等性，需要一个经典定义在这里，我们表明，我们可以使用经典的cHa{ 0， 1}作为一个估值，使本地平等的实施是立即可能的CASL。6区间布尔局部集在[15]中发现的非布尔局部集，由Bedregal和Santiago [3]推广到局部代数（局部群，局部环等）。我们现在以如下方式基于Ω-集到局部集的规范扩展来构建区间局部相等的布尔版本：命题6.1给定一个Ω-集一赋予与一部分操作H：A×A→A是幂等的、交换的和结合的，函数lc lc. =. ：A×A→ Ω，定义为x=y=def（xHy）定义了一个局部集。证据证据很简单。 局部集合的前三个性质正是““的幂等性、交换性和结合性。最后一LC证明了三个性质：（4）x=x =def（x x）return（x）;lc lc（五）x=y=def（xHy）=def（yHx）=y=x;（6）由于定义def（xHLCz）=x=z，那么，平凡地，局部传递性是满足的。特别地，对于布尔代数{0， 1}，我们有：6欧洲法律委员会值得注意的是，局部集合是一个6元组的集合A，。=.，def，. =.，。 =.，H，因为它是一个扩展e一个Ω-集的ΩA，. =.，def，. =. - 是的y=zx=z）⇒LCLCQ142R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133LC⟨命题6.2设Ω ={0，1}是标准布尔代数，"=”是定义2.2中的通常等式，函数def：（）→ Ω，其中def（[ a，b ]）= 1，对所有[ a，b ] ∈（）。然后，结构，（），=：（）×（）→Ω，是Ω-集。证据简单地说，等式是对称的和传递的。此外，由于它也是自反的，并且对所有A∈（），def（A）= 1，则（A=A）= 1 =def（A）。Q注意，由于def（[a，b]）=1，对于所有[a，b]∈e（），然后是存在强我们使用通常的区间相等符号现在，由于（），=是Ω-集，结构来规范地为区间构建局部相等“=”。此外，为了实现我们的目标，该操作必须捕获一致性，从某种意义上说，（六）“LCB当且仅当A=B所需的操作是区间交，表示为重载，它是部分的，可交换的，结合的和幂等的。因此，所需的局部集被定义为：定义6.3规范区间局部集是结构LC（），=，def，=，∩⟩7使得LC=B=def（A B）。 见命题第6.1条.推论6.4（在CASL中的实现）由于CASL实现了强等式，因此只需在其数库中添加一个带有Moore算法的区间规范，并直接将局部等式定义为：<“x lc y => def（x capy）“。其中“def”是CASL中的原语，“cap”是CASL中区间库的交集运算（详细信息请参见Lopes [ 5 ]）。推论6.5表2中的所有相容性性质，现在都可以用局部等式来表示，从而产生一种称为局部场的数学结构。因为如果A=B，则A<$B∈LC（），它等于A=B= 1。这意味着这结构可以用CASL语言表示，使得能够使用间隔来指定具有实数的系统，就好像它们是具有错误信息的实数一样。上述性质使我们能够将相容区间视为相等的，然而，它们不足以使我们能够从局部方程导出局部方程并进行方程推理。换句话说，我们需要一种局部平等的等式逻辑。为此，我们仍然需要一个同余定律和其他一些公理。这些定律必须作为公理引入CASL Interval 库。下面我们证明区间算术的正确性（见（1））保证了同余公理的可靠性。请注意，由于CASL是一阶语言，因此像全等这样的一般原则不能被一般地陈述即每个算术符号需要一个公理。 为此，7由于存在等式和强等式与通常的区间等式一致，因此区间局部集可以被视为5元组。此外，我们不区分句法的“def”和语义的R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133143K∈∩∈−=∩∈如果这项工作被应用于高阶语言，例如HASCASL [10]，CASL的高阶扩展，理论会更简单。7CASL库7.1同余在等式逻辑中，全等性是一个基本公理，它指出对于规范中的每个运算符号f(7)x1=y1. n=yn→f（x1，.，xn）= f（yi，...，yn）该属性的实例化和适应性为本地平等和四算术运算给出了下面的公理。同余公理lc lc(i) x=y→ −x= −y（k = r-k）;LC111lc11(ii) x=y<$（defx<$defy）→x=y（<$rk）;lc lc lc(iii) x=y<$w=z→x+w=y+z（<$r+）;lc lc lc(iv) x= y w = z → x × w = y × z（r ×）。命题7.1同余公理（Kr-k），（Kr1），（Kr+）和（Kr（三）健全。证据 根据定义，如果X，YLC（），则XlcY- def（XY）.因此，我们建议，X= Y当且仅当XY（）。因此，我们认为，LC(1) 如果X=Y，则X<$Y∈（ ）即 X<$Y=[a，b]∈（ ）. 根据定义，−X={−x∈：x∈X}，−Y={−y∈：y∈Y}和−X<$−Y={−z∈：−z∈ −X<$−z∈ −Y}={−z∈：z∈ X<$z∈Y}={−z∈：z∈X<$Y}={−z∈：z∈[a，b]}=−[a，b];即−X<$−Y∈（），因此−(2) 类似于（r-k）。LCX=Y。LC(3) 如果X=Y且WLC=Z，则X<$Y=[a，b]∈（）且WLC=Z=[c，d]∈（），X + W ={x + w ∈：x ∈ X <$w ∈ W}，Y + Z ={y + z ∈：y ∈ Y <$z∈ Z}.由于X<$Y∈（）和W<$Z∈（），则有k1∈X<$Y和k2∈W<$Z。简单地说，k1∈X，k1∈Y，k2∈W，k2∈Z，因此k1+ k2∈X + W且k1+k2∈Y+Z;X + WY + Z。既然是非空闭区间的交，则X + WY + Z（），根据定义LC表示X+W=Y+Z。(4) 类似于（r ×）。Q更一般地说，我们有：定理7.2若F：（）→（）是表示实函数f：→的正确区间函数，即F具有性质144R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133（1），则满足局部等式的同余。R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133145X1LC证据 设[a，b]=[c，d]，则[a，b]<$[c，d] ∈ （）中选择。 因为F是正确的，所以(1) - 则对所有x∈[a，b]<$[c，d]，f（x）∈F（[a，b]）和f（x）∈F（[c，d]），则F（[a，b]）<$F（[c，d]）∈LC（），因此F（[a，b]）=F（[c，d]）。7.2H-引进与单调性下一个公理负责在演绎中引入交集的定义这个公理非常重要，因为没有它就不可能导出局部等式。（sup-intro）X±U<$Y ±V<$U=V→def（XHY）<$X±V<$Y±U这个公理定义了交集存在的条件，也在演绎中产生了信息X±V和Y±U;这是针对U和V是不同项但意义相同的情况，使我们能够在演绎中需要时使用这个事实。这个公理被称为H-介绍，它的ASCII缩写是命题7.3公理H-介绍是合理的。证据 给定X，U，Y，V∈ （），设X±U，Y±V，U=V，则X<$Y <$联合 因此，X <$Y<$，因此X<$Y∈ （）和 def（X<$Y）=1。以来U = V，则X±V和Y± U。Q下一个公理表达了摩尔算术的单调性。注意“±”是包含顺序“± "的相反顺序。因此，Moore算法的包含算术的单调性（M +）X±Y<$W±Z→X+W±Y+ Z。（M×）X±Y<$W±Z→X×W±Y×Z。（M -）X±Y→ −X±−Y。（M invm）X±Y→1 ±Y;如果0/∈X或0/∈Y。8应用公理CASL的间隔库在Lopes [5]中实现。该库扩展了“Basic/Numbers vs. 0.7”库，其中包含有理数的规范。从这个有理数的具体化中，建立了称为RatPair的笛卡尔乘积。RatPair的一个元素具有[.. ].称为IntervalRat的摩尔区间的集合是RatPair的子集，其中对于所有[x. y] ∈RatPair，x≤y。规范是用CATS（CASL工具集）8开发和检查的（语法和静态语义）。8见http：//www.informatik.uni-bremen.de/co fi/Tools/CATS.htmlQ146R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133下面我们将展示此规范的部分内容（省略，例如，一些运算的定义，公理的名称）：库Intervalversion 0.7从Basic/Numbers version 0.7获取Rat。（x lc y）=>（y lc x）. def（x capz）=>（（x lcy）/\（ylcz）=>（xlc z））spec RatPair = Rat然后%def生成的类型RatPair：：=[. .]（项目1：Rat;项目2：Rat）%地方平等介绍. （xlcy）<=>def（x cap y）（% IntroLc 01%）. （x = y）=>（xlc y）（% IntroLc 02%）一致性%. （x lc y）=>（inva（x）lc inva（y））操作项目1proj2：RatPair ->Rat;：RatPair ->Rat;. （（x lc y）/\（def（invm（x））/\def（invm（y）=>（invm（x）lc invm（y））. （（x lc y）/\（wlc z））=>（（x+ w）lc（y+z））变量a、b、c、d：大鼠. [a.. b]=[c. d]<=>a=c/\b=d %（Interval_Equality）%然后%def.然后%defsort IntervalRat = {a：RatPair. proj 1（a）<=proj 2（a）}则%defops[1. 1]，[0.. 0]：IntervalRat;. （（x lc y）/\（wlc z））=>（（x* w）lc（y*z））%defSup. （（x infw）/\（y inf z）/\（w =z））=>def（x cap y）/\（x inf z）/\（y inf w）%单调性. （（x inf y）/\（winf z））=>（x+ w）inf（y+z）. （（x inf y）/\（winf z））=>（x* w）inf（y*z）. （x inf y）=>（inva（x）inf inva（y））. （x inf y）=>（invm（x）inf invm（y））+inva-*invm/M：IntervalRat * IntervalRat ->IntervalRat，interval，as interval，unit[0.. 0];：IntervalRat-> IntervalRat;：IntervalRat * IntervalRat -> IntervalRat;：IntervalRat*IntervalRat->IntervalRat，interval，as interval，unit [1.. 1];：IntervalRat->？IntervalRat;：IntervalRat * IntervalRat -> IntervalRat;：IntervalRat-> Rat;%（中点）%则%意味着变量x、y、z、w：间隔率%（次分布）. x *（y+z）=（x* y）+（x* z）ifdegen（x）. x *（y+z）包括（x * y）+（x * z）局部域公理. （x+（y+z））lc（（x+y）+z）dist：IntervalRat * IntervalRat -> Rat; %（距离）%。（x *（y*z））lc（（x * y）* z）宽度：IntervalRat-> Rat;%（width）%. （x+y）lc（y+x）abs：IntervalRat-> Rat;%（绝对值）%。（x * y）lc（y * x）然后帽 ：IntervalRat * IntervalRat ->？IntervalRat;%（交叉点）%. （x+inva（x））lcw/w =[0.. 0个字符]. （x * invm（x））lcw/w =[1..第1页]. （x+ w）lcx/w =[0.. 0个字符]普雷兹包括：IntervalRat*IntervalRat;. （x* w）lcx/w =[1.第1页]degenlcinf：IntervalRat;%（$x$是退化的）%：间隔Rat*中间值Rat;%（局部相等）%：间期Rat*间期Rat;%（Inform. 订单）%. （x*（y+z））lc（（x*y）+（x*z））%区间的代数性质. （x+（y+z））=（（x+y）+z）（%Ass+%）. （x*（y*z））=（（x*y）*z）（%Comm+%）变量x、y、w、z：间隔率% 一些定义. defx%每个间隔都已定义. x包括y<=>（proj1（x）>=proj1（y）/\proj2（x）= proj2（y））. degen（x）<=>proj1（x）=proj2（x）. （x inf y）<=>（proj1（x）= proj1（y）/\proj2（y）<=proj2（x））%局部相等公理. （x lc x）<=>defx（% lc %）. （x+y）=（y+x）. （x*y）=（y*x）. （x + w）= x/w=[0.. 0]（%id+%）. （x* w）= x/w =[1..第1页]. （x+inva（x））= w/l（w =[0.. 0] ifdegen（x））（%inv+%）. （x * invm（x））=w/l（w =[1.. 1] 如果退化（x））. （x*（y+z））=（（x*y）+（x*z））如果degen（x）/\degen（y）/\degen（z）端请注意，在“% Local equality introduction“中，“LCx=y下面我们给出方程π+x =π2的解，文[3，4]、[1，2]和X. “pi”任何分别近似π和2的退化区间。 本决议表明，应用局部相等的区间，使我们能够代数操纵他们，因为我们做的实数。在下面的推导中，我们使用了通常的equals替换equals，因为局部等式和其他任何等式一样是一个二元谓词。我们用（eq）（这在CASL中是基本的）来代替通常的equals。我们用（cong）表示强相等的同余（这在CASL中R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133147也是本原的）。我们尽可能地省略公理的实例化，而肯定前件被缩写为“MP”。每一个（req）的出现都来自于每一个区间的可定义性。下面的公理是在正文中介绍的，或者是在148R.H.N. Santiago等人理论计算机科学电子笔记184（2007）133具体化（来自区间理论）。我们使用“− x“而不是inva（x）。 (8)1.pi + x = sqrt{2}- 假设2.Xinf x- 假设3.[3，4] inf pi- 假设4.[1，2] inf sqrt{2}- 假设5.[3，4]+ Xlc[1，2]- 假设6.[3，4]+X inf pi+ x-（MP：M+，2，3）7.- [3，4] inf-π-（MP：M-，3）8.pi= pi- Refl9.pi = pi =>-pi =-pi-Congr.大鼠10.-pi=-pi-（MP： 8，9）11.-[3，4]=-[3，4]-参考12.- [3，4] lc-[3，4]-（MP：11，IntroLc02）13. -[3，4] lc -[3，4]/\[3，4]+ Xlc [1，2]- （导言12、5）14.-[3，4]+（[3，4]+ X）LC-[3，4]+[1，2]- （MP：13，Bullerr+）15. (-[3，4]+[3，4]）+ Xlc-[3，4]+[1，2]- （eq：14，Ass+）16.X+（（-[3，4]）+[3，4]）lc -[3，4]+[1，2]- （eq：15，Comm+）17. X+（[3，4]+（-[3，4]））lc -[3，4]+[1，2]- （eq：16，Comm+）18. -[3，4]+（[3，4]+ X）inf -pi+（pi+ x）-（MP：7、6、M+）19. -pi+（pi+ x）=-pi+ sqrt{2}- （cong：10，1）20. （-pi+pi）+x=-pi+sqrt{2}（eq：Ass+，19）21. （pi+（-pi））+x=-pi+sqrt{2}（等式：Comm+，20）22. 0+x=-pi + sqrt{2}-（等式：inv+，21）23. x + 0 =-pi+ sqrt{2}-（等式： com+，22）24.x =-pi+ sqrt{2}-（等式：id+， 23）25. -[3，4] inf-pi/\ [1，2] inf sqrt{2}- （Intro/\： 7，4）26. -[3，4]+[1，2] inf - pi+ sqrt{2} -（MP：25，M+）27. XINFx/\-[3，4]+[1，2] inf -pi+ sqrt{2}- （Intro/\： 2，26）28. X INFx/\-[3，4]+[1，2] inf -pi+sqrt{2}/\x =-pi+sqrt{2}-（简介\：27，24）29. def（Xcap -[3，4]+[1，2]）/\Xinf -pi+ sqrt{2}/\-[3，4]+[1，2] infx-（MP：sup-intro，28）30. def（X cap-[3，4]+[1，2]）-（Elim/29）31. XLC-[3，4]+[1，2]-（MP：30，无菌）32. Xlc[-4+1，-3+2]-应用+和-33. Xlc [-3，-1]-整数库9一个简单的应用程序工程中开发的一些系统需要数据和公差的处理即，这些系统需要处理具有已知精度的非精确量的能力，并且必须能够产生具有已知精度的数字的输出。在下文中，我们提出了一个简单的系统。它计算并联连接的两个电阻器R1和R2的电阻Rp众所周知的公式是（九）Rp=11 1+R1R2这些电阻器的电阻值通常是已知的，并由制造商给出例如，电阻器为6。80欧姆，10%的公差，保证电阻器的电阻值在6. 80± 0。68，即 它位于6之间。八十比零68= 6。12和6。80+ 0。68= 7。48欧姆-或者换句话说，电阻值属于区间[6. 十二，七。48]。因此，当阻力为6时。80欧姆，10%的公差与另一个并联，4。7欧姆和5%的公差，电阻的组合必须在2。58欧姆和2. 97欧姆。因为对于电阻器R1= 6。80 ± 0。68，R2= 4。70 ± 0。23，工程师计算的结果属于区间[2。58，2。97]，其相应公差的中点等于2。77 ± 0。20.我们的意思是，这类系统考虑的数据是区间，相应的算法将实现（9）的区间版本为实数设计的等式（9）可以扩展到摩尔算术（即，扩展到以下区间R.H.N. Sa