Re: [isabelle] Code generation from abstract types



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

On Thu, Dec 27, 2012 at 1:30 PM, René Thiemann <rene.thiemann at uibk.ac.at> wrote:
> 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é
>
> Am 27.12.2012 um 10:17 schrieb Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
>
>> Hi Jesus,
>>
>>> When we try to generate code for operations over matrices which return
>>> a matrix (for instance, matrix multiplication), we do not know how to
>>> define the "code abstract" lemma for such operation, since it involves
>>> a "vec_nth of a vec_lambda of a vec_nth", for which the code generator
>>> produces a "violation abstraction error":
>>>
>>> lemma mat_mult [code abstract]: "vec_nth (m ** m') = (%f. vec_lambda
>>> (%c. setsum (%k. ((m$f)$k) * ((m'$k)$c)) (UNIV :: 'n::finite set)))"
>>>  unfolding matrix_matrix_mult_def
>>>  using vec_lambda_beta by auto
>>>
>>> Is there a way to express the previous lemma and that code generation
>>> for matrix multiplication is still possible? Is anybody aware of any
>>> possible workaround?
>>
>> 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.
>>
>> --
>>
>> PGP available:
>> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.