### 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 language | English |
---|---|

Title of host publication | Types for Proofs and Programs |

Subtitle of host publication | International Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers |

Editors | Stefano Berardi, Ferruccio Damiani, Ugo de’Liguoro |

Publisher | Springer |

Pages | 220-236 |

Number of pages | 17 |

ISBN (Electronic) | 9783642024443 |

ISBN (Print) | 9783642024436 |

DOIs | |

Publication status | Published - 2009 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Berlin Heidelberg |

Volume | 5497 |

ISSN (Print) | 0302-9743 |

### Keywords

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

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

## Cite this

Bertot, Y., & Komendantskaya, E. (2009). Using structural recursion for corecursion. In S. Berardi, F. Damiani, & U. de’Liguoro (Eds.),

*Types for Proofs and Programs: International Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers*(pp. 220-236). (Lecture Notes in Computer Science; Vol. 5497). Springer. https://doi.org/10.1007/978-3-642-02444-3_14