Conversation
Limit algebra: - finite + finite is positive or negative only when both signs agree; mixed signs give unknown - log(c) for finite positive c is unknown (negative below 1) - 1/0, 0^(-c) and log(0) need the zero to be approached from above; callers pass that knowledge, otherwise the result is unknown - c^0 with c -> 0 or c -> inf is indeterminate Scalar limit visitor: - a symbol other than the limit variable takes its sign from its assumptions, otherwise unknown - sin, tan, asin, atan of an argument tending to 0 tend to 0; cos and acos tend to a positive value; other finite arguments of sin, cos, tan and a positive argument of acos give unknown - asin of an infinite argument is unknown; atan and asin keep the argument's sign - sign(x) at 0 follows the side of approach Tensor-to-scalar limit visitor: - invariants independent of the limit variable take their sign from their assumptions, otherwise unknown - a scalar wrapper takes the sign of its scalar value - pow and log of the exact limit variable use the side of approach Signed-off-by: petlenz <peterlenz89.pl@gmail.com>
ScalarLimit.OtherVariableFinite: y has no assumptions, so as x -> 0+ it is a constant of either sign; finite_positive is not provable (y = -1 is a counterexample). Expected result is now unknown. T2sLimit.TensorDepIndependentExpr: det(G) is independent of F but a general 3x3 determinant takes either sign (det(-I) = -1). Expected result is now unknown. Signed-off-by: petlenz <peterlenz89.pl@gmail.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
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 #357.
The limit visitors now report a direction only when it is provable; otherwise
unknown.Behavior changes (before → after)
log(c), c finite > 01/f,f^(-c),log(f)with f → 0 and side unknownc^gwith g → 0 and c → 0 or ∞sin,tan,asin,atanof f → 0sin,cos,tanof finite nonzeroasinof ±∞atan,asinof finite⁻acosof finite⁺ (acos(1) = 0)sign(x)at 0⁺ / 0⁻trace,det,dot,norm, eigenvalue, …) independent of the variabledetof a PD tensor), else unknownSigned zero: no new direction values.
limit_algebra::apply_log/apply_pow/apply_reciprocaltake azero_from_aboveflag; the visitors set it when the argument is the limit variable approaching 0⁺ or is inferred positive.Needs a decision: two existing tests changed (separate commit
b6f32cd). Both asserted a positive sign that is not provable:ScalarLimit.OtherVariableFinite: an unassumed symbolyas x → 0⁺ can be negative (y = −1), sofinite_positive→unknown.T2sLimit.TensorDepIndependentExpr:det(G)takes either sign (det(−I) = −1), sofinite_positive→unknown.Trade-off. There is no sign-neutral "finite" direction, so an unknown-sign constant now makes
∞ + yunknown where +∞ would be true. Adding such a direction would restore that precision; left for a follow-up.Tests (
LimitVisitorTest.h):LimitAlgebra.{AddSigns, MulSigns, ZeroNeedsApproachSide, LogAndPowOfFiniteValues},ScalarLimit.{OddFunctionsAtZero, ReciprocalOfSinAtZeroIsNotFinite, ZeroFromBelowHasNoLogOrReciprocal, SignAtZeroFollowsApproachSide, AssumedSignOfOtherSymbols, InverseTrigSigns},T2sLimit.{ConstantSignsComeFromValuesAndAssumptions, ExactMatchReciprocalNeedsApproachSide}. Negative control againstmain's limit sources: 9 of the new tests fail;MulSignspasses (locks in already-correct behavior); the two algebra probes using the new signature can't compile there and are covered end to end. Full suite 2358/2358 (gcc-14 Debug,-Werrorminus pre-existing pedantic/deprecated).