Skip to content

Sums are not canonical: like-term matching cannot pair a term with its scaled or negated form (282/1728 associativity triples differ) #468

Description

@petlenz

Sums do not canonicalize: 282 of 1728 triples over a 12-term corpus produce structurally unequal expressions depending only on how the sum is associated. All results are value-correct — this is canonical form, not arithmetic. Measured during #411 (2026-09-17).

Two root causes, neither of which is merge_add's reverse-probe hygiene (the part #411 names):

1. n_ary_tree::like_term_of's cross-type branch is dead code. Its final line implements exactly "c*T is a like term of T", but an early hash guard rejects the pair before reaching it, and the two hashes differ by construction (hash(x) = 2654435889, hash(2*x) = 173676443751). So find_like can never pair a bare term with its scaled form. x + 2x → 3x works only through the type dispatchers, and inside merge_add it does not: (x+y) + (2x+y) → x + 2*x + 2*y.

2. A negated term never merges with a scaled one, with no adds involved at all:

-x + 2x   ->  2*x-x       (expected x)
-x + -2x  ->  -2*x-x      (expected -3x)

Both fixes are blocked on a design decision:

merge_add is shared (functions.h) and used by the tensor add simplifier too, so cause 1 applies in every domain.

Related: #414 (negative-of-add children are opaque) is the same canonicalization family; #379 (canonical form + hash-consing) is where this ultimately belongs, and #453 records why the lossy-hash/identity conflation must be resolved before interning.

Signed-off-by: petlenz peterlenz89.pl@gmail.com

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions