Vector and Matrix Support #69
Comments
|
Vectors and matrices are something we've long wanted to have, but as you've
hinted, it's important to get the design right, and we've never yet quite
convinced ourselves that we have the right design.
For a little background: KeYmaera X's data structures do feature a
rudimentary type system that could be extended with other types, but by and
large our actual proof algorithms are designed with real numbers in mind.
In particular, there's a very clean story for how to automate proofs of
first-order formulas that only talk about reals, but automation for
arbitrary vectors or matrices would require a very different approach.
On the type-system side, vectors and matrices have dimensions, and treating
their dimensions correctly often demands at least a rudimentary form of
dependency or polymorphism in the type system.
That's not to say it can't or shouldn't be done, this is just to say why
we've thought about it for so long without having implemented a solution
yet.
If you're working with fixed-length vectors or matrices, you can sometimes
make your life a little better by making extensive use of function
definitions (here is an example proof where we used definitions a lot:
https://github.com/LS-Lab/KeYmaeraX-projects/tree/master/ijrr/robix.kyx).
You could define functions like norm, distance, dot product, cross product,
etc. KeYmaeraX also allows you to prove a lemma and use it in a proof of
another theorem.
If you identify some general lemmas for finite vectors or matrices, you
could try writing them as lemmas and using them in the proof.
(I might caution that the lemma feature has mainly been used by our lab, so
if you run into any weird issues or poor error messages while using it,
feel free to ask us)
If there are some natural or important lemmas for fixed-size matrices or
vectors, one option would be to assemble a library of functions and lemmas
which could be shipped with future releases. But for all the reasons
discussed above, that would also require a lot of discussion and thought.
By the way, KeYmaera X does have pairs. At least internally, it should be
possible to implement fixed-size vectors using nested pairs. However, I
have never tried to use them from a .kyx file or from the UI, and do not
know if that is currently supported.
…On Thu, Sep 24, 2020 at 2:05 PM zstone1 ***@***.***> wrote:
Is there any plan for syntactic support for vectors and matrices in
KeYmaera?
I've got a non-trivial matlab algorithm that I want to encode in a hybrid
program. It uses lots of vector operations (dot products, cross products,
read/write to the nth element). I happen to know all the lengths of the
vector statically, so I can flatten to a bunch of reals. However, that will
make all the proofs rather nasty. Is there a trick here, or do I have to do
this the hard way?
Depending on how hard it would be, I might be able to attempt adding such
support myself. But that would depend on having a suitable design already
agreed on.
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
<#69>, or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAO6WYNP5ZE5IJM2IOBA3YLSHOC7HANCNFSM4RYTMHHQ>
.
|
|
Yeah, there's no silver bullet as I suspected. I had thought about the dependent typing issues, and it's not nice. Is there even a decision procedure for vector arithmetic? Certainly for statically known lengths it's easy to convert to standard real QE, so at least in my case there is hope. I'm already making heavy use of function symbols. But to make that feature really nice, being able to import a library of functions (and function symbols + assertions) would be really important. For example, I'm adding Tuples are an interesting suggestion that would help a lot with readability. Unfortunately, all of the arithmetic like To simulate tuples, I was considering "encoding" a vector as a real by adding uninterpreted function symbols For a bit of context, I'm writing a Scala program to translate simulink/matlab models into hyrbid programs, so features without UI should be fine. But I'm a tad unsure how to setup an interactive theorem proving environment for KeYmaera without the UI. I've got lots of experience with Coq using vscoq, but I don't see an analogous feature here. All I really need is something to apply a tactic and pretty print the new context. Is there a doc for this? |
|
When we're not working with the UI, we usually write a Scala test case and
write proofs using the Scala embedding of our tactic language bellerophon.
The wiki has an article on setting up the development environment and
running tests.
We do also have a rudimentary REPL, but it's not actively maintained, and I
am unsure of its status
…On Fri, Sep 25, 2020, 12:41 PM zstone1 ***@***.***> wrote:
Yeah, there's no silver bullet as I suspected. I had thought about the
dependent typing issues, and it's not nice. Is there even a decision
procedure for vector arithmetic? Certainly for statically known lengths
it's easy to convert to standard real QE, so at least in my case there is
hope.
I'm already making heavy use of function symbols. But to make that feature
really nice, being able to import a library of functions (and function
symbols + assertions) would be really important. For example, I'm adding sin
cos and pi symbols, and then assuming some properties about them. I'd
love to do this once, and then import a file. Does anything like this exist?
Tuples are an interesting suggestion that would help a lot with
readability. Unfortunately, all of the arithmetic like plus have
RBinaryCompositeTerm, which requires its arguments to be Real sort. So
I'd also have to add plus1, plus2, plus3, losing the readability benefit.
A naive idea is to define a notion for sorts of "recursively real", and
assert that both sorts are equal, and recursively real. The Assign class is
already does this kind of equality check in its insist block. Extending
ODE and Assign with this behavior would be provide a fairly complete tuples
feature in the syntax. I have no idea how that would affect the tactics...
To simulate tuples, I was considering "encoding" a vector as a real by
adding uninterpreted function symbols length : (encoded R) -> nat, read :
(encoded R) -> nat -> R, write : (encoded R) -> nat -> R -> (encoded R)
(where nat and (encoded R) are of course just R) then assuming the lens
laws. I'd have to add uninterpreted plus, dot, cross, ect forall of these
as well. Good news about this approach is assignment magically works out.
Bad news is ODEs do not work at all.
For a bit of context, I'm writing a Scala program to translate
simulink/matlab models into hyrbid programs, so features without UI should
be fine. But I'm a tad unsure how to setup an interactive theorem proving
environment for KeYmaera without the UI. I've got lots of experience with
Coq using vscoq, but I don't see an analogous feature here. All I really
need is something to apply a tactic and pretty print the new context. Is
there a doc for this?
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#69 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAO6WYKSEXT5BWWWCGWQMH3SHTB2HANCNFSM4RYTMHHQ>
.
|
|
I was recently reminded that there is another project which tries to
generate KeYmaera X models from Simulink models.
I have not used this project myself, and it's possible that their goals or
approach differ from yours, but I thought their paper may be helpful in
your efforts:
https://link.springer.com/chapter/10.1007/978-3-030-02450-5_6
On Fri, Sep 25, 2020 at 12:45 PM Brandon Bohrer <[email protected]>
wrote:
… When we're not working with the UI, we usually write a Scala test case and
write proofs using the Scala embedding of our tactic language bellerophon.
The wiki has an article on setting up the development environment and
running tests.
We do also have a rudimentary REPL, but it's not actively maintained, and
I am unsure of its status
On Fri, Sep 25, 2020, 12:41 PM zstone1 ***@***.***> wrote:
> Yeah, there's no silver bullet as I suspected. I had thought about the
> dependent typing issues, and it's not nice. Is there even a decision
> procedure for vector arithmetic? Certainly for statically known lengths
> it's easy to convert to standard real QE, so at least in my case there is
> hope.
>
> I'm already making heavy use of function symbols. But to make that
> feature really nice, being able to import a library of functions (and
> function symbols + assertions) would be really important. For example, I'm
> adding sin cos and pi symbols, and then assuming some properties about
> them. I'd love to do this once, and then import a file. Does anything like
> this exist?
>
> Tuples are an interesting suggestion that would help a lot with
> readability. Unfortunately, all of the arithmetic like plus have
> RBinaryCompositeTerm, which requires its arguments to be Real sort. So
> I'd also have to add plus1, plus2, plus3, losing the readability
> benefit. A naive idea is to define a notion for sorts of "recursively
> real", and assert that both sorts are equal, and recursively real. The
> Assign class is already does this kind of equality check in its insist
> block. Extending ODE and Assign with this behavior would be provide a
> fairly complete tuples feature in the syntax. I have no idea how that would
> affect the tactics...
>
> To simulate tuples, I was considering "encoding" a vector as a real by
> adding uninterpreted function symbols length : (encoded R) -> nat, read
> : (encoded R) -> nat -> R, write : (encoded R) -> nat -> R -> (encoded R)
> (where nat and (encoded R) are of course just R) then assuming the lens
> laws. I'd have to add uninterpreted plus, dot, cross, ect forall of
> these as well. Good news about this approach is assignment magically works
> out. Bad news is ODEs do not work at all.
>
> For a bit of context, I'm writing a Scala program to translate
> simulink/matlab models into hyrbid programs, so features without UI should
> be fine. But I'm a tad unsure how to setup an interactive theorem proving
> environment for KeYmaera without the UI. I've got lots of experience with
> Coq using vscoq, but I don't see an analogous feature here. All I really
> need is something to apply a tactic and pretty print the new context. Is
> there a doc for this?
>
> —
> You are receiving this because you commented.
> Reply to this email directly, view it on GitHub
> <#69 (comment)>,
> or unsubscribe
> <https://github.com/notifications/unsubscribe-auth/AAO6WYKSEXT5BWWWCGWQMH3SHTB2HANCNFSM4RYTMHHQ>
> .
>
|
|
Let me add that these translations can be quite impactful between rigorous verification tools such as KeYmaera X and modeling tools used in engineering practice such as SF/SL. I wish you all the best in your research and encourage you to get in touch with us via email and keep us up to date. BTW, in theory the relationship of single reals to vectors is perfectly definable by bijection in differential dynamic logic [JAR'08,TOCL'17]. In practice, however, vectors should be done much more pragmatically. |
Is there any plan for syntactic support for vectors and matrices in KeYmaera?
I've got a non-trivial matlab algorithm that I want to encode in a hybrid program. It uses lots of vector operations (dot products, cross products, read/write to the nth element). I happen to know all the lengths of the vector statically, so I can flatten to a bunch of reals. However, that will make all the proofs rather nasty. Is there a trick here, or do I have to do this the hard way?
Depending on how hard it would be, I might be able to attempt adding such support myself. But that would depend on having a suitable design already agreed on.
The text was updated successfully, but these errors were encountered: