Representing Continuous Functions between Greatest Fixed Points of Indexed Containers
Logic in Computer Science
2023-06-22 v4
Abstract
We describe a way to represent computable functions between coinductive types as particular transducers in type theory. This generalizes earlier work on functions between streams by P. Hancock to a much richer class of coinductive types. Those transducers can be defined in dependent type theory without any notion of equality but require inductive-recursive definitions. Most of the properties of these constructions only rely on a mild notion of equality (intensional equality) and can thus be formalized in the dependently typed language Agda.
Keywords
Cite
@article{arxiv.1902.10971,
title = {Representing Continuous Functions between Greatest Fixed Points of Indexed Containers},
author = {Pierre Hyvernat},
journal= {arXiv preprint arXiv:1902.10971},
year = {2023}
}