Module nary 

Ordered n-ary rule-pattern layer for exact induction.

Generalizes the four fixed 2-body binary topologies to rule patterns over heads of arity >= 1 with bodies of up to max_body_atoms atoms, where every body-atom position binds either a head argument position or a bounded, canonically-numbered existential join variable. The shipped binary engine’s templates are exactly four members of this space at head_arity = 2, two body atoms and one join variable — see canonical_binary_pattern, which is the parity surface the general enumeration is tested against.

This module is deliberately pure host-side: pattern types, canonical-form validation and deterministic enumeration. Scoring the patterns on device is a separate stage that consumes NaryRulePattern values as its rule templates.

Three laws are enforced here rather than documented elsewhere:

• Canonical form (join-variable naming). Join variables are numbered densely in first-appearance order across the body read left to right, so the ENUMERATOR never emits two patterns differing only by join-variable renaming — it does not need to filter them.

  Note the exact scope: canonicality is a property of what enumerate_patterns EMITS, not of the type. NaryRulePattern has public fields, so a caller can hand-build a non-canonical alpha-twin, and the public flatten/score path will score it identically to its canonical form. That is safe (the score is the same), but it means alpha-duplicates are avoided by construction of the generator and REJECTED by NaryRulePattern::validate — not made unrepresentable by the type. Callers assembling patterns by hand own that obligation.

• Canonical form does NOT quotient atom order or multiplicity. H :- A(x),B(x) and H :- B(x),A(x) are distinct members, as are H :- A(x) and H :- A(x),A(x). Semantically identical bodies score identically, tie perfectly in the reduction, can co-occupy top-K, and inflate total_scored. This matches the shipped binary engine, whose ordered (topology, L, R) grid likewise scores both orderings; a sorted-body canonical form would be a behavior change, not a bug fix.

• No silent truncation. The enumeration refuses with a typed error when the pattern space exceeds max_patterns, and when the SEARCH exceeds max_traversal_nodes; it never quietly caps. The two bounds are separate because the first bounds output and the second bounds work — a search that keeps nothing can still be enormous.

Structs

BodyAtomPattern

One body atom: a candidate-relation slot plus its ordered bindings.

NaryEnumerationConfig

Enumeration bounds for one n-ary induction request.

NaryRulePattern

A canonical n-ary rule pattern: H(h0..h{a-1}) :- body....

Enums

PatternVar

A variable slot inside a body-atom binding pattern.

Functions

canonical_binary_pattern

The four shipped binary topologies expressed as n-ary patterns.

enumerate_patterns

Deterministically enumerate every well-formed canonical pattern.