Coinduction - 清晰、简洁的描述

Question

我正在学习 coduction（notinduction）作为静态分析课程的一部分。在互联网上翻找，我根本找不到清晰、简洁的描述：

• 什么是共感应
• 联合归纳实际上是如何证明一些事情的（似乎联合归纳就像在我读过的治疗方法中挥舞着一只神奇的手）
• 哪些命题需要共同证明
• 如何操作一个硬币归纳证明

Answer 1

在逻辑编程的上下文中，共归纳更容易理解。我推荐以下教程论文：Gupta 等人的 Coinductive Logic Programming and its Applications，出现在 Proc。国际逻辑编程会议 2007 年。正如递归对应于归纳（最小不动点语义），共同递归对应于共归纳（最大不动点语义）。可以将共同递归视为“没有基本情况的递归”。在没有基本情况的情况下，终止标准必须基于识别计算中的循环（理性的无限证明）。更多细节在教程文件中。

Answer 2

共归纳是沿着计算或过程的步骤进行的归纳。如果每一步都适用，那么它适用于无限计算及其可能无限的结果数据结构。

Answer 3

我的理解（可能是错误的）是这样的：

Coinduction 是一种证明无限数据结构的方法。

就像感应一样，一开始看起来像是作弊。要实现的关键是，而不是：

1. 证明某些东西适用于基本案例
2. 证明它适用于每个“单步”，假设它适用于所有（有限）情况
3. 然后声称它因此适用于所有（有限）情况（这是归纳）

你：

1. 在它适用于所有非有限情况的假设下证明它适用于每个“单步”
2. 声称它因此适用于所有非有限情况（这是共归纳，这是合理的，因为每个非有限情况都是一个（有限）单步序列，后跟一个根据假设起作用的非有限部分）

Coinduction 是一种有用的证明技术，用于建立关于无限数据结构的结构“显而易见”的命题。不幸的是（或不是？）它通常用于证明“显而易见”的事情这一事实使得更难看出它是如何证明任何事情的，而不仅仅是挥手。

This paper 在某些方面很有帮助，而在其他方面则令人困惑（至少是那些没有涉足范畴论的人，我也算在内）。