On the Foundations of Corecursion

Abstract

We consider foundational questions related to the definition of functions by corecursion. This method is especially suited to functions into the greatest fixed point of some monotone operator, and it is most applicable in the context of non-wellfounded sets. We review the work on the Special Final Coalgebra Theorem of Aczel [1] and the Corecursion Theorem of Barwise and Moss [4]. We offer a condition weaker than Aczel's condition of uniformity on maps, and then we prove a result relating the operators satisfying the new condition to the smooth operators of [4].