Coinduction

定义 Definition

coinduction（余归纳/共归纳）：一种在逻辑与计算机科学中常用的证明与定义方法，主要用于处理无限结构或持续过程（如无限流、反应式系统）。它通常通过展示某种不变关系（常见为“双模拟”bisimulation）来证明性质成立，与“归纳（induction）”常用于有限构造相对。

发音 Pronunciation (IPA)

/ˌkoʊɪnˈdʌkʃən/

例句 Examples

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.
使用余归纳法，我们可以通过给出两者之间的双模拟关系来证明两个进程等价。

词源 Etymology

co- 表示“共同、对应”，induction 表示“归纳”。“coinduction”字面上可理解为“与归纳相对/相伴的归纳方式”，在形式化方法中常与coalgebra（余代数）、最大不动点（greatest fixed point）的思想相关，用来刻画无限对象或持续行为。

相关词 Related Words

• Bisimulation
• Coalgebra
• Corecursion
• Deduction
• Fixed Point
• Induction
• Invariant
• Recursion

文学与典籍 Literary Works

• Davide Sangiorgi, Introduction to Bisimulation and Coinduction（专门系统介绍双模拟与余归纳的经典教材）
• Benjamin C. Pierce, Types and Programming Languages（在类型系统与语言语义的语境中提到余归纳/相关概念）
• Yves Bertot & Pierre Castéran, Interactive Theorem Proving and Program Development: Coq’Art（在 Coq 证明助手的形式化证明背景下涉及余归纳对象与证明）
• Peter Van Roy & Seif Haridi, Concepts, Techniques, and Models of Computer Programming（讨论流、惰性计算等内容时与余归纳思想相关）