From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/81 Path: news.gmane.org!not-for-mail From: Bas Spitters Newsgroups: gmane.science.mathematics.categories Subject: Re: "Kantor dust" Date: Thu, 12 Feb 2009 10:05:10 +0100 Message-ID: Reply-To: Bas Spitters NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1234492900 13304 80.91.229.12 (13 Feb 2009 02:41:40 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 13 Feb 2009 02:41:40 +0000 (UTC) To: "Galchin, Vasili" Original-X-From: categories@mta.ca Fri Feb 13 03:42:54 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1LXo0y-0006Z1-GS for gsmc-categories@m.gmane.org; Fri, 13 Feb 2009 03:42:52 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXnUu-0000Td-EH for categories-list@mta.ca; Thu, 12 Feb 2009 22:09:44 -0400 Content-Disposition: inline Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:81 Archived-At: 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