Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Best practices for introducing domain specific...

Email Gateway (Aug 22 2022 at 19:47):

From: Dominique Unruh <unruh@ut.ee>
Hi,

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).

* 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 feel that a clear guideline for such situations might be useful not
just for me, but could also make the AFP more reuse-friendly.
(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.

Best wishes,
Dominique.

Email Gateway (Aug 22 2022 at 19:52):

From: Alexander Krauss <krauss@in.tum.de>
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

Email Gateway (Aug 22 2022 at 19:52):

From: Lawrence Paulson <lp15@cam.ac.uk>
Count me in as interested in a better (simpler to set up and use) way of managing syntax. For example, there are some infix operators declared in Algebra that in most cases don’t need to be visible outside.

Larry

Email Gateway (Aug 22 2022 at 19:52):

From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Hi,

I am very interested in the topic.
Our AFP entry (see https://www.isa-afp.org/entries/UTP.html) suffers from
such a problem.
Actually UTP has a very strong syntactic flavor which I would like to
activate and de-activate whenever I want.

I am thinking of an approach that uses a top-level command that allow me to
activate the UTP syntax inside the cartouch and de-activate it whenever I
am out of the scope of the command.
One problem is: it might that my top-level command need the syntax of HOL
as well as the document model "HOL" since I would like to define new
concepts or prove new lemmas with the activated syntax.
But technically I am not sure how practical is this, since I did not yet
start doing it.

I agree that it is not a trivial problem we have here.

Best wishes,

Yakoub.

Email Gateway (Aug 22 2022 at 19:52):

From: Dominique Unruh <unruh@ut.ee>
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.

Email Gateway (Aug 22 2022 at 19:52):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Alex,

• 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.

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.

thanks for digging into that.

This indeed resembles the state of the art (which is not applied
everywhere, though), with the following disadvantages:

• The switches have to be maintained by hand; at least they are in local
  proximity, which is far superior than requiring ad-hoc no_notation
  declarations which are fragile since priorities must match exactly etc.
  Extensible bundles would be helpful here.

• There is no way to store global syntax declarations in bundles, see e.
  g. Library/Lattice_Syntax.thy. This is the reason why e. g. lattice
  syntax has not been organized using bundles yet.

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...

Indeed. The »subscriptive« nature of locales also provides no means for
switching on and off things, the conceptual main distinction between
locales and bundles.

Cheers,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC