Email Gateway (Aug 17 2022 at 13:28): Email Gateway (Aug 17 2022 at 13:28):From: Steven Obua <obua@in.tum.de>
I like your idea of defining precedence by partial ordering; I dislike
the system of assigning numerical values as precedences, because this
implies that you know the numerical precedences of all the other
constants that have precedences, which I don't.
I do not agree to force "x" to relate to "a" and "b" if it does not. If
ambiguity between "x" and "a" or "b" arises, then the parser
should signal a parse error. This is less confusing, too, I think,
because otherwise you have the old problem: What again was the nearest
element less than "c"?? One should just accept that precedence is a
partial ordering, not a total one.
Steven
Email Gateway (Aug 17 2022 at 13:28):From: Lucas Dixon <lucas.dixon@ed.ac.uk>
Dear Isabelle users,
I've been wondering how easy it is to implement, and how useful people
would find, a different mechanism for defining precedence: something
based on partial orderings instead of numerical values. (I believe that
the underlying representation is a search tree anyway...)
I'm thinking of something like:
consts "*" :: "N => N => N" (infixr [> "="])
consts "+" :: "N => N => N" (infixr [< "*", > "="])
consts "^" :: "N => N => N" (infixr [> "*"])
consts "++" :: "N => N => N" (infixr [= "+"])
where the [> "X"] makes the constant have greater precedence than X. [<
"X"], less than and [= "X"] equal to X. I think this would be a nicer
way to specify them... what do you think?
There is a little question as to the treatment of less well defined
situations, such as:
consts "a" :: "N => N => N" (infixr [> "="])
consts "b" :: "N => N => N" (infixr [> "a"])
consts "c" :: "N => N => N" (infixr [> "b"])
consts "x" :: "N => N => N" (infixr [< "c"])
in particular, how does "x" relate to "a" and "b"? I suggest that when
such ambiguity arises "x" would be given precedence equal to the nearest
element less than "c". Similarly for greater than: it could be
interpreted, when ambiguity arises, as 'just a little bigger than': the
same as the nearest next value.
Cycles should obviously produce errors. :)
Do any of you know of something like this in other systems? I do not
know much about parsing, so perhaps there is some reason why such
approaches are not implemented... ? (if so, I'd like to know!)
cheers,
lucas
Email Gateway (Aug 17 2022 at 13:45):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Steven Obua wrote:
an observation which I confirm.
Florian
florian.haftmann.vcf
signature.asc
Last updated: May 03 2024 at 04:19 UTC