The Symbolic Layer¶

Modules: symbolic-core, symbolic-minus, symbolic-pow, symbolic-integers, diff · Prerequisite: an arithmetic substrate

Term simplification and symbolic differentiation, purely inside the reasoning engine. As with arithmetic, there is no computer-algebra code in the C++ core: terms are ordinary graph structure, rewrite rules are ordinary forward-chaining rules, and every simplified form and every derivative arrives as an ordinary fact carrying its derivation (⇐).

The import order matters — the &-literals in these scripts are parsed by the loaded zelph/number at import time — but math takes care of it.

zelph> .import math
zelph+> x ~ symvar
zelph> ? (x * x) diffby x
Answer: ((x * x) diffby x) = (x + x)

The derivative was not computed by a differentiation routine; it was derived, the same way Berlin is located in Europe follows from a transitivity rule — and like every derived fact, it persists.

Terms Are Graph Structure¶

A symbolic term is nothing new. Binary operations use the same predicates as the numeric modules: a symbolic (x + y) and a numeric (&2 + &3) are knowledge about the same + node. Symbolic atoms are named nodes with declared sorts:

x ~ symvar        # variables
c ~ symconst      # opaque base constants

Unary functions have no dedicated fact arity in zelph; they are application facts (exp of x) with the function symbol as a first-class node. This is the meta-rule pattern from Logic and Computation transplanted to function symbols: properties of functions are ordinary facts,

exp inverseof ln
ln inverseof exp

and a single generic rule collapses f(f⁻¹(u)) for all declared pairs. New function symbols work out of the box; undeclared ones simply have no rewrites.

Two exact identities complete the pair: ln 1 rewrites to &0, and exp 0 into &1. The second is indispensable, not merely ornamental: simplification proceeds from the bottom up through the term (a node’s reduced form is constructed exclusively from the normal forms of its children, as detailed in the pipeline below), hence congruence forms exp(ln 1) beginning with the normal form &0 of its child, the inverse-pair rule never sees the ln, and without the second identity exp(ln 1) would stop at (exp of &0).

Numerals – the cons lists generated by the loaded arithmetic module – serve as leaves here, interpreted in their canonical form: <1 0>, which denotes the numeral 1 with a leading zero, simplifies to &1, while a list that fails to represent a numeral, such as <x c>, remains its own normal form. The layer operates in a representation-agnostic manner: its &0/&1 leaves are whatever the loaded module builds, which is why the symbolic layer’s own tests (test_symbolic.cpp) are executed against all three arithmetic modules.

Declaring sorts is not optional politeness: an undeclared atom gets no normal form at all, and the request stays silently unanswered. Partiality by absence — silence, never a wrong answer.

The Simplification Core¶

The user-facing idiom mirrors testprime: a request self-fact seeds the work — entered with the self-fact prefix : — and a query retrieves the result repeatably.

zelph+> ? :simplify (x + &0)
Answer: (:simplify (x + &0)) = x

Internally the module follows the arithmetic architecture, with one new stage:

Trigger — the request self-fact (T simplify T) marks the term (needssimp, the needscanon pattern generalised to terms).
Decompose — markers propagate to all subterms.
Base cases – a declared atom stands as its own normal form, a numeral simplifies to its canonical form, and every other list remains its own normal form.
Congruence — once the children are normal, the context-reduced form is built: (T red (P + Q)). Thanks to hash-consing, a term whose children were already normal reduces to itself — a self-fact (T red T).
Rewrite — directed rules on reduced forms produce (T rw S).
Connect — the rewrite result if one exists, otherwise the reduced form itself; exposed under =.

Two design decisions deserve emphasis.

No free commutativity or associativity. Rules exclusively generate new facts, never remove prior ones: allowing free commutation would double every term, and combining associativity with congruence would lead to uncontrolled growth of the term space. Instead, every rewrite rule is directed and measure-reducing, with both orientations of symmetric identities explicitly stated (X + &0 and &0 + X), and the entire system is gated by markers to prevent interaction with numeric facts. Equality saturation within the e-graph framework – essentially, forward chaining over equalities – presents a natural future experiment, not the core principle.

