归纳法

在计算机科学中，协同归纳是一种定义和证明并发互动对象系统属性的技术。协同归纳是结构归纳的数学对偶。协同归纳定义的类型被称为codata，通常是无限的数据结构，如流。作为一种定义或规范，协同归纳描述了一个对象如何被观察、分解或破坏为更简单的对象。作为一种证明技术，它可以被用来证明一个方程被这种规范的所有可能的实现所满足。为了生成和操作编码数据，人们通常使用corecursive函数，并结合懒惰评估。非正式地，我们不是通过对每个归纳构造函数进行模式匹配来定义一个函数，而是在函数结果上定义每个析构器或观察者。在编程中，共同逻辑编程（Co-LP）是逻辑编程和共同归纳逻辑编程的自然概括，它反过来又概括了逻辑编程的其他扩展，如无限树、懒惰谓词和并发交流谓词。Co-LP在有理树、验证无限属性、懒惰评价、并发逻辑编程、模型检查、双相似性证明等方面有应用。Co-LP的实验性实现可以从德克萨斯大学达拉斯分校以及Logtalk（例子见）和SWI-Prol中获得。

在本文中对归纳原则和联合归纳原则都做了简明的陈述。虽然本文主要关注的不是归纳法，但一次性考虑它们的一般化形式是很有用的。为了说明这些原则，需要一些初步的资料。当你的所有断言都被其他断言所支持时（即没有非F逻辑的假设），X{displaystyleX}是F-conistent。Knaster-Tarski定理告诉我们，F的最小固定点是F{displaystyleF}的最小固定点(表示为μF{displaystylemuF}的最小固定点（表示μF)是由所有F封闭集的交集给出的，而xxx的固定点(表示为νF{displaystylenuF}）由所有F封闭集的交集给出。)是由所有F封闭集的联合体给出的。我们现在可以说明归纳和联合归纳的原则。

归纳法的原则。如果{displaystyleX}是F封闭的。讨论如上所述，这些原则有些不透明，但可以有效地用以下方式来思考。

定义一个数据类型集考虑下面的数据类型语法。以及（非同质的）列表。这些类型可以用字母表上的字符串来识别{displaystyletimes}，以及字符串x{displaystyletimes}的连接。.我们现在应该把我们的数据类型集定义为F{displaystyleF}的火点。