是否可以用一阶逻辑表示上下文无关文法？

Question

简单地说，我有一个 EBNF 语法和一个解析树，但我不知道是否有一个程序可以在一阶逻辑中翻译它。

例如：

DR ::= E and P
P ::= B | (and P)* | (or P)*
B ::= L | P (and L P)
L ::= a

Answer 1

是的，有。翻译表格产生式的一般模式

A ::= B C ... D

is to paraphrase 声明式地表示

终结符序列s是一个A（或者：A生成序列s，如果你更喜欢那个公式）如果：

• s 是 s_1、s_2、...s_n 和

  的串联

• s_1是一个B/B生成序列s_1，而

• s_2是一个C/C生成序列s_2，而

• ...

• s_n是一个D/D生成的序列s_n。

假设我们使用 generates 谓词以显而易见的方式编写这些，并且我们可以使用 || 编写连接。运算符，你的第一条规则变成（如果我猜对了 E 和 P 是非终结符并且“and”是终结符）类似于

generates(DR,s) ⊃ generates(E,s1) 
                  ∧ generates(and,s2)
                  ∧ generates(P,s3)
                  ∧ s = s1 || s2 || s3
         

要确定后件（即证明 s 是 A），请证明前件。只要语法确实生成了一些句子，并且只要你有一些前提来定义终结符号的“生成”关系，证明就会很简单。

Prolog 定子句语法是这种模式的一个很好的实例。我们中的一些人需要一些时间来理解和欣赏 DCG 中差异列表的使用，但它们处理将 s 划分为子序列以及子序列与右侧不同部分的关联比上面给出的简单逻辑转换要优雅得多。