Email Gateway (Aug 22 2022 at 13:17): Email Gateway (Aug 22 2022 at 13:17):From: Christian Sternagel <c.sternagel@gmail.com>
Dear list,
as far as I can tell "mult" from "~~/src/HOL/Library/Multiset" does not
support code generation at the moment.
So maybe the attached theory (which I extracted from recent work on
IsaFoR) is of general interest.
Summary: The main (but not new, and maybe obvious) observation is that
we may always drop the common part of two multisets that should be
compared (I got the idea to use the converse of a finite well-founded
relation in the main induction proof by Vincent van Oostrom). Now, when
checking whether "(N, M) : mult r", instead of guessing an arbitrary
decomposition "M = I + A" and "N = I + B" such that "ALL b :# B. EX a :#
A. (b, a) : r" (which currently does not support code generation and
would lead to a worst-case exponential implementation), we may always
choose "A = M - M #Int N" and "B = N - M #Int N" (which supports code
generation and yields a worst-case quadratic implementation).
However, since the equivalence between my implementation and "mult r"
basically requires "r" to be irreflexive and transitive, we only obtain
executable code for specific "r" (or rather its predicate variant; see
the attached file) satisfying these requirements.
cheers
chris
Executable_Multiset_Extension.thy
Email Gateway (Aug 22 2022 at 13:17):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
I will take care for this.
Just one question: since the equation is guarded by preconditions, how
do you apply it for code generation? By instantiating it to a specific
relation and generation code for that instance only?
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 13:17):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Florian,
right, that's what I apparently failed to convey ;)
But maybe you, or others know tricks to make code generation work
automagically for each suitable instance?
cheers
chris
Email Gateway (Aug 22 2022 at 13:18):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
But maybe you, or others know tricks to make code generation work
automagically for each suitable instance?
there are different approaches to make it work.
a) Provide a locale (»functorial style«)
locale executable_mult =
fixes r :: "'a => 'a => bool"
assumes irrefl: "irrefl r" and trans: "trans r"
begin
lemma [code]
"mult r = …"
using irrefl trans …
end
interpretation executable_mult foo …
b) Provide an abstract type (»dictionary passing style«)
typedef 'a irrefl_trans = "{r. irrefl r & trans r}" …
setup_lifting …
definition "R = Abs_irrefl_trans r"
lemma [code abstract]:
"Rep_irrefl_trans R = r" …
definition "mult_exec R = mult (Rep_irrefl_trans R)"
Depends on the particular application which one is preferrable.
Cheers,
Florian
cheers
chris
On Thu, May 5, 2016, 10:36 Florian Haftmann
<florian.haftmann@informatik.tu-muenchen.de
<mailto:florian.haftmann@informatik.tu-muenchen.de>> wrote:Hi Christian,
I will take care for this.
Just one question: since the equation is guarded by preconditions, how
do you apply it for code generation? By instantiating it to a specific
relation and generation code for that instance only?Cheers,
FlorianAm 04.05.2016 um 15:24 schrieb Christian Sternagel:
> Dear list,
>
> as far as I can tell "mult" from "~~/src/HOL/Library/Multiset"
does not
> support code generation at the moment.
>
> So maybe the attached theory (which I extracted from recent work on
> IsaFoR) is of general interest.
>
> Summary: The main (but not new, and maybe obvious) observation is that
> we may always drop the common part of two multisets that should be
> compared (I got the idea to use the converse of a finite well-founded
> relation in the main induction proof by Vincent van Oostrom). Now,
when
> checking whether "(N, M) : mult r", instead of guessing an arbitrary
> decomposition "M = I + A" and "N = I + B" such that "ALL b :# B.
EX a :#
> A. (b, a) : r" (which currently does not support code generation and
> would lead to a worst-case exponential implementation), we may always
> choose "A = M - M #Int N" and "B = N - M #Int N" (which supports code
> generation and yields a worst-case quadratic implementation).
>
> However, since the equivalence between my implementation and "mult r"
> basically requires "r" to be irreflexive and transitive, we only
obtain
> executable code for specific "r" (or rather its predicate variant; see
> the attached file) satisfying these requirements.
>
> cheers
>
> chris
>--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Email Gateway (Aug 22 2022 at 13:21):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
See now
http://isabelle.in.tum.de/repos/isabelle/rev/f2177f5d2aed
http://isabelle.in.tum.de/repos/isabelle/rev/40134ddec3bf
Florian
signature.asc
Last updated: Apr 19 2024 at 16:20 UTC