On the Foundations of Corecursion

Lawrence S. Moss? Norman Dannery

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 [NWF] and the Corecursion Theorem of Barwise and Moss [VC]. We prove some results relating the two approaches, and we present a framework from which one can derive the results of both.

1 Introduction

By a stream of natural numbers we mean a pair hn; si where n 2 N and s is again a stream of natural numbers. Let f : N ! N . Consider the following function which purports to define a function from N into the streams:

iterf (n) = hn; iterf f(n)i (1)

For each n, iterf (n) is a stream, so iterf itself is a function from numbers to streams. This is an example of a function defined by corecursion. It seems to be similar to recursion, since the symbol iterf is used on both sides of (1). On the other hand, there is no base case," so something different seems to be going on. The purpose of this paper is to consider the foundational problem of justifying such definitions. We review the existing work on this and we offer a general approach as well.

Here is a second example: A tree of natural numbers is a triple hn; t1; t2i where n 2 N and t1, t2 are again trees of natural numbers. Consider the following function o from fa; b; cg into trees over natural numbers:

o(a) = h61; o(c); o(c)i
o(b) = h4; o(b); o(c)i
o(c) = h4; o(a); o(c)i
(2)

This again is a corecursion, this time into the trees. Our main foundational aim is to offer a general theory of such definitions, modeled after what is now standard for definition by recursion. The approach should be broad enough to cover (1) and (2), as well as any similar" example that one would expect to arise.
Our last example has to do with functions into the universe of sets. We ask for a function h defined on f0; 1g so that
h(0) = f3; fh(1)gg
h(1) = f4; h(0); h(1)g (3)

?Departments of Mathematics and Computer Science, Indiana University, Bloomington, IN 47405 USA. yDepartment of Mathematics, Indiana University, Bloomington, IN 47405 USA.