kraghen

The definition of "basic step", which includes arithmetic on unbounded integers, is suspicious. And I don't see any attempt at establishing an upper bound on the size of coefficients. I wouldn't be surprised if they grow exponentially.

I sometimes wonder if using logarithms would be more appropriate in most cases. Then we can simply add up the numbers as one "would expect".

We could choose the base to be ~2.7048138 such that 1% regular growth corresponds to 1% logarithmic growth. For low percentages they would mostly agree. But +40% would become +34% while -40% would become -51%, thus making the combined effect more apparent.

I work on developing better tools for solving computational geometry problems robustly and efficiently, so I got quite excited when this paper first appeared.

However, while the type theoretic developments based on Abstract Stone Duality is interesting, they mostly ignore the problem of efficiency by simply representing every real number as a Dedekind cut. Thus, it doesn't scale without significant advances in compiling real arithmetic. A problem I'm working on presently, but it might take a few years...

The lost cause I am referring to is deriving a useful relative error bound on evaluating a+b+c. The implied conclusion is not that floating point arithmetic itself is a lost cause, merely that it's a minefield from step one.

Of course, if you move the goalposts and measure the error compared to the magnitude of the largest number it gets significantly more manageable! Such a situation is benign, relatively speaking.

In my primary domain of computational geometry we don't have this luxury as the sign must be correct. Even ordering by magnitude is insufficient then; for example evaluating 2^54 - 2^54 + 2 - 1 using this method gives 0 when it should have been 1 (and incidentally, in this case a simple left associative ordering would have gotten it right so it's not even guaranteed to improve matters -- not that anyone said otherwise, but it's yet another example that extreme caution is warranted).

Eventually you end up with ideas like http://www.cs.cmu.edu/~quake/robust.html. The effort that goes into getting even the sign of a sum of products correct in every case is absurd.

Unfortunately, most of the computational geometry code I see usually involves starting with the naive implementation and when things go awry various tricks like Kahan sums or ordering by magnitude are applied hoping that the problem goes away or becomes sufficiently obscure, but never is there an attempt to clarify the exact numerical requirements of the result. Even expensive industrial software is prone to this and will sometimes crash if you happen to present it with a slightly unusual piece of geometry.

Well, the general case is that there might be a subtraction. In IEEE arithmetic the sum (or difference) of two numbers is guaranteed to be within 1 ulp, which is a very good bound on the relative error. The problem begins when you feed this slightly inaccurate result into some other computation that magnifies the error.

Now, one might have hoped to derive some bound on the relative error of sums with a small number of addends. My point is that already with three terms this is a lost cause.

Of course with extra assumptions on the nature of the input it's possible to state something stronger. In my example of computational geometry this is never the case since unstable arithmetic corresponds to geometric singularities and the real world is never in general position.

I haven't really seen the issue of equality dealt with explicitly, but it appears that you can extract the bounds of the interval implied by a given unum. Essentially, it seems like an alternative to interval arithmetic with potentially tighter bounds and faster computation.

This sounds like unums, a proposed alternative to IEEE floats, where roughly speaking the significand can have variable size thus only boasting as much precision as the accuracy warrants.

It gets even worse: (1 + 2 ^ 53) - 2 ^ 53 evaluates to 0 while 1 + (2 ^ 53 - 2 ^ 53) evaluates to 1 (the correct result), which means that even the operation of adding three floating point numbers has unbounded relative error in the general case.

This is a great source of frustration in computational geometry, where this turns from a quantitative issue to a qualitative one, since if we get the sign of an expression wrong our data structures might no longer reflect the actual topology of the problem.

I have a suspicion that all non-trivial C++ programs contain undefined behaviour (e.g. not checking for or preventing overflow at every arithmetic operation involving signed integers), so trying to understand the semantics of these programs is kind of a moot point.

On the other hand, if anyone tried to formalise the semantics of C++ and prove some kind of soundness theorem they would probably find that the language definition is technically inconsistent.

Paraphrasing Feynman, if you think you understand C++ then you don't understand C++.

One important aspect of programming with functors is the ability to quantify over them, i.e. higher-kinded types. This is crucial for building reusable components on the functor-level of abstraction.

In modern OOP this would amount to quantifying over interfaces which is typically not even possible in those languages.