The normal-form contract. It comprises two components. The first mandates that every instance of a rewrite’s right-hand side must be in normal form. A rule meets this requirement if at most the root of the instance is newly introduced: the instance is a subterm of the reduced form, a canonical leaf (a declared atom, a canonical numeral, a negative integer like (neg zint &2)), or a single new node constructed above such elements to which no rule applies. This is why a single bottom-up pass suffices. The second stipulates that simp is single-valued exclusively because, additionally, the rule set is conflict-free: rules that match one reduced form yield the same node. All shipped rules comply with both parts. Rules that break the contract (for example, distributivity) require an iterated design and must not be introduced without careful consideration.

Single-valuedness is verified in addition to being engineered. Rule SU,

(T simp A, T simp B, A != B) => !

reports a second normal form as a contradiction naming both, in every evaluation mode. The default rules do not activate it. What can trigger it comes from outside the shipped rule set: a declared equation, as explained in Knowledge Folding, or an added rewrite rule that meets the first part of the contract yet overlaps a shipped rule with a distinct outcome.

The module’s sole negation – and, since diff contains no negation, the sole one throughout the whole symbolic stack – is the identity fallback: a term whose reduced form undergoes no rewrite takes that reduced form as its normal form – the term itself when its children were already normal,

(T red C, ¬(T rw S)) => (T simp C)

deferred by stratified evaluation until the positive rules — including the entire numeric cascade feeding knowledge folding — have reached quiescence. Fallback results feed parent congruences, which re-open the positive stratum; the alternating schedule makes chains like exp(ln(x + 0)) → x sound across multiple deferred rounds.

Knowledge Folding¶

