Structured general corecursion and coinductive graphs [extended abstract]

TL;DR

This paper extends the theory of structured recursion to include productive definitions like streams by introducing coinductive graphs, providing a unified framework for both terminating and productive function definitions.

Contribution

It introduces the concept of coinductive graphs to generalize structured recursion, enabling the treatment of productive definitions alongside terminating ones.

Findings

Defines coinductive relations for productive functions

Ensures unique solutions for both terminating and productive definitions

Provides a unified framework for structured recursion and corecursion

Abstract

Bove and Capretta's popular method for justifying function definitions by general recursive equations is based on the observation that any structured general recursion equation defines an inductive subset of the intended domain (the "domain of definedness") for which the equation has a unique solution. To accept the definition, it is hence enough to prove that this subset contains the whole intended domain. This approach works very well for "terminating" definitions. But it fails to account for "productive" definitions, such as typical definitions of stream-valued functions. We argue that such definitions can be treated in a similar spirit, proceeding from a different unique solvability criterion. Any structured recursive equation defines a coinductive relation between the intended domain and intended codomain (the "coinductive graph"). This relation in turn determines a subset of the intended domain and a quotient of the intended codomain with the property that the equation is uniquely solved for the subset and quotient. The equation is therefore guaranteed to have a unique solution for the intended domain and intended codomain whenever the subset is the full set and the quotient is by equality.