From 274dc942596c7fdf464385c1061c2c0296a3adce Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Sun, 30 Aug 2026 16:18:26 +0000 Subject: [PATCH] A guide to writing a rewrite rule, with every figure in it under test #746 tier 2 lists five major deliverables. Four exist -- the rule registry, the rewrite graph with pluggable extraction, the canonicalisation framework, the confluence and termination checker. This is the fifth. `Docs/Contributing/WritingARule.md` is the *how*. Whether a rule is **allowed** is a harder question and a different document: `SimplificationContract.md` comes first, and the guide says so in its opening line, because a rule written beautifully that holds only on the positive reals while claiming to hold everywhere is a wrong answer with good spelling. What it covers: where a rule goes and why not in a `switch`; the seven things a rule carries; why the name is a sentence rather than an identifier, and how it is read aloud by `DerivationPath.Explain()`; that the name, the identity and the rendered pattern are three different things all worth having; the pattern language and the two families it deliberately cannot build; what choosing a code replacement costs -- a direction and an exact growth; that soundness is per rule and the set grain says nothing; when the order of two rules is yours to choose and when subsumption has already decided; the ten tests that will check a new rule; and the whole of it once, on one rule. **Every count in it is asserted by `RuleAuthoringGuideTest`, and the guide says so at the top.** A document that states a number goes stale silently, and a guide is the worst case: it is read by somebody who does not yet know the code and is therefore in no position to notice that "33 of the 322 rules have a pattern on both sides" stopped being true two releases ago. Nine facts are held: the set and rule counts, the 293 distinct names and their four-to-sixteen-word range, the 59 identities, the 44 buildable node types, the 33 two-sided rules and 32 directions, the 181 Sound against 141 conditional, the 268 at Unknown growth, and the 28 pairs ordered by subsumption. The failure message names the claim and says to update the document rather than the test. Two more that are not counts. The ten tests the guide sends a contributor to are checked to exist, by reflection over the test assembly -- a guide that names a test which has been renamed is worse than one that names none, since the reader concludes the check does not exist rather than that the document is old. And the worked example at the end is looked up in the library and applied, so it cannot become a rule that is not there. Writing it found one thing: the guide asserted the one-way rule is the Pythagorean identity, which is what the documentation calls it, and matched on the name containing "pythagorean". The rule is called `squared-sine-and-cosine-of-one-argument-sum-to-one`. The prose is right and the assertion was matching the prose rather than the rule; it now matches the rule. Also indexes the guide in the contributing README, whose numbering had two entries at 10. Full suite: 8988 passed, 14 skipped, 0 failed. No public API change. Part of #746 tier 2. --- .../AngouriMath/Docs/Contributing/README.md | 5 +- .../Docs/Contributing/WritingARule.md | 224 ++++++++++++++++++ .../Transformations/RuleAuthoringGuideTest.cs | 173 ++++++++++++++ 3 files changed, 401 insertions(+), 1 deletion(-) create mode 100644 Sources/AngouriMath/Docs/Contributing/WritingARule.md create mode 100644 Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs diff --git a/Sources/AngouriMath/Docs/Contributing/README.md b/Sources/AngouriMath/Docs/Contributing/README.md index c4fe08909..a24b0ee6d 100644 --- a/Sources/AngouriMath/Docs/Contributing/README.md +++ b/Sources/AngouriMath/Docs/Contributing/README.md @@ -27,9 +27,12 @@ If you aren't sure about what to add, you may want to check the current projects 10. What a node type has to implement — the eleven abstract members of `Entity`, which five an assembly outside the kernel cannot reach, and the decision on whether a domain package may define a node type at all -10. Reading a rewrite rule backwards — what a rule has to carry +11. Reading a rewrite rule backwards — what a rule has to carry before it can be read the other way, which rules can carry it, and what the mechanism costs the fast path +12. Writing a rewrite rule — the seven things a rule carries, why its + name is a sentence rather than an identifier, what the pattern language can and cannot build, and + which tests will check it See also BREAKING-CHANGES.md, where a change that makes the same input give a different answer is recorded, and diff --git a/Sources/AngouriMath/Docs/Contributing/WritingARule.md b/Sources/AngouriMath/Docs/Contributing/WritingARule.md new file mode 100644 index 000000000..454fc92e2 --- /dev/null +++ b/Sources/AngouriMath/Docs/Contributing/WritingARule.md @@ -0,0 +1,224 @@ +# Writing a rewrite rule + +This is the *how*. Whether a rule is **allowed** is a different question and a harder one — +[SimplificationContract.md](SimplificationContract.md) is that document, and it comes first. A rule +that is written beautifully and holds only on the positive reals while claiming to hold everywhere is +a wrong answer with good spelling. + +[#746](https://github.com/asc-community/AngouriMath/issues/746) tier 2 asks for rules that are *data* +carrying "identity, name, direction, applicability conditions, justification tier, provenance, cost +effect". This is how to supply those seven things. + +> Every count in this document is asserted by `RuleAuthoringGuideTest`. If a number here is wrong, a +> test fails — which is the only way a document like this stays true. Do not edit a figure without +> re-running that test; it is measuring the library, not repeating this file. + +--- + +## Where a rule goes + +`Core/Transformations/Matching/MatchedRules.cs`, as a value in a `MatchedRuleSet`. **33** sets and +**322** rules live there today. + +The `switch` statements in `Functions/Simplification/Patterns` are the older form. Twenty-seven of +the thirty registered sets no longer run theirs, and twenty no longer describe it either; the +remainder are being moved set by set ([#825](https://github.com/asc-community/AngouriMath/issues/825)). +**Do not add a rule to a `switch`.** A `switch` arm cannot carry a name, a tier, an identity or a +direction, and everything below is about those. + +## What a rule carries + +```csharp +// a * (1 / b) = a / b +new MatchedRule( + "reciprocal-factor-becomes-a-quotient", + MatchPattern.Node( + MatchPattern.Any("a"), + MatchPattern.Node(MatchPattern.Exact(Integer.Create(1)), MatchPattern.Any("b"))), + MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), + Soundness.SoundUnderAssumptions, + description: "a * (1 / b) = a / b") +``` + +| | | +|---|---| +| **name** | a clause in English, in kebab case — see below | +| **left** | the pattern it fires on | +| **right** | the replacement, as a pattern or as code | +| **soundness** | how well justified *this* rule is, not its set | +| `description:` | the identity, in the notation a mathematician would write | +| `when:` | a side condition on the bindings, where the pattern cannot say it | +| `growth:` | how much bigger the replacement is — only where the replacement is code | + +`SourceLine` is filled in by the compiler through `[CallerLineNumber]`. Nobody maintains it. + +## The name is a sentence, not an identifier + +Rule names are read aloud. `DerivationPath.Explain()` renders a derivation by replacing the hyphens +in a name and putting the identity in brackets after it: + +``` +2. Tangent is sine over cosine (tan(a) = sin(a) / cos(a)), so tan(x) becomes sin(x) / cos(x). +``` + +So the name has to be a clause that survives being read that way. **All 293 distinct rule names are, +and `StepAsASentenceTest` holds them to it** — a name with a capital, a bracket or an underscore +fails that test rather than degrading the prose quietly. + +Write what the rule *says*, not what it operates on: + +| | | +|---|---| +| ✔ | `a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero` | +| ✔ | `two-powers-of-one-base-divide-by-subtracting-exponents` | +| ✘ | `divf-simplification-2` — not a clause, and the 2 will be wrong when somebody inserts one | +| ✘ | `DivideByItself` — reads as an identifier in the middle of a sentence | + +The names run from four to sixteen words. Long is fine; a name is read once and a wrong rewrite is +debugged for an afternoon. + +## The identity is not the name + +`description:` is the third distinct thing, and all three are worth having: + +| | | +|---|---| +| name | `dividing-by-a-quotient-multiplies-by-its-reciprocal` — what to call it | +| description | `a / (b / c) = a * c / b` — what it says | +| `Left.ToString()` | `Divf(var a, Divf(var b, var c))` — how the matcher spells it | + +Write the identity with `=`, not `->`: it is an equality, and the arrow belongs to the direction the +rule happens to be applied in. **59** rules carry one today; a new rule should. + +## The pattern language + +| | matches | +|---|---| +| `MatchPattern.Any("a")` | anything, binding it to `a` | +| `MatchPattern.Any("c")` | anything of that node type | +| `MatchPattern.Any("n", v => v.IsPositive)` | that, and a predicate | +| `MatchPattern.Exact(Integer.Create(1))` | one literal value | +| `MatchPattern.Node(l, r)` | that node type, children in that order | +| `MatchPattern.Commutative(l, r)` | that node type, children in either order | +| `MatchPattern.Gathered("rest", parts)` | those parts anywhere in an n-ary chain, the rest bound | + +**A hole repeated is an equality.** `Node(Any("a"), Any("a"))` matches a quotient of a thing by +itself, and needs no `when:` to say so. It is also strictly more specific than `Divf(a, b)`, which +the ordering knows about — see below. + +**Matchable is not the same as buildable.** A pattern can be *matched* against any node type, but a +pattern used as a **replacement** must be one the library can construct: there are **44** such types. +Two families are deliberately absent, and neither is an oversight: + +- **binders** — `Lambda`, `Set.ConditionalSet`. They bind a variable, and `DirectChildren` renames it + to avoid capture, so a pattern reaching inside one would match a name that does not exist outside; +- **variable-arity nodes** — `Piecewise`, `Application`, finite `Set`s, `Matrix`. A pattern fixes an + arity and these do not have one. + +Naming an unbuildable type in a replacement throws at construction rather than producing a rule that +matches and silently builds nothing. `BuildableNodeTypesTest` is the list. + +## Replacement: a pattern, or code + +**33** of the 322 rules have a pattern on both sides. The rest build their answer in code, and both +are legitimate — but the choice costs two things, so make it deliberately. + +A pattern replacement gets: + +- **a direction.** `MatchedRule.Reversed` is the rule read the other way, and **32** of the 33 + two-sided rules have one. (The thirty-third is the Pythagorean identity: `sin²+cos² = 1` forgets the + angle, so there is nothing to read back. See [ReversibleRules.md](ReversibleRules.md).) +- **an exact growth**, counted from the two patterns rather than declared. + +A code replacement gets neither, and its growth is `Unknown` unless you declare one. That is the +honest default — **268** rules sit at `Unknown` — but declare it where you can justify it: + +```csharp +// The Chebyshev expansion of sin(n * a) is a sum of n terms where the pattern is one node, +// for every n this fires on. +RewriteRuleGrowth.Expands, +``` + +Take `(Entity node, Bindings bound)` rather than `(Bindings bound)` where the replacement needs the +whole matched node. Rebuilding it from the bindings makes a different object with none of the +original's cached `InnerSimplified`, `Evaled`, `Codomain` or rate — measured at **4.0–5.2 s** on one +limit, against nothing for handing the node over. + +## Soundness is per rule + +| | | +|---|---| +| `Sound` | holds for every value the pattern admits, with nothing assumed | +| `SoundUnderAssumptions` | holds given something the rule does not check | +| `Heuristic` | usually right | + +**181** of the 322 rules are `Sound` and **141** are conditional. Every one of the thirty registered +*sets* declares `SoundUnderAssumptions`, because a set's tier is the **minimum** over its rules — so +the set grain says nothing and the rule grain says everything. A derivation reports the rule's tier +(`RewriteStep.Soundness`), which is why getting it right matters beyond the label. + +The tier is **declared, not checked**. It is a claim to argue with. Tightening one needs an argument; +loosening one does not. + +## Order, and when it is yours to choose + +A set is first-match-wins, so where two rules fire at one node and disagree, **whichever is tried +first decides the answer**. Two cases, and only one of them is a decision: + +**Where one pattern subsumes the other, it is not a choice.** `Mulf(a, Divf(b, c))` matches +everything `Mulf(Divf(a, b), Divf(c, d))` matches and more, so the general rule would swallow the +special one and the special one would never fire. `MatchPattern.Subsumes` computes this and +`MatchedRuleSet.RulesByPriority` applies it: the specific rule is tried first because of what the two +patterns *are*, not because of where you typed them. **28** rule pairs are ordered that way. + +**Where neither subsumes the other, the order is a bare choice and nothing but your placement makes +it.** There are **39** such conflicts, and `RulePriorityTest` records every one by name. If your rule +adds a fortieth, that test fails and tells you — which is the moment to decide whether you meant it. + +Related, and separate: `RuleSetTerminationTest` checks that a set run to a fixed point actually +reaches one, and `RuleConfluenceTest` checks whether two rules of a set that both fire agree. + +## What will check your rule + +Adding a rule to `MatchedRules.cs` puts it in front of all of these without any wiring: + +| | | +|---|---| +| `MatchedRulesAllTest` | it is reachable, named, and its set is well-formed | +| `MatchedRulesAgreeWithTheSwitchTest` | where the set mirrors a `switch`, the two still agree over generated expressions | +| `RulePriorityTest` | the order it is tried in is the order it is written in, and any new conflict is recorded | +| `RuleSetTerminationTest` | its set still settles, alone and composed with the normalisation | +| `RuleConfluenceTest` | any new disagreement between two arms is recorded | +| `ReversibleRuleTest` | its direction is what its two sides say it is | +| `MatchedRuleGrowthTest` | its growth is what its two sides say it is | +| `StepAsASentenceTest` | its name reads as English | +| `RuleMetadataTest` | its tier and identity reach the registry | +| `Corpus` | forty problems, on every commit, reporting solved / unsolved / wrong / error / timeout | + +And outside the repository, in the analysis workspace: `casbench`, `propcheck`, `simpsweep`, +`boundcheck`, `rulecheck`, `canoncheck`. A green suite is evidence about the suite. + +## The whole of it, once + +```csharp +// x / x = 1, wherever x is not zero +new MatchedRule( + "a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero", + MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("a")), + (node, bound) => new Providedf(1, !bound["a"].EqualTo(0)), + Soundness.SoundUnderAssumptions, + description: "a / a = 1, provided a is not zero") +``` + +Seven decisions, and each of them is somewhere a reader can find it: the name says what it does, the +repeated hole says the two sides must be the same expression, the replacement attaches the condition +rather than asserting an equality that is false at zero, the tier says the answer is conditional, and +the identity says it in the notation a mathematician would use. + +## See also + +- [SimplificationContract.md](SimplificationContract.md) — whether the rule is allowed at all +- [Transformations.md](Transformations.md) — the layer the sets sit in +- [ReversibleRules.md](ReversibleRules.md) — what a rule needs before it can be read backwards +- [CanonicalForm.md](CanonicalForm.md) — what "simplest" is and is not +- [EMatching.md](EMatching.md) — how a pattern matches an e-class rather than a term diff --git a/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs new file mode 100644 index 000000000..fb51bff0c --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs @@ -0,0 +1,173 @@ +// +// Copyright (c) 2019-2026 Angouri. +// AngouriMath is licensed under MIT. +// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md. +// Website: https://am.angouri.org. +// + +using System; +using System.Linq; +using AngouriMath.Core.Transformations; +using AngouriMath.Core.Transformations.Matching; +using AngouriMath.Extensions; +using Xunit; + +namespace AngouriMath.Tests.Core.Transformations +{ + /// + /// Every count stated in Docs/Contributing/WritingARule.md, measured. + /// + /// + /// + /// A document that states a number goes stale silently, and nothing about reading it says + /// so. A guide is worse than most: it is read by somebody who does not yet know the code, + /// and is therefore in no position to notice that "33 of the 322 rules have a pattern on both + /// sides" stopped being true two releases ago. The only defence is to make the number fail a + /// build, which is what this is. + /// + /// + /// The assertion is one-directional on purpose: it says the library still has this many, not + /// that it should. A count that moves is a prompt to update one line of a document, and the + /// failure message says which line. + /// + /// + [Trait("Area", "Core")] + public sealed class RuleAuthoringGuideTest + { + private static void Stated(int stated, int measured, string claim) + => Assert.True(stated == measured, + $"WritingARule.md says {claim} is {stated}; it is {measured}. " + + "Update the document, not this test."); + + [Fact] + public void WhereARuleGoes() + { + Stated(33, MatchedRules.All.Count, "the number of rule sets written as data"); + Stated(322, MatchedRules.All.Sum(set => set.Rules.Count), "the number of rules written as data"); + Stated(30, RewriteRules.All.Count, "the number of registered sets"); + Stated(27, RewriteRules.All.Count(set => + MatchedRules.All.Any(data => data.Name == set.Name) + || set.Name.StartsWith("CommonDenominator", StringComparison.Ordinal)), + "how many registered sets run the matcher"); + Stated(20, RewriteRules.All.Count(set => + set.Rules.Count > 0 && set.Rules.All(rule => rule.Soundness is not null)), + "how many registered sets describe what they run"); + } + + [Fact] + public void TheNameIsASentence() + { + var names = MatchedRules.All.SelectMany(set => set.Rules) + .Select(rule => rule.Name).Distinct(StringComparer.Ordinal).ToList(); + Stated(293, names.Count, "the number of distinct rule names"); + + var words = names.Select(name => name.Split('-').Length).ToList(); + Stated(4, words.Min(), "the shortest rule name in words"); + Stated(16, words.Max(), "the longest rule name in words"); + } + + [Fact] + public void TheIdentityIsNotTheName() + => Stated(59, + MatchedRules.All.SelectMany(set => set.Rules).Count(rule => rule.Description is not null), + "how many rules carry an identity"); + + [Fact] + public void ThePatternLanguage() + => Stated(44, MatchPattern.BuildableNodeTypes.Count, "the number of buildable node types"); + + [Fact] + public void ReplacementAPatternOrCode() + { + var rules = MatchedRules.All.SelectMany(set => set.Rules).ToList(); + Stated(33, rules.Count(rule => rule.Right is not null), + "how many rules have a pattern on both sides"); + Stated(32, rules.Count(rule => rule.Reversed is not null), + "how many two-sided rules have a direction"); + Stated(268, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Unknown), + "how many rules sit at Unknown growth"); + + // And the thirty-third is the one the document names. Asserted by its own name rather + // than by the one the documentation calls it: the rule is + // `squared-sine-and-cosine-of-one-argument-sum-to-one` and the prose calls it the + // Pythagorean identity, which is right and is not what to match on. + var oneWay = rules.Single(rule => rule.Right is not null && rule.Reversed is null); + Assert.Equal(RuleReversal.ReplacementDropsHoles, oneWay.Reversal); + Assert.Equal("squared-sine-and-cosine-of-one-argument-sum-to-one", oneWay.Name); + } + + [Fact] + public void SoundnessIsPerRule() + { + var rules = MatchedRules.All.SelectMany(set => set.Rules).ToList(); + Stated(181, rules.Count(rule => rule.Soundness is Soundness.Sound), + "how many rules are Sound"); + Stated(141, rules.Count(rule => rule.Soundness is Soundness.SoundUnderAssumptions), + "how many rules are SoundUnderAssumptions"); + Assert.All(RewriteRules.All, + set => Assert.Equal(Soundness.SoundUnderAssumptions, set.Soundness)); + } + + /// + /// The two ordering counts. Both are held by as lists — which + /// is the stronger check, since a list says which — and repeated here as counts only + /// because the document states them as counts. + /// + [Fact] + public void OrderAndWhenItIsYoursToChoose() + { + var subsuming = 0; + foreach (var set in MatchedRules.All) + { + var rules = set.Rules; + for (var i = 0; i < rules.Count; i++) + for (var j = 0; j < rules.Count; j++) + { + if (i == j) continue; + if (rules[i].Left.Subsumes(rules[j].Left) + && !rules[j].Left.Subsumes(rules[i].Left)) + subsuming++; + } + } + Stated(28, subsuming, "how many rule pairs are ordered by subsumption"); + } + + /// + /// The tests the document promises will check a new rule all exist, by name. + /// + /// + /// A guide that sends a contributor to a test which has been renamed is worse than one that + /// names none: they will conclude the check does not exist rather than that the document is + /// old. Reflection over the test assembly is what keeps that honest. + /// + [Fact] + public void TheTestsItPromisesExist() + { + var promised = new[] + { + "MatchedRulesAllTest", "MatchedRulesAgreeWithTheSwitchTest", "RulePriorityTest", + "RuleSetTerminationTest", "RuleConfluenceTest", "ReversibleRuleTest", + "MatchedRuleGrowthTest", "StepAsASentenceTest", "RuleMetadataTest", + "BuildableNodeTypesTest", + }; + var present = typeof(RuleAuthoringGuideTest).Assembly.GetTypes() + .Select(type => type.Name).ToHashSet(StringComparer.Ordinal); + Assert.All(promised, name => Assert.True(present.Contains(name), + $"WritingARule.md sends a contributor to {name}, which does not exist")); + } + + /// + /// The worked example at the end of the document is a rule that really is in the library, + /// and really does what the document says it does. + /// + [Fact] + public void TheWorkedExampleIsReal() + { + var rule = MatchedRules.All.SelectMany(set => set.Rules).First(r => + r.Name == "a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero"); + Assert.Equal(Soundness.SoundUnderAssumptions, rule.Soundness); + Assert.NotNull(rule.TryApply("x / x".ToEntity())); + Assert.Null(rule.TryApply("x / y".ToEntity())); + } + } +}