AngouriMath

DerivationPath

Summary

How an expression became an answer: an ordered chain of whole expressions, each one the
result of the step before it, from the input to the value that was actually returned.

Remarks

This is what Steps and Derivation are not. Those are the rewrites that fired, across every candidate
Simplify(System.Int32) generated including the ones it discarded, each on the
subexpression it matched. Reading them in order does not walk from the input to the answer.
This does: Steps[i].After == Steps[i + 1].Before holds for every i,
Steps[0].Before is the Input, and the last step lands on the
Result. Compared as expressions, not as printed forms.
The losing candidates are not here. The simplifier explores far more expressions than
it keeps — ExpressionsExplored says how many — and a route through a discarded
candidate is not a route to the answer. They are excluded rather than labelled because a
derivation is read forwards: a reader following the chain from the input needs every entry
to be a step towards the answer, and a marked dead end is something to skip, which is the
same as not being there while costing the reader the skip. What was explored but not taken
is a fact about the search, and it is reported as a count for that reason.
Every step really happened. Each one is an edge the engine actually traversed, with
the expression it started from and the one it produced. Where several recorded routes reach
the answer, the shortest is taken, and ties are settled by the order the engine recorded
them in — so the same input gives the same path.

Example

using AngouriMath;
using AngouriMath.Core.Transformations;
            
foreach (var step in DerivationPath.OfSimplifying("x ^ (-1) / (y / z)")!.Steps)
    Console.WriteLine(step);

DerivationStep

Summary

One whole expression turning into another: the grain a derivation is read at.

Remarks

Not the same thing as RewriteStep, and the difference is the whole point.
A RewriteStep is one rule firing on one subexpression, somewhere in
the middle of a pass; a DerivationStep is a pass, with the entire expression
as it stood before it and as it stood after. The second is what can be chained — the
After of one step is the Before of the next — and the first is
what says which identity was used, which is why the rewrites are carried along in
Rewrites rather than replaced by the pass that contained them.

EGraph

Summary

An e-graph: e-classes over a union-find, e-nodes keyed by operator, child class and
non-default codomain, hash-consed. The codomain is in the key because an e-class is an
equality claim and a codomain is something two unequal entities can differ in.

Remarks

#746 tier 2's e-graph,
moved from the work/egraph measurement harness into the library once the harness had
answered what it was built to answer — see that harness's own report for the measurement
this design rests on.

ENode

Summary

One e-node: an operator, and the e-classes of its children.

EntityOrder

Summary

A total order on expressions, for choosing the representative of a set of equal
ones rather than a nice one.

Remarks

Why this is not a CostModel. A cost model answers "which of these is
nicer" with a Double, and two expressions it cannot separate therefore tie —
which CostModel's own remarks say is common enough to design the models
against. A tie is settled by whichever candidate was reached first, and that is an accident
of traversal rather than a form anybody chose. A canonical form cannot be built on an
accident: it needs exactly one least member, and the same one every run. No
Double can carry a total order on trees, so this is a comparison instead.
Why this is not Entity.SortHash. That key orders the operands within a
commutative chain, which is what RewriteRules.CanonicalOrder and its two siblings
sort by. Choosing between whole expressions that are equal is a different question — the
operands are not siblings, they are rival writings of one value — and a key built to answer
the first is not thereby an answer to the second. The two do not compete: a canonical
extraction under this order still wants its operands sorted by that one.

Explanation

Summary

Turns a rewrite into a sentence, in one place so that a step, a pass and a whole derivation
all say things the same way.

Remarks

#746 tier 2's last
requirement is "transformation metadata rich enough that v5.0 can render a step as a
sentence". This is the check on that claim: metadata is rich enough to render a sentence
exactly when a sentence can be rendered from it, and nothing else settles it.
Every word here comes off a rule. There is no table of phrasings, no per-rule English
written a second time, and no verb chosen by looking at what a rewrite did — which is the
shape this would have taken if the metadata had not been there, and the shape that goes
stale the first time a rule changes. A rule's name is already a clause a person wrote, its
description is already the identity, and the only work is joining them.

RewriteRecording

Summary

Collects the rewrites that fire while it is open, so that an answer can be asked how
it was reached rather than only what it is.

Remarks

