Re: [isabelle] executable multiset-extension

See now


Am 05.05.2016 um 10:35 schrieb Florian Haftmann:
> 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
> 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.