Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Annoying syntax issue wrt parentheses

view this post on Zulip Email Gateway (May 24 2022 at 18:54):

From: Angeliki Koutsoukou Argyraki <ak2110@cam.ac.uk>
Dear all,

this is a very minor thing indeed (and similar instances of this have caught my attention many times before)
but I think it may be worth looking into:

Sometimes, and in particular very often when summations are involved,
the user is expected to put parentheses where their lack wouldn't cause any ambiguity.

Here is a striking example.

This gives an error:
" a ≤ ∑x ∈X. f x " ("inner syntax error/failed to parse prop")

while this is fine:

" a ≤ ( ∑x ∈X. f x ) "

One wouldn't/ shouldn't expect the first version to be problematic as the lack of parentheses
would not be causing any ambiguity.

Any thoughts?

Thanks,
Angeliki

view this post on Zulip Email Gateway (May 25 2022 at 00:22):

From: Alex Weisberger <alex.m.weisberger@gmail.com>
I remember being surprised that if and case expressions require parentheses
like this as well, and reading that it has to do operator / syntax
precedence:
https://stackoverflow.com/a/60466980.

Surrounding ambiguous expressions with parens seems reasonable. It might be
unambiguous to the eye, but source code has to be parsed by a machine.

view this post on Zulip Email Gateway (May 25 2022 at 00:48):

From: Michael Norrish <cl-isabelle-users@lists.cam.ac.uk>
Though possible in principle, it’s very hard to write the context-free grammar that would allow this.

It is something that otherwise annoyingly weak precedence parsers can give you.

Michael
signature.asc

view this post on Zulip Email Gateway (May 25 2022 at 05:41):

From: Tobias Nipkow <nipkow@in.tum.de>
As two other readers already pointed out, this is a grammar/parser issue. I made
this choice intentionally, but what my intentions where I cannot remember. The
choice is unform (eg f x = (if ...), P --> (ALL x. ...) etc) and I was certainly
aware of the need for parentheses. In principle, an Earley parser can handle
this w/o parentheses, and Isabelle uses Earley, but it may just be that the
required grammar is the issue (as Michael mentioned).

Tobias
smime.p7s

view this post on Zulip Email Gateway (May 25 2022 at 06:29):

From: Stepan Holub <holub@karlin.mff.cuni.cz>
All those binders are very weak, with preference 10.

It would be enough to increase the preference. For example, one needs at
least 51 to beat ≤

See:

abbreviation Sum ("MYSUM")
  where "MYSUM ≡ sum (λx. x)"

syntax
  "_sum" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::comm_monoid_add"
("(2MYSUM(_/∈_)./ _)" [0, 51, 10] 51)

lemma " a ≤ MYSUM x ∈X. f x"

For implication, at least 25 is needed:

definition myAll :: "('a ⇒ bool) ⇒ bool"  (binder "MYALL" 25)
  where "myAll P ≡ (P = (λx. True))"

lemma "P ⟶ MYALL x. Q x"

Stepan

view this post on Zulip Email Gateway (May 25 2022 at 23:19):

From: Michael Norrish <cl-isabelle-users@lists.cam.ac.uk>
This approach will lead to undesired behaviour if the binder/quantifier is to the left of the infix. In particular:

Binder x. foo(x) <= z

will put the <= as the top level operator.

Michael

view this post on Zulip Email Gateway (May 26 2022 at 07:30):

From: Stepan Holub <holub@karlin.mff.cuni.cz>

This approach will lead to undesired behaviour if the
binder/quantifier is to the left of the infix.   In particular:

Binder x. foo(x) <= z

will put the <= as the top level operator.

Michael

Michael, not sure what you mean. This works fine:

definition myAll :: "('a ⇒ bool) ⇒ bool"  (binder "MYALL" 25)
   where "myAll P ≡ (P = (λx. True))"

lemma "(∀ x. x ≤ y) ⟶ MYALL x. x ≤ y"
  by (simp add: myAll_def)

