Comment by michaelochurch | Hacker News Reader

Comment by michaelochurch | Hacker News Reader

We should stop this limited-precision dyadic nonsense and go back to first principles.

    Natural  := Zero | Succ of Natural

    Integer  := Positive of Natural | Negative of Natural
    ## Negative(0) |=> error in constructor

    Rational := {num:Integer, denom:Integer}
    ## denom <= 0 || gcd(num, denom) != 1 |=> error in const.

    Real := (Rational, () => Real)
    ## Lazy Cauchy Sequence-- user is responsible for convergence.

    Complex := {re:Real, im:Real}

    Quaternion := {re: Real, i:Real, j:Real, k:Real}

    Octonion := ... ## NOW we can use FP because octonions   
                    ## are non-associative anyway!

Example usage (still pseudocode):

    $ realMath.sqrt(Positive(Succ(Succ(Zero)))
    -> (Rational{num = Positive(Succ(Succ(Zero))) 
                 denom = Positive(Succ(Zero))},
        #<fn () => Real@f73d>)  ## function produces (3/2, fn)

    ## Of course, with a proper type system, we'd never let sqrt return a Real! Sorry.
    ## It should be List[Complex], like so. 

    $ realMath.sqrt(Negative(Succ(Zero))
    -> Cons(Complex{re = (Rational{num = Positive(Zero),
                                   denom = Positive(Succ(Zero))},
                          #<fn ...>,
                    im = (Rational{num = Negative(Succ(Zero)),
                                   denom = Positive(Succ(Zero))},
                          #<fn ...>)},
            Cons(Complex{...},  ## The other root...
                 Nil))

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 =)

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).

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

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.

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.

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.

> 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.

> 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?

Does there exist a legitimate practical use case for octonions? :)

Quaternions are useful for modeling rotations, which become non-commutative in 3+ dimensions. Octonions? They're connected to certain loops (in the abstract algebra sense... they aren't a real group because of non-associativity) for which I have no idea whether there are real-world applications. Group theory gets some play in cryptography, and loops turn out to be useful in survey design.

More screwy are the sedenions (16 basis vectors) which also have zero divisors (i.e. xy = 0 does not imply x = 0 or y = 0).

If you believe that Lie theory is "pratical," then yes. See John Baez's excellent survey: http://math.ucr.edu/home/baez/octonions/

Reply on news.ycombinator.com