Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Operator clash for $


view this post on Zulip Email Gateway (Aug 22 2022 at 13:37):

From: Manuel Eberl <eberlm@in.tum.de>
Hallo,

it appears that the infix operator $ is used both for the n-th component
of a vector and the n-th coefficient of a Formal Power Series.

Since I now use both Multivariate_Analysis and Formal_Power_Series, I
get lots of syntax ambiguity warnings all the time. We should probably
do something about this.

I see the following three options:

  1. Rename one of the operators. Since Formal_Power_Series is used less
    than vectors, this is probably the one to change in this case. I am not
    sure, however, what it could be renamed to. The standard mathematical
    notation is something like "[X^n] f", so I suppose we could go for
    "⟨X^n⟩ f", but I'm not sure if that's a good idea.

  2. Disable the "$" notation completely outside the FPS theory, or put it
    in a locale that has to be interpreted every time one wants to use the
    notation. On the down side, one still runs into problems when one wants
    to use the $ notation for FPSs but has Multivariate_Analysis loaded as
    well. I guess one could put both of them in locales, but I don't know if
    we want that.

  3. Use ad-hoc Overloading, similar to what is done for monads. One could
    then also use $ e.g. for the n-th coefficient of a polynomial, or
    perhaps even unify the notation with the n-th element of lists and
    arrays etc. at some point. The down side of this is that when there are
    ambiguities/type errors, the error messages get a bit confusing.

Note that "normal" overloading does not work, since the constant would
have to have the type "'a => nat => 'b", and that means one has to write
type annotations everywhere.

Any opinions? Whatever the outcome is, I will take care of implementing it.

Cheers,

Manuel

view this post on Zulip Email Gateway (Aug 22 2022 at 13:37):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Note that starting from a59801b7f125 bundles have become a convenient
mechanism to organize modularized syntax. The »$« notation would be a
nice candidate to demonstrate that.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 13:37):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,

The $ notation is used also in other places of the HOL Library, e.g., in
Library/FinFun_Syntax and HOLCF/Cfun. I'd recommend that the operations by default use
subscripts for disambiguation, e.g. (we can discuss about the concrete subscripts),

op $\<^sub>v for vectors
op $\<^sup>p for formal power series
op $\<^sup>f for FinFun

In HOLCF/Cfun, Rep_cfun uses \<cdot> in jEdit, so one could in theory drop the ASCII
notation there.

Then, if a user wants to use several of the theories at the same time, she can always use
unambiguous syntax. However, typing subscripts can be annoying, so there should be support
for users that use only one of the theories. Makarius recently [1] renovated bundles to
support that. Then, users can install their op $ syntax for what they want in one line.

I am against adhoc_overloading, because the type error messages just get incomprehensible
and adhoc_overloading is not complete (in some cases, it fails to find a resolution of
overloading, but when I add type annotations, then it succeeds).

[1] https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-June/006891.html

Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 13:37):

From: Tobias Nipkow <nipkow@in.tum.de>
I would like to see the following setup:

It would be suboptimal if we would need to sprinkle additional lines all over
MVA to cater for potential conflicts.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 13:40):

From: Makarius <makarius@sketis.net>
On 16/06/16 12:08, Andreas Lochbihler wrote:

Hi Manuel,

The $ notation is used also in other places of the HOL Library, e.g., in
Library/FinFun_Syntax and HOLCF/Cfun. I'd recommend that the operations
by default use subscripts for disambiguation, e.g. (we can discuss about
the concrete subscripts),

op $\<^sub>v for vectors
op $\<^sup>p for formal power series
op $\<^sup>f for FinFun

(This thread still seems to be unresolved.)

How about this?

$ for vectors
$\<^sup>p for formal power series
$\<^sup>f for FinFun

Then, if a user wants to use several of the theories at the same time,
she can always use unambiguous syntax. However, typing subscripts can
be annoying

How about this in etc/abbrevs?

"$" = "$\<^sub>f"
"$" = "$\<^sub>p"

Makarius


Last updated: Mar 29 2024 at 12:28 UTC