How do I add operator precedence to a lark grammar for FOL with Equality?

Question

How do I modify this grammar so it matches parenthesis that are further away?

?wff: compound_wff
?compound_wff: biconditional_wff
?biconditional_wff: conditional_wff (SPACE? BICONDITIONAL_SYMBOL SPACE? biconditional_wff)*
?conditional_wff: disjunctive_wff (SPACE? CONDITIONAL_SYMBOL SPACE? conditional_wff)*
?disjunctive_wff: conjunctive_wff (SPACE? DISJUNCTION_SYMBOL SPACE? disjunctive_wff)*
?conjunctive_wff: negated_wff (SPACE? CONJUNCTION_SYMBOL SPACE? conjunctive_wff)*
?negated_wff: (NEGATION_SYMBOL SPACE)* atomic_wff
?atomic_wff: predicate
           | term EQUAL_TO term
           | quantified_wff* LEFT_PARENTHESIS SPACE? wff SPACE? RIGHT_PARENTHESIS
?term: function
    | NAME
    | VARIABLE
?predicate: PREDICATE_NAME [LEFT_PARENTHESIS term (COMMA term)* RIGHT_PARENTHESIS]
?function: FUNCTION_NAME LEFT_PARENTHESIS term (COMMA SPACE? term)* RIGHT_PARENTHESIS
?quantified_wff: curly_quantifiers | quantifiers
?curly_quantifiers: quantifier_symbol LEFT_CURLY_BRACE VARIABLE (COMMA SPACE? VARIABLE)* RIGHT_CURLY_BRACE SPACE?
?quantifiers: quantifier_symbol SPACE? VARIABLE (COMMA SPACE? VARIABLE)* SPACE?

SPACE: /\s+/
COMMA: ","
EQUAL_TO: "="
LEFT_PARENTHESIS: "("
RIGHT_PARENTHESIS: ")"
LEFT_CURLY_BRACE: "{"
RIGHT_CURLY_BRACE: "}"
quantifier_symbol: UNIVERSAL_QUANTIFIER_SYMBOL | EXISTENTIAL_QUANTIFIER_SYMBOL
UNIVERSAL_QUANTIFIER_SYMBOL: "\\forall" | "∀"
EXISTENTIAL_QUANTIFIER_SYMBOL: "\\exists" | "∃"
NAME: /[a-t]/ | /[a-t]_[1-9]\d*/
VARIABLE: /[u-z]/ | /[u-z]_[1-9]\d*/
PREDICATE_NAME: /[A-HJ-Z]/ | /[A-HJ-Z]_[1-9]\d*/
FUNCTION_NAME: /[a-z]/ | /[a-z]_[1-9]\d*/
NEGATION_SYMBOL: "\\neg" | "\\lnot" | "¬"
CONJUNCTION_SYMBOL: "\\wedge" | "\\land" | "∧"
DISJUNCTION_SYMBOL: "\\vee" | "\\lor" | "∨"
CONDITIONAL_SYMBOL: "\\rightarrow" | "\\Rightarrow" | "\\Longrightarrow" | "\\implies" | "→" | "⇒"
BICONDITIONAL_SYMBOL: "\\leftrightarrow" | "\\iff" | "↔" | "⇔"

I'm trying to parse this using my grammar:

Which in LaTeX is:

\exists{x} \forall{y} (P(f(x, y)) \vee \forall{z}(V(z) \iff \neg R(a) \wedge B(a)))

I followed the calculator example and modified my original grammar to add operator precedence which resulted in this. But it's no longer accepting the input string.

I'm getting this error:

lark.exceptions.UnexpectedCharacters: No terminal matches '\' in the current parser context, at line 1 col 35

