Skip to content

Four rewrite rules hold only where they are written to #2434

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Rafael-SOWNet wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Four rewrite rules hold only where they are written to #2434

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
8c1e96f
Gather a quotient of powers with a whole exponent factor only where i…
Rafael-SOWNet Nov 13, 2026
60be679
Decide a chain of comparisons by transitivity only where its operands…
Rafael-SOWNet Nov 13, 2026
3ed79e1
Turn an inverse function of a numeric reciprocal only for a nonzero n…
Rafael-SOWNet Nov 13, 2026
6178967
Cancel a sign times a thing over its absolute value only for a real o…
Rafael-SOWNet Nov 13, 2026
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
56 changes: 56 additions & 0 deletions BREAKING-CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,20 @@ divisor answers at once. A two-sided limit is not changed. Found by limitcheck;
| `"arcsin(-x * log(-1, x))".ToEntity().Limit("x", 0, ApproachFrom.Right)` | `limitright(arcsin(-x * log(-1, x)), x, 0)` | `0` |
| `"x * log(2 + x, x)".ToEntity().Limit("x", 0, ApproachFrom.Right)` | `0` after 27 s | `0` in 0.25 s |

### A quotient of powers whose exponents differ by a whole factor is gathered only where that holds

**Silent: `a^n / b^(c*n)` and `a^(c*n) / b^n` are no longer gathered into one power unless `n` is whole or both
bases are positive reals**, the condition `a^n / b^n -> (a/b)^n` has carried since
[#802](https://github.com/asc-community/AngouriMath/issues/802). The two rules gathering a whole factor `c` had no
guard. At `x = 1, y = -1, n = 1/2` the quotient `x^n / y^(2n)` is `1 / (-1)^1 = -1`, while the gathered
`(x / y^2)^n` is `1`. Found by the v3 definedness specification; no issue was filed.

| Input | Was (2.6.0) | Now |
|---|---|---|
| `"x^n/y^(2*n)".ToEntity().Simplify()` | `(x / y ^ 2) ^ n` | `x ^ n / y ^ (2 * n)` |
| `"x^(2*n)/y^n".ToEntity().Simplify()` | `(x ^ 2 / y) ^ n` | `x ^ (2 * n) / y ^ n` |
| `"2^n/3^(2*n)".ToEntity().Simplify()` | `(2/9) ^ n` | `(2/9) ^ n`, unchanged |

### A product with a power for a factor is read by the power's exponent's limit in a one-sided limit

**Silent: a one-sided limit of a product whose factors tend to 0 and to an infinity, one of them a power `u^v` whose
Expand All @@ -71,6 +85,22 @@ limitcheck; no issue was filed.
| `"(tan(x) + 1)^(x^(x - 1))".ToEntity().Limit("x", 0, ApproachFrom.Right)` | `limitright((tan(x) + 1) ^ x ^ (x - 1), x, 0)` | `e` |
| `"tan(x) * x^(x - 1)".ToEntity().Limit("x", 0, ApproachFrom.Right)` | `1` after 11 s | `1` in 0.21 s |

### A chain of comparisons is decided by transitivity only where its operands are ordered

**Silent: `(a > b and b > c) implies a > c`, and the same with `<`, is no longer simplified to `True` for symbols
over the complex plane.** An order comparison has no truth value off the real line, so at `a = i, b = 1, c = 0`
the implication is `NaN`, and the answer `True` gave it one. It is still `True` over the reals
(`MathS.Settings.Codomain` set to `Domain.Real`) and for operands known to be real. A condition `a in RR` cannot be
attached instead, as `x > x` attaches it ([#876](https://github.com/asc-community/AngouriMath/issues/876)): at
`a = i, b = 0, c = 1` the conjunction is false and the implication is `True`. Found by the v3 definedness
specification; no issue was filed.

| Input | Was (2.6.0) | Now |
|---|---|---|
| `"((a > b) and (b > c)) implies (a > c)".ToEntity().Simplify()` | `True` | `a > b and b > c implies a > c` |
| `"((a < b) and (b < c)) implies (a < c)".ToEntity().Simplify()` | `True` | `a < b and b < c implies a < c` |
| the same over `Domain.Real` | `True` | `True`, unchanged |

### A derivative keeps an exponent that is not rational exact

**Silent: the power rule writes a constant exponent that is not rational as it is, where it wrote its decimal
Expand All @@ -87,6 +117,19 @@ rational exponent is still written as its value. Found by limitcheck; no issue w
| `"x^(abs(x)^arctan(2))".ToEntity().Limit("x", 0, ApproachFrom.Left)` | unevaluated | `1` |
| `"x^(abs(x)^arctan(2))".ToEntity().Limit("x", 0, ApproachFrom.Right)` | unevaluated | `1` |

### An inverse function of a zero over a symbol is not turned into its reciprocal function

**Silent, through the rule registry only: `arcsin(0 / x)` is no longer rewritten to `arccsc(x / 0)` by
`RewriteRules.Trigonometric`, nor `arccos(0 / x)` to `arcsec(x / 0)`.** The rules read `n / d` as `1 / (d / n)`,
which needs a nonzero `n`; at `n = 0` the input is `0` (or `pi / 2`) wherever `x` is not `0`, and the answer has no
value. `Simplify` folds `0 / x` before the rules are asked, so its answers do not change. Found by the v3
definedness specification; no issue was filed.

| Input | Was (2.6.0) | Now |
|---|---|---|
| `Transformation.Rewriting(RewriteRules.Trigonometric).ApplyOrKeep("arcsin(0/x)")` | `arccsc(x / 0)` | `arcsin(0 / x)` |
| `Transformation.Rewriting(RewriteRules.Trigonometric).ApplyOrKeep("arccos(0/x)")` | `arcsec(x / 0)` | `arccos(0 / x)` |

### A two-sided limit whose sides are undecided is left unevaluated

**Silent: a two-sided limit is left unevaluated, rather than `NaN`, where a side's limit stops at an indeterminate form
Expand Down Expand Up @@ -114,6 +157,19 @@ limit is still `NaN`. Found by limitcheck; no issue was filed.
| `"1 / log(x^2, cos(x))".ToEntity().Limit("x", 0)` | `-oo` | `limit(1 / log(x ^ 2, cos(x)), x, 0)` |
| `"1 / (x * arccot(x))".ToEntity().Limit("x", 0)` | `NaN` | `limit(1 / (x * arccotan(x)), x, 0)` |

### A sign times a thing over its absolute value cancels only for a real operand

**Silent, through the rule registry only: `sgn(x) * (y * x) / abs(x)` is no longer rewritten to
`y provided not x = 0` by `RewriteRules.Common` for an `x` not known to be real.** `sgn(x)` is `x / abs(x)`, so the
quotient is `y * x^2 / abs(x)^2`, which is `-y` at `x = i`. Over the reals (`MathS.Settings.Codomain` set to
`Domain.Real`) and for an operand known to be real it still cancels. `Simplify` sorts the product before the rule is
asked, so its answers do not change. Found by the v3 definedness specification; no issue was filed.

| Input | Was (2.6.0) | Now |
|---|---|---|
| `Transformation.Rewriting(RewriteRules.Common).ApplyOrKeep("sgn(x)*(y*x)/abs(x)")` | `y provided not x = 0` | `sgn(x) * y * x / abs(x)` |
| the same over `Domain.Real` | `y provided not x = 0` | `y provided not x = 0`, unchanged |

### A limit at the jump of a step function is not answered by substitution

**Silent: a limit of an expression built on `floor`, `ceil`, `round` or `sgn`, where the step's argument arrives on one
Expand Down
39 changes: 34 additions & 5 deletions Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2057,12 +2057,15 @@ is var (divided, remainder)
// larger the angle is.
growth: RewriteRuleGrowth.Collects),

// The four rules below are the definitions arccsc(z) = arcsin(1 / z) and its siblings,
// read through n / d = 1 / (d / n), which holds for a nonzero n. At n = 0 the left
// side is arcsin(0) = 0 and the right arccsc(d / 0), which has no value.
new MatchedRule(
"an-arcsine-of-a-numeric-reciprocal-is-an-arccosecant",
MatchPattern.Node<Arcsinf>(MatchPattern.Node<Divf>(MatchPattern.Any("n"), MatchPattern.Any("d"))),
bound => new Arccosecantf(bound["d"] / bound["n"]),
Soundness.SoundUnderAssumptions,
when: bound => bound["n"] is Number && bound["d"] is not Number,
when: bound => bound["n"] is Number && bound["n"] != Integer.Zero && bound["d"] is not Number,
description: "arcsin(1 / c) = arccosec(c), for a numeric c",
// One inverse function becomes another and the quotient stays a quotient with its
// operands the other way round, so the two are the same size whatever they are.
Expand All @@ -2073,7 +2076,7 @@ is var (divided, remainder)
MatchPattern.Node<Arccosf>(MatchPattern.Node<Divf>(MatchPattern.Any("n"), MatchPattern.Any("d"))),
bound => new Arcsecantf(bound["d"] / bound["n"]),
Soundness.SoundUnderAssumptions,
when: bound => bound["n"] is Number && bound["d"] is not Number,
when: bound => bound["n"] is Number && bound["n"] != Integer.Zero && bound["d"] is not Number,
description: "arccos(1 / c) = arcsec(c), for a numeric c",
// One inverse function becomes another and the quotient stays a quotient with its
// operands the other way round, so the two are the same size whatever they are.
Expand All @@ -2084,7 +2087,7 @@ is var (divided, remainder)
MatchPattern.Node<Arccosecantf>(MatchPattern.Node<Divf>(MatchPattern.Any("n"), MatchPattern.Any("d"))),
bound => new Arcsinf(bound["d"] / bound["n"]),
Soundness.SoundUnderAssumptions,
when: bound => bound["n"] is Number && bound["d"] is not Number,
when: bound => bound["n"] is Number && bound["n"] != Integer.Zero && bound["d"] is not Number,
description: "arccosec(1 / c) = arcsin(c), for a numeric c",
// One inverse function becomes another and the quotient stays a quotient with its
// operands the other way round, so the two are the same size whatever they are.
Expand All @@ -2095,7 +2098,7 @@ is var (divided, remainder)
MatchPattern.Node<Arcsecantf>(MatchPattern.Node<Divf>(MatchPattern.Any("n"), MatchPattern.Any("d"))),
bound => new Arccosf(bound["d"] / bound["n"]),
Soundness.SoundUnderAssumptions,
when: bound => bound["n"] is Number && bound["d"] is not Number,
when: bound => bound["n"] is Number && bound["n"] != Integer.Zero && bound["d"] is not Number,
description: "arcsec(1 / c) = arccos(c), for a numeric c",
// One inverse function becomes another and the quotient stays a quotient with its
// operands the other way round, so the two are the same size whatever they are.
Expand Down Expand Up @@ -2548,17 +2551,26 @@ is var (divided, remainder)
bound => Functions.Patterns.PushNotInside(Orf.LinearChildren((Orf)bound["chain"]), disjoin: false),
Soundness.Sound,
description: "not (a or b or ...) = (not a) and (not b) and ..."),
// Transitivity is a fact about an order, so the pair below fires only where the
// three operands are known to be ordered. Elsewhere the implication need not have a
// truth value -- at a = i, b = 1, c = 0 it is NaN -- and the ordered condition cannot
// be attached instead, as its siblings attach it: a comparison with no truth value
// inside a conjunction that is already false leaves the implication true, so at
// a = i, b = 0, c = 1 the chain of greaters is True and `True provided a in RR` is
// not. https://github.com/asc-community/AngouriMath/issues/876
new MatchedRule(
"a-chain-of-greaters-implies-its-own-ends",
MatchPattern.Node<Impliesf>(MatchPattern.Node<Andf>(MatchPattern.Node<Greaterf>(MatchPattern.Any("a"), MatchPattern.Any("b")), MatchPattern.Node<Greaterf>(MatchPattern.Any("b"), MatchPattern.Any("c"))), MatchPattern.Node<Greaterf>(MatchPattern.Any("a"), MatchPattern.Any("c"))),
bound => Entity.Boolean.True.Provided(bound["a"].DomainCondition).Provided(bound["b"].DomainCondition).Provided(bound["c"].DomainCondition),
Soundness.SoundUnderAssumptions,
when: bound => Functions.Patterns.AreOrdered(bound["a"], bound["b"], bound["c"]),
description: "(((a > b) and (b > c)) implies (a > c)) = True"),
new MatchedRule(
"a-chain-of-lesss-implies-its-own-ends",
MatchPattern.Node<Impliesf>(MatchPattern.Node<Andf>(MatchPattern.Node<Lessf>(MatchPattern.Any("a"), MatchPattern.Any("b")), MatchPattern.Node<Lessf>(MatchPattern.Any("b"), MatchPattern.Any("c"))), MatchPattern.Node<Lessf>(MatchPattern.Any("a"), MatchPattern.Any("c"))),
bound => Entity.Boolean.True.Provided(bound["a"].DomainCondition).Provided(bound["b"].DomainCondition).Provided(bound["c"].DomainCondition),
Soundness.SoundUnderAssumptions,
when: bound => Functions.Patterns.AreOrdered(bound["a"], bound["b"], bound["c"]),
description: "(((a < b) and (b < c)) implies (a < c)) = True"),
new MatchedRule(
"a-equals-with-zero-on-the-left-turns-round",
Expand Down Expand Up @@ -3086,6 +3098,13 @@ is var (divided, remainder)
MatchPattern.Any("n")))),
bound => new Powf(bound["a"] / new Powf(bound["b"], bound["c"]), bound["n"]),
Soundness.SoundUnderAssumptions,
// The guard of the quotient rule above, for the same reason: b ^ (c * n) is
// (b ^ c) ^ n, and a ^ n / (b ^ c) ^ n is (a / b ^ c) ^ n, only for a whole n or
// positive real bases. At a = 1, b = -1, n = 1/2 the quotient is
// 1 / (-1) ^ 1 = -1 and the gathered power (1 / 1) ^ (1/2) = 1.
when: bound => bound["n"] is Integer
|| (bound["a"].Evaled is Real { IsPositive: true }
&& bound["b"].Evaled is Real { IsPositive: true }),
description: "a ^ n / b ^ (c * n) = (a / b ^ c) ^ n, for a positive whole c",
// The exponent is matched twice and written once, and one power node goes: the delta
// is -(1 + |n|), at most -2 and further the larger the exponent is.
Expand All @@ -3102,6 +3121,11 @@ is var (divided, remainder)
MatchPattern.Node<Powf>(MatchPattern.Any("b"), MatchPattern.Any("n"))),
bound => new Powf(new Powf(bound["a"], bound["c"]) / bound["b"], bound["n"]),
Soundness.SoundUnderAssumptions,
// Guarded as its mirror is: at a = -1, b = 1, n = 1/2 the quotient is -1 and the
// gathered power ((-1) ^ 2 / 1) ^ (1/2) is 1.
when: bound => bound["n"] is Integer
|| (bound["a"].Evaled is Real { IsPositive: true }
&& bound["b"].Evaled is Real { IsPositive: true }),
description: "a ^ (c * n) / b ^ n = (a ^ c / b) ^ n, for a positive whole c",
// The exponent is matched twice and written once, and one power node goes with it:
// the delta is -(1 + |n|), the mirror of the rule that takes it into the divisor.
Expand Down Expand Up @@ -4017,7 +4041,12 @@ is var (divided, remainder)
MatchPattern.Node<Divf>(MatchPattern.Node<Mulf>(MatchPattern.Node<Signumf>(MatchPattern.Any("a")), MatchPattern.Node<Mulf>(MatchPattern.Any("b"), MatchPattern.Any("a"))), MatchPattern.Node<Absf>(MatchPattern.Any("a"))),
bound => bound["b"].Provided(!bound["a"].EqualTo(Integer.Zero)),
Soundness.SoundUnderAssumptions,
description: "(sgn(a) * (b * a)) / abs(a) = b, provided a is not zero",
// sgn(a) is a / abs(a), so sgn(a) * a / abs(a) is a^2 / abs(a)^2: 1 for a real a and
// not otherwise -- at a = i it is -1. Realness is a reading, not a condition on
// where either side is defined, so it is decided here, as the comparison rules
// decide it, and the rule does not fire on an operand not known to be real.
when: bound => Functions.Patterns.OrderedConditionFor(bound["a"]) == Entity.Boolean.True,
description: "(sgn(a) * (b * a)) / abs(a) = b, for a real a, provided a is not zero",
// Three copies of a go and one comes back inside the condition; the sign, the
// absolute value, the quotient and two products go against the three nodes the
// condition and its attachment add: the delta is -1 - 2|a|, at most -3.
Expand Down
3 changes: 2 additions & 1 deletion Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Common.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -263,7 +263,8 @@ internal static Integer DenominatorOf(Entity entity)

