3 · Terms and Rewriting¶

Prerequisites: 2 · Numbers from Nothing.

So far every term was consumed by ≡ and vanished into a normal form. This tutorial works with terms as objects: how they are built, how the simplifier reduces them, and — the payoff — how to teach zelph an operator it has never heard of, in two rules.

A term is graph structure, and sorts are facts¶

No expression type exists. A term is constructed using the same facts as everything else, and its leaves need a declared sort, symvar for an indeterminate, and symconst for an opaque constant:

zelph> .import math
zelph+> x ~ symvar
zelph> c ~ symconst

Binary operations reuse the same predicates as the numeric modules. A symbolic (x + y) and a numeric (&2 + &3) are knowledge about the same + node. That sharing is not an accident; it is what makes constant folding free, as you will see in a moment.

Unary functions are application facts (f of u), with the function symbol as a first-class node. math-syntax writes them f(u) in both directions:

zelph> $( exp(x) ) ~ probe

builds exactly ((exp of x) ~ probe).

Declaring sorts is not politeness. An undeclared atom gets no normal form at all, and the request stays unanswered:

zelph> ? :simplify undeclared
zelph+>

Silence, never a wrong answer — the same discipline as everywhere in the standard library.

The simplifier¶

:simplify T is the request; the answer comes back under =:

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

The last one is worth pausing on. There is no table of function inverses in the engine. There are two facts,

exp inverseof ln
ln inverseof exp

and one generic rule in symbolic-core.zph that consumes them:

(F inverseof G, T red (F of (G of U))) => (T rw U)

Declare a new inverse pair and it collapses too. Declare none, and nothing breaks — an unknown function symbol simply has no rewrites.

The pipeline is bottom-up: mark the term and all its subterms, reduce leaves to themselves, rebuild each node from its already-normal children (the reduced form), apply rewrite rules to that, and expose the result. Because zelph hash-conses, a node whose children were already normal reduces to itself — the machinery notices that for free.

Constant folding without an arithmetic bridge¶

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

No arithmetic was added to the simplifier to make this work. The reduced form of (&2 + &3) is an ordinary + fact, so the arithmetic module's trigger fires on it and derives = &5 — and one bridge rule adopts whatever the graph knows:

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

Then congruence materialises the fresh fact (&5 * &10) mid-simplification, the numeric cascade answers that too, and the bridge fires again.

The rule is intentionally broader than constant folding: it consumes any equational fact concerning the reduced form, and solely that form. An equation imported from a knowledge graph drives simplification in precisely the same way as a computed one, as long as it refers to a reduced form (why). Knowledge and computation are one substrate – this one line marks where that unity ceases to be merely a slogan.

Partiality composes through it unchanged:

zelph+> ? :simplify $( 5 / 0 )
Answer: (:simplify (&5 / &0)) = (&5 / &0)

&5 / &0 derives no = fact, matches no rewrite rule, and falls back to itself. Undefinedness stays visible instead of folding to a wrong value.

Why there is no commutativity rule¶

A forward-chaining engine exclusively introduces facts: no rule has the ability to remove one. A rule (X + Y) => (Y + X) would therefore not normalize anything – it would double the term space, in a way that is irreversible. Associativity combined with congruence would lead to an even more severe outcome.

So every rewrite rule in the standard library is directed and measure-reducing, both orientations of a symmetric identity are spelled out explicitly (X + &0 and &0 + X), and the whole machinery is gated behind markers so it never touches numeric facts.

The contract for anyone adding a rule has two obligations. Every instance of a rewrite’s right-hand side must itself be a normal form: either a subterm within the reduced form, a canonical leaf, or one new node built from such components to which no rule applies. This ensures that a single bottom-up pass is sufficient. And a newly introduced rule must agree with every rule that matches the same reduced form, otherwise the outcome ceases to be uniquely determined: (X / X) → &1 meets the first obligation, yet on input &0 / &0 it overlaps the included rule (&0 / X) → &0, and the request gets two answers, which zelph reports as a contradiction. Distributivity violates the first obligation and is intentionally excluded.

Which raises the obvious question: if the simplifier will not expand products, how was (1+x)(1−x) ≡ 1−x² proven in tutorial 1? It was not proven by rewriting at all. Canonicalisation is the polynomial layer's job, and it reaches it by a different route — see 5 · Inside the Normal Form.

Teaching zelph a new operator¶

Here is the part that a specialised CAS cannot offer.

Take the circle operation of ring theory, x ∘ y = x + y + xy. It is the operation under which the elements of the Jacobson radical form a group, and it is not built into anything.

In a fresh session, begin by providing it with notation – a single call that registers it both with the island grammar and the island printer:

