Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions BREAKING-CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -677,6 +677,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)` |
Expand Down
3 changes: 3 additions & 0 deletions Sources/.editorconfig
Original file line number Diff line number Diff line change
Expand Up @@ -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/Compilation/IntoLinq/TensorCompilation.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

Expand Down
60 changes: 39 additions & 21 deletions Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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<Powf>(
MatchPattern.Any<Number>("c"),
MatchPattern.Any<Number>("c", static c => c != Integer.Zero && c != Integer.One),
MatchPattern.Node<Logf>(MatchPattern.Any<Number>("c"), MatchPattern.Any("a"))),
bound => bound["a"],
Soundness.SoundUnderAssumptions,
Expand All @@ -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<Number>` 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<Number>` 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<Powf>(
MatchPattern.Exact(Variable.e),
MatchPattern.Node<Logf>(MatchPattern.Exact(Variable.e), MatchPattern.Any("a"))),
MatchPattern.Any<Constant>("c"),
MatchPattern.Node<Logf>(MatchPattern.Any<Constant>("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<Powf>(
MatchPattern.Any("c"),
MatchPattern.Node<Logf>(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(
Expand Down
17 changes: 9 additions & 8 deletions Sources/AngouriMath/Docs/Contributing/WritingARule.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.

Expand All @@ -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

Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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.
Expand All @@ -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
Expand Down
9 changes: 9 additions & 0 deletions Sources/AngouriMath/Functions/Compilation/IntoFE/Compiler.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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) =>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
13 changes: 11 additions & 2 deletions Sources/AngouriMath/Functions/Substitute.cs
Original file line number Diff line number Diff line change
Expand Up @@ -98,15 +98,24 @@ public override Entity Substitute(Entity x, Entity value)
partial record Logf
{
/// <inheritdoc/>
// 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
{
/// <inheritdoc/>
// 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
Expand Down
16 changes: 9 additions & 7 deletions Sources/Tests/UnitTests/Common/ExponentialOfALogarithmTest.cs
Original file line number Diff line number Diff line change
Expand Up @@ -39,16 +39,18 @@ public void ANumericBaseStillDoes(string input, string expected)
=> Assert.Equal(expected.ToEntity(), input.ToEntity().Simplify());

/// <summary>
/// A symbolic base stays refused, and must: <c>b ^ log(b, a) = a</c> needs <c>ln(b)</c> to be
/// non-zero, which is not decidable for a symbol, and at <c>b = 1</c> the left side is
/// <c>1</c> rather than <c>a</c>. <c>e</c> is decidably neither <c>0</c> nor <c>1</c>, which
/// is the whole of what the new rule relies on.
/// A symbolic base folds under the condition it needs: <c>b ^ log(b, a) = a</c> needs
/// <c>ln(b)</c> to be non-zero, which is not decidable for a symbol -- at <c>b = 1</c> the
/// left side is undefined rather than <c>a</c> -- so the logarithm's own domain condition
/// travels with the answer. <c>e</c> and <c>pi</c> are decidably neither <c>0</c> nor
/// <c>1</c>, and fold outright.
/// https://github.com/asc-community/AngouriMath/issues/994
/// </summary>
[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());
}

/// <summary>And the base it would be wrong for is still answered the way it was.</summary>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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));
}

/// <summary>
Expand Down
Loading
Loading