From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/103 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re Dedekind versus Cauchy reals Date: Sat, 21 Feb 2009 19:17:59 +0100 Message-ID: Reply-To: Thomas Streicher NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1235285799 6475 80.91.229.12 (22 Feb 2009 06:56:39 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 22 Feb 2009 06:56:39 +0000 (UTC) To: Paul Taylor , Original-X-From: categories@mta.ca Sun Feb 22 07:57:55 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 1Lb8Hi-00049z-EG for gsmc-categories@m.gmane.org; Sun, 22 Feb 2009 07:57:54 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lb7kN-00063L-0f for categories-list@mta.ca; Sun, 22 Feb 2009 02:23:27 -0400 Content-Disposition: inline Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:103 Archived-At: Dear Paul and Andrej, I was aware of the fact that locatedness is part of definition of Dedekind cut it guarantees. It guarantees that there are close enough approximations for any required degree of precision. Having had a look at Andrej's slides I can't say that they provided me with an understanding of the operational semantics of the language. The impression I got is that he is using (kind of) interval arithmetic for determining truth values of terms of type \Sigma. That's ok but doesn't answer the question what is a computationally given real number. Do I understand your approach correctly as follows: when given a Dedekind cut as a mapping c : Q -> 2_\bot and an accuracy eps then \exists p,q : Q c(p) = 0 /\ c(q) = 1 /\ q-p < eps is true and computing this truth value gives the witnesses p and q. I.e. one evaluates terms of type \Sigma of the ASD language in a way reminiscent of logic programming. Thomas