Re: [isabelle-dev] Remaining uses of defer_recdef?
On 7 Jun 2015, at 07:38, Dmitriy Traytel tray...@in.tum.de wrote: I'm not sure if this is something for the repository though, since it has a factor of 2 impact on the build-time: Thanks for investigating. But how do we explain this? Possibly “fun” insists on converting on creating unconditional patterns only, while “recdef” allows conditional equations. But one could easily insert conditions manually in order to simplify the set of patterns. There are 14 instances of recdef in Cooper.thy. Do any of them stand out as extra slow? Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of defer_recdef?
So are there any experience reports that the combinatorial explosion in pattern matching in fun/function had to be worked around somehow? Or do we have to conclude that the pattern complexity of the applications in src/HOL/Decision_Procs is indeed domain-specific? I have some experience with the combinatorial explosion in fun. You don't need much: just take extended regular expressions (~10 constructors) and define binary normalizing constructors (by some sequential pattern matching on both arguments). The AFP entry MSO_Regex_Equivalence is full of ~30 sec fun declarations. While this is still on the edge of being bearable, try to add one more constructor... (I've seen examples where fun from 10 lines of specification produced something like 10^5 simp equations.) In a different formalization (AFP entry Formula_Derivatives) where I needed to have more then 10 constructors, I had to work around the function package by separating the datatype into two and defining the functions separately. (In the end, the separation had also positive effects, but still it felt like fighting the system when doing it.) OK, the dragons are still there and not just a historic relic. Note that the domain is quite similar to Cooper---syntactic manipulations of expressions/formulas---but isn't it what we do quite often in Isabelle? Orthogonally, I have no idea, whether recdef would have helped me. I would definitely not suggest to use recdef for any new application… the open question is whether we have to think about a refinement or extension of function. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of defer_recdef?
On 7 Jun 2015, at 07:38, Dmitriy Traytel tray...@in.tum.de mailto:tray...@in.tum.de wrote: I'm not sure if this is something for the repository though, since it has a factor of 2 impact on the build-time: Thanks for investigating. But how do we explain this? Possibly “fun” insists on converting on creating unconditional patterns only, while “recdef” allows conditional equations. But one could easily insert conditions manually in order to simplify the set of patterns. As far as I know, this is due to layered architecture of the function package. »recdef« does everything in one bunch and can hence optimize for sequential pattern matching. Each layer of »function« must feed its result to its successor in a standardized form, and since there is no overall concept of sequential pattern matching, it has to be compiled away once and for all from the very beginning. (roughly spoken) An optimization would require a modified architecture. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of defer_recdef?
I could not believe that recdef could not be replaced by fun, so here is the patch that removes usages of recdef from Decision_Procs. The proof rules that come out of the function package are fine (one just needs a few split_format (complete) attributes in a few places). I'm not sure if this is something for the repository though, since it has a factor of 2 impact on the build-time: recdef: Finished HOL-Decision_Procs (0:03:53 elapsed time, 0:13:26 cpu time, factor 3.45) fun : Finished HOL-Decision_Procs (0:08:24 elapsed time, 0:28:10 cpu time, factor 3.35) On the other hand 8 minutes is still not much. The longest fun invocation (numadd in MIR) takes about 2 minutes, other are all below 20 seconds. A compromise could be to let just the 2 min recdef stand and migrate the others… Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of defer_recdef?
I suggest looking for ways for users to avoid exponential blowup. Presumably this means avoiding deeply nested patterns in favour of conditional expressions in some cases. Such a formalisation might be easier to reason with too, who wants an induction rule with hundreds of cases? But coming up with simple guidelines for users might be tricky. Larry On 7 Jun 2015, at 20:33, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: As far as I know, this is due to layered architecture of the function package. »recdef« does everything in one bunch and can hence optimize for sequential pattern matching. Each layer of »function« must feed its result to its successor in a standardized form, and since there is no overall concept of sequential pattern matching, it has to be compiled away once and for all from the very beginning. (roughly spoken) An optimization would require a modified architecture. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of defer_recdef?
I could not believe that recdef could not be replaced by fun, so here is the patch that removes usages of recdef from Decision_Procs. The proof rules that come out of the function package are fine (one just needs a few split_format (complete) attributes in a few places). Let me emphasize this particular point. When you give a specification in Isabelle, there are two expectations: a) The system is able to construct something which satisfies this specification (the primitive definition) AND b) The system provides a mechanism to actually *reason* about resulting properties in a (natural, intuitive, straight-forward) way (for non-trivial specifications, typically an induction rule) Practically, a) is of little (or at least reduced) value without b) Hence, if there is evidence that working around function's pattern explosion diminishes b), it is definitely a restriction and not just a matter of taste how to construct and design specifications. The question what can really be done to improve the situation, however, is written on a different sheet. Florian P.S: Just a remark: in my personal view b) is even the dominant role of advanced specification tools – the way how a specification is given suggests how proofs can be conducted successfully. Hence I still prefer »primrec« if applicable since this makes it immediately clear that proofs most likely will require induction on the corresponding datatype. -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of defer_recdef?
On Sat, 6 Jun 2015, Gerwin Klein wrote: On 06.06.2015, at 21:23, Makarius makar...@sketis.net wrote: (2) 'defer_recdef' which is unused in the directly visible Isabelle universe. So it could be deleted today. This mailing list thread is an opportunity to point out dark matter in the Isabelle universe, where 'defer_recdef' still occurs. Otherwise I will remove it soon, lets say within 1-2 weeks. Unused in our part of the dark matter universe as well. The thread has shifted over to actual 'recdef'. Are there remaining uses of 'recdef' in the NICTA dark matter? So far I always thought the remaining uses in HOL-Decision_Procs are only a reminder that there are other important applications. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of defer_recdef?
Hi, I could not believe that recdef could not be replaced by fun, so here is the patch that removes usages of recdef from Decision_Procs. The proof rules that come out of the function package are fine (one just needs a few split_format (complete) attributes in a few places). I'm not sure if this is something for the repository though, since it has a factor of 2 impact on the build-time: recdef: Finished HOL-Decision_Procs (0:03:53 elapsed time, 0:13:26 cpu time, factor 3.45) fun : Finished HOL-Decision_Procs (0:08:24 elapsed time, 0:28:10 cpu time, factor 3.35) On the other hand 8 minutes is still not much. The longest fun invocation (numadd in MIR) takes about 2 minutes, other are all below 20 seconds. Dmitriy On 07.06.2015 07:18, Amine Chaieb wrote: I remember trying to convert Cooper's as well as other Decision proc's recdefs to fun, also with the help of Alex but gave up at some point. I think the killer at the time was rather the induction principle and not the simp rules. The one derived by recdef really fits the definition and spirit of development. Also runtime at the time was not acceptable. I also remember havin the runtime problem with fun vs. primrec (so we left those there too). Context: Deep embedding of datatype + normal form on this data type + set of recursive functions on syntax preserving normal form. The normal Form has conditions on nested patterns -- introduce new constructor for these common nested patterns in normal form. We had combinatorial explosion due to the depth of the patterns (which is the main reason to introduce special constructors in the datatype, to reduce deep patterns). The induction priciples with recdef really fitted, i.e. induct auto with spice did the job for lemmas you do not expect to spend time thinking as a software developer. One could argue that one should introduce a new data type for normalized syntactic elements and perform such computations as needed. I dismissed this idea and did not explore it, since it comes with a high price. Perhaps there are better ways to do the formalization. Amine. On 06/06/2015 08:37 PM, Tobias Nipkow wrote: On 06/06/2015 20:11, Larry Paulson wrote: Pattern matching is a convenience, and can always be eliminated manually. Is there really no reasonable way to re-express the definitions in Cooper.thy? You can always turn all patterns of the lhs into cases on the rhs and derive the individual equations as lemmas. You also need to derive an induction principle. I would rather keep recdef than do all that by hand. Tobias Larry On 6 Jun 2015, at 16:11, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: The reason for the continued existence of recdef is that function can cause a combinatorial explosion the way it compiles pattern matches. I just tried Cooper.thy and changing one of the recdefs to function makes Isabelle go blue (purple) in the face until one gives up. Hardware alone will not solve that one. Now one could argue that since we need recdef, we should also keep the special variant defer_recdef, but if nobody speaks up for it, we don't have a proof that we really need it and it should go. At the time of their writing the recdef examples in (nowadays) src/HOL/Decision_Procs were the power applications of their times. Since then power applications have grown bigger and bigger and fun/function have been used widespread. It seems strange to me that no application since then had never hit the same concrete wall again. So are there any experience reports that the combinatorial explosion in pattern matching in fun/function had to be worked around somehow? Or do we have to conclude that the pattern complexity of the applications in src/HOL/Decision_Procs is indeed domain-specific? Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev # HG changeset patch # User traytel # Date 1433658664 -7200 # So Jun 07 08:31:04 2015 +0200 # Node ID 03ef7232e0f060ed68756b902bd55ec9a51ed9b7 # Parent 392402362c3e01d9556b59674ce2d4f38903bd0b get rid of recdef from Decision_Procs diff -r 392402362c3e -r 03ef7232e0f0 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Fr Jun 05 09:15:37 2015 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy So Jun 07 08:31:04 2015 +0200 @@ -6,7 +6,6 @@ imports Complex_Main
