Repository navigation
Put a leftover reciprocal under the line, not on top of it - #712
Merged
Merged
Conversation
The rewrite that turns a vanishing factor against a diverging one into a quotient multiplied every remaining factor into the numerator. The children of a product arrive flattened through any division in it -- tan(x) * ln(x) comes apart into sin(x), cos(x)^(-1) and ln(x) -- so a leftover could itself be a reciprocal, and putting that on top rebuilt the very product the rewrite exists to take apart. The quotient simplified straight back to its own input and the rule worked at it until something else stopped it. Split into a numerator and a denominator instead. lim x->0+ (x * ln(x) / cos(x)) went from not terminating inside thirty seconds to 0. Suite 4675 passed, 0 failed; corpus unchanged at 111/117 with 0 wrong, 0 error and 0 timeout.
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.
A bug in my own #710, found chasing the one case that PR left unanswered.
The rewrite that turns vanishing × diverging into a quotient multiplied every remaining factor into the numerator. But the children of a product arrive flattened through any division in it —
tan(x) * ln(x)comes apart intosin(x),cos(x)^(-1)andln(x)— so a leftover can itself be a reciprocal. Putting that on top rebuilt the very product the rewrite exists to take apart: the quotient simplified straight back to its own input, and the rule worked at it until something else stopped it.Split into a numerator and a denominator instead.
lim x->0+ (x * ln(x) / cos(x))The plain forms with no leftover —
x * ln(x),sin(x) * ln(x),x * cotan(x)and the rest — go through the same path and are unchanged, which the tests pin.Suite
Failed: 0, Passed: 4675, Skipped: 14, Total: 4689; corpus 111/117, 0 wrong / 0 error / 0 timeout.Still not fixed:
lim x->0+ (tan(x) * ln(x))is the case I was chasing, and it is still NaN. The rewrite now produces the right shape for it —ln(x) / (cos(x) / sin(x)), which answers 0 when handed to the limit machinery directly — so whatever turns it away is further down, in a guard l'Hopital's rule applies to the rewritten quotient. Recorded rather than left implied; I have not found it yet.