Recursive Function Definition over Coinductive Types
John Matthews

---

Using the notions of unique fixed point, converging equivalence relation, and contracting function, we generalize the technique of well-founded recursion. We are able to define functions in the Isabelle theorem prover that recursively call themselves an infinite number of times. In particular, we can easily define recursive functions that operate over coinductively-defined types, such as infinite lists. Previously in Isabelle such functions could only be defined corecursively, or had to operate over types containing "extra" bottom-elements. We conclude the paper by showing that the functions for filtering and flattening infinite lists have simple recursive definitions.


Sun Feb 28 19:15:56 PDT 1999