Repository navigation
A limit binds the variable it approaches along (#989) - #1091
Merged
Merged
Conversation
`FreeVariables` learned about a summation, a product and a definite integral in #1045, and about `limit` not at all. That commit enumerates the indefinite integral and the derivative as deliberate exclusions and does not mention a limit, so this was an omission rather than a decision. And the reason those two are excluded is what makes this one bind. An antiderivative of `t * b` over `t` is `b * t ^ 2 / 2 + C` and `d/dt` denotes a function of `t` -- both are still functions of the variable. **A limit never is.** `lim(t, t, 0)` is 0, and no limit's value depends on the name it approaches along, so the variable is consumed exactly as a summation index is. The destination is where the dependence goes and is bound over as well, so `lim(t, t, b)` is a function of `b` alone. `Limitf` is a `CalculusOperator(Expression, Var)`, the same shape as `Integralf`, so this is one arm next to it -- unconditional where the integral's is conditional, which is the distinction the comment now records. Measured on a build of each side: `limit(t * b, t, 0).FreeVariables` was `{ t, b }` and is `{ b }`. `Vars` and `VarsAndConsts` untouched.
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 the last part of #989.
FreeVariableslearned about a summation, a product and a definite integral in #1045, and aboutlimitnot at all. That PR's message enumerates the indefinite integral and the derivative asdeliberate exclusions and does not mention a limit — so this was an omission, not a decision.
"limit(t * b, t, 0)".FreeVariables{ t, b }{ b }"limit(t, t, b)".FreeVariables{ t, b }{ b }"limitleft(t * b, t, 0)".FreeVariables{ t, b }{ b }"limit(t, t, 0)".FreeVariables{ t }{ }Measured on a build of each side.
Why a limit binds where those two do not
The reason #1045 gives for excluding them is exactly what separates them from this. An
antiderivative of
t * bovertisb * t ^ 2 / 2 + C, andd/dtdenotes a function oft—both are still functions of the variable.
A limit never is.
lim(t, t, 0)is0. No limit's value depends on the name it approachesalong, so the variable is consumed exactly as a summation index is — and unlike the integral,
which binds only when it has limits to bind between, this is unconditional. The comment
records that distinction rather than leaving the reader to infer it.
The destination is where a limit's dependence goes, so it is bound over too:
lim(t, t, b)is afunction of
balone. A one-sided limit binds the same way — the side is not a variable.Limitfis aCalculusOperator(Expression, Var), the same shape asIntegralf, so this is onearm next to it.
VarsandVarsAndConstsare untouched, as in #1045 — they mean every name occurring.Full suite: 8740 passed, 0 failed.
🤖 Generated with Claude Code
https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd