[isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Thu Oct 29 15:37:41 CET 2015
»const_decl« is shared by different primitives and operations on various
targets. Hence the patch looks fine.
The »revert_abbrev« goes back to changeset 2b86fac03ec5 in
named_target.ML, although the guarding criterion has changed over time.
2b86fac03ec5 is already in the highly experimental layer of local
theory experiments from 2007. I doubt that digging further will reveal
any insight. Hence, we just assume that the reverted abbreviations will
not exhibit any problems here. I have spend no though on the issue
I have not spend any thoughts whether there could be terminaton issues.
Is there any argument beyond the absence of counterexamples that that
can never happen?
Cheers,
Florian
Am 29.10.2015 um 11:48 schrieb Florian Haftmann:
> Hi Clemens,
>
> thanks for undertaking this.
>
> I will have a look at this and give feedback.
>
> Cheers,
> Florian
>
> Am 27.10.2015 um 18:59 schrieb Clemens Ballarin:
>> Related to the below discussion on isabelle-users, I have now refined the patch I had circulated then. Here is the NEWS entry:
>>
>> * More gentle suppression of syntax along locale morphisms while
>> printing terms. Previously 'abbreviation' and 'notation' declarations
>>
>> would be suppressed for morphisms (except term identity). Now merely
>> 'notation' is suppressed. This can be of great help when working with
>>
>> complex locale hierarchies, because proof states are displayed much
>> more succinctly. It also means that only notation needs to be
>> redeclared if desired, as illustrated by this example:
>>
>> locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65)
>> begin
>> definition derived (infixl "\<odot>" 65) where ...
>> end
>>
>> locale morphism =
>> left!: struct composition + right!: struct composition'
>> for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" 65)
>> begin
>> notation right.derived ("\<odot>''")
>> end
>>
>> The full patch is attached. Interestingly, it is fully compatible also with the AFP. Since I'm not particularly familiar with generic_target.ML I'm posting it here for feedback. My intention is to push this in the near future.
>>
>> Clemens
>>
>>
>> On 28 July, 2015 12:12 CEST, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
>>
>>> 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
>>>
>>> On 28/07/15 11:33, Julian Brunner wrote:
>>>> 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).
>>>>
>>>> On Tue, Jul 28, 2015 at 8:53 AM Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch
>>>> <mailto:andreas.lochbihler at inf.ethz.ch>> wrote:
>>>>
>>>> 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
>>>>
>>>>
>>>> On 27/07/15 21:12, Julian Brunner wrote:
>>>> > 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.
>>>> >
>>>>
>>>
>>
>>
>>
>>
>>
>>
>>
>> _______________________________________________
>> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151029/44c6fed8/attachment.sig>
More information about the isabelle-dev
mailing list