图形化关系推理形式化方法：B/Z归纳与coinduction在关系系统开发中的应用

理论计算机科学电子札记127（2005）87-105www.elsevier.com/locate/entcs关系系统开发中的图追踪迈克尔·埃伯特1Georg Struth2计算机科学系德国慕尼黑联邦武装部队大学摘要我们提出了图形化的关系推理的形式化方法，如B或Z，特别是归纳和coinduction。这些类似于范畴论中的功能图，并受到重写理论的启发图被赋予了一个简单的代数语义，在表达能力和算法能力之间实现了一个方便的平衡。这使得该方法特别适合于机械化和自动化。它的实用性的视觉推理说明了各种例子。关键词：图，半交换，形式语义，关系系统开发，B，Z，归纳，余归纳，迭代代数。1介绍在数学科学中，用函数作图是一种常见的做法。函数f：A→B与从源A到目标B的箭头f相关联。 函数的组合，关于源和靶或功能的域和共域与箭头的并列相关联函数之间的方程f=gh与交换图相关联，其中从给定源对于一个给定的目标是相等的。关于函数的等式推理和图解推理是一一对应的。众所周知，范畴论提供了这种风格的抽象基础。 它成功地用于1电子邮件：ebert@informatik.unibw-muenchen.de2电子邮件：struth@informatik.unibw-muenchen.de1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.08.04988M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）87计算机科学的许多不同领域，其中包括软件系统的规范和分析。然而，对于许多软件分析任务来说，功能方法的限制太多了。首先，规范通常是不确定的，因此允许元素的一对多关联程序的确定性通常是在精化过程中建立的。非确定性甚至是并发或反应系统的基本特征。其次，函数对于谓词转换器或分析形式主义（如动态或时态逻辑或μ演算）的语义建模因此，希望从函数推广到关系。事实上，关系构成了软件开发中B [3]或Z [18]等形式化方法的支柱。但是如何将关系推理可视化呢？我们建立在重写理论的经验教训（c.f. [4]）和寓言理论[11]，用于开发半交换图的简单方便的代数语义。这些都是不平等的推理关系什么交换图是方程推理的功能。我们的基本代数是Kleene代数[14]。我们认为，这是非常方便的建模软件系统中的控制流程。特别是，这种语义产生了简单的基于定点的规则和相关的图表，用于归纳和共归纳推理的有趣片段。这种方法很好地平衡了图的表达能力和算法能力，特别是决策过程。一个特别的好处是，正则和欧米茄正则恒等式及其相关的图表可以自由地用于diagram追逐。这种简单性与以前需要大量机器的方法形成对比然而，我们的方法的力量不仅在于通过健全和完整的图解演算来可视化代数公理，而且还在于用于变换和（解）构成图的直观和强大的派生规则我们介绍的规则，捕捉重写理论的典型的非正式的图解风格。然而，我们在半交换的一般设置中的考虑增加了它们对使用B或Z等方法的关系软件开发的适用性。将图表技术从重写转移到软件工程的想法可能是新颖的。重写理论和并发控制的几个例子支持这种方法的有用性关系图追踪在重写中的一般优点是毫无疑问的：它是这一领域的标准推理方式。图表显示了证明的本质，同时隐藏了无聊的技术细节。与逻辑或代数的形式严格证明相比，图证明是非形式严格的。我们的例子表明，目前的方法统一了这两种M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）8789一个简单而方便的形式主义。在相应的形式化方法中，证明工程师可能首先使用图表绘制证明，然后使用我们导出的规则逐步完善它。潜在的代数语义为图表论证的简单机械化验证铺平了道路这种方法是开放的，因为用户可以很容易地定义和验证进一步的图规则。在本文中，我们试图非正式地激发我们的图解演算背后的主要思想，并通过例子来说明它们。关于Kleene代数及其相关理论的理论结果可以在文献[14，6，9]中找到。演算的实现和集成到一个正式的方法是留给未来的工作。本文的其余部分组织如下：第2节展示了如何重写图可以用于建模并发系统和过程的有意义的属性。第3节提出了一个半交换关系图的代数语义。第四节给出了图的变换和保持律。第5节和第6节介绍图解归纳法的技巧和例子。第7节给出了共归纳的图表和技巧。第8节和第9节进一步讨论了结果，得出结论，并提出了一些未来的工作。2图的风格推理让我们首先回忆一下在重写理论中图解是如何产生的。设R是某个集合A上的二元关系。我们写a→Rb而不是（a，b）∈R，并可视化·→R·作为整个关系R的基本图解构建块。关系R和S的组合通过y·→R·→S·来可视化d。 当a→Rc且c→Sb时，对某个c∈A，则称m b e r t h a t a → R <$Sb。最后，包含R∈R在S中，可以用图来R··S如果RS是有效的，那么我们说这个图是半交换的。下面的例子说明了这个概念的普遍性和适用性。例2.1考虑下面的半交换图。90M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）87··R··UR··U··R··RT S它专注于各种有趣的属性，其中包括以下内容。(i) 设T=S。然后我们说US-模拟R.模拟是并发理论和进程代数中根据初等集合论，这种模拟性质在以下情况下成立：对所有的x1，x2，x3∈A，如果x1→Rx2和x2→Sx3成立，则存在某个y∈A，使得x1→Ty和y→Ux3。因此，在半交换图中，实线的路径对应于万有量化，虚线存在主义量化。这种符号在重写理论中也是标准的。我们将介绍几种应用。作为特殊情况，当T是一个映射时，那么图说T是一个同态。(ii) 设U=R。然后我们说S在R上半交换。在并发系统中，这表示S的执行总是可以优先于R的执行;动作S之后的R-动作序列总是可以被动作R之后的S-动作序列替换。下面我们将使用几个较弱的半对易概念(iii) 设R=S=T=U=V，其中运算和表示递归传递闭包和转换.我们通过反转箭头来形象化对话。然后，该图表示V的连续性，即所有发散。v-paths最终会加入。这是重写和函数式编程的基本概念。它用于保证计算过程的唯一解的存在性。(iv) 设T=S，U=R。然后我们说这个图是对易的，我们可以用实线代替虚线。两个关系R和S的交换，即R<$S=S<$R可以用来表示它们的独立执行。这对于分析并发系统很有意思例如，用于部分降阶[1]，用于表示物理系统中测量的独立性，或者用于对程序中变量分配的独立性进行建模。与这些概念相对应的图是S ssSVVSS··R··R·V∗···VM. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）87913半交换图现在我们从集合论关系抽象到用一些合适的代数的元素标记的箭头，并逐步激发我们的标记代数的公理。我们将图建模为特殊的有向图。考虑任何有向无环图G，它有一个源和一个汇，有两种边（或箭头）-实线和虚线-并且箭头由某个标号代数A的元素标号。链接是从源到接收器的路径，只包含一种箭头。如果从源到汇的所有路径都是链路，则G是一个图我们通过路径等价定义图D的可换性。因此，我们需要一个乘法的标签（由并列表示）的操作。对于D中的每一条路π，我们定义l（π），与路π相关联的标号，作为将箭头与它们的标号和空路与1相关联的映射的同态扩张，并且使得l（πρ）=l（π）l（ρ）。这里，路径的并置表示路径组成。显然，l是一个双射，如果标签的乘法是结合的，并且l映射到相应的等价类。 我们将实施这一要求。 对于D中的所有π1和π2，关系π1<$Aπ2定义为l（π1）=l（π2）是一个同余（关于路径合成），我们称之为路径同余。我们说D是可交换的，如果所有的链路都是（路径-）等价的。我们写C（π1，.，π n）如果具有链接π1，.，π n通勤。因此C（π1，.，π n）惠π i<$Aπ j，对所有1 ≤i，j≤ n.例3.1下图为上下文。AB··a· b在我们预期的应用中，箭头对应于动作;图中有意义的路径概念预先假定动作的组合是关联的。关系的构成，当然是。拥有保存或摧毁一切的箭头也很方便。它们对应于动作skip和abort，或者对应于恒等式和空关系。这些动作出现在许多形式主义中，其中包括谓词Transformer演算、命题动态逻辑和进程代数。我们引入标签1和0，并要求交换92M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）87一一00········1· aa·10·aa·0这将标记代数变成一个单位为1，元素为0的幺半群，满足湮灭定律0a =0 =a 0。一些应用程序建议删除0= 0。当a总是非终止的，人们可能希望ab=a对所有b，特别是对b= 0;一个连续的。[21]这是一个更深层次的 讨论。将并发系统建模为动作选择的有限次或无限次迭代是很方便的因此，我们添加一个运算+的加法到我们的标号代数，它是结合的，交换的和幂等的（x+x=x）。在关系层次上，加法是集并。从关系中抽象出来，我们要求0是加法的单位，乘法从左到右分布在加法上。下面考虑迭代的操作综上所 述 ， 我们要求代数a（A，+，·，0，1）是幂等半环.从形式上讲，这意味着，• （A，+，0）是一个交换幂等幺半群，即半格，• （A，·，1）是m，• 乘法从左到右分布在加法• 零是左和右零化子。半交换图的定义现在很简单了。每个幂等半环A都有一个自然序，定义为a≤bi∈a +b=b，对所有a，b∈A。它是唯一一个包含最少元素0的序，并且加法和乘法都是保序的。 图中的路径π1和π2我们定义π1≤π2i ∈l（π1）≤l（π2）。 根据乘法的保序性，≤是一个路预同余。我们说D是半交换的，如果D中的每个实链环都小于D中的每个虚链环。当然，图的半对易性可以用对 易性来定义，亦然我们写S（π1，.，π m; ρ1，.，ρ n）来表示具有实链接π1，.，π m和虚线链路ρ1，..，ρ n半通勤。因此，我们建议，S （π1， .，π m; ρ1，.， ρ n）惠π i≤ρ j ，对于所有1≤i≤m 和1≤j≤n。根据自然序，幂等半环允许关于前半环的推理。gram和系统细化。a≤b保持i ∈a是b的精化。这是因为在所有上下文中，a总是可以用来代替b由于l是图到标号代数的同态，并且半交换是根据不等式的有效性通过这种解释定义的，标号代数为半交换图提供了语义。因为l实际上是双射的（直到乘法的结合性M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）8793nn半交换图是代数的可视化此外，通过这种简单的构造，很明显，从幂等半环的公理可以建立的半交换图对于这种语义是可靠的和完备的。4转换与保存图与代数不等式之间简单的一一对应关系使我们能够直接用半交换图来表示标号代数的定理。特别地，幂等半环理论中的有效拟恒等式，即以下形式的公式a1≤b1···an≤b na0 ≤b0，立即转化为半对易的守恒定律：S（l−1（a1）; l−1（b1））<$··<$S（l−1（a ）; l−1（b ））S（l−1（a0）;l−1（b0））反之亦然。这个定律说，只要前件中的图是半可换的，那么后件也是。因此，等式逻辑的任何证明系统都可以作为图的证明系统。然而，经验表明，人类的推理与幂等半环本质上是不平等的。因此，使用一种逻辑来进行有序和预同余的推理更为方便。[22]这是一个系统。因此，推理半交换图可以很容易地机械化，并集成到一个正式的方法。由于幂等元半环的方程理论是可判定的，所以给定的图是否半交换是可判定的。然而，图之间的蕴涵可能是不可判定的;这是半群的一致字问题的不可判定性的结果[7]。因此，图解推理的大部分可以很容易地自动化;其余部分可能需要人工交互。因此，标号代数的算法能力对于检查图解推理的有效性是非常有帮助的。然而，一个普通的通用形式证明系统是不够的图追逐。正如范畴论所表明的那样，真正的图解推理应该基于导出的变换规则，这些规则在拓扑上是直观的和自然的，并且保持了相关的性质，例如交换或半交换。我们将介绍两种这样的规则：替换图中路径的规则我们首先介绍分裂和denominating规则。分裂规则允许我们在交换图和半交换图之间进行转换。94M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）87Ba一··⇔··bB一∧··B显然，它是有效的，因为a=bi <$a≤b且b≤a。当从左到右使用时，denominator规则产生一个更紧凑的图表示在相反的方向上，它引入了进一步的规范形式图，它正好由两个链接组成.a a··⇔··C cB∧··C通过交换实线和虚线可以得到类似的规则。我们的第二个派生规则是案例分析规则a+B··C一⇔··CB∧··C它是有效的，因为a+b≤ci ∈a≤c，b≤c对某个幂等半环的所有元素a，b，c使用分配性，我们可以进一步将所有图分解为一个标准形式，其中所有实线箭头都标记为单个字母虚线没有相应的定律。由于这种情况的分析，我们不介绍任何图形法律的加在虚线的上下文，但处理加法完全由性质的标签代数。 人们可以很容易地推导出进一步的图解证明规则，例如a≤b→a≤b+c或a≤a+b。我们的第三组派生规则转换图中的路径。它们基于乘法的保序性，即导出规则π1≤π2<$ρπ1≤ρπ2，π1≤π2<$π1ρ≤ π2ρ。关于半对易的路式π1，π2和ρS（π1;π2）<$S（ρπ1;ρπ2），S（π1; π2）<$S（π1ρ; π2ρ）。虽然这些保序性规则是代数学上的基本规则，但它们对于图解演算来说并不自然。现在我们给出两个替换半交换图中边的基本规则。第一个是M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）8795·· c··· 一X···Bx 阿克斯b/第二条规则可以通过交换实线和虚线来获得。利用这些规则和分裂规则，我们可以推导出另一个规则，用于交换具有相同形状且所有线都是实线的图。 对于可交换图和半可交换图的组合，存在可以使用分裂规则从基本规则导出为了简洁起见，我们使用路径表达式来表示它们。π1ρ1π2<$π3<$ρ2≤ρ1<$π1ρ2π2≤π3 ，π1<$π2ρ1π3<$ρ2≤ρ 1 <$π 1≤π2ρ2π3，π1ρ1π2≤π3<$ρ1<$ρ2<$π2≤π3，π1≤π2ρ1π3<$ρ1<$ρ 2 <$π1≤π2ρ2π3。将其转化为保护法也很简单。例如，第二个转化规则转化为保存法，C（π1，π2ρ1π3）<$S（ρ2; ρ1）<$S（π1; π2ρ2π3）.我们的第四组派生图规则处理图的组成同样，这些规则是基于乘法的保序性，但现在上下文在两个先行词中都使用。同样，半交换图有两个基本的组成规则。第一个是一··cx··B 布拉奇D一··B··D第二条规则可以通过替换实线和虚线再次获得。对易图的相应规则直接来自半对易图和分裂规则。进一步导出的规则再次处理交换和半交换的组合。他们是π1<$π3ρ$>ρπ2≤π4<$π1π2≤π3π4，π1≤ π3ρ $>ρπ2<$π4<$π1π2≤π3π4，π1ρ<$π3<$π2≤ρπ4<$π1π2≤ π3π4 ， π1ρ ≤ π3 <$π 2<$ρπ4<$π1π2≤ π3π4。所有这些导出的图规则的合理性可以很容易地显示与帮助··C·· 一96M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）87C一·c⇒∗·标签代数。此外，所有规则对应于交换和半交换的保持律。我们导出的变换和合成规则形式化了重写理论中图追逐的本质，但推广到半交换的设置，并具有潜在的抽象代数语义。对人类来说，图追踪通常比执行详细的基本代数操作方便得多（除了幂等半环的宗派主义者）。本方法的简单形式语义产生了这些对立的巧合。5归纳的图解技巧用图表进行推理常常是归纳的。对程序和系统的推理通常需要某种形式的迭代或递归。现在我们将考虑由有限迭代产生的一种限制形式的归纳法。虽然严格地说，它的表达能力不如一般递归的归纳法，但它仍然捕捉到了一些有趣的行为。在[12]中已经提出了一种以前的方法来进行几何图的归纳推理。然而，这种方法中使用的目标和技术与我们的完全不同。为了在我们的标号代数中模拟归纳，我们将标号代数从幂等半环扩展到Kleene代数[14]。从形式上讲，这是一个结构-真（K，ε），使得K是幂等半环，且星ε是一元的由星展开定律和星感应定律定义的运算1+aa≤a，b+ac≤cab≤c，b+ca≤cba≤c，对所有的a，b，c∈K.星展开定律和第一星归纳定律对应于图解表达式a·aa·b·a··c·1B星感应第二定律的图解是通过颠倒箭头得到的。或者，也可以使用归纳法则ac≤c<$a<$c≤c和ca≤c<$a<$c≤c让我们简要地讨论一下这些法律。 展开定律说，A或者什么也不做或者执行A步骤，然后继续迭代。归纳法意味着（通过设置b= 1）a是具有该性质的最小元素。由此可知，a是a的自反传递闭包，自反性意味着1≤a，传递性意味着aa≤a。 也是及物动词M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）8797一个一个一个一个小∗闭包运算符+可以很容易地定义为a+=aa，其中a=1+a+。在操作上，星感应定律是星消去定律。我们将看到下面的例子。对Kleene代数的扩展保留了图追踪的良好算法性质。Kleene代数的方程理论仍然可以使用有限自动机和Kleene代数表达式与正则表达式之间的对应来判定[14]。因此，人们可以自由地使用众所周知的正则恒等式和相关的正则图。实例是1a····a·a····一一个人·一个人 ·最后，关系的自反传递闭包满足星形展开和归纳定律。更一般地说，在并、关系复合和自反传递闭包下的集合论关系形成了一个Kleene代数，我们称之为关系模型。6归纳示例现在我们给出几个用图表进行归纳推理的例子首先，我们展示了一个双星展开定律，它是从第一个展开定律通过反向箭头得出的：一个一个一个··1证明是下面的图表追逐。正如定理证明中常见的那样，我们从结论向后移动到假设。首先，我们使用Denmark规则。这就产生了图aa阿吉亚····1第一个图直接从Kleene代数的Denmark规则和星展开定律得出。对于第二个图，我们的推理如下。98M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）87··一··B·a∗··· b·····cbc·1·····cb··C c··（a+b）一个人··b∗···Bba·aa拉瓜一个·一个......a a·一个人 ·隐含链的最后一步（也是我们向后证明的第一步）使用星感应定律作为星消去规则。剩下的一步是通过denominate，并产生两个新的目标。第一个目标是从星形展开图和展开图中直接得出的。第二个目标是我们以前的一个常规图，我们不再进一步分析。Kleene代数中的基本证明可以很容易地恢复。整个目标也可以通过正则表达式的决策过程有效地处理我们的第二个例子考虑了一个模拟属性，作为一个派生规则，它在程序转换、精化和并发理论的许多应用中都很有用ccc其证明如下。b ca·∗拉克什茨babB··1C第一个图可视化了恒星展开定律。第一步使用等渗性。第二步使用假设和单位消去法。 第三步使用星感应。我们的模拟概念与过程论的模拟概念是一致的。 对于Kleene代数K和a，b，s∈K，我们说bs-模拟a如果≤sb.与数据细化有一个有趣的联系，在[21]中考虑。第三个例子是分离定理。它规定了将并发系统（a + b）的动作作为原子单位的条件。考虑财产··一份优惠bM. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）8799·····一个人·····一个人··∗Bb这是Church-Rosser定理的一个变体。 见[19]的一个广泛的代数处理这个例子。 证明中最有趣的部分是证明ba（a+b）≤a：B·b·∗ ∗ ∗∗babb b（a+b）··⇒··⇒b⇒ ⇒··一个b/一个a·b第一个图使用了正则恒等式bb≤b和自反性。第一步使用星感应。第二步使用等渗性。 第三步使用假设和星形展开来生成新的图。第四步使用开始归纳和案例分析。再一次，证明应该向后阅读。 将b设为a的逆，从重写理论 中 恢 复 了 Church-Rosser 定 理 的 标 准 教 科 书 证 明 。 对 应 于ba<$b<$+aa<$b<$≤a<$b<$的图产生诱导步骤。在[19]中已经表明，更多的抽象重写定理可以在Kleene代数中得到证明，其中包括λ演算中Church-Rosser定理的两个标准证明的抽象部分。这包括Barendregt带引理，Hindley-Rosen交换引理和Hindley-Rosen交换并引理。在所有情况下，标准的语法论证都可以立即转换成代数，反之亦然，并根据我们的简单语义进行验证。在此之前，Nipkow已经在ISABELLE证明检查器中形式化了一个基于集合论的图的概念[17]。他的方法使用了更多的技术机器。7共归纳：图表与技巧Kleene代数可以通过一个算子进行（严格）无限次迭代来扩展。一个ω-代数[6]是一个结构（K，ω），使得K是一个Kleene代数，并且ω满足ω展开律和ω余归纳律aω≤aaω，c≤b+ac <$c≤aω+a<$b，对所有的a，b，c∈K.翻译成图表是显而易见的。同样，具有无限迭代的Kleene代数的关系模型是ω-代数，ω运算相对于自然序是保序的。与Kleene代数不同，ω-代数允许我们表达迭代的终止：它可以被编码为不存在无限迭代，即ω= 0。文[6]中指出ω-代数的有效恒等式就是ω-正则表达式之间的有效恒等式。 因此，我们自由地使用众所周知∗100M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）87···· b······B+aω-正则恒等式及其证明中的相关图我们将在他们出现的时候提到他们。现在我们给出两个共归纳图解推理的例子在前一节中，我们已经给出了一个基于半对易条件的分离定理。如果没有这个条件，我们至少得到以下分离性质[20]：（a + b）= ab+ ab+a（a + b）。它将一个任意序列的动作a和b分成我们的第一个例子比较了两个不同的条件用于分离动作。第一个是半对易条件b;第二个是准对易条件ba≤a（a+b）。利用我们前面例子中的模拟律，很容易证明准对易等价于b<$a≤a（a+b）<$。也很容易证明半对易蕴涵准对易。对于相反的含义，需要终止条件aω≤0。因此，我们的第一个例子是表明a的拟对易和终止蕴涵半对易。用图表表示如下：aω··∧·b·baaa+a0··∗（a+b）现在我们给出一个半形式的图解论证，它可以在以后被转化为ω-代数的形式证明。因此，让我们假设前件成立，但后件不成立，因此特别是b+a/≤0。然后，从上面的好序列和坏序列的分离以及集合论可以得出，B+一a+（a+b）重复这一论点产生了一个带有无限a链的雅各∗M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）87101···B+一···B+a···B+a·B+一 （一个·+b）Baa+（a+b）a+（a+b）注意这个雅克布阶梯不是正式意义上的半交换图。虚线表示它更确切地表示通过迭代逐步构造的半交换图形式上，这个阶梯的构造对应于直到保序性为止的Ω展开定律在图中的应用+（a+b）····a+·b+ ·a（a+b）··∗（a+b）这种无限次迭代是通过应用欧米茄共归纳定律来正式捕获的。它产生半交换图a+ω··∗现在，通过a+ω=aω的omega正则图，假设aω≤0和我们在半交换图中替换边的基本规则，我们可以用另一条虚线替换虚线，标记为0.通过类似的论证，使用1≤a的正则图和我们的单元图，我们可以用另一个标记为B+A。由此产生的图表表达了一个矛盾。因此，b<$a≤a+b<$。这种直观的论证需要超越Ω代数的集合论推理，因为在集合论中对好序列和坏序列的单独考虑是有效的在[20]中给出了Ω代数中的一个非常相似的证明。在那里，一个上下文表示良好的序列进行了证明。然而，这种推理方式不太适用于图表，因为出现在ω共归纳规则右侧的和不允许模化处理。这进一步强调了将我们的图解方法整合到102M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）87一种基于集合的程序开发的形式化方法。我们的第二个例子表明，如果a在b上准交换，则a的终止蕴涵b的终止。在这个例子中，我们再次展示了如何从半形式图中恢复代数证明。就像上次考试一样-我们使用虚线和箭头来表示一系列生长图的迭代构造。为了证明，通过反证法假设一个无限的b-链。然后，通过前面的例子，如果a终止且a在b上准交换，则每个b→a-序列都可以变换为a+b→ a-链。因此，b产生一个无穷a序列，一个矛盾。为了恢复半可换图，内部虚线箭头应该被丢弃，并且最后的虚线箭头应该被虚线箭头替换。 因此，在某种意义上，虚线箭头记住了迭代构造半交换图的先前步骤。下面的代数证明是验证二分法证明的直接翻译。首先，通过我们前面的例子，我们可以假设半对易而不是准对易，因为a终止。因此（b<$a）ω= b<$a（b<$a）ω≤ a+b<$（b<$a）ω= a+（b<$a）ω。第 一 步 使 用 Omega 展 开 。 第 二 步 是 假 设 。 第 三 步 使 用 ω 正 则 恒 等 式b<$（b<$a）ω=（b<$a）ω。现在，我们不再使用omega unfold迭代这个构造（我们没有显式地显示在图中），我们通过ω余诱导使无限链显式化，得到（b<$a）ω≤a+ω。然后断言（b<$a）ω≤0由Ω正则恒等式a+ω=aω和终止假设aω≤0跟随。我们把全部的图解式发展留给读者。在[20]中，使用在对[5]中关于动作序列终止的模性定理的代数证明中：a和b终止i，a+b终止且a在b上拟交换。这证明了我们的图解技术在终止分析中的适用性。8讨论我们的考虑表明，我们的代数方法图追逐是非常适合集成到一个正式的方法。它很好地平衡了表达-·b∗······一b一b一bbb·a+·a+·a+·M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）87103和算法能力。与此同时，底层代数已经在各种交互式定理证明器中实现[19，21，13]，Kleene代数的专用交互式定理证明器[2]已经开发，并且正在进行此类证明器中的决策过程的集成[8]。使用这种工具的证明通常从目标到假设进行回溯。例如，星归纳法则被用作星消去法则。因此，在交互式定理证明器中实现我们导出的图转换规则的语义是很简单的。向后使用我们的转换规则支持分解推理。图是迭代缩小的：实线箭头的向后替换产生更大的边;虚线箭头的向后替换产生相对于自然排序的更小的边这与不等式推理的通常风格相对应因此，在现阶段，主要任务是设计和实现一个图形前端，允许显式操作图表，支持用户定义的转换规则，并增强代数和图解推理之间的转换。一个主要的问题是证据的呈现。乍一看，通过以拖放方式应用转换规则，在屏幕上成功地修改图似乎是最自然的。这种工具的具体实现是开放的。我们的方法是由关系推理的动机。在基于集合的程序开发方法中，这通常是首选的抽象级别因此，集成到像Z或B这样的方法中似乎非常有趣。9结论我们已经提出了关系式推理与形式语义的基础上的Kleene代数的变种图我们已经证明了一系列的并发和重写理论，包括归纳和共归纳推理的例子的方法的有用性。我们认为这种方法特别适合于机械化和自动化。大部分的推理使用可以由自动机决定的正则和欧米茄正则恒等式我们设想进一步开展以下工作。首先，我们的技术应该集成到一个图形界面，允许拖放图追逐结合代数计算。然后，通过实现图的语义，将该接口包含到正式方法中这种将重写风格的图技术集成到软件工程方法（如B或Z）中的新方法可能有助于增加它们的舒适度。其次，Kleene代数的其他变体，例如精化代数[21]，懒惰Kleene代数[16]和类型Kleene代数应该被认为是一个se-104M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）87关于完全正确性的图解推理方法。第三，该方法应推广到Kozen这将支持通过关于部分正确性的图和诸如动态或时态逻辑的形式主义进行推理。第四，考虑图的一般化形式似乎很有趣，例如有几个源和汇的图，以及只有部分交换或半交换的图。最后，本文中开发的技术应在算法、程序和协议的分析和开发中进一步测试。致谢：作者要感谢匿名裁判和VLFM'04的参与者引用[1] Abdulla，P. A.，B. Jonsson，M. Kindahl和D. Peled，A general approach to partial orderreductions in symbolic verification，A. J.Hu和M. Y. Vardi，编辑，计算机辅助验证，第10届国际会议，CAV379-390.[2] Aboul-Hosn，K.和D.Kozen，KAT-ML：一个用于Kleene代数的交互式定理证明器，在：B。Konev 和 R.Schmidt ， editors ， 4th International Workshop on the ImplementationofLogics，Technical Report ULCS-03-018，University of Liverpool，2003，pp. 2比12[3] Abrial，J.- R.，“The B-Book,” Cambridge University Press,[4] Baader，F. 和T. Nipkow，“Ter m R e wri t in g and A l l T h at t，“C am b r ig d e UniversityPress，1998.[5] 巴赫迈尔湖和N. 德肖维茨，《换向、变换和终止》，载于：J.H. Siekmann，编辑，第8届国际自动演绎会议，LNCS230（1986），pp. 五比二十[6] Cohen，E.，分离和还原，在：R. Backhouse和J.N. Oliveira，editors，Proc. ofMathematics ofProgram Construction，5th International Conference，MPC 2000，LNCS 1837（2000），pp. 45比59[7] 戴维斯，M.，[8] Desharnais，J.（2004），personal communication.[9] 这 是 我 的 ， J 。 ， B.M ？ollerandG.Struth ， Kleenealgebrawithdomain ，ACMTransactionsonComputational Logic（2004），to appear.[10] 这是真的J ，B. M？ollerandG. Struth，TerminationofmodalKlenealgebra，in：J. Mit c hell，editor，IFIP-TCS 2004（2004），to appear.[11] Freyd，P. 和A. Scedrov，“Ca t e gories，A llegories，“N or t h - H olla n d，1990.[12] Jam n ik，M. ，“用D i agrams进行的数学计算：从逻辑到逻辑“，C S L I出版社，2001年。[13] K ahl， W. ， Calculationrelation-algebraic profsinIsabelle/Isar， in ： R.Berghammer，B.Müoller 和 G. Struth， 编 辑 ， 计算机科学 中的关 系 和 Kleene-Algebra 方 法 ， LNCS 3051（2004），pp. 178比190[14] Kozen，D.，Kleene代数和正则事件代数的完备性定理，信息与计算110（1994），pp. 366-390.M. Ebert，G.Struth/Electronic Notes in Theoretical Computer Science 127（2005）87105[15] Kozen，D.，Kleene algebra with tests，Trans. Programming Languages and Systems19（1997），pp. 427-443[16] 莫勒湾，LazyKlenealgebra，in：D. 王志文，王志文，等.电力系统的结构与性能分析.北京：中国电力出版社，2004.[17] Nipkow，T.，More Church-Rosser proofs（in Isabelle/HOL），J.自动推理26（2001），pp.51比66[18] Spivey，J. M. ，“Under erst and in g Z，“C am brig de e University Press，1988.[19] Struth，G.，在Kleene代数中计算Church-Rosser证明，在：H。de Swart，editor，RelationalMethods in Computer Science，6th International Conference，LNCS2561（2002），pp.276-290。[20] Struth，G.，Abstract abstract rewriting，Journal of Logic and Algebraic Programming（2004）.[21] 我们走吧，J。，FromKleenealgebratorefinementalgebra，in：E. A. 我是一个很好的朋友。Müoller ， editors ， MathematicsofProgramConstruction ： 6thInternationalConference，MPC 2002，LNCS 2386（2002），pp. 233-263。[22] Wec h ler，W. ，“Universa l A lge b r a for C om p ut e r S cie n t i s t s，“S pringer，1992.