我正在尝试创建一个库，用于从TPTP（千问题定理证明器）语言的公式中生成抽象语法树。我使用了一个很好的ANTRL4语法https://github.com/TobiasGleissner/TPTP-ANTLR4-Grammar来生成解析器。我有一个公式（TPTP表达式）(![A:animal]:?[H:human]:H=owner_of(A))，它通过标准的ANTLR4解析器生成的美化（漂亮打印）解析树如下所示：

thf_formula  thf_logic_formula    thf_unitary_formula (      thf_logic_formula        thf_binary_formula          thf_binary_pair            thf_unitary_formula              thf_quantified_formula                thf_quantification                  thf_quantifier                    fof_quantifier !                  [                  thf_variable_list                    thf_variable                      thf_typed_variable                        variable A                        :                        thf_top_level_type                          thf_unitary_type                            thf_unitary_formula                              thf_atom                                thf_function                                  atom                                    untyped_atom                                      constant                                        functor                                          atomic_word animal                  ]:                thf_unitary_formula                  thf_quantified_formula                    thf_quantification                      thf_quantifier                        fof_quantifier ?                      [                      thf_variable_list                        thf_variable                          thf_typed_variable                            variable H                            :                            thf_top_level_type                              thf_unitary_type                                thf_unitary_formula                                  thf_atom                                    thf_function                                      atom                                        untyped_atom                                          constant                                            functor                                              atomic_word human                      ]:                    thf_unitary_formula                      thf_atom                        variable H            thf_pair_connective =            thf_unitary_formula              thf_atom                thf_function                  functor                    atomic_word owner_of                  (                  thf_arguments                    thf_formula_list                      thf_logic_formula                        thf_unitary_formula                          thf_atom                            variable A                  )      )

通常情况下，原始解析树相当复杂，但我理解其中的每一部分，除了我的问题所在——为什么解析树中会出现thf_binary_formula和thf_binary_pair？据我所知，TPTP二元公式是用于二元连接词（合取、析取、蕴含）的，但我的公式中没有这些，我的公式只有等式函数=和两个量词，这两个量词都形成了嵌套的一元公式。

那么，TPTP二元公式的含义是什么，为什么在没有二元连接词的这个简单公式的解析树中会出现它？

回答：

这里没有真正的答案，只能说：因为语法作者就是这样定义规则的 🙂

让我们看一个非常简单的语法：

grammar Expr;parse : expr EOF ;expr : add_expr ;add_expr : mult_expr ( ('+' | '-') mult_expr)* ;mult_expr : atom ( ('*' | '/') atom)* ;atom : '(' expr ')' | NUMBER ;NUMBER : ( [0-9]* '.' )? [0-9]+ ;SPACES : [ \t\r\n]+ -> skip ;

因为add_expr放在mult_expr之前，像1+2*3这样的输入会导致*运算符的优先级高于+运算符。这会生成以下解析树：

然而，由于语法是这样写的，解析树中也会为简单的数字1包含（空的）add_expr和mult_expr节点：

这就是为什么你在解析树中会看到一些你可能没想到的空节点。