VENANZIO CAPRETTA VENANZIO.CAPRETTA@NOTTINGHAM.AC.UK
Assistant Professor
Contractive Functions on Infinite Data Structures
Capretta, Venanzio; Hutton, Graham; Jaskelioff, Mauro
Authors
Professor GRAHAM HUTTON GRAHAM.HUTTON@NOTTINGHAM.AC.UK
Professor of Computer Science
Mauro Jaskelioff
Abstract
Coinductive data structures, such as streams or infinite trees, have many applications in functional programming and type theory, and are naturally defined using recursive equations. But how do we ensure that such equations make sense, i.e. that they actually generate a productive infinite object? A standard means to achieve productivity is to use Banach’s fixed-point theorem, which guarantees the unique existence of solutions to recursive equations on metric spaces under certain conditions. Functions satisfying these conditions are called contractions. In this article, we give a new characterization of contractions on streams in the form of a sound and complete representation theorem, and generalize this result to a wide class of non-well-founded structures, first to infinite binary trees, then to final coalgebras of container functors. These results have important potential applications in functional programming, where coinduction and corecursion are successfully deployed to model continuous reactive systems, dynamic interactivity, signal processing, and other tasks that require flexible manipulation of non-well-founded data. Our representation theorems provide a definition paradigm to compactly compute with such data and easily reason about them.
Citation
Capretta, V., Hutton, G., & Jaskelioff, M. (2016). Contractive Functions on Infinite Data Structures. In IFL 2016: Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages (1-13). https://doi.org/10.1145/3064899.3064900
Conference Name | 28th Symposium on Implementation and Application of Functional Languages |
---|---|
Conference Location | Leuven, Belgium |
Start Date | Aug 31, 2016 |
End Date | Sep 2, 2016 |
Acceptance Date | Feb 2, 2016 |
Publication Date | Aug 31, 2016 |
Deposit Date | Mar 16, 2017 |
Publicly Available Date | Mar 16, 2017 |
Journal | Symposium on Implementation and Application of Functional Languages Proceedings |
Publisher | Association for Computing Machinery (ACM) |
Peer Reviewed | Peer Reviewed |
Pages | 1-13 |
Book Title | IFL 2016: Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages |
Chapter Number | Article no. 5 |
ISBN | 9781450347679 |
DOI | https://doi.org/10.1145/3064899.3064900 |
Public URL | https://nottingham-repository.worktribe.com/output/847912 |
Publisher URL | https://dl.acm.org/doi/10.1145/3064899.3064900 |
Files
final_contractions_IFL.pdf
(280 Kb)
PDF
You might also like
Game Forms for Coalition Effectivity Functions
(2019)
Conference Proceeding
The Coinductive Formulation of Common Knowledge
(2018)
Conference Proceeding
A coalgebraic view of bar recursion and bar induction
(2016)
Journal Article
The continuity of monadic stream functions
(2017)
Conference Proceeding
Monadic compiler calculation (functional pearl)
(2022)
Journal Article
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: digital-library-support@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search