Infinite Objects and Proofs
Potentially infinite lists
The chapter on co-inductive types of our book
is mainly illustrated with the theory of finite or infinite ("lazy") lists.
This file contains the complete development
of this theory.
Please notice that most of exercises proposed in the book are solved
in .
Here are some more exercises on this topic.
Exercise 13.1 page 350 Mapping finite lists to lazy lists
Exercise 13.5 page 357 Mapping a function on a stream
Erratum 6th line (on the book) : read "such that LMapcan ..." instead
of "such that LMap ..."
Exercise 13.13 page 366 A boggy definition of Infinity
Exercise 13.16 page 367 Finiteness, infinity and classical logic
Exercise 13.17 page 368 Another definition of infinite lists
Exercise 13.29 page 373 Using finiteness hypotheses
Building a recursor for finite Llists
Lazy binary trees
All the technology illustrated by linear lists apply to
tree structures. The following thread of exercises is devoted to
binary trees which may have infinite branches.
Exercise 13.2 page 351 Potentially infinite trees
Exercise 13.3 page 355 Building some complex trees
Exercise 13.4 page 355 Grafting trees
Exercise 13.14 page 366 Trees with [in]finite branches
Exercise 13.23 page 370 Tree bisimilarity
Exercise 13.26 page 371 A theorem on graft
Further Reading
Yves Bertot, then Yves Bertot and Ekaterina Komendantskaya published two papers
for solving the filter issue on infinite lists. The first paper shows how
to define the stream of prime numbers using Erathsthenes's sieve.
The second paper presents a generalization of the employed techniques.
Both papers show how to mix inductive and co-inductive techniques. They also
use sophisticated techniques of dependent elimination.