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

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

6 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 language	English
Title of host publication	Types for proofs and programs
Editors	S Berardi, F Damiani, U DeLiguoro
Place of Publication	Berlin
Publisher	Springer
Pages	220-236
Number of pages	17
ISBN (Print)	978-3-642-02443-6
DOIs	https://doi.org/10.1007/978-3-642-02444-3_14
Publication status	Published - 2009
Event	Types for Proofs and Programs: International Conference - Villa Gualino, Turin, Italy Duration: 26 Mar 2008 → 29 Mar 2008 http://types2008.di.unito.it/

Conference

Conference	Types for Proofs and Programs: International Conference
Abbreviated title	TYPES 2008
Country/Territory	Italy
City	Turin
Period	26/03/08 → 29/03/08
Internet address	http://types2008.di.unito.it/

Keywords

Constructive Type Theory
Structural Recursion
Coinductive types
Guarded Corecursion
Coq
DEFINITIONS
PRODUCTIVITY

Access to Document

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

Cite this

@inproceedings{c645f4d4cfee4b129b68e60e65c5e9d6,

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 = "Constructive Type Theory, Structural Recursion, Coinductive types, Guarded Corecursion, Coq, DEFINITIONS, PRODUCTIVITY",

author = "Yves Bertot and Ekaterina Komendantskaya",

year = "2009",

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

language = "English",

isbn = "978-3-642-02443-6",

pages = "220--236",

editor = "S Berardi and F Damiani and U DeLiguoro",

booktitle = "Types for proofs and programs",

publisher = "Springer ",

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

url = "http://types2008.di.unito.it/",

}

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 - Constructive Type Theory

KW - Structural Recursion

KW - Coinductive types

KW - Guarded Corecursion

KW - Coq

KW - DEFINITIONS

KW - PRODUCTIVITY

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

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

M3 - Conference contribution

SN - 978-3-642-02443-6

SP - 220

EP - 236

BT - Types for proofs and programs

A2 - Berardi, S

A2 - Damiani, F

A2 - DeLiguoro, U

PB - Springer

CY - Berlin

T2 - Types for Proofs and Programs: International Conference

Y2 - 26 March 2008 through 29 March 2008

ER -

Using structural recursion for corecursion

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this