Email Gateway (Aug 19 2022 at 09:26): Email Gateway (Aug 19 2022 at 09:26):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jesus,
there is no support for nested abstract datatypes. To achieve abstract
matrices, you would need to provide an explicit type for matrices (e.g.
using datatype ('a, 'm, 'n) matrix = Matrix "'a ^ 'm ^ 'n" (*)) and then
lift all operations you want to that explicit matrix type. When doing
this, the recently emerged lifting and transfer infrastructure could be
helpful – unfortunately, I have no canonical reference for this at hand
and have not used it myself, but others on this mailing list will know
better.
I hope these meagure hints show the way. Feel free to ask again if you
are still lost.
Cheers,
Florian
(*) I am not familiar with the vectors/matrix stuff, so this might be wrong.
signature.asc
Email Gateway (Aug 19 2022 at 09:26):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Jesus,
there is also the possibility to use the matrices from the AFP which are fully
executable, but where all lemmas are guarded by their dimension, as in
"mat n m m1 ==> mat n m m2 ==> mat_plus m1 m2 = mat_plus m2 m1"
Cheers,
René
Email Gateway (Aug 19 2022 at 09:41):From: andreas.lochbihler@kit.edu
Hi Jesus and Florian,
The code generator does support nested abstract datatypes in this case,
although only indirectly. As the abstraction function vec_lambda must
not appear in any code equation, you have to promote any such subterm
to a proper constant and prove the corresponding code equation. The
following works:
definition mat_mult_row where
"mat_mult_row m m' f = vec_lambda (%c. setsum (%k. ((m$f)$k) *
((m'$k)$c)) (UNIV :: 'n::finite set))"
lemma mat_mult_row_code [code abstract]:
"vec_nth (mat_mult_row m m' f) = (%c. setsum (%k. ((m$f)$k) *
((m'$k)$c)) (UNIV :: 'n::finite set))"
by(simp add: mat_mult_row_def fun_eq_iff)
lemma mat_mult [code abstract]: "vec_nth (m ** m') = mat_mult_row m m'"
unfolding matrix_matrix_mult_def mat_mult_row_def[abs_def]
using vec_lambda_beta by auto
export_code "op **" in SML file -
So there is no need to wrap all types and do the lifting.
Hope this helps,
Andreas
Zitat von Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>:
Email Gateway (Aug 19 2022 at 09:52):From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Hi Andreas,
thanks for your help, your proposed solution was really helpful, it
worked perfectly. Let's
see if we can successfully apply it to some other operations on matrices!
Thanks again,
Jesus
Email Gateway (Aug 19 2022 at 09:53):From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Dear all,
Happy New Year for everyone.
Thanks for your hints, Florian and René. We had been exploring the
approach that Florian suggests, by means of a dedicated "('a, 'm, 'n)
matrix" datatype, but asked to be sure that there was no direct way to
achieve code generation from nested datatypes. If we have any further
questions on that we will let you know.
We were also aware of the AFP matrices implementation by René and
Christian, we already have used then succesfully in some other
experiment.
I am just speculating, but, would it be possible to set up the code
generator to generate, from a given "('a, 'n) vec" type, lists over
"'a" (of length ""card 'n")? Then, hopefully, matrices would be
"directly" generated to "lists of lists over 'a".
The question remains open how a given function representing a vector
should be generated to a list, but, once again, I was just
speculating.
Thanks for your ideas and your interest,
Jesus
Last updated: Nov 21 2024 at 12:39 UTC