Filters on Co-Inductive streams: an application to Eratosthenes' sieve
Résumé
We show how to model filter functions on the co-inductive types of infinite streams in type theory. These functions are partial but the theory imposes total functions. Our solution relies on describing a predicate characterizing the definition domain of filter functions, with a combination inductive and co-inductive aspects.
Loading...