[isabelle-dev] Future of permanent_interpretation

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Nov 19 15:00:40 CET 2015 

Hi Clemens,

thanks for your feedback.

> 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.

This is part of the still ongoing struggle for consistent terminology.
Concerning equations, the term »rewrite morphisms« is established, but
this actually fits equally to equations and definitions alike.  The
difference is just how such morphisms are specified.  Correct phrases
would be »rewrite morphisms induced by equations« and »rewrite morphisms
induced by definitions«, but this is way to long.  Maybe »rewrite
equations« and »rewrite definitions« is something we could converge towards.

> 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?

Concerning c), a use case could be to activate some fancy syntax exactly
during the scope of a single theory, without spoiling descendant theories.

A sketched example for b):

	locale complete_lattice_syntax =
          fixes inf sup and Inf Sup

	locale complete_lattice = complete_lattice_syntax +
          assumes …

	locale conditionally_complete_lattice = complete_lattice_syntax
        begin

	definition some_funny_predicate …

	context
          fixes A
	  assumes "some_funny_predicate A"
        begin

        sublocale complete_lattice inf sup Inf Sup …

	end

OK, this uses sublocale rather than an interpretation into a global
theory, but the core issue is to demonstrate what the result of
interpretation in a nested local theory could be.  Here, we would get
properties of a complete lattice but guarded with an additional
predicate, e.g. ‹some_funny_predicate A ==> a : A ==> Inf A <= a›

> 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.

If you take the sentence »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.« and
substitute »sublocale« for »permanent_interpretation«, you'll end up
with the argument I once brought forward for unifying sublocale and
interpretation ;-).  Since then your argument that the specific impact
of »sublocale« should not be hidden behind a generic keyword has
convinced me to let it stand.  Anyway, I argue that to a lesser extent
this also applied to global interpretation into a theory: it has a
global impact that a user must oversee in order not to produce mess.
Hence my proposal to strictly separate it, using e.g.
»global_interpretation«.  This would emphasize the delicate nature of
»sublocal« and »global_interpretation« over the non-intrusive
»interpretation«/»interpret«.

> 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.

To some extent it is a transitional state, but it also exposes the very
confusion caused by one keyword »interpretation« with two quite
different classes of behaviour.

Beside that, I am currently working on the following issues:
* Proper treatment of polymorphism in rewrite definitions.
* Issuing definitions in a proper Local_Theory.open_target block rather
than low-level fiddling with the background theory.
* Re-consolidation of terminology in sources.
* Polishing of documentation.

Cheers,
	Florian

> 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
>>
>  
>  
>  
>  
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151119/f7d18893/attachment.sig>

More information about the isabelle-dev mailing list