Coinduction - 清晰,简洁的描述

Question

我正在研究coinduction(非归纳)作为静态分析课程的一部分.在互联网上肆虐,我根本没有找到清晰,简洁的描述:

• 什么是coinduction
• coinduction如何实际证明了某些东西(似乎coinduction就像在我读过的治疗中挥舞着一只神奇的手)
• 什么命题需要共同证明
• 如何操作共同证明

Answer 1

我的理解(可能是错的)是这样的:

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

就像感应一样,一开始似乎在作弊.要意识到的关键是:而不是:

1. 证明某些东西适用于基本情况
2. 证明它适用于每个"单步",假设它适用于所有(有限)情况
3. 然后声称它适用于所有(有限)案例(这是归纳法)

你改为:

1. 证明,它适用于所有非有限的情况,它适用于每个"单步"
2. 声称它适用于所有非有限的情况(这是共同诱导,并且它是合理的,因为每个非有限情况是一个(有限的)单步骤序列,后面是一个非假设的无限部分)

Coinduction是一种有用的证明技术,用于建立关于无限数据结构的结构"明显"命题.不幸的是(或者不是？)事实上,它通常有助于证明"明显"的东西,这使得它更难以看出它是如何证明任何东西而不仅仅是挥手.

本文在某些方面有所帮助,而在其他方面则令人困惑(至少那些在类别理论中不了解的人,我自己也算在其中).

Answer 2

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