AngouriMath

Navigation

Home Quick start Wiki Almanac Research What's new Try Use Angouri.org GitHub Report a bug Donate Contacts

← Back to list of members

CanonicalizationOverGraph

 Method with 2 overloads

• CanonicalizationOverGraph​(AngouriMath.​Core.​Budgets.​WorkBudget,​AngouriMath.​Core.​Transformations.​RewriteRuleGrowth)

  Summary

  Brings an expression to the least of the forms the rules can reach from it, over an
  e-graph — #746 tier 2's "canonicalisation framework built on" the rewrite graph.
  

  Parameter "budget"

  What bounds the search. See EqualitySaturation(AngouriMath.Core.Budgets.WorkBudget,AngouriMath.Core.CostModel).

  Parameter "widest"

  The widest RewriteRuleGrowth admitted, as a ceiling over
  Collects, Rearranges,
  Expands. This is the knob that matters — see the
  measurement below.
  

  Remarks

  How this differs from Canonicalization, which is a rule pass. A
  pass rewrites and commits: having applied a rule it is standing on the result, and if
  recognising an equality needed a larger intermediate form, the pass cannot get
  there and back. A graph does not commit — it holds every form at once and chooses at
  the end — so it can pass through a bigger writing to reach a smaller one.
  That difference is measured, and the measurement says the ceiling matters less than
  it looks. Two rewrite chains run from each of 1458 generated expressions produced
  no divergent pair at all under Collects ∪
  Rearranges: those rules are confluent on that corpus,
  so a pass already reaches the same form a graph would, and over that ceiling this
  earns nothing at all. Widening it barely helps — over six expression pairs equal only
  through a larger intermediate form, Rearranges proved
  two and Expands, all nine expanding rules added, proved
  the same two. Only Unknown — which admits the
  270 rules whose growth nobody judged, against 52 that were — proved a third.
  Why the default is nonetheless the narrow ceiling. Because the widest one is
  where the risk is, not merely where the rules are: the work/egraph harness
  measured a 7,147× blow-up over the undirected rule set — a different mechanism (term
  enumeration, no budget, no pre-filter) on the same question. Six pairs completing
  inside their budget is not evidence against that. So each step up is offered and none
  is assumed, and the caller who takes one is the caller who sets the budget.
  What this is not. Not a canonical form for the language — no such thing
  exists here, since zero-equivalence is undecidable, and
  Docs/Contributing/CanonicalForm.md states that boundary. It is a canonical form
  modulo these rules, this budget, and the answer having settled: equal trees mean
  the rules proved the two expressions equal, different trees mean they did not, and a
  budget that ran out is reported rather than hidden. The run stops once the least
  member of the input's class has survived two passes unchanged, which is the fixed
  point that matters to an extraction and comes where the graph's own may never — on
  a rational coefficient beside a variable the regrouping rules add a member on every
  pass for as long as they are allowed (#1200),
  and the answer was settled on the third. Measured on the corpus and on those inputs,
  no answer moved and the nine of them went from two seconds to milliseconds. Nothing
  in the library calls this — like Canonicalization it is offered, not
  applied.
  

  Remarks

  Built on Canonicalization rather than beside it. The graph does
  not sort a commutative operand pair: the rules that do build their replacement in code,
  so their RewriteRuleGrowth is Unknown and
  no ceiling admits them — measured, by x + y and y + x canonicalising to
  themselves. Nor does it flatten (x + y) + a against x + (y + a), which
  are different trees that print alike. The rule pass does both, is already measured
  idempotent and order-independent, and is not improved by being written again — so it
  runs on each side of the graph step: once so that equal inputs enter the graph as one
  tree, and once so that what extraction rebuilt leaves as one.
  

• CanonicalizationOverGraph​(AngouriMath.​Core.​Budgets.​WorkBudget)

  Summary

  CanonicalizationOverGraph(AngouriMath.Core.Budgets.WorkBudget,AngouriMath.Core.Transformations.RewriteRuleGrowth) over the rules
  that do not expand, which is the ceiling
  EqualitySaturation(AngouriMath.Core.Budgets.WorkBudget,AngouriMath.Core.CostModel) also draws from.
  

  Parameter "budget"

  What bounds the search.