行为和共归纳重写：理论计算机科学电子笔记36

理论计算机科学电子笔记36（2000）网址：http://www.elsevier.nl/locate/entcs/volume36.html22页行为和共归纳重写（邀请演讲）1JosephGoguen，KaiLin和GrigoreRoRangsu计算机科学工程加州大学圣地亚哥分校La Jolla，CA 92093，USA电子邮件：{goguen，klin，grosu}@ cs.ucsd.edu摘要行为重写不同于标准重写，因为它考虑了行为逻辑的较弱推理规则，但它与标准重写有很多共同之处，包括终止和连续等概念。我们描述了一个高效的实现行为重写，使用标准的重写。循环共归纳重写结合了行为重写和循环共归纳，为行为性质提供了一种令人惊讶的强大证明方法;它在BOBJ系统中实现，在我们的示例中使用。其中包括几个惰性函数流程序等价物和一个行为细化。1介绍行为规范（Behavioral Specification）是模型（实现）只能在逻辑上满足规范的领域;它还支持无限数据结构、行为细化和共归纳证明方法。行为规范区分可见类和隐藏类，在实验的不可否认性意义上，平等对可见类是严格的，行为行为方程演绎现在已经被很好地理解了，行为重写[6，20]对于行为演绎就像标准重写对于标准方程演绎一样，是一种简单但有用的证明方法。循环共归纳重写是一种将行为重写与循环共归纳相结合的证明行为等式的算法[22，14];它还通过允许在证明中使用共归纳假设来加强与归纳的对偶性。它在实践中是惊人的强大，即使没有这样的算法可以完成[3]。我们还讨论了多余基的存在性，以及系统的并发连接。1本文中报告的研究部分得到了国家科学基金会资助CCR-9901002的支持，并得到了日本信息促进机构（IPA）的CafeOBJ项目的支持，作为其高级软件技术计划的一部分2000年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。GOGUEN，LIN，ROSU2BΣ空间限制迫使我们省略所有的证明和许多定义，并假设读者已经熟悉代数规范和定理证明（例如，[11])，特别是许多有序代数和术语重写;还需要熟悉OBJ [15]。BOBJ系统实现了行为重写、循环共归纳重写、自动共基生成和并发连接。我们在示例中使用它，其中包括流的几个等价物，例如可能在懒惰函数式编程中出现的，通过指向数组的指针对堆栈进行行为细化，以及正则表达式的等价性。2行为规范与推理我们首先回顾我们当前的隐代数的基础，它放弃了[8]中原始公式的所有一个隐藏的签名是一个有序的签名，它的排序分为可见的V和隐藏的H。一个模型是一个代数。模型中的可见排序的元素称为数据，而隐藏排序的元素称为状态。 行为规范或理论是一个隐藏签名r，一个隐藏子签名r，以及一个集合E关于E-equationsΓ中的操作被称为行为的，用于构建实验或上下文，这些实验或上下文是具有可区分的隐藏变量的可见结果的Γ项这些在任何模型上生成行为等价关系，表示为Γ 或者仅仅是两个数据元素相关且它们相等，并且两个状态相关且它们不能被任何实验区分，即，所有的实验在应用于它们时产生相同的值。一个模型在行为上满足一个等式，即两个项在所有变量值的E中的方程限制了模型到行为上满足每个方程的模型一个Σ-运算σ是Γ-行为全等，或仅仅全等（[2019 - 06 - 16]更多详情这个一般框架的一些特殊情况包括原始的隐藏代数[8，9，13，12]，CafeOBJ [7，6]的相干隐代数，Bidoit和Hennicker[17，2]的观测逻辑，以及我们自己以前的版本[8，22，23]。重要的相关方法包括余代数[1，18]和Padawitz的摆动类型[19]。2.1隐方程演绎法标准的等式推导对于行为满意度是不合理的，因为全等规则对于非全等操作是不合理的。然而，斯坦-可以采用标准的等式推导[22]。给定一个行为规范B=（E， r，E），通过以下公式定义EqGOGUEN，LIN，ROSU3B| ≡ ∀B组|∀(1) 回复率：tEqt(2) 对称性：t<$EqtJtJEqt(3) 传递性：t<$EqtJ，tJ<$EqtJJtEqtJJ(4)替换：（Y）t=tJ，如果t1=tJ1，...，tn=tJn∈E，θ（ti）<$Eqθ（ti）(5) 一致性：（a）（b）θ（t）<$Eqθ（tJ）t<$EqtJ，sort（t，tJ）∈V<$σ（W，t）<$Eqσ（W，tJ），对于每个σ∈Der（t）<$t<$EqtJ，sort（t，tJ）∈H<$δ(W, t) ≡Eqδ(W, tJ), for each congruentδ∈ Σ定义B（X）t=tJitEqtJ。 这些规则通过考虑全等和非全等运算推广了[7]中的规则。注意（5b）仅适用于全等运算;如果所有运算都全等，则这些规则成为标准等式演绎。由于行为操作是全等的，我们有许多情况下（5b）适用，更多的情况可以通过证明操作全等来获得，例如，方法[14]。我们将看到，行为重写是行为演绎的一个特例，就像标准项重写是标准等式演绎的一个特例一样。以下内容表达了等式和行为满意度的合理性，概括了[6，7]中的一个结果，即当所有操作都一致时，等式推导是合理的。命题2.1给定（X）t = tJ，则E =<$（X）t = tJ，并且（X）t = tJ.如果所有的操作都是全等的，那么等式演绎对于行为满意度来说是合理的。2.2共诱导经常发生的情况是，并不是所有的实验都需要，因为方程意味着一些实验与其他实验是等价的。在抽象数据类型理论中，当所有元素都由称为构造函数、生成器或基（当GOGUEN，LIN，ROSU4≡≡∀∀→诱导参与）。上基的对偶概念出现在[22]中，后来被简化[14，20，23，21];对于本文，读者可以考虑上基在这个意义上，没有其他实验可以区分这些实验无法区分的两个状态如果是B的上基，则令Eq，是由第2.1节中的规则（1）-（5）生成的关系（6）δ-余归纳：δ（W，t）<$Eq，<$δ（W，tJ）对于所有适当的δ∈<$tEq，tJ[21][22][23][24][25][26][27][28][29][这意味着要证明两个项t，tJ在行为上等价，它必须显示tEq，tJ。余归纳法的优点是，一旦给出一个余基，它就完全成立了找到一个最小的上基似乎是不可判定的，但是有一些共基准则在实践中工作得很好[2，22，23]（详细说明见[21]）。2.3圆余诱导虽然双余归纳法很有用，但由于递归定义的运算在行为规范中会出现循环，因此它仅限于大型实际例子。因此，我们将循环共诱导推广到循环共诱导，通过检测循环，减少的细节。更确切地说，它声明了一个目标t tJ被证明，只要它证明了δ（W，t）δ（W，tJ），或者证明了δ（W，t）和δ（W，tJ）分别是t和tJ的实例，对于上基中的每个运算δ;“实例”的人们可以把它看作是替代品。3行为重写行为重写[6，20]将行为演绎限制在一个单一的许多标准的重写理论被沿用下来。特别地，如果重写是连续的，则方程（X）t=tJ可由下式导出：上面的五个规则i_t和t_J在行为上重写为一个公共术语。也标准重写的终止意味着行为重写的终止，因为$是标准重写的子关系;因此，用于标准重写的任何终止准则都可以应用于行为重写。此外，行为重写可以通过标准项重写以优雅和高效的方式实现，这可以为PVS [24]和Maude [4]等系统添加行为验证。我们首先介绍我们的一般公式：定义3.1重写规则是一对项，写作（Y）l r，其中Y是l，r中的变量集。行为（或隐藏）重写GOGUEN，LIN，ROSU5∀→系统是一个三元组（R，r，R），其中R是一个隐藏签名，r是R的一个隐藏子签名，R是一组重写规则。在下文中，我们假设R=（R，r，R）是行为重写系统，并且B=（R，r，E）是其相关联的行为规范，即，E={（Y）l=r|（<$X）l→r∈R}.定义3.2与行为重写系统R相关联的行为（项）重写关系是最小关系$，使得：- θ（l）$θ（r），对于R中的eachh（X）l→r和eachhθ：Y→T（X），- 若t$tJ且sort（t，tJ）∈V，则对所有σ ∈Der（n），σ（W，t）$σ（W，tJ- 如果t$TJ且sort（t，TJ）∈ H，则对所有δ ∈ Γ，δ（W，t）$δ（W，TJ）.行为重写对标准项重写进行了如下修改：无论何时找到隐藏的redex，当从该redex到根的路径上只有行为2如果没有找到可见的排序，如果从redex到根的路径上的所有操作都是行为性的，则仍然应用重写。定义3.3一个上下文c是行为的，如果在通往它的区别变量的路径上的所有操作都是行为的，并且如果它是行为的或者存在一些可见的行为上下文cJ使得对于一些cJJ，c=cJ[cJ]，那么它是安全的。对于任何出现在t中的变量x，t= c1 [x] = c2 [x]，c1安全当且仅当c2安全。R是弱左（右）线性的，对于R中的每一个重写规则l→r，l（r）是弱线性的。命题3.4 t $tJi在R中有重写规则（Y）lr，安全上下文c，和替换θ使得t = c [θ（l）]和tJ= c [θ（r）]。CafeOBJ在其reduce命令中实现了行为重写的子关系：当在从Redex到根的路径上只有行为操作时，应用规则，直到出现可见排序;如果在该路径上没有可见排序，则不进行重写。然而，行为重写的一般版本可以很容易地在CafeOBJ目前不健全的行为-reduce命令中实现我们的经验是，在许多实际情况下，所有的操作都是全等的，因此可以将Γ视为[22]，在这种情况下，行为重写正是标准重写。命题3.5如果$是c对q，那么q=$q;@q。设bnf（t）表示t的标准形式，如果它存在的话。 然后我们有推论3.6如果$是正则的，则t<$EqtJi <$bnf（t）= bnf（tJ）。2我们的方法要求尽可能多的操作是行为操作，特别是所有一致的操作[22]。但如果愿意的话，可以在这里和以后用“行为或一致”代替GOGUEN，LIN，ROSU63.1BOBJBOBJ支持基于第2节的隐藏代数的行为规范和验证。除了标准重写和顺序排序方程逻辑上的行为重写之外，它还实现了循环归纳重写;所有形式的重写都是模属性，可以是关联、交换和恒等的任何组合。BOBJ使用同余准则自动计算规范的cobases [22]。BOBJ受到CafeOBJ系统的启发，该系统提供重写逻辑以及更严格的隐藏代数版本[6]。BOBJ语法几乎与OBJ 3 [15]相同，除了以下例外：由于使用JavaCC进行解析，术语语法更灵活;除了OBJ 3中的关键字“th“和“obj“之外，BOBJ模块还可以以具有初始语义的数据理论的关键字“dth“（相当于关键字“obj“）开始，以及具有隐藏语义的非线性理论的关键字“bth“开始;所有模块都以关键字“end“结束;行为理论中的操作被认为是一致的，除非给定属性“ncong“;当前选择的模块自动生成的cobasis由命令“show cobasis”显示。”, 命令“set trace on。” BOBJ的实现是KaiLin提出的，它包含了一些新的技术，可以加速重写，实现行为和循环共归纳重写。下面的规范STREAM和ZIP在我们的示例中使用，应该被认为是预加载的。第一个声明由TRIV参数化的无限流，这是一个只有可见排序Elt的内置可见理论。bth STREAM[X：：TRIV]是sortStream。op head：Stream -> Elt.op tail：Stream -> Stream。op_&_：Elt Stream ->Stream。var E：Elt.var S：Stream. eq水头（E&S）= E。eqtail（E&S）=S。端BOBJ的协基算法发现， & 不需要：sort Stream的共同基础是：ophead：Stream -> Elt操作tail：Stream -> Stream第二个规范添加了一个操作，通过交替取元素将两个流“压缩”在一起; BOBJ查找cobasis { head，tail }。bth ZIP[X：：TRIV]是pr STREAM[X]。opzip：Stream Stream -> Stream.GOGUEN，LIN，ROSU7我们 的服务|}→→vars S S ' ： S t r e a m .eq head（zip（S，S '））= head（S）。eq tail（zip（S，S '））= zip（S'，tail（S））。端几种数据类型和许多等式是“内置”的，即，无需用户声明即可使用。 数据类型BOOL布尔值和自然数的NAT。用户可以通过命令“show MOD”查看模块MOD提供的内容。“，用于用户提供的模块和内置模块 。 例 如 ， “ 显 示 真相.. “将 显 示 内 置 i ft h e ne l s ef i 条 件 的 等 式 。3.2用标准重写本节描述了一种用标准重写实现行为重写的方法;它可以将标准重写引擎扩展为具有相对较少编程和较小运行时开销的行为重写引擎。 在这种方法中，操作被“涂成”绿色或红色，重写被应用于项中的位置，如果在该位置处的操作被涂成绿色。 为了简化说明，我们使用相同的符号对于绿色操作，以及对于红色操作具有下标r的新符号：给定隐藏签名<$r，令<$r是具有与<$r相同种类的标准签名，并且具有操作σr：s1.对于每个操作，隐藏结果σ的运算：s1. Snh在k中;也设kJ为签名Σ联系我们S对于每一个S。最后，令Γ是f的隐藏子签名，并且令P是f，Γ是以下f，J项重写系统：1) （X）g（σr（X））→g（σ（X）），对所有的算子σ：s1. sn→h，其中X是适当的不同变量的集合，{x1：s1，.，xn：sn}，σ（X）是σ（x1，.， xn）;2) （σZj，X）τ（Zj，σ（X））→τ（Zj，σr（X）），对于所有τ：w1.wj−1h wj+1. wk→sinn−r and σ：s1. sn→ h，使得h是一个隐藏排序，其中X是如上所述的一组变量，Zj={z1：w1，...，zj−1：wj−1，zj+1：wj+1，.，zk：wk}，τ（Zj，σ（X））是τ（z1，.， zj−1，σ（x1，.，xn），zj+1，...， zk）;3) （<$Zj，X）σjr（Zj，σ（X））→σjr（Zj，σr（X）），对所有σJ：w1.wj−1h wj+1. wk→s和σ：s1. sn→h，使得h是一个隐排序;4) （Z_j，X）δ（Z_j，σ_r（X））→δ（Z_j，σ_r（X）），其中δ：w1.wj−1h wj+1. 在Γ中wk→s，σJ：s1. sn→h，使得h是一个隐藏排序。这些规则描绘术语，以便行为重写只能应用于绿色位置。 第一条规则确保在每个术语是绿色的。 操作g被引入以控制项之上的操作。第二条规则是说，隐藏排序的操作，直接在一个非行为操作下面，必须是红色的，这样行为重写将不会应用在这个位置。第三和第四条规则GOGUEN，LIN，ROSU8⇒BRE∪R向下传播颜色命题3.7 P是正则的，Γ是正则的。”[21]这是一个证明。由此可见，任何一项都有唯一的正规形.，定义3.8设=是与PAINTn，r相关联的n项重写关系，并且给定N项u，设n（u）是它在PAINTn，r中的唯一标准形;如果t是n项，则称n（t）是t的着色。给定一个（j）项u，设（u）为忘记你身上所有的颜色。 设<$（R）是e{（<$X）<$（l）→<$（r）|（X）l→r∈R}，设R是关联的（R∈r（R）作为-n）-重写系统，let =n关联的重写关系，设RJ是RJ-重写系统<$（R）<$PAINT<$，Γ，n（ R） n，r设为关系式==。我们将定义3.3推广到（p.100r）-context：定义3.9A（n = r）-context c是行为的，如果在通往可区分变量的路径上的所有操作都在r中，并且c是安全的，如果它是可区分的，或者存在一些可见的行为上下文cJ，使得对于一些适当的c j j，c = cJ [cJ]。命题3.10如果c是安全的，则对任意的应用重写规则（<$X）<$（l）→<$（r）在<$（R）和任意的替换θ，有<$（c [θ（<$（l））]）$<$（c [θ（<$（r））]）。定理3.11设g（n（t））nn（u）是最内层重写序列，其中t是n-项，u是（n，n，r）-项. 然后1）t$（u）;2) 若R是弱左线性的，g（u）是 R中的正规形，则g（u）是 R中的bnf;3) 如果R终止于t，则R J终止于g（n（t））。[21]见《无量寿经》。我们现在描述行为重写引擎，缩写为BRE，其将行为重写系统R和R的签名上的项t作为输入，并返回R中的t的行为范式：（R，t）n= bnf（t）.给定一个可以设置为使用最内层重写的术语重写引擎RE，例如OBJ3[15]，CafeOBJ [6]或Maude [4]，我们可以使用RE实现BRE，如图1所示。第一步很容易在O（n2）中实现，其中n是的大小。 命题3.7这意味着步骤2终止，并且绘制的t是唯一的。 通过定理3.11中的3），只要R终止为行为重写系统，步骤3就终止，并且通过定理3.11中的2），如果R是弱线性的，则GOGUEN，LIN，ROSU9RBRE（R，t）(i) 生成r（R）和PAINTr，r(ii) 使用RE（PAINTt，r，t）得到t（t）(iii) 得到nf（g（n（t），比如g（u），使用RE（n（R）PAINTn，r，g（n（t）(iv) returnint（u）.图1.一、通过标准项重写实现行为重写可以从在步骤3返回的任何范式中提取行为范式。例3.12由于堆栈例子已经被广泛使用，它们提供了一个有用的基准，而且，它们经常揭示一些新的和有趣的东西。在这里，我们给出了一个非确定性堆栈的行为规范，没有通常的mix-fix-notation：bthNDSTACK正在保护NAT。sort堆栈optop：Stack -> Nat.oppop：Stack ->Stack。操作push：Stack-> Stack[ncong]。var S：Stack.等式pop（push（S））= S。端那么作为BOBJ标准理论的Paint，r如下：此PAINT是prNAT 。 sort 堆栈op top：Stack -> Nat [strat（1 0）].ops pop popr：Stack -> Stack [strat（1 0）].操 作 push pushr ： Stack -> Stack [strat （ 10）]。op g：Stack -> Stack [strat（1 0）].op g：Nat-> Nat[strat（10）]。var S：Stack.等式g（popr（S））= g（pop（S））。***类型第一章等式g（pushr（S））=g（push（S））。***类型第一章等式push（pop（S））=push（popr（S））。***类型（二）等式push（push（S））=push（pushr（S））。***类型（二）等式popr（pop（S））=popr（popr（S））。***类型第三GOGUEN，LIN，ROSU10章等式popr（push（S））=popr（pushr（S））。***类型第三章等式pushr（pop（S））=pushr（popr（S））。***类型第三章等式pushr（push（S））= pushr（pushr（S））。我的天啊类型第三章等式top（popr（S））=top（pop（S））。***类型四、等式top（pushr（S））=top（push（S））。***类型四、等式pop（popr（S））=pop（pop（S））。***类型四、等式pop（pushr（S））=pop（push（S））。***类型四、端GOGUEN，LIN，ROSU11RR现在我们将一些项简化为标准形式，如下所示：打开PAINT。op s：-> Stack.红色push（pop（push（s）。*>应该是：push（popr（pushr（s）red pop（push（pop（push（s）。*>应该是：pop（push（pushr（pushr（s）red pop（pop（push（push（pop（push（s））。*>应该是：pop（pop（push（pushr（pushr（s）redpush（pop（pop（push（push（pop（push（s））。*>应该是：push（popr（popr（pushr（pushr（popr（pushr（s））close因为push下面的操作是红色的，所以下面的RJ规则不会直接应用：R '是保护PAINT。等式pop（push（S））= S。端现在让我们使用平移来计算上面的正规形式打开R '。op s：-> Stack.红色g（push（popr（pushr（s）。*>应该是：g（push（popr（pushr（s）red g（pop（push（popr（pushr（s）。*>应为：g（s）红色g（pop（pop（push（pushr（popr（pushr（s）。*>应为：g（s）红色g（push（popr（popr（pushr（pushr（popr（pushr（s））。*>应该是：g（push（popr（popr（pushr（pushr（popr（pushr（s））关闭定理3.11暗示行为范式分别是push（popr（pushr（s），s，s和push（pop（pop（push（pop（push（push（s））如果我们约简了f（t2）或f（t3）（其中t2，t3是第二项和第三项）而不是g（f（t2））或g（f（t3）），那么我们得到J中的范式popr（pushr（s））。操作g将颜色变为绿色，然后进一步减少，获得真正的行为范式s。应该注意的是，BOBJ并没有用这种方法实现行为重写，而是直接执行，这当然更有效。我们现在讨论有关上述方法的一些问题。1. 真的需要弱左线性吗？是的.我们bth R保护TRIV可见。索尔特河opa：h ->v。op f：h hGOGUEN，LIN，ROSU12-> v.GOGUEN，LIN，ROSU13→→∀→→RR=op m：h-> h[ncong]。var x：h.等式f（m（x），x）= a（x）。端将bre应用于项t =f（m（m（x）），m（x）），其行为范式是a（m（x）），我们在步骤2中得到，f（m（mr（x）），m（x））。 那么g（f（m（mr（x）），m（x）不能在第3步中被约简，所以第4步的结果是f（m（m（x）），m（x））并且没有行为重写发生，这是错误的，因为f（m（m（x）），m（x））$a（m（x））。然而，可以将非弱线性行为系统“线性化”为条件重写系统，例如，在abovee示例中，将beh替换为vioralrule（x）f（m（x），x）→a（x）inRJ通过条件规则（x）f（m（x），xJ）a（x），如果<$（x）=<$（xJ），其中<$是递归实现的无条件规则，忘记了颜色。猜想3.13 t是R i中的bnf，则t（t）是R j中的正规形。证明这个猜想可能是冗长的，但如果它是真的，则定理3.11的2）中不需要R的弱左线性2. 在P AINTn，r中真的需要运算g：s s吗？不总是这样对于v visible的操作g：v v并不是真正必要的，它们只是简化了算法;没有它们，需要对项g（t）进行案例分析，如果t的排序是可见的，则用t替换g（t）。 然而，可能需要针对h hidden的操作g：hh。例如，在NDSTACK中，RJ中的n（t2）和n（t3）是popr（pushr（s）），并且没有办法提取s，T2和T3的行为正常型。但如果没有规则只有一个变量，它的右边，则不需要g操作3. 有必要重写最内层 我们 不知道;但我们知道，没有策略的j项重写可能会产生不合理的模拟行为重写。考虑以下人工示例：bthR是保护TRIV-VISIBLE排序h操作a： h -> vops b c d： h-> hopm：h h-> h[ncong]var x：h等式b（x）= m（x，x）等式c（x）= d（x）...端那么b（c（x））$b（d（x））$m（d（x），d（x））。另一方面，以下是RJ的非最内层有效约简，g（n（b（c（x）=g（b（c（x）n（R）g（m（c（x），c（x）（R），=g（m（c（x），d（x）=g（m（c（x），d（x），GOGUEN，LIN，ROSU14C≡∈≡GCBE并且g（m（cr（x），dr（x）被减小。由于m不在Γ中，所以行为约简b（c（x））$f（c（x），d（x））m可能是不合理的;不合理的重写above的发生是因为RJ不是弱右线性的。猜想3.14如果R是弱右线性的，则定理3.11对RJ中的任意重写成立。4BOBJ中的循环共归纳重写只有少数行为性质可以用等式行为推理来证明。语境归纳[16]和共归纳要强大得多，但需要人为干预。循环共归纳重写集成了循环共归纳重写[23]。它的输入是一对术语，当它证明术语在行为上等价时返回true，否则返回false或无法终止，就像通过重写证明术语相等一样。参见[21]的（非平凡的）正确性证明;这里我们只描述BOBJ实现。根据行为规范=（r，r， ）和一个cobasiteΓ，a一组成对的项（BOBJ可以重新排序以减少非终止的可能性）C和一个n项u，令bnfC（u）表示从u通过在通常的限制下尽可能多地用E重写，行为重写，然后将C中的方程应用于项位置，如果所有（零个或多个）到该位置的路径上的操作 都在Γ-π中。给定一对双项（t，tJ），循环共归纳重写算法（以下表示为CCRW）如下：(i) 设C=0且G={（t，tJ）}(ii) 对于G中的每个（u，uJ），(iii)将（u，uJ）从G移动到C(iv)对于每个δ∈ε(v)设v=bnfC（δ[u，x]）且vJ=bnfC（δ[uJ，x]）(vi)如果vi=vJ，则将（v，vJ）加到G包含仍然未经证明的目标，并包含“循环”中使用的证明。通过定义上基，证明了t tJ的存在性，即证明了δ[t，x]δ[tJ，x]对所有的δn和所有适当的x都成立。注意，方程（t，tJ）可以以上述特殊方式用于证明方程（δ[t，x]，δ[tJ，x]），然后用于证明（t，tJ）;这解释了单词“循环”还要注意，算法可能无法终止。5一些示例我们首先给出了懒惰函数式编程的例子。Louise Dennis使用一个名为CoClam的系统完成了许多类似的示例，GOGUEN，LIN，ROSU15--复杂的启发式规划算法[5];我们尝试的所有示例都是在BOBJ中完成的，没有人工干预或机器推理。感谢Wolfram Schulte让我们开始讨论这个问题。例5.1定义一个函数rev，它接受布尔值的无限流，并返回一个流，其中每个值都被反转，如下所示：bth REV是prSTREAM[BOOL]。op rev：Stream -> Stream. var S：Stream.eq head（rev（S））= nothead（S）。eq tail（rev（S））= rev（tail（S））。端现在我们证明rev（rev（S））等价于S：BOBJ>设置跟踪BOBJ> cred rev（rev（S））== S.=========================================c-REV中的reduce：rev（rev（S））== S，使用REV的协基：操作头：Stream -> Bool操作tail：Stream -> Stream简化为：rev（rev（S））== S添加规则（C1）：rev（rev（S））= S目标是：rev（rev（S））== Sexpand by：op head： Stream -> Bool简化为：truenf：头部（S）目标是：rev（rev（S））== Sexpand by：optail： Stream ->Stream derived using（C1）：truenf：尾部（S）结果：trueC-重写时间：82 ms解析时间：6 ms第一个命令set traceon告诉BOBJ显示它的执行信息;这通常有助于发现规范中的错误，并建议引理。BOBJ的cobasis算法发现rev是全等的，所以cobasis就是head，tail。共基运算应用于这两个项，给出子目标head（rev（rev（S）==head（S）和tail（rev（rev（S）== tail（S）. 第一个直接遵循行为重写（内置模块BOOL包含对于任何布GOGUEN，LIN，ROSU16尔B都不是B == B的事实）。第二子目标需要循环，因为它被简化为rev（rev（tail（S）GOGUEN，LIN，ROSU17==tail（S），这是它的初始目标的实例，其中S被tail（S）替换。BOBJ通过显示关键字“derived”而不是“reduced”来报告循环性，例5.2我们定义有限个流0、1和blink，其中只有0bth BLINK是pr ZIP[NAT]。ops zero one blink：-> Stream.eq头（零）= 0。eq尾（零）=零。eq头（一）=1。eqtail（一）=一。eq head（blink）= 0。eq头部（尾部（闪烁））= 1。eq tail（tail（blink））=blink。端BLINK导入ZIP实例化与内置模块NAT的自然数。blink = zip（zero，one）的性质通过循环推导证明如下：BOBJ>credblink == zip（zero，one）.产生输出BLINK中的c-reduce： blink== zip（zero，one）使用BLINK的cobasis：操作头：Stream -> Nat操作tail：Stream -> Stream简化为：blink== zip（zero， one）添加规则（C1）：blink=zip（zero，one）目标是：blink==zip（zero，one）expand by：op head：Stream-> Nat缩减为：truenf：0目标是：blink==zip（zero，one）expandby：optail：Stream->Stream简化为：tail（blink）==zip（one，zero）添加规则（C2）：tail（blink）=zip（one，zero）targetis： tail（blink）==zip（one， zero）expandby：op head：Stream -> Nat reducedto：truenf：1GOGUEN，LIN，ROSU18--targetis： tail（blink）==zip（one， zero）expandby：optail：Stream -> Stream derivedusing（C1）：truenf：zip（0，1）结果：truecobasis算法找到了BLINK的头和尾，接下来的四个步骤将其用于循环共归纳重写。第一个头应用于两个流，在每种情况下都给出0。然后应用tail，得到新的目标tail（blink）==zip（1，0）。再次将head应用于两个新项，得到1，然后应用tail，得到循环，即子目标blink==zip（zero，one），因此结果为true。例5.3定义所有自然数流的一个明显方法，01234. . . . 定义一个函数natbynat（N）=N&nat（N+1），然后考虑nat（0）。 不太明显的是定义一个函数succ， 通过succ（S） =（head（S）+1）&succ（tail（S））递增流中的所有元素，然后定义nat&' b y n a t '（N）= N s u cc（n a t '（N））。bthNAT-STREAM是pr STREAM[NAT]。op nat：Nat -> Stream.var N：Nat.var S：Stream.eq head（nat（N））=N。eq tail（nat（N））= nat（N+1）。op succ：Stream-> Stream.eq head（succ（S））= head（S）+1。eq tail（succ（S））= succ（tail（S））。op nat' ： N a t - >S t r e a m .eq head（nat '（N））= N。eq tail（nat '（N））= succ（nat'（N））。端我们证明这些定义是等价的，即，nat（0）==BOBJ> cred nat（N）== n a t' （ N ） 。=========================================NAT-STREAM中的c-reduce：nat（N）== nat '（N）简化为：nat（N）== nat'（N）添加规则（C1）：nat（N）=nat'（N）.......添加规则（C2）：.......结果：trueGOGUEN，LIN，ROSU19新规则（C1）用于（C2），（C2）用于最终子目标。GOGUEN，LIN，ROSU20例5.4我们证明了斐波那契流的两种定义的等价性。dthFIBO-NAT是ex NAT。var N：Nat.op f：Nat -> Nat.等式f（0）= 0。等式f（1）= 1。等式f（N +2）= f（N +1）+f（N）。端bthFIBO-STREAM是pr ZIP[FIBO-NAT]。var N：Nat.var S：Stream.op nat：Nat -> Stream.eq head（nat（N））= N。eq tail（nat（N））= nat（N +1）。op f：Stream-> Stream。等式head（f（S））= f（head（S））。等式tail（f（S））= f（tail（S））。opfib：Nat -> Stream。等式fib（N）= f（nat（N））。op add：Stream -> Stream。等式head（add（S））= head（S）+head（tail（S））。eq tail（add（S））= add（tail（tail（S）。op fib '：Nat -> Stream.eqhead（N ′ （ N ） ）= f （ N ）。等式head（tail（N ） ） = f （ N + 1 ） 。eq tail（tail（N））= add（zip（N），tail（N）。端我们省略了长BOBJ输出，但注意发现了三个圆。例5.5我们证明了流的两种行为规范是等价的。首先，我们宣布他们的共同签名：bth SIGMA[X：：TRIV]是sortStream。op head：Stream -> Elt.op tail：Stream -> Stream。op_&_ ：Elt Stream ->Stream。操作奇偶：Stream ->Stream。opzip ：Stream Stream-> Stream.端前三个操作和最后一个操作都是平常的，而奇和偶给出了由奇和偶位置上的元素形成的流。例如，奇数（1 2 3 4 5 6 7 89.）是1 3 5 79、而even（123456789. . . ）是2468。. . . 所有操作都是行为，因为它们保持了预期的行为等效性，如果流具有相同顺序的相同元素，则它们是等价的