Mulf(Absf(var any1), Absf(var any2)) => new Absf(any1 * any2),
Divf(Absf(var any1), Absf(var any2)) => new Absf(any1 / any2),
Divf(Mulf(Signumf(var any1), Mulf(var any2, var any1a)), Absf(var any1b)) when any1 == any1a && any1a == any1b => any2.Provided(!any1.EqualTo(Integer.Zero)),
// sgn(a) * a / abs(a) is 1 only for a real a: at a = i it is -1.
Divf(Mulf(Signumf(var any1), Mulf(var any2, var any1a)), Absf(var any1b)) when any1 == any1a && any1a == any1b && OrderedCondition(any1) == Entity.Boolean.True => any2.Provided(!any1.EqualTo(Integer.Zero)),
Mulf(Signumf(var any1), Absf(var any1a)) when any1 == any1a => any1,
Mulf(Absf(var any1a), Signumf(var any1)) when any1 == any1a => any1,

Expand Down
12 changes: 10 additions & 2 deletions Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.EqualityInequality.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,6 +136,14 @@ internal static Entity OrderedConditionOf(Entity comparison, int operand)
/// <inheritdoc cref="OrderedConditionOf"/>
internal static Entity OrderedConditionFor(Entity entity) => OrderedCondition(entity);

/// <summary>
/// Whether every operand is known to be ordered, so that a chain of comparisons between
/// them can be decided by transitivity. Asked rather than attached: see the rule
/// <c>a-chain-of-greaters-implies-its-own-ends</c>.
/// </summary>
internal static bool AreOrdered(params Entity[] operands)
=> operands.All(operand => OrderedCondition(operand) == True);

