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



Hi,

the syntax/nosyntax bundle idea is a nice hack, and possibly the best we can do right now. (I didn't know that one can do no_notation in a bundle! :) )

On the long run, I think the following would be good:

 * Extensible bundles (so that we can add notation throughout the
   theory as it comes up).
 * Ability to use the bundle syntax everywhere.

   Currently, we can use it in lemma-statements and proofs using
   includes/include, we cannot use bundled notation in the definition
   of a locale/class, or in the output of the thm diagnostic command.
   (We can use unbundle  before the local/thm, of course, but that has
   a global effect.)

   The syntax/nosyntax hack solves this, though.
 * Some way to also bundle advanced notation. I think there is
   currently no easy way to bundle syntax that involves parse/print
   translations.

   (The only current way I see is to create an attribute that sets a
   flag, in the code of the parse/print translation to check whether
   that flag is set, and then activate/deactivate the flag using the
   attribute in a bundle.)

Best wishes,
Dominique.




On 5/17/19 11:55 AM, Alexander Krauss wrote:
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.