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
20 changes: 20 additions & 0 deletions BREAKING-CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -1558,6 +1558,26 @@ in 2.5.0.
| `forall p in PP : forall a in ZZ : a^p mod p = a mod p` | `UnhandledParseException` | `True` |
| `forall p in PP : forall a, b in ZZ : (a + b)^p = a^p + b^p (mod p)` | `UnhandledParseException` | `True` |

### An equation the solver cannot invert is left unsolved, not answered with no roots

`x! = 6` was answered `{ }`, a claim that it has no roots, and it has 3. The solver isolates `x`
by inverting the function around it, and for a factorial, a binomial coefficient, `mod`, `gcd`,
`lcm`, `min`, `max`, `phi`, `prime`, the valuation, a sum, a product, a limit, a set with `x`
inside it and a few more, the inversion had no way to write the preimage and returned none. Such
an equation is now left unsolved, as the set of `x` for which it holds, the way a statement
the solver has no arm for already was. Roots found beside it are kept. A value these functions
provably never take still has no roots: the factorial is the gamma function one along, which
has no zeros, so `x! = 0` is still `{ }`, and so is `arcsin(x) = 5`.

| Input | Was (2.5.0) | Now |
|---|---|---|
| `"x! = 6".Solve("x")` | `{ }` | `{ x : x! = 6 }` |
| `"x mod 3 = 1".Solve("x")` | `{ }` | `{ x : x mod 3 = 1 }` |
| `"gcd(x, 4) = 2".Solve("x")` | `{ }` | `{ x : gcd(x, 4) = 2 }` |
| `"max(x, 1) = 3".Solve("x")` | `{ }` | `{ x : max(x, 1) = 3 }` |
| `"phi(x) = 4".Solve("x")` | `{ }` | `{ x : phi(x) = 4 }` |
| `"binomial(x, 2) = 3".Solve("x")` | `UnhandledParseException` | `{ x : binomial(x, 2) = 3 }` |

### `binomial(n, k)` is a function

**Addition, not silent.** The binomial coefficient is a node, `Entity.Binomialf`, spelled
Expand Down
3 changes: 3 additions & 0 deletions Sources/.editorconfig
Original file line number Diff line number Diff line change
Expand Up @@ -207,6 +207,9 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed
[Tests/UnitTests/Algebra/SolveTest/NegationIsNotTheEmptySetTest.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/Algebra/SolveTest/AnUnwrittenInverseIsNotTheEmptySetTest.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/Common/LimitTermination.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
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,21 @@ internal static class AnalyticalEquationSolver
/// <param name="expr">Expression</param>
/// <param name="x">Variable to solve over</param>
internal static Set Solve(Entity expr, Variable x, bool compensateSolving = false)
{
// An inversion that could not write its preimage leaves this equation unsolved, as
// the set of x for which it holds. At this level and no further out, so the roots
// found beside it stay: (x - 1) x! = 0 is { 1 } and the x with x! = 0.
try
{
return SolveInverting(expr, x, compensateSolving);
}
catch (CannotInvertException)
{
return new ConditionalSet(x, (compensateSolving ? expr : expr.InnerSimplified).Equalizes(0));
}
}

private static Set SolveInverting(Entity expr, Variable x, bool compensateSolving)
{
if (!compensateSolving) expr = expr.InnerSimplified; // don't simplify away the 0 on the right hand side of the subtraction
if (expr == x)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -71,9 +71,9 @@ partial record Modf
{
// x % a = value has one solution per period, so inverting it means introducing
// an integer parameter the way the trigonometric inversions do. Until that is
// written, no solutions is the honest answer -- a wrong one would be worse.
// written the equation is left unsolved: no solutions would claim it has none.
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> Enumerable.Empty<Entity>();
=> throw new CannotInvertException();
}

partial record Powf
Expand Down Expand Up @@ -212,18 +212,21 @@ private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x

partial record Factorialf
{
// TODO: Inverse of factorial not implemented yet
// The factorial is the gamma function one along, and the gamma function has no
// zeros anywhere in the complex plane, so x! = 0 has no roots. Every other value
// has some -- x! = 6 at 3 -- and no node here writes them.
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x) =>
Enumerable.Empty<Entity>();
value is Integer { IsZero: true } ? Enumerable.Empty<Entity>() : throw new CannotInvertException();
}

partial record Binomialf
{
// The preimage of a binomial coefficient is not a function of either argument
// that can be undone: binomial(n, k) = binomial(n, n - k), and 1 is taken at
// every (n, 0) and (n, n).
// every (n, 0) and (n, n). It has one all the same -- binomial(x, 2) = 3 at 3 and
// at -2 -- so the equation is left unsolved rather than answered with none.
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x) =>
Enumerable.Empty<Entity>();
throw new CannotInvertException();
}

