跳至内容
Topos Uranos
中文 (中国)

范式算法及其应用

摘要

关于范式的一课证明了每个公式都等价于一个析取范式和一个合取范式；本课讲授如何不借助真值表来计算它们，以及如何使用它们。计算是一个分三个阶段的重写算法：消去双条件、不相容析取、或非和蕴涵；用德摩根律和双重否定把否定推到变元上；然后进行分配，求析取范式时把合取对析取分配，求合取范式时把析取对合取分配。本课证明它的正确性（这是语义替换的推论）和它的终止性（借助一个在每个阶段的每一步都减小的数值度量）；还证明它的局限：由 nn 个两变元合取构成的析取，其合取范式必然有 2n2^n 个子句。随后，从一个看不见内部的装置的真值表得到范式，通过合并相邻行加以化简，并把它们转换为串联和并联的开关电路。一个四开关装置的问题得到完整解答，包括它的表、两种范式和电路；五开关的问题留作挑战。

学习目标

  1. 运用重写算法求出一个公式的析取范式和合取范式，并根据双条件出现的位置选择合适的消去方式。
  2. 借助语义替换证明算法是正确的，借助在每一步都减小的度量证明它会终止；并解释为什么合取范式可能比原公式长出指数倍。
  3. 从黑箱的真值表构造它的范式，并通过合并相邻行加以化简。
  4. 用公式表示串联和并联的开关电路，并设计、化简满足以自然语言给出的规格的电路。

关于范式的一课给出了范式存在的两个证明。第一个借助真值表，它有 2n2^n 行，对应 nn 个变元；第二个从变元出发，沿着公式唯一的形成规则遍历公式。两者都没有说明，面对一个用蕴涵、双条件和嵌套否定写成的公式该如何处理，而公式通常正是以这种样子出现的。如果是这样，就缺少一个直接作用于写法本身的程序：它可以不加思考地执行，确知它会终止，并且给出一个等价的公式。这就是算法，研究它是本课的第一个目标；第二个目标是用它来做的事：用公式描述一个装置的行为，并构造一个再现这种行为的电路。

写法与替换

回顾一下：本课程的公式是由圆圈和圆盘组成的符号串，而 ¬\neg、∨\vee、∧\wedge、→\rightarrow、↔\leftrightarrow 和 ⊻\veebar 是由或非定义的缩写（见关于命题逻辑的语言的一课）。当我们写 ((p∨q)→(¬q∧p))((p \vee q) \rightarrow (\neg q \wedge p)) 时，写的不是符号串，而是它的一种写法：一棵树，它的叶是变元，节点是联结词 ¬\neg、∧\wedge、∨\vee、→\rightarrow、↔\leftrightarrow、⊻\veebar 和 ↓\downarrow，每个节点带有各自的成分。每种写法只指称一个公式，即展开其缩写后得到的公式；而同一个公式可以有多种写法：关于范式的一课已经指出，¬¬φ\neg\neg\varphi 和 (φ∨φ)(\varphi \vee \varphi) 是同一个符号串。算法读的是写法，而不是符号串；因此有必要区分两者。由于这种区分只在需要知道每一步作用于何处时才重要，我们用字母 φ\varphi、ψ\psi、χ\chi 既表示写法，也表示它们所指称的公式，并在所指称的公式语义等价时写 φ≡ψ\varphi \eqsem \psi。一个写法的子写法是以它的某个节点为根的子树。

算法的一步把一个子写法替换为另一个。保证这种替换不改变意义的工具，是关于语义后承与语义等价的一课中的语义替换定理；但那条定理替换的是符号串中的一次出现，而一个子写法可能对应符号串中的多次出现，因为每个缩写都会复制它的成分：在 (φ∨ψ)=((φ↓ψ)↓(φ↓ψ))(\varphi \vee \psi) = ((\varphi \downarrow \psi) \downarrow (\varphi \downarrow \psi)) 中，成分 φ\varphi 出现了两次。下面的引理把替换推广到写法上。

引理写法中的替换

设 χ\chi 是一个写法，θ\theta 是它的一个子写法，θ′\theta' 是一个写法，满足 θ≡θ′\theta \eqsem \theta'。若 χ′\chi' 是把 χ\chi 中的这个子写法替换为 θ′\theta' 所得的结果，则 χ≡χ′\chi \eqsem \chi'。

证明

  1. χ′=θ′≡θ=χ\chi' = \theta' \eqsem \theta = \chi

    对 θ\theta 所在根节点的深度作归纳，深度即 χ\chi 中位于该节点之上的联结词的个数。若深度为 00，子写法就是整个写法。

  2. χ=c(χ1,χ2),χ′=c(χ1′,χ2),χ1′≡χ1\dato{hi}{\chi = c(\chi_1, \chi_2), \qquad \chi' = c(\resaltar{\chi_1'}, \chi_2), \qquad \chi_1' \eqsem \chi_1}

    若深度大于 00，则 χ\chi 的根是一个联结词 cc，其成分为 χ1\chi_1（以及 χ2\chi_2，如果 cc 是二元的），而 θ\theta 以其中一个成分（比如 χ1\chi_1）中的某个节点为根，深度更小。由归纳假设，在 χ1\chi_1 内部所作的改变给出一个等价的写法。

  3. v(χ′)=Fc(v(χ1′),v(χ2))=Fc(v(χ1),v(χ2))=v(χ)v(\chi') = F_c\left( v(\chi_1'), v(\chi_2) \right) = F_c\left( v(\chi_1), v(\chi_2) \right) = v(\chi)

    由派生联结词的值定理（见关于命题逻辑的语义学的一课）以及或非的条款，c(χ1,χ2)c(\chi_1, \chi_2) 在一个赋值下的值是 χ1\chi_1 和 χ2\chi_2 的值的函数，而这两个值不变。因此 χ\chi 和 χ′\chi' 在每个赋值下取相同的值。

这里 FcF_c 是联结词的真值函数：F¬(a)=1−aF_\neg(a) = 1 - a，F∧(a,b)=abF_\wedge(a, b) = ab，其余依此类推。同样的结果也可以由语义替换定理得到：对符号串中 θ\theta 的每个副本各应用一次，再用传递性把这些等价连接起来；借助写法的证明更短，因为它计算的是写出的联结词，而不是副本。