如何为带等词的FOL Lark语法添加算子优先级并解决歧义？

最终语法代码 #

# 严格无歧义的带等词一阶逻辑Lark语法
start: wff

# 按算子优先级分层，仅允许同层级或括号包裹的跨层级组合
wff: iff_wff
iff_wff: primary_wff "↔" primary_wff | primary_wff
implies_wff: primary_wff "→" primary_wff | primary_wff
disj_wff: primary_wff "∨" primary_wff | primary_wff
conj_wff: primary_wff "∧" primary_wff | primary_wff
equality_wff: primary_wff "=" primary_wff | primary_wff

# 核心基础WFF单元：仅允许三种合法无括号形式
primary_wff: neg_atom_wff | atom_wff | "(" wff ")"

# 唯一允许的无括号否定形式：否定直接作用于原子公式
neg_atom_wff: "¬" atom_wff

# 原子公式定义：谓词应用或项等词
atom_wff: pred_app | term_equality
pred_app: IDENTIFIER "(" term ("," term)* ")"
term_equality: term "=" term

# 项：常量或变量
term: IDENTIFIER

# 词法规则
IDENTIFIER: /[a-zA-Z_][a-zA-Z0-9_]*/
%ignore " "  # 忽略输入中的空格

语法设计说明 #

1. 解决嵌套括号解析问题

通过primary_wff中的"(" wff ")"规则，明确支持任意层级的嵌套括号，彻底解决之前的解析报错（原问题中的反斜杠错误大概率是括号未正确定义或规则冲突导致，此规则直接明确括号包裹的公式为合法基础单元）。

2. 消除同算子歧义并强制右结合

• 同算子连用必须通过括号显式指定右结合（如P(a)∧(Q(a)∧R(a))），语法层面禁止无括号的同算子链式写法（如P(a)∧Q(a)∧R(a)会直接报错），从根源上避免多解析树问题。
• 如果需要语法自动处理同算子右结合（无需括号），可将对应层级规则修改为右结合链式结构，例如将合取规则改为：

  conj_wff: primary_wff (("∧") conj_wff)?
  

  这样P(a)∧Q(a)∧R(a)会被唯一解析为P(a)∧(Q(a)∧R(a))，满足右结合要求。

3. 修正否定优先级问题

• 仅允许¬直接作用于原子公式（neg_atom_wff），且该形式属于最高优先级的primary_wff，因此¬P(a)会被优先解析为一个整体。
• 否定作用于复合公式时必须加括号（如¬(P(a)∧Q(b))），而¬P(a)∧Q(b)会因违反“强制括号”规则报错，必须写成(¬P(a))∧Q(b)，彻底消除歧义。

4. 强制括号约束（除无括号否定原子外）

• 仅三种无括号形式合法：¬P(a)（否定原子）、P(a)/a=b（原子公式）、(...)（括号包裹的任意公式）。
• 所有跨算子组合、复合公式的运算都必须加括号，确保每一步运算的结合顺序唯一，生成唯一解析树。

合法/非法输入示例 #

内容的提问来源于stack exchange，提问作者Vivek Joshy