Implicit complexity for coinductive data: a characterization of corecurrence

Daniel Leivant
(Indiana University and LORIA Nancy)
Ramyaa Ramyaa
(Indiana University and Ludwig-Maximilians-Universität München)

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].

In Jean-Yves Marion: Proceedings Second Workshop on Developments in Implicit Computational Complexity (DICE 2011), Saarbrücken, Germany, April 2nd and 3rd, 2011, Electronic Proceedings in Theoretical Computer Science 75, pp. 1–14.
Published: 1st January 2012.

ArXived at: https://dx.doi.org/10.4204/EPTCS.75.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org