zlf implements deterministic positive two-level tabling. A tabled predicate’s answers are computed to a fixpoint once, cached in a table, and persisted to RocksDB. Declare tabled predicates at the runtime level (declare_tabled); in the REPL a tabled predicate is one registered as such through the query facade. Left-recursive rules such as transitive closure terminate and produce the complete reachable set.
Tables support selective invalidation: mutating a fact, rule, or table that a table depends on marks it stale and recomputes only the affected tables (with a full-recompute fallback).
zlf provides negation-as-failure (\+/1) with a static stratification guarantee over stored rules:
call/1, once/1, ,/2, ;/2, ->/2) and flipping polarity at each \+.\+/1 and table machinery.p(X) :- \+ q(X).
q(a).
? p(a). % fails (q(a) holds)
? p(b). % succeeds (q(b) absent)
Tabled negation is supported: negating a lower-stratum tabled goal completes that table first, then answers by absence. If the required table is left Evaluating/Failed (e.g. by a prior interrupted run), evaluation errors instead of returning an unsound answer.
q(X) :- edge(X, kind, a).
p(X) :- \+ q(X).
Rules with a non-ground meta-call (p(X) :- call(Y).) are rejected — dynamic dispatch cannot be stratified statically. Query-time call/N is unaffected.
ZlfDatabase::analyze_rules() returns the current strata assignment and any violations read-only, without rejecting writes.