/// <summary>
/// Whether pushing a <c>not</c> through this conjunction or disjunction leaves the
/// expression no more complex: at most one operand may be something other than a
Expand Down Expand Up @@ -195,10 +203,10 @@ internal static Entity PushNotInside(IEnumerable<Entity> operands, bool disjoin)
=> PushNotInside(Orf.LinearChildren(a), disjoin: false),

Impliesf(Andf(Greaterf(var any1, var any2), Greaterf(var any2a, var any3)), Greaterf(var any1a, var any3a))
when any1 == any1a && any2 == any2a && any3 == any3a => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition),
when any1 == any1a && any2 == any2a && any3 == any3a && AreOrdered(any1, any2, any3) => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition),

Impliesf(Andf(Lessf(var any1, var any2), Lessf(var any2a, var any3)), Lessf(var any1a, var any3a))
when any1 == any1a && any2 == any2a && any3 == any3a => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition),
when any1 == any1a && any2 == any2a && any3 == any3a && AreOrdered(any1, any2, any3) => True.Provided(any1.DomainCondition).Provided(any2.DomainCondition).Provided(any3.DomainCondition),

Equalsf(var zero, var anyButZero) when IsZero(zero) && !IsZero(anyButZero) => anyButZero.EqualTo(zero),
Greaterf(var zero, var anyButZero) when IsZero(zero) && !IsZero(anyButZero) => anyButZero < zero,
Expand Down
15 changes: 13 additions & 2 deletions Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -154,10 +154,21 @@ internal static bool IsWholeOrAnOddRoot(Number n) =>
// These read that pair back. Restricted to a whole c so that nothing gains a
// root it did not have -- b^c goes into the base, rather than the exponent
// being divided. https://github.com/asc-community/AngouriMath/issues/740
// And guarded as the rule above is, since gathering the exponent is the same move:
// at {1} = 1, {2} = -1, n = 1/2 the quotient is 1 / (-1) ^ 1 = -1 and the gathered
// power (1 / 1) ^ (1/2) is 1.
Divf(Powf(var any1, var any3), Powf(var any2, Mulf(Integer { IsPositive: true } const1, var any3a)))
when any3 == any3a => new Powf(any1 / new Powf(any2, const1), any3),
when any3 == any3a
&& (any3 is Integer
|| (any1.Evaled is Real { IsPositive: true }
&& any2.Evaled is Real { IsPositive: true }))
=> new Powf(any1 / new Powf(any2, const1), any3),
Divf(Powf(var any1, Mulf(Integer { IsPositive: true } const1, var any3)), Powf(var any2, var any3a))
when any3 == any3a => new Powf(new Powf(any1, const1) / any2, any3),
when any3 == any3a
&& (any3 is Integer
|| (any1.Evaled is Real { IsPositive: true }
&& any2.Evaled is Real { IsPositive: true }))
=> new Powf(new Powf(any1, const1) / any2, any3),

// x / x^n
Divf(var any1, Powf(var any1a, var any2)) when any1 == any1a => new Powf(any1, 1 - any2),
Expand Down
Loading
Loading