Skip to content

Commit ebf8475

Browse files
Make the derivation a path from the input to the answer (#28, #273) (#1012)
* Make the derivation a path from the input to the answer (#28, #273) A recording held every rewrite that fired, across every candidate the simplifier generated including the ones that lost, each on the subexpression it matched. Read in order that does not walk from the input to the answer, and the type's own documentation said so in three places. `RewriteRecording.PathFrom(input, result)` walks it. Every step is a whole expression turning into another: `Steps[i].After` is `Steps[i + 1].Before`, the first starts at the input, and the last lands on what `Simplify` returned. `DerivationPath.OfSimplifying(expression)` is the same in one call, and prints as the stages with the identity that produced each one beside it. Two grains in two types, because a rewrite pass walks bottom-up and no partly-rewritten whole expression exists inside one: `DerivationStep` is the pass, and its `Rewrites` are the `RewriteStep`s that fired in it, each naming the rule that did it. What was missing was attribution. A rule-set pass now records what it turned into as well as what it matched, and `Simplificator` records the stages that are not rewrite passes -- inner simplification, the boolean minimiser, the polynomial rearrangement, expansion, factoring -- since the chain otherwise has a hole wherever the simplifier tidies up. Losing candidates are absent rather than marked: nothing leads from one to the answer, so none can be on a path to it, and what the search produced and did not keep is reported as `ExpressionsExplored`. Free when nobody is recording, which is what #746 requires of anything above the tree: one ambient read per stage against a tree walk per stage, and no allocation. `RewriteAllocationTest` guards the new fast path the way it already guarded `ApplyOnce`. `Simplify` returns what it returned before, and the raw recording is unchanged -- 270 rewrites on `x^(-1)/(y/z)`, 251 of them normalisation, measured on both builds. Corrected in passing, each re-measured: `Common` has 100 arms and not 103; `Derivation` on that expression is 5 rewrites and not 6; and `Transformations.md` said a source generator over the switch bodies was still for #746 item 50 to decide, which #951 shipped. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011emtnRT6EWTrxXNtqDVK3e * Say per flow and ambient read, which is what the recording has been since #863 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011emtnRT6EWTrxXNtqDVK3e --------- Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
1 parent d401eed commit ebf8475

8 files changed

Lines changed: 867 additions & 98 deletions

File tree

Lines changed: 188 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,188 @@
1+
//
2+
// Copyright (c) 2019-2026 Angouri.
3+
// AngouriMath is licensed under MIT.
4+
// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.
5+
// Website: https://am.angouri.org.
6+
//
7+
8+
using System;
9+
using System.Collections.Generic;
10+
using System.Text;
11+
12+
namespace AngouriMath.Core.Transformations
13+
{
14+
/// <summary>
15+
/// One whole expression turning into another: the grain a derivation is read at.
16+
/// </summary>
17+
/// <remarks>
18+
/// <para>
19+
/// Not the same thing as <see cref="RewriteStep"/>, and the difference is the whole point.
20+
/// A <see cref="RewriteStep"/> is one rule firing on one <i>subexpression</i>, somewhere in
21+
/// the middle of a pass; a <see cref="DerivationStep"/> is a pass, with the entire expression
22+
/// as it stood before it and as it stood after. The second is what can be chained — the
23+
/// <see cref="After"/> of one step is the <see cref="Before"/> of the next — and the first is
24+
/// what says which identity was used, which is why the rewrites are carried along in
25+
/// <see cref="Rewrites"/> rather than replaced by the pass that contained them.
26+
/// </para>
27+
/// </remarks>
28+
public readonly struct DerivationStep
29+
{
30+
internal DerivationStep(Entity before, Entity after, RewriteRuleSet? ruleSet, string name, IReadOnlyList<RewriteStep> rewrites)
31+
=> (Before, After, RuleSet, Name, Rewrites) = (before, after, ruleSet, name, rewrites);
32+
33+
/// <summary>The whole expression as it stood before this step.</summary>
34+
public Entity Before { get; }
35+
36+
/// <summary>The whole expression as it stood after it. Never equal to <see cref="Before"/>.</summary>
37+
public Entity After { get; }
38+
39+
/// <summary>
40+
/// Which registered rule set did it, where the step is one set applied once —
41+
/// <see langword="null"/> where the step is something else the simplifier does
42+
/// (inner simplification, expansion, factoring, polynomial rearrangement).
43+
/// </summary>
44+
/// <remarks>
45+
/// The same "null where it is not addressable" convention as
46+
/// <see cref="RewriteStep.Rule"/>: a step that is not a rule set has no rule set to
47+
/// name, and saying so is better than inventing one.
48+
/// </remarks>
49+
public RewriteRuleSet? RuleSet { get; }
50+
51+
/// <summary>What did it, named. <see cref="RewriteRuleSet.Name"/> where there is one.</summary>
52+
public string Name { get; }
53+
54+
/// <summary>
55+
/// The individual rewrites that fired inside this step, in the order they fired.
56+
/// </summary>
57+
/// <remarks>
58+
/// Not the same list as <see cref="RuleSet"/> being non-null. A step that is one rule set
59+
/// applied once carries what that set matched; a step that is a chain of them — the
60+
/// tidying pass every stage of the simplifier runs is six — carries everything that fired
61+
/// anywhere inside it, and names no single set. And empty is ordinary: a polynomial
62+
/// rearrangement or an expansion changes the expression without any rule matching.
63+
/// </remarks>
64+
public IReadOnlyList<RewriteStep> Rewrites { get; }
65+
66+
/// <summary>What this step claims about its output, where it is a rule set. See <see cref="RewriteRuleSet.Relation"/>.</summary>
67+
public TransformationRelation? Relation => RuleSet?.Relation;
68+
69+
/// <summary>How well justified that claim is, where it is a rule set. See <see cref="Soundness"/>.</summary>
70+
public Soundness? Soundness => RuleSet?.Soundness;
71+
72+
/// <inheritdoc/>
73+
public override string ToString() => $"{Name}: {Before.Stringize()} -> {After.Stringize()}";
74+
}
75+
76+
/// <summary>
77+
/// How an expression became an answer: an ordered chain of whole expressions, each one the
78+
/// result of the step before it, from the input to the value that was actually returned.
79+
/// </summary>
80+
/// <remarks>
81+
/// <para>
82+
/// This is what <see cref="RewriteRecording.Steps"/> and <see cref="RewriteRecording.Derivation"/>
83+
/// are not. Those are the rewrites that fired, across every candidate
84+
/// <see cref="Entity.Simplify(int)"/> generated including the ones it discarded, each on the
85+
/// subexpression it matched. Reading them in order does not walk from the input to the answer.
86+
/// This does: <c>Steps[i].After == Steps[i + 1].Before</c> holds for every <c>i</c>,
87+
/// <c>Steps[0].Before</c> is the <see cref="Input"/>, and the last step lands on the
88+
/// <see cref="Result"/>. Compared as expressions, not as printed forms.
89+
/// </para>
90+
/// <para>
91+
/// <b>The losing candidates are not here.</b> The simplifier explores far more expressions than
92+
/// it keeps — <see cref="ExpressionsExplored"/> says how many — and a route through a discarded
93+
/// candidate is not a route to the answer. They are excluded rather than labelled because a
94+
/// derivation is read forwards: a reader following the chain from the input needs every entry
95+
/// to be a step towards the answer, and a marked dead end is something to skip, which is the
96+
/// same as not being there while costing the reader the skip. What was explored but not taken
97+
/// is a fact about the search, and it is reported as a count for that reason.
98+
/// </para>
99+
/// <para>
100+
/// <b>Every step really happened.</b> Each one is an edge the engine actually traversed, with
101+
/// the expression it started from and the one it produced. Where several recorded routes reach
102+
/// the answer, the shortest is taken, and ties are settled by the order the engine recorded
103+
/// them in — so the same input gives the same path.
104+
/// </para>
105+
/// </remarks>
106+
/// <example>
107+
/// <code>
108+
/// using AngouriMath;
109+
/// using AngouriMath.Core.Transformations;
110+
///
111+
/// foreach (var step in DerivationPath.OfSimplifying("x ^ (-1) / (y / z)")!.Steps)
112+
/// Console.WriteLine(step);
113+
/// </code>
114+
/// </example>
115+
public sealed class DerivationPath
116+
{
117+
internal DerivationPath(Entity input, Entity result, IReadOnlyList<DerivationStep> steps, int expressionsExplored)
118+
=> (Input, Result, Steps, ExpressionsExplored) = (input, result, steps, expressionsExplored);
119+
120+
/// <summary>Where it started.</summary>
121+
public Entity Input { get; }
122+
123+
/// <summary>Where it ended — the value the operation returned.</summary>
124+
public Entity Result { get; }
125+
126+
/// <summary>
127+
/// The steps, in order. Empty where the input was already the answer, which is a path of
128+
/// length zero rather than a failure.
129+
/// </summary>
130+
public IReadOnlyList<DerivationStep> Steps { get; }
131+
132+
/// <summary>
133+
/// How many distinct expressions the search produced on the way, of which
134+
/// <see cref="Steps"/> is the chain it kept.
135+
/// </summary>
136+
/// <remarks>
137+
/// Here so that the path does not read as though it were the whole of what happened. On
138+
/// <c>x^(-1)/(y/z)</c> the search produces eleven expressions, keeps four of them, and
139+
/// fires 270 rewrites doing it; a four-step derivation presented on its own says none of
140+
/// that.
141+
/// </remarks>
142+
public int ExpressionsExplored { get; }
143+
144+
/// <summary>
145+
/// Runs <see cref="Entity.Simplify(int)"/> under a recording and returns how it got there,
146+
/// or <see langword="null"/> where the chain could not be reconstructed.
147+
/// </summary>
148+
/// <param name="expression">The expression to simplify.</param>
149+
/// <param name="level">As <see cref="Entity.Simplify(int)"/>.</param>
150+
/// <remarks>
151+
/// The whole of <a href="https://github.com/asc-community/AngouriMath/issues/28">#28</a> in
152+
/// one call, and it opens and closes the recording itself so that nothing is left on.
153+
/// </remarks>
154+
public static DerivationPath? OfSimplifying(Entity expression, int level = 2)
155+
{
156+
if (expression is null)
157+
throw new ArgumentNullException(nameof(expression));
158+
using var recording = RewriteRecording.Start();
159+
var result = expression.Simplify(level);
160+
return recording.PathFrom(expression, result);
161+
}
162+
163+
/// <summary>
164+
/// The path written out: the input, then one line per step giving what the expression
165+
/// became and what made it so.
166+
/// </summary>
167+
/// <remarks>
168+
/// The names are lined up in a column, which is what makes a derivation scannable — the
169+
/// reader is looking down the list of identities used, not reading the expressions.
170+
/// </remarks>
171+
public override string ToString()
172+
{
173+
var stages = new string[Steps.Count];
174+
var column = 0;
175+
for (var i = 0; i < Steps.Count; i++)
176+
{
177+
stages[i] = " = " + Steps[i].After.Stringize();
178+
if (stages[i].Length > column)
179+
column = stages[i].Length;
180+
}
181+
var text = new StringBuilder(Input.Stringize());
182+
for (var i = 0; i < stages.Length; i++)
183+
text.Append('\n').Append(stages[i]).Append(' ', column - stages[i].Length)
184+
.Append(" // ").Append(Steps[i].Name);
185+
return text.ToString();
186+
}
187+
}
188+
}

0 commit comments

Comments
 (0)