But to be clear, I do not suggest any change. Just wanted to Illustrate
the behavior.
Any order of preferences will require parentheses in some cases, that is
why we have them.

For example, low preference of ∀ makes sense, compare

lemma: "∀ x. x ≤ y ⟶ x ≤ y"
  by simp

lemma: "MYALL x. (x ≤ y ⟶ x ≤ y)"
  by (simp add: myAll_def)

(In the original case of sum, higher preference maybe makes better sense.)

Best

Stepan

*From: *cl-isabelle-users-request@lists.cam.ac.uk
<cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Stepan Holub
<holub@karlin.mff.cuni.cz>
*Date: *Wednesday, 25 May 2022 at 16:30
*To: *cl-isabelle-users@lists.cam.ac.uk
<cl-isabelle-users@lists.cam.ac.uk>
*Subject: *Re: [isabelle] Annoying syntax issue wrt parentheses

All those binders are very weak, with preference 10.

It would be enough to increase the preference. For example, one needs at
least 51 to beat ≤

See:

abbreviation Sum ("MYSUM")
   where "MYSUM ≡ sum (λx. x)"

syntax
   "_sum" :: "pttrn ⇒'a set ⇒'b ⇒'b::comm_monoid_add"
("(2MYSUM(_/∈_)./ _)" [0, 51, 10] 51)

lemma " a ≤ MYSUM x ∈X. f x"

For implication, at least 25 is needed:

definition myAll :: "('a ⇒bool) ⇒bool"  (binder "MYALL" 25)
   where "myAll P ≡ (P = (λx. True))"

lemma "P ⟶MYALL x. Q x"

Stepan

On 25-May-22 7:40 AM, Tobias Nipkow wrote:

As two other readers already pointed out, this is a grammar/parser
issue. I made this choice intentionally, but what my intentions where
I cannot remember. The choice is unform (eg f x = (if ...), P --> (ALL
x. ...) etc) and I was certainly aware of the need for parentheses. In
principle, an Earley parser can handle this w/o parentheses, and
Isabelle uses Earley, but it may just be that the required grammar is
the issue (as Michael mentioned).

Tobias

On 24/05/2022 20:53, Angeliki Koutsoukou Argyraki wrote:

Dear all,

this is a very minor thing indeed (and similar instances of this have
caught my attention many times before)
but I think it may be worth looking into:

Sometimes, and in particular very often when summations are involved,
the user is expected to put parentheses where their lack wouldn't
cause any ambiguity.

Here is a striking example.

This gives an error:
  " a ≤ ∑x ∈X. f x  " ("inner syntax error/failed to parse prop")

while this is fine:

" a ≤  ( ∑x ∈X. f x )  "

One wouldn't/ shouldn't expect the first version to be problematic as
the lack of parentheses
would not be causing any ambiguity.

Any thoughts?

Thanks,
Angeliki

--
Tento e-mail byl zkontrolován na viry programem AVG.
https://aus01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.avg.cz%2F&data=05%7C01%7Cmichael.norrish%40anu.edu.au%7Cc24731260c694275eccf08da3e17f50d%7Ce37d725cab5c46249ae5f0533e486437%7C0%7C0%7C637890570010616781%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=sdb5INUlWrxARAdrh%2F%2BQkTBcYZSnDv3VbSNczoS6QSg%3D&reserved=0
<https://aus01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.avg.cz%2F&data=05%7C01%7Cmichael.norrish%40anu.edu.au%7Cc24731260c694275eccf08da3e17f50d%7Ce37d725cab5c46249ae5f0533e486437%7C0%7C0%7C637890570010616781%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=sdb5INUlWrxARAdrh%2F%2BQkTBcYZSnDv3VbSNczoS6QSg%3D&reserved=0>

view this post on Zulip Email Gateway (May 27 2022 at 00:04):

From: Michael Norrish <cl-isabelle-users@lists.cam.ac.uk>
The latter is exactly what I meant by “undesired": you had to parenthesise the body of the term under MYALL.

Michael
signature.asc

Last updated: Apr 18 2024 at 08:19 UTC