Mixing Induction and Coinduction

Mixing Induction and Coinduction
Nils Anders Danielsson and Thorsten Altenkirch
Draft, 2009. For an extended description of the total parser combinators described in this paper, see Total Parser Combinators. For an extended discussion of subtyping for recursive types, see Subtyping, Declaratively. For more information about working around productivity checkers, see Beating the Productivity Checker Using Embedded Languages. For another spin on coinductive operational semantics, see Operational Semantics Using the Partiality Monad. [pdf, highlighted code, tarball with code]

Abstract

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.

Nils Anders Danielsson
Last updated Thu Oct 8 16:21:25 UTC 2009.