Adds a tool interface for Mathematica's AsymptoticDSolveValue command. #84
Conversation
This file contains 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
The executor may be null if a tool or subtool isn't initialized before use. This can happen, e.g., when adding a new subtool to the main Mathematica tool and forgetting about the various pieces of boilerplate (calling .init, .shutdown, etc. in the relevant methods of the Mathematica tool). I've run into this issue a few times now, and I always lose a significant amount of time before remember that tools have state and associated protocols. Hopefully this error message will make tool extension/development easier.
Mathematica uses C[i] as its default form for parameters/constants.
For example, when computing series approxiamtions to solutions of ODEs, C[i]
is used to represent the constant of integration.
Perhaps a better way of handling this is to ensure that we never get C[i] back from
Mathematica. This can be achieved by always specifying initial conditions in calls to solvers.
For example, instead of:
```
AsymptoticDSolveValue[
{
x'[t] == y[t],
y'[t] == x[t],
y[0] == x0,
x[0] == y0
},
{x[t], y[t]},
{t, 0, 10}
]
```
instead do:
```
AsymptoticDSolveValue[
{
x'[t] == y[t],
y'[t] == x[t],
y[0] == x0,
x[0] == y0
},
{x[t], y[t]},
{t, 0, 10}
]
```
and then handle x0 and y0 before passing formulas back out of the tool.
Note: this is not currently used in any soundness-critical way that I'm aware of,
but both Reduce and DSolve are capable of generating C[i] symbols. Therefore,
we should do a thorough check that C[i]s are never handed back to us when not expected
or else revert this commit.
See https://reference.wolfram.com/language/ref/C.html for more information on what C[i]
is used for in Mathematica.
Note: this code would already written in the DSolve tool, and now exists in two different places. We should unify this code and clean up the interface to the DifferenitalProgram converter.
Computes asymptotic approximations to the solutions of ODEs. See https://reference.wolfram.com/language/ref/AsymptoticDSolveValue.html
…amed) taylorize cli mode.
The executor may be null if a tool or subtool isn't initialized before use. This can happen, e.g., when adding a new subtool to the main Mathematica tool and forgetting about the various pieces of boilerplate (calling .init, .shutdown, etc. in the relevant methods of the Mathematica tool). I've run into this issue a few times now, and I always lose a significant amount of time before remember that tools have state and associated protocols. Hopefully this error message will make tool extension/development easier.
Mathematica uses C[i] as its default form for parameters/constants.
For example, when computing series approxiamtions to solutions of ODEs, C[i]
is used to represent the constant of integration.
Perhaps a better way of handling this is to ensure that we never get C[i] back from
Mathematica. This can be achieved by always specifying initial conditions in calls to solvers.
For example, instead of:
```
AsymptoticDSolveValue[
{
x'[t] == y[t],
y'[t] == x[t],
y[0] == x0,
x[0] == y0
},
{x[t], y[t]},
{t, 0, 10}
]
```
instead do:
```
AsymptoticDSolveValue[
{
x'[t] == y[t],
y'[t] == x[t],
y[0] == x0,
x[0] == y0
},
{x[t], y[t]},
{t, 0, 10}
]
```
and then handle x0 and y0 before passing formulas back out of the tool.
Note: this is not currently used in any soundness-critical way that I'm aware of,
but both Reduce and DSolve are capable of generating C[i] symbols. Therefore,
we should do a thorough check that C[i]s are never handed back to us when not expected
or else revert this commit.
See https://reference.wolfram.com/language/ref/C.html for more information on what C[i]
is used for in Mathematica.
Note: this code would already written in the DSolve tool, and now exists in two different places. We should unify this code and clean up the interface to the DifferenitalProgram converter.
Computes asymptotic approximations to the solutions of ODEs. See https://reference.wolfram.com/language/ref/AsymptoticDSolveValue.html
…amed) taylorize cli mode.
|
To reiterate, I'm not so sure this merge request should be accepted as-in. Primarily, I want to get opinions on whether the addition of |
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.
This pull request contains an interface for Mathematica's AsymptoticDSolveValue and also exposes a CLI interface to this tool. The roadmap here is to rewrite the series approximation tactics so that they are more general, and also incorporate this tactic into
master(for proving systems where there are either numeric or approximation-looking pre/post-conditions). I'm including just theToolin a first pull request because the implementation details require significant consideration.The AsymptoticDSolveValue tool itself is not soundness-critical. However, this pull request does contain some changes that perhaps require review/consideration prior to merging:
Reducecan return results that containC[]'s, so this is possibly soundness critical. However, I'm fairly certain that the particular inputs we give to Reduce will never result in return values that containC[](after all, we haven't known how to translate those until now). So, I'm (a) pretty sureC[]s will not show up in the QE tool code and (b) even if they do not sure if that would break soundness. So, whether it makes sense to convert C[]'s -- or especially whether it makes sense to add some logic that prevents QE tools from knowing about C[]'s -- is perhaps a reasonable thing to discuss before merging this pull request.