Pierre Hyvernat - Representing Continuous Functions between Greatest Fixed Points of Indexed Containers

lmcs:5247 - Logical Methods in Computer Science, July 28, 2021, Volume 17, Issue 3 - https://doi.org/10.46298/lmcs-17(3:13)2021
Representing Continuous Functions between Greatest Fixed Points of Indexed Containers

Authors: Pierre Hyvernat

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.


Volume: Volume 17, Issue 3
Published on: July 28, 2021
Accepted on: March 15, 2021
Submitted on: March 4, 2019
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 43 times.
This article's PDF has been downloaded 20 times.