Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] The set difference operator symbol

view this post on Zulip Email Gateway (Feb 09 2024 at 15:41):

From: Lawrence Paulson <lp15@cam.ac.uk>
The set difference operator in Isabelle/HOL is written with a minus sign. This is for historical reasons and especially because the more usual backslash was reserved as an escape character. However, we now have a much larger character palette including a dedicated \<setminus> symbol, which resembles but is distinct from the backslash character on your keyboard. This raises the question of whether to consider changing the symbol used for such a difference. It might look more natural. But implementing the change would be a lot of work. I don't see an alternative to manually inserting each and every occurrence.

Note that one can provide this symbol as an alternative by entering a single declaration:

abbreviation set_difference :: "['a set,'a set] ⇒ 'a set" (infixl "∖" 65)
where "A ∖ B ≡ A-B"

With this, the new symbol is accepted for input and displayed for output, but the minus sign is also accepted as before. The only argument for eliminating the use of the minus sign is to allow its use for some other purpose between sets (e.g. to denote the differences between the elements of two sets).

Thoughts?

Larry

view this post on Zulip Email Gateway (Feb 09 2024 at 16:06):

From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
I think like this, it can lead to a lot of confusion. The setminus looks
like a backslash. So users will see what they think is a backslash in
the output, but Isabelle will not accept a backslash as an input. I
would expect regular questions on this mailing list asking about this.
Maybe there is a way to avoid this, but I am not sure how exactly.

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Feb 09 2024 at 17:01):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Formally, this is the right way to do it – the »_ - _« is a type class
parameter used in a lot of different contexts.

Note that a lot of familiar syntax for sets (subset, superset, empty
set, universe, …) is just abbreviation syntax for generic operations.

Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

view this post on Zulip Email Gateway (Feb 12 2024 at 06:32):

From: Tobias Nipkow <nipkow@in.tum.de>
I am not too keen either on more duplicate syntax on a global level.

Tobias

smime.p7s

view this post on Zulip Email Gateway (Feb 12 2024 at 07:03):

From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
I’ve never really seen a problem with using “-“ for set difference. Is this something people find confusing?

Cheers,
Gerwin

view this post on Zulip Email Gateway (Feb 12 2024 at 08:48):

From: Tjark Weber <tjark.weber@it.uu.se>
On Mon, 2024-02-12 at 07:03 +0000, Gerwin Klein wrote:

I’ve never really seen a problem with using “-“ for set difference.
Is this something people find confusing?

It's not the biggest hurdle, but it's one more thing that people
currently need to learn when they start using Isabelle. It is clearly
desirable in general to keep formal notation aligned with standard
mathematical notation.

Best,
Tjark

Cheers,
Gerwin

On 12 Feb 2024, at 5:31 pm, Tobias Nipkow <nipkow@in.tum.de> wrote:

I am not too keen either on more duplicate syntax on a global
level.

Tobias

On 09/02/2024 17:01, Dominique Unruh (via cl-isabelle-users Mailing

List) wrote:

I think like this, it can lead to a lot of confusion. The
setminus looks like a backslash. So users will see what they
think is a backslash in the output, but Isabelle will not accept
a backslash as an input. I would expect regular questions on this
mailing list asking about this. Maybe there is a way to avoid
this, but I am not sure how exactly.
Best wishes,
Dominique.

On 2/9/24 16:41, Lawrence Paulson wrote:

The set difference operator in Isabelle/HOL is written with a
minus sign. This is for historical reasons and especially
because the more usual backslash was reserved as an escape
character. However, we now have a much larger character palette
including a dedicated \<setminus> symbol, which resembles but
is distinct from the backslash character on your keyboard. This
raises the question of whether to consider changing the symbol
used for such a difference. It might look more natural. But
implementing the change would be a lot of work. I don't see
an alternative to manually inserting each and every occurrence.

Note that one can provide this symbol as an alternative by
entering a single declaration:

abbreviation set_difference :: "['a set,'a set] ⇒ 'a set"
(infixl "∖" 65)
where "A ∖ B ≡ A-B"

With this, the new symbol is accepted for input and displayed
for output, but the minus sign is also accepted as before. The
only argument for eliminating the use of the minus sign is to
allow its use for some other purpose between sets (e.g. to
denote the differences between the elements of two sets).

Thoughts?

Larry

VARNING: Klicka inte på länkar och öppna inte bilagor om du inte
känner igen avsändaren och vet att innehållet är säkert.
CAUTION: Do not click on links or open attachments unless you
recognise the sender and know the content is safe.

När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

view this post on Zulip Email Gateway (Feb 12 2024 at 09:13):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
But standard mathematical notation allows both A \ B and A - B. Here, for example, the first site that popped up in Google when searching for "set difference":

https://www.splashlearn.com/math-vocabulary/difference-of-sets

Jasmin

smime.p7s

view this post on Zulip Email Gateway (Feb 12 2024 at 10:23):

From: Tjark Weber <tjark.weber@it.uu.se>
On Mon, 2024-02-12 at 10:12 +0100, Jasmin Blanchette wrote:

But standard mathematical notation allows both A \ B and A - B. Here, for
example, the first site that popped up in Google when searching for "set
difference":

<https://www.splashlearn.com/math-vocabulary/difference-of-sets>

For me, the top two Google results are
<https://en.wikipedia.org/wiki/Complement_(set_theory)> and
<https://mathworld.wolfram.com/SetDifference.html> . Both sites are clearly
biased towards A \ B but mention A - B as alternative notation that is
"sometimes" used.

Other data points:

\- LaTeX: \setminus looks backslash-like.

\- Unicode: U+2216 (Set Minus) looks backslash-like.

\- ISO 80000-2:2019 prescribes "A ∖ B" and remarks that "The notation A − B
should not be used."

Best,

Tjark

Page Title

När du har kontakt med oss på Uppsala universitet med e-post så innebär det
att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan
du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data.
For more information on how this is performed, please read here:
http://www.uu.se/en/about-uu/data-protection-policy

Last updated: Apr 29 2024 at 04:18 UTC