Skip to content

Fold abs where the sign of its argument is known (#881) - #901

Merged
Rafael-SOWNet merged 2 commits into
masterfrom
fix/abs-of-known-sign
Aug 12, 2026
Merged

Fold abs where the sign of its argument is known (#881)#901
Rafael-SOWNet merged 2 commits into
masterfrom
fix/abs-of-known-sign

Conversation

@Rafael-SOWNet

@Rafael-SOWNet Rafael-SOWNet commented Aug 12, 2026

Copy link
Copy Markdown
Collaborator

Closes #881.

|x| is x for a non-negative real x and -x for a negative one. That is the definition of
the function, not an identity carrying a side condition — but it was applied only where the argument
was a Number node. An argument whose value is a known real, without its node being a number,
was left alone:

was is
abs(-sqrt(6)) left as written sqrt(6)
abs(-pi), abs(-e) left as written pi, e
abs(1 - sqrt(2)) left as written sqrt(2) - 1
abs(-2) 2 2, unchanged
abs(sqrt(-4)) 2 2, unchanged — the magnitude of 2i
abs(-a) for symbolic a left as written left as written

Where it is visible is in an answer built out of radicals. (2x^2 - 3 > 0) and (x > 0) solved to
(abs(-sqrt(6)) / 2; +oo) and now solves to (sqrt(6) / 2; +oo). The endpoint was always the same
number, printed in a form that reads as unfinished work.

What is not assumed

The sign is read off Evaled, which means the rule declines rather than guesses in the two cases
where guessing would be wrong:

  • A symbol has no sign. abs(-a) stays as written. Nothing here assumes a is real, let alone
    which side of zero it is on.
  • Off the real line there is no answer of this shape. sqrt(-4) evaluates to 2i, whose
    absolute value is 2 — neither the argument nor its negation. A rule reading "the value is
    negative, so negate it" would be wrong there, so a value that is not a finite real does not fire
    it.

The half that is not here, and why

#881 also asks for |-x| = |x| for a symbolic x. That is unconditionally sound — negation is
an isometry — and it is the example SimplificationContract.md uses for an empty assumption set. It
is not in this PR, and the reason is measured rather than guessed:

simplify(sgn(-a))               => sgn(-a)          // no odd-symmetry normalisation
simplify(sgn(-a) * abs(-a))     => -a               // this works today
simplify(abs(-a) + abs(a))      => abs(-a) + abs(a) // this is what the rewrite would buy

Rewriting abs(-a) to abs(a) on its own breaks the middle line: the pairing rule wants
sgn(t) * abs(t) for the same t, and sgn(-a) does not normalise to -sgn(a). So the even
symmetry of abs wants the odd symmetry of sgn alongside it, as one change with the collection of
abs(-a) + abs(a) to show for it. Trading a working answer for a new one is not a fix, so it is left
to be done properly.

Measured

Suite 6320 passed / 0 failed, including 10 new cases in SimplificationRegressionTest. casbench
117/119 with 0 wrong, rootcheck 596/596, simpsweep 10463/10463, propcheck 0 failures, crashcheck
1652 cases with 0 crashes.

boundcheck needed four builds to read honestly, so here they all are:

build shapes rewritten disagreements
master d8bfcd51 46 6
master + this branch 46 6
master + #899 44 4
master + #899 + this branch 44 4

This change adds no disagreement in either context. The middle two rows are the interesting
part, and they correct something the commit message on this branch gets wrong: it says the report
checked in alongside the harness was stale, and it was not. It says four because it was generated
on a build that already carried #899, which removes exactly the two entries master still has —
abs(sgn(x)) and sgn(abs(x)), each simplifying to 1 where both are 0 at x = 0. Those are
#892, already fixed in #899, and not
something this branch discovered or needs to file.

These two PRs conflict, and they do compose

#899 replaces the two arms immediately above the one added here, so git reports a conflict in
Evaluation.Continuous.Arithmetics.Classes.cs, in SimplificationRegressionTest.cs, and in
BREAKING-CHANGES.md — all three are adjacent additions rather than disagreements. Merged together
on a throwaway branch and measured: 6342 tests passed / 0 failed, and the four boundcheck
disagreements above. abs(-sqrt(6)) still folds to sqrt(6), abs(sgn(x)) is still left alone, and
abs(sgn(0)) is still 0.

Resolution order matters and is worth stating for whoever merges second: #899's
Signumf(var signOf) when ValueWithCondition(...) arm goes before the var argument when argument.Evaled is Real ... arm from this branch. The latter is a catch-all with a guard, so put it
last. A C# switch takes the first arm that matches, so with it first the abs(sgn(2)) case would
reach the catch-all and hand back its argument sgn(2) — the same number, one reduction step short
of what #899's arm gives it. The merge I measured has them in the order above.

One follow-up on release

The Solvers wiki page prints the old
(abs(-sqrt(6)) / 2; +oo), and docsamples reports it as its single output mismatch. The page
should be updated when this ships, not before — until then it correctly describes 2.0.0.

|x| is x for a non-negative real x and -x for a negative one, which is the definition of
the function rather than an identity carrying a side condition. It was applied only where
the argument was a Number node, so an argument whose *value* is a known real kept its abs:
abs(-sqrt(6)) and abs(-pi) came back exactly as written.

That is visible in answers built out of radicals. (2x^2 - 3 > 0) and (x > 0) solved to
(abs(-sqrt(6)) / 2; +oo) and now solves to (sqrt(6) / 2; +oo) -- the endpoint was always
the same number, printed in a form that read as unfinished work. The Solvers wiki page
shows the old output and wants updating with the release; docsamples reports it as its one
output mismatch until then.

The sign is read off Evaled, so nothing is assumed about a symbol -- abs(-a) is left alone
-- and an argument off the real line declines rather than being guessed at. sqrt(-4)
evaluates to 2i, whose absolute value is 2, which is neither the argument nor its
negation; a rule reading "negative, therefore negate" would be wrong there. Non-finite
values decline too.

#881 also asks for |-x| = |x| for a symbolic x, which is unconditionally sound and is not
here. Measured why: sgn(-a) does not normalise to -sgn(a), so rewriting abs(-a) to abs(a)
on its own breaks the pairing that gives sgn(-a) * abs(-a) -> -a. It wants the odd
symmetry of sgn alongside it.

Suite 6320 passed; casbench 117/119 with 0 wrong; rootcheck 596/596; simpsweep
10463/10463; propcheck 0 failures; crashcheck 1652 cases with 0 crashes.

boundcheck reports 46 shapes rewritten and 6 disagreements both with this change and on
the commit before it, measured separately, so it adds none. The report committed in the
workspace said four, and was stale rather than better: two of the six are abs(sgn(x)) and
sgn(abs(x)), each simplifying to 1 where both are 0 at x = 0. Those are wrong answers in
master, not here, and get their own issue.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
#892's fix landed in master while this branch was open, and it replaces the two arms
immediately above the one added here. Three conflicts, all adjacent additions rather than
disagreements: the Absf switch, the regression tests, and BREAKING-CHANGES.md.

In the switch, master's Signumf(var signOf) when ValueWithCondition(...) arm goes first and
this branch's `var argument when argument.Evaled is Real ...` last. A C# switch takes the
first arm that matches, and the second is a catch-all with a guard, so reversing them would
send abs(sgn(2)) to the catch-all and hand back sgn(2) rather than 1. Measured in that
order: abs(sgn(2)) is 1, abs(sgn(0)) is 0, abs(sgn(x)) is left alone, and abs(-sqrt(6)) is
sqrt(6).

BREAKING-CHANGES.md keeps master's section where master put it and adds this one after it.

Suite 6342 passed, F# wrapper 130 passed, both 0 failed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@Rafael-SOWNet
Rafael-SOWNet merged commit 6093741 into master Aug 12, 2026
25 checks passed
Rafael-SOWNet added a commit that referenced this pull request Aug 12, 2026
One conflict, in BREAKING-CHANGES.md, where #901 and #903 landed their glance rows and their
sections around the place this branch adds its own. All three are additions rather than
disagreements: master's rows and sections keep their positions and this branch's follow.

Verified after resolving rather than assumed: abs(-sqrt(6)) is sqrt(6), ln(e^x) is left as
written, and a solve answer carrying a conditional set still prints its own binder. Suite 6359
passed, F# wrapper 130 passed, both 0 failed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Rafael-SOWNet added a commit that referenced this pull request Aug 12, 2026
Stringize prints the NaN value as NaN, the grammar had no such token, so reading it back gave a
variable of that name -- which then behaved like any symbol. NaN - NaN simplified to 0,
NaN / NaN to `1 provided not NaN = 0`, and NaN * 0 to 0, each of them the ordinary rewrite for a
free variable. Nothing on the page distinguished the two, because a variable named NaN prints as
NaN as well.

Its two siblings already had tokens -- +oo and -oo both print and parse -- and Latexize has
emitted \mathrm{undefined} all along, which is the token CSharpMath decodes back to MathS.NaN, so
the LaTeX round trip was already closed and is untouched. Verified in CSharpMath's own source
rather than assumed: Evaluation.cs has
`case ("undefined", 0, FontStyle.Roman): @this = MathS.NaN; break;`.

Declared as a lexer rule above VARIABLE rather than as an inline literal, which is where BOOLEAN
sits and for the same reason: equal-length matches go to the earlier rule, and this word would
otherwise be an identifier. One spelling only. BOOLEAN carries two capitalisations of each word
because it has to read back its own output -- Entity.Boolean prints True where a caller types
true -- and NaN prints and reads the same way, so there is nothing to reconcile.

Reserving the word costs the identifier, as `mod` did in 2.0, and only the exact spelling: NaNx,
NaN_1 and aNaN are still variables, since the lexer takes the longest match.

The round trip is now tested in both directions. Every case in StringizeRoundTripTest began from a
string, so it could only reach expressions the parser already produces, and a value with no source
form was invisible to all of them however many cases were added -- which is why this defect lived
in an output. It now also enumerates the named constants of MathS and Entity.Number.Real by
reflection, prints each and reads it back, so a constant added later is covered without anyone
remembering the file exists. MathS.NaN and Real.NaN are the two that fail against the old grammar.

Regenerated with the committed antlr-4.13.1 jar and the post-processor. The unmodified grammar was
regenerated first and its diff confirmed empty, so nothing in the generated files here is a
toolchain difference. Syntax.md lists the new literal.

New tests fail 9 of 219 against master and pass 219 of 219 here. Suite 6451 passed, F# wrapper 130
passed; casbench 117/119 with 0 wrong; rootcheck 596/596; simpsweep 10463/10463; propcheck 1340
checks 0 failures; crashcheck 1652 cases 0 crashes; boundcheck 2 disagreements and 0 that did not
parse; docsamples 0 compile errors, its one output mismatch being the Solvers wiki page that #901
made stale.

Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

abs does not fold a negated radical or constant: abs(-sqrt(6)) survives Simplify

1 participant