zelph 0.9.8
This release makes negation-as-failure sound under forward chaining, completes the rule-based arithmetic system started in 0.9.7, introduces semi-naive (delta-driven) fixpoint evaluation, and ships a primality test written as a textbook logic rule.
Stratified negation-as-failure (bugfix + semantics upgrade)
The problem (all versions ≤ 0.9.7): a negated condition ¬(pattern) succeeds when no matching fact exists — but it was evaluated against the graph state at the moment the rule happened to be scheduled, while other rules were still deriving facts. A rule could therefore fire because a fact had not been derived yet, and since forward chaining is monotonic, the premature deduction could never be retracted. Minimal example:
(A trigger A) => (A step1 A)
(A step1 A) => (A step2 A)
(A trigger A, ¬(A step2 A)) => (A racewin A)
x trigger x
Previous versions derived x racewin x even though x step2 x is derived in the very same run — the outcome depended on internal rule ordering.
The fix: rules whose conditions contain a negation at any nesting depth now form a deferred stratum. The positive rules run to quiescence first; only then are the deferred rules evaluated, against the saturated fact base. Their consequences may feed positive rules, so the two phases alternate until neither derives anything. Soundness rests on monotonicity: new facts can make a negation fail, but never make it newly succeed — a negation that succeeds at a stratum boundary is final. Both evaluation strategies (classic and semi-naive) implement the same schedule, and .semi-naive check verifies their equivalence; the scripts that demonstrated the race are now permanent regression tests (src/test/test_stratified.cpp).
Upgrade note: rule sets that (knowingly or not) relied on a negation firing against un-saturated intermediate state will now produce the stratified — i.e. correct — result. This also benefits the neuro-symbolic generator pattern from 0.9.7 (≈ proposing facts, filtered by ¬(existing fact)): the negation now tests against the saturated graph. Not affected: the SPARQL layer (sparql.zph, including FILTER NOT EXISTS) — it implements query evaluation independently of the rule engine's scheduling and was never subject to this race.
Docs: Stratified Evaluation
Complete rule-based arithmetic
0.9.7 shipped multi-digit addition as a proof of concept. 0.9.8 completes the system — still with no arithmetic code in the C++ core; digits are ordinary nodes, digit tables are ordinary facts, algorithms are ordinary forward-chaining rules:
- Comparison (
cmp) — results are relational facts<,>,==that compose with meta-rules like any declared knowledge (> is transitive) - Subtraction — deliberately a partial function on the naturals:
&5 - &7derives nothing; undefinedness is encoded as absence - Multiplication — schoolbook recursion; LSB-first cons lists make the base shift a single cons, and the accumulation delegates to the addition module through shared facts
- Division & remainder — Euclidean division as the deepest cross-module cascade: candidate products from the multiplication module, differences from subtraction, quotient-digit selection from comparison
- Canonicalization — non-canonical results (leading zeros) are connected to their canonical node: one value, one node, so downstream rules never see two nodes for one number
- Decimal I/O for any internal base —
zelph/set-number-digitsregisters a digit alphabet;&-literals are decimal on input and output, while the internal representation is up to the loaded script
The recursion rules are byte-identical between stdlib/arithmetic.zph (base 10, Janet-generated tables) and stdlib/binary-arithmetic.zph (base 2, hand-written full-adder / full-subtractor / AND-gate truth tables) — the base is a property of the data, not of the rules.
New docs page: Semantic Arithmetic
Prime numbers, twice
Two new stdlib modules answer "is N prime?" on top of the arithmetic stack — contributing no arithmetic of their own:
.import arithmetic # or: .import binary-arithmetic
.import primes-naf # or: .import primes
(&113 testprime &113) = X
Answer: (&113 testprime &113) = prime
primes-naf.zph— the textbook formulation, sound under stratified evaluation:
(N testprime N, &2 < N, ¬(N hasdivisor D)) => (N isprime N)primes.zph— negation-free: a positive fold(N nodivupto D)proves primality one verified non-divisor at a time and simultaneously schedules the search — for composite N the scan halts at the smallest divisor, andhasdivisornames the smallest prime factor
Both use the trial-division square bound (candidates stop at E·E > N) and run unchanged on either base. A single primality test cascades through five rule modules.
Semi-naive (delta-driven) evaluation
New default fixpoint strategy: after one classic pass, every further iteration evaluates rules only against the facts created in the previous iteration — each new fact seeds exactly the rule conditions that could match it, with no scans. Exposed as a command:
.semi-naive on (default) delta-driven evaluation
.semi-naive off classic naive evaluation
.semi-naive check delta-driven, followed by classic verification passes
Results are identical in all modes; the entire test suite runs permanently in check mode, so every test doubles as an equivalence proof between the strategies. The payoff is largest for deeply iterative workloads: multi-digit multiplications run several times faster, with the gap widening super-linearly with operand size.
Other improvements
- Engine: bound-pattern grounding (fully bound structured conditions resolve via a single hash lookup instead of a scan) and a reworked cost-based condition-ordering planner; cardinality scoring now uses size-only lookups instead of copying whole relation extents — significant on Wikidata-scale graphs
- New test suites:
test_seminaive,test_stratified,test_primes,test_node_display - Documentation: new Semantic Arithmetic page; stratified-evaluation section in Logic and Computation
Packages for Linux (AUR, Debian), macOS (Homebrew), and Windows (Chocolatey) as usual — see the Quick Start Guide.