Skip to content

Commit d495672

Browse files
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 (#1428)
#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. Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
1 parent 6afe38a commit d495672

15 files changed

Lines changed: 202 additions & 70 deletions

File tree

‎BREAKING-CHANGES.md‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -677,6 +677,9 @@ they had.
677677
| | `"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)` |
678678
| **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` |
679679
| | `"e ^ ln(x)".ToEntity().Simplify()`, and every exponential of a natural logarithm | `e ^ ln(x)` — left as written | `x` |
680+
| | `"pi ^ log(pi, x)".ToEntity().Simplify()`, and every constant raised to a logarithm of itself | `pi ^ log(pi, x)` — left as written | `x` |
681+
| | `"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)) |
682+
| **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` |
680683
| | `"a => a + 3".ToEntity()`, and every lambda written with an arrow | `UnhandledParseException` | `lambda(a, a + 3)` |
681684
| | `"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)` |
682685
| | `"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)` |

‎Sources/.editorconfig‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -267,6 +267,9 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed
267267
[AngouriMath/Functions/Continuous/ExtremumOverSet.cs]
268268
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
269269

270+
[Tests/UnitTests/Core/Transformations/LogarithmSpellingsTest.cs]
271+
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
272+
270273
[AngouriMath/Functions/Compilation/IntoLinq/TensorCompilation.cs]
271274
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
272275

‎Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs‎

Lines changed: 39 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -2974,10 +2974,19 @@ is var (divided, remainder)
29742974
// is one node more: the delta is 1 - |a|, nothing at a leaf and a shrink beyond it.
29752975
growth: RewriteRuleGrowth.Collects),
29762976

2977+
// b ^ log_b(a) = a, in three arms by what can be said of the base. A number other
2978+
// than 0 and 1, and a constant -- e, pi -- are decidably neither 0 nor 1, which is all
2979+
// the identity needs: log_b(a) is defined only where b is neither, and where it is
2980+
// defined the power undoes it. It holds off the positive reals too -- at a = -3,
2981+
// ln(-3) is ln(3) + i*pi and e^(ln(3) + i*pi) is -3 -- and at a = 0, where ln(0) is
2982+
// -oo here and e^(-oo) is 0, so both sides are 0 and no definedness moves. Labelled
2983+
// under assumptions rather than Sound because it is the principal branch of the
2984+
// logarithm that makes it true away from the reals, which is a branch convention.
2985+
// A base of 0 or 1 is refused rather than answered: 1 ^ log(1, a) is 1, not a.
29772986
new MatchedRule(
29782987
"a-number-raised-to-a-logarithm-of-itself-is-the-antilogarithm",
29792988
MatchPattern.Node<Powf>(
2980-
MatchPattern.Any<Number>("c"),
2989+
MatchPattern.Any<Number>("c", static c => c != Integer.Zero && c != Integer.One),
29812990
MatchPattern.Node<Logf>(MatchPattern.Any<Number>("c"), MatchPattern.Any("a"))),
29822991
bound => bound["a"],
29832992
Soundness.SoundUnderAssumptions,
@@ -2986,31 +2995,40 @@ is var (divided, remainder)
29862995
// four nodes around the remaining hole disappear: exactly -4, for every input.
29872996
growth: RewriteRuleGrowth.Collects),
29882997

2989-
// The same identity through `e`, which the rule above cannot reach: `ln(b)` is stored
2990-
// as log(e, b) and `e` is a Constant, not a Number, so `Any<Number>` never binds it
2991-
// however the logarithm is written.
2992-
// https://github.com/asc-community/AngouriMath/issues/994
2993-
//
2994-
// Nothing is left to discharge once the base is `e`: b^log_b(a) = a needs ln(b) to be
2995-
// non-zero, and e is decidably neither 0 nor 1, which is exactly what the numeric arm
2996-
// above cannot say about an arbitrary Number. It holds off the positive reals too --
2997-
// at a = -3, ln(-3) is ln(3) + i*pi and e^(ln(3) + i*pi) is -3 -- and at a = 0, where
2998-
// ln(0) is -oo here and e^(-oo) is 0, so both sides are 0 and no definedness moves.
2999-
// Labelled under assumptions rather than Sound because it is the principal branch of
3000-
// the logarithm that makes it true away from the reals, which is a branch convention.
3001-
// Written with a pattern on the right rather than the `bound => bound["a"]` its
3002-
// numeric sibling uses, so it is data in both directions: the constructor can then
3003-
// check the replacement only builds names the pattern binds, and the rule classifies
3004-
// as Reversible instead of ReplacementIsCode.
3005-
new MatchedRule(
3006-
"e-raised-to-a-natural-logarithm-is-the-antilogarithm",
2998+
// The same identity through a constant: `ln(b)` is stored as log(e, b) and `e` is a
2999+
// Constant, not a Number, so `Any<Number>` never binds it however the logarithm is
3000+
// written, and pi ^ log(pi, b) was left standing for the same reason. Written with a
3001+
// pattern on the right rather than the `bound => bound["a"]` its numeric sibling uses,
3002+
// so it is data in both directions: the constructor can then check the replacement
3003+
// only builds names the pattern binds, and the rule classifies as Reversible instead
3004+
// of ReplacementIsCode. https://github.com/asc-community/AngouriMath/issues/994
3005+
new MatchedRule(
3006+
"a-constant-raised-to-a-logarithm-of-itself-is-the-antilogarithm",
30073007
MatchPattern.Node<Powf>(
3008-
MatchPattern.Exact(Variable.e),
3009-
MatchPattern.Node<Logf>(MatchPattern.Exact(Variable.e), MatchPattern.Any("a"))),
3008+
MatchPattern.Any<Constant>("c"),
3009+
MatchPattern.Node<Logf>(MatchPattern.Any<Constant>("c"), MatchPattern.Any("a"))),
30103010
MatchPattern.Any("a"),
30113011
Soundness.SoundUnderAssumptions,
30123012
description: "e ^ ln(b) = b"),
30133013

