[isabelle-dev] Future of permanent_interpretation

[Clemens Ballarin]

Hi Florian,

I looked at the documentation generated with this patch, and the first impression of the "Locale interpretation" section is that it now looks funny -- probably due to the transitional nature of the patch.  For "interpretation" there are now two declarations and two productions, while previously they were merged into one.  The current state is confusing.  Readers must be able to quickly identify what is relevant by looking at the keyword.

>From what I saw it looks as if we could get rid of a second keyword for interpretation by just merging the "defines" clauses into "interpretation".  I am not concerned about the "defines" clause only being available in some kinds of contexts.  From a user perspective, being able to say "interpretation" regardless of the context will be more natural than having to remember whether "interpretation" or "permanent_interpretation" (for example) is the right keyword.  The command could simply raise an error if a "defines" clause is used in situations where it is not available.

Regarding your concerns b) and c) I'm not sure I fully understand them.  Regarding b), while it might be conceptually possible to make an interpretation from a locale context (say) in a theory, I don't think the proof document would read very well.  Regarding c), making an interpretation in a theory but confine it to the closing "end" keyword of the theory, this is conceivable, but do we have a use case for this?  Should we decide to go for such functionality in the future I would be more comfortable with modifiers rather than long keywords.

I have seen that you use the term 'mixin definition' in NEWS and isar-ref.  I'm not sure this is needed but if so it must be explained.

Clemens


On 15 November, 2015 10:53 CET, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote: 
 
> For further discussion, see now fd4ac1530d63, particulary
> src/Pure/Isar/interpretation.ML and 5.7.3 »Locale interpretation« in
> *isar-ref*.
> 
> This goes along the following lines:
> 
> * »Interpretation« in general is used as generic heading for every kind
> of intepretation into different destination contexts.
> * *interpretation* in particular denotes interpretation into a confined
> context. (The wording in the implementation is not yet consistent,
> ranging from »epheremal« to »confined«; I have a slight inclination to
> stick to the latter). *interpret* is the variant for proof blocks. This
> use of terminology IMHO is consistent with typical uses in mathematics
> and there had been little debate about that so far.
> 
> So far for the seemingly non-controversial matter.
> 
> Concerning the »persistent« / »permanent« / »subscribing« kinds of
> interpretation, there are two conflicting views so far:
> 
> * Each local theory can »subscribe« to locales, given that it underlying
> target implements it. Hence all targets (particularly, global theories
> and locales) are treated uniformly, using one keyword
> *permanent_interpretation.*
> * The user interfaces emphasizes the non-trivial differences between
> »subscription« into global theories and into locales, particularly the
> side effects of the latter on the existing locale hierarchy.
> 
> Personally I have no strong inclination to follow the one or the other
> and I am happy to abandon the first in favour for the second. However
> then I also suggest a dedicated keyword for interpretation into global
> theories:
> a) *interpretation* would otherwise be strangely overloaded, allowing
> mixin definitions on the level of global theories but not in other local
> theories.
> b) Conceptually it would also be possible to allow »subscribing«
> interpretation into global theories inside a nested local theory
> (although it is not clear whether our current implementation is actually
> suitable for that). Then *theory* … *context* … *begin … interpretation*
> would be ambiguous.
> c) Similarly, also a theory itself can be seen as a confined context
> block, making *theory* … *interpretation* itself ambiguous.
> Suitable candidates could be *theory_interpretation *or
> *global_interpreation*. Better suggestions welcome. Of course, the
> actual replacement would not occur in the upcoming but a later release.
> 
> On that single matter I want to excite some feedback before continuing.
> Also suggestions on 5.7.3 »Locale interpretation« in *isar-ref* are welcome.
> 
> Cheers,
> 	Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>