[isabelle-dev] Future of permanent_interpretation

Thu Oct 29 12:19:40 CET 2015

I am very happy to see that we agree that a "defines" section is a useful 
addition to the interpretation command. But at the moment, this section only 
exists for "permanent_interpretation".

It would be nice if "interpretation" were enhanced with "defines", in which case 
people could make use of it w/o having to learn about and load 
"permanent_interpretation" (whose future is still under discussion).

Tobias

On 29/10/2015 11:31, Florian Haftmann wrote:
> Hi Clemens et al.,
>
> let me put things in a broader perspective. I think we have two views on
> the whole machinery:
>
> * The algebraic view with locales, sublocale statements and (somehow
> global) interpretation statements. This view is important because it
> essentially describes the implementation of the whole thing.
>
> * The »local everything« view, where you have certain targets which
> allow certain operations, most notably »notes«, »defines«, and something
> which might internally be called »subscribes«, a permanent connection to
> existing locales covered by a locale expression. Internally, this falls
> back to existing mechanism, particularly »sublocale« for subscriptions
> into locales. But note that this is only the typical sandwich principle
> of target implementations, similiarly to definitions in locales which
> are essentially global definitions plus an abbreviation, which appears
> in theory text as plain »definition« nonetheless!
>
> (Also note that »subclass« is something special between type classes
> only, it is not a generic »local everything« construct.)
>
> We may well come to the conclusion that both views are legitimate to be
> present in user space, i.e. as isar keywords; although this is not very
> common in Isabelle, it may be attributed to the complexity of the
> machinery itself.
>
> However I forsee two possible future extensions where both notions are
> in conflict an a decision has to be made.
>
> Starting point: there has been the decision that »interpretation« in
> confined contexts (locales, classes, nested contexts, …) denotes
> epheremal interpretation.  This fits nicely with »interpret« in proofs.
>
> But
>
> a) Also a theory is a confined context »theory … begin … end«; although
> we are technically far off from that, in future it might be possible to
> issue interpretation epheremal inside a particular theory only, and in
> the current setting this would just be »interpretation«, demanding an
> alternative keyword for subscriptions into theories.
>
> b) Similarly, also interpretation in a »context … begin … end« block
> might include a subscription into the surrounding target, leaving
> additional premises in the results of subscription.  As a possible
> example, think of conditionally complete lattices which subscribe to a
> existing complete
> lattice locale under the premise of an additional predicate.  Again, if
> the surrounding target is a theory, how would the keyword look like, as
> »interpretation« is already needed for epheremal interpretation?
>
> So, if we want to maintain both views in the long run consistenly, we must
> 1) either find an alternative keyword for interpretation/subscription
> into theories
> 2) or find an alternative keyword for epheremal interpretation.
>
> In the light of this, some minor remarks:
>
>>>>> Your 'permanent_interpretation' lets users make some definitions
>>>>> followed by, depending on the context, an interpretation or a
>>>>> sublocale declaration.
>
> Note that it is just a restriction of the current implementation that
> permanent_interpretation requires either a theory or a locale/class
> target; each target is able to provide its own implementation for that,
> and currently only these to do so.
>
>>>>> 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.
>
> This »blurring« is inherent in the »local everything« approach.
> »definition« in locale targets is essentially an abbreviation, but
> called that nonetheless.
>
>>>>> 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
>
> It is not clear whether the »lifetime« of theories should exceed the
> final »end« or not.
>
>>>>> 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.
>
> According to my feelings, the whole locale machinery is an excellent and
> powerful part of the systems.  The addition of mixin definitions as
> special case of mixin rewrites do not touch the foundations (locale.ML /
> expression.ML) at all – there is no restriction to achieve the same
> result withotuh them.
>
>>>>> 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 'instantiati
>> on
>>>> '.
>>>>>
>>>>> 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
>>>>>
>>>>>
>>>>
>>>
>>>
>>>
>>>
>>>
>>
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151029/cb9cfa7d/attachment.bin>