3014+
// And through a symbolic base, where b != 0 and b != 1 cannot be decided and so
3015+
// travel with the answer as its condition -- the domain condition of the logarithm
3016+
// that the rewrite would otherwise lose, which SimplificationContract.md says a rule
3017+
// either attaches or does not fire on. a ^ log(a, b) at a = 1 is undefined and b is
3018+
// not, so the difference is exactly that condition.
3019+
new MatchedRule(
3020+
"a-symbol-raised-to-a-logarithm-of-itself-is-the-antilogarithm-where-defined",
3021+
MatchPattern.Node<Powf>(
3022+
MatchPattern.Any("c"),
3023+
MatchPattern.Node<Logf>(MatchPattern.Any("c"), MatchPattern.Any("a"))),
3024+
bound => bound["a"].Provided(!bound["c"].EqualTo(0) & !bound["c"].EqualTo(1)),
3025+
Soundness.SoundUnderAssumptions,
3026+
when: bound => bound["c"] is not Number and not Constant,
3027+
description: "a ^ log(a, b) = b provided not a = 0 and not a = 1",
3028+
// The base is written twice again inside the condition, beside six new nodes
3029+
// for it: more than the power and the logarithm that go.
3030+
growth: RewriteRuleGrowth.Expands),
3031+
30143032
// Four `switch` arms: the power on either side of a product, and the shared base in
30153033
// either position inside it. A commutative pattern says both halves at once.
30163034
new MatchedRule(

‎Sources/AngouriMath/Docs/Contributing/WritingARule.md‎

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ effect". This is how to supply those seven things.
1818
## Where a rule goes
1919

2020
`Core/Transformations/Matching/MatchedRules.cs`, as a value in a `MatchedRuleSet`. **33** sets and
21-
**328** rules live there today.
21+
**329** rules live there today.
2222

2323
The `switch` statements in `Functions/Simplification/Patterns` are the older form. **All thirty
2424
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:
6464
2. Tangent is sine over cosine (tan(a) = sin(a) / cos(a)), so tan(x) becomes sin(x) / cos(x).
6565
```
6666

67-
So the name has to be a clause that survives being read that way. **All 299 distinct rule names are,
67+
So the name has to be a clause that survives being read that way. **All 300 distinct rule names are,
6868
and `StepAsASentenceTest` holds them to it** — a name with a capital, a bracket or an underscore
6969
fails that test rather than degrading the prose quietly.
7070

@@ -91,7 +91,7 @@ debugged for an afternoon.
9191
| `Left.ToString()` | `Divf(var a, Divf(var b, var c))` — how the matcher spells it |
9292

9393
Write the identity with `=`, not `->`: it is an equality, and the arrow belongs to the direction the
94-
rule happens to be applied in. **325** rules carry one today; a new rule should.
94+
rule happens to be applied in. **326** rules carry one today; a new rule should.
9595

9696
## The pattern language
9797

@@ -128,9 +128,10 @@ are legitimate — but the choice costs two things, so make it deliberately.
128128

129129
A pattern replacement gets:
130130

131-
- **a direction.** `MatchedRule.Reversed` is the rule read the other way, and **33** of the 35
132-
two-sided rules have one. The other two forget something: `sin²+cos² = 1` forgets the angle, and
133-
`{ x : x in S } = S` forgets the name the set builder bound, so neither has anything to read back.
131+
- **a direction.** `MatchedRule.Reversed` is the rule read the other way, and **32** of the 35
132+
two-sided rules have one. The other three forget something: `sin²+cos² = 1` forgets the angle,
133+
`{ x : x in S } = S` forgets the name the set builder bound, and `c ^ log(c, a) = a` for a
134+
constant `c` forgets which constant, so none has anything to read back.
134135
See [ReversibleRules.md](ReversibleRules.md).
135136
- **an exact growth**, counted from the two patterns rather than declared.
136137

@@ -224,7 +225,7 @@ limit, against nothing for handing the node over.
224225
| `SoundUnderAssumptions` | holds given something the rule does not check |
225226
| `Heuristic` | usually right |
226227

227-
**186** of the 328 rules are `Sound` and **142** are conditional. Every one of the thirty registered
228+
**186** of the 329 rules are `Sound` and **143** are conditional. Every one of the thirty registered
228229
*sets* declares `SoundUnderAssumptions`, because a set's tier is the **minimum** over its rules — so
229230
the set grain says nothing and the rule grain says everything. A derivation reports the rule's tier
230231
(`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:
241242
everything `Mulf(Divf(a, b), Divf(c, d))` matches and more, so the general rule would swallow the
242243
special one and the special one would never fire. `MatchPattern.Subsumes` computes this and
243244
`MatchedRuleSet.RulesByPriority` applies it: the specific rule is tried first because of what the two
244-
patterns *are*, not because of where you typed them. **28** rule pairs are ordered that way.
245+
patterns *are*, not because of where you typed them. **29** rule pairs are ordered that way.
245246

246247
**Where neither subsumes the other, the order is a bare choice and nothing but your placement makes
247248
it.** There are **39** such conflicts, and `RulePriorityTest` records every one by name. If your rule

‎Sources/AngouriMath/Functions/Compilation/IntoFE/Compiler.cs‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,15 @@ public override int GetHashCode()
6363
=> Name.GetHashCode();
6464
}
6565

