Date: 2013-12-03
Categories: news; parsing; p3

Implementing algorithms efficiently

I reimplemented the core Earley parser used by P3. The new version of the core Earley parser, earley3, now appears to meet the desired asymptotic worst-case time complexity of O(n^3. ln n). The following are some observations on implementing algorithms so that they achieve a given complexity bound.

The first point to make is that implementing algorithms to achieve a given bound is hard. It is interesting to observe that as the code approaches the worst-case bound, even the slightest imperfections in the code tend to show up as observably-bad performance. It feels as though you are trying to squeeze a big balloon into a small box, and whenever you push on one part of the balloon, in order to get it to fit in the box, another part of the balloon escapes the box. My sense is that implementing algorithms so that they have the correct time complexity is harder than functional correctness, and that formalizing a proof that the implementation meets a given bound is going to be extremely difficult.

With Earley, I spent about a day going through the existing code, identifying invariants, which in this setting include not only functional correctness invariants, but also size invariants and time invariants. For example, an invariant might be: the size of every set in the range of this finite map is O(n) and each set can be accessed (looked up in the map) in time O(ln n). I then thought about the code, and decided that, from a complexity viewpoint, it was too complicated. This is interesting because I normally write code for functional correctness, but it is now clear that correctness in terms of execution time might also influence how the code is written. I then reorganized the code to make the time-cost more transparent, and more aligned to an informal argument I had about why the time complexity should be O(n^3. ln n). The result appears to hit the desired time bound, but I can't help but feel slightly nervous because it took so much effort to get to this point, and I am still not absolutely certain that the code has the correct time complexity.

Of course, one way to be sure is to produce a formal proof that the implementation meets the desired time complexity bound. One barrier to doing this is that informal proofs about time complexity leave out an awful lot of details, and tend to be hard to formalize. Reasoning about time complexity is qualitatively different from the reasoning typically found in functional correctness proofs. I was reading Okasaki's "Purely Functional Data Structures" book recently, where he talks about amortized costs of algorithms, and the Banker's and Physicist's methods. These seem like plausible approaches that could be formalized to give formal guarantees, but my sense is that the task of giving a mechanized proof that an implementation meets a given time bound is still phenomenally difficult. Interesting though!

Update on 2013-12-04: it now appears that the reason previous versions seemed not to hit the time bound was due to GC issues (again!). The current version appears not to hit the time bound, until you fiddle about with various parameters. Also, fiddling about with a central datastructure also seemed to help (although theoretically this was a no-op): I changed a map from pairs of ints to a map from an int to (a map from an int) ie a currying-like change. Anyway, the algorithm is now nicely within the time bound. Rewriting the algorithm allowed me to be absolutely clear about how I thought the algorithm should behave, which in turn made it possible to track down the reason it was not behaving as expected.