Mixing Induction and Coinduction
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.Nils Anders Danielsson
Last updated Fri May 15 12:14:37 UTC 2009.