森林砍伐技术：程序等价性证明的自动化搜索和程序转换

88《理论计算机科学电子札记》44卷第1期（2001）网址：http://www.elsevier.nl/locate/entcs/volume44.html40页森林砍伐、规划改造和采伐淘汰Robin Cockett罗宾·科基特1，2卡尔加里大学计算机科学系天气-卡尔加里，加拿大摘要在任何合理的编程语言中，证明两个程序是等价的问题是众所周知的不可判定的。在一个形式化的程序系统中，等价性的规则是有限的，可证明等价性的问题是半可判定的。尽管这种情况得到了改善，但仍然缺乏普遍接受的自动化技术来系统地搜索程序等价性的证明（或反证）寻找等价性证明的技术常常会在归纳法的公式化上遇到困难，当然，还有共同归纳法（当它存在的时候），它们的公式化方式常常需要灵感的猜测。然而，有一些众所周知的程序转换技术可以解决这些问题。本文特别感兴趣的是由菲尔Wadler和Burstall和达林顿介绍的折叠/展开程序转换技术介绍的森林砍伐技术。这些技术是基本的剔除程序的影子，因此，应更普遍地被视为证据技术。在本文中，我们表明，这些技术适用于语言，既有归纳和共归纳datashees。 这些程序转换技术和切割消除之间的关系需要从初始和最终的“代数”证明规则转换为Santocanale引入的“循环”证明规则（并在模型检查社区中隐式使用）。 这种转换只有在某些证明系统中才 是 可 能 的 。 在这 里 ，我 们 表 明 ， 它 可 以 适 用 于 carbohydrate 封 闭 范 畴 与datathees：封闭性是一个基本要求。这里提出的割消定理和伴随的程序转换技术在很大程度上依赖于归纳法和共归纳法的交替表示。1电子邮件地址：robin@cpsc.ucalgary.ca2由加拿大NSERC提供部分支助2000年1月，出版社dbyElsevierScienceB。 V.操作访问和C CB Y-NC-ND许可证。COCKETT891介绍在任何合理的程序设计语言中，证明两个程序等价的问题都是不可判定的。在形式化的编程系统中，等价性是由一组有限的规则来确定的，这种情况得到了更好的控制，因为人们至少可以保证问题的半可判定性。尽管有这种改进，即使在正式系统中，仍然严重缺乏普遍接受的自动化技术，用于系统地搜索两个程序等价性的证明（或反证）寻找两个程序等价的证明的技术通常依赖于归纳的公式化，当然也依赖于共归纳（当共归纳类型存在时）。两个根深蒂固的传统强化了这一点：• 第一个是归纳证明的数学传统，在这个传统中，一个有灵感的“猜测”来制定归纳步骤通常被描绘成是不可避免的。这种发展证明的观点不仅是对自动化的诅咒，而且还助长了这样一种看法，即寻找归纳（因此是共归纳证明）本质上是困难的。• 第二个是计算机科学的习惯，允许一般的递归程序不需要终止。这意味着，在任何（归纳）等价性证明中，都存在第二个问题，即证明终止条件的等价性。这不仅使证明系统复杂化，而且还创造了一个心理上的1.1形式系统中的程序等价本文的目的是提供一个归纳和共归纳数据集的证明理论的观点，这为了做到这一点，我将提出一个正式的编程语言，并讨论其证明理论。我将通过选择一个具有良好终止性的形式系统来避开上面第二点中提到的“良好的端接性能”的确切含义有点技术性。虽然这不是本文的主要重点，但为了更准确地理解这些正式编程系统中的程序等价实际上意味着什么，更准确地理解评估程序的能力提供和不提供什么是有用的。3这超出了本文的范围，但也许值得一提的是，最近的进展在等式的理解中，（见[6，3]）表明，有可能制定简单的等式编程逻辑，给出了一个正式的帐户 这意味着，即使在这个“黑洞”之外，也可能有数量惊人的光！COCKETT901.1.1正式程序设计系统中的评价我将考虑的语言是慈善的一个变体[5]：它既有归纳的也有共归纳的数据集。这意味着我们不能承诺完全终止。例如，考虑产生素数无限列表的程序（当然可以用这种语言编写）：显然不可能产生整个列表。相反，语言以终止的方式还原为“中心范式”的能力较弱。在我们的例子中，这允许素数在需求的基础上一个接一个地产生，并保证我们总是可以以终止的方式产生下一个素数。有关这些问题的进一步讨论，请参见[16]。一个头部的正常形态通常会包含更多的未评估的材料，这些材料可以通过共感破坏的过程来解锁。这导致了共归纳类型的“懒惰”求值策略，它不仅仅是求值顺序的一个侧面：它是整个类型系统的基础。在共归纳记录之外（回想起来，共归纳记录是由类型预先确定的），人们可以以任何顺序进行求值。一个余归纳记录在等价物中冻结了它的参数。这意味着人们实际上可以在这种语言中混合（具有潜在的效率优势）按值求值和惰性求值，而无需更改终止属性。现在评价只适用于封闭项，因此，严格地说，不能解决程序的等价性问题-这通常不会是封闭的。当然，在高阶语言中，我们可以将任意程序内化为高阶类型的闭项。然而，这些更高的类型本质上是共归纳的，因此求值仅仅产生未求值的程序作为头范式，因此，没有获得关于等式的额外信息。然而，在我们抛弃评价之前，值得回顾的是，它可以用来反驳等价性。本质上，这个想法是找到两个程序执行不同的基础“值”（或“点”）。对于任意程序，这是通过提供值和析构到基础类型的组合来实现的这两个过程都是可以理解的，因此可以有条不紊地进行。显然，这种使用程序的逐点行为来区分程序的技术应该是任何自动证明系统的一个组成部分，因为试图证明明显错误的东西可能会导致大量的浪费。1.1.2不可区分的和形式上等价的程序我们注意到，这一讨论揭示了形式编程系统的一个基本（可能相当令人不安）特征：两个在点上不可区分或不可区分的程序不一定是可证明相等的。 如果他们是，我们将立即有一个平等的决定程序-我们不能有！因此，在这样的系统中，不可区分的程序和可证明等价的程序永远不会相同。因此，事实上，没有点，两个给定的程序可以COCKETT91区别并不意味着必须证明这两个程序是等价的。这反过来又引起了一个不愉快的幽灵，即证明系统可能是如此薄弱，以至于人们可能经常遇到在“点”上明显无法区分事实上，在我下面将要考虑的系统中，情况并非如此。对于低复杂度的程序，等价程序和不可区分程序是一致的，因此对于这些程序，等价问题是可判定的。然而，程序复杂性与可判定性的精确关系1.2归纳与余归纳我们现在更直接地转向程序等价性的问题，特别是如何驯服归纳和共归纳程序等价性证明的问题第一小步远离标准的数学归纳法，是所谓的结构归纳法的第一步。这允许以与数学归纳法相同的形式方便地表达任意归纳（或初始）数据类型的归纳参数，其中归纳步骤的形式由数据类型的结构确定（参见Slind [13]）。然而，作为一个可以在编程设置中包含共归纳和归纳数据集的原则，它有明显的缺点。首先，它的表述依赖于子对象（子集）演算的存在：结构归纳论证本质上是通过表明由命题确定的子对象事实上必须是完整的对象来工作的。现在，程序逻辑是否先验地配备了足够强大的子逻辑演算来支持这些归纳论点是可以理解的。先把我们对这些论证所隐含的逻辑水平的关注放在一边，我们立即被迫对这种方法对共同归纳的含义感到更深层次的不适。因为类似的结构共归纳理论必须使用商结构。同样，人们可能会争辩说，这在程序逻辑的层次上是不存在的。然而，这种结构与子对象的结构相比--在实践中，人们必须通过子对象结构来模拟这种结构，这最终导致了互模拟理论。现在，我并不想暗示，对演绎类型的互模拟理论是没有价值的：事实上，我相信它是一个重要的工具，我们对共归纳的理解然而，要达到这一点，人们不能不注意到，人们不得不使用一系列复杂的扭曲。特别是，这些步骤完全掩盖了归纳COCKETT92和共归纳类型作为一个已被迫覆盖的基本程序逻辑与进一步的结构，这严重强调了不对称的基础设置。因此，我认为，这就成为一个合理的问题，问是否可能没有比这更直接的方法来证明一个包含通过共同归纳的证明系统。1.2.1分类公式一个明显的替代出发点，其中归纳和共归纳之间的对称性由对偶给出，使用与归纳（初始）和共归纳（最终）数据集相关的范畴普适性质。这是范畴理论家所熟悉的，他们会声称这是数据范畴所期望的基本属性。其基本思想（见第3节）是归纳（共归纳）数据集是初始代数（分别为）。最终余代数（final coalgebras），因此有唯一确定的映射到所有其他代数（分别）。所有其他的coalgebras）。然而，这种（分类的）抽象观点存在一个主要问题：它很难作为一个证明原则。特别是一个可能需要considerable灵感，以产生一个代数（或余代数），确保所需的等价。因此，从证明自动化的角度来看，这是令人沮丧的，几乎没有改善数学归纳法所描述的原始情况。然而，我们不应该忽视对称性已经恢复的事实。此外，这些概念似乎确实捕捉到了这些结构类型的基本属性。因此，我们可能选择设计的任何系统至少应该满足初始和最终数据集的抽象范畴1.2.2模型检验的经验教训初始和最终代数，在最小和最大不动点的伪装下，也广泛用于模型检验，特别是模态-μ演算。这些发展在硬件和协议验证中找到了有利可图的应用。虽然这些应用程序涉及姿态模型，但涉及的抽象证明理论适用于被视为证明的程序。引人注目的是，这些逻辑中更成功的放弃了初始和最终固定点规则（这是分类的初始和最终“代数”规则，但在该社区中，它们通常被称为“Kozen规则”[9]），以支持更复杂的证明技术。我将把这些称为“循环证明规则”，因为Santocanale [11]以我在这里使用的大致形式向我介绍了它们。这种远离简单固定点规则的运动的优点是显著的，因为这些系统允许人们很容易地看到可导性，即从另一个事物证明一个事物的能力，是可判定的。虽然这不是我们希望解决的问题，但这表明COCKETT93这些循环验证系统提供的更大的功率。从证明理论的观点来看，采用这种改进的证明系统也是一种强烈的必要性：分类或Kozen系统没有一个非常令人满意的割消公式。在这个时间点上，从模型检查社区本身来证实我所做的声明可能相当困难。模型检查器通常不采用证明论的世界观。事实上，即使有“循环证明”（据我所知），也没有关于模态-微演算的割消的直接公开证明相反，有一个博弈论的论点，它在模态微积分中的证明和博弈之间的获胜策略之间进行转换事实上，直接证明更简单，并将在Aldwinckle的论文[1]中与模态-μ1.3削减淘汰的重要性证明系统的一个基本属性是人们应该能够组合证明：这是逻辑系统中切割规则的重要性。以这种方式构造证明的能力对于我们希望在这里利用的程序作为证明的观点来说显然是绝对基本的。根岑[14]的一个重要观察是，逻辑系统通常允许人们通过一系列的证明重写来消除切割基本上这意味着，如果有一个证明，从一个命题到另一个（其中可能使用一些中间命题），然后有一个直接证明，不使用任何中间命题。任何熟悉Phil Wadler关于计划砍伐森林的想法的人[17]都会看到那里的想法与削减消除的目标之间的相似之处。这一点在西蒙·马洛的论文中得到了更明确的阐述程序变形的思想这种移除通常会导致更有效的计划，因为中间结构不再只是为了被摧毁而建造，因此这已经成为程序转换和编译器社区的极大兴趣人们很容易认为，削减消除和森林砍伐是同一件事的计划。然而，情况并非如此：砍伐森林的条款仍然可以有削减。事实上，在某些情况下，必须有剩余削减。然而，保留下来的切割是被移除的采伐是“毁林”采伐：这些采伐会导致数据库（包括副产品和产品）的破坏。在一个逻辑系统中，割消过程具有更进一步的意义。这是一个建设性的过程和它的步骤，这通常是不一致的，实际上决定了证明之间需要的等式。4这就是为什么4并非所有的证明等价都必须由割消强制：逻辑系统也可以有表示规则（例如“左边的逗号是等价的”）。COCKETT94割消也与程序等价的讨论有关：因此，在某种意义上，可以从割消过程确定程序等价的概念。现在，在循环证明系统中，从这些考虑中自然产生的等价规则的形式与程序转换的折叠/展开方法学有着惊人的相似之处[2]：这可能有助于解释为什么这些想法，尽管只是部分正确，仍然是大多数高级程序优化技术的基础我应该提到的是，还有另一种重要的程序转换方法，它确实以基本的方式使用了证明系统的绝对初始和最终代数表示。这些都是fold/build- fusion技术在[？[1]并在[？]. 这些定律依赖于这样一个事实，即应用于由“生产者”程序产生的数据类型的fold这意味着，如果我们可以抽象生产者程序中的（正确的）构造函数，就可以用一个简单的高阶应用程序来替换复合，从而消除这种复合（或切割）。这种技术推广到共归纳数据类型。当然，该技术的难点在于确定如何抽象正确的构造函数在生产者。1.3.1转换证明系统证明系统从基于初始和最终数据集的证明系统（我称之为“基于代数的”证明系统）到“循环证明”系统的转换这解除了他们的必要性，保持平等的证据。不幸的是，当人们把证明看作程序时，证明平等就成了主要的关注点。另外，如果证明要成为编程语言中的程序，正确表达循环证明的方式就成了另一个令人感兴趣的问题这个方向已经由David Turner发展了：事实上，在[15]中，他认为这种编程风格，他称之为“基本强函数式编程”，是函数式编程的未来。本文中的讨论将他的思想与慈善系统联系起来，表明他的编程系统（就其是循环证明系统而言，我没有详细检查这个）有同样的权力。 这是对David Turner伟大的编程直觉的致敬事实证明，循环证明系统意味着初始和最终数据的存在，但相反的含义取决于证明系统的细节（如果它是真的）。鉴于循环证明系统的良好特性，直接使用循环证明而不是初始和最终数据表可能隐含的规则是很有吸引力的。然而，循环产品”），这可能会产生进一步的COCKETT95⇒×证明最终与系统的所有规则相互作用，如果整个程序包不适合在一起，系统就不会表现良好。因此，我花了一些功夫来建立我下面介绍的编程逻辑，它既有循环证明表示，也有基于代数的表示。1.4内容在这个相当长的介绍之后，适当地展示这些关系如何在特定的编程逻辑中发挥作用。为此，我们提出了一个长期演算的carbohydrate封闭范畴与积极的datastries。我们描述了它如何可以被视为一个证明系统，并说明了一些简单的编程示例系统。在这种情况下，最后，我们讨论了隐含的程序等价性，一种技术，为deforesting，和自动化等价证明的可能性。2归纳和共归纳数据库我们将把编程逻辑建立为一种类型理论，因为我们希望把命题作为类型，把程序作为证明范式。我们的程序设计语言的语义基础是一个具有正数据集的Carnival闭范畴我们将认为，余积是原始归纳数据集，而与固定对象（A）的乘积和取幂是余归纳结构的原语。为了避免由逆变函子引起的常见问题（并使事情简单化），我们将只承认原始函子：• 常数函子K;• 乘积函子XY，或对I是有限集，则I∈IXi，其中1是空积;• 余积函子X+Y，或空余积;Σi∈IYi，对于I是一个有限集合，其中0是• 关于固定对象A的指数化，如AX。我们将把从这些基本函子导出的函子称为集合的多项式当然，这些可以涉及多个自由类型变量。这些基本多项式是形成设置的数据集的基础：这些包括多项式和那些可以从基本函子和以下两种类型绑定形式获得的类型：• 一个归纳绑定μX.T，给出类型T相对于类型变量X的初始数据类型或最小固定点;• 给出最终数据类型或最大固定的共归纳绑定νX.TCOCKETT96{r，x：X，r，t：Y}1i i2i、我、∈I总和Γ1，z：i∈IXi，Γ2≠ΣLixi<$→ti i∈Iz：Y{Γti：Yi}i∈IΓ（i：ti）i∈I：i∈IYi prodΓ ►t：YRri（t）：Σ 我i∈IYi总和Rr 1，x1：X1，...，x n：X n，Γ 2π Y乘积r 1，（i1：x1，.， i n：xn）：<$i∈IXi，Γ 2<$YLΓs：YΓx：Xt：ZΓf：Y<$X<$t[f@s/x]：Z密切 Lx：X，Γt：Y关闭rλx.t：XYR图1.一、求和、乘积和闭包规则类型T相对于类型变量X的点。这些构成了我们下面描述的编程环境的积极类型程序逻辑的术语注释规则可以在下面的三个表中描述。第一个图1给出了控制求和、乘积和取幂的推理规则：下面是一些关于图1中定义的术语的注意事项，我们应该将这些术语视为程序：(i) 索引集I都是有限的，其中元素由i1，.， 我，(ii) 在序列左边“声明”的变量必须始终是不同的，但通常可以是产品模式。 因此，以下是一个有效的表达式：(fst ：x1，snd：x2）：Xfst× Ysndx1：X.这是“指数化”产品符号的范例。当没有混淆的危险时，我们倾向于省略索引，让组件的顺序携带这些信息。(iii) 我们遵循标准编程惯例，将所有乘积和联乘积的索引分开，以便索引的名称唯一地确定类型。(iv) 产品具有作为索引记录的术语：(fst ：t1，snd：t2）：Xfst× Ysnd.从这个记录到第一个坐标的投影就是COCKETT97x：Ax：Aid（原子）Y weakr，x：Xt：YΓ1，x1：X，x2：X，Γ2=t：Y 控制r1，x：X，r2t [x/x1，x/x2]：Yr1，x1：X1，x2：X2，r2=Yr1，x2：X2，x1：X1，r2=YexchtJ：Cr1， r，r2<$ [x<$→t]tJ：YΓ1，x：C，Γ2，t：Y切割这个坐标，fst。图二.结构规则(v) 来自联积的映射通过“case”项表示rgtx›→t1t2→t2 X：Xrgt+Ylft→Z和余积嵌入由索引表示(vi) 该逻辑使用λ抽象，并由infix运算符@给出应用程序，正如所有运算符一样，它比普通组合更紧密地绑定下一个图2给出了结构规则，特别是切割规则：注意，第一个规则为原子类型引入了标识规则。重要的是要认识到必须为非原子类型派生标识映射。这种限制在逻辑中很常见，并且大大简化了证明理论。然而，从编程的角度来看，这看起来有点疯狂！虽然可以在不需要“扩展”恒等映射的情况下制定逻辑，但它确实使程序等价性检查稍微复杂一些，因为恒等映射无论如何都需要扩展。这里我们将采用标准的逻辑约定，因为我们的主要兴趣是程序而不是程序优化。请注意，此逻辑具有由语法给出的显式[x<$→t]tJ这直观地意味着x应该被t中的tJ代替。写为令x=t，J，in，t。COCKETT98›→›→›→还请注意，唯一使用显式替换的规则是cut规则。因此，例如，我已经使用直接替换编写了contr（action）规则：这保持了cut的使用与程序中显式替换的出现之间的对应关系。[x t]和tJ的并列应被视为表达式普通的组成。因此，在[x t]f@s中，作为运算符，比组成，应用程序是计算之前的组成。那些熟悉函数式编程和λ演算的人可能会觉得奇怪，我们区分高阶项的应用和函数的应用。在这方面，由于我们希望我们的术语表示证明，我们只是盲目地忠实于作出这种区分的逻辑。显然，表达式[x t]f@s应该在形式上等价于替换式t[（f@s）/x]，事实上也是。正如我们将发现的，许多迫使某些证明等价存在的切消步骤，实际上涉及到将显式替换变成普通替换，在这个意义上是相当平凡的。然而，回想一下，外显替换确实允许被替换的“变量”是一个让淘汰步骤更有内涵的模式现在应该清楚的是，这个片段的证明理论的语义在于具有上积的carbohydrate闭范畴。这个片段满足割消是众所周知的，因为它是直觉主义逻辑的一个变体。此外，这个片段有它的证明等价可判定。在纯逻辑中（即没有原子类型和非逻辑公理），实际上几乎是直接的，因为初始模型只是有限集。在一般情况下，允许任意类型和公理，问题更难，但即使在这种一般情况下，微积分也是可判定的（这些问题在Ghani的论文[7]和Altenkirch，Dybjer，Ho Bertman和Scott [12]的近期工作中进行了讨论） 。最后，我们来谈谈最重要的逻辑规则这个讨论。它们是决定归纳和共归纳数据集行为的规则。术语构造的规则如图3所示。这些需要一些解释：我们将从cons（trash）和dest（rash）规则开始，因为它们稍微简单一些。构造规则允许从其组件构建归纳数据类型：例如，列表可以通过µcons从元素和列表构建。或（作为）一个nil列表，通过µnil。 应用µ规则将一个余积项变为列表项。这种语法可能看起来有点奇怪，因为通常不区分余积项和归纳数据类型项。我们建立这种逻辑的方式要求我们进行区分。我们经常会忽略这个要求，以使这些术语看起来更熟悉。析构规则是双重的：它允许我们将共归纳数据类型分解为它的组成部分。请注意，destruction必须在术语中替换COCKETT99（Zi：=µx。Pi（x））i∈I|zi：Zi，y：ΓfYx：P（Z），.，X：P（Z），y：Γ11 1nn nJ► t：Y中文（简体）x：µx.P（x），.，y：r11► .=.（x，.，y）：Y. （：= x，.，：= x，y）›→ t.J11JnJΓt：P（μx.P（x））consΓµµx.P（x）t：µx.P（x）Z：=νx.P（x） | Γ►gZΠyJ：rt：P（Z）y：Γ ππ。：g=... P（x）= P（x）. y →t。JΓ1，z：P（νx.P（x）），Γ2τt：YdestΓ1，zJ：νx. P（x），Γ2<$t [ννx.P（x）zJ/z]：Y图三.循环归纳与共归纳证明规则在这里使用显式替换可能很诱人，但这应该被抵制，因为如上所述，我们保留显式替换来记录cut规则的出现。剩下的两个规则是归纳和共归纳循环证明规则。这些规则的形式需要一些讨论，因为它们可能不是那么熟悉：本质上它们允许函数的递归指定，但以严格控制的方式。因此，这些规则本质上是Landin请注意，我遵循慈善传统，使用花括号表示归纳项，圆括号表示共归纳项。我们将命名数据集：例如，归纳自然数和列表数据集的定义如下：Nat= µx。1零 +x成功COCKETT1001.好吧2.好吧-是.好吧..：rev（：=，yJ= nil）=- 是的x›→ .. nil（）.- 是的›→yJ..-是的Xj. cons（v，vs）›→ rev 1（vs，µ cons（v，y））.见图4。快退版本：rev：==- 是的x›→ .. nil（）›→- 是的µnil（）..-是的X.. cons（v，vs）›→ app（rev 2（vs），µ cons（v，nil））.图五.天真的逆转列表（A）= µx。1 nil+（Afst× xsnd）cons.这个系统中的append函数变为：：app =x，y›→好吧..- 是的（xJ：=，yJ）›→尼日尔›→yJ没关系- 是的xj.-是的J（x，y）.cons（v，vs）›→ µ cons（v，app（vs，y））。注意，我简化了乘积表示法。还请注意，我们用：=符号表示重新生成的变量。 为了减少括号的嵌套，我们可以用另一种方式来写：app（：=，yJ=y）=- 是的x，y›→ .. nil（）.- 是的›→yJ..-是的Xj. cons（v，vs）›→ µ cons（v，app（vs，y））。这使得符号更接近于函数式语言和慈善机构使用的符号。注意递归变量是如何放在外部的，而非递归参数是如何在引入函数的地方赋值的另一个利用这些循环定义的力量的程序的例子是“快速”反向函数。这在图4中显示：将其与更高阶的定义进行比较，见图13。这个函数的循环（或递归）部分实际上是将第一个列表反转为固定的第二个列表。reverse函数的简单版本（见图5）在外部递归中重复使用append函数。特别要注意的是，尽管我没有指出它们，但在这些术语中有一些削减。例如，像app这样的循环项只能有变量作为参数，所以这些变量必须由cut提供COCKETT101好吧. （零，）›→µ零.好吧好吧x，y›→：monus（：=，：=）=- 是的好吧..- 是的 （m，zero） ›→m- 是的... （x，y）。.. （succ（m），succ（n））›→ μ succ monus（m，n）.图六、同时递归Monus第二个一般来说，我们不应该一丝不苟地记录削减，因为有一个显着的记法开销，而不是我们将随时使用替代（虽然往往无法推导）的术语。然而，我们注意到，切口的存在往往表明某些东西可以简化。还请注意，我们可以随意使用以前定义的循环函数的名称。归纳数据集的循环证明规则也允许同时递归。因此，可以同时“解开”多个归纳数据类型。然而，请注意，我们不能对共归纳数据集这样做，因为在逻辑中存在一个基本的不对称性，它允许左边的命题（类型）列表，但右边只有一个命题（类型）。同时递归的能力具有实际的重要性，因为它允许有效地实现某些功能。这里有一个众所周知的例子：没有同时递归或高阶函数项，就不可能提供图6所示的monus的有效实现。请注意，术语逻辑中递归参数的位置由：=类型绑定器指示，因此，在要递归应用的循环函数f中，我们精确地知道哪些参数是活动的。在证明理论中，循环函数涉及引入的类型Zi，其范围由方框分隔。这些类型变量Zi是底层递归类型的重新生成Zi：=µx.Pi（x）.当然，再生关系是可传递的。一个类型变量ZiJ是另一个类型Zi的再生，它可以被完全当作类型Zi来处理。关键的是，反过来是不正确的，因此循环函数不能应用于其类型变量的早期生成重新生成的类型变量与其起源的数据类型之间存在另一种重要的区别：我们不允许将构造（或析构）规则应用于重新生成的变量。这是因为这样的应用程序将逆转再生过程。但是，我们允许重新生成的变量应用数据类型的循环证明规则。因此可以进行多次再生，也就是说，再生的变量本身也可以再生。为了说明再生的力量，考虑生产的问题，COCKETT102-是. nil（）›→ µnil. nil（）›→µnil）.好吧.x›→：odd（：=）=- 是的好吧.-是的- 是的-是的- 是的cons（v，vs）›→ µcons（v，...好吧. X..vs）好吧- 是的JJJ.-是的.. cons（，L）›→ odd（L））。 .见图7。奇函数Z：=列表（A）|列表（A）ZJ：=ZZJList（A）奇怪A，ZJAA，ZJList（A）A，ZJA×List（A）A，ZJ1+A×List（A）µconsA，1个列表（A）µnilA，ZJList（A）A，A，ZJList（A）A，A×ZJList（A）弱A，1+A×ZJList（A）A，ZList（A）µnilA×Z List（A） 1List（A）1+A×ZList（A）List（A）List（A）图8.第八条。奇数的循环证明从一个列表中，有奇数索引的元素的列表。 程序如图7所示：我使用了另一个约定：即一个从不使用其循环函数的循环证明项可以通过简单地完全省略所引入的函数来表示。这几乎将语法简化为casecombinator的语法，当然，这种近乎混乱的符号是故意的。本示例的目的是说明多重再生的使用。虽然不难看出，我们可以在没有多重再生的情况下实现这一点（见后面的图14），但我认为最终的程序要不那么自然。在图8中，我们给出了这个项的推导，它显示了证明中的再生模式请注意，首先，重新生成的类型变量Z被视为.COCKETT103Z：= InfL（A）|InfL（A），List（A）A，List（A）A×List（A）consACCJList（A）列表（A）A，List（A）List（A）InflL（A），List（A）ZcutA、列表（A）、InfL（A）和ZInfL（A），List（A）List（A）InfL（A），List（A）ZInfL（A），List（A）List（A）×ZA×InfL（A），List（A），目标Z-是的.（L，vs）›→► ►：accJ：InfL（A），List（A）→List（A）=- 是的IL›→IL。HD：vs. . nil（IL，µ nil）.- 是的..tl：accJ（tlνL，µ cons（hdνL，vs））-是的..见图9。简单累加无List（A）InfL（A）、List（A）InfL（List（A））切割InfL（A）InfL（列表（A））图10个。简单累加函数的证明列表（A）是循环推导的主题。然而，这个内部循环推导并不使用它的循环函数。相反，重新生成的类型变量ZJ被视为Z，并应用了函数oddJ到它。现在，同样的考虑也适用于共归纳数据集。我们用一个“累加”无限列表的函数来说明这种语言的共归纳方面给定一个无限列表InfL（A），这个函数产生一个无限列表InfL（List（A）），其中内部列表给出了迄今为止看到的元素列表。现在有两种方法可以累计到目前为止看到的值：第一种，见图9，以逆序收集元素，第二种，见图11，按顺序收集元素。无限列表数据类型定义如下：InfL（A）= νx.Ahd× xtl.注意，这种无限列表总是有一个由fiat表示的“下一个元素”。它不能为空或决定停止！这是一个简单的例子，说明了如何将共归纳数据集和归纳数据集结合使用来生成程序。 这一术语的推导是（近似！）图10显示。注意，这个证明确实包含了一些削减，在术语中，我压抑了。然而，这些削减都是软削减，所以实际上我们应该把这个词看作是已经砍伐森林。然而，图11中的accumulate函数的版本以正确的顺序收集列表，COCKETT104-是的.（L，vs）›→：accJ：InfL（A），List（A）→List（A）=- 是的IL›→IL。HD：vs. . nil（IL，nil）.- 是的..tl：acc（tlL， app（vs，cons（hdL， nil）-是的..图十一岁按顺序累加我们将在第4.3.3节中看到如何砍伐森林）：这就结束了我们对正式编程语言的介绍，我们将在续集中使用在这个阶段，读者应该相信，一个人可以写出非平凡的程序这种语言是一种基本的3初始和最终数据的转换这些循环证明规则尽管符合递归编程风格，但乍一看似乎并不符合数据集的初始代数和最终余代数解释。回想一下，如果F（A，X）是函子，那么μX.F（A，X）配备有映射cons：F（A，μX.F（A，X））→μX.F（A，X）是F（A，）的初始代数，如果对每个F（A，）-代数g：F（A，Z）→Z存在唯一的映射h：μX.F（A，X）→Z，使得以下等式可以交换：F（A，μX.F（A，X））与μX.F（A，X）F（A，h）HJJF（A，Z）gZ.这是初始代数的普适性质最终余代数的对偶共轭性定义如下：νX.F（A，X）配以映射dest：νX.F（A，X）→F（A，νX.F（A，X））是F（A，）的一个最终代数，如果对每个F（A，）-余代数gJ：Z→F（A，Z）COCKETT105dest，。 .、r，z：P（Y），r，t：Y1J2r1，v：μx.P（x），r2μ x..初始. zJ›→t. v：YΓt：P（μx.P（x））consr_（x）t：μx.P（x）Γ，x：Zt：P（Z）..r，v：Z...Σ最终. x→t。v：v x.P（x）Γ1，z：P（νx.P（x）），Γ2τt：Ydestr1，zJ：νx.P（x），r2nt [destνx.P（x）zJ/z]：Y图12个。基于代数的证明系统存在唯一的映射hJ：Z→νX.F（A，X）使得下列可交换：ZgJF（A，Z）hJF（A，hJ）J JνX.F（A，X） F（A，νX.F（A，X））.这些条件不仅断言比较映射的存在，而且重要的是断言该映射的唯一性比较映射的唯一性迫使系统的程序具有某些自然的等式。这种基于代数的数据库方法也可以转换为注释的推理规则（见图12）。当一个人写下这些规则时，他很快就会意识到，他需要“在上下文中”的初始属性，因为为了保持逻辑的风格，他必须允许在逻辑的左手边的初始属性之外的其他命题（类型）。这并不直接涉及上述归纳数据集的属性，然而，至少在卡氏闭合设置中，上述图表确实可以将上下文分流到右侧。 这些问题在[4]和巴特·雅各布斯关于范畴逻辑的书[8]中有非常详细的描述。这基本上是慈善语法，如[5]所述，该论文提供了几个程序的例子。本节的主要目的是表明，它是可能的翻译COCKETT106这两种证明方式之间的区别5我们将通过这两个证明来说明这一点，但重要的是要认识到，这一工作也必须对证明项起作用，这实际上给出了一种在两种编程风格之间进行转换的方法。我们将首先展示基于代数的证明系统（在模型检查社区中有时被称为Kozen系统[9]）可以通过循环证明系统来模拟。为此，我们首先需要展示如何在循环证明系统中获得初始代数推导。所需的推导具有以下形式：Z：=µx。P（x）|Γ1ZΓ2<$fXFΓ1，Z，Γ2<$X函子假设Γ1，P（Z），Γ2<$P（X）Γ1，P（X），Γ2<$XΓ1，P（Z），Γ2<$XΓ1，μx.P（x），Γ2<$X切割标记为“函子”的推论它对应于一个众所周知的范畴观察，即所有涉及的函子都是接下来，我们需要展示如何在循环证明系统中模拟最终余代数推导。这与上面的非常相似，并再次使用函子P的强度：Z：= νx.P（x）|r 1，Y，r 2，r 3，r 4，r 5，r 6，r 7，r 8，r 9，r 10，r 11，r 12，r 13，r14，r 15，r 16，r 17，r 18，r19假设Γ1，Y，Γ2<$Zh函子Γ1，Y， Γ2<$P（Y）Γ1，P（Y），Γ2<$P（Z）截集Γ1，Y，Γ2<$P（Z）r1，Y， r2，rv x，P（x）这表明循环证明系统可以模拟基于代数的证明系统的所有推导。我们现在必须证明我们可以在基于代数的证明系统中模拟循环证明系统的所有证明。这有点困难，因为我们还必须处理多次再生和同时递归的可能性。因此，我们将分三个阶段处理这一问题首先我们5请注意，这篇译文背后的想法并非原创。特别是，我非常感谢Santocanale向我介绍了他对具有初始和最终不动点的有限双完全偏序集情况的证明[11]：我毫不羞愧地借用了他的想法。COCKETT107...将表明，当递归是顺序的，并且没有多次重新生成时，我们可以很容易地将证明转换为基于代数的证明系统。接下来，我们将展示一个同时递归的循环证明可以（在循环证明系统中）简化为一个只有顺序递归的循环证明。最后，我们展示了如何证明与多个再生可以减少到一个只有单一的再生。考虑一个归纳类型的程序的循环证明，没有再生。让π代表从圆形假设导出的结果，这具有一般形式：Z：= µx.P（x）|Γ，Z<$XΓ，Z<$Xπ（Z）Γ，P（Z）<$XΓ，μx.P（x）<$X实际上有很多证明，我们可以把它转化成，但是我们必须要小心。例如，下面这句话似乎是一个合理的翻译：XXweakΓ，X， Γ<$X π（X）Γ，P（X）<$X初始Γ，μx.P（x）<$X这里我们大量使用了一个事实，这并不完全明显，证明π（Z）在Z中是参数的。之所以这样做是因为唯一可以涉及使用Z的隐式类型的规则是该类型的循环归纳规则。然而，使用该规则将意味着存在多次再生。因此，我们可以在证明π（Z）中用任意的X代替Z，得到一个涉及X的证明。然而，考虑一下这种转变对图4中介绍的快速反转的核心有什么影响：它变成了- 是的..（x，y）›→ n..nil：（） ›→y.-是的. 缺点：（，vs）›→ vs.它等价于（x，y）→y。完全不是我们想要的！这种转换方法的问题是，非递归参数在被rev1函数使用之前就被修改了。通过削弱，我们实际上抛弃了这些修改。为了获得正确的翻译，必须充分利用语言的高级方面可以方便地假定，X