Mixing Induction and Coinduction
Mixing Induction and Coinduction
复制标题
混合感应和共感应
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Thorsten Altenkirch
中科院分区：
文献类型：
--
作者：
Nils Anders Danielsson;Thorsten Altenkirch
纯归纳定义产生树形的值，其中所有分支都有有限的深度，而纯粹的余归纳定义产生所有分支潜在无限的值。如果这过于严格，那么另一种选择是使用混合归纳和共归纳。这项技术似乎相当鲜为人知。本文的目的是使这项技术更加广为人知，并介绍它的几个新的应用，包括一个保证分析终止的分析器组合器库，以及一种将协归纳定义的推理系统与传递性等规则相结合的方法。论文中提出的发展已经在AGDA中得到了形式化和检查，AGDA是一种依赖类型的编程语言和证明助手。
Purely inductive definitions give rise to tree-shaped values where all branches have finite depth, and purely coinductive definitions give rise to values where all branches are potentially infinite. If this is too restrictive, then an alternative is to use mixed induction and coinduction. This technique appears to be fairly unknown. The aim of this paper is to make the technique more widely known, and to present several new applications of it, including a parser combinator library which guarantees termination of parsing, and a method for combining coinductively defined inference systems with rules like transitivity. The developments presented in the paper have been formalised and checked in Agda, a dependently typed programming language and proof assistant.
影响因子：
0.6
作者：
Ghani N
通讯作者：
Ghani N