5 ms·

As long as you’re prepared to wait while the computer tries to figure out which branch to take on "if (a != 0)”, without knowing if it will ever make a decision

As long as you’re prepared to wait while the computer tries to figure out which branch to take on "if (a != 0)”, without knowing if it will ever make a decision =)

michaelochurch 14y ago
Excellent point, but perhaps termination is just a detail. We already know that it's unsolvable. What's the rush? Next you'll be telling me that different polynomials in P matter, like O(n^27) is too slow or at least requires attention to constants and scale. This construction also solves the divide-by-zero problem very elegantly. When we promote Natural Zero to Real, we make sure that it's something like: (1, λ_:Unit. (1/2, λ_:Unit. (1/3, λ...))) This makes division by zero a legal operation (pointwise division of sequences) if we extend our tolerance to sequences without the Cauchy property (and why not? It's just bits).
DanWaterworth 14y ago
The simplest solution to that is not to define equality for the reals.
- pavpanchekha 14y ago
  Sure. But you realize that reals are sometimes equal? Also, comparison is also undecideable, and that's pretty certainly an operation you want to have at times.
  - dragonwriter 14y ago
    Rather than the Cauchy-sequence approach for reals, you could just use a symbolic representation with a standard set of simplification rules, like most Computer Algebra Systems, with resort to floating point approximation for explicit inexact operations (including approximate comparisons). For strict equality, if two reals have the same symbolic simplification, they are equal, otherwise, not. For greater than or less than comparisons (on possibly a "tolerant" form of equality), but if you can't resolve the comparison symbolicly using a set of guaranteed-to-terminate operations, you can resort to calculating floating point approximations of the reals and then comparing those. You might even have "exact" comparison operations that throw an exception if they can't be resolved without resorting to floating point approximations, and "tolerant" comparisons that allow approximations.
    - DanWaterworth 14y ago
      That's not really necessary. If you need approximate comparison/equality, just compare up to a fixed depth. You'll get an answer that is one of: gt, lt, eq or unknown. There are some cases where your system provides better results, comparing two equal irrational numbers for example, but I can't think of a use case for that.
      - dragonwriter 14y ago
        > That's not really necessary. If you need approximate comparison/equality, just compare up to a fixed depth. You'll get an answer that is one of: gt, lt, eq or unknown. I was trying to (provide a user option to) rule out "unknown" as an answer. Though, you can do that with your method, too (with the same kind of risk of error that you'd have with resort to floating point approximation, so in that regard its no worse than my method.) > There are some cases where your system provides better results, comparing two equal irrational numbers for example, but I can't think of a use case for that. I suspect that doing symbolic calculations with a standard set of reduction rules may be more efficient over multiple manipulations involving irrational numbers than manipulating them in lazy Cauchy sequence form, at least when you actually need at some point to do comparisons or numerical approximations (and, certainly, for display, either a more traditional symbolic form or a numerical approximation is going to be preferred to any kind of direct representation of a lazy Cauchy sequence.) But that's just an intuition, and certainly not in an area that I am an expert in.
  - DanWaterworth 14y ago
    > Sure. But you realize that reals are sometimes equal? Of course. > Also, comparison is also undecideable, and that's pretty certainly an operation you want to have at times. Why?

As long as you’re prepared to wait while the computer tries to figure out which branch to take on "if (a != 0)”, without knowing if it will ever make a decision =)

michaelochurch 14y ago

Excellent point, but perhaps termination is just a detail. We already know that it's unsolvable. What's the rush? Next you'll be telling me that different polynomials in P matter, like O(n^27) is too slow or at least requires attention to constants and scale. This construction also solves the divide-by-zero problem very elegantly. When we promote Natural Zero to Real, we make sure that it's something like: (1, λ_:Unit. (1/2, λ_:Unit. (1/3, λ...))) This makes division by zero a legal operation (pointwise division of sequences) if we extend our tolerance to sequences without the Cauchy property (and why not? It's just bits).

DanWaterworth 14y ago

The simplest solution to that is not to define equality for the reals.

pavpanchekha 14y ago
Sure. But you realize that reals are sometimes equal? Also, comparison is also undecideable, and that's pretty certainly an operation you want to have at times.
- dragonwriter 14y ago
  Rather than the Cauchy-sequence approach for reals, you could just use a symbolic representation with a standard set of simplification rules, like most Computer Algebra Systems, with resort to floating point approximation for explicit inexact operations (including approximate comparisons). For strict equality, if two reals have the same symbolic simplification, they are equal, otherwise, not. For greater than or less than comparisons (on possibly a "tolerant" form of equality), but if you can't resolve the comparison symbolicly using a set of guaranteed-to-terminate operations, you can resort to calculating floating point approximations of the reals and then comparing those. You might even have "exact" comparison operations that throw an exception if they can't be resolved without resorting to floating point approximations, and "tolerant" comparisons that allow approximations.
  - DanWaterworth 14y ago
    That's not really necessary. If you need approximate comparison/equality, just compare up to a fixed depth. You'll get an answer that is one of: gt, lt, eq or unknown. There are some cases where your system provides better results, comparing two equal irrational numbers for example, but I can't think of a use case for that.
    - dragonwriter 14y ago
      > That's not really necessary. If you need approximate comparison/equality, just compare up to a fixed depth. You'll get an answer that is one of: gt, lt, eq or unknown. I was trying to (provide a user option to) rule out "unknown" as an answer. Though, you can do that with your method, too (with the same kind of risk of error that you'd have with resort to floating point approximation, so in that regard its no worse than my method.) > There are some cases where your system provides better results, comparing two equal irrational numbers for example, but I can't think of a use case for that. I suspect that doing symbolic calculations with a standard set of reduction rules may be more efficient over multiple manipulations involving irrational numbers than manipulating them in lazy Cauchy sequence form, at least when you actually need at some point to do comparisons or numerical approximations (and, certainly, for display, either a more traditional symbolic form or a numerical approximation is going to be preferred to any kind of direct representation of a lazy Cauchy sequence.) But that's just an intuition, and certainly not in an area that I am an expert in.
- DanWaterworth 14y ago
  > Sure. But you realize that reals are sometimes equal? Of course. > Also, comparison is also undecideable, and that's pretty certainly an operation you want to have at times. Why?