Hi Florian,
Am 04.08.2013 um 18:57 schrieb Florian Haftmann
<[email protected]>:
> 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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
