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
29 changes: 29 additions & 0 deletions BREAKING-CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ read first.
| **silent** | `DomainCondition` of a logarithm, under the default reading | the real condition, so `log(-3, -3)` was declared undefined while evaluating to `1` | `not b = 0 and not b = 1 and not a = 0` |
| **silent** | `ln(x).DomainCondition` | `x > 0` | `not x = 0` |
| **silent** | `"x ^ n".Differentiate("x").Simplify()` | `x ^ n * n / x provided x > 0` — `NaN` at every negative `x` | `x ^ n * n / x provided not x = 0` |
| **silent** | `ln(a) + ln(b)` and `ln(a) - ln(b)` for symbolic `a`, `b` | `ln(a * b)`, `ln(a / b)` — wrong by `2*pi*i` off the positive reals | left as written |
| **silent** | `"x^5 + 2x^3 - 2x^2 - 4".SolveEquation("x")` | three of the five roots, one of them a float | all five, exact |
| | `"x^4 + x^2 + 1".SolveEquation("x")` | `sqrt((-1 - sqrt(-3)) / 2)` and its three companions | `(-1 - sqrt(-3)) / 2` and its three, with no nested radical |
| | `"x^4 + 3x^2 + 2".SolveEquation("x")` | `{ sqrt(-2), -sqrt(-2), i, -i }` | the same four, in the order the factors are found |
Expand Down Expand Up @@ -81,6 +82,34 @@ Both sets are unchanged as sets — the members were checked to be equal, not me
a solution set is only reordered, as for `x^4 + 3x^2 + 2` and `2x^4 + 6x^2 + 4`, code that indexed
into the result rather than searching it will see different elements at the same positions.

### A sum of logarithms is no longer gathered unless that is exact

`ln(a) + ln(b) = ln(a*b)` is false off the positive reals. At `x = -3` the two sides differ by
`2*pi*i`, the turn of the argument the principal branch discards:

```
"ln(x) + ln(x+1)" at x = -3 1.7918 + 6.2832i
gathered to ln(x*(1+x)) 1.7918 — the value that was returned
```

Both rules were applied unconditionally, and this was the last disagreement `boundcheck` reported.
It now reports **none**.

**Numbers still gather.** `ln(2) + ln(3)` is `ln(6)` and `ln(6) - ln(2)` is `ln(3)`, because there
the operands are decidably positive. What no longer happens is the same rewrite on a *symbol*,
which may be anything.

**And the identity is not lost where it was doing real work.** Taking a limit states where the
expression is going, and on a stated approach the sign of each operand is decidable — so the
gathering still happens inside a limit, exactly where it is exact. A sum needs both operands
positive; a difference needs only that their signs *agree*, since `ln` of a negative is
`ln|.| + pi*i` and that cancels in a difference while it would double in a sum. No limit answer is
lost, which was measured rather than assumed: withdrawing the rule without putting it back this way
does not cost coverage, it costs **termination**, because the limit machinery's own expansion
creates the pairs that only this puts back together.

