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.
%0 Conference Paper
%1 Capretta2016Contractive
%A Capretta, Venanzio
%A Hutton, Graham
%A Jaskelioff, Mauro
%B Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages - IFL 2016
%D 2016
%I ACM Press
%K 47h09-contraction-type-mappings-nonexpansive-mappings 68n18-functional-programming-and-lambda-calculus 68p05-data-structures 68q85-models-and-methods-for-concurrent-and-distributed-computing
%P 1--13
%R 10.1145/3064899.3064900
%T Contractive Functions on Infinite Data Structures
%U http://dx.doi.org/10.1145/3064899.3064900
%X 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.
%@ 9781450347679
@inproceedings{Capretta2016Contractive,
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.}},
added-at = {2019-03-01T00:11:50.000+0100},
author = {Capretta, Venanzio and Hutton, Graham and Jaskelioff, Mauro},
biburl = {https://www.bibsonomy.org/bibtex/2ffa9c8dbfd13a2e0921202ac7d782f59/gdmcbain},
booktitle = {Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages - IFL 2016},
citeulike-article-id = {14460109},
citeulike-attachment-1 = {capretta_16_contractive.pdf; /pdf/user/gdmcbain/article/14460109/1120781/capretta_16_contractive.pdf; c7db4af77104e9a22d64c3c6aec1ffe95b14767b},
citeulike-linkout-0 = {http://dx.doi.org/10.1145/3064899.3064900},
doi = {10.1145/3064899.3064900},
file = {capretta_16_contractive.pdf},
interhash = {1e7128b0b970bbcddaa4803803338deb},
intrahash = {ffa9c8dbfd13a2e0921202ac7d782f59},
isbn = {9781450347679},
keywords = {47h09-contraction-type-mappings-nonexpansive-mappings 68n18-functional-programming-and-lambda-calculus 68p05-data-structures 68q85-models-and-methods-for-concurrent-and-distributed-computing},
location = {Leuven, Belgium},
pages = {1--13},
posted-at = {2017-10-17 23:14:53},
priority = {5},
publisher = {ACM Press},
timestamp = {2019-03-01T00:11:50.000+0100},
title = {{Contractive Functions on Infinite Data Structures}},
url = {http://dx.doi.org/10.1145/3064899.3064900},
year = 2016
}