vaelii.impl.rewrite — com.vaelii/vaelii 0.1.0

Symbolic (schematic) equational rewriting — the oriented term-rewriting half of equality, the gap docs/equality.md leaves open.

A schematic equation (equals L R) with variables — (equals (fatherOf (fatherOf ?x)) (grandfatherOf ?x)) — is not a merge of two symbols (that is the partition, docs/equality.md) nor a ground reifiable-NAT compound (that reifies to symbols, docs/nat.md). It is a rewrite rule over a schema: oriented into a terminating reduction L → R, it lets a term be normalized so that a stored (parentChain (fatherOf (fatherOf Tom))) and a query (parentChain (grandfatherOf Tom)) meet at one normal form.

Orientation and termination

An equation is oriented by a reduction order — the Knuth-Bendix order kbo> with unit weights — so rewriting strictly decreases every term at each step and therefore terminates, whatever the rule set and without any confluence/completion argument (orient). The heavier side (by term-size) rewrites to the lighter; an equal-weight pair is oriented by a fixed symbol precedence (root, then lexicographically on the arguments), so a shape like (f (g ?x)) = (g (f ?x)) orients where a size-only rule would refuse it. Both are gated by the variable condition (var-dominates?), which keeps the order stable under every substitution. Only a permutative equation — (rel ?x ?y) = (rel ?y ?x), which no term order can orient — or one whose variable condition fails both ways is refused (orient returns nil).

What normalizes, and what does not

Rewriting applies to terms in argument position — the denoting terms a schematic equation is about — never to a top-level predication (normalize-sentence keeps the sentence's functor and rewrites each argument). fatherOf the function symbol and fatherOf a predicate are the same symbol; protecting the predication is what stops a rule about the term fatherOf(fatherOf(x)) from rewriting a fact that merely happens to share the shape.

This namespace is pure: it takes the oriented rules as data and knows nothing of the store, the taxonomy, or belief. The taxonomy caches the active oriented rules (belief-following, like the equality partition), vaelii.impl.kb threads normalize-sentence into rewrite-term so migration and query both see one normal form, and vaelii.impl.special justifies each rewritten twin — the same belief-following machinery ground congruence already uses. Bottom layer: it requires only vaelii.impl.sentex.

kbo> clj

(kbo> s t)

The Knuth-Bendix order with unit weights: is s ≻ t? A genuine reduction order (stable under substitution and context, well-founded), so a rule l → r with l ≻ r terminates whatever the rule set — the termination guarantee for schematic rewriting.

Decided in order: the variable condition gates it; then the heavier side wins; an equal-weight pair is decided by the root symbol precedence, and same-root by a lexicographic comparison of the arguments. With unit weights term-size is the weight, so this refines the old size-only rule — it agrees on unequal sizes and additionally orients an equal-size pair like (f (g ?x)) vs (g (f ?x)).

match clj

(match pattern subject)

One-way match of pattern (a rule LHS, whose variables may bind) against subject (a term, possibly variable-bearing): the substitution σ of the pattern's variables with (subst pattern σ) = subject, or nil. Only the pattern's variables bind — a variable in the subject is treated as an opaque constant — so a rule never captures a query's variables, and since orientation forbids an RHS variable absent from the LHS, σ binds every variable the RHS will substitute.

non-joining-pairs clj

(non-joining-pairs new-rule all-rules)

The overlaps between new-rule and the other rules in all-rules whose two reducts do not normalize to one form — the non-confluent conflicts worth surfacing. Each entry is {:with <other handle> :form-a t :form-b t}. Self-overlaps are excluded (see the section note). all-rules includes new-rule; it is the whole active set the reducts are normalized against.

normalize clj

(normalize rules term)

The normal form of term under the oriented rules: rewrite innermost subterms to a fixpoint, then the root, repeating until nothing applies. Terminates by the reduction order (each root rewrite strictly decreases size); the guard is a pure safety net.

normalize-sentence clj

(normalize-sentence rules sentence)

Normalize a sentence (pred arg…): rewrite each argument as a term, leaving the predication's functor and shape untouched. A schematic equation is about denoting terms, which live in argument position; a predication is an assertion, not a term. A no-op when rules is empty.

orient clj

(orient l r)

Orient (equals l r) into a terminating rewrite [big small], or nil when no terminating orientation exists. The Knuth-Bendix order (kbo>) decides: the heavier side rewrites to the lighter, and two equal-weight sides are oriented by the symbol precedence — so (f (g ?x)) = (g (f ?x)) now orients, where a size-only rule refused it. nil only when the sides are KBO-incomparable: a permutative equation like (rel ?x ?y) = (rel ?y ?x), which no term order can orient, or one whose variable condition fails in both directions.

rule-applies? clj

(rule-applies? {:keys [lhs]} sentence)

Does the oriented rule {:lhs …} rewrite some argument subterm of sentence? The test for whether a schematic equation justifies a migrated twin — a rule that matches nothing in the sentence contributed nothing to its normal form.

schematic-equation? clj

(schematic-equation? sentence)

Is sentence a schematic equational rule — an (equals L R) whose sides carry a variable-bearing compound? This is the shape that becomes a rewrite rule rather than a partition merge: equals specifically (not sameAs, individuals-only, nor rewriteOf, whose compound form is a NAT declaration), with a compound side and a variable, so a ground (equals (F a) (F b)) — which reifies to symbols — is not one.

term-size clj

(term-size term)

The KBO unit weight of term: the count of symbol / variable / number leaves, functors included. (fatherOf (fatherOf ?x)) is 3, (grandfatherOf ?x) is 2.