From 9306108ede7835078f42d27370ac8d641dd725be Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Fri, 18 Sep 2026 22:45:30 +0000 Subject: [PATCH] A power undoes a logarithm of its own base whatever the base, every logarithm rule is held to both spellings, and the base of ln is not a mention of e #994, the three-step route the thread settled on, the node declined. The antilogarithm rule matched a numeric base only, and the twin written for e -- ln(b) being log(e, b) with a Constant base -- matched e only, so pi ^ log(pi, x) and a ^ log(a, x) stood while 2 ^ log(2, x) and e ^ ln(x) folded. Three arms now, by what can be said of the base: a number other than 0 and 1 (a base of 1 or 0 is refused rather than answered, 1 ^ log(1, a) being 1 and not a), a constant, which is decidably neither, and a symbol, where b != 0 and b != 1 travel with the answer as its condition -- the logarithm's own domain condition, which SimplificationContract.md says a rule attaches or does not fire on. The switch spelling has the same three arms. LogarithmSpellingsTest holds every rule set to both spellings: an identity written in base 2 and in base e is rewritten by a set on one exactly when on the other, which is the test the thread asked for and the thing that would reopen the node question. Substituting for e no longer reaches the base of ln or exp: it is Euler's number standing in the operator's own definition, compared by reference to Constant.EulerIntrinsic, exactly as a binder over the name e already treated it since #991; log(e, x) and e ^ x, where the writer named e, still substitute. The guide's counts and the pinned rule lists move by one each. Recorded in BREAKING-CHANGES.md against a v2.5.0 build. Closes #994. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura --- BREAKING-CHANGES.md | 3 + Sources/.editorconfig | 3 + .../Transformations/Matching/MatchedRules.cs | 60 ++++++++++----- .../Docs/Contributing/WritingARule.md | 17 ++-- .../Functions/Compilation/IntoFE/Compiler.cs | 9 +++ .../Simplification/Patterns/Patterns.Power.cs | 28 +++---- Sources/AngouriMath/Functions/Substitute.cs | 13 +++- .../Common/ExponentialOfALogarithmTest.cs | 16 ++-- .../Transformations/AddressableRulesTest.cs | 2 +- .../Transformations/LogarithmSpellingsTest.cs | 77 +++++++++++++++++++ .../Transformations/ReversibleRuleTest.cs | 2 + .../Transformations/RuleAuthoringGuideTest.cs | 21 ++--- .../Core/Transformations/RuleMetadataTest.cs | 6 +- .../Core/Transformations/RulePriorityTest.cs | 13 +++- .../Transformations/StepAsASentenceTest.cs | 2 +- 15 files changed, 202 insertions(+), 70 deletions(-) create mode 100644 Sources/Tests/UnitTests/Core/Transformations/LogarithmSpellingsTest.cs diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index 0b8f3876c..cc505351f 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -663,6 +663,9 @@ they had. | | `"sin(x)^2 + 2 sin(x) + 1".ToEntity().Factorize()`, and every polynomial in one subexpression of its variable | `sin(x) ^ 2 + 2 * sin(x) + 1` — left alone | `(sin(x) + 1) ^ 2`; `sin(x) + sin(x)^3` is `sin(x) * (sin(x) ^ 2 + 1)` | | **Silent** | `"arccotan(-1)".ToEntity().Simplify()`, and every negative argument the inverse-trigonometric table knows | `3/4 * pi` — the textbook range, and **not equal to `arccotan(-1)`**, whose value is `-pi/4` | `-1/4 * pi` | | | `"e ^ ln(x)".ToEntity().Simplify()`, and every exponential of a natural logarithm | `e ^ ln(x)` — left as written | `x` | +| | `"pi ^ log(pi, x)".ToEntity().Simplify()`, and every constant raised to a logarithm of itself | `pi ^ log(pi, x)` — left as written | `x` | +| | `"a ^ log(a, x)".ToEntity().Simplify()`, and every symbolic base raised to a logarithm of itself | `a ^ log(a, x)` — left as written | `x provided not a = 0 and not a = 1` — the logarithm's own domain condition, which the rewrite would otherwise lose ([#994](https://github.com/asc-community/AngouriMath/issues/994)) | +| **Silent** | `MathS.Ln("x").Substitute("e", 3)`, and `"exp(x)".ToEntity().Substitute("e", 3)` | `log(3, x)` and `3 ^ x` — the base of `ln` and `exp` was reached as a mention of `e` | `ln(x)` and `exp(x)` — it is Euler's number in the operator's definition, not a mention; `log(e, x)` and `e ^ x`, where the writer named `e`, still become `log(3, x)` and `3 ^ x` | | | `"a => a + 3".ToEntity()`, and every lambda written with an arrow | `UnhandledParseException` | `lambda(a, a + 3)` | | | `"sqrt(5 + 2 * sqrt(6))".ToEntity().Simplify()`, and every nested radical whose discriminant is a rational square | `sqrt(5 + 2 * sqrt(6))` — left as written | `sqrt(3) + sqrt(2)` | | | `"sum(k, k, 1, n)".ToEntity().Simplify()`, and every summation whose body is a polynomial in the index | `sum(k, k, 1, n)` — carried | `piecewise((n + n ^ 2) / 2 provided n >= 0, 0)` | diff --git a/Sources/.editorconfig b/Sources/.editorconfig index 110b0e774..d200b4d32 100644 --- a/Sources/.editorconfig +++ b/Sources/.editorconfig @@ -267,6 +267,9 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed [AngouriMath/Functions/Continuous/ExtremumOverSet.cs] file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n +[Tests/UnitTests/Core/Transformations/LogarithmSpellingsTest.cs] +file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n + [AngouriMath/Functions/IntervalArithmetic.cs] file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs index 7e3461360..d7c101134 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs @@ -2974,10 +2974,19 @@ is var (divided, remainder) // is one node more: the delta is 1 - |a|, nothing at a leaf and a shrink beyond it. growth: RewriteRuleGrowth.Collects), + // b ^ log_b(a) = a, in three arms by what can be said of the base. A number other + // than 0 and 1, and a constant -- e, pi -- are decidably neither 0 nor 1, which is all + // the identity needs: log_b(a) is defined only where b is neither, and where it is + // defined the power undoes it. It holds off the positive reals too -- at a = -3, + // ln(-3) is ln(3) + i*pi and e^(ln(3) + i*pi) is -3 -- and at a = 0, where ln(0) is + // -oo here and e^(-oo) is 0, so both sides are 0 and no definedness moves. Labelled + // under assumptions rather than Sound because it is the principal branch of the + // logarithm that makes it true away from the reals, which is a branch convention. + // A base of 0 or 1 is refused rather than answered: 1 ^ log(1, a) is 1, not a. new MatchedRule( "a-number-raised-to-a-logarithm-of-itself-is-the-antilogarithm", MatchPattern.Node( - MatchPattern.Any("c"), + MatchPattern.Any("c", static c => c != Integer.Zero && c != Integer.One), MatchPattern.Node(MatchPattern.Any("c"), MatchPattern.Any("a"))), bound => bound["a"], Soundness.SoundUnderAssumptions, @@ -2986,31 +2995,40 @@ is var (divided, remainder) // four nodes around the remaining hole disappear: exactly -4, for every input. growth: RewriteRuleGrowth.Collects), - // The same identity through `e`, which the rule above cannot reach: `ln(b)` is stored - // as log(e, b) and `e` is a Constant, not a Number, so `Any` never binds it - // however the logarithm is written. - // https://github.com/asc-community/AngouriMath/issues/994 - // - // Nothing is left to discharge once the base is `e`: b^log_b(a) = a needs ln(b) to be - // non-zero, and e is decidably neither 0 nor 1, which is exactly what the numeric arm - // above cannot say about an arbitrary Number. It holds off the positive reals too -- - // at a = -3, ln(-3) is ln(3) + i*pi and e^(ln(3) + i*pi) is -3 -- and at a = 0, where - // ln(0) is -oo here and e^(-oo) is 0, so both sides are 0 and no definedness moves. - // Labelled under assumptions rather than Sound because it is the principal branch of - // the logarithm that makes it true away from the reals, which is a branch convention. - // Written with a pattern on the right rather than the `bound => bound["a"]` its - // numeric sibling uses, so it is data in both directions: the constructor can then - // check the replacement only builds names the pattern binds, and the rule classifies - // as Reversible instead of ReplacementIsCode. - new MatchedRule( - "e-raised-to-a-natural-logarithm-is-the-antilogarithm", + // The same identity through a constant: `ln(b)` is stored as log(e, b) and `e` is a + // Constant, not a Number, so `Any` never binds it however the logarithm is + // written, and pi ^ log(pi, b) was left standing for the same reason. Written with a + // pattern on the right rather than the `bound => bound["a"]` its numeric sibling uses, + // so it is data in both directions: the constructor can then check the replacement + // only builds names the pattern binds, and the rule classifies as Reversible instead + // of ReplacementIsCode. https://github.com/asc-community/AngouriMath/issues/994 + new MatchedRule( + "a-constant-raised-to-a-logarithm-of-itself-is-the-antilogarithm", MatchPattern.Node( - MatchPattern.Exact(Variable.e), - MatchPattern.Node(MatchPattern.Exact(Variable.e), MatchPattern.Any("a"))), + MatchPattern.Any("c"), + MatchPattern.Node(MatchPattern.Any("c"), MatchPattern.Any("a"))), MatchPattern.Any("a"), Soundness.SoundUnderAssumptions, description: "e ^ ln(b) = b"), + // And through a symbolic base, where b != 0 and b != 1 cannot be decided and so + // travel with the answer as its condition -- the domain condition of the logarithm + // that the rewrite would otherwise lose, which SimplificationContract.md says a rule + // either attaches or does not fire on. a ^ log(a, b) at a = 1 is undefined and b is + // not, so the difference is exactly that condition. + new MatchedRule( + "a-symbol-raised-to-a-logarithm-of-itself-is-the-antilogarithm-where-defined", + MatchPattern.Node( + MatchPattern.Any("c"), + MatchPattern.Node(MatchPattern.Any("c"), MatchPattern.Any("a"))), + bound => bound["a"].Provided(!bound["c"].EqualTo(0) & !bound["c"].EqualTo(1)), + Soundness.SoundUnderAssumptions, + when: bound => bound["c"] is not Number and not Constant, + description: "a ^ log(a, b) = b provided not a = 0 and not a = 1", + // The base is written twice again inside the condition, beside six new nodes + // for it: more than the power and the logarithm that go. + growth: RewriteRuleGrowth.Expands), + // Four `switch` arms: the power on either side of a product, and the shared base in // either position inside it. A commutative pattern says both halves at once. new MatchedRule( diff --git a/Sources/AngouriMath/Docs/Contributing/WritingARule.md b/Sources/AngouriMath/Docs/Contributing/WritingARule.md index 4641a747a..67cdd97a6 100644 --- a/Sources/AngouriMath/Docs/Contributing/WritingARule.md +++ b/Sources/AngouriMath/Docs/Contributing/WritingARule.md @@ -18,7 +18,7 @@ effect". This is how to supply those seven things. ## Where a rule goes `Core/Transformations/Matching/MatchedRules.cs`, as a value in a `MatchedRuleSet`. **33** sets and -**328** rules live there today. +**329** rules live there today. The `switch` statements in `Functions/Simplification/Patterns` are the older form. **All thirty registered sets now run as data and describe what they run**; none executes its `switch` any more. @@ -64,7 +64,7 @@ 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 299 distinct rule names are, +So the name has to be a clause that survives being read that way. **All 300 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. @@ -91,7 +91,7 @@ debugged for an afternoon. | `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. **325** rules carry one today; a new rule should. +rule happens to be applied in. **326** rules carry one today; a new rule should. ## The pattern language @@ -128,9 +128,10 @@ 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 **33** of the 35 - two-sided rules have one. The other two forget something: `sin²+cos² = 1` forgets the angle, and - `{ x : x in S } = S` forgets the name the set builder bound, so neither has anything to read back. +- **a direction.** `MatchedRule.Reversed` is the rule read the other way, and **32** of the 35 + two-sided rules have one. The other three forget something: `sin²+cos² = 1` forgets the angle, + `{ x : x in S } = S` forgets the name the set builder bound, and `c ^ log(c, a) = a` for a + constant `c` forgets which constant, so none has anything to read back. See [ReversibleRules.md](ReversibleRules.md). - **an exact growth**, counted from the two patterns rather than declared. @@ -224,7 +225,7 @@ limit, against nothing for handing the node over. | `SoundUnderAssumptions` | holds given something the rule does not check | | `Heuristic` | usually right | -**186** of the 328 rules are `Sound` and **142** are conditional. Every one of the thirty registered +**186** of the 329 rules are `Sound` and **143** 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. @@ -241,7 +242,7 @@ first decides the answer**. Two cases, and only one of them is a decision: 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. +patterns *are*, not because of where you typed them. **29** 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 diff --git a/Sources/AngouriMath/Functions/Compilation/IntoFE/Compiler.cs b/Sources/AngouriMath/Functions/Compilation/IntoFE/Compiler.cs index f820cf2e1..ab99829a1 100644 --- a/Sources/AngouriMath/Functions/Compilation/IntoFE/Compiler.cs +++ b/Sources/AngouriMath/Functions/Compilation/IntoFE/Compiler.cs @@ -63,6 +63,15 @@ public override int GetHashCode() => Name.GetHashCode(); } + public partial record Constant + { + // A constant is its value. The named ones are substituted by value before + // compiling; the base of ln and exp is Euler's number standing in the operator's + // definition, which substitution leaves alone (#994), so it arrives here. + private protected override void CompileNode(Compiler compiler) => + compiler.Instructions.Add(new(InstructionType.PUSH_CONST, Value: Value.ToNumerics())); + } + partial record Matrix { private protected override void CompileNode(Compiler compiler) => diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs index a84ef7593..402cd3697 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs +++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs @@ -140,22 +140,24 @@ expr is Powf(var @base, Integer { IsNegative: true } pow) // x^n / x Divf(Powf(var any1, var any2), var any1a) when any1 == any1a => new Powf(any1, any2 - 1), - // c ^ log(c, a) = a - Powf(Number const1, Logf(Number const1a, var any1)) when const1 == const1a => any1, + // c ^ log(c, a) = a for a number other than 0 and 1, which are refused: 1 ^ log(1, a) + // is 1 rather than a. + Powf(Number const1, Logf(Number const1a, var any1)) when const1 == const1a && const1 != Integer.Zero && const1 != Integer.One => any1, - // e ^ ln(a) = a, which is the same identity and needs its own arm because the one - // above cannot reach it: `e` is a Variable rather than a Number, so `ln(a)` -- which - // is stored as log(e, a) -- never presents a numeric base however it is written. - // https://github.com/asc-community/AngouriMath/issues/994 - // - // Assumptions: none. b^log_b(a) = a needs ln(b) to be non-zero, and e is decidably - // neither 0 nor 1, so there is nothing left to discharge. It is not restricted to the - // positive reals either, because on the principal branch ln(-3) is ln(3) + i*pi and + // The same through a constant -- e, whose ln(a) is stored as log(e, a), and pi -- + // which is decidably neither 0 nor 1, so nothing is left to discharge. Not restricted + // to the positive reals: on the principal branch ln(-3) is ln(3) + i*pi and // e^(ln(3) + i*pi) is -3; and at a = 0 both sides are 0, since ln(0) is -oo here and - // e^(-oo) is 0. A symbolic base stays refused -- b != 1 is not decidable for it, and - // 1^log(1, a) is 1 rather than a. + // e^(-oo) is 0. https://github.com/asc-community/AngouriMath/issues/994 + Powf(Constant base1, Logf(Constant base1a, var any1)) + when base1 == base1a => any1, + + // And through a symbol, where b != 0 and b != 1 cannot be decided and travel with the + // answer as its condition: the logarithm's own domain condition, which the rewrite + // would otherwise drop. Powf(var base1, Logf(var base1a, var any1)) - when base1 == base1a && base1 == Variable.e => any1, + when base1 == base1a && base1 is not Number and not Constant + => any1.Provided(!base1.EqualTo(0) & !base1.EqualTo(1)), Mulf(Powf(var any1, var any3), Mulf(var any1a, var any2)) when any1 == any1a => new Powf(any1, any3 + 1) * any2, Mulf(Powf(var any1, var any3), Mulf(var any2, var any1a)) when any1 == any1a => new Powf(any1, any3 + 1) * any2, diff --git a/Sources/AngouriMath/Functions/Substitute.cs b/Sources/AngouriMath/Functions/Substitute.cs index a597e4446..aa74750a3 100644 --- a/Sources/AngouriMath/Functions/Substitute.cs +++ b/Sources/AngouriMath/Functions/Substitute.cs @@ -98,15 +98,24 @@ public override Entity Substitute(Entity x, Entity value) partial record Logf { /// + // The base of ln is Euler's number standing in the operator's own definition, not a + // mention of the name e, so substituting for e leaves it alone: ln(x) at e = 3 is + // still ln(x), as sum(ln(x), e, 1, 2) already was 2 * ln(x). Compared by reference, + // which is what Constant.EulerIntrinsic exists for; log(e, x), where the writer did + // name e, still becomes log(3, x). + // https://github.com/asc-community/AngouriMath/issues/994 public override Entity Substitute(Entity x, Entity value) - => this == x ? value : New(Base.Substitute(x, value), Antilogarithm.Substitute(x, value)); + => this == x ? value + : New(ReferenceEquals(Base, Constant.EulerIntrinsic) ? Base : Base.Substitute(x, value), Antilogarithm.Substitute(x, value)); } partial record Powf { /// + // As for ln: the base of exp is not a mention of e. public override Entity Substitute(Entity x, Entity value) - => this == x ? value : New(Base.Substitute(x, value), Exponent.Substitute(x, value)); + => this == x ? value + : New(ReferenceEquals(Base, Constant.EulerIntrinsic) ? Base : Base.Substitute(x, value), Exponent.Substitute(x, value)); } partial record Arcsinf diff --git a/Sources/Tests/UnitTests/Common/ExponentialOfALogarithmTest.cs b/Sources/Tests/UnitTests/Common/ExponentialOfALogarithmTest.cs index 162308424..24f7f7627 100644 --- a/Sources/Tests/UnitTests/Common/ExponentialOfALogarithmTest.cs +++ b/Sources/Tests/UnitTests/Common/ExponentialOfALogarithmTest.cs @@ -39,16 +39,18 @@ public void ANumericBaseStillDoes(string input, string expected) => Assert.Equal(expected.ToEntity(), input.ToEntity().Simplify()); /// - /// A symbolic base stays refused, and must: b ^ log(b, a) = a needs ln(b) to be - /// non-zero, which is not decidable for a symbol, and at b = 1 the left side is - /// 1 rather than a. e is decidably neither 0 nor 1, which - /// is the whole of what the new rule relies on. + /// A symbolic base folds under the condition it needs: b ^ log(b, a) = a needs + /// ln(b) to be non-zero, which is not decidable for a symbol -- at b = 1 the + /// left side is undefined rather than a -- so the logarithm's own domain condition + /// travels with the answer. e and pi are decidably neither 0 nor + /// 1, and fold outright. + /// https://github.com/asc-community/AngouriMath/issues/994 /// [Fact] - public void ASymbolicBaseIsNotFolded() + public void ASymbolicBaseFoldsWhereTheLogarithmIsDefined() { - var expr = "a ^ log(a, x)".ToEntity(); - Assert.Equal(expr, expr.Simplify()); + Assert.Equal("x provided not a = 0 and not a = 1".ToEntity(), "a ^ log(a, x)".ToEntity().Simplify()); + Assert.Equal("x".ToEntity(), "pi ^ log(pi, x)".ToEntity().Simplify()); } /// And the base it would be wrong for is still answered the way it was. diff --git a/Sources/Tests/UnitTests/Core/Transformations/AddressableRulesTest.cs b/Sources/Tests/UnitTests/Core/Transformations/AddressableRulesTest.cs index 6209dfc1a..b571c4969 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/AddressableRulesTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/AddressableRulesTest.cs @@ -299,7 +299,7 @@ public void TheRegistryIsAddressableAsFarAsItSaysItIs() // are thirty-three; NumericNeat's sixteen are eleven, six of them being three rules // written once per side a negative factor can sit on; and the two factorial sets are // eight arms each written as three. Every other repointed set is one arm for one rule. - Assert.Equal(325, withRules.Sum(set => set.Rules.Count)); + Assert.Equal(326, withRules.Sum(set => set.Rules.Count)); } /// diff --git a/Sources/Tests/UnitTests/Core/Transformations/LogarithmSpellingsTest.cs b/Sources/Tests/UnitTests/Core/Transformations/LogarithmSpellingsTest.cs new file mode 100644 index 000000000..9c4486442 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/LogarithmSpellingsTest.cs @@ -0,0 +1,77 @@ +// +// 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.Linq; +using AngouriMath; +using AngouriMath.Core.Transformations.Matching; +using AngouriMath.Extensions; +using Xunit; + +namespace AngouriMath.Tests.Core.Transformations +{ + /// + /// ln(x) is log(e, x) with the base a constant rather than a number, so a rule + /// matching a logarithm can quietly stop matching the one spelling while it matches the + /// other. Every rule that reads a logarithm is exercised here on both: an identity written + /// in base 2 and the same identity in base e, and a rule fires on one exactly when it fires + /// on the other. #994 + /// + [Trait("Area", "Transformations")] + public sealed class LogarithmSpellingsTest + { + [Theory] + [InlineData("2 ^ log(2, x)", "e ^ ln(x)")] + [InlineData("x ^ (n / log(2, x))", "x ^ (n / ln(x))")] + [InlineData("log(2, x ^ 3)", "ln(x ^ 3)")] + [InlineData("log(2, 8)", "ln(8)")] + [InlineData("log(2, 2)", "ln(e)")] + [InlineData("log(2, 1 / x)", "ln(1 / x)")] + [InlineData("log(2, x) + log(2, y)", "ln(x) + ln(y)")] + [InlineData("log(2, x) - log(2, y)", "ln(x) - ln(y)")] + // A reciprocal base has to be written as a quotient to be one -- 1/2 is a number -- and + // the rule asks that the base be decidably positive, which a symbol is not; so the pair + // here is the other constant against e. + [InlineData("log(1 / pi, x)", "log(1 / e, x)")] + [InlineData("log(1 / pi, 1 / x)", "log(1 / e, 1 / x)")] + public void EveryLogarithmRuleSetReadsBothSpellings(string inBaseTwo, string natural) + { + var two = inBaseTwo.ToEntity(); + var e = natural.ToEntity(); + // Per set rather than per rule: a set may read a numeric base and a constant one + // through two rules, and what is owed is that the set answers both. + var disagreeing = MatchedRules.All + .Where(set => !ReferenceEquals(set.ApplyHere(two), two) != !ReferenceEquals(set.ApplyHere(e), e)) + .Select(set => set.Name) + .ToList(); + Assert.True(disagreeing.Count == 0, + $"these rule sets rewrite one spelling and not the other of {inBaseTwo} / {natural}: " + string.Join(", ", disagreeing)); + } + + [Theory] + // b ^ log(b, a) = a wherever the logarithm is defined, whatever the base. + [InlineData("2 ^ log(2, x)", "x")] + [InlineData("e ^ ln(x)", "x")] + [InlineData("pi ^ log(pi, x)", "x")] + [InlineData("(1/2) ^ log(1/2, x)", "x")] + [InlineData("a ^ log(a, x)", "x provided not a = 0 and not a = 1")] + [InlineData("(x + 1) ^ log(x + 1, y)", "y provided not 1 + x = 0 and not 1 + x = 1")] + // A base of 1 or 0 is not a base, and the identity is not asserted of it. + [InlineData("1 ^ log(1, x)", "NaN")] + public void APowerUndoesALogarithmOfItsOwnBase(string input, string expected) + => Assert.Equal(expected.ToEntity(), input.ToEntity().Simplify()); + + [Fact] + public void TheBaseOfLnIsNotAMentionOfE() + { + Assert.Equal("ln(x)".ToEntity(), "ln(x)".ToEntity().Substitute("e", 3)); + Assert.Equal("exp(x)".ToEntity(), "exp(x)".ToEntity().Substitute("e", 3)); + // Where the writer did name e, the name is substituted. + Assert.Equal("log(3, x)".ToEntity(), "log(e, x)".ToEntity().Substitute("e", 3)); + Assert.Equal("3 ^ x".ToEntity(), "e ^ x".ToEntity().Substitute("e", 3)); + } + } +} diff --git a/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs b/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs index 54deb572a..102dcee5f 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs @@ -136,6 +136,7 @@ public void EveryDataRuleIsClassifiedAsWritten() "a-conjunction-of-negations-is-a-negated-disjunction: ReplacementIsCode", "a-conjunction-with-a-falsehood-is-false: ReplacementIsCode", "a-conjunction-with-itself-is-itself: ReplacementIsCode", + "a-constant-raised-to-a-logarithm-of-itself-is-the-antilogarithm: ReplacementDropsHoles", "a-cosecant-times-a-sine-of-one-angle-is-one: ReplacementIsCode", "a-difference-chain-is-sorted-and-grouped: ReplacementIsCode", "a-difference-of-even-powers-splits: ReplacementIsCode", @@ -295,6 +296,7 @@ public void EveryDataRuleIsClassifiedAsWritten() "a-sum-of-two-negatives-is-a-negated-sum: ReplacementIsCode", "a-sum-or-difference-that-is-a-perfect-square: ReplacementIsCode", "a-sum-over-its-own-reverse-is-one: ReplacementIsCode", + "a-symbol-raised-to-a-logarithm-of-itself-is-the-antilogarithm-where-defined: ReplacementIsCode", "a-tangent-times-a-cotangent-of-one-angle-is-one: ReplacementIsCode", "a-term-added-to-a-difference-that-starts-from-it: ReplacementIsCode", "a-term-added-to-a-difference-that-takes-it-away: ReplacementIsCode", diff --git a/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs index e22cdfec1..e19460a8a 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs @@ -43,7 +43,7 @@ private static void Stated(int stated, int measured, string claim) public void WhereARuleGoes() { Stated(33, MatchedRules.All.Count, "the number of rule sets written as data"); - Stated(328, MatchedRules.All.Sum(set => set.Rules.Count), "the number of rules written as data"); + Stated(329, MatchedRules.All.Sum(set => set.Rules.Count), "the number of rules written as data"); Stated(30, RewriteRules.All.Count, "the number of registered sets"); // Two families register under one name and run a data set under another -- // CommonDenominator over MatchedRules.CommonDenominator(level), CanonicalOrder over @@ -64,7 +64,7 @@ public void TheNameIsASentence() { var names = MatchedRules.All.SelectMany(set => set.Rules) .Select(rule => rule.Name).Distinct(StringComparer.Ordinal).ToList(); - Stated(299, names.Count, "the number of distinct rule names"); + Stated(300, 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"); @@ -73,7 +73,7 @@ public void TheNameIsASentence() [Fact] public void TheIdentityIsNotTheName() - => Stated(325, + => Stated(326, MatchedRules.All.SelectMany(set => set.Rules).Count(rule => rule.Description is not null), "how many rules carry an identity"); @@ -87,7 +87,7 @@ public void ReplacementAPatternOrCode() var rules = MatchedRules.All.SelectMany(set => set.Rules).ToList(); Stated(35, rules.Count(rule => rule.Right is not null), "how many rules have a pattern on both sides"); - Stated(33, rules.Count(rule => rule.Reversed is not null), + Stated(32, rules.Count(rule => rule.Reversed is not null), "how many two-sided rules have a direction"); Stated(123, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Unknown), "how many rules sit at Unknown growth"); @@ -101,14 +101,14 @@ public void ReplacementAPatternOrCode() "how many rules are declared Collects"); Stated(49, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Rearranges), "how many rules are declared Rearranges"); - Stated(32, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Expands), + Stated(33, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Expands), "how many rules are declared Expands"); - // And the two the document names. By their own names rather than by what the prose + // And the three the document names. By their own names rather than by what the prose // calls them: the first 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. Both forget something the backwards direction would have to invent -- the - // angle, and the name the set builder bound. + // match on. All three forget something the backwards direction would have to invent + // -- the angle, the name the set builder bound, and which constant was raised. var oneWay = rules .Where(rule => rule.Right is not null && rule.Reversed is null) .Select(rule => rule.Name) @@ -118,6 +118,7 @@ public void ReplacementAPatternOrCode() new[] { "a-conditional-set-whose-condition-is-its-own-membership-is-that-set", + "a-constant-raised-to-a-logarithm-of-itself-is-the-antilogarithm", "squared-sine-and-cosine-of-one-argument-sum-to-one", }, oneWay); @@ -132,7 +133,7 @@ public void SoundnessIsPerRule() var rules = MatchedRules.All.SelectMany(set => set.Rules).ToList(); Stated(186, rules.Count(rule => rule.Soundness is Soundness.Sound), "how many rules are Sound"); - Stated(142, rules.Count(rule => rule.Soundness is Soundness.SoundUnderAssumptions), + Stated(143, rules.Count(rule => rule.Soundness is Soundness.SoundUnderAssumptions), "how many rules are SoundUnderAssumptions"); Assert.All(RewriteRules.All, set => Assert.Equal(Soundness.SoundUnderAssumptions, set.Soundness)); @@ -159,7 +160,7 @@ public void OrderAndWhenItIsYoursToChoose() subsuming++; } } - Stated(28, subsuming, "how many rule pairs are ordered by subsumption"); + Stated(29, subsuming, "how many rule pairs are ordered by subsumption"); } /// diff --git a/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs index 11e66f6d6..0d2589c7c 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs @@ -88,9 +88,9 @@ public void AddressableGrowthIsTheRulesOwnAnswer() public void SoundnessIsFinerPerRuleThanPerSet() { var rules = MatchedRules.All.SelectMany(set => set.Rules).ToList(); - Assert.Equal(328, rules.Count); + Assert.Equal(329, rules.Count); Assert.Equal(186,rules.Count(rule => rule.Soundness is Soundness.Sound)); - Assert.Equal(142, rules.Count(rule => rule.Soundness is Soundness.SoundUnderAssumptions)); + Assert.Equal(143, rules.Count(rule => rule.Soundness is Soundness.SoundUnderAssumptions)); // And every set still reports the weakest of them, which is what makes the set grain // uninformative rather than wrong. @@ -174,7 +174,7 @@ public void EveryRuleOfARepointedSetCarriesItsIdentity() var repointed = RewriteRules.All .Where(set => set.Rules.Count > 0 && set.Rules.All(rule => rule.Soundness is not null)) .ToList(); - Assert.Equal(325, repointed.Sum(set => set.Rules.Count)); + Assert.Equal(326, repointed.Sum(set => set.Rules.Count)); Assert.All(repointed, set => Assert.All(set.Rules, rule => Assert.NotNull(rule.Description))); } diff --git a/Sources/Tests/UnitTests/Core/Transformations/RulePriorityTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RulePriorityTest.cs index 095682e79..3a32159fa 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/RulePriorityTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/RulePriorityTest.cs @@ -144,8 +144,8 @@ private static SortedSet Subsumptions() /// /// /// Over every rule rather than within a set, because the relation is about patterns and - /// nothing about it stops at a set boundary: 961 ordered pairs claim subsumption, - /// 501 of them are put to the test by the corpus containing something the narrower + /// nothing about it stops at a set boundary: 962 ordered pairs claim subsumption, + /// 502 of them (501 before the constant antilogarithm rule of #994 subsumed the symbolic one) are put to the test by the corpus containing something the narrower /// pattern matches, and none is contradicted across 85,153 nodes. All three counts /// are asserted — a corpus that stopped reaching these shapes would otherwise turn this /// into a test that passes by asking nothing, and a witnessed count means nothing without @@ -205,8 +205,8 @@ public void SubsumptionIsNeverContradictedByMatching() if (put) witnessed++; } - Assert.Equal(961, claims.Count); - Assert.Equal(501, witnessed); + Assert.Equal(962, claims.Count); + Assert.Equal(502, witnessed); // Asserted so the two figures in the remark above cannot go stale in silence: the // whole point of `witnessed` is that it is a coverage number, and it means nothing // without knowing what it was measured over. @@ -278,6 +278,11 @@ public void TheRecordedSubsumptionsAreTheOnesThereAre() "InequalityEquality: an-equality-or-a-less-than-the-other-way-round-is-at-least before two-comparisons-of-one-pair-that-leave-no-case-are-true", "Power: a-logarithm-of-a-reciprocal-in-a-reciprocal-base-turns-round-twice before a-logarithm-in-a-reciprocal-base-negates", "Power: a-logarithm-of-a-reciprocal-in-a-reciprocal-base-turns-round-twice before a-logarithm-of-a-reciprocal-negates", + // A constant base is a symbolic base that says more, so the arm that discharges + // the condition goes before the one that attaches it. The numeric arm is guarded + // by a predicate, which subsumption does not read, so it is ordered by declaration. + // https://github.com/asc-community/AngouriMath/issues/994 + "Power: a-constant-raised-to-a-logarithm-of-itself-is-the-antilogarithm before a-symbol-raised-to-a-logarithm-of-itself-is-the-antilogarithm-where-defined", }; Assert.Equal(recorded.OrderBy(name => name, StringComparer.Ordinal), Subsumptions()); } diff --git a/Sources/Tests/UnitTests/Core/Transformations/StepAsASentenceTest.cs b/Sources/Tests/UnitTests/Core/Transformations/StepAsASentenceTest.cs index d034b4c81..8f4ed6dff 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/StepAsASentenceTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/StepAsASentenceTest.cs @@ -59,7 +59,7 @@ public void EveryRuleWrittenAsDataIsNamedInProse() { var names = MatchedRules.All.SelectMany(set => set.Rules).Select(rule => rule.Name) .Distinct(StringComparer.Ordinal).ToList(); - Assert.Equal(299, names.Count); + Assert.Equal(300, names.Count); Assert.All(names, name => Assert.True(Explanation.IsProse(name), $"'{name}' is a rule name that does not read as a phrase in English"));