Constant folding needs no dedicated machinery, because the reduced form is an ordinary +/*// fact: the arithmetic module's triggers fire on it automatically, derive its = result, and one bridge rule adopts it:

(T red C, C = R) => (T rw R)

zelph+> ? :simplify ((&2 + &3) * (&4 + &6))
Answer: (:simplify ((&2 + &3) * (&4 + &6))) = &50

The inner sums fold to &5 and &10; congruence then materialises the fresh fact (&5 * &10) mid-simplification, whose numeric cascade the bridge consumes — the same cross-module mechanism by which multiplication delegates to addition.

The rule deliberately extends beyond constant folding: it consumes any equational fact concerning the reduced form – either computed via arithmetic modules or directly specified – and exclusively in reference to that form. An equation imported from a knowledge graph drives simplification in precisely the same manner as one derived through calculation, as long as it pertains to a reduced form; thus, knowledge and computation stay unified within a single substrate. A declaration regarding a term as written is not consulted when the term fails to be its own reduced form: given ((x + &0) * &2) = c declared, :simplify ((x + &0) * &2) still yields (x * &2), avoiding contradiction; the actual declaration interpreted by the request is (x * &2) = c. The reason is that arithmetic also computes = facts about the term as written, which can be non-canonical – the sum (<1 0> + &0) keeps the leading zero from <1 0> – so reading them would give the term a second normal form. Atoms and eml terms lack a reduced form entirely, so equations about them are likewise ignored. (The ≡ from the polynomial layer does not read declared equations at all.)

Declared equations must satisfy the normal-form contract on their right-hand side. If a declaration concerning the reduced form conflicts with a rewrite, the term acquires a second normal form, and rule SU reports this as a contradiction:

zelph> .import math
zelph+> x ~ symvar
zelph> z ~ symconst
zelph> (x * &1) = z
(x mul &1) ⇐ (x * &1)
zelph> :simplify (x * &1)
(:needssimp (x * &1)) ⇐ (:simplify (x * &1))
(:needssimp x) ⇐ (:needssimp (x * &1))
(:simp x) ⇐ {(:needssimp x) (x ~ symvar)}
(:red (x * &1)) ⇐ {(:needssimp (x * &1)) (:simp x) (:simp &1)}
((x * &1) rw x) ⇐ (:red (x * &1))
((x * &1) rw z) ⇐ {(:red (x * &1)) ((x * &1) = z)}
((x * &1) simp z) ⇐ {(:red (x * &1)) ((x * &1) rw z)}
((x * &1) simp x) ⇐ {(:red (x * &1)) ((x * &1) rw x)}
! ⇐ {(x != z) ((x * &1) simp z) ((x * &1) simp x)}
((:simplify (x * &1)) = z) ⇐ {((x * &1) simp z) (:simplify (x * &1))}
((:simplify (x * &1)) = x) ⇐ {((x * &1) simp x) (:simplify (x * &1))}
Found one or more contradictions!

The same happens when a declaration concerning the reduced form is received after the response was already delivered through the identity fallback, such as (a + b) = c following :simplify (a + b): the engine never retracts the original reply, causing the term to be linked to two answers, and thus SU names both. .semi-naive check further identifies the late declaration as a negation-check failure, because the fallback’s conclusion was derived under a premise that was negated, yet that premise has now come to hold. The declaration and the recorded contradiction remain embedded in the network, which is why each new example starting with .import math initiates a new session.

Confluence with the plain rewrites holds on every overlap, as the numeric results of canonical operands are canonical – addition by construction; subtraction, multiplication, and division through canonnum. Partiality composes: &5 / &0 derives no = fact, fails to match any rewrite rule, and falls back to itself – undefinedness remains apparent rather than collapsing into an incorrect result.

Constant Reassociation¶

The one associativity rule in the module, admitted as an exception:

(T red ((A cons R) * ((B cons S) * U)))     => ((A cons R) * (B cons S))
(T red ((A cons R) * ((B cons S) * U)),
 ((A cons R) * (B cons S)) = K, K != &0)    => (T rw (K * U))

It is present due to iterated differentiation organizing constants through successive layers – the third derivative of x⁵ arrives as 5·(4·(3·x²)) – and while each multiplier is accurate, that does not ensure clarity. It reduces measure (two multiplicative terms consolidate into one), its right-hand side forms a new node to which no rule applies, and both factors are restricted to numerals by pattern, leaving symbolic operands untouched and preventing the generation of spurious facts.

The guard sits on the result: K is &0 exactly when a factor is, which is the case the absorbing rules already answer, and answer differently. symbolic-integers carries the ℤ counterpart.

A declaration can still make a rule apply to the newly introduced node. After declaring (&20 * x) = c, the command :simplify (&20 * x) answers c, yet :simplify (&5 * (&4 * x)) answers (&20 * x): knowledge folding inspects equations concerning the reduced form (&5 * (&4 * x)), not about the node that this rule rewrites it into. Further simplification of that result produces c, and rule SU detects nothing, since each of the two terms possesses a single normal form. The right-hand side remains a normal form solely when no declaration pertains to it.

Definitional Extension¶

An operator may additionally connect to the simplifier through its definition rather than via rewrites. The congruence rule states what a term is, expressed as (T expandsto R) where R is constructed from the normal forms of T's children, and two rules from the core complete the rest:

(T expandsto R) => (R needssimp R)
(T expandsto R, R simp S) => (T simp S)

R is simplified as an ordinary term, and its normal form becomes that of T. A defined term intentionally has no reduced form of its own, ensuring the identity fallback never activates for it: its sole simp is that of R. (A reduced form that rewrites to the normal form of R would let the fallback of T trigger in the same deferred round when R first gets its normal form, before the existence of that rewrite – resulting in two answers.)

The contract for a defined operator: R must not contain the operator itself, and it is built from the normal forms of T's operands. Normal forms therefore never contain a defined operator.

eml is the reference application. The expression eml(x, y) is defined as exp(x) − ln(y), with the identities associated with the EML operator emerging directly from this definition, rather than being established as independent rules:

zelph> .import math
zelph+> .import eml
zelph> x ~ symvar
zelph> ? :simplify (&1 eml &1)
Answer: (:simplify (&1 eml &1)) = e
zelph+> ? :simplify (&1 eml ((&1 eml x) eml &1))
Answer: (:simplify (&1 eml ((&1 eml x) eml &1))) = $( ln(x) )

Operator Modules¶

Each of the following contributes the three parts of the operator extension protocol – decompose, congruence, rewrites – and, when differentiation is relevant, adds two further components: decompose rules that pass the dstate request to their operands, and an assemble rule that builds its derivative from those of its operands. Nothing more than this: no composite needs a constancy rule or an independent shape declaration, and a module introducing a kind of leaf, like symbolic-integers, establishes the constancy of that leaf through a positive rule. eml joins from outside the core, sharing the same decompose phase, but its congruence rule states the operator’s definition instead of a reduced form, and an eml term undergoes no rewrites of its own.

Subtraction and Negation¶

symbolic-minus adds the binary - and unary negation.

zelph+> ? :simplify $( x - 0 )
Answer: (:simplify (x - &0)) = x
zelph+> ? :simplify $( -(-x) )
Answer: (:simplify $( neg(neg(x)) )) = x
zelph+> ? :simplify (&5 - &3)
Answer: (:simplify (&5 - &3)) = &2

neg needs no decompose or congruence rules of its own — (neg of U) is an ordinary application fact, covered by the core's generic (F of U) rules. Its involution needs no rule either: one neg inverseof neg declaration feeds the existing generic inverse-pair rule.

Numeric folding is inherited, not implemented. (&3 - &5) derives nothing over the naturals and falls back to itself — until symbolic-integers is loaded, which completes exactly that partiality.

Cancellation. Every term of the form X - X rewrites to &0, and x - (x - a) reduces to a:

zelph+> y ~ symvar
zelph> ? :simplify (x - x)
Answer: (:simplify (x - x)) = &0
zelph+> ? :simplify (x - (x - y))
Answer: (:simplify (x - (x - y))) = y
zelph+> ? :simplify ((x + y) - (y + x))
Answer: (:simplify $( x + y - (y + x) )) = $( x + y - (y + x) )

Neither rule assigns a second normal form to any term. Regarding X - X, this is valid since each nonnegative integer corresponds to precisely one node (see Integers as Leaves): in every case where knowledge folding also answers X - X, for two equal numerals – whether natural or signed – the result uniformly remains the natural &0. The expression x - (x - a) matches no other rule, and a numeric - fact needs two numerals. X - X compares nodes, not values, thus ((x + y) - (y + x)) remains unchanged: its operands are distinct expressions. Cancelling entire polynomials continues to be the job of the polynomial layer.

Exponentiation¶

symbolic-pow adds ^.

zelph+> ? :simplify $( x^1 )
Answer: (:simplify (x ^ &1)) = x
zelph+> ? :simplify $( x^0 )
Answer: (:simplify (x ^ &0)) = &1
zelph+> ? :simplify (&2 ^ &10)
Answer: (:simplify (&2 ^ &10)) = &1024
zelph+> ? :simplify (x ^ (&1 + &2))
Answer: (:simplify (x ^ (&1 + &2))) = (x ^ &3)

The exponent constitutes a subterm. The expression (U ^ N) breaks down into base and exponent, with the reduced form preserving both, simplified. If the exponent appears as a compound subject to folding, as a numeral written in non-canonical form, or in the zint operand form (pos zint N), it thereby acquires the node corresponding to its canonical spelling, and both the rewrites and numeric folding are applied to it. Differentiation and topoly read the exponent by value and require a natural numeral, except for two inputs that their comparison reads as zero (refer to the details below).

x² and x·x are different nodes. Local rewrites deliberately do not expand powers into products — that would reintroduce the blow-up ^ exists to avoid. Their equality is a statement of the polynomial layer.

The power rule d(uⁿ)/dx = n·uⁿ⁻¹·du/dx applies in this setting too. The exponent-zero case follows a separate rule: because n−1 has no natural value in that instance, the general rule stays silent. An in-system comparison makes the two cases mutually exclusive, thus preserving deriv as a single-valued function. The exponent-zero rule still demands the derivative of the base, even though it does not utilize it: (u ^ &0) constitutes a composite just like any other, implying that an undeclared base like z below leaves it silent. An exponent that is not a numeral fails both comparisons, leading to no derivative for (c ^ x) – silence, not an incorrect &0. Two inputs that are not numerals still qualify as exponent zero: the empty list nil, which resides beyond the arithmetic contract but is interpreted as zero by the comparison, being the exhausted tail of its digit recursion; and a negative signed zero such as (neg zint &0), which the façade compares as &0. The canonical (pos zint &0) stays silent. The case n = 1 needs no special rule: it composes.

zelph+> c ~ symconst
zelph> ? (x ^ &3) diffby x
Answer: ((x ^ &3) diffby x) = $( &3 * x ^ &2 )
zelph+> ? (x ^ &0) diffby x
Answer: ((x ^ &0) diffby x) = &0
zelph+> ? (z ^ &0) diffby x
zelph+> ? (c ^ x) diffby x

Integers as Leaves¶

symbolic-integers makes ℤ numerals first-class symbolic leaves and adds the ℕ → ℤ promotions that complete natural partiality.

zelph+> ? :simplify (x + (pos zint &0))
Answer: (:simplify (x + (pos zint &0))) = x
zelph+> ? :simplify (neg of (pos zint &3))
Answer: (:simplify (neg of (pos zint &3))) = (neg zint &3)
zelph+> ? :simplify (&3 - &5)
Answer: (:simplify (&3 - &5)) = (neg zint &2)
zelph+> ? :simplify ((neg zint &2) - (neg zint &5))
Answer: (:simplify ((neg zint &2) - (neg zint &5))) = &3
zelph+> ? :simplify (&2 + (neg zint &5))
Answer: (:simplify (&2 + (neg zint &5))) = (neg zint &3)
zelph+> ? :simplify (((&0 - &1) * (&0 - &1)) * &1)
Answer: (:simplify $( (&0 - &1) * (&0 - &1) * &1 )) = &1
zelph+> ? :simplify ((neg zint &1) * ((neg zint &1) * x))
Answer: (:simplify ((neg zint &1) * ((neg zint &1) * x))) = x

Numeric folding on ℤ requires no rules in this context: a reduced form over two integer numerals, with at least one being negative, constitutes a standard +/-/* fact, the façade routes it and re-exposes the result under =, lowered to the natural numeral if the result is nonnegative, and the knowledge-folding bridge proceeds with it. This module adds only what the façade cannot – leaf status, constant reassociation across signed factors, negation of numerals, and the promotions.

One world for the nonnegative integers. Each nonnegative value is the natural numeral; a zint term surfaces solely for negative values, expressed as (neg zint N). An explicit (pos zint N) continues to be allowed as input and normalizes to N, in canonical form, at the leaf (and an input (neg zint &0), or any negative zint with magnitude zero, normalizes to &0: zero carries no sign). A zint whose magnitude fails to be a numeral, like (pos zint x), is not a number and stays its own normal form. Zero and one therefore each possess a single node, and the rules defined in symbolic-core for &0 and &1 are the rules for the integer zero and one; this module needs no additional neutral or absorbing rules. With two nodes per value, both rule sets would be applicable to every mixed form, yielding two distinct normal forms.

The single world also enables diff's &0/&1 seeds to function without modification across ℤ coefficients: d((neg zint &3)·x)/dx assembles ((&0 * x) + ((neg zint &3) * &1)), and the core’s identities reduce it to (neg zint &3).

One site preserves (pos zint N) intentionally: the polynomial layer uses it as its coefficient form; topoly generates outputs from this layer, where a constant polynomial is expressed as a zint term: :topoly (x - x) produces (pos zint &0), and :topoly &7 yields (pos zint &7). The exponent in ^ is a subterm just like any other, thus (x ^ (pos zint &2)) simplifies to (x ^ &2).

Division needs no signed rules when handling nonnegative operands. The distinction among floor, truncation, and Euclidean division only arises with negative operands; for nonnegative ones, all three methods yield the same result, and nonnegative integers are treated as naturals. Thus, ((pos zint &7) / (pos zint &2)) simplifies to &3: its operands first normalize to &7 and &2, upon which natural division completes the rest. mod has no rules within the symbolic layer at all, so :simplify (&7 mod &2) remains unresolved, despite the numeric fact (&7 mod &2) = R leading to &1. The façade does not route either / or mod, so a direct fact with a zint operand derives nothing. When either the dividend or the divisor is negative, numeric folding does not occur, a behaviour deliberately left unspecified; in cases where no identity applies, the expression keeps its shape, with only its operands normalized:

zelph+> ? :simplify ((pos zint &7) / (pos zint &2))
Answer: (:simplify ((pos zint &7) / (pos zint &2))) = &3
zelph+> ? :simplify ((neg zint &7) / &2)
Answer: (:simplify ((neg zint &7) / &2)) = ((neg zint &7) / &2)
zelph+> ? :simplify (x ^ (pos zint &2))
Answer: (:simplify (x ^ (pos zint &2))) = (x ^ &2)

Differentiation¶

diff implements sum, product and chain rule as Trigger / Decompose / Assemble / Connect blocks.

zelph+> ? (x * c) diffby x
Answer: ((x * c) diffby x) = c
zelph+> ? ((exp of x) * x) diffby x
Answer: ($( exp(x) * x ) diffby x) = $( exp(x) * x + exp(x) )
zelph+> ? ((ln of x) diffby x)
Answer: ($( ln(x) ) diffby x) = (&1 / x)

Function derivatives are again facts about function symbols (exp hasderivative exp), consumed by one generic chain rule; ln has a dedicated rule because its derivative 1/u is not of the form g(u) for a named symbol.

The raw derivative is deliberately not the exposed result: the connect stage asserts an ordinary :simplify request on it, the core answers that, and the simplified form is exposed under =. That is why d(x + c)/dx answers &1 and not &1 + &0.

Constancy at the Leaves¶

Constancy is declared exclusively at the leaves, each governed by a positive rule:

(X dstate X, X ~ symvar)                       => ((X wrt X) deriv &1)
(T dstate X, X ~ symvar, T ~ symvar, T != X)   => ((T wrt X) deriv &0)
(T dstate X, X ~ symvar, T ~ symconst, T != X) => ((T wrt X) deriv &0)
((A cons R) dstate X, X ~ symvar, (A cons R) isnumeral true)
=> (((A cons R) wrt X) deriv &0)

Each composite, including constant ones, undergoes structural differentiation. The raw derivative of a constant composite is assembled from the &0 values of its leaves, and the simplifier transforms this into &0:

zelph+> ? (c * c) diffby x
Answer: ((c * c) diffby x) = &0
zelph+> ((c * c) wrt x) deriv D
Answer: ((c * c) wrt x) deriv $( &0 * c + c * &0 )

diff contains no negation. The textbook definition – "a term not containing x is constant" – serves as one, and a negation holds validity only to the extent that the positive recursion it evaluates is sound: a structure that the containment test cannot traverse satisfies it merely because nothing could ever derive its containment, and thus would be labelled constant. Stating constancy at the leaves eliminates the issue. Any term possessing a subterm outside the vocabulary – /, a foreign predicate, an undeclared atom, or a list that is not a numeral – fails to yield a derivative, because no rule reaches it:

zelph> ? (x / c) diffby x
zelph+> ? <x c> diffby x
zelph+> ? &5 diffby x
Answer: (&5 diffby x) = &0

Silence, never a wrong answer. Two losses are tolerated: an undeclared function of a constant, (sin of c) lacking a sin hasderivative … fact, and a power with an exponent that is not a numeral, like (c ^ y) differentiated with respect to x, are allowed to remain silent as well.

Numerals undergo validation, not default acceptance as valid. A cons list qualifies as a numeral precisely when it is non-empty, terminates with nil, and each constituent element constitutes a digit based on the currently loaded substrate – specifically, it satisfies (D isdigit true) – the identical criterion the engine evaluates when rendering a list into an &-literal, with the additional requirement of being in canonical form. This validation mechanism is realized within common-arithmetic and only activates when explicitly triggered: a consumer marks a list with (L needsnumeral L) and then checks (L isnumeral true), thus ensuring cons lists remain universally applicable, with no implicit conversion to numerical values unless a specific rule demands it. The diff component requests the check for each list reaching a dstate fact, symbolic-core for every list leaf, symbolic-integers for the magnitude of a zint leaf, topoly for its numeral leaves, and the integer façade for (the magnitude of) each operand of +, -, *, and cmp it routes.

Observe the placement of variables. A dstate fact takes the form (TERM dstate VARIABLE), meaning the rules for the other leaves bind term and variable separately – the self-fact pattern (X dstate X, X ~ symvar) applies solely to a leaf differentiated with respect to itself – and the guard T != X keeps a symbol from simultaneously qualifying as constant with respect to itself. This guard is significant for symconst as well: since sorts are facts, a single symbol may carry both (the polyring declaration in math makes every ring indeterminate a symvar), and when differentiated with respect to such a symbol, it must yield &1 exclusively.

At most one raw derivative per term. Each shape is associated with precisely one rule, ensuring that each term possesses no more than one raw derivative per variable, and the exposed result remains inherently single-valued. Rule DU transforms this into a check:

((T wrt X) deriv A, (T wrt X) deriv B, A != B) => !

A second raw derivative would mean a flaw within the rule set, and it is reported as a contradiction instead of being silently propagated.

Iterated Differentiation¶

(T diffalong <x y>) = E     d/dy (d/dx T), reading order
(T diffalong <x x>) = E     the second derivative
(T diffalong nil)   = T

Four rules, and no new machinery: each step is an ordinary diffby request whose = result feeds the next. A cons list rather than extra objects on the fact, because a zelph fact carries a set of objects — (T d x y) and (T d y x) would be the same node, and order has to live in the data.

Partiality is compositional: if any stage remains silent, the entire sequence becomes silent – possibly in a single order only, because the derivative of ln is a quotient and diff lacks a rule for /, as demonstrated in the final example; when both orders provide answers, they produce the same result and converge to the same node wherever the two simplified expressions match, as illustrated by ((x * x) * y); there, the symmetry of Schwarz/Clairaut arises via node identity rather than being assumed. The simplifier does not enforce normalization of commutativity or associativity, hence the two orders may terminate in different arrangements of the same value, which topoly subsequently establishes as equal:

zelph> .import math
zelph+> <x y> ~ polyring
(:needsring <x y>) ⇐ (<x y> ~ polyring)
zelph+> ? ((x * x) * y) diffalong <x y>
Answer: ($( x * x * y ) diffalong <x y>) = (x + x)
zelph+> ? ((x * x) * y) diffalong <y x>
Answer: ($( x * x * y ) diffalong <y x>) = (x + x)
zelph+> ? ((x * y) * (x + y)) diffalong <x y>
Answer: ($( x * y * (x + y) ) diffalong <x y>) = $( x + y + y + x )
zelph+> ? ((x * y) * (x + y)) diffalong <y x>
Answer: ($( x * y * (x + y) ) diffalong <y x>) = $( x + y + x + y )
zelph+> ? (((x + y) + y) + x) ≡ (((x + y) + x) + y)
Answer: ($( x + y + y + x ) ≡ $( x + y + x + y )) = proven
zelph+> ? (x * (ln of y)) diffalong <x y>
Answer: ($( x * ln(y) ) diffalong <x y>) = (&1 / y)
zelph+> ? (x * (ln of y)) diffalong <y x>

Coexistence with the Numeric Substrate¶

Sharing predicates incurs a deliberate cost: numeric triggers fire on symbolic facts and create internal states like ((x add y) ci 0). These are innocuous – whatever they derive is true, and a symbolic operand never yields an = result – and remain finite per fact. For atoms, digit recursion stalls immediately: one state each for +, -, and *, and for / one seed per digit, keyed by the divisor, plus a dvd state. A numeral operand, however, is traversed: the left factor of *, the dividend in /, and the trial products of a numeral divisor, which run to full completion. Their count increases with the numeral’s length, and the completed multiples table is the one a later numeric division by that numeral reuses. In return, the derivative scaffolding comprises genuine +/* facts whose numeric outcomes appear within the same graph, which is why knowledge folding functions as a one-rule bridge rather than an integration layer.

Scope and Honest Limitations¶

Identities are formal: exp inverseof ln assumes the principal branch and u > 0 over the reals, and &0 / X ignores division by zero. Side conditions are not tracked — declare only directions you accept.

Rewriting operates with a single-pass approach per request: the outcome of a rewrite is not subjected to further processing within the same request, which is why each right-hand side must already be in normal form. A definitional extension does not violate this principle: the right-hand side of a definition is a term of its own, simplified during its own pass, and thus eml reduces eml(1, 1) to e in a single request.

There is no quotient rule, so d(u/v)/dx is silent — an operator extension away, but not shipped.

What is not a limitation of this layer: canonicalisation. Distributivity, the cancellation of terms that are equal only after reordering, and the equality of x² to x·x belong to the polynomial layer, which decides them by construction rather than by rewriting. Attempting to apply a distributivity rewrite here would break the normal-form contract; invoking topoly incurs a single request.

Testing¶

src/test/test_symbolic.cpp executes each scenario across all three arithmetic modules and both parallelism modes, continuously operating in .semi-naive check mode – meaning classic passes are applied to every result, and the re-test of the fallback’s negation is performed for every case. Most assertions are structural (zelph/exists probes on graph nodes): symbolic results are checked as the nodes they are. When the number of answers matters, the tests count the Answer: lines and compare them after normalizing whitespace.

The engine machinery that turned these workloads from intractable into routine — the layered fact-structure lookup, the acceleration stores, and candidate-set anchoring — is documented for contributors in Internals: Performance Architecture.