Using structural recursion for corecursion

Yves Bertot*, Ekaterina Komendantskaya

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

We propose a (limited) solution to the problem of constructing stream values defined by recursive equations that do not respect the guardedness condition. The guardedness condition is imposed on definitions of corecursive functions in Coq, AGDA, and other higher-order proof assistants. In this paper, we concentrate in particular on those non-guarded equations where recursive calls appear under functions. We use a correspondence between streams and functions over natural numbers to show that some classes of non-guarded definitions can be modelled through the encoding as structural recursive functions. In practice, this work extends the class of stream values that can be defined in a constructive type theory-based theorem prover with inductive and coinductive types, structural recursion and guarded corecursion.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages220-236
Number of pages17
Volume5497 LNCS
DOIs
Publication statusPublished - 2009
EventInternational Conference on Types for Proofs and Programs, TYPES 2008 - Torino, Italy
Duration: 26 Mar 200829 Mar 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5497 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

ConferenceInternational Conference on Types for Proofs and Programs, TYPES 2008
Country/TerritoryItaly
CityTorino
Period26/03/0829/03/08

Keywords

  • Coinductive types
  • Constructive Type Theory
  • Coq
  • Guarded Corecursion
  • Structural Recursion

Fingerprint

Dive into the research topics of 'Using structural recursion for corecursion'. Together they form a unique fingerprint.

Cite this