tag:blogger.com,1999:blog-11295132.post6558089432442147035..comments2014-10-20T08:43:52.658-07:00Comments on A Neighborhood of Infinity: Constructing Intermediate ValuesDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger9125tag:blogger.com,1999:blog-11295132.post-46534489949741675962011-05-01T09:22:17.599-07:002011-05-01T09:22:17.599-07:00Alexey,
ivt3 g works as g is monotonically increa...Alexey,<br /><br />ivt3 g works as g is monotonically increasing. I should move that sentence earlier because, as you point out, it leads people to expect failure.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-65469430556175416422011-05-01T08:58:30.842-07:002011-05-01T08:58:30.842-07:00Um, ivt3 g produced 0.5 as expected when I ran you...Um, ivt3 g produced 0.5 as expected when I ran your code just now. What problem did you actually have in mind?Alexeyhttp://www.blogger.com/profile/11095629814500390449noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-48814474251929174722010-08-20T08:05:13.738-07:002010-08-20T08:05:13.738-07:00My paper "A lambda calculus for real analysis...My paper "A lambda calculus for real analysis" has at last appeared in the Journal of Logic and Analysis, vol 2, no 5.Paul Taylorhttp://www.PaulTaylor.EU/ASD/lamcranoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-18168101814746986002010-05-30T14:07:08.374-07:002010-05-30T14:07:08.374-07:00@Andrej,
I tried implementing all the usual arith...@Andrej,<br /><br />I tried implementing all the usual arithmetic operations for exact reals a while back. There were a lot of deltas and epsilons to keep track of. The main conclusion I came to was that I'd rather write this kind of code in cooperation with a theorem checker.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-26262184866437860702010-05-30T08:40:46.082-07:002010-05-30T08:40:46.082-07:00To amplify Andrej's comment, the paper has bee...To amplify Andrej's comment, the paper has been revised a lot, and in particular now contains a version of the IVT with the samer generality as the classical theorem (but a different formulation of the result) and a sketch proof of (essentially) the Brouwer fixed point theorem in R^n.Paul Taylorhttp://www.PaulTaylor.EU/ASD/lamcranoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-52665632881893245502010-05-30T06:30:43.220-07:002010-05-30T06:30:43.220-07:00Excellent! So are you going to implement Theorem 1...Excellent! So are you going to implement Theorem 14.15 from <a href="http://www.paultaylor.eu/ASD/lamcra/asdivt" rel="nofollow">Paul's paper</a> for us? That would be cool.Andrej Bauerhttp://www.blogger.com/profile/17920316604280193336noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-88081640352732112982010-05-29T16:38:41.184-07:002010-05-29T16:38:41.184-07:00Put in replacement code. This code hasn't been...Put in replacement code. This code hasn't been tested much so I may have to update it. Thanks for pointing out the problem.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-17628231743934850502010-05-29T16:14:00.861-07:002010-05-29T16:14:00.861-07:00Oops. That's the non-working version of those ...Oops. That's the non-working version of those functions from a draft when I wanted to talk about problems with implementing those functions! Trouble with rcs. Let me sort it out...sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-10086659796546912902010-05-29T16:09:34.388-07:002010-05-29T16:09:34.388-07:00The Eq and Ord instances seem of. They don't e...The Eq and Ord instances seem of. They don't even use the delta and they make strong assumptions about the representation of the numbers (two numbers are inequal when their ith aproximation differ - even when the difference is less than delta)Anonymousnoreply@blogger.com