zelph> .import math
zelph+> <x y z> ~ polyring
(:needsring <x y z>) ⇐ (<x y z> ~ polyring)
zelph+> %(math-syntax/operator "circ" 15)

15 is the precedence: between + (10) and * (20). Then give it meaning, in two rules:

zelph> ((U circ V) needstopoly (U circ V)) => (((U + V) + (U * V)) needstopoly ((U + V) + (U * V)))
zelph> ((U circ V) needstopoly (U circ V), ((U + V) + (U * V)) aspoly P) => ((U circ V) aspoly P)

The first rule says: when asked to compile U ∘ V, also ask for its defining term. The second: whatever normal form the defining term reached, adopt it. This is delegation — the pattern eml.zph uses for its whole macro chain — and it is all the polynomial layer needs.

zelph now knows the operation, in your notation:

zelph> ? :topoly $( x circ y )
Answer: (:topoly (x circ y)) = (x poly <(y poly <(pos zint &0) (pos zint &1)>) (y poly <(pos zint &1) (pos zint &1)>)>)

Read the normal form: the x⁰ coefficient is (y poly ⟨0, 1⟩) = y, the x¹ coefficient is (y poly ⟨1, 1⟩) = 1 + y. So x ∘ y = y + x(1 + y) = x + y + xy — which you can also just ask:

zelph+> ? $( x circ y ) ≡ $( x + y + x*y )
Answer: ((x circ y) ≡ $( x + y + x * y )) = proven

And the laws come out as theorems, not assumptions:

zelph+> ? $( (x circ y) circ z ) ≡ $( x circ (y circ z) )
Answer: ($( x circ y circ z ) ≡ (x circ (y circ z))) = proven
zelph+> ? $( x circ y ) ≡ $( y circ x )
Answer: ((x circ y) ≡ (y circ x)) = proven
zelph+> ? $( x circ 0 ) ≡ $( x )
Answer: ((x circ &0) ≡ x) = proven

Associativity, commutativity, and a neutral element — a commutative monoid, verified over ℤ[x, y, z], from three lines you typed into a REPL. Nothing was recompiled and no plug-in interface was involved, because there is no interface: rules about circ are the same kind of object as rules about +.

Notice the first answer: you wrote $( (x circ y) circ z ) and zelph printed $( x circ y circ z ), dropping the parentheses its own precedence declaration makes redundant — and that output parses back to the same node.

One table, two directions

The island grammar and the island display scheme are generated from a single operator table, which is why math-syntax/operator is the way to extend the notation. Registering an operator for display alone — with zelph/set-infix-display on the math-syntax scheme — would let zelph print island syntax its own parser refuses to read.

Word-shaped operators are matched with an identifier boundary, so circ never matches inside circle, and they need surrounding whitespace. Operators sharing a precedence must share an associativity; mixing them is an error rather than a silent choice. Prefix and postfix operators are not user-definable.

Extending the simplifier instead¶

The two rules above taught the polynomial compiler. To teach the simplifier — so that :simplify reduces terms containing your operator — you contribute three things instead: decompose rules that propagate the needssimp marker to subterms, a congruence rule that builds the reduced form, and rewrite rules on reduced forms. symbolic-core's connect stage and identity fallback then work unchanged.

That is the operator extension protocol, and the standard library invokes it three times: for - and unary negation (symbolic-minus), for ^ (symbolic-pow), and for ℤ numerals (symbolic-integers). Each of the three serves as a readable template.

An operator accompanied by a definition may follow a more direct path: the delegation of circ above, applied within the simplifier. Its congruence rule states the definition rather than constructing a reduced form, ((U eml V) expandsto ((exp of P) - (ln of Q))), where P and Q represent the normal forms of the operands, and symbolic-core simplifies the right-hand side as an ordinary term and hands its normal form back. The operator does not require any rewrite rules of its own. This is how eml is introduced, and its identities follow from the definition.

Exercises¶

Declare sq inverseof sqrt and check that :simplify $( sq(sqrt(x)) ) collapses. Then think about what you have actually asserted — for which x is it true? (The standard library calls this out: identities are formal, side conditions are not tracked.)
Teach zelph the operation x ⋄ y = x + y − xy — notation with math-syntax/operator, meaning with the same two-rule delegation — and prove it is associative and commutative with neutral element 0. What is its relation to circ?
Why does ? :simplify $( (x + y) * (x - y) ) not answer x² − y²? Which rule would you have to add, and which contract would it break?
? :simplify $( 0 * (5 / 0) ) — predict the answer before running it.

Next¶

4 · Differentiation puts the term layer to work, and shows how far you can push it with rules of your own.