[isabelle-dev] Future of permanent_interpretation

[Florian Haftmann]

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
> 

-- 

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