From [#721](https://github.com/asc-community/AngouriMath/issues/721).

### The logarithm's domain follows the reading, as every other node's already did

`Arcsinf`, `Arccosf`, `Arcsecantf` and `Arccosecantf` each state one condition over the reals and
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,27 @@ namespace AngouriMath.Functions.Algebra
using static Entity.Number;
internal static partial class LimitFunctional
{
/// <summary>
/// Everything below here reads the expression on its way to <c>+oo</c>, whichever
/// destination was asked for, so that is stated once and held for the whole computation.
/// </summary>
/// <remarks>
/// It has to be the whole computation rather than the simplification below: the
/// logarithm pairs that have to be gathered are created *inside* the simplifier's own
/// candidate search and are gathered there, without ever being a subexpression any of
/// these methods sees. Measured -- with the approach stated around only the first
/// simplification, the rule was reached 192 times for <c>lim x-&gt;-oo (x-5)^x / x^x</c>
/// with the operands <c>-x</c> and <c>-(x+5)</c>, and every one of them found no approach
/// to check against. https://github.com/asc-community/AngouriMath/issues/721
/// </remarks>
private static Entity? SimplifyAndComputeLimitToInfinity(Entity expr, Variable x)
{
var outerApproach = EnterApproach(x, Real.PositiveInfinity);
try { return SimplifyAndComputeLimitToInfinityCore(expr, x); }
finally { LeaveApproach(outerApproach); }
}

private static Entity? SimplifyAndComputeLimitToInfinityCore(Entity expr, Variable x)
{
expr = expr.Simplify();
if (expr is Providedf(var expression, _)) expr = expression; // limits operate assuming a continuous expression even though some points may be undefined.
Expand Down Expand Up @@ -65,9 +85,9 @@ internal static partial class LimitFunctional
var logarithmDivisionResult = LimitSolvers.SolveAsLogarithmDivision(expr, x);
if (logarithmDivisionResult is { }) return logarithmDivisionResult;

// Last, because it is the only one here that asks for a limit of its own and so is
// the only one whose cost is another walk of the machinery. Everything above reads
// the expression where it stands.
// Last, because its cost is another walk of the machinery over an expression no
// smaller than this one -- unlike the rule above, whose sub-limits are subtrees. The
// readers before both of them settle the expression where it stands.
var boundedResult = LimitSolvers.SolveAsBoundedTimesVanishing(expr, x);
if (boundedResult is { }) return boundedResult;

Expand Down Expand Up @@ -144,6 +164,18 @@ private static Entity ExpandLogarithm(Entity expr)
};

public static Entity? ComputeLimit(Entity expr, Variable x, Entity dest, ApproachFrom side = ApproachFrom.BothSides, bool acceptNaN = false)
{
// The approach is stated for the whole computation, not only where the destination
// has been normalised to +oo. Everything below simplifies as it goes, and a rule that
// may only fire while the approach is in scope is otherwise declining through most of
// the work -- which is not a wrong answer but is a slower one, since what it declines
// to collapse the search then has to explore.
var enclosingApproach = EnterApproach(x, dest);
try { return ComputeLimitWithinApproach(expr, x, dest, side, acceptNaN); }
finally { LeaveApproach(enclosingApproach); }
}

private static Entity? ComputeLimitWithinApproach(Entity expr, Variable x, Entity dest, ApproachFrom side, bool acceptNaN)
{
// A piecewise is not continuous and is still something a limit can be taken of: it
// agrees with one of its cases on the whole of the way in, and that case is
Expand Down Expand Up @@ -278,9 +310,21 @@ private static Entity ExpandLogarithm(Entity expr)
// by substituting for x, but there it would be replacing answers the rules
// above already give rather than adding ones they do not -- a change worth
// making on its own evidence and not as a side effect of this.
if (Gruntz.LimitToPositiveInfinity(
dest.Evaled is Real { IsNegative: true } ? expr.Substitute(x, -x) : expr, x)
is { } byGruntz && byGruntz.Evaled != MathS.NaN)
// Gruntz reads everything on its way to +oo -- a negative destination is
// normalised by substituting -x, exactly as above -- and it simplifies as it
// goes, so the approach is stated for it too. This is the one that carries
// lim x->-oo (x-5)^x / x^x: what the substitution leaves is
// ln(-x) - ln(-(x+5)), both operands negative, gathered inside the
// simplifier and nowhere a rewrite of ours can reach.
var gruntzApproach = EnterApproach(x, Real.PositiveInfinity);
Entity? byGruntz;
try
{
byGruntz = Gruntz.LimitToPositiveInfinity(
dest.Evaled is Real { IsNegative: true } ? expr.Substitute(x, -x) : expr, x);
}
finally { LeaveApproach(gruntzApproach); }
if (byGruntz is { } && byGruntz.Evaled != MathS.NaN)
return byGruntz;
return atInfinity;
}
Expand Down
148 changes: 148 additions & 0 deletions Sources/AngouriMath/Functions/Continuous/Limits/Transformations.cs
Original file line number Diff line number Diff line change
Expand Up @@ -232,6 +232,154 @@ private static bool IsEventuallyPositive(Entity expr, Variable x, Entity dest)
return limit == Real.PositiveInfinity || limit is Real { IsPositive: true };
}

/// <summary>
/// The sign an expression settles on approaching <paramref name="dest"/>: <c>1</c> where
/// it stays positive, <c>-1</c> where it stays negative, <c>0</c> where neither can be
/// read -- a limit of zero, a non-real one, or none at all.
/// </summary>
private static int SignOnTheApproach(Entity expr, Variable x, Entity dest)
{
var limit = EvalAssumingContinuous(expr.Limit(x, dest));
if (limit == Real.PositiveInfinity) return 1;
if (limit == Real.NegativeInfinity) return -1;
return limit switch
{
Real { IsPositive: true } => 1,
Real { IsNegative: true } => -1,
_ => 0
};
}

/// <summary>
/// <see cref="SignOnTheApproach"/>, asked once per expression per approach. An
/// <see cref="Entity"/> hashes structurally, so the same operand written the same way is
/// the same key.
/// </summary>
private static int MemoisedSign(Entity expr, Approach approach)
{
var key = (approach.Dest, expr);
if (signMemo is { } memo && memo.TryGetValue(key, out var known))
return known;
var sign = SignOnTheApproach(expr, approach.X, approach.Dest);
if (signMemo is { } store)
store[key] = sign;
return sign;
}

/// <summary>
/// How deep <see cref="MayGatherLogarithmsHere"/> may re-enter itself. It asks for a
/// limit per operand, and those limits run the machinery the question was asked from.
/// </summary>
private const int MaxGatherLogarithmsDepth = 1;

[System.ThreadStatic] private static int gatherLogarithmsDepth;

/// <summary>
/// The approach the limit machinery is currently reading an expression on, or
/// <see langword="null"/> where an expression is being simplified on its own account.
/// </summary>
/// <remarks>
/// This is the one thing a simplification rule cannot work out for itself and the limit
/// machinery can: *where the expression is going*. <c>ln(a) + ln(b) = ln(a*b)</c> is
/// false off the positive reals, so <c>Simplify</c> may not apply it to a symbol -- but
/// on a stated approach the sign of each operand is decidable, and where the two signs
/// agree the identity is exact. Without this the rule would have to be either unsound
/// (as it was) or absent, and absent costs termination rather than coverage: the limit
/// machinery's own expansion creates logarithm pairs that only this can put back
/// together. https://github.com/asc-community/AngouriMath/issues/721
/// <para/>
/// Thread-static because the limit machinery is synchronous and every other setting here
/// is; it is swapped rather than set, so a nested reading restores the outer one.
/// </remarks>
[System.ThreadStatic] private static Approach? currentApproach;

/// <summary>
/// A destination being approached, and the signs already established against it.
/// </summary>
/// <remarks>
/// The memo is not an optimisation to be taken or left. The rule is asked once per match
/// per candidate the simplifier generates, and it is asked about the *same* operands over
/// and over: <c>lim x-&gt;-oo (x-5)^x / x^x</c> put the same pair to it 192 times. Each
/// answer costs two limits, which run this whole machinery, so without the memo the
/// #596 limit stops finishing inside the minute its own test allows it.
/// </remarks>
internal readonly record struct Approach(Variable X, Entity Dest);

/// <summary>
/// The signs already established, keyed by the destination they were established against
/// as well as by the expression, and shared by every approach inside the outermost one.
/// </summary>
/// <remarks>
/// A memo per approach is very nearly no memo at all: the limit machinery re-enters
/// itself constantly and asks about the same operands each time -- one computation put
/// the same pair to the rule 192 times, and each answer costs two limits, which run this
/// whole machinery. It is dropped when the outermost approach is left, so nothing
/// survives a call.
/// </remarks>
[System.ThreadStatic] private static Dictionary<(Entity Dest, Entity Expr), int>? signMemo;

[System.ThreadStatic] private static int approachDepth;

/// <summary>
/// States that <paramref name="x"/> is being read on its way to <paramref name="dest"/>,
/// and returns the previous approach for <see cref="LeaveApproach"/> to put back.
/// </summary>
internal static Approach? EnterApproach(Variable x, Entity dest)
{
var previous = currentApproach;
approachDepth++;
signMemo ??= new();
currentApproach = new Approach(x, dest);
return previous;
}

/// <summary>
/// Puts back what <see cref="EnterApproach"/> returned, and drops the memo once the
/// outermost approach is left.
/// </summary>
internal static void LeaveApproach(Approach? previous)
{
currentApproach = previous;
if (--approachDepth == 0)
signMemo = null;
}

/// <summary>
/// Installs <paramref name="approach"/> as the current one and returns the previous, for
/// the caller to put back.
/// </summary>
internal static Approach? SwapApproach(Approach? approach)
{
var previous = currentApproach;
currentApproach = approach;
return previous;
}

/// <summary>
/// Whether the simplifier's logarithm gathering may fire here, which it may only while
/// an approach is being read and only where the operands hold their sign on it.
/// </summary>
/// <remarks>
/// The approach is withdrawn for the duration of the check, so that the limits it asks
/// for cannot come back through this same door -- conservative, and it terminates.
/// </remarks>
internal static bool MayGatherLogarithmsHere(Entity left, Entity right, bool isDifference)
{
if (currentApproach is not { } approach || gatherLogarithmsDepth >= MaxGatherLogarithmsDepth)
return false;
gatherLogarithmsDepth++;
var previous = SwapApproach(null);
try
{
var leftSign = MemoisedSign(left, approach);
if (leftSign == 0)
return false;
var rightSign = MemoisedSign(right, approach);
return isDifference ? leftSign == rightSign : leftSign == 1 && rightSign == 1;
}
finally { SwapApproach(previous); gatherLogarithmsDepth--; }
}

/// <summary>
/// How many times over <see cref="ApplySecondRemarkable"/> may be re-read into an
/// expression that <see cref="SimplifyAndComputeLimitToInfinity"/>'s simplification
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -196,8 +196,22 @@ when IsPositiveReal(any2) && MayBeTakenAsReal(any3) => any3 * MathS.Log(any1, an
Logf(Divf(Integer(1), var any1), var any2) => -MathS.Log(any1, any2),


Sumf(Logf(var any3, var any1), Logf(var any3a, var any2)) when any3 == any3a => any3.Log(any1 * any2),
Minusf(Logf(var any3, var any1), Logf(var any3a, var any2)) when any3 == any3a => any3.Log(any1 / any2),
// ln(a) + ln(b) = ln(a*b), and the difference likewise, are false off the positive
// reals: at x = -3 the sum of ln(x) and ln(x+1) exceeds ln(x*(1+x)) by 2*pi*i, the
// turn of the argument the principal branch discards. Both were applied
// unconditionally, and that was the last disagreement `boundcheck` reported.
//
// Two ways to earn them. Either the operands are decidably positive here, or the
// limit machinery is reading the expression towards a destination and has
// established that they hold their sign on the way to it -- which is the only thing
// that can discharge the condition for a symbol, and is what the identity is for.
// Withdrawing it outright does not merely cost coverage: the limit machinery's own
// expansion creates the pairs, so nothing puts them back and some limits stop
// terminating. https://github.com/asc-community/AngouriMath/issues/721
Sumf(Logf(var any3, var any1), Logf(var any3a, var any2)) when any3 == any3a
&& MayGatherLogarithms(any1, any2, isDifference: false) => any3.Log(any1 * any2),
Minusf(Logf(var any3, var any1), Logf(var any3a, var any2)) when any3 == any3a
&& MayGatherLogarithms(any1, any2, isDifference: true) => any3.Log(any1 / any2),

// sqrt(8) = 2 * sqrt(2), cbrt(54) = 3 * cbrt(2)
Powf(Integer { IsPositive: true } radicand, Rational and not Integer and var power)
Expand Down Expand Up @@ -309,6 +323,15 @@ internal static Entity GatherPowersOfOneBase(Entity x)
private static bool IsPositiveReal(Entity entity)
=> entity.Evaled is Real { EDecimal.IsFinite: true } value && value.IsPositive;

/// <summary>
/// Whether two antilogarithms may be gathered into one: because both are decidably
/// positive numbers, or because a limit is being read and they hold their sign on the
/// approach to its destination.
/// </summary>
private static bool MayGatherLogarithms(Entity left, Entity right, bool isDifference)
=> (IsPositiveReal(left) && IsPositiveReal(right))
|| Algebra.LimitFunctional.MayGatherLogarithmsHere(left, right, isDifference);

/// <summary>
/// Whether this operand may be taken as real: because the expression is being read as a
/// real-valued one, because the node's own declared codomain says so, or because its value
Expand Down
Loading
Loading