论文标题
共同引导简单而简单
Coinduction Plain and Simple
论文作者
论文摘要
共同诱导是指无限流，所谓的尾巴的定义技术，也指证明共同指定尾巴的平等的技术。本文首先回顾了声明性编程的共同点。其次，它回顾并稍微扩展了通常用于指定尾巴的形式主义。第三，它概括了共同诱导原理，该原理最初是为相等性谓词指定的其他谓词。这种概括使共同诱导的证明原理更加直观，并强调了其与结构诱导的亲密关系。本文最终提出了其功能和逻辑编程的结论扩展，并具有有限且可决定的广义诱导证明原理。
Coinduction refers to both a technique for the definition of infinite streams, so-called codata, and a technique for proving the equality of coinductively specified codata. This article first reviews coinduction in declarative programming. Second, it reviews and slightly extends the formalism commonly used for specifying codata. Third, it generalizes the coinduction proof principle, which has been originally specified for the equality predicate only, to other predicates. This generalization makes the coinduction proof principle more intuitive and stresses its closeness with structural induction. The article finally suggests in its conclusion extensions of functional and logic programming with limited and decidable forms of the generalized coinduction proof principle.