The C++17 equivalent would be something like the following (not tested):

  using NumberExpr = int;
  using VarExpr = std::string;
  struct AddExpr;

  using Expr = std::variant<NumberExpr, AddExpr, VarExpr>;

  struct AddExpr {
    std::unique_ptr<Expr> a;
    std::unique_ptr<Expr> b;
  }

Of course, this being C++, you need forward declarations and a firm grasp of the rules of incomplete types to be confident about declaring a simple AST type.

CMOV introduces a data dependency. Predictable branches, on the other hand, are basically free.

It's only described in my thesis, which is not yet publicly available. (It should be, but the university thesis publication process seems to have a latency measured in years...)

The case for triangle joins is simple to describe, though. Suppose we have attributes A, B and C and finite maps (relations) R : A x B -> X, S : A x C -> Y and T : B x C -> Z. Now build tries for each so we have

abx : Trie A (Trie B X)

acy : Trie A (Trie C Y)

bcz : Trie B (Trie C Z)

We can join two tries using join : Trie k v1 -> Trie k v2 -> (v1 -> v2 -> v) -> Trie k v. Putting this all together we have:

triangleJoin : Trie A (Trie B (Trie C (X, Y, Z)))

triangleJoin = join abx acy (\bx cy -> join bx bcz (\x cz -> join cy cz (\y z -> (x, y, z))))

Compared to a database that doesn't know how to handle triangle joins the difference is absolutely stunning. The above one-liner managed to do in 5 seconds what took MySQL over an hour...

Sorry, I was being imprecise. By conventional I meant comparison-based sorting functions that are polymorphic in the element type and thus not allowed to examine individual bytes.

Multikey Quicksort indeed looks like a special case of discrimination, exploiting some of the same principles.

Are you saying that you can sort strings in O(n log n + D) using a conventional sorting algorithm such as merge sort? If so, I don't understand why D would be an additive factor implying that each string is only involved in a constant number of comparisons.

(I wasn't, by the way, only considering strings when discussing variable sized keys -- the beauty of discrimination is that we essentially reduce all sorting problems to string sorting.)

Discrimination runs in linear time not in the number of items but in the total size of the data. If you have n items each of size k it takes O(kn). Conventional sorting often assumes that you can compare keys of size k in constant time and therefore gets O(n lg n) but a more honest analysis would yield O(kn log n) for (say) merge sort.

It might, I never really discussed this aspect with Fritz! For my thesis I was mostly focussed on applications to database queries, and I never encountered any concrete examples of orderings that couldn't be dealt with in an obvious way using discrimination based sorting.

I can't say I have had much success explaining my thesis clearly to anyone except people from the same department, but I can try to give my understanding of discrimination from an implementor's perspective.

The succinct version is that all (discrete) data can be serialised as bit strings and those bit strings can be sorted in linear time by (say) radix sort.

There are two ideas at work here: that all (discrete) data structures ultimately are composed of primitive types that can be sorted in linear time, and that we should only examine each primitive value once.

However, to be fair it should be mentioned that the analysis uses a different machine model (the RAM model) than is usually employed in sorting (where all comparisons are considered to take constant time, which is arguably an inferior model of real computers if you are sorting e.g. strings of variable length).

To be honest, though, the original paper is so well-written that I have a hard time explaining it better.

All orderings must be specified as a reduction to a primitive order using the fact that if you have an equivalence relation on some type A and a reduction f : B -> A then you have an equivalence on B defined by x = y when f(x) = f(y).

Now, take the rational numbers. For the usual binary comparison we can simply define (a/b) < (c/d) as ad < cb. It's not obvious how to express this as a reduction to a primitive ordering (the answer is to compute the continued fraction).

In fact, I'm not aware of any systematic way of deriving discrimination-suitable orderings from binary predicates -- it might be an open research problem, as far as I am aware.

I'm happy to see this excellent paper mentioned. Fritz Henglein (the author) was my thesis supervisor last year, and I worked on developing some of his ideas further.

In particular, I generalised discrimination (and added a touch of linear algebra) to devise a simple multi-way join algorithm that computes the join of any number of relations in optimal time (in a specific technical sense). Such results have been obtained recently, but only with far more complicated algorithms.

Alas, the fully general proof of optimality eludes us, so nothing has been published yet.