partial record Derivativef
Expand All @@ -250,49 +253,50 @@ partial record Maximumf
{
// The unknown sits under a binder; see Summationf below.
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x) =>
Enumerable.Empty<Entity>();
throw new CannotInvertException();
}

partial record Minimumf
{
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x) =>
Enumerable.Empty<Entity>();
throw new CannotInvertException();
}

partial record Argmaxf
{
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x) =>
Enumerable.Empty<Entity>();
throw new CannotInvertException();
}

partial record Argminf
{
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x) =>
Enumerable.Empty<Entity>();
throw new CannotInvertException();
}

partial record Summationf
{
// The unknown sits under a binder, and inverting would have to solve for it inside a
// sum whose length may be symbolic. Declining is the honest answer -- and the wrong
// one is on record: solving through an opaque Derivativef returns a non-solution,
// https://github.com/asc-community/AngouriMath/issues/964.
// https://github.com/asc-community/AngouriMath/issues/964. Declining is leaving the
// equation unsolved; no roots would claim it has none.
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x) =>
Enumerable.Empty<Entity>();
throw new CannotInvertException();
}

partial record Productf
{
// Same reasoning as Summationf above.
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x) =>
Enumerable.Empty<Entity>();
throw new CannotInvertException();
}

partial record Limitf
{
// TODO: We can't just do a limit on the inverse function: https://math.stackexchange.com/q/3397326/627798
// We can't just do a limit on the inverse function: https://math.stackexchange.com/q/3397326/627798
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x) =>
Enumerable.Empty<Entity>();
throw new CannotInvertException();
}

partial record Signumf
Expand Down Expand Up @@ -386,28 +390,28 @@ partial record Minf
// of x. Nothing here can express that, and inventing a branch would answer
// confidently and wrongly, so this declines the way Factorialf and Phif do.
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> Enumerable.Empty<Entity>();
=> throw new CannotInvertException();
}

partial record Maxf
{
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> Enumerable.Empty<Entity>();
=> throw new CannotInvertException();
}

partial record Gcdf
{
// The preimage of a gcd is every pair whose greatest common divisor is the
// value, which is not a function of x that can be undone.
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> Enumerable.Empty<Entity>();
=> throw new CannotInvertException();
}

partial record Lcmf
{
// As for the gcd.
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> Enumerable.Empty<Entity>();
=> throw new CannotInvertException();
}

partial record Boolean
Expand Down Expand Up @@ -564,7 +568,7 @@ partial record FiniteSet
{
// set{,,,} = value
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> this == x ? new[] { value } : Enumerable.Empty<Entity>();
=> this == x ? new[] { value } : throw new CannotInvertException();
}

partial record Interval
Expand All @@ -580,14 +584,14 @@ private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x
return Left.Invert(Right, x).Select(c => c.Provided(MathS.Equality(Right, value)));
else
return Right.Invert(Left, x).Select(c => c.Provided(MathS.Equality(Left, value)));
return Enumerable.Empty<Entity>();
throw new CannotInvertException();
}
}

partial record ConditionalSet
{
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> this == x ? new[] { value } : Enumerable.Empty<Entity>();
=> this == x ? new[] { value } : throw new CannotInvertException();
}

partial record SpecialSet
Expand Down Expand Up @@ -660,7 +664,7 @@ partial record IndexedSetOperation
{
// The unknown sits under a binder; see Summationf.
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> Enumerable.Empty<Entity>();
=> throw new CannotInvertException();
}

partial record Powersetf
Expand All @@ -677,15 +681,15 @@ partial record Valuationf
// valuation(n, p) = k has every multiple of p^k prime to p for a solution, a set the
// inverter cannot hand back.
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> Enumerable.Empty<Entity>();
=> throw new CannotInvertException();
}

partial record Primef
{
// prime(n) = p has the one solution n = pi(p) where p is prime and none otherwise,
// and pi is not a node here; declined the way Phif is.
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> Enumerable.Empty<Entity>();
=> throw new CannotInvertException();
}

