Skip to content

A factor of -1 is a sign, not a factor to take out (#1167) #1172

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

Merged
Rafael-SOWNet merged 1 commit into from
Sep 5, 2026
Merged

A factor of -1 is a sign, not a factor to take out (#1167) #1172

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
23 changes: 16 additions & 7 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 @@ -1023,12 +1023,18 @@ is var (divided, remainder)
// one node for one.
growth: RewriteRuleGrowth.Rearranges),

// (-a * x) * y -> -(a * (x * y)), the negative factor either way round
// (-a * x) * y -> -(a * (x * y)), the negative factor either way round.
// A factor of -1 is declined here and in the three rules below it: its magnitude is 1,
// so "taking the factor out" leaves a literal `1 *` behind that says nothing, and the
// numerator rule and the denominator rule then undo each other around it -- `-x / (-y)`
// grew by four nodes a pass for ever. -1 is not a factor to take out, it is the sign,
// and the two rules above this one already answer it.
// https://github.com/asc-community/AngouriMath/issues/1167
new MatchedRule(
"a-negative-factor-in-a-left-product-comes-out",
MatchPattern.Node<Mulf>(
MatchPattern.Commutative<Mulf>(
MatchPattern.Any<Real>("n", value => value.IsNegative),
MatchPattern.Any<Real>("n", value => value.IsNegative && value != -1),
MatchPattern.Any("x")),
MatchPattern.Any("y")),
bound => -((-(Real)bound["n"]) * (bound["x"] * bound["y"])),
Expand All @@ -1040,12 +1046,13 @@ is var (divided, remainder)
// 63 firings over the corpus.
growth: RewriteRuleGrowth.Expands),

// (-a * x) / y -> -(a * (x / y))
// (-a * x) / y -> -(a * (x / y)). Declines -1; see the left-product rule above, and
// note that this rule and the denominator one below are the pair that cycled.
new MatchedRule(
"a-negative-factor-in-a-numerator-comes-out",
MatchPattern.Node<Divf>(
MatchPattern.Commutative<Mulf>(
MatchPattern.Any<Real>("n", value => value.IsNegative),
MatchPattern.Any<Real>("n", value => value.IsNegative && value != -1),
MatchPattern.Any("x")),
MatchPattern.Any("y")),
bound => -((-(Real)bound["n"]) * (bound["x"] / bound["y"])),
Expand All @@ -1056,13 +1063,13 @@ is var (divided, remainder)
// at +2 on all 63 firings over the corpus.
growth: RewriteRuleGrowth.Expands),

// y * (-a * x) -> -(a * (x * y))
// y * (-a * x) -> -(a * (x * y)). Declines -1; see the left-product rule above.
new MatchedRule(
"a-negative-factor-in-a-right-product-comes-out",
MatchPattern.Node<Mulf>(
MatchPattern.Any("y"),
MatchPattern.Commutative<Mulf>(
MatchPattern.Any<Real>("n", value => value.IsNegative),
MatchPattern.Any<Real>("n", value => value.IsNegative && value != -1),
MatchPattern.Any("x"))),
bound => -((-(Real)bound["n"]) * (bound["x"] * bound["y"])),
Soundness.Sound,
Expand All @@ -1074,12 +1081,14 @@ is var (divided, remainder)
// y / (-a * x) -> -(y / (a * x)). What is left stays under the line: written the
// other way, as the numerator rules above are, the quotient came back inverted --
// https://github.com/asc-community/AngouriMath/issues/936 and the note on the switch.
// Declines -1; see the left-product rule above, and note that this rule and the
// numerator one are the pair that cycled.
new MatchedRule(
"a-negative-factor-in-a-denominator-comes-out",
MatchPattern.Node<Divf>(
MatchPattern.Any("y"),
MatchPattern.Commutative<Mulf>(
MatchPattern.Any<Real>("n", value => value.IsNegative),
MatchPattern.Any<Real>("n", value => value.IsNegative && value != -1),
MatchPattern.Any("x"))),
bound => -(bound["y"] / ((-(Real)bound["n"]) * bound["x"])),
Soundness.Sound,
Expand Down
31 changes: 31 additions & 0 deletions Sources/AngouriMath/Docs/Contributing/InversePairTable.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,37 @@ addressability itself for 29 sets.
that: infrastructure that cannot be exercised by the registry as it stands, which is why the first
attempt was reverted rather than shipped.

## A pair that cannot be derived can still be observed

Everything above is about deriving the table — from syntax, or from `MatchPattern`. There is a third
source, and it is neither: **run the sets and watch what comes back**.

`RuleSetsDoNotCycleTest` applies each set to a fixed point over a generated corpus and fails on a term
the set has already produced. Two of the loops it reports are one inverse pair:

```
Power: 1 ^ (-2) * x ^ (-2) -> (1 * x) ^ (-2) -> 1 ^ (-2) * x ^ (-2)
Power: (-2) ^ 2 * (1/2) ^ 2 -> ((-2) * 1/2) ^ 2 -> (-2) ^ 2 * (1/2) ^ 2
```

`two-powers-of-one-exponent-share-a-base` collects `a ^ b * c ^ b` into `(a * c) ^ b`;
`positive-power-of-a-product-distributes` takes it straight back. Nothing derived that. The loop is
the evidence, and the two rule names fall out of reading which arms fired.

What this is and is not:

- **It is a lower bound, and a cheap one.** A pair that never fires on the corpus is invisible to it,
and a pair split across two sets never meets. It cannot enumerate the table.
- **It needs no reversibility mechanism at all**, which is the whole of what makes it available
today: it is behaviour observed at the top of the pipeline, not a property computed about a rule.
- **It answers the question equality saturation actually asks.** The consumer in the opening quote
needs to know which rewrites undo each other *so that it stops*; a pair that provably makes a set
fail to terminate is exactly that, whether or not it is the whole table.

Filed as [#1171](https://github.com/asc-community/AngouriMath/issues/1171), which is a design question
rather than a bug — both rules are correct and each is wanted in its own direction. `Simplify` is
unaffected, because it folds between passes and the shape the second rule needs stops existing.

## What is not decided here

Which of the two real options — generator-level reversibility, or redirecting `Rules` to
Expand Down
21 changes: 13 additions & 8 deletions 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 @@ -44,21 +44,26 @@ internal static partial class Patterns
Mulf(Real { IsNegative: true } num1, Real { IsNegative: true } num2) => (-num1) * (Entity)(-num2),
Divf(Real { IsNegative: true } num1, Real { IsNegative: true } num2) => (-num1) / (Entity)(-num2),

Mulf(Mulf(Real { IsNegative: true } num, var any1), var any2) => -((-num) * (any1 * any2)),
Mulf(Mulf(var any1, Real { IsNegative: true } num), var any2) => -((-num) * (any1 * any2)),
Divf(Mulf(Real { IsNegative: true } num, var any1), var any2) => -((-num) * (any1 / any2)),
Divf(Mulf(var any1, Real { IsNegative: true } num), var any2) => -((-num) * (any1 / any2)),
Mulf(var any2, Mulf(Real { IsNegative: true } num, var any1)) => -((-num) * (any1 * any2)),
Mulf(var any2, Mulf(var any1, Real { IsNegative: true } num)) => -((-num) * (any1 * any2)),
// Each of these eight declines a factor of -1: its magnitude is 1, so taking it out
// leaves a literal `1 *` that says nothing, and the numerator arms and the denominator
// arms then undo each other around it -- -x / (-y) grew by four nodes a pass for ever.
// -1 is not a factor to take out, it is the sign, and the two arms above answer it.
// https://github.com/asc-community/AngouriMath/issues/1167
Mulf(Mulf(Real { IsNegative: true } num, var any1), var any2) when num != -1 => -((-num) * (any1 * any2)),
Mulf(Mulf(var any1, Real { IsNegative: true } num), var any2) when num != -1 => -((-num) * (any1 * any2)),
Divf(Mulf(Real { IsNegative: true } num, var any1), var any2) when num != -1 => -((-num) * (any1 / any2)),
Divf(Mulf(var any1, Real { IsNegative: true } num), var any2) when num != -1 => -((-num) * (any1 / any2)),
Mulf(var any2, Mulf(Real { IsNegative: true } num, var any1)) when num != -1 => -((-num) * (any1 * any2)),
Mulf(var any2, Mulf(var any1, Real { IsNegative: true } num)) when num != -1 => -((-num) * (any1 * any2)),
// A negative factor under the line comes out as a sign in front, and what is left
// stays under the line: a / (-b * c) is -(a / (b * c)), not -(b * (c / a)). Written
// the latter way -- as the four rules above it are, where the negative factor is in
// the numerator and multiplying by it is right -- the quotient came back inverted,
// and Simplify takes whichever candidate is shortest, so the inverted one won
// wherever it was smaller: 1 / (x * (-1 - 1/x)) simplified to -(1 + x), which is its
// reciprocal.
Divf(var any2, Mulf(Real { IsNegative: true } num, var any1)) => -(any2 / ((-num) * any1)),
Divf(var any2, Mulf(var any1, Real { IsNegative: true } num)) => -(any2 / ((-num) * any1)),
Divf(var any2, Mulf(Real { IsNegative: true } num, var any1)) when num != -1 => -(any2 / ((-num) * any1)),
Divf(var any2, Mulf(var any1, Real { IsNegative: true } num)) when num != -1 => -(any2 / ((-num) * any1)),

_ => x
};
Expand Down
55 changes: 41 additions & 14 deletions Sources/Tests/UnitTests/Core/Transformations/RulePriorityTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,13 @@ namespace AngouriMath.Tests.Core.Transformations
[Trait("Area", "Core")]
public sealed class RulePriorityTest
{
private static readonly string[] Leaves = { "x", "y", "2", "-1", "1/2", "0", "1", "3" };
// `-2` earns its place by not being `-1`. Four rules that take a negative factor out of a
// product decline a factor of -1, which is the sign rather than a factor to take out
// (https://github.com/asc-community/AngouriMath/issues/1167) — so with -1 as the only
// negative leaf they matched nothing here and the subsumption claims about them went
// unwitnessed. A corpus whose only negative is the one case a rule excludes cannot
// exercise the rule.
private static readonly string[] Leaves = { "x", "y", "2", "-1", "-2", "1/2", "0", "1", "3" };

private static readonly string[] Unary =
{
Expand Down Expand Up @@ -135,12 +141,26 @@ private static SortedSet<string> Subsumptions()
/// by the wider one too.
/// </summary>
/// <remarks>
/// <para>
/// Over all 322 rules rather than within a set, because the relation is about patterns and
/// nothing about it stops at a set boundary: <b>961</b> ordered pairs claim subsumption,
/// <b>513</b> of them are put to the test by the corpus containing something the narrower
/// pattern matches, and none is contradicted across 56,892 nodes. The count of witnessed
/// claims is asserted as well — a corpus that stopped reaching these shapes would otherwise
/// turn this into a test that passes by asking nothing.
/// <b>501</b> of them are put to the test by the corpus containing something the narrower
/// pattern matches, and none is contradicted across <b>85,153</b> nodes. All three counts
/// are asserted — a corpus that stopped reaching these shapes would otherwise turn this
/// into a test that passes by asking nothing, and a witnessed count means nothing without
/// what it was measured over.
/// </para>
/// <para>
/// <b>Why 501 and not 513.</b> Adding <c>-2</c> to the leaves moved it, and not the way it
/// looks. Measured four ways: on the old leaves the <c>-1</c> guard of
/// <a href="https://github.com/asc-community/AngouriMath/issues/1167">#1167</a> cost 24
/// witnesses (513 to 489), because <c>-1</c> was the only negative leaf and the four
/// guarded rules then matched nothing at all. With <c>-2</c> present the guard costs
/// <b>nothing</b> — 501 either way — which is what says the leaf restores exactly what the
/// guard removed. The remaining 513-to-501 is not coverage at all: <c>level3</c> samples
/// every eleventh element of <c>level2</c>, so a longer <c>level2</c> lands the sample on
/// different expressions.
/// </para>
/// </remarks>
[Fact]
public void SubsumptionIsNeverContradictedByMatching()
Expand Down Expand Up @@ -185,7 +205,11 @@ public void SubsumptionIsNeverContradictedByMatching()
}

Assert.Equal(961, claims.Count);
Assert.Equal(513, witnessed);
Assert.Equal(501, witnessed);
// Asserted so the two figures in the remark above cannot go stale in silence: the
// whole point of `witnessed` is that it is a coverage number, and it means nothing
// without knowing what it was measured over.
Assert.Equal(85153, nodes.Count);
}

/// <summary>
Expand Down Expand Up @@ -370,22 +394,21 @@ public void OnlyTheRecordedConflictsAreLeftToDeclarationOrder()
"Common: a-common-factor-of-two-subtracted-products-comes-out | a-term-subtracted-from-itself-vanishes",
"Common: a-factor-shared-by-a-product-and-a-quotient-added-comes-out | a-negated-term-in-a-sum-is-a-subtraction",
"Common: a-factor-shared-by-a-quotient-and-a-product-added-comes-out | a-negated-term-in-a-sum-is-a-subtraction",
"Common: a-function-times-a-number-puts-the-number-first | a-negated-reciprocal-rational-factor-is-a-negated-division",
"Common: a-function-times-a-number-puts-the-number-first | a-reciprocal-rational-factor-is-a-division",
"Common: a-product-of-two-quotients-is-one-quotient | a-thing-times-itself-is-its-square",
"Common: a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero | a-difference-over-its-own-reverse-is-minus-one",
"Common: a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero | a-shared-factor-cancels-between-two-products",
"Common: a-quotient-times-a-thing-keeps-the-divisor-outermost | a-negated-reciprocal-rational-factor-is-a-negated-division",
"Common: a-quotient-times-a-thing-keeps-the-divisor-outermost | a-reciprocal-rational-factor-is-a-division",
"Common: a-quotient-times-a-thing-keeps-the-divisor-outermost | a-thing-times-a-quotient-keeps-the-divisor-outermost",
"Common: a-quotient-times-a-thing-keeps-the-divisor-outermost | a-thing-times-itself-is-its-square",
"Common: a-term-added-to-itself-doubles | a-negated-term-in-a-sum-is-a-subtraction",
"Common: a-thing-times-a-quotient-keeps-the-divisor-outermost | a-negated-reciprocal-rational-factor-is-a-negated-division",
"Common: a-thing-times-a-quotient-keeps-the-divisor-outermost | a-reciprocal-rational-factor-is-a-division",
"Common: a-thing-times-a-quotient-keeps-the-divisor-outermost | a-thing-times-itself-is-its-square",
"Common: a-variable-times-a-number-puts-the-number-first | a-reciprocal-rational-factor-is-a-division",
"Common: dividing-by-a-quotient-multiplies-by-its-reciprocal | a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero",
"Common: dividing-by-a-quotient-multiplies-by-its-reciprocal | dividing-twice-divides-by-the-product",
"Common: dividing-twice-divides-by-the-product | a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero",
"Common: two-numbers-around-a-factor-collect | a-negated-reciprocal-rational-factor-is-a-negated-division",
"Common: two-numeric-factors-around-a-variable-collect | a-negated-reciprocal-rational-factor-is-a-negated-division",
"Common: two-numbers-around-a-factor-collect | a-reciprocal-rational-factor-is-a-division",
"Common: two-numeric-factors-around-a-variable-collect | a-reciprocal-rational-factor-is-a-division",
"Common: two-numeric-multiples-of-one-variable-add | a-common-factor-of-two-added-products-comes-out",
"Common: two-numeric-multiples-of-one-variable-add | a-negated-term-in-a-sum-is-a-subtraction",
"Common: two-numeric-multiples-of-one-variable-add | a-term-added-to-itself-doubles",
Expand All @@ -394,8 +417,12 @@ public void OnlyTheRecordedConflictsAreLeftToDeclarationOrder()
"Factorization: a-factor-shared-by-two-added-products-comes-out | a-term-added-to-itself-doubles",
"Factorization: a-factor-shared-by-two-subtracted-products-comes-out | a-term-subtracted-from-itself-vanishes",
"Factorization: a-term-added-to-itself-doubles | a-common-factor-is-collected-out-of-a-whole-sum",
"NumericNeat: a-negative-factor-in-a-left-product-comes-out | a-negative-factor-in-a-right-product-comes-out",
"NumericNeat: a-negative-factor-in-a-numerator-comes-out | a-negative-factor-in-a-denominator-comes-out",
// NumericNeat had two entries here and has none. They were
// `a-negative-factor-in-a-left-product-comes-out | ...-right-...` and
// `a-negative-factor-in-a-numerator-comes-out | ...-denominator-...`, and the
// second of those is the pair that undid each other for ever on `-x / (-y)`. All
// four decline a factor of -1 now, so they no longer fire on one node together.
// https://github.com/asc-community/AngouriMath/issues/1167
"Power: a-numeric-factor-comes-out-of-a-power-of-a-product | a-reciprocal-power-is-a-quotient",
"Power: a-power-of-a-power-multiplies-the-exponents | a-reciprocal-power-is-a-quotient",
"Power: a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero | two-powers-of-one-base-divide-by-subtracting-exponents",
Expand Down
20 changes: 15 additions & 5 deletions Sources/Tests/UnitTests/Core/Transformations/RuleSetTerminationTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,14 +46,24 @@ public sealed class RuleSetTerminationTest
/// needs to be actionable.
/// </summary>
/// <remarks>
/// <para>
/// <c>Power</c> splits a power of a product — <c>(2 * x) ^ 2</c> to <c>2 ^ 2 * x ^ 2</c> —
/// and something has to fold <c>2 ^ 2</c> before the result stops being a power of a
/// product. <c>NumericNeat</c> rewrites <c>--x</c> through a product of ones that only
/// collapses when the normalisation multiplies them out. Both are the same shape: a rule
/// whose right-hand side is a fixed point only after arithmetic that the set itself does
/// not do.
/// product: a rule whose right-hand side is a fixed point only after arithmetic that the
/// set itself does not do.
/// </para>
/// <para>
/// <c>NumericNeat</c> was here for the same reason and is not any more. It rewrote
/// <c>--x</c> through a product of ones that collapsed only when the normalisation
/// multiplied them out, because four rules took a factor of <c>-1</c> out of a product and
/// left its magnitude behind as a literal <c>1 *</c>. They decline <c>-1</c> now — it is
/// the sign rather than a factor to take out — so the ones are never made and the set
/// settles on its own. That is
/// <a href="https://github.com/asc-community/AngouriMath/issues/1167">#1167</a>, and this
/// list is one of the two places that recorded it.
/// </para>
/// </remarks>
private static readonly HashSet<string> SettleOnlyComposed = new() { "Power", "NumericNeat" };
private static readonly HashSet<string> SettleOnlyComposed = new() { "Power" };

private static readonly string[] Leaves = { "x", "y", "2", "-1", "1/2", "1", "0" };

Expand Down
Loading
Loading