RE: Tauchain R&D Analysis and Discussion: Subsumptive tabling beats magic sets.
Really glad that they're hiring, it means Ohad Asor, the lead dev, is likely past the most difficult R+D stages of the project and now top CPP devs have an opportunity to contribute.
I recall Ohad, after only studying this for a few days, reached out to Annie Liu about a possible error in the paper. After a little bit of back and forth, it was concluded that Ohad was indeed correct. To give an indication of how technical it was, this was the passage in question:
The s-demand pattern of the given query p(a1,...,ak) is <p, 1, _, true, s>,
where 1 and _ indicate that the given query can be regarded
as the first (and only) hypothesis of a non-existing rule, and
the ith character of s is ‘b’ if ai is a constant, and ‘f’ otherwise. For each computed s-demand pattern hp, n, r, g, si,
for each rule r2 that defines p, and for each jth hypothesis
h of r2 whose predicate is an IDB predicate, say, q, add an
s-demand pattern hq, j, r2, g2, s2i, if this s-demand pattern
is not subsumed by an s-demand pattern already computed,
where g2 is true iff (i) g is true, (ii) j is 1, and (iii) the ith
character of s2 is ‘b’ if the ith argument of h is a constant,
appears in a hypothesis to the left of h in r, or is an argument of the conclusion of r bound by s; and ‘f’ otherwise.
I'm very much looking forward to what Ohad can do with Tau