3 ms·

Marshall: Exact real arithmetic based on Dedekind reals

• lmm 14y ago
  Exact real representation is cool but has some serious limitations. You can't (in general) determine whether two numbers are equal (kind of true for regular floating point as well); more problematic is that every time you use a number in a calculation, the result becomes less and less performant.
  • antics 14y ago
    This is not my area of specialty, so correct me if I'm wrong, but isn't it the case that we can determine whether to numbers are inequal? If so, then isn't also the case that your criticism that you can't determine equality is overstated?
    • lmm 14y ago
      We can determine some of the time. You can ask "does a equal b?" and your answer will either be "no" or "maybe" So you can't even say that a number is equal to itself. You can't use it as an index into another datastructure. Doing physics gets hard because you can never say whether two objects have collided. Just about the only thing you can do with these numbers is print them out or plot them on a graph - and you have to discretize to do that - so all it really gives you is a very expensive way to make sure you never lost any precision through all your intermediate calculations.
• mjn 14y ago
  Dedekind-cut formalizations of the reals appear now and then in theorem-proving settings (e.g. Coq provides one), but this is the first implementation I've found in a normal programming language. I was looking for one for pedagogical purposes, hoping for a real-number analog to the ubiquitous Peano-arithmetic examples that you find in SICP and other texts. This is probably a bit too complex for those purposes, especially since it proceeds by first recasting the Dedekind construction in a new formalism rather than the classic set-theoretic definition. But I found it interesting anyway.