coinduction（余归纳/共归纳）：一种在逻辑与计算机科学中常用的证明与定义方法，主要用于处理无限结构或持续过程（如无限流、反应式系统）。它通常通过展示某种不变关系（常见为“双模拟”bisimulation）来证明性质成立，与“归纳（induction）”常用于有限构造相对。
/ˌkoʊɪnˈdʌkʃən/
Coinduction is useful for reasoning about infinite streams.
余归纳法有助于推理无限流。
Using coinduction, we can prove that two processes are equivalent by exhibiting a bisimulation relation between them.
使用余归纳法，我们可以通过给出两者之间的双模拟关系来证明两个进程等价。
co- 表示“共同、对应”，induction 表示“归纳”。“coinduction”字面上可理解为“与归纳相对/相伴的归纳方式”，在形式化方法中常与coalgebra（余代数）、最大不动点（greatest fixed point）的思想相关，用来刻画无限对象或持续行为。
Select Language