Canonization and the node kinds
Chapter 4 defines the algebraic declaration contract. This chapter describes the physical child representations selected by those declarations and the canonization pipeline that prepares an e-node for hash-consing.
The five child representations
Each operator selects one of five representations for its children. Literal nodes are a separate leaf kind that carries a concrete value.
| representation | internal kind | stored children | information not represented |
|---|---|---|---|
| ordered tuple | Normal | a fixed-arity tuple in argument order | none |
| unordered pair | Commutative | two class ids in sorted order | argument order |
| sequence | A | a variadic sequence of class ids | selected associative nesting |
| sorted multiset | MSet | class-id and multiplicity pairs | order and nesting |
| sorted set | Set | sorted, distinct class ids | order, nesting, and repetition |
Ordinary operators use ordered tuples. Tuples of up to three children have
dedicated storage, while wider tuples use a pooled slice. :comm selects the
unordered pair. The associative declarations select a sequence,
:assoc-comm selects a multiset, and :assoc-comm-idem selects a set.
The missing information in the last column cannot distinguish two e-nodes. Chapter 4 defines the corresponding equations and Chapter 5 defines how patterns inspect each representation.
The canonization pipeline
Term construction performs these operations before inserting an e-node:
- Replace every child id with its current e-class representative.
- Flatten eligible nested applications of the same variadic operator.
- Normalize the resulting child representation.
- Resolve an empty or singleton variadic result when its declaration permits it.
- Look up the operator and normalized children in the hash-cons table.
Normalization sorts an unordered pair. It preserves sequence order. For a multiset it sorts children, coalesces equal entries, and applies the configured unit, count, and inverse transforms. For a set it sorts and deduplicates children and removes a configured unit. The legality and meaning of those transforms belong to Chapter 4.
(sort E)
(function a () E)
(function b () E)
(function c () E)
;; A binary commutative operator stores a sorted pair. Building the swapped
;; spelling reuses the same node, so both size reports have total 3.
(function eq (E E) E :comm)
(let eq_ab (eq a b))
(print-size)
(let eq_ba (eq b a))
(print-size)
(check-eq eq_ab eq_ba)
Both print-size commands report total: 3. The second spelling replaces its
children by the same representatives, sorts them to the same pair, and finds
the existing eq node.
Ground-term insertion and rewrite right-hand-side evaluation use this same pipeline. The full procedure is specified in design §5.2.
Recanonization during rebuild
A class merge can make a stored child id noncanonical or make two direct children equal. Rebuild revisits affected parents, replaces their direct children with current representatives, and reapplies the representation’s sorting, coalescing, deduplication, unit removal, and multiplicity clamp. A hash-cons collision then triggers the generic congruence merge described in Chapter 6. Recanonization does not cancel inverse pairs. A separate repair round in every rebuild cancels the pairs that later merges form. A coalesced multiplicity past the configured width leaves the node unchanged, and the command or run reports the overflow as an error.
Multisets retain the original multiplicities until the configured clamp runs.
Nilpotent operators therefore remain MSet nodes even at order two. Sets store
no explicit counts because every represented count is one.
Sequence nodes have a narrower rebuild boundary. Rebuild recanonizes the ids
already present in a sequence span, but it cannot enlarge that span when a
child class later acquires a same-operator sequence. Chapter 11 describes the
optional associative inter-reduction work that can add further equalities, and a
rule tagged :flatten matches through such nesting without changing what is
stored (Chapter 5).
The boundary
Canonization normalizes one node under its selected representation. It does not derive consequences that require equations between separate stored nodes. Generic congruence belongs to Chapter 6, domain equations belong to the rules of Chapter 5, and optional completion belongs to Chapter 11.