Re: [isabelle] Best practices for introducing domain specific notation



Hi Dominique, hi all,

This thread hasn't got much attention so far, but I think it touches an
issue that is worth discussing. I also want to learn more about this.

Am 06.05.2019 um 14:50 schrieb Dominique Unruh:
> one thing that has always been bugging me is the pollution of Isabelle
> syntax with domain specific notation.
> 
> For example, if I develop a theory involving inner products, I may want
> to introduce the notation "a · b" to make my theorems readable.
> 
> But that means that everyone who uses my theory will suddenly have my
> notation "·" in their namespace. Possibly conflicting with syntax from
> other theories.
> 
> Of course, there are mechanisms for local syntax. For example, locals
> and bundles. But I am not sure what the best practices are for using them.
> 
>  * With locales, I have the following problems: I cannot separate the
>    notation from the logical context. For example, sometimes my
>    definition will not be in any natural way part of a locale. For
>    example, if I introduce a datatype and an operation on it (say,
>    lists, and · for concatenation) then I would not know where to put
>    the notation. Also, as far as I understand, with locales, there is
>    no way to use the notation (like "including" with bundles) locally
>    without actually using the whole logical context of the locale (in
>    particular, if I want to use some notation from a locale in the
>    statement of a lemma by using "(in name)", that lemma will then
>    automatically be in the name space of the locale).

I think locales were built mostly with the logical applications in mind.
I would consider their use for just syntax/extra-logical matters an
abuse, although that has been common...


>  * Bundles seem to have more flexibility. I can put a number of syntax
>    elements together and include them as needed. Unfortunately, it
>    seems that bundles are not extensible. For example, assume a theory
>    that introduces a number of concepts throughout the theory (or even
>    several theories). E.g., inner product, norm, closure of sets,
>    Minkowski product, etc. If I want to use bundles, I have the
>    following choices:
>      o I introduce all the definitions at the beginning of the theory
>        (and thus break the logical structure of the presentation) and
>        make a bundle with syntax at the beginning.
>      o I introduce all the definitions where they fit logically, and
>        introduce syntax only at the very end (as one bundle). Then I
>        cannot use the notation within the theories.
>      o I introduce a new bundle each time I introduce new syntax (and
>        end up with a lot of bundles that I can later combine into one
>        bundle). That avoids the above problems, but it means that I
>        pollute the name space with a lot of temporary bundle names.
> 
> What is the best approach here?

I looked around a bit to see what others do with bundles today. Here are
some things I found:

* Sometimes there are "negative" syntax bundles in the style of

    bundle no_foo_syntax
    begin
      no_notation foo    ("**")
    end

* In particular, I saw this pattern in the end of HOL/Library/Perm.thy,
which I found interesting.

    subsection ‹Syntax›

    bundle no_permutation_syntax
    begin
      no_notation swap    ("⟨_↔_⟩")
      no_notation cycle   ("⟨_⟩")
      no_notation "apply" (infixl "⟨$⟩" 999)
    end

    bundle permutation_syntax
    begin
      notation swap       ("⟨_↔_⟩")
      notation cycle      ("⟨_⟩")
      notation "apply"    (infixl "⟨$⟩" 999)
      no_notation "apply" ("(⟨$⟩)")
    end

    unbundle no_permutation_syntax

This effectively gives users an "on/off" switch, although it is not
particularly pretty when the respective (no_)notation declarations are
stacked onto each other. A similar thing is done in the end of
HOL/Decision_Procs/Approximation.thy and in several places in the AFP.

* HOL/Main.thy also removes quite a bit of common syntax at the end, and
declares a bundle cardinal_syntax which contains some of the previously
removed notation.

> I feel that a clear guideline for such situations might be useful not
> just for me, but could also make the AFP more reuse-friendly.

Given the observations above, I think in current Isabelle the best
practice for library developers would be:

* Provide a canonical entry point for users of your library.
* At the end of that entry point, remove any syntax that is specific to
your library.
* Declare a foo_syntax bundle that users can use to activate the syntax,
and possibly also a no_foo_syntax bundle.

> (Currently, I get all the notation introduced by an author when I import
> an AFP theory, even if I only want to use one theorem of theirs for a
> technical lemma.) I'd even go so far to say that I think on the long run
> it would be a good idea to require the absence of syntax pollution as
> part of the requirements for AFP submissions.

I think not everything was designed for being reused, and this is
probably ok, since AFP contains both libraries and applications. But
when something is used as a library, it should avoid syntax pollution.


Another interesting question is: What concepts should future-Isabelle
provide to make this more natural? I find the above pattern quite
verbose and somewhat unintuitive. Would extensible bundles help?


Best
Alex




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.