eyeprolog

Relational cube lookup

Can 2000 two-key lookups over 3375 facts stay fast and fully explained?

Data-heavy rule sets spend most of their time looking things up. This example stores a 3375-row table and asks 2000 questions that each bind two of its four columns, so it measures clause indexing as much as logic. The answer is a single “passed”, but its proof and check cover every lookup.

Run it in the playground · Source


The question

A relation here is a table with four columns, relation(A, B, C, Value). A typical query knows the first and third columns and asks whether a matching row exists. Answering 2000 such questions by scanning all 3375 rows each time would mean millions of comparisons. Answering them with an index on the bound arguments is nearly instant.


The data

relation(a0, b0, c0, v0_0).
relation(a0, b31, c1, v0_1).
relation(a0, b62, c2, v0_2).
relation(a0, b93, c3, v0_3).

These are the first 4 of 3375 generated facts: 225 values of A, each paired with 15 values of C, so the table is a 225 × 15 cube with one row per (A, C) pair.


The rules

relation_exists(A, C) :- relation(A, _, C, _).

lookupResult(case, passed) :-
  relation_exists(a0, c0),
  relation_exists(a44, c5),
  relation_exists(a88, c10),
  relation_exists(a132, c0),

relation_exists/2 asks for a row with given first and third columns. The lookupResult/2 rule has 2000 such goals in its body (four are shown); it holds only if every one succeeds.


The answer

eyeprolog examples/relational-cube-lookup.pl
lookupResult(case, passed).
reason(case, "2000 two-key lookups over 3375 facts").

All 2000 lookups succeed. On the CLI the whole run, including parsing 5388 lines of source, takes well under a second, because each call with A and C bound goes straight to candidate rows through the argument indexes.


The reason

eyeprolog --proof examples/relational-cube-lookup.pl
step(relation_exists(a44, c5),
     rule(3376),
     ['A' = a44, 'C' = c5],
     [relation(a44, b903, c5, v44_5)]).
step(relation(a44, b903, c5, v44_5), fact(666), [], []).

Each lookup is justified by one fact, named by its position in the file: a44 with c5 is row 666. The proof has one such pair of steps per lookup, plus the two conclusions.


The check

condition('C1', resolution, ok, 4002).
condition('C4', coverage, ok, 4003).
condition('C7', relevance, ok, 4004).
steps(4002).
verified(4002).
trusted(0).
verdict(checked).

The checker replays all 4002 steps against the program. Every lookup is verified against the exact row it cites, and nothing is trusted.


Try it

Learn more in The Art of EyeProlog, Chapter 13 (clause indexing).