[isabelle-dev] Future of permanent_interpretation

[Clemens Ballarin]

On 26 October, 2015 10:38 CET, Tobias Nipkow <nipkow at in.tum.de> wrote: 
 
> My desire to generate code from locale interpretations w/o having to make a 
> number of trivial function definitions was what started this whole business a 
> number of years back. Florian's very useful implementation of that really needs 
> to make it into Main.

It could simply be integrated with the current interpretation and sublocale commands, where the definitions could be supplied in a separate clause, as suggested by Florian, perhaps using "defines" as keyword.  Would this suit your needs?

(Independently I intend to change the keyword for the rewrite morphisms clause of these commands from "where" to "rewrites", to better distinguish it from named instantiations in locale expressions.)

> My understanding of "sublocale" is that it is an interpretation within a locale 
> and I have used that explanation in papers because I find it very succinct. Thus 
> I would welcome if the same keyword is used.

This view is of course valid, but it isn't the whole story.  With "sublocale" these interpretations are orchestrated in a manner such that the locale hierarchy is effectively changed.  Now I can see that there might be domains where this more abstract view is not relevant, but when working with a hierarchy of locales representing algebraic structures it is certainly appropriate.  It should also be kept in mind that "sublocale" is established in the locale documentation including my JAR paper [1].  If the desire for a different keyword is so strong, perhaps an alias might be a solution.

Clemens

[1] Clemens Ballarin. Locales: a module system for mathematical theories. Journal of Automated Reasoning, 52(2):123–153, 2014.


> On 25/10/2015 11:16, Clemens Ballarin wrote:
> > Hi Florian,
> >
> > this proposal goes too far, of perhaps, not far enough.  Let me explain.
> >
> > There is of course nothing wrong with providing new commands and enhancements for frequent use cases.  However, I don't see a good reason why users should be forced to write 'permanent_interpretation' where they could write 'interpretation' or 'sublocale'.
> >
> > I don't object to a careful evolution of the user interface to locales, but I don't think you're heading in the right direction.  Your 'permanent_interpretation' lets users make some definitions followed by, depending on the context, an interpretation or a sublocale declaration.  This is certainly useful, but it is not general enough for making it the preferred command.  For example, it doesn't permit function declarations.  It also blurs the distinction between 'interpretation' and 'sublocale' by calling the latter 'permanent_interpretation' when in a locale context, but not at the level of theories, but instead calling the former 'permanent_interpretation' at the level of theories.
> >
> > It should be kept in mind that in the current design the 'interpretation' commands are effective for the lifetime of their context: in theories they are therefore permanent, in context blocks they persist for that block and within a proof 'interpret' provides services for that proof.  This is pretty straightforward.  On the other hand, 'locale' and 'sublocale' are theory-level commands that relate a locale to a locale expression (which in both cases becomes a sublocale of the locale).  Their only difference is that 'locale' declares a new locale while 'sublocale' refers to an existing one.  We have allowed the use of 'sublocale' in locale contexts as a notational convenience, but I don't consider it a good idea to further blur the distinction between 'interpretation' and 'sublocale'.  Calling 'sublocale' 'permanent_interpretation' in some contexts and 'sublocale' in others is certainly bad.  The current design is, of course, not cast in stone, but for changing it, there has to be a 
> consistent vision first, so we know where we are heading.
> >
> > Certainly, your work has partly been inspired by the feeling that the current locale commands only provide the bare basics for manipulating locales.  For example, basing an interpretation or sublocale declaration on definitions is certainly something that could be done in a fancier manner.  The situation is perhaps a bit similar to that of 'axclass' several years ago, where your work on type classes has improved the user experience dramatically.  If you would like to bring locales forward, you might consider developing ideas along those lines.  The required definitions and proofs for an interpretation could for example be collected in a dedicated context in a step-by-step manner similar to that of class instantiation.  Your work also seems to be inspired by the desire to gradually rename 'sublocale' to 'interpretation', which I find surprising, because, compared to classes, 'sublocale' is the direct analogue of 'subclass' and 'interpretation' is the direct analogue of 'instantiation
> '.
> >
> > Clemens
> >
> >
> > On 13 October, 2015 15:13 CEST, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> >
> >> Recently in private discussion there was the question what the supposed
> >> future of permanent_interpretation is supposed to be.
> >>
> >> It looks as follows:
> >> Step 1)
> >> 	* Put »permanent_interpretation« into Pure directly.
> >> Step 2)
> >> 	* Careful revisiting of the documentation to emphasize the presence of
> >> permanent_interpretation.
> >> 	* »permanent_interpretation« as leading construct in the distribution
> >> and the AFP as far as appropriate
> >> Step 3)
> >> 	* Discontinue theory-global »interpretation«, which then is just a
> >> degenerated form of »permanent_interpretation«.
> >> 	* Discontinue locale-level »sublocale«, which then is just a
> >> degenerated form of »permanent_interpretation«.
> >>
> >> There will definitely be one release to breath between step 2 and step 3.
> >> Cheers,
> >> 	Florian
> >>
> >> --
> >>
> >> PGP available:
> >> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> >>
> >
> >
> >
> >
> >
> >
> >
> >
> > _______________________________________________
> > isabelle-dev mailing list
> > isabelle-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> >
>