Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)
Hi Jasmin,
There will be a high level of compatibility between the old and the
new package.
For nonnested recursive datatypes, compatibility is quasi-100%; and for nested
datatypes, the package will support an optional nested to mutual reduction
to
simulate the old package, so that the same theorems as before are available
(albeit under different names).
has an explicit need for a »nested to mutual« mode ever been
articulated? In my personal opinion this construction has always
appeared counter-intuitive, because the inherent redundancy with an
existing type springs to your eyes after you have done this game a few
times. Maybe a chance to save some work.
A rough, optimistic time plan follows.
Overall, a realistic and reasonable schedule.
October--December 2013 (?):
Release Isabelle2013-1 with both datatype and datatype_new
Spring 2014:
Rename {datatype |- legacy_datatype, datatype_new |- datatype}
Summer/Fall 2014:
Release Isabelle2014 with both legacy_datatype and datatype
Is there any experimental evicdence how many datatype specifications
would break by a drop-in replacement (real applications, not
demonstration examples)? If this is significantly little, I would even
think about doing the switch {datatype |- legacy_datatype,
datatype_new |- datatype} immediately. The »_new« suffix has a
strange connotation of »almost done… ad multos annos«.
Cheers,
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] New (Co)datatypes: Status Plan (FYI)
Hi Jasmin,
What is the proper technical term for that? Isn't it just corec?
If the proper name for primrec is primrec, then the proper name for this
is primcorec.
I wouldn't mind killing the prim -- after all, the recursor constants are
just called _rec -- but that's an orthogonal question. Another alternative:
prim_rec and prim_corec.
To add a further dimension to the design space, there was once the idea
of a generalized primrec in the manner:
1. recursive specification following some pattern considered »primitive«
2. foundational definition of this specification using a suitable
recursion combinator
3. maybe some proof by the user that certain conditions a satisfied
4. deriving the original specification again
A new command »primitive_recursion« would then expose (3) to the user,
whereas the existing »primrec« would assume a trivial proof instead
(similar in appearance like the pair »function« and »fun«)
An example could be something like
primitive_recursion card :: 'a set = nat
where
card {} = 0
card (insert x A) = Suc (card A)
proof -
show !!x y. insert x o insert y = insert y o insert x
show !!x. insert x o insert x = insert x
qed
thm card.simps -- {*
card {} = 0
finite A == card (insert x A) = Suc (card A)
*}
using Finite_Set.fold internally.
Apart from that aside, are separated keywords for primrec and primcorec
really needed, or can they be distinguished just syntactically?
The corecursive counterpart to fun, corecursion up-to, is something Andrei
urges us to work on, but where Dmitry and I are applying the brakes because
of the pile of work that remains to be done on the new (co)datatype package
before we can consider adding such nice features. In fact, inspired by Leino
et al.'s (co)recursion mixture in Dafny [*], Andrei has some ideas to support
some recursion in conjuction with corecursion up-to.
Agree. Such a fundamental replacements needs some time to iron out
properly, before new floors can built on top.
Also related to the new (co)datatypes: Larry pointed out in private that my
email to the mailing list didn't mention performance (compared with the old
package). Performance is generally decent, but we're fighting with n-way
mutual recursive defitions where n = 8. This is certainly solvable by
changing the LFP construction, and perhaps Brian's simplifications, which we
haven't incorporated yet, would solve this; but until this is addressed, we
cannot realistically hope to dislodge the old package. This goes to show once
again how challenging (but also rewarding) package writing can be.
I guess (co)primrec(_new) has no problem with performance. Concerning
datatypes, this is indeed an issue which deserves attention. We have
still some recdef applications not migrated yet to function due to
performance issues.
Cheers,
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] Converting existing proofs from apply-style to structured Isar-style
Hi Josh, QUESTION STATED BRIEFLY: If I convert existing proofs in src/HOL/**.thy from apply-style to Isar-style, would those changes be welcome in the main repository? beyond the general hints given by Makarius, you could go the following way: a) Find a nice example (section) in theories sources. b) Do a quick plausibility check that there has been no movement in the repository tip concerning that particular example(s) (http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL). c) Post a announcement here. d) If nobody objects, go ahead and isarify. e) Post the resulting refinement here. Also note that if you want to practice Isar, there are also plenty of AFP theories which would profit from isarification and are a less critical point to start with. My personal favorite is the lattice development in http://sourceforge.net/p/afp/code/ci/default/tree/thys/JinjaThreads/DFA/. Cheers, 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] New (Co)datatypes: Status Plan (FYI)
Am 04.08.2013 18:57, schrieb Florian Haftmann: For nonnested recursive datatypes, compatibility is quasi-100%; and for nested datatypes, the package will support an optional nested to mutual reduction to simulate the old package, so that the same theorems as before are available (albeit under different names). has an explicit need for a »nested to mutual« mode ever been articulated? In my personal opinion this construction has always appeared counter-intuitive, because the inherent redundancy with an existing type springs to your eyes after you have done this game a few times. Maybe a chance to save some work. I also find it always counter-intuitive when I have to use it (of course the have to will not apply anymore in our case). However the mutualized primrec seems to be more flexible. Without the mutualization, in order to define a primitive recursive function on say datatype 'a tree = Node 'a 'a tree list one is allowed to apply the recursive calls through the map on lists only. Defining a function that additionally filters the nested list of children becomes counter-intuitive then. There is also a more technical reason why we want to perform the nested to mutual reduction: It gives us a very cheap compatibility layer for the old package. I.e. everything that is defined by the new package and falls into the fragment of the old package can be registered as an old datatype benefiting from all the infrastructure built around it (e.g. size function, Quickcheck, and other datatype interpretations). We expect this actually to save much work, compared to reimplementing that functionality now before moving to Main (instead we can do it in a lazy fashion). Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)
On 08/04/2013 07:09 PM, Florian Haftmann wrote: To add a further dimension to the design space, there was once the idea of a generalized primrec in the manner: 1. recursive specification following some pattern considered »primitive« 2. foundational definition of this specification using a suitable recursion combinator 3. maybe some proof by the user that certain conditions a satisfied 4. deriving the original specification again A new command »primitive_recursion« would then expose (3) to the user, whereas the existing »primrec« would assume a trivial proof instead (similar in appearance like the pair »function« and »fun«) That sounds like a derivation of a primitive recursion specification over an ad-hoc nonfree datatype that specifies the primitive pattern. Andrei and I submitted a paper on nonfree datatypes to CPP 2013: http://home.in.tum.de/~schropp/nonfree-data.pdf (see appendix for recursors on finite sets) Integration with the new datatype package is possible by registering the nonfree datatypes as BNFs. Cheers, Andy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] some actual find_theorems functionality (fb1f026c48ff)
Hi isabelle-dev, Makrius should know already, but I think it is a good idea to inform everyone here that a current student's project is about to provide a bit more advanced user interface for the find theorems functionality. It should be finished in two weeks time. Fabian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)
There is also a more technical reason why we want to perform the nested to mutual reduction: It gives us a very cheap compatibility layer for the old package. I.e. everything that is defined by the new package and falls into the fragment of the old package can be registered as an old datatype benefiting from all the infrastructure built around it (e.g. size function, Quickcheck, and other datatype interpretations). We expect this actually to save much work, compared to reimplementing that functionality now before moving to Main (instead we can do it in a lazy fashion). That's indeed the striking point. Thanks for explaining. 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] New (Co)datatypes: Status Plan (FYI)
On Sunday, August 4, 2013 at 20:32:50 (+0200), Dmitriy Traytel wrote: I.e. everything that is defined by the new package and falls into the fragment of the old package can be registered as an old datatype benefiting from all the infrastructure built around it (e.g. size function, Quickcheck, and other datatype interpretations). On the topic of size functions: I found it always odd that the existing datatype package (however I think this particular functionality is now provided by the function package) defines under datatype_name.simps two definitions of the corresponding size function. Consider for example datatype test = A1 | A2 | A3 test thm test.size test_size A1 = 0 test_size A2 = 0 test_size (A3 ?test) = test_size ?test + Suc 0 size A1 = 0 size A2 = 0 size (A3 ?test) = size ?test + Suc 0 Surely, it would be more uniform to have just the equations for size, no? Is there any usage for the test_size definitions? If not, then maybe in the course of updating the datatype package, this oddity can be eliminated (Nominal needed to work around it). But I am happy to admit that I might miss something important. Best wishes, Christian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)
Hi Florian,
Am 04.08.2013 um 18:57 schrieb Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de:
has an explicit need for a »nested to mutual« mode ever been
articulated?
Yes, on a couple of occasions. First, as Dmitriy mentioned, compatibility is
important -- I certainly don't want to be at the receiving end of emails
written by angry Australians. Second, I explicitly asked one of our power users:
to what extent to you agree or disagree with the following claims?
1. Porting existing old-style specs to the new style is difficult enough,
and
the scenario arises often enough, that it would be desirable/necessary
for
the new package to support it.
2. Even for new specifications, the old style is sometimes preferable.
Hence it
should be encouraged and fully supported, presumably even for
codatatypes.
He or she answered:
I strongly agree with both. I see an analogy with fold(l/r): Many functions
in Isabelle could be defined as folds, but hardly anybody does, because the
terms are unreadable once you unfold the definition in a goal. For
(co)datatype, the common case of recursion through 'a list in general leads
exactly to the foldr definition. And usually, you want different equations
than those for foldr for combining the lists. So, you introduce the constant
and abstraction and rewrite the equations afterwards.
To avoid heated debates, we want to support both the modular view and the
nonmodular view, in all combinations, and also for primcorec. (Moreover, it's
an interesting academic challenge; we're not aware of any literature about
doing this reduction at the level of (co)recursions and (co)induction
principles.)
Overall, a realistic and reasonable schedule.
Great! I fear the schedule erring on the optimistic side, but in any case do
expect some constant progress, because we are not going to give up after two
years of work on this.
Is there any experimental evicdence how many datatype specifications
would break by a drop-in replacement (real applications, not
demonstration examples)? If this is significantly little, I would even
think about doing the switch {datatype |- legacy_datatype,
datatype_new |- datatype} immediately. The »_new« suffix has a
strange connotation of »almost done… ad multos annos«.
It appears highly desirable to have at least one iteration of official Isabelle
release where datatype_new is more or less a drop-in replacement for
datatype, so that it gives plenty of time for developers of huge theories
(e.g. the Australians) to experiment with it, one type at a time, and give us
their feedback.
Another reason for procrastination is that we're getting a bit close to the
Isabelle2013-1 release. By the time we're done with primrec_new and the
nested-to-mutual reduction, we should look into convergence, not divergence.
Dmitriy also mentioned some reasons, related to the need to adapt some
infrastructure (e.g. the interpretation mechanism, used for size and many
other extensions).
Finally, there's the performance issue I mentioned in another email regarding
n-way mutual recursion for n = 8 approximately. I'm sure this will bite one or
two users at least. We'll need to take a very close look at that, but unlikely
before the next release.
Thanks for your interest and comments!
Cheers,
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
