coinductive(余归纳的/共归纳的):指一种与 inductive(归纳的) 相对的定义或证明方式,常用于描述无限对象或持续过程(如无限流、反应式系统)。它通常通过“可观察行为”或“保持某种关系不变”(如双模拟 bisimulation)来刻画对象,并常与最大不动点(greatest fixed point)相关。
(在数学逻辑与计算机科学、类型论、形式化验证中最常见。)
/ˌkoʊɪnˈdʌktɪv/
Coinductive definitions are useful for describing infinite streams.
余归纳定义很适合用来描述无限的数据流。
The proof uses a coinductive argument to establish that the two processes are behaviorally equivalent.
该证明使用余归纳论证来确立这两个过程在行为上是等价的。
由前缀 **co-**(“共同、对应”)+ inductive(“归纳的”)构成。含义上强调与归纳方法“对应/对偶”的思路:归纳多用于构造与证明有限结构(常对应最小不动点),而余归纳更侧重刻画可无限展开的结构与其外在可观测性质(常对应最大不动点)。