Fold the negation a half-turn table lookup builds, so InnerSimplified is idempotent (#930) - #932
Open
Rafael-SOWNet wants to merge 2 commits into
Open
Fold the negation a half-turn table lookup builds, so InnerSimplified is idempotent (#930)#932Rafael-SOWNet wants to merge 2 commits into
Rafael-SOWNet wants to merge 2 commits into
Conversation
… is idempotent (#930) "cos(0 ^ y)".InnerSimplified -(-1) provided y / 2 * (1 + 1 / sgn(y) ^ 2) > 0 "cos(0 ^ y)".InnerSimplified.InnerSimplified 1 provided y / 2 * (1 + 1 / sgn(y) ^ 2) > 0 Both are the same value, so nothing was wrong. What was wrong is that applying the normalisation twice gave a different tree from applying it once, and a great deal of the library treats what InnerSimplified hands back as settled -- rules match on it, caches key on it, tests compare against it. Whichever of the two trees a caller saw then depended on how many times something happened to normalise it. An exact trigonometric value is read off the table either directly or after a half turn, and the half-turn arm returns `-turned` for the odd case. That negation is built above a value already in its final form, so nothing downstream is obliged to look at it again -- and where the answer is *wrapped* rather than rebuilt, nothing does. `cos(0 ^ y)` is exactly that shape: `0 ^ y` is `0 provided ...`, and the cosine of it comes back wrapped in the same condition with the negation still standing. A bare `cos(0)` was fine because its result gets rebuilt on the way out. So the fold happens where the negation is made rather than being left to whoever receives it, which covers every table pull that goes through a half turn rather than this one expression. The exact values themselves are unchanged, which has tests: cos(pi) is -1, sin(pi/6) is 1/2, cos(pi/3) is 1/2, tan(pi/4) is 1. Found by `canoncheck`, the canonical-form harness added for #746 tier 1. Idempotence needs no oracle -- it compares a form against itself -- so it can be checked over generated input for nothing, and this was the only failure in 834 expressions. That count is now zero. The regression test compares **entities** rather than printed forms, and says why: the general class of idempotence failure includes two trees that print alike and differ, which `(x + y) + a` and `x + (y + a)` already do. Measured: suite 6960 passed / 0 failed; casbench 116/119 with 0 wrong, 0 error, 0 timeout; propcheck 1340 checks / 0 failures; rootcheck 596/596 clean; simpsweep 10463/10463 agree; canoncheck idempotence 1 failure -> 0 of 834. #930 Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
…-idempotence # Conflicts: # BREAKING-CHANGES.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #930.
Both are the same value, so nothing was wrong. What was wrong is that applying the normalisation twice gave a different tree from applying it once, and a great deal of the library treats what
InnerSimplifiedhands back as settled — rules match on it, caches key on it, tests compare against it. Which of the two trees a caller saw then depended on how many times something happened to normalise it.Cause
An exact trigonometric value is read off the table either directly or after a half turn, and the half-turn arm returns
-turnedfor the odd case. That negation is built above a value that is already in its final form, so nothing downstream is obliged to look at it again — and where the answer is wrapped rather than rebuilt, nothing does.cos(0 ^ y)is exactly that shape:0 ^ yis0 provided ..., so the cosine comes back wrapped in the same condition with the negation still standing. A barecos(0)was fine only because its result gets rebuilt on the way out.So the fold now happens where the negation is made rather than being left to whoever receives it, which covers every table pull that goes through a half turn rather than this one expression.
The exact values themselves are unchanged, and that has tests:
cos(pi)is-1,sin(pi/6)is1/2,cos(pi/3)is1/2,tan(pi/4)is1.How it was found
canoncheck, the canonical-form harness added for #746 tier 1 (see #928). Idempotence needs no oracle — it compares a form against itself — so it can be checked over generated input for nothing. This was the only failure in 834 expressions, and that count is now zero.The regression test compares entities rather than printed forms, and says why: the general class of idempotence failure includes two trees that print alike and differ, which
(x + y) + aandx + (y + a)already do.Measured
Suite 6960 passed / 0 failed; casbench 116/119 with 0 wrong, 0 error, 0 timeout; propcheck 1340 checks / 0 failures; rootcheck 596/596 clean; simpsweep 10463/10463 agree; canoncheck idempotence 1 → 0 of 834.
BREAKING-CHANGES.mdcarries the entry —InnerSimplifiedis public, so the tree it returns changing is recorded even though the value did not.🤖 Generated with Claude Code