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
18 changes: 16 additions & 2 deletions BREAKING-CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -118,6 +118,7 @@ read first.
| **Silent** | `"1/x - 1/x".ToEntity().Simplify()`, and every difference of a term from itself where that term can be undefined | `0`, including at `x = 0` where neither side has a value | `0 provided not x = 0` |

| **Silent** | `"(x + 1)!/(x + 1)!".ToEntity().Simplify()`, and every cancelled quotient whose repeated part can be undefined | `1 provided not (1 + x)! = 0` | `1 provided 1 + x in RR and (1 + x >= 0 or not 1 + x in ZZ)` — the same value everywhere, a condition that says why |
| | `"ln(x)/ln(x)".ToEntity().Simplify()`, and every quotient divided out by a divisor that can be undefined | `1 provided not ln(x) = 0` — which is `1` at `x = 0`, where the quotient has no value | `1 provided not ln(x) = 0 and not x = 0` |

### A cancelled quotient says its operand is defined, not only non-zero

Expand All @@ -141,8 +142,21 @@ three gamma poles and `1` elsewhere. The old form was adequate there by accident
than relying on it. `x / x`, `sin(x) / sin(x)`, `(x * y) / (x * y)` and every other operand that
cannot be undefined fold the added clause away and are unchanged.

**`ln(x) / ln(x)` itself still answers `1`**, from a candidate `PolynomialLongDivision` produces
rather than from either of these rules, and #1174 stays open for it.
**And the polynomial division carries its divisor's domain too.** `n / d = quotient + remainder` is
only the quotient where `d` has a value: `ln(x) / ln(x)` divides out to `1 + 0 / ln(x)`, which is `1`
at `x = 0` while the quotient it came from is undefined there, because the remainder term carries
only `ln(x) != 0`. That candidate is the one `Simplify` rated best, so it was what a caller actually
saw. With it fixed:

```
"ln(x) / ln(x)".Simplify() was 1 provided not ln(x) = 0 at x = 0: 1
is 1 provided not ln(x) = 0 and not x = 0 at x = 0: NaN
```

Ordinary divisions are untouched, because a divisor that cannot be undefined has a domain condition
of `True` and it folds away — `(x^2 - 1)/(x - 1)`, `(x^3 + 1)/(x + 1)`, `x^2 / x` and `x^3 / x^2` all
answer exactly what they did. `x!/x!` moves the same way `(x + 1)!/(x + 1)!` does, and for the same
reason; measured at x = -4, -3, -2, -1, 0, 1, 3, 1/2 and -1/2, old and new agree at every point.

### A term subtracted from itself says what it assumes

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -716,12 +716,18 @@ internal static class MatchedRules
new MatchedRule(
"a-quotient-of-polynomials-is-divided-out",
MatchPattern.Node<Divf>(MatchPattern.Any("n"), MatchPattern.Any("d")),
// The division is only the quotient where the divisor has a value. `ln(x) / ln(x)`
// divides out to `1 + 0 / ln(x)`, which is 1 at x = 0 while the quotient it came
// from is undefined there -- ln(0) is a pole, and the remainder term carries only
// `ln(x) != 0`. The condition folds away for any divisor that cannot be undefined.
// https://github.com/asc-community/AngouriMath/issues/1174
(node, bound) => TreeAnalyzer.PolynomialLongDivision(bound["n"], bound["d"])
is var (divided, remainder)
? divided + remainder
? (divided + remainder).Provided(bound["d"].DomainCondition)
: node,
Soundness.SoundUnderAssumptions,
description: "n / d = quotient + remainder, by polynomial long division"));
description: "n / d = quotient + remainder, by polynomial long division, "
+ "provided d is defined"));

/// <summary>
/// <see cref="Functions.Patterns.PolynomialGcdCancellation"/>, as data.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -54,10 +54,15 @@ internal static Entity SortAndGroup(Entity original, IEnumerable<Entity> childre
_ => x,
};
[AddressableRules]
// The division is only the quotient where the divisor has a value. `ln(x) / ln(x)` divides
// out to `1 + 0 / ln(x)`, which is 1 at x = 0 while the quotient it came from is undefined
// there -- ln(0) is a pole, and the remainder term carries only `ln(x) != 0`. The condition
// folds away for any divisor that cannot be undefined.
// https://github.com/asc-community/AngouriMath/issues/1174
internal static Entity PolynomialLongDivision(Entity x) =>
x is Divf(var num, var denom)
&& TreeAnalyzer.PolynomialLongDivision(num, denom) is var (divided, remainder)
? divided + remainder
? (divided + remainder).Provided(denom.DomainCondition)
: x;

/// <summary>
Expand Down
8 changes: 5 additions & 3 deletions Sources/Tests/UnitTests/PatternsTest/SimplifyTest.cs
Original file line number Diff line number Diff line change
Expand Up @@ -93,14 +93,16 @@ [Fact] public void Patt8Negative() =>
[Fact] public void FactorialXP1OverFactorialXM1() => AssertSimplify(MathS.Factorial(1 + x) / MathS.Factorial(-1 + x), x * (1 + x));
[Fact] public void FactorialXP1OverFactorialXM3() => AssertSimplifyIdentical(MathS.Factorial(x + 1) / MathS.Factorial(x - 3));
[Fact] public void FactorialXOverFactorialXP1() => AssertSimplify(MathS.Factorial(x) / MathS.Factorial(x + 1), 1 / (1 + x));
[Fact] public void FactorialXOverFactorialX() => AssertSimplify(MathS.Factorial(x) / MathS.Factorial(x), "1 provided not x! = 0");
[Fact] public void FactorialXOverFactorialX() => AssertSimplify(MathS.Factorial(x) / MathS.Factorial(x), "1 provided x in RR and (x >= 0 or not x in ZZ)");
[Fact] public void FactorialXOverFactorialXM1() => AssertSimplify(MathS.Factorial(0 + x) / MathS.Factorial(x - 1), x);
[Fact] public void FactorialXOverFactorialXM2() => AssertSimplify(MathS.Factorial(x + 0) / MathS.Factorial(x - 2), x.Pow(2) - x);
[Fact] public void FactorialXOverFactorialXM3() => AssertSimplifyIdentical(MathS.Factorial(x) / MathS.Factorial(x - 3));
[Fact] public void FactorialXM1OverFactorialXP1() => AssertSimplify(MathS.Factorial(x - 1) / MathS.Factorial(x + 1), 1 / (x * (x + 1)));
[Fact] public void FactorialXM1OverFactorialX() => AssertSimplify(MathS.Factorial(-1 + x) / MathS.Factorial(x), 1 / x);
// The domain condition, as above. `FactorialXOverFactorialX` keeps the older form and is
// not a inconsistency to fix here: a bare `x!` reaches this through a different candidate.
// The domain condition, as above. `FactorialXOverFactorialX` kept the older form for one
// commit, because a bare `x!` reached this through the candidate polynomial long division
// produces rather than through a cancellation rule. That division carries its divisor's
// domain now as well, so all three of these agree again.
[Fact] public void FactorialXM1OverFactorialXM1() => AssertSimplify(MathS.Factorial(x - 1) / MathS.Factorial(x - 1), "1 provided x - 1 in RR and (x - 1 >= 0 or not x - 1 in ZZ)");
[Fact] public void FactorialXM1OverFactorialXM2() => AssertSimplify(MathS.Factorial(-1 + x) / MathS.Factorial(-2 + x), x - 1);
// Same two factors, now in ascending order: the polynomial factorer offers
Expand Down
Loading