partial record Phif
Expand All @@ -694,7 +698,7 @@ partial record Phif
// There is an algorithm to find exactly one solution but we can do no more.
// TODO: Mess with that...
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> Enumerable.Empty<Entity>();
=> throw new CannotInvertException();
}

partial record Cardf
Expand Down Expand Up @@ -728,7 +732,7 @@ partial record Quantifier
{
// The unknown sits under a binder; see Summationf.
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> Enumerable.Empty<Entity>();
=> throw new CannotInvertException();
}

partial record Providedf
Expand Down Expand Up @@ -758,14 +762,14 @@ partial record Application
{
// TODO
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> Enumerable.Empty<Entity>();
=> throw new CannotInvertException();
}

partial record Lambda
{
// TODO
private protected override IEnumerable<Entity> InvertNode(Entity value, Entity x)
=> Enumerable.Empty<Entity>();
=> throw new CannotInvertException();
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -319,6 +319,16 @@ private static Set Filtered(FiniteSet listed, ConditionalSet condition, Entity s
/// <summary>How large a modulus is tried residue by residue for a congruence that is not linear.</summary>
private const int LargestModulusTried = 4096;

/// <summary>
/// The equation as it was written where the solver left the whole of it unsolved: the
/// solver works on <c>left - right = 0</c>, and <c>{ x : x! = 6 }</c> reads better than
/// <c>{ x : x! - 6 = 0 }</c>, which says the same.
/// </summary>
private static Set AsWritten(Set solved, Entity difference, Entity equation, Variable x)
=> solved is ConditionalSet { Predicate: Equalsf(var rearranged, Integer { IsZero: true }) } && rearranged == difference.InnerSimplified
? new ConditionalSet(x, equation)
: solved;

internal static Set Solve(Entity expr, Variable x)
=> expr switch
{
Expand All @@ -327,7 +337,7 @@ internal static Set Solve(Entity expr, Variable x)

Equalsf(var left, var right) when left is not Set && right is not Set
=> UnsolvedWhereIndependenceIsDenied(
WithoutSpuriousRoots(AnalyticalEquationSolver.Solve(left - right, x), left - right, x),
WithoutSpuriousRoots(AsWritten(AnalyticalEquationSolver.Solve(left - right, x), left - right, expr, x), left - right, x),
expr, x),

Equalsf => Empty,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,16 @@

namespace AngouriMath
{
/// <summary>
/// Thrown by an inversion that cannot write the preimage it is asked for, so that the
/// equation is answered as the set of <c>x</c> for which it holds rather than as the empty
/// set. Caught by the analytical solvers, never seen by a caller.
/// </summary>
internal sealed class CannotInvertException : Core.Exceptions.AngouriMathBaseException
{
internal CannotInvertException() : base("The preimage has no written form") { }
}

partial record Entity : ILatexizeable
{
/// <summary><para>This <see cref="Entity"/> MUST contain exactly ONE occurance of <paramref name="x"/>,
Expand All @@ -27,6 +37,12 @@ internal IEnumerable<Entity> Invert(Entity value, Entity x)
return InvertNode(simplified, x).Where(el => el.IsFinite);
}
/// <summary>Use <see cref="Invert(Entity, Entity)"/> instead which auto-simplifies <paramref name="value"/></summary>
/// <remarks>
/// No roots means the equation has none. A node that cannot write the preimage it is
/// asked for throws <see cref="CannotInvertException"/> instead, and the solver answers
/// the equation as unsolved. <c>x! = 6</c> has the root 3, and no node here inverts a
/// factorial, so returning no roots answered <c>{ }</c>: a claim that it has none.
/// </remarks>
private protected abstract IEnumerable<Entity> InvertNode(Entity value, Entity x);
/// <summary>
/// Returns true if <paramref name="a"/> is inside a rect with corners <paramref name="from"/>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -30,10 +30,18 @@ internal static Set Solve(Entity left, Entity right, Variable x)
+
right.DirectChildren.Count<Entity>(c => c == x) != 1)
return Empty;
if (left.ContainsNode(x))
return left.Invert(right, x).ToSet();
else
return right.Invert(left, x).ToSet();
// As in the equation solver, an inversion with no written form leaves it unsolved.
try
{
if (left.ContainsNode(x))
return left.Invert(right, x).ToSet();
else
return right.Invert(left, x).ToSet();
}
catch (CannotInvertException)
{
return new ConditionalSet(x, left.EqualTo(right));
}
}
}
}
Loading
Loading