\exists{x} \forall{y} (P(f(x, y)) \vee \forall{z}(V(z) \iff \neg R(a) \wed
                                  ^
Expected one of: 
    * RIGHT_PARENTHESIS

Ideally I want to force requiring parenthesis wherever possible except in the case of in front of a negated atomic_wff without parenthesis. This is to make sure only one parse tree is produced even on explicit ambiguity setting. How do I resolve this issue?

Edit 1

I want to clarify that operator precedence for the same operators should be right associative. So P(a) ∧ Q(a) ∧ R(a) will resolve as P(a) ∧ (Q(a) ∧ R(a))

Edit 2

I have made the lark grammar easier to debug using proper terminals. It now parses the long latex equation, but is still ambiguous for simpler inputs like P(a) ∧ Q(a) ∧ R(a) which produces two parse trees. I still don't know what I am doing wrong. The grammar is doing right recursion and still failing to produce a single parse tree.

Edit 3

My latest attempted solution works in every case except for giving negation a higher precedence. Any idea?

?wff: compound_wff
compound_wff: biconditional_wff
biconditional_wff: conditional_wff (SPACE? BICONDITIONAL_SYMBOL SPACE? conditional_wff)*
conditional_wff: disjunctive_wff (SPACE? CONDITIONAL_SYMBOL SPACE? disjunctive_wff)*
disjunctive_wff: conjunctive_wff (SPACE? DISJUNCTION_SYMBOL SPACE? conjunctive_wff)*
conjunctive_wff: negated_wff (SPACE? CONJUNCTION_SYMBOL SPACE? negated_wff)*
negated_wff: (NEGATION_SYMBOL SPACE?)* atomic_wff
atomic_wff: predicate
          | term EQUAL_TO term
          | quantified_wff* LEFT_PARENTHESIS SPACE? wff SPACE? RIGHT_PARENTHESIS
term: function
    | NAME
    | VARIABLE
predicate: PREDICATE_NAME [LEFT_PARENTHESIS term (COMMA term)* RIGHT_PARENTHESIS]
function: FUNCTION_NAME LEFT_PARENTHESIS term (COMMA term)* RIGHT_PARENTHESIS
quantified_wff: curly_quantifiers | quantifiers
curly_quantifiers: quantifier_symbol LEFT_CURLY_BRACE VARIABLE (COMMA SPACE? VARIABLE)* RIGHT_CURLY_BRACE SPACE?
quantifiers: quantifier_symbol SPACE? VARIABLE (COMMA SPACE? VARIABLE)* SPACE?

SPACE: /\s+/
COMMA: /,\s*/
EQUAL_TO: /\s*=\s*/
LEFT_PARENTHESIS: "("
RIGHT_PARENTHESIS: ")"
LEFT_CURLY_BRACE: "{"
RIGHT_CURLY_BRACE: "}"
quantifier_symbol: UNIVERSAL_QUANTIFIER_SYMBOL | EXISTENTIAL_QUANTIFIER_SYMBOL
UNIVERSAL_QUANTIFIER_SYMBOL: "\\forall" | "∀"
EXISTENTIAL_QUANTIFIER_SYMBOL: "\\exists" | "∃"
NAME: /[a-t]/ | /[a-t]_[1-9]\d*/
VARIABLE: /[u-z]/ | /[u-z]_[1-9]\d*/
PREDICATE_NAME: /[A-HJ-Z]/ | /[A-HJ-Z]_[1-9]\d*/
FUNCTION_NAME: /[a-z]/ | /[a-z]_[1-9]\d*/
NEGATION_SYMBOL: "\\neg" | "\\lnot" | "¬"
CONJUNCTION_SYMBOL: "\\wedge" | "\\land" | "∧"
DISJUNCTION_SYMBOL: "\\vee" | "\\lor" | "∨"
CONDITIONAL_SYMBOL: "\\rightarrow" | "\\Rightarrow" | "\\Longrightarrow" | "\\implies" | "→" | "⇒"
BICONDITIONAL_SYMBOL: "\\leftrightarrow" | "\\iff" | "↔" | "⇔"

%ignore SPACE
%ignore COMMA
%ignore LEFT_CURLY_BRACE
%ignore RIGHT_CURLY_BRACE

So it fails to to produce a single parse tree for ¬P(a) ∧ Q(b).

You are indeed missing a right parenthesis in your expression `(P(f(x, y))` — gimix, Nov 20 '22 at 13:15
No I'm not. The first bracket before P should match the last bracket in the entire formula. — Vivek Joshy, Nov 20 '22 at 22:48
You say " I want to force requiring parenthesis wherever possible except in the case of in front of a negated atomic_wff without parenthesis". But your example wff includes `... ⟺¬R(a)∧B(a)`, where the right-hand operator to `⟺` is the conjunction `¬R(a)∧B(a)`, written without parentheses. So which is it? Parentheses are optional and ambiguity is resolved because `⟺` has lower precedence than `∧`? Or parentheses are required and the example wff is incorrect? — rici, Nov 21 '22 at 17:16
I ask because I have a grammar which requires parentheses, as per request, but it rejects your example precisely because the required parentheses are missing. I'll post it once you clarify. — rici, Nov 21 '22 at 17:17
Sorry I just realized that I want right associativity to resolve ambiguity and also allow parenthesis. The parser that I tested allows for the sentence above also appears to to be right associative for all the connectives. — Vivek Joshy, Nov 21 '22 at 19:37
@daegontaven: Sorry, I didn't see that comment earlier. Sometimes @'s are essential. With all due respect, I don't think that "right associative for all connectives" is a good idea. That would parse `P∨Q⟺P∧R` as `P∨(Q⟺(P∧R))`, which is almost certainly not the intended interpretation. If you mean that connectives are right associative with themselves, that's fine (and normal, I think), but it won't accept `P∨Q⟺P∧R` without the disambiguating parentheses `(P∨Q)⟺(P∧R)`, which is why your example input doesn't parse. There's a lot to be said for common precedence rules :-) But your choice. — rici, Nov 22 '22 at 16:07
For future reference, please edit your clarifications into your question. Comments here are ephemeral. — rici, Nov 22 '22 at 16:08
@rici Yes I want right associativity but with operator precedence such that negation over conjunction over disjunction over conditional over biconditional. So `P∨Q⟺P∧R` will automatically resolve as `(P∨Q)⟺(P∧R)` since ∧ and ∨ have higher precedence than ⟺. — Vivek Joshy, Nov 22 '22 at 18:02

Vivek Joshy · Accepted Answer · 2022-12-09T11:15:07.890

The issue was each wff rule was not matching the antecedent rule in it's parts. So:

?biconditional_wff: conditional_wff (SPACE? BICONDITIONAL_SYMBOL SPACE? biconditional_wff)*

Should be changed to:

?biconditional_wff: conditional_wff (SPACE? BICONDITIONAL_SYMBOL SPACE? conditional_wff)*

The solution to this issue is to have a grammar like this:

?wff: compound_wff
compound_wff: biconditional_wff
biconditional_wff: conditional_wff (SPACE? BICONDITIONAL_SYMBOL SPACE? conditional_wff)*
conditional_wff: disjunctive_wff (SPACE? CONDITIONAL_SYMBOL SPACE? disjunctive_wff)*
disjunctive_wff: conjunctive_wff (SPACE? DISJUNCTION_SYMBOL SPACE? conjunctive_wff)*
conjunctive_wff: negated_wff (SPACE? CONJUNCTION_SYMBOL SPACE? negated_wff)*
negated_wff: (NEGATION_SYMBOL SPACE?)* atomic_wff
atomic_wff: predicate
          | term EQUAL_TO term
          | quantified_wff* LEFT_PARENTHESIS SPACE? wff SPACE? RIGHT_PARENTHESIS
term: function
    | NAME
    | VARIABLE
predicate: PREDICATE_NAME [LEFT_PARENTHESIS term (COMMA term)* RIGHT_PARENTHESIS]
function: FUNCTION_NAME LEFT_PARENTHESIS term (COMMA term)* RIGHT_PARENTHESIS
quantified_wff: curly_quantifiers | quantifiers
curly_quantifiers: quantifier_symbol LEFT_CURLY_BRACE VARIABLE (COMMA SPACE? VARIABLE)* RIGHT_CURLY_BRACE SPACE?
quantifiers: quantifier_symbol SPACE? VARIABLE (COMMA SPACE? VARIABLE)* SPACE?

SPACE: /\s+/
COMMA: /,\s*/
EQUAL_TO: /\s*=\s*/
LEFT_PARENTHESIS: "("
RIGHT_PARENTHESIS: ")"
LEFT_CURLY_BRACE: "{"
RIGHT_CURLY_BRACE: "}"
quantifier_symbol: UNIVERSAL_QUANTIFIER_SYMBOL | EXISTENTIAL_QUANTIFIER_SYMBOL
UNIVERSAL_QUANTIFIER_SYMBOL: "\\forall" | "∀"
EXISTENTIAL_QUANTIFIER_SYMBOL: "\\exists" | "∃"
NAME: /[a-t]/ | /[a-t]_[1-9]\d*/
VARIABLE: /[u-z]/ | /[u-z]_[1-9]\d*/
PREDICATE_NAME: /[A-HJ-Z]/ | /[A-HJ-Z]_[1-9]\d*/
FUNCTION_NAME: /[a-z]/ | /[a-z]_[1-9]\d*/
NEGATION_SYMBOL: "\\neg" | "\\lnot" | "¬"
CONJUNCTION_SYMBOL: "\\wedge" | "\\land" | "∧"
DISJUNCTION_SYMBOL: "\\vee" | "\\lor" | "∨"
CONDITIONAL_SYMBOL: "\\rightarrow" | "\\Rightarrow" | "\\Longrightarrow" | "\\implies" | "→" | "⇒"
BICONDITIONAL_SYMBOL: "\\leftrightarrow" | "\\iff" | "↔" | "⇔"

Also remove the %ignore directives.

%ignore SPACE
%ignore COMMA
%ignore LEFT_CURLY_BRACE
%ignore RIGHT_CURLY_BRACE

How do I add operator precedence to a lark grammar for FOL with Equality?

Edit 1

Edit 2

Edit 3

1 Answers1