Skip to content

Semantic Arithmetic

zelph performs arithmetic — addition, subtraction, comparison, multiplication and division with remainder of arbitrarily large natural numbers — purely inside its reasoning engine. There is no arithmetic code in the C++ core: digits are ordinary named nodes, numbers are ordinary cons-lists, digit tables are ordinary facts, and the algorithms are ordinary forward-chaining rules. When you type &12 * &34, the engine does not call a multiplication routine; it derives the fact ((&12 * &34) = &408) the same way it derives Berlin is located in Europe from a transitivity rule.

This page describes the complete arithmetic system: the number representation, the shared architecture of the four rule modules, the base-independence property, and the engine machinery — bound-pattern grounding, cost-based condition ordering, semi-naive evaluation — that makes rule-based computation fast enough to be practical. It complements Logic and Computation, which builds up the addition module step by step.

The modules live in the standard library:

Both expose the identical user interface:

zelph> .import arithmetic
zelph> (&128 + &53) = X
((&128  +  &53)  =  &181) ⇐ ...
zelph> &42 cmp &9
(&42  >  &9) ⇐ ...
zelph> (&105 - &98) = X
((&105  -  &98)  =  &7) ⇐ ...
zelph> (&12 * &34) = X
((&12  *  &34)  =  &408) ⇐ ...
zelph> (&17 / &5) = X
((&17 / &5) = &3) ⇐ ...
zelph> (&17 mod &5) = X
((&17 mod &5) = &2 ⇐ ...

Every result arrives with its derivation (⇐). A computation in zelph is not a black box returning a value — it is a set of ordinary facts, each carrying the conditions that produced it.

Numbers Are Graph Structure

A number is a cons-list of digit nodes, stored least-significant digit first: <42> is the structure 2 cons (4 cons nil). Cons cells are relation nodes — triples with cons as the predicate — so a number is nothing but nested statements, the same S-P-O material everything else in zelph is made of (see the Lisp comparison). The LSB-first order is an algorithmic choice: carries and borrows propagate from the least significant digit, so the recursion of every arithmetic rule simply follows the list. It also makes multiplication by the base a single cons: in LSB-first representation, base * X is just (0 cons X) — the "shift" of schoolbook multiplication is free.

The engine core knows exactly one convention about numbers: the & prefix means decimal, on input and on output. Everything else is defined by scripts. On input, the parser turns &42 into the Janet call (zelph/number "42") — a hook each arithmetic script redefines to build its internal representation. The decimal script maps the literal one-to-one onto digit nodes; the binary script converts by pure string arithmetic (so arbitrarily large literals work) into a base-2 list. On output, the script registers its digit alphabet via (zelph/set-number-digits ...); node_to_string then renders any nil-terminated cons-list consisting solely of registered digit nodes as a decimal &-literal — the exact inverse of the input conversion. Any other list keeps the generic <...> display, so cons-lists remain general-purpose and nothing globally reinterprets them.

The consequence: a binary session reads and writes decimal (&5 in, &5 out) while internally computing on <101>. Lists with leading zeros are tolerated as non-canonical values — &105 - &98 internally yields the list <007>, which the &-display normalizes to &7 and which the comparison module treats as equal to <7> by value.

Janet's role ends at load time: it generates the digit tables, a macro-like input-time job (see Scripting with Janet). During inference, only the reasoning engine runs.

The Anatomy of an Arithmetic Module

All four operations — about forty rules in total — follow the same architecture, visible at a glance in the scripts.

Digit knowledge as facts. All single-digit arithmetic lives in lookup tables of ordinary facts. For base 10 they are generated by short Janet loops at load time; the largest is the multiplication table ((a dx b) tci c) pd d / ((a dx b) tci c) mco e, which covers all digit pairs with a running carry c ∈ {0..8} — 1,800 facts, and the carry range is closed since floor((81+8)/10) = 8. For base 2 the tables are written by hand and are recognizable classics: the 16-fact full-adder truth table, the full subtractor, and an AND gate with increment.

Trigger → Decompose → Assemble → Connect. Each module seeds an internal recursion from the user-facing fact:

(N + M) => ((N add M) ci 0)

Decomposition rules then peel the operand lists digit by digit while threading the carry (or borrow) state; assembly rules build the result list bottom-up once the inner subproblem is solved; a final connect rule exposes the result under the user-facing predicate:

(N + M, ((N add M) ci 0) sum T) => ((N + M) = T)

The internal state facts — ((<A> add <B>) ci C) and friends — are themselves ordinary facts: you can query them, and they persist as reusable knowledge. Computing &99 + &1 leaves behind every intermediate carry state, and future computations that reach the same state reuse it instead of re-deriving it.

Table space vs. state space. The digit tables are keyed by dedicated predicates (tci for the carry, tbi for the borrow) that differ from the recursion-state predicates (ci, bi, mci). This schema separation guarantees that table facts are only ever reached through fully bound lookups and never appear in the extensions the recursion rules scan — a design decision that turned out to matter enormously for performance (see below).

Partiality by absence. Subtraction on the naturals is a partial function, and the module encodes this without any error machinery: there is deliberately no base fact for a net borrow (((nil sub nil) bi 1) does not exist), so &5 - &7 simply derives nothing. Absence of a fact encodes undefinedness — the natural failure mode of a monotonic forward-chaining system.

The Four Operations

Addition is the archetype, developed in detail in Logic and Computation: a full-adder cascade over the digit lists, with zero-extension for operands of unequal length.

Comparison (N cmp M) is an LSB-first state machine. Decomposition rules derive an lcmp state for every suffix pair; compute-upward rules then resolve them from the inside out — the more significant rest dominates unless it is eq, in which case the current digit pair decides via the dcmp table. Missing digits of the shorter operand count as 0, so non-canonical lists compare correctly by value. The results are relational facts — N < M, N > M, N == M — which compose with meta-rules like any declared knowledge:

zelph> (R is transitive, A R B, B R C) => (A R C)
zelph> > is transitive
zelph> &30 cmp &20
zelph> &20 cmp &10
( &30  >  &10 ) ⇐ ...

The derived &30 > &10 was never computed digit-wise; it follows from the transitivity meta-rule applied to two computed facts. Computation and reasoning are literally the same operation.

Subtraction mirrors addition with borrow in place of carry — the rule blocks are the structural mirror image — plus the deliberate partiality described above.

Multiplication is schoolbook recursion on the first operand's digits: (A cons R) * M = A*M + base * (R * M), where the base-shift is a free cons. The digit-times-number stage threads a running carry through the dx table. The accumulation stage does something worth pausing on: one rule asserts an ordinary + fact, the addition module derives its = result, and a follow-up rule consumes it. The modules know nothing about each other — they communicate exclusively through the shared fact space. This cross-module cascade is the pattern the whole system scales by: any rule, including user-defined ones, can consume computed results and trigger further computations.

Division (N / M) and remainder (N mod M) complete Euclidean division on the naturals -- and they are the deepest cross-module cascade in the system. The module contributes no digit table of its own: candidate products come from the multiplication module's digit-times-number engine (dmul), candidate differences from the subtraction module, and quotient-digit selection from the comparison module. Its only base-specific data is the digit alphabet itself, stated as facts (0 isdigit true, ...).

Long division looks like the wrong fit for LSB-first lists -- it works on the most significant digit first -- but the representation pays off a third time. For N = (A cons R), i.e. N = A + base*R, the recursion descends into the more significant part R first. If R = QR*M + RR with RR < M, then the current step must solve t = q*M + r for t = A + base*RR -- and in LSB-first representation, t is the cons cell (A cons RR). The "bring down the next digit" step of schoolbook long division is a single cons, just as the base-shift of multiplication was.

The quotient digit is selected without backtracking and without any digit-ordering knowledge, exploiting the fixpoint engine's natural parallelism over candidates: all products q*M are derived up front (shared across all recursion steps -- and, by hash-consing, across every computation involving M), all differences t - q*M are asserted as ordinary - facts, and the unique candidate with t - q*M < M is selected via cmp. Uniqueness is an arithmetic theorem the rules simply inherit: the invariant rem < M bounds t below base*M, so exactly one digit satisfies the constraint. Candidates with q*M > t need no handling at all -- subtraction is partial, their difference facts simply never come into existence.

Partiality composes: division by zero requires no dedicated rule. Every candidate difference equals t by value, t < 0 is unsatisfiable, no quotient digit is ever selected -- &5 / &0 derives nothing, exactly as &5 - &7 derives nothing. Undefinedness remains encoded as absence.

One Rule Set, Any Base

The rule blocks of the decimal and the binary script are byte-identical; only the digit tables (and the input conversion) differ. This is a checked property of the code base, and it makes a satisfying point: the recursion rules are base-agnostic theorems about digit sequences, and the tables are the only place where "ten" or "two" appears. Loading the binary module gives you full adders, full subtractors, and AND gates as facts, with the identical algorithms running on top — a semantic network computing like digital hardware, while reading and writing decimal at the boundary.

Asserting and Querying

&A + &B is an assertion: it states the fact and lets the fixpoint derive everything that follows, including ((&A + &B) = ...). Repeating the same assertion after the fixpoint correctly produces no output — there is nothing new to derive. The repeatable retrieval idiom is the query form with a variable, uniform across all operations:

(&12 + &34) = X
(&42 - &9) = X
(&42 cmp &9) = X
(&12 * &34) = X

Queries are always evaluated; once the result fact exists, they answer from the graph (Answer: ...), repeatably. For cmp, a bridge rule additionally exposes the outcome under = (answering gt, lt, or eq), while the relational facts remain the primary, composable output.

Arbitrary Precision for Free

Because numbers are lists, there is no word size:

zelph> (&3495734893 * &92348793847) = X
((&3495734893  *  &92348793847)  =  &322826900977421603371) ⇐ ...

That is an exact 21-digit result. For comparison, asking the embedded Janet runtime — a full scripting language — for the same product yields 3.22826900977422e+20, a double-precision approximation. The reasoning engine is more precise than the programming language living in the same binary, because structural numbers have no width limit.

Why This Is More Than a Demo

The comparisons in Logic and Computation position zelph relative to Prolog and Datalog, Lean, Gödel numbering, and Lisp. Arithmetic is where those comparisons stop being philosophical.

In Lean, numbers, proofs, and the inference machinery live on different levels; reasoning about the machinery requires stepping up to a meta-level. In zelph there is no meta-level to step up to: the number <42>, the rule that adds it, the fact that records the sum, the derivation that justifies the fact, and a meta-rule quantifying over the predicates involved are all nodes in one graph, processed by one engine. When the multiplication module asserts a + fact for the addition module to answer, object level and meta level have collapsed into plain fact flow.

Where Gödel numbering encodes formulas as numbers to make arithmetic self-referential, zelph runs the arrow in the other direction and makes numbers structural: no encoding, no decoding — the digit list is the number, and it participates in statements directly. And against Datalog: computed facts are indistinguishable from declared ones, predicates are first-class, and therefore arithmetic results feed meta-rules (> is transitive) that standard Datalog cannot even express.

The mid-term goal is a mathematics engine: numeric and symbolic mathematics performed purely by the reasoning engine. The arithmetic modules are the proof of concept for the numeric half. With division and canonicalization complete, the roadmap continues with integers, number-theoretic demos such as the primality module, and then symbolic experiments. The bet behind the symbolic half is exactly the property demonstrated here: because terms, rules, and equations share one substrate, algebraic rewriting is just more rules over the same graph.

From Arithmetic to Number Theory: Primality

The four operations invite a first genuinely number-theoretic question: is N prime? The standard library answers it twice, with two deliberately different designs on top of the same arithmetic modules:

Both load on top of either arithmetic module and expose the same repeatable query idiom:

.import arithmetic            # or: .import binary-arithmetic
.import primes                # or: .import primes-naf
(&113 testprime &113) = X
Answer: (&113 testprime &113) = prime

Both perform trial division with the square bound (candidates stop once EE > N), and the primes modules contribute no arithmetic of their own*: candidate successors are asserted as ordinary + facts, the bound as * and cmp facts, divisibility as mod facts — the arithmetic modules answer them all. A single primality test is the deepest cross-module cascade in the standard library, with division itself internally cascading through multiplication, subtraction, and comparison.

The negation-free version: the fold is the scheduler. "N is prime" is a universally quantified statement — all candidates leave a remainder — which a monotonic engine cannot answer with a single lookup. primes.zph builds the universal from positive facts: a fold (N nodivupto D) grows one verified non-divisor at a time, and the next candidate E = D+1 only comes into existence after D has been verified. The chain that constitutes the proof simultaneously throttles the search: for composite N the recursion halts at the smallest divisor — no work is performed past the verdict, and hasdivisor names exactly one witness, which is necessarily the smallest prime factor.

The NAF version: the definition itself, executable. Under stratified evaluation the textbook formulation is sound as written:

(N testprime N, &2 < N, ¬(N hasdivisor D)) => (N isprime N)

The rule is deferred until the positive rules — the full candidate scan — have reached quiescence, so the negation tests absence against the complete scan. The trade-offs mirror the fold version: enumeration is eager (composites pay the full scan, no early exit), and in return hasdivisor lists all divisors up to the square bound.

Shared properties: 0 and 1 receive no verdict at all — neither prime nor composite, partiality by absence as everywhere in the stdlib. And the verdicts are ordinary relational facts (N isprime N, N hasdivisor D) plus a result bridge under =, so they compose with meta-rules and further computations like any declared knowledge — a computed isprime fact can, for instance, feed a rule that cross-checks Wikidata's prime-number claims.

Making It Fast

Naively, "arithmetic as rules" sounds hopeless: a fixpoint engine re-evaluates rules until nothing new appears, and a single multiplication spawns hundreds of intermediate facts. Three engine mechanisms make it practical — none of them arithmetic-specific.

Bound-pattern grounding. A structured condition subject whose variables are all bound — such as the table lookup ((A d+ B) tci C) once A, B, and C are known — denotes exactly one fact node. The engine resolves it with a single hash lookup instead of any scan; if the denoted fact does not exist, the condition fails immediately. This is what makes the digit tables behave like actual lookup tables even though they are ordinary facts: 1,800 multiplication-table entries, and the engine touches exactly the one it needs.

Cost-based condition ordering. Before evaluating a rule, the engine orders its conditions so that cheap, binding-rich conditions run first and every later condition profits from the accumulated bindings — ideally becoming groundable. The scoring estimates the actual scan each condition would cause (bound anchors, relation cardinalities) rather than guessing from syntax alone.

Semi-naive Evaluation

The engine's default fixpoint strategy is delta-driven. After one classic pass over the whole graph, every further iteration evaluates rules only against the facts created in the previous iteration: for each new fact, the engine looks up which rule conditions could match it, binds that condition directly against the single fact — no scan at all — and evaluates only the remaining conditions of the rule, which, thanks to the fresh bindings, are then mostly direct lookups.

This is a general evaluation strategy, not an arithmetic feature — it is how mature Datalog engines operate. Its payoff is largest for deeply iterative rule systems: workloads with many fixpoint iterations that each add only a few facts while the internal state relations keep growing. Naive evaluation re-scans all of that state in every pass, so its cost per new fact grows as the computation proceeds. Arithmetic recursion is the extreme case of this shape, which is why the effect is dramatic here: multi-digit multiplications run several times faster than under naive evaluation, and the gap widens super-linearly with operand size — a ten-by-eleven-digit binary multiplication completes in seconds semi-naively, while the equivalent naive run had to be aborted after minutes. One-shot workloads that reach their fixpoint in a pass or two — applying a constraint rule once over an imported Wikidata graph, say — see correspondingly less benefit.

The strategy is 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 — check exists to enforce that. After the delta drains, it re-runs classic passes until quiescence and turns any fact the delta path missed into a hard error. The entire zelph test suite runs in check mode permanently, so every test doubles as an equivalence proof between the two evaluation strategies.