66+
public partial record Constant
67+
{
68+
// A constant is its value. The named ones are substituted by value before
69+
// compiling; the base of ln and exp is Euler's number standing in the operator's
70+
// definition, which substitution leaves alone (#994), so it arrives here.
71+
private protected override void CompileNode(Compiler compiler) =>
72+
compiler.Instructions.Add(new(InstructionType.PUSH_CONST, Value: Value.ToNumerics()));
73+
}
74+
6675
partial record Matrix
6776
{
6877
private protected override void CompileNode(Compiler compiler) =>

‎Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs‎

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -140,22 +140,24 @@ expr is Powf(var @base, Integer { IsNegative: true } pow)
140140
// x^n / x
141141
Divf(Powf(var any1, var any2), var any1a) when any1 == any1a => new Powf(any1, any2 - 1),
142142

143-
// c ^ log(c, a) = a
144-
Powf(Number const1, Logf(Number const1a, var any1)) when const1 == const1a => any1,
143+
// c ^ log(c, a) = a for a number other than 0 and 1, which are refused: 1 ^ log(1, a)
144+
// is 1 rather than a.
145+
Powf(Number const1, Logf(Number const1a, var any1)) when const1 == const1a && const1 != Integer.Zero && const1 != Integer.One => any1,
145146

146-
// e ^ ln(a) = a, which is the same identity and needs its own arm because the one
147-
// above cannot reach it: `e` is a Variable rather than a Number, so `ln(a)` -- which
148-
// is stored as log(e, a) -- never presents a numeric base however it is written.
149-
// https://github.com/asc-community/AngouriMath/issues/994
150-
//
151-
// Assumptions: none. b^log_b(a) = a needs ln(b) to be non-zero, and e is decidably
152-
// neither 0 nor 1, so there is nothing left to discharge. It is not restricted to the
153-
// positive reals either, because on the principal branch ln(-3) is ln(3) + i*pi and
147+
// The same through a constant -- e, whose ln(a) is stored as log(e, a), and pi --
148+
// which is decidably neither 0 nor 1, so nothing is left to discharge. Not restricted
149+
// to the positive reals: on the principal branch ln(-3) is ln(3) + i*pi and
154150
// e^(ln(3) + i*pi) is -3; and at a = 0 both sides are 0, since ln(0) is -oo here and
155-
// e^(-oo) is 0. A symbolic base stays refused -- b != 1 is not decidable for it, and
156-
// 1^log(1, a) is 1 rather than a.
151+
// e^(-oo) is 0. https://github.com/asc-community/AngouriMath/issues/994
152+
Powf(Constant base1, Logf(Constant base1a, var any1))
153+
when base1 == base1a => any1,
154+
155+
// And through a symbol, where b != 0 and b != 1 cannot be decided and travel with the
156+
// answer as its condition: the logarithm's own domain condition, which the rewrite
157+
// would otherwise drop.
157158
Powf(var base1, Logf(var base1a, var any1))
158-
when base1 == base1a && base1 == Variable.e => any1,
159+
when base1 == base1a && base1 is not Number and not Constant
160+
=> any1.Provided(!base1.EqualTo(0) & !base1.EqualTo(1)),
159161

160162
Mulf(Powf(var any1, var any3), Mulf(var any1a, var any2)) when any1 == any1a => new Powf(any1, any3 + 1) * any2,
161163
Mulf(Powf(var any1, var any3), Mulf(var any2, var any1a)) when any1 == any1a => new Powf(any1, any3 + 1) * any2,

‎Sources/AngouriMath/Functions/Substitute.cs‎

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -98,15 +98,24 @@ public override Entity Substitute(Entity x, Entity value)
9898
partial record Logf
9999
{
100100
/// <inheritdoc/>
101+
// The base of ln is Euler's number standing in the operator's own definition, not a
102+
// mention of the name e, so substituting for e leaves it alone: ln(x) at e = 3 is
103+
// still ln(x), as sum(ln(x), e, 1, 2) already was 2 * ln(x). Compared by reference,
104+
// which is what Constant.EulerIntrinsic exists for; log(e, x), where the writer did
105+
// name e, still becomes log(3, x).
106+
// https://github.com/asc-community/AngouriMath/issues/994
101107
public override Entity Substitute(Entity x, Entity value)
102-
=> this == x ? value : New(Base.Substitute(x, value), Antilogarithm.Substitute(x, value));
108+
=> this == x ? value
109+
: New(ReferenceEquals(Base, Constant.EulerIntrinsic) ? Base : Base.Substitute(x, value), Antilogarithm.Substitute(x, value));
103110
}
104111

105112
partial record Powf
106113
{
107114
/// <inheritdoc/>
115+
// As for ln: the base of exp is not a mention of e.
108116
public override Entity Substitute(Entity x, Entity value)
109-
=> this == x ? value : New(Base.Substitute(x, value), Exponent.Substitute(x, value));
117+
=> this == x ? value
118+
: New(ReferenceEquals(Base, Constant.EulerIntrinsic) ? Base : Base.Substitute(x, value), Exponent.Substitute(x, value));
110119
}
111120

112121
partial record Arcsinf

‎Sources/Tests/UnitTests/Common/ExponentialOfALogarithmTest.cs‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -39,16 +39,18 @@ public void ANumericBaseStillDoes(string input, string expected)
3939
=> Assert.Equal(expected.ToEntity(), input.ToEntity().Simplify());
4040

4141
/// <summary>
42-
/// A symbolic base stays refused, and must: <c>b ^ log(b, a) = a</c> needs <c>ln(b)</c> to be
43-
/// non-zero, which is not decidable for a symbol, and at <c>b = 1</c> the left side is
44-
/// <c>1</c> rather than <c>a</c>. <c>e</c> is decidably neither <c>0</c> nor <c>1</c>, which
45-
/// is the whole of what the new rule relies on.
42+
/// A symbolic base folds under the condition it needs: <c>b ^ log(b, a) = a</c> needs
43+
/// <c>ln(b)</c> to be non-zero, which is not decidable for a symbol -- at <c>b = 1</c> the
44+
/// left side is undefined rather than <c>a</c> -- so the logarithm's own domain condition
45+
/// travels with the answer. <c>e</c> and <c>pi</c> are decidably neither <c>0</c> nor
46+
/// <c>1</c>, and fold outright.
47+
/// https://github.com/asc-community/AngouriMath/issues/994
4648
/// </summary>
4749
[Fact]
48-
public void ASymbolicBaseIsNotFolded()
50+
public void ASymbolicBaseFoldsWhereTheLogarithmIsDefined()
4951
{
50-
var expr = "a ^ log(a, x)".ToEntity();
51-
Assert.Equal(expr, expr.Simplify());
52+
Assert.Equal("x provided not a = 0 and not a = 1".ToEntity(), "a ^ log(a, x)".ToEntity().Simplify());
53+
Assert.Equal("x".ToEntity(), "pi ^ log(pi, x)".ToEntity().Simplify());
5254
}
5355

5456
/// <summary>And the base it would be wrong for is still answered the way it was.</summary>

‎Sources/Tests/UnitTests/Core/Transformations/AddressableRulesTest.cs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -299,7 +299,7 @@ public void TheRegistryIsAddressableAsFarAsItSaysItIs()
299299
// are thirty-three; NumericNeat's sixteen are eleven, six of them being three rules
300300
// written once per side a negative factor can sit on; and the two factorial sets are
301301
// eight arms each written as three. Every other repointed set is one arm for one rule.
302-
Assert.Equal(325, withRules.Sum(set => set.Rules.Count));
302+
Assert.Equal(326, withRules.Sum(set => set.Rules.Count));
303303
}
304304

305305
/// <summary>

0 commit comments

Comments
 (0)