Using structural recursion for corecursion

Yves Bertot; Ekaterina Komendantskaya

doi:10.1007/978-3-642-02444-3_14

Using structural recursion for corecursion

Yves Bertot^*, Ekaterina Komendantskaya

^*Corresponding author for this work

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages	220-236
Number of pages	17
Volume	5497 LNCS
DOIs	https://doi.org/10.1007/978-3-642-02444-3_14
Publication status	Published - 2009
Event	International Conference on Types for Proofs and Programs, TYPES 2008 - Torino, Italy Duration: 26 Mar 2008 → 29 Mar 2008

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5497 LNCS
ISSN (Print)	03029743
ISSN (Electronic)	16113349

Conference

Conference	International Conference on Types for Proofs and Programs, TYPES 2008
Country/Territory	Italy
City	Torino
Period	26/03/08 → 29/03/08

Keywords

Coinductive types
Constructive Type Theory
Coq
Guarded Corecursion
Structural Recursion

Access to Document

10.1007/978-3-642-02444-3_14

Cite this

Bertot, Y., & Komendantskaya, E. (2009). Using structural recursion for corecursion. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5497 LNCS, pp. 220-236). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5497 LNCS). https://doi.org/10.1007/978-3-642-02444-3_14

Bertot, Yves ; Komendantskaya, Ekaterina. / Using structural recursion for corecursion. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5497 LNCS 2009. pp. 220-236 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{145160f30a1441048d0681fdedae95c9,

title = "Using structural recursion for corecursion",

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.",

keywords = "Coinductive types, Constructive Type Theory, Coq, Guarded Corecursion, Structural Recursion",

author = "Yves Bertot and Ekaterina Komendantskaya",

year = "2009",

doi = "10.1007/978-3-642-02444-3_14",

language = "English",

isbn = "3642024432",

volume = "5497 LNCS",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "220--236",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

note = "International Conference on Types for Proofs and Programs, TYPES 2008 ; Conference date: 26-03-2008 Through 29-03-2008",

}

Bertot, Y & Komendantskaya, E 2009, Using structural recursion for corecursion. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 5497 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5497 LNCS, pp. 220-236, International Conference on Types for Proofs and Programs, TYPES 2008, Torino, Italy, 26/03/08. https://doi.org/10.1007/978-3-642-02444-3_14

Using structural recursion for corecursion. / Bertot, Yves; Komendantskaya, Ekaterina.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5497 LNCS 2009. p. 220-236 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5497 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Using structural recursion for corecursion

AU - Bertot, Yves

AU - Komendantskaya, Ekaterina

PY - 2009

Y1 - 2009

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

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

KW - Coinductive types

KW - Constructive Type Theory

KW - Coq

KW - Guarded Corecursion

KW - Structural Recursion

UR - http://www.scopus.com/inward/record.url?scp=68749099892&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-02444-3_14

DO - 10.1007/978-3-642-02444-3_14

M3 - Conference contribution

AN - SCOPUS:68749099892

SN - 3642024432

SN - 9783642024436

VL - 5497 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 220

EP - 236

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

T2 - International Conference on Types for Proofs and Programs, TYPES 2008

Y2 - 26 March 2008 through 29 March 2008

ER -

Bertot Y, Komendantskaya E. Using structural recursion for corecursion. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5497 LNCS. 2009. p. 220-236. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-02444-3_14

Using structural recursion for corecursion

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Fellowship CLANN EP/F044046/1: Computational Logic in Artificial Neural Networks

Cite this

Using structural recursion for corecursion

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Projects

Fellowship CLANN EP/F044046/1: Computational Logic in Artificial Neural Networks

Cite this