Mixing Induction and Coinduction

Mixing Induction and Coinduction
TYPES 2009, Aussois, 2009-05-15. For more information, see Total Parser Combinators and Subtyping, Declaratively. [pdf]

Abstract

Few people seem to be aware of the utility of mixing induction and coinduction in the same definition, as in νX.μY.…. I will discuss some types which are defined using this technique. The common theme is that, while values of these types can be "infinite", the infinity is not unrestricted. For instance, when defining subtyping for recursive types it is natural to let the arrow rule be coinductive, reflecting the fact that recursive types can (conceptually) be infinite. However, the transitivity rule should be inductive, because a coinductive reading of transitivity does not make sense.