[isabelle-dev] Interpretation in arbitrary targets.

[Florian Haftmann]

Hi Clemens,

nice to hear from you.

Let me add my perspective here, and see how we can converge.

> 2. sublocale and interpretation are more different than it looks:
> interpretation provides inheritance of mixins (or, from the user
> perspective, rewrite morphisms) and it is possible to amend mixins in
> interpretation (currently only through the API).

Yes.  The underlying primitive mechanisms (I tend to follow locale.ML
here and call them »registrations« and »dependencies«) are different and
will always be.

> On the other hand, I see that interpretation in a locale context can
> help working in an incremental fashion in such a context (which I assume
> is the motivation for your patches).
> 
> So, what should interpretation in a locale be like?  Currently,
> sublocale is used for two purposes:
> 
> a) relating two locales to each other (such as "a total order is a
> lattice")
> 
> b) import (a typically small number of) lemmas, which are needed for
> establishing some result, from one locale A into another locale B

Ack.  I tend to compare a) with a watering can.  There is currently no
chance to achieve b) except inside proofs.  b) would be one of the most
important use cases for locales also, since the watering can is only
appropriate in very »canonical« situations, type classes being one
prominent case.  In my terminology, I tend to call a) »subscription«, to
emphasize the permanent character.

But note that in my way of thinking, the current »interpretation« and
»sublocale«  commands are different facets of »subscription«.  Indeed, I
was first considering to rename the target-sensitive interpretation
command »subscription«.  However the name does not so much matter for
me.  Now your argument is that »interpretation« and »sublocale« should
be kept apart since they are implemented by different means
(»registrations« vs. »dependencies).  But this is what local theories
are about: abstract over the common essence.  That the underlying
primitive mechanisms also allow different things should not bother here:
e.g. you can add axioms to global theories but not to locales, but this
does not invalidate the local theory concept either.

> 1. sublocale modifies the locale graph of the underlying theory.  This
> is a big change and shouldn't happen as a side effect of a command in a
> target context.

Changing the underlying target is the essence of commands in target
contexts – in the case of interpretation (in …), it is not a side
effect, but the central issue.  You might argue that »interpretation«
suggests a different thing, but maybe then we have to choose a different
name for that, see above.

But see now how scenario b) would integrate into my design.  Recently
the local theory concept has been enriched with free-floating contexts

	context
	  fixes … assumes …
	begin

  	…

	end

Now what would

	context
	  …
	begin

  	…

	interpretation

	…

	end

be?  Currently, there is check that »interpretation« may only be issued
at the bottom level of the local theory stack, outside any free-floating
context.  Although I have no constructive proof at hand yet, I believe
that by lifting the check appropriately we get b) for free: similar to
»interpret«, this would only yield facts inside the context (whose
bindings disappear after »end«) without any additional dependencies or
registrations.  This is also why I adhered to »interpretation« in the
end.  So, your example could somehow look like

context B begin
  context
  begin
    interpretation A
  end
  context
  begin
    interpretation A'
  end
  context
  begin
    interpretation A''
  end
  interpretation A'' -- {* permanent subscription *}
end

You might still argue about syntax, e.g. having separate commands
  subscription – what is currently interpretation and subscription, not
in free-floating contexts (as implemented in the patches).
  interpretation – only in confined contexts (locales, context begin …
end, but not global theories any longer) without any subscription.

Overall I am amazed how well this all would fit to the existing local
theories.

> What do you think of these ideas?  I would appreciate, if you could work
> towards them (I myself never quite mastered the intricacies of the ML
> level target code).

Restarting after some years left aside, I slowly start to comprehend the
details…

Cheers,
	Florian

-- 

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: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130326/1634d24e/attachment.sig>