AngouriMath

Navigation

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

AngouriMath.Core.Transformations.Matching

← Back to list of namespaces

Classes within the AngouriMath.Core.Transformations.Matching namespace

• Bindings

  Summary

  A set of named holes and what they stood for.

  Remarks

  A cons list rather than a dictionary, because of how it is used: a handful of holes, and a
  new set built on every step of a backtracking search. Sharing the tail makes
  With(System.String,AngouriMath.Entity) one small object instead of a copy of the whole map, which measured as
  the larger part of what a rule expressed as data cost over the same rule as a
  switch arm.
  Immutability is not an optimisation here but a correctness requirement: a branch that
  fails must leave nothing behind for the branch tried next, and sharing one mutable map
  across attempts is how a matcher silently starts accepting things it should not.
  

• EBindings

  Summary

  The e-graph counterpart of Bindings: a set of named holes, each standing for
  an e-class id rather than an Entity. Same cons-list shape, for the same reason
  -- see Bindings's own remarks -- plus one concrete win it gets for free: a name
  bound twice (x - x -> 0's repeated x) becomes an O(1) class-id comparison
  instead of an Equals(AngouriMath.Entity) call.
  

• MatchedRule

  Summary

  One rewrite rule, addressable on its own: a name, a pattern to match, a side condition,
  what to build, and the tier its claim is justified at.
  

  Remarks

  This is what #825 asks for and what a switch arm cannot be. A rule here can be listed, named in a
  bug report, tested by itself, and — the part that matters most —
  carry its own Soundness. A *set's* tier is the minimum over its arms,
  so one conditional arm drags every unconditional one down with it and every set in the
  registry ends up declaring the same value — which is the honest label for a set and a
  useless one for a rule. A rule declares its own, and unlike the set's it distinguishes:
  both tiers are well populated. No count is repeated here, because a number in a comment
  drifts silently; RuleAuthoringGuideTest measures the live ones and fails when they
  move.
  Where the right-hand side is a pattern too, the rule has two directions rather than
  one.Reversed is the same rule read the other way, and
  Reversal says why a rule has no such reading when it has none. That was
  #746 tier 2's first
  missing piece; it is delivered and it has a production consumer, since
  Saturation.RulesUpTo uses a declared inverse pair to keep the collecting direction
  and withhold the expanding one. Docs/Contributing/ReversibleRules.md is the argument
  for when a reversal is licensed.
  

• MatchedRules

  Summary

  Rule sets written as data, a few at a time and deliberately so: the value of this file is
  that a set expressed here can be checked against the switch that already expresses
  it, so the migration is proven one set at a time rather than asserted wholesale.
  

  Remarks

  MatchedRulesAgreeWithTheSwitchTest is that check. It runs both forms over
  generated expressions and requires them to agree on every one, which is what makes
  replacing the switch a mechanical step rather than a leap.
  PythagoreanIdentity is the exception, and is here for the opposite reason:
  there is nothing for it to agree with. It uses n-ary matching to say something the
  switch has no way of saying, so it is checked against the mathematics rather than
  against the code it would replace.
  Both sides of every rule here are patterns, so thirteen of the fourteen can be read
  backwards — Reversed, and
  Docs/Contributing/ReversibleRules.md for what that requires and what it does not
  claim. The fourteenth is the Pythagorean identity, which cannot, for a reason that is about
  the mathematics rather than about the encoding.
  What it costs to use one of these has been measured end to end, and the first answer
  was wrong about the reason. The first exchange cost about 5% of
  Simplify's time for one set, which was recorded here as the price of the idea
  and as the argument against doing it wholesale. It was not the idea: NodePattern recomputed IsDeterministic on every attempt, walking the
  whole pattern tree behind a delegate before any matching began, so the case that does the
  least work — a rule that does not fire — paid the most for it. Settled once instead, a
  miss goes 29.99 ns → 13.48 ns and a whole pass 1182.9 ns → 659.9 ns at identical
  allocation.
  Re-measured against Simplify itself, three arms in one process with the third a
  second copy of the first, the exchange is inside the noise floor on time — six
  samples each, medians +0.12% apart where the same binary spreads 1.90% — and
  +0.14% on allocation, which is the one figure that reproduces: two copies of the
  same assembly agree to 5 bytes in 45.6 MB. So a set is exchanged when its rules want to
  be data, and the cost is no longer the reason not to.
  

• MatchedRuleSet

  Summary

  An ordered list of MatchedRule, applied first-match-wins over every node —
  the same discipline the switch-based rule sets follow, so that one can be
  exchanged for the other and the two compared.
  

• MatchPattern

  Summary

  The left-hand side of a rewrite rule, as a value rather than as an arm of a
  switch.
  

  Remarks

  #746 v1.0 asks for
  "pattern matching as a data structure, not a switch: matchable, enumerable,
  testable, with commutative and n-ary matching handled by the engine"
  (#248). Three
  things tier 2 wants are blocked on rules not being values: a rule cannot carry its own
  justification tier, a rule cannot be addressed individually
  (#825), and an
  e-graph cannot match against an e-class because there is no pattern to match with.
  Matching enumerates solutions rather than returning one, and that is not a
  refinement — it is what commutativity requires. b*a + c*a has to match
  k*p + k*q with k = a, and a matcher that commits to the first way of
  matching the left operand binds k = b and then fails on the right, in both
  orders of the sum. Only backtracking finds it, so every pattern yields every way it can
  match and the caller takes the first that survives to the end.
  Commutativity over a binary node — a + b matches b + a — is
  Commutative``1(AngouriMath.Core.Transformations.Matching.MatchPattern,AngouriMath.Core.Transformations.Matching.MatchPattern). Matching across a flattened chain, so that a rule about two
  terms finds them among five, is Gathered``1(System.String,AngouriMath.Core.Transformations.Matching.MatchPattern[]): the n-ary half of #248.
  

• RuleReversal

  Summary

  Whether a MatchedRule can be read backwards, and where it cannot, what stops
  it.
  

  Remarks

  Not every rewrite has an inverse worth having, and this says which do.x - x -> 0 is a rewrite nobody wants to read backwards and nobody could: from
  0 there is no recovering which x was cancelled. That is
  ReplacementDropsHoles, and it is a fact about the rule rather than a
  judgement about it.