Let the logarithm's domain follow the reading (#721, #890) - #916
Merged
Conversation
…y do Arcsinf, Arccosf, Arcsecantf and Arccosecantf each state one condition over the reals and another over the complex plane and pick between them by the reading. Logf stated the real one as though it were the only one, so the library gave log(-3, -3) the value 1 and declared it undefined at the same time -- the contradiction #890 reports. Over the complex plane log_b(a) is ln(a)/ln(b), which asks only that both logarithms exist and that the denominator is not zero. The zero cases are stated rather than read off evaluation, which returns the extended-real -oo for ln(0): -oo is not a complex number, and taking it for one drops the condition on ln(x) * 0, which is NaN at x = 0. The log_b(b) -> 1 rewrite asserted 'provided x > 0' rather than reading the node's condition, and was wrong in both directions at once: NaN at x = -3 where the logarithm is 1, and 1 at x = 1 where it is NaN. boundcheck now reports one disagreement where it reported two; the survivor needs an assumption travelling with the variable and is untouched. The derivative of x^n loses 'provided x > 0' for 'provided not x = 0', which is what ln(x) * 0 actually requires -- at n = 3, x = -2.5 it answered NaN and now answers 75/4. 6504 C# and 130 F# tests pass. Every changed answer is in BREAKING-CHANGES.md. Issue: #721 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Aug 13, 2026
Rafael-SOWNet
added a commit
that referenced
this pull request
Aug 13, 2026
… still names (#917) Three things #916 made stale: the DomainCondition table still gave the logarithm's real condition, section 7's 'ln and sqrt disagree about which reading their domain describes' was fixed by it, and section 8 said the rules-driven harness 'does not exist yet' when boundcheck is that harness and was built in the same PR that wrote this file. Section 11 is new, and is a measurement rather than a plan. ln(a) + ln(b) -> ln(a*b) is boundcheck's last disagreement and carries no condition, so by O2 it asserts there is nothing to assume, which is false. Guarding it with the file's own IsPositiveReal idiom fails three tests and then hangs -- three and a half hours against a normal five minutes, with four of the five candidate tests under --blame-hang being limit tests. So the dependency is termination, not coverage: the limit machinery expands logarithms and relies on the simplifier to gather them back. TRIAGE recorded the cost as 'the log-equation solver loses coverage', and that is not what it is. The precedent is eight rules up in the same file -- a^n / b^n was guarded for this reason and repaired by teaching the limit reader to recognise the shape itself, where IsEventuallyPositive can check positivity on the approach. That repair also needed a re-read bound, which the logarithm path has no equivalent of, and which is the likeliest reason its symptom is a hang. Section 10 gains the caution that follows: this rule was the standing example of what per-symbol assumptions would rescue, and no assumption on a and b discharges a termination dependency. Issue: #721 Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
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
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 the cheap half of #721, and #890's contradiction with it.
Arcsinf,Arccosf,ArcsecantfandArccosecantfeach state one condition over the reals and another over the complex plane, and pick between them by the reading.Logfstated the real one as though it were the only one. So the library gave an expression a value and declared it undefined at the same time — which is exactly what #890 reported:What changes
Over the complex plane
log_b(a)isln(a) / ln(b), which asks only that both logarithms exist and that the denominator is not zero: no complex number has0as its exponential, soaandbmust be nonzero, andln(b) = 0isb = 1.log(-3, -3).DomainConditionFalseTrueln(x).DomainConditionx > 0not x = 0"log(x, x)".Simplify()1 provided x > 01 provided not x = 0 and not x = 1"x ^ n".Differentiate("x").Simplify()x ^ n * n / x provided x > 0x ^ n * n / x provided not x = 0The real condition is still there and still reachable.
expr.WithCodomain(Domain.Real)givesx > 0 and not x = 1forlog(x, x)exactly as before. What changed is which of the two is the default, and the default is now the same complex reading the evaluator has always used.The rewrite was wrong in both directions at once
log_b(b) -> 1assertedprovided x > 0— the real condition, written out inside the rule rather than read from the node. It withdrew an answer that exists and kept one that does not:Only the first of those is a
boundcheckfinding; the second was not reported by anything and turned up on the way.The zero cases are stated, not read off evaluation
Evaluation returns the extended-real
-ooforln(0), so reading the condition off it would callln(x)defined everywhere.-oois not a complex number, and taking it for one loses a condition that is needed downstream:ln(x) * 0is0whereverln(x)has a value andNaNatx = 0, since-oo * 0is indeterminate. That is whyd/dx x^nkeepsnot x = 0rather than losing its condition altogether — and it dropsx > 0, which had been costing the answer at every negativex:Measured
boundcheck: 2 disagreements -> 1, both runs on the same harness build (master re-measured rather than read off the committed report, which was generated by an older one: 945 comparisons then, 966 now).ln(x) + ln(x+1) -> ln(x*(1+x)), which needs an assumption travelling with the variable — Unify Codomain with a "provided ... in RR" condition #721's expensive half — and is untouched here.DerivativeGapsTest.SymbolicExponentsAreUnaffected, whoseprovided x > 0was the stale real-domain claim. Its stated purpose — that a genuinely symbolic exponent still takes the logarithmic rule, condition and all — still holds.Every changed answer is in
BREAKING-CHANGES.mdunderUnreleased — since 2.1.0, with the value before and after, measured on a build of each.What this does not do
The other half of #721 — assumptions attached to variables,
Symbol('x', positive=True)-style and three-valued — is untouched. That is what would buy theln(a) + ln(b)guard and the two limits #902 withdrew, and it is #746's tier 1 rather than a rule fix.