Re: [isabelle] executable multiset-extension

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?


Am 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:

Attachment: signature.asc
Description: OpenPGP digital signature

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