Re: "Kantor dust"

[Bas Spitters <spitters@cs.ru.nl>]

Let me use this as an excuse to advertise the work of Russell O'Connor, who is
about to complete a PhD in Nijmegen working with me.

O'Connor's project was to implement exact real numbers in type theory in a
machine verified way. His implementation is fairly efficient and completely
verified in the Coq proof assistant.
Real numbers are implemented using (a variant of) Cauchy sequences. He used
the completion monad on metric spaces to write a Haskell-style "effectful"
functional program in Coq (http://arxiv.org/abs/cs/0605058).

He combined the same monad with the list monad to obtain an implementation of
compact sets (pictures, graphs, i.e. Cantor set).
http://arxiv.org/abs/0806.3209

Together we implemented the Riemann integral by combining the step function
monad with the completion monad:
http://arxiv.org/abs/0809.1552

It was very pleasant to see how much category theory pops up naturally when
one tries to implement exact real numbers in a certified way.

To come back to your question: there is a *certified implementation* of
compact sets of the plane. Cantor set is an example of this.
O'Connor's paper includes much more discussion than what I would like to
repeat here. I recommend it.

Bas


On Friday 30 January 2009 08:18:39 Galchin, Vasili wrote:
> [Note from moderator: this may have been sent incorrectly earlier,
> apologies if you have received it twice.]
>
> Dear Category group,
>
>       Here is a definition of Cantor dust ....
> http://en.wikipedia.org/wiki/Cantor_set.
>
>       My question is from a constructivist viewpoint does this set really
> exist and if so, why?
>
> Very kind regards,
>
> Vasili