Anti-unification modulo the declared algebra

Chapter 4 defines the algebraic declarations, and Chapter 10 shows their child representations. This chapter measures their effect on anti-unification. Order and repetition can disappear during term canonization. A declared identity also lets the anti-unifier align collection nodes with different cardinalities.

Order, absorbed by commutativity

The two pairs below differ only in whether their operator is declared commutative:

(sort E)
(function a () E)
(function b () E)
(function Pair (E E) E)
(function PairC (E E) E :comm)

(let ordered_left (Pair (a) (b)))
(let ordered_right (Pair (b) (a)))
(antiunify ordered_left ordered_right :algorithm exact)
(checkau ordered_left ordered_right :max_size 5 :algorithm exact)

(let commutative_left (PairC (a) (b)))
(let commutative_right (PairC (b) (a)))
(antiunify commutative_left commutative_right :algorithm exact)
(checkau commutative_left commutative_right :max_size 3 :algorithm exact)

The order-sensitive pair reports both positional disagreements. The commutative pair was already one canonical e-node before the query:

(anti-unify :size 5 :cr 0.6667 :completion exact
  (Pair (Variants a b) (Variants b a)))
(anti-unify :size 3 :cr 0.0000 :completion exact
  (PairC a b))

Declaring commutativity changes the measured result from size 5 and ratio 0.6667 to size 3 and ratio 0.

Repetition, absorbed by idempotence

The next comparison gives the left operand two copies of a and the right operand two copies of b. Bag preserves those multiplicities, while SetI is idempotent:

(sort E)
(function a () E)
(function b () E)
(function c () E)
(function Bag (E) E :assoc-comm)
(function SetI (E) E :assoc-comm-idem)

(let bag_left (Bag (a) (a) (b)))
(let bag_right (Bag (a) (b) (b)))
(antiunify bag_left bag_right :algorithm exact)
(checkau bag_left bag_right :max_size 5 :algorithm exact)

(let set_left (SetI (a) (a) (b)))
(let set_right (SetI (a) (b) (b)))
(antiunify set_left set_right :algorithm exact)
(checkau set_left set_right :max_size 3 :algorithm exact)

(let changed_left (SetI (a) (b)))
(let changed_right (SetI (a) (c)))
(antiunify changed_left changed_right :algorithm exact)
(checkau changed_left changed_right :max_size 4 :algorithm exact)

The multiset result shares one a and one b, then reports the unmatched copies. Canonization removes the duplicate members from both SetI terms:

(anti-unify :size 5 :cr 0.2500 :completion exact
  (Bag a b (Variants a b)))
(anti-unify :size 3 :cr 0.0000 :completion exact
  (SetI a b))

Idempotence changes the measured result from size 5 and ratio 0.25 to size 3 and ratio 0.

Arity, aligned by an identity element

Order and duplicate removal happen while Semper constructs the operands. Different cardinalities require an additional AU operation: when an AC or ACI operator has an identity, the solver can pad the shorter collection with that identity before aligning children.

The next fixture compares a three-condition conjunction with the same conjunction missing one condition. AndU declares (Lit true) as its identity; AndN has the same ACI properties but no identity:

(sort Formula)
(sort Bucket)
(sort Region)

(function Lit (bool) Formula)
(function AndU (Formula) Formula :assoc-comm-idem :identity (Lit true))
(function AndN (Formula) Formula :assoc-comm-idem)

(function src () Bucket)
(function dst () Bucket)
(function regionOf (Bucket) Region)
(function versioningOn (Bucket) Formula)
(function encrypted (Bucket) Formula)
(function approvedRegion (Region) Formula)

(let fullU
  (AndU
    (versioningOn (src))
    (encrypted (src))
    (approvedRegion (regionOf (dst)))))
(let droppedU
  (AndU
    (versioningOn (src))
    (encrypted (src))))
(antiunify fullU droppedU :algorithm exact)
(checkau fullU droppedU :max_size 10 :algorithm exact)

(let fullN
  (AndN
    (versioningOn (src))
    (encrypted (src))
    (approvedRegion (regionOf (dst)))))
(let droppedN
  (AndN
    (versioningOn (src))
    (encrypted (src))))
(antiunify fullN droppedN :algorithm exact)
(checkau fullN droppedN :max_size 13 :algorithm exact)

The two measured results are:

(anti-unify :size 10 :cr 0.6250 :completion exact
  (AndU
    (versioningOn src)
    (encrypted src)
    (Variants (approvedRegion (regionOf dst)) (Lit true))))
(anti-unify :size 13 :cr 1.0000 :completion exact
  (Variants
    (AndN (versioningOn src) (encrypted src) (approvedRegion (regionOf dst)))
    (AndN (versioningOn src) (encrypted src))))

With the identity, the absent condition is paired with true, while the two shared conditions remain in the skeleton. Without it, the unequal-cardinality nodes have no structural alignment and both conjunctions are generalized whole. Identity padding changes the measured result from size 13 and ratio 1 to size 10 and ratio 0.625.

Where absorption stops

The final query in the repetition fixture compares (SetI a b) with (SetI a c). ACI canonization absorbs order and repetition, but it does not equate b with c:

(anti-unify :size 4 :cr 0.3333 :completion exact
  (SetI a (Variants b c)))

This is a genuine replacement under the declared algebra: a remains shared and the replacement remains visible. A domain equality can still be established by a Chapter 5 rule before the query. Part IV covers cases that require a reviewer rather than another equality.