Re: [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 
 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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Future of permanent_interpretation

[Florian Haftmann]

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



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Future of permanent_interpretation

[Florian Haftmann]

> What is the conclusion of this thread for the coming release? Whatever
> happens, the time window for it is approx. Nov/Dec 2015.

The situation is still somehow inconclusive.  I am working currently to
re-integrate permanent_interpretation »as it is« into Pure, to provide a
base for further discussion and clarification.  This will still take
some time but I am confident that this thread shall be over at the end
of this year.

Until then,
Florian

-- 

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



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Future of permanent_interpretation

[Clemens Ballarin]

 On 09 November, 2015 11:56 CET, Makarius  wrote: 
 
> It is formally trivial to have 'permanent_interpretation' in Isabelle/Pure 
> as separate command. If there is a simple way to have just one 
> 'interpretation' command with 'defines' vs. 'rewrites', I would prefer 
> that.

I would prefer to just have 'interpretation' as well.  Possibly 'sublocale' 
should also be extended by a 'defines' clause.

Clemens
 
 


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Future of permanent_interpretation

[Makarius]

What is the conclusion of this thread for the coming release? Whatever 
happens, the time window for it is approx. Nov/Dec 2015.


Historically, the 'permanent_interpretation' command had to stay outside 
Isabelle/Pure and Main Isabelle/HOL, because it was overwriting the 
'interpretation' command in an ad-hoc manner -- causing a lot of confusion 
to everybody.  (This incident also accelerated the strict discpline of 
authentic commands.)


It is formally trivial to have 'permanent_interpretation' in Isabelle/Pure 
as separate command. If there is a simple way to have just one 
'interpretation' command with 'defines' vs. 'rewrites', I would prefer 
that.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Future of permanent_interpretation

[Clemens Ballarin]

Hi Florian,

thanks for your feedback.  Local theories have done Isabelle and its users a 
great service in presenting a uniform view of different kinds of declarations 
in several contexts, and the locales reimplementation would have been much more 
painful without them.  However, if "local everything" forces us to name 
commands in the proof language after features that I would consider secondary 
(permanent vs. ephemeral interpretation) rather than primary (simple 
interpretation vs. interpretation that changes the locale hierarchy) then we 
need to check whether we are pushing this idea too far.

Clemens


On 29 October, 2015 11:41 CET, Florian Haftmann 
 wrote: 
 
> (this continues the previous mail)
> 
>  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 without them.  This implementation simplicity is the main reason
> I dared to undertake this adventure.
> 
> > This is certainly useful, but it is not general enough for making it the 
> > preferred command.  For example, it doesn't permit function declarations.  
> 
> I don't think this generality is needed.  The idea behind mixin
> definitions could be fomulated as »reinterpret this term as a new
> definition«; the properties are already there afterwards, there is no
> need for definitional extensions or construct them.
> 
> > 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.
> 
> This could be thought of, but is another story.
> 
> > 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
> > '.
> 
> You are right with the type class / locale analogy.  But type classes
> only permit the algebraic view, they are too restricted for the »local
> everything« approach.  As mentioned in my previous mail, I am happy to
> leave both views stand in the long run, if we find a way to sort out the
> (now still hypothetic) corner cases of epheremal interpretation on the
> theory level and permanent interpretation in a nested context.
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
 
 
 
 


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Future of permanent_interpretation

[Tobias Nipkow]

On 28/10/2015 21:41, Clemens Ballarin wrote:

On 26 October, 2015 10:38 CET, Tobias Nipkow  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?


That would be just fine.


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


Thanks for the explanation. Since sublocale is more than a local interpretation, 
I withdraw my comment.


Tobias


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 

Re: [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 

Re: [isabelle-dev] Future of permanent_interpretation

[Florian Haftmann]

(this continues the previous mail)

 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 without them.  This implementation simplicity is the main reason
I dared to undertake this adventure.

> This is certainly useful, but it is not general enough for making it the 
> preferred command.  For example, it doesn't permit function declarations.  

I don't think this generality is needed.  The idea behind mixin
definitions could be fomulated as »reinterpret this term as a new
definition«; the properties are already there afterwards, there is no
need for definitional extensions or construct them.

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

This could be thought of, but is another story.

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

You are right with the type class / locale analogy.  But type classes
only permit the algebraic view, they are too restricted for the »local
everything« approach.  As mentioned in my previous mail, I am happy to
leave both views stand in the long run, if we find a way to sort out the
(now still hypothetic) corner cases of epheremal interpretation on the
theory level and permanent interpretation in a nested context.

-- 

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



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Future of permanent_interpretation

[Tobias Nipkow]

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 

Re: [isabelle-dev] Future of permanent_interpretation

[Clemens Ballarin]

On 26 October, 2015 10:38 CET, Tobias Nipkow  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 

[isabelle-dev] Future of permanent_interpretation

[Florian Haftmann]

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



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev