Email Gateway (Aug 22 2022 at 10:41): Email Gateway (Aug 22 2022 at 10:41):From: Julian Brunner <julianbrunner@gmail.com>
Dear all,
Isabelle will not contract the abbreviations introduced for locale
definitions when the locale is interpreted through a morphism other than
the identity. This behavior is described in the following threads:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-September/msg00040.html
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-January/msg00029.html
The workaround that is proposed in these threads is to introduce additional
abbreviations after having interpreted the locale. In my formalization,
this would result in so much boilerplate as to make the whole appproach
using locales unusable. Now I'm wondering why this behavior was introduced
in the first place. Since there is no problem with expanding these
abbreviations, why would there be one with contracting them?
It seems like the reason for the abbreviations not being contracted is that
they use the "internal" print mode. Unfortunately, I was unable to find the
place where the print mode is set on these abbreviations in order to do
more experiments on this. So, before spending more time on this, I wanted
to ask what the original reasons for this behavor were and if it might be
possible to enable contraction of these abbreviations.
Email Gateway (Aug 22 2022 at 10:41):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Julian,
I also regularly suffer from these pretty-printing nightmares, but I vaguely remember a
discussion with Clemens Ballarin on the subject. IIRC the problem is that it is not clear
whether collapsing the abbreviations terminates in all cases. Clemens has never showed me
an example where it actually happens, though.
Yet, I can still think of difficult situations as as the following:
locale foo =
fixes f :: "'a => 'a => bool"
and g :: "'a => 'a => 'a => bool"
definition (in foo) test where "test = f"
sublocale foo ⊆ f: foo "%x y. f y x" "%x y z. g y z x" .
This sublocale declaration makes the locale subgraph cyclic, However, the round-up
algorithm realises that if you go six times through the circle, the composed parameter
instantiations are alpha-beta-eta-equivalent to f and g again, so it stops. That means
that the sublocale command adds five copies of foo to itself. Now consider the situation
for the abbreviations. We have
local.test == foo.test f
from the original definition. From the sublocale command, we would also get
local.f.test == foo.test (%x y. f y x)
local.f.f.test == foo.test f
local.f.f.f.test == foo.test (%x y. f y x)
local.f.f.f.f.test == foo.test f
local.f.f.f.f.f.test == foo.test (%x y. f y x)
Obviously, they overlap. So which one should be used by the pretty-printer?
Andreas
Email Gateway (Aug 22 2022 at 10:42):From: Julian Brunner <julianbrunner@gmail.com>
Hi Andreas,
Good call on the overlapping abbreviations, I did not consider this case.
However, the conflict already arises with the current implementation.
Consider the following:
locale foo =
fixes f :: "'a => 'a => bool"
fixes g :: "'a => 'a => 'a => bool"
begin
definition test where "test = f"
sublocale f!: foo f "% x y z. g y z x" by this
end
This generates the following abbreviations (they end up in the Consts
record in this order):
f.test == foo.test f
f.f.test == foo.test f
test == foo.test f
Since 'test' only depends on the parameter f, which is interpreted under
the identity morphism (eta contraction seems to matter here, so this does
not happen with your original example), all of these abbreviations are set
up to be contracted before printing. In fact, 'test' is printed as 'f.test'
(presumably due to the order of the abbreviations in the Consts record).
Given that these contraction conflicts are already a problem as it is, I do
not think that it would make things significantly worse to allow
contraction of abbreviations introduced via other morphisms (barring other
problems like the one you discussed with Clemens Ballarin).
Email Gateway (Aug 22 2022 at 10:42):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Julian,
First of all, I would be very happy if you could solve this problem of missing
contractions. Clemens has never showed me an example where folding of abbreviations would
lead to non-termination. And I do not know precisely how abbreviations and locales are
implemented, so it is hard for me to decide whether something would lead to a problem.
Nevertheless, here is another example:
locale l = fixes f :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a"
definition (in l) foo where "foo ≡ f (%x. x)"
interpretation l "id" where "l.foo id == id (%x. x)" sorry
If the interpretation installs abbreviations which respect the rewrite morphism, then the
abbreviation reads as "id (%x. x) == id (%x. x)" which clearly loops. If it does not, then
"id (%x. x)" is always printed as "foo". This might not be optimal, as the right-hand
sides can be arbitrary general terms that should remain the way they are.
Andreas
Last updated: Nov 21 2024 at 12:39 UTC