Off unless asked for, and off is free: with no recording open, applying a rule set
costs one ambient read more than it did before — per rule set, not per node — and
allocates nothing. That is the condition
#746 puts on
every layer above the tree, and it is why this is a scope rather than a setting that
something might leave on.
Per flow, like Settings: the recording belongs to the call rather
than to the thread running it. It survives an await, and work
started under it — including on another thread — reports to it. A recording opened
inside a task is invisible to that task's siblings and to whatever started it.
Order is not guaranteed once work is parallel. Steps from one flow keep the
order they fired in, but two flows recording into the same open recording interleave
however they happen to run. The single-threaded case — which is what
Simplify(System.Int32) is — is unaffected.
Three views, and they answer different questions.Steps is every
rewrite that fired, on the subexpression it matched, across every candidate
Simplify(System.Int32) generated including the ones that lost.
Derivation is the same list with the normalisation and the repeats taken
out — 270 rewrites down to 5 on x^(-1)/(y/z) — and it is still a *set* of
rewrites, so reading it in order does not walk from the input to the answer.
PathFrom(AngouriMath.Entity,AngouriMath.Entity) is the one that does: whole expressions, in
order, from the input to the value that was returned, with the losing candidates left
out. Ask the first what fired, the second which identities were used, the third how it
got there.

Example

using AngouriMath;
using AngouriMath.Core.Transformations;
            
using var recording = RewriteRecording.Start();
var simplified = ((Entity)"a / (b / c)").Simplify();
foreach (var step in recording.Steps)
    Console.WriteLine(step);

RewriteRule

Summary

One rewrite, addressable on its own: what it matches, what it puts there instead, where it
is written and which way it moves.

Remarks

A RewriteRuleSet is the unit the library applies; this is the unit inside it.
The distinction is what
#28 asks for — a
derivation that says which rewrite fired rather than which group of them — and what
#825 is about.
These are generated from the switch that defines them, arm by arm, rather
than written out a second time. That is deliberate and it is the whole design: the
switch stays the thing a human edits and the thing the simplifier calls, so nothing
on the hot path changes and the two forms cannot drift apart. Transcribing forty arms into
forty objects by hand would be forty chances to alter a pattern silently, and expressing
them through the runtime matcher in
AngouriMath.Core.Transformations.Matching was measured at about five percent of
Simplify(System.Int32) per rule set exchanged.
A per-rule Soundness is here now, and it is empty for most rules on
purpose. This paragraph used to say the tier was absent, on the argument that a rule's
tier is a claim somebody has to argue for and cannot be derived from syntax. That argument
is right and it is not a reason for the property to be missing: where the argument has been made, the claim needs somewhere to live. A rule written as data declares one, and the
two tiers are both well populated — most rules are
Sound — against every set in the registry declaring
SoundUnderAssumptions, so the per-rule tier says
something the per-set one cannot. The live counts are measured by
RuleAuthoringGuideTest rather than quoted here, where they would drift. A rule
read off a switch arm declares nothing, so its Soundness is
null — which says the set's tier is a fallback rather than a measurement,
where silently copying the set's down would have said the opposite.

RewriteRuleGrowth

Summary

Which way a rewrite moves: does it make the expression bigger, smaller, or neither.

Remarks

Counted from what the rule is written as — operators plus operands on the pattern side
against operators plus operands on the replacement side — and therefore a statement about
the rule, not about any particular expression it fires on.
It exists because a rewrite graph needs it and a rewrite pipeline does not.
Simplify(System.Int32) applies a set, keeps a candidate and moves on, so an
expanding rule and a collecting one never meet: the order they run in decides which wins.
Equality saturation deletes that order and keeps both results, so it has to be told which
pairs undo each other or it will grow without bound —
#746 tier 2, measured
in the egraph harness at up to 7,143 times the e-nodes when it is not told.

RewriteRules

Summary

The rewrite rule sets this library ships, as data: named, described, attributed with
what they claim, and enumerable through All.

Remarks

Registration is explicit and static — there is no assembly scanning and no
Activator, so the registry survives trimming and NativeAOT, and
All is in a fixed order that does not depend on hashing, reflection or
which type happened to be loaded first.
Every rule set the simplifier applies is registered here, and the simplifier reaches
them through this registry rather than through Patterns directly. That is what
lets an account of what the simplifier did to an expression be a complete one: a set
reachable only by its method has no name to report and nothing to attribute a step to,
so a derivation built while some sets were still unregistered would quietly omit
whatever they had done.
Every entry is declared SoundUnderAssumptions. That is a claim
about what has been argued, not about what is true — nothing here checks a tier, so
the registry starts conservative and promoting an entry means making the case for it.

RewriteRuleSet

Summary

A named, attributable group of rewrites — the unit this library has always written
them in — carrying what it is called, what it claims and how well justified the
claim is, so that the set can be enumerated, tested and referred to by name instead
of only being called.

Remarks

The set is the unit the library applies; Rules is the unit inside
it. Those rules are generated from the switch that defines the set rather than
written out again, so the switch stays the thing a human edits and the thing
this calls, and the two cannot drift apart. See
#825 and
#746 item 50.

RewriteRuleSetExtensions

Summary

Reading order for ApplyOnce(AngouriMath.Entity).

Remarks

The simplifier applies a dozen rule sets in sequence, and written as calls the
sequence reads inside out. This is the same operation with the expression in front,
so that a pipeline still reads in the order it runs.

RewriteStep

Summary

One rewrite that actually fired: which rule set did it, the subexpression it matched,
and what it put there instead.

Remarks

The subexpression, not the whole expression. A rewrite pass walks the tree bottom-up
and rewrites nodes as it goes, so there is no moment at which a partly-rewritten
whole expression exists to be photographed — reporting one would mean building it,
and it would be a picture of something the engine never held.

Saturation

Summary

Runs rules over an e-graph until nothing more merges or the budget runs out — the shared
half of every transformation built on the rewrite graph.

Remarks

Shared rather than written once per caller because the loop is subtle in ways that are not
visible from a second copy of it: what is charged and when, which rules can be skipped
without an attempt, and which of two matching paths a rule takes. Two transformations
already want it — one extracting the cheapest member of the root class and one extracting
the least — and they differ only in that extraction, not in any of this.

Soundness

Summary

How well justified the relation a Transformation claims between its
input and its output is. The three tiers are never blurred: a heuristic labelled as
a proof is a wrong answer with a friendly face.

Remarks

The tier is declared by whoever wrote the transformation, not derived from it.
Nothing in the library checks a declaration today, so a tier is a claim to be argued
with rather than a guarantee to be relied on, and the registry starts conservative
on purpose: tightening a label needs an argument, loosening one does not.

Transformation

Summary

A named mathematical operation that consumes an Entity and produces
one, together with enough about itself — what it claims, how well justified the
claim is — to be inspected and composed rather than only invoked.

Remarks

This is the layer the 1.x entry points sit on:
Simplify(System.Int32), Expand(System.Int32) and
Factorize(System.Int32) are adapters over the transformations named
below, and the algorithms underneath are unchanged. Callers who only want an answer
should keep using those methods; this type is for callers who want to know which
operation produced it, or to build an operation out of others.
Deterministic: the same transformation applied to the same expression under the same
Settings gives the same result. Composition is by explicit
ordering — there is no registry that decides what to run next, and nothing here
consults reflection, so the layer stays trimmable and AOT-publishable.
Experimental. The three concepts — a transformation, its relation, its
soundness tier — are meant to last; the catalogue of factories will grow and the
signatures here may still move. The stable surface is MathS and the
methods on Entity.

Example

using System;
using AngouriMath;
using AngouriMath.Core.Transformations;
            
Entity expr = "(x + 1) ^ 2";
var result = Transformation.Expansion.Apply(expr);
Console.WriteLine(result.Output);
Console.WriteLine(result.Relation);
Console.WriteLine(result.Soundness);

Prints

1 + 2 * x + x ^ 2
Equivalence
SoundUnderAssumptions

TransformationRelation

Summary

What a Transformation claims about its output relative to its input.
Without this, Soundness would be meaningless: "sound" is only a
statement about some relation, and the relation is not the same one for every
operation.

TransformationResult

Summary

What one application of a Transformation produced: the input, the
output if there was one, and which transformation was asked.

Remarks

A struct, so that routing an ordinary Simplify or Differentiate call
through this layer costs no allocation.

Table of contents

AngouriMath

AngouriMath.Core.Transformations