Termination Checking in the Presence of Nested Inductive and Coinductive Types

Termination Checking in the Presence of Nested Inductive and Coinductive Types
Thorsten Altenkirch and Nils Anders Danielsson
Short note supporting a talk given at PAR 2010, Workshop on Partiality and Recursion in Interactive Theorem Provers. [pdf]

Abstract

In the dependently typed functional programming language Agda one can easily mix induction and coinduction. The implementation of the termination/productivity checker is based on a simple extension of a termination checker for a language with inductive types. However, this simplicity comes at a price: only types of the form νX.μY.F X Y can be handled directly, not types of the form μY.νX.F X Y. We explain the implementation of the termination checker and the ensuing problem.