vaelii.impl.rewrite — com.vaelii/vaelii 0.29.0

The pure term algebra of schematic equational rewriting: Knuth-Bendix orientation, one-way matching, normalization of argument terms, and critical-pair detection. It takes the oriented rules as data and reads no store, taxonomy or belief, and it requires only vaelii.impl.sentex. See docs/equational.md.

equality-relations clj

The equality relations, whose argument positions are mentions: (equals A B) relates two names and uses neither as a term. normalize-sentence and rule-applies? leave those positions as written, at any depth. Normalizing them would restate what the sentence says: under (equals (fatherOf (fatherOf ?x)) (grandfather_of ?x)), the denial (not (equals (fatherOf (fatherOf Tom)) (grandfather_of Tom))) would become (not (equals (grandfather_of Tom) (grandfather_of Tom))), a denial of reflexivity. Ground congruence reads the same set (res/equality-mention-heads is this var), and kb/equality-predicates mirrors it.

kbo> clj

(kbo> s t)

The Knuth-Bendix order with unit weights: is s ≻ t? The variable condition must hold; then the heavier side wins; an equal-weight pair is decided by the precedence on the two roots (a constant's root is itself), and same-root compounds by a lexicographic comparison of the arguments. A constant against a same-named nullary compound (c vs (c)) is incomparable.

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, as {:with <other handle> :form-a t :form-b t}. all-rules, new-rule included, is the 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. An equality relation's arguments are not rewritten, at the top or nested (equality-relations). A no-op when rules is empty.

orient clj

(orient l r)

Orient (equals l r) into a terminating rewrite [big small] by kbo>, or nil when the sides are KBO-incomparable: a permutative equation such as (rel ?x ?y) = (rel ?y ?x), or one whose variable condition fails both ways.

rule-applies? clj

(rule-applies? rule sentence)

Does the oriented rule {:lhs …} rewrite some argument subterm of sentence? Asked at exactly the positions normalize reduces at (rewritable-subterms, outside the equality-relations arguments), so a rule justifies only the twins it rewrote.

schematic-equation? clj

(schematic-equation? sentence)

Is sentence a schematic equational rule: an (equals L R) with a compound side and a variable? A ground (equals (F a) (F b)) is not one; it reifies to symbols (docs/nat.md). A compound sameAs is refused by wff, and a compound rewriteOf is a NAT declaration.

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, (grandfather_of ?x) is 2.