My reasoning engine proved that 114 is prime - a debugging story about negation

zelph> 114 testprime 114 ( 114 isprime 114 ) ⇐ {(¬( 114 hasdivisor D)) ( 114 testprime 114 )}

114 is 2 · 3 · 19. My engine was very confident it's prime. Even better: it printed a proof.

Quick context: I build zelph, an open-source reasoning engine (C++) where everything is one graph - facts, rules, predicates, even numbers. There is no arithmetic code in the engine core: numbers are linked lists of digit nodes, and addition, comparison, multiplication and division are ordinary inference rules that rewrite the graph (how that works).

As a showcase, I wanted a primality test written the way a textbook states it: N is prime if no candidate divides it. In zelph syntax:

(N testprime N, ¬(N hasdivisor D)) => (N isprime N)

¬ is negation-as-failure: the condition succeeds if no matching fact exists. Other rules enumerate divisor candidates and assert (N mod D) facts, which the division module answers. The rule looks correct. It even is correct - as a formula. As a program, it was broken twice.

Bug #1: 114 wasn't even a number

In zelph, 114 without a prefix parses as an atom - a node whose name is "114" - not as a digit list. No arithmetic rule can divide an atom, so no hasdivisor fact could ever exist, so the negation was trivially true, so everything was prime. The classic "your test tests nothing" bug, in logic form.

Fix: number literals are written &114. Moving on - because bug #2 is the one worth a blog post.

Bug #2: a race condition in pure logic

Even with real numbers, the rule kept deriving isprime for composite numbers - sometimes, depending on the order in which rules had been defined. When a bug depends on ordering, I stop debugging the big system and distill. This is the entire bug class in four lines:

(A trigger A) => (A step1 A)
(A step1 A) => (A step2 A)
(A trigger A, ¬(A step2 A)) => (A racewin A)

x trigger x → step2 is always derivable from trigger. So racewin should never fire.

The old engine:

( x step1 x ) ⇐ ( x trigger x )
( x racewin x ) ⇐ {(¬( x step2 x )) ( x trigger x )}
( x step2 x ) ⇐ ( x step1 x )

There it is, in the output order: the negation was evaluated while the answer was still being computed. At that moment x step2 x didn't exist yet, so ¬(...) succeeded, so racewin was derived.

And here's the trap that makes this fatal rather than transient: A forward chainer is monotonic. Facts are only ever added, never retracted. When step2 arrived one inference step later, it was too late - the wrong conclusion was already a fact, with a proof attached, and nothing in the engine's universe could take it back.

For the primality test this meant: isprime(42) raced against dozens of mod computations cascading through many fixpoint iterations. Whoever finished first won.

The scariest part: sometimes it was right

A variation of the probe - same shape, one extra indirection - produced the correct result on my machine. Why? Because the engine iterates its rules from an unordered hash set, and the hash order happened to schedule the fact-producing rule before the negation rule. I've debugged race conditions between threads before. A race condition inside single-threaded logic, decided by unordered_set iteration order, was new to me.

The fix: stratification

The theory has been known since the 1980s (stratified Datalog). My own documentation even claimed zelph had these semantics. The engine just... didn't implement them. Ouch.

The fix:

• Rules whose conditions contain a ¬ (at any nesting depth) form a deferred stratum.
• Phase 1: run all purely positive rules to their fixpoint.
• Phase 2: only then evaluate the deferred rules - against the saturated fact base.
• Their consequences may enable positive rules again, so the phases alternate until neither derives anything.

The soundness argument is one sentence, and I find it satisfying that the villain of this story is also the hero: monotonicity caused the bug (no retraction) and also fixes it - new facts can make a negation fail, but never make it newly succeed. So a negation that succeeds after positive quiescence is final.

The four-line repro and its friends are now permanent regression tests in the suite.

The payoff

zelph> .import arithmetic
zelph> .import primes-naf
zelph> (&113 testprime &113) = X
((&113 testprime &113) = prime) ⇐ {(&113 isprime &113) ...}
zelph> (&42 testprime &42) = X
((&42 testprime &42) = composite) ⇐ {(&42 hasdivisor &2) ...}

The textbook rule, executable as written - with the entire arithmetic underneath (comparison, subtraction, multiplication, Euclidean division with remainder) running as forward-chaining graph rewriting, arbitrary precision included.

One more thing I find mildly beautiful: the standard library also ships a negation-free twin (primes.zph). It proves primality via a positive fold - "no divisor up to D" grows one verified candidate at a time - and the fold doubles as a scheduler: for composite N, the search halts at the smallest divisor. On composites it's roughly 3–4× faster than the eager NAF version; on primes they tie, because both must pay for the full scan up to √N. Same mathematics, two proof strategies - and the proof strategy is the execution strategy.

Takeaways

• Negation-as-failure in a forward chainer is a scheduling problem, not just a semantics footnote. If your engine evaluates ¬ against in-flight state, you have a race - you just haven't lost it yet.
• When a bug depends on iteration order, don't debug the application. Distill it below five lines first; the repro is worth more than the fix, because it becomes the regression test.
• Documentation that describes semantics your code doesn't enforce is a bug report you wrote to yourself in advance.

Release notes for v0.9.8: https://github.com/acrion/zelph/releases/tag/v0.9.8

Try it: brew tap acrion/zelph && brew install zelph · choco install zelph · AUR: zelph

A question for people who've built or used forward-chaining systems (Datalog engines, rule engines, CEP systems): how does yours schedule negation? Static stratification analysis at compile time, runtime deferral like this, well-founded semantics, something else entirely? I chose runtime deferral because zelph's rules quantify over predicates (predicates are graph nodes), which makes static predicate-level stratification too coarse - but I'd genuinely like to hear other approaches.