Recursion and Corecursion Have the Same Equational Logic
Lawrence S. Moss · Electronic Notes in Theoretical Computer Science · 1999
This paper is concerned with the equational logic of corecursion, that is of definitions involving final coalgebra maps. The framework for our study is iteration theories (cf. e.g. [1,2]), recently reintroduced as models of the FLR0 fragment of the Formal Language of Recursion [5–7]. We present a new class of iteration theories derived from final coalgebras. This allows us to reason with a number of types of fixed-point equations which heretofore seemed to require to metric or order-theoretic ideas. All of the work can be done using finality properties and equational reasoning. Having a semantics, we obtain the following completeness result: the equations involving fixed-point terms which are valid for final coalgebra interpretations are exactly those valid in a number of contexts pertaining to recursion. For example, they coincide with the equations valid for least-fixed point recursion on cpo's.