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())); + } + } +}