Implicit complexity for coinductive data: a characterization of corecurrence

TL;DR

This paper introduces a framework for reasoning about programs with coinductive and inductive data using equational programs and productivity as a core concept, providing an implicit characterization of corecurrence.

Contribution

It offers a novel approach combining computation and reasoning for coinductive data, and characterizes corecurrence through productivity provability in coinductive formulas.

Findings

Characterizes corecurrence via productivity in coinductive formulas.

Uses equational programs to unify computation and reasoning.

Provides an analog to recurrence characterization in a weaker form.

Abstract

We propose a framework for reasoning about programs that manipulate coinductive data as well as inductive data. Our approach is based on using equational programs, which support a seamless combination of computation and reasoning, and using productivity (fairness) as the fundamental assertion, rather than bi-simulation. The latter is expressible in terms of the former. As an application to this framework, we give an implicit characterization of corecurrence: a function is definable using corecurrence iff its productivity is provable using coinduction for formulas in which data-predicates do not occur negatively. This is an analog, albeit in weaker form, of a characterization of recurrence (i.e. primitive recursion) in [Leivant, Unipolar induction, TCS 318, 2004].