查看“︁前束范式”︁的源代码

[[分类:谓词逻辑]]{{DEFAULTSORT:qian2shu4fan4shi4}}
{{#seo:
|keywords=前束范式, 范式, PNF
|description=本文介绍前束范式（PNF）的定义、性质与转换方法，包括这种范式作为谓词公式标准形式的概念，其结构特点及其在逻辑化简和计算机科学中的重要性。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-07-24
}}
{{InfoBox
|name=前束范式
|eng_name=prenex normal form
|aliases=PNF
}}
[[谓词公式]]可以表示为[[逻辑等值]]的标准形式。
全部量词都是常见量词，全部[[量词|量化表达式]]都在最前，且量词均非否定、无取值范围、辖域覆盖到公式尾部，称为'''前束范式'''('''prenex normal form''', '''PNF''')。
前束范式是谓词公式的重要的标准形式。

== 定义 ==

{{InfoBox
|name=首标
|eng_name=prefix
}}
{{InfoBox
|name=基式
|eng_name=matrix
|aliases=母式
}}
对谓词公式，若其具有形式 <math>\mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n \phi</math> ，其中 <math>\phi</math> 不含量词，量词 <math>\mathsf{Q}_i \in \{\forall, \exists \}</math> 且每个约束变项 <math>x_i</math> 均有在 <math>\phi</math> 中的出现，则称其为一个'''前束范式'''('''prenex normal form''', '''PNF''')。其中 <math>\mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n</math> 称为'''首标'''('''prefix''')， <math>\phi</math> 称为'''母式'''/'''基式'''('''matrix''')。

对谓词公式 <math>\psi</math> ，若有一前束范式与其逻辑等值，则称其为公式 <math>\psi</math> 的一个'''前束范式'''。

注：有的定义不要求约束变项均有在基式中出现。

=== 形式语言定义 ===

前束范式构成的集合是[[谓词语言]]的子集，但合法前束范式要求约束变项与基式间的关系，是[[上下文有关文法]]。

== 性质 ==

* '''前束范式存在定理'''('''prenex normal form theorem''')：对每个公式 <math>\psi</math> ，都存在一个前束范式 <math>\phi</math> 与其逻辑等值。

== 转换算法 ==

任意谓词公式都能通过以下步骤转换为前束范式。
# 将非常用量词通过常用量词表达：仅通过 <math>\exists,\forall</math> 表达。
# 消去非基本逻辑联结词（主要指[[蕴涵]] <math>\rightarrow</math> 和[[等价（逻辑）|等价]] <math>\leftrightarrow</math> ）：将其他逻辑联结词替换为仅含 <math>\lnot,\land,\lor</math> 的表达方式。
# 深化否定词到否定表达式：使用[[de Morgan 律（逻辑）|德·摩根律]]将限定对象不是原子公式的否定符号移到原子公式前。包括析取、合取、存在量词、全称量词外的否定符号均被移到内部，经此步骤后，否定词仅能作用于原子公式。
# 检查各量词所作用的变项是否有重复，若存在，需要进行[[易字]]避免冲突。
# 量词前移，使每个量词的辖域均覆盖全公式。

== 例子 ==

* <math>\forall x \exists y \forall z (p(x, y) \land \lnot r(z))</math>
* <math>\forall x \exists y \forall z p(x, y, z)</math> （基式是一个原子，不需要逻辑联结词）
* 若允许零元谓词， <math>p \land q</math> （基式中全部谓词都是零元谓词，没出现个体变项，就不需要量化表达式）

反例：
* <math>\lnot \forall x \exists y \forall z (p(x, y) \land \lnot r(z))</math> ：其中第一个否定词作用的不是原子公式，应当放到原子公式前，即 <math>\exists x \forall y \exists z (\lnot p(x,y) \lor r(z))</math> 。
* <math>\forall x \exists y (p(x, y) \land \forall z r(z))</math> ：量化表达式 <math>\forall z</math> 未提前，需要将其和 <math>\forall x \exists y</math> 放在一起。另外，由于 <math>x,y</math> 出现在同一个原子公式中，而 <math>z</math> 出现在另一个里，此处 <math>\forall x \exists y</math> 之间存在固定顺序，而 <math>\forall z</math> 和这两个表达式的顺序不影响，可以放在这两个表达式的前面、中间或后面。
* <math>\exists x p(x) \land \forall x q(x)</math> ：也是未提前，但是由于同时出现了 <math>x</math> ，需要将一个进行易字处理，如 <math>\exists x \forall y (p(x) \land q(y))</math> 。


{{谓词逻辑}}