命题逻辑的解析器组合器

Parser combinator for propositional logic

我想设计一个组合器来解析命题逻辑。这是 simple BNF:

<sentence> ::= <atomic-sentence> | <complex-sentence>
<atomic-sentence> ::= True | False | P | Q | R
<complex-sentence> ::= (<sentence>)
                       | <sentence> <connective> <sentence>
                       | ¬<sentence>
<connective> ::= ∧ | ∨ | ⇒ | ⇔

问题是语法是左递归的,导致死循环:一个句子可以是一个复句,可以从一个句子开始,可以是一个复句,...永远。这是导致此问题的例句:

P∧Q

是否有一种简单的方法来修复语法以使其适用于解析器组合器?谢谢

FWIW,我在 F# 中使用 FParsec,但我认为任何解析器组合器库都会有同样的问题。

FParsec 可以使用 OperatorPrecedenceParser class 处理中缀运算符,您只需指定哪些运算符具有哪些关联性和优先级,而无需实际为中缀表达式编写语法。对于 class 不适用的情况,对于没有等效 class 的解析器组合器或在如果您只是不想使用它,或者至少对没有它如何解决问题感兴趣。

解析器组合器往往不支持 left-recursion,但它们确实倾向于支持重复。幸运的是,可以使用 * 重复运算符将 <a> ::= <a> <b> | <c> 形式的 left-recursive 规则重写为 <a> ::= <c> <b>*。如果您然后 left-fold 遍历结果列表,您可以构建一棵树,它看起来就像您从原始语法中获得的解析树。

因此,如果我们先将 <complex-sentence> 内联到 <sentence> 中,然后应用上述模式,我们将得到 <a> = <sentence><b> = <connective> <sentence><c> = <atomic-sentence> | '(' <sentence> ')' | ¬<sentence>,结果是转换后的规则如下:

<sentence> ::= ( <atomic-sentence>
               | '(' <sentence> ')'
               | ¬<sentence>
               )* <connective> <sentence>

为了提高可读性,我们将括号内的部分放入其自己的规则中:

<operand>  ::= <atomic-sentence>
             | '(' <sentence ')'
             | ¬<sentence>
<sentence> ::= <operand> (<connective> <sentence>)*

现在如果你尝试这个语法,你会发现一些奇怪的东西:由 * 创建的列表将只包含一个元素(或 none)。这是因为如果有两个以上的操作数,right-recursive 对 <sentence> 的调用将耗尽所有操作数,创建一个 right-associative 解析树。

所以上面的语法真的等同于此(或者更确切地说,语法是有歧义的,但解析器组合器会将其视为等同于此):

<sentence> ::= <operand> <connective> <sentence>

这是因为原来的语法有歧义。模棱两可的定义 <s> ::= <s> <c> <s> | <o> 可以解释为 left-recursive <s> ::= <s> <c> <o> | <o>(这将创建一个 left-associative 解析树)或 right-recursive <s> ::= <o> <c> <s> | <o>( right-associative 解析树)。因此,我们应该首先通过选择其中一种形式来消除歧义,然后在适用的情况下应用转换。

所以如果我们选择 left-recursive 形式,我们最终会得到:

<sentence> ::= <operand> (<connective> <operand>)*

这确实会创建包含多个元素的列表。或者,如果我们选择 right-recursive 规则,我们可以只保留它 as-is(不需要重复运算符),因为没有要消除的 left-recursion。

正如我所说,我们现在可以通过从 left-recursive 版本中获取列表并 left-fold 得到一棵 left-associative 树,或者通过获取 right-associative 一个right-recursive 版本。然而,这两个选项都会给我们留下一个将所有运算符视为具有相同优先级的树。

要确定优先级,您可以将调车场算法之类的东西应用于列表,或者您可以先 re-write 考虑优先级的语法,然后应用转换。