研一选修课程

形式化方法

课程大纲

数学基础

计算复杂性理论

研究的是哪些问题是可以被计算机计算的：

• P问题：存在多项式时间复杂度解法的问题（比如大家常刷的LeetCode算法题）
• NP问题：不确定能否找到多项式时间复杂度解法，但是有多项式时间复杂度的方法来验证答案是否正确的问题(就比如Q:打印出集合$A$的所有子集，现有方法似乎只有穷举法，$2^n$ 的时间复杂度，但是验证某个集合是否是集合$A$的子集可以很快判定出来，因此人们不禁乐观的想(^_^)是否只是人们没有发现多项式的解法，而非数学意义上完全不存在这样的多项式时间算法来求解这样的NP问题)
• NPC问题：NPC完全问题。NPC问题 $\subseteq$ NP问题,而且对于任何 $\forall x \in $ NP问题,都可以在多项式时间内转换或归约成某一个NPC问题。

NPC问题是最近几十年对P?=NP问题比较大的理论突破。人们乐观的认为，只需要解决一个NPC问题，也就可以解决所有的NP问题。但是可惜的是，直到现在，人们还是没有解决出一个NPC问题。所以慢慢的更多的人感觉用永远也无法找到了。

以及证明任意一个NPC问题都可以解决所有的NP问题，但是NPC问题也有难度的区别，因此将目光聚焦于那些更简单的NPC问题会更简单。

上下文无关文法

是一套通过四元组来描述形式系统的符号工具。

四元组： G = {N、 T、 S、 P}

• N是非终结符的有限集合。
• T是终结符的有限集合，且 $\text{N} \cap \text{T} = \varnothing$。
• S是开始符号，且 $\text{S} \in \text{N}$。
• P是产生式的有限集合，每个产生式具有的形式如：$\text{N} \to \alpha, \alpha \in (\text{N} \cup \text{T})^*$

下面我们来分析什么是上下文无关：

假设我们有产生式 $\text{S} \to \text{a} \mid \text{b}$,那么如果我们遇到式子 $\text{aS}$,那么可以替换为 $\text{aS} \to \text{aa} \mid \text{ab}$,同理当我们遇到式子 $Sb$ 时，可以替换为 $\text{Sb}\to\text{ab}\mid\text{bb}$。所以在上下文无关文法中，我们遇到 $\text{S}$ 时，我们无需去关心 $\text{S}$ 的左边和右边是什么符号（这里的a、b其实就是所谓的上下文），直接根据产生式去替换就行。

但是如果我们还有产生式 $\text{aS}\to aa$,那么下次当我们遇到式子 $\text{aS}$ 时，不能直接去替换 $\text{S}$，还得去研究 $\text{S}$ 的上下文。这时候就是上下文有关了。

例1.1 给定文法G

​ $E ::= E + E \mid E - E \mid E * E \mid E / E \mid (E) \mid n$

其中，终结符 $T$ 的集合为 $\lbrace +,-,*,/,n,()\rbrace$,

并且符号 $n$ 表示整数； 非终结符 $N$ 的集合为 $\lbrace E \rbrace$；

解： 上面其实就是一个标准的上下文无关文法，他包含了我们之前说的四元组：G = {N、 T、 S、 P}，通常我们使用大写字母表示非终结符，小写字母表示终结符。这里的 $E$ 其实充当开始符号S的作用，不必拘泥于字母表示。

这个文法G可表示的集合为整数域上加减乘除的表达式

Q1： 判断表达式 $1+2*3$ 是否是文法G的元素？

当然由于我们的文法G的规则不够完善，还未支持四则运算的优先级，所以上面的推导过程不是唯一的。

我们还可以用推导树来表示刚刚的推导过程：

Q2： 怎么修改文法G的规则使得可以支持四则运算的优先级？

在《形式化方法》这门课中，上下文无关文法只是我们用来表达命题逻辑、谓词逻辑等等的一个最基本的表达形式，所以了解到这里就已经够了，如果想要更深入的进行学习，可以学习另一门课程《编译原理》。

结构化归纳法

归纳法(Induction)是一个非常强大的数学工具。

• 数学归纳法(Mathematical induction)：我们在高中阶段就已经学过了，他其实是建立在natural number上的一套普适原则。在高中阶段我们并没有研究数学归纳法的证明，其实这个涉及到了什么是natural number?我们需要使用纯数中的皮亚诺公理系统（Piano number)来证明这个定理。
• 结构化归纳法(Structural induction)：Do induction on any recursive defined structures。
• 良基归纳(Well-founded induction)：是基于 $2^{nd}$ 数学归纳法而推广到任意线性序的归纳法。

下面我们给出对于结构化归纳法的定义：

对于产生式：

其中非终结符A在 $\alpha_i、1 \leq i \leq m$ 中不出现。要证明某个命题P(A)成立，只要证明如下两个步骤：

1. 基础步：证明命题 P 对 $\alpha_i、1 \leq i \leq m$ 都成立；
2. 归纳步：分别假设命题 P 对 $\beta_i A \gamma_i、1 \leq i \leq n$ 中的A成立，分别证明 $P(\beta_i A \gamma_i)$ 成立。

综合上述两个步骤，可证明命题P(A)成立。

例1.2 证明例1.1给定文法表示的集合A，左括号和右括号的数量相等

证明：设用符号(L(A))和(R(A))分别来表示集合A的左括号和右括号的数量。

归纳基础：首先对集合A的元素进行证明，可得 $L(n) = R(n) = 0$，成立。

归纳推理：设 $L(E) = R(E)$ 成立，则：

成立，同理可证 $E - E、E * E、E / E$ 成立；对 $(E)$ 进行验证，可得：

成立。所以，我们可以得出对于例（1.2）给定文法所表示的集合，具有左括号等于右括号的性质。证毕。

命题逻辑

语法规则

首先我们用之前学到的上下文无关文法，给出命题逻辑的语法规则：

符号 $\top , \bot , x$ 分别表示逻辑常量“真”，逻辑常量“假”，和原子命题变量。这三种语法形式都是基本的，因此我们可称它们为原子命题（其实就是上面的终结符）。

后面4个是通过连接词连接子命题，而构成复合命题。

证明系统

我们使用自然演绎系统这种形式化的逻辑证明方式系统来作为命题逻辑的证明系统。

首先我们需要先确定一些假定的推理规则，然后利用这些规则，在假定的一个真前提下，得出真结论。这里假定的真前提就是所谓的环境。（我们不关心这些前提实际的真假，只是在推理过程中假定他们为真）

定义 $2.1$（环境） 环境 $\Gamma$ 是由$n，n\ge 0$，个命题构成的命题列表

特别的，若 $n=0$,我们称 $\Gamma$ 为空环境。

定义 $2.2$(断言) 断言是由环境 $\Gamma$，和命题 $P$ 构成的元组

$\vdash $ 是推导符号，也即环境 $\Gamma$ 为真可以断言得到命题 $P$ 为真。

定义 $2.3$(证明规则) 证明规则是形如

的一条公式，其中 $n \ge 0$。

证明规则由三部分组成：

• 规则的前提：横线上方的 $n$ 条断言
• 规则的结论：横线下方唯一的断言
• Rule-Name：规则的名字，唯一的表示了该规则

推导规则

首先我们来看看最简单的变量规则，它是一条公理，也就是这个规则结论的推出是不需要前提的：

显然如果命题$P$在环境中出现，根据定义就可以推出$P$成立。

下面是真引入规则：

它也是一条公理，表示在任意环境 $\Gamma$ 中，命题 $\top$ 都无条件成立。

接下来我们来看看假消除规则：

可以理解为环境 $\Gamma$ 能推出 “假”，即 $\Gamma$ 中包含矛盾（比如同时有 $A$ 和 $\neg A$），那么环境 $\Gamma$ 能推出任意命题 $P$（无论 $P$ 本身是否合理）。

逻辑意义：维护 “无矛盾则有效” 的体系，它揭示了 “矛盾会摧毁推理有效性” 这一本质，迫使使用者必须保证前提的一致性，否则推理将失去意义。

其他的规则我们也就不一一讲解了，下面给出完整的最基础的$14$条命题逻辑的推理规则：

例2.1 根据上面的推导规则，画出命题 $\vdash P \to \neg \neg P$ 的证明树

从下往上根据上面的14条推理规则去找匹配的进行推导就行，最后推导到公理即可：

SAT

SAT（布尔可满足性理论）：given a proposition P, is it satisfiable?

第一个NPC问题(Cook-Levin, 1971)

显然我们可以通过画真值表的方式来得到答案，但是时间复杂度是$O(2^n)$。

那么有没有更快一点的方式让计算机来解决SAT问题呢？

有的有的兄弟，那就是就是DPLL算法：

• CNF（合取范式）
• 解析与传播
  • 解析：决策
  • 传播：布尔约束传播（BCP）

所有命题公式都可以转换成 CNF 的等价公式。在布尔逻辑中，如果一个公式公式(数理逻辑)是子句的，那么它是合取范式（CNF）的。作为规范形式，它在自动定理证明中有用。

例如，下列所有公式都是CNF:

而下列不是:

上述三个公式分别等价于合取范式的下列三个公式:

等价转换公式：

例2.2 转换命题

$$ > (p_1 \land \neg \neg p_2) \lor (\neg q_1 \to q_2) > $$

为CNF命题。

1. 消去蕴含。

2. 转换为NNF。

3. 等价转换为CNF

构造逻辑

与经典命题逻辑的区别：是否接受排中律 $\vdash P \lor \neg P$ ?

也就会导致我们无法使用反证法来证明命题成立。也就是我们再也无法通过证明 $\neg P$ 成立来证明 $P$ 不成立。

语法规则

$\neg P$ 被替换为 $p \to \bot$，而不再出现。

证明系统

同命题逻辑。

推导系统

剔除了双重否定律以及$\neg$的引入和消去规则，其他都同命题逻辑。

谓词逻辑

语法规则

$E$:表达式

$x$：变量

$c$：常量

$R$:关系

$r()$：关系算符

$P$：命题

Intuition:

我们把上面的这套公理化系统引入到数论中直观感受一下各项代表着什么：

很明显：上面这套谓词逻辑是数论的一种抽象，这种Syntax是由逻辑学派创建出来的。逻辑学已经有2000多年的历史了，最终确定下来这种形式，其实是对其中的抽象性和具体性的一种平衡。如果太讲究抽象性，那么就无法得出什么meaningful的结论，但如果太讲究具体性，就有可能会偏向于某一理论。

谓词逻辑其实就是从数论、集合论、矩阵理论等等中抽象出了一个共性语法规则，他的好处就是如果能正面共性成立，就无需去将每一个底层理论继续证明，就比如哥德尔不完备性定理就是在数理逻辑框架下证明，所以对于任意框架都成立。

证明系统

同命题逻辑。

Bound free variables

Bound variables （绑定变量）：作用域内定义的变量，默认只绑定最近的一个命题

Free variables （自由变量）：作用域内使用却未在该作用域内定义的变量

$\forall x, P(x,y)$中，$x$ 就是绑定变量，$y$ 就是自由变量。

其实就可以翻译成类似下面的code：

1
2
3
4

int y = 10;
int f(int x) {
	return p(x, y);
}

下面给出绑定变量的计算规则：

根据上面的计算规则，即可输入一个命题，返回一个绑定变量的集合。

例4.1 计算命题 $A = \exists x (P(x, y) \lor \forall y Q(x, y) \to R(x, z))$ 中的绑定变量集合

同理，下面给出自由变量的计算规则：

例4.2 计算命题 $A = \exists x (P(x, y) \lor \forall y Q(x, y) \to R(x, z))$ 中的自由变量集合

替换

作用域内的自由变量被替换成表达式

和上面一样，我们下面给出替换规则：

其中 $\mapsto$ 用于表示映射箭头，表示将某个变量替换成指定的表达式/值

例4.3 设存在一个命题

$$ > F = \exists x \bigl( P(y, x) \land \forall y \, (\neg Q(y, x)) \lor P(y, z) \bigr)， > $$

给出使用替换规则 $F[y \mapsto x]$ 的结果。

要切记替换规则，遇到绑定变量，是不用替换的，需要进行绑定变量的重命名，也就是上面第二行到第三行所做的事。

$\alpha$ - 重命名

如果在替换自由变量之后带来了变量名的冲突问题，我们就需要提前将一些绑定变量进行 $\alpha$ - 重命名

推导规则

谓词逻辑的推导规则是在之前命题逻辑的14条推导规则的基础上，新增了下面四条推导规则：

SAT

SAT（可满足性理论）：given a proposition P, is it satisfiable?

SAT for 命题逻辑:

• NPC问题。但是从实践上来说，使用DPLL等算法可以在很合理的时间内求解相当大规模的实际问题

SAT for 谓词逻辑:

• 不可判定/理论上证明不可能有算法可以在合理时间求解/不可解
• 这就引导我们去思考：有没有可能通过我们使用一些特殊的子集，对这个子集进行求解仍然是可解的呢？其实这就是下面我们要讲的theory

theory

比如 EUF理论（等式与未解释函数理论），

EUF

等式理论定义：

未解释函数定义：

未解释函数，它通常指在一个公式中没有被解释的函数，或者说没有被定义的函数。例如，公式 $F(x) = F(G(y))$中 $F、G$就是未解释函数。

那么对于等式与未解释函数该怎么求解？

下面我们给出一条全等规则：

这个规则也是我们用来证明两个未解释函数相等的重要规则，这个思想也是被广泛应用于一些实际证明中的，就比如程序等价性的证明，以及编译器中产生很多中间表示，这些中间表示的等价性。

线性算数理论

线性算数理论定义：

下面有一个反常识的特性：

求解算法的变量论域

• 整数域（$\mathbb{Z}$），复杂度：NPC
• 有理数域（$\mathbb{Q}$），复杂度polynomial

结果是更大的有理数域的复杂度是多项式的。

下面介绍三种算法：

1. Fourier-Motzkin(消元法)

2. 单纯形法

3. 分支定界

数据结构理论

SMT

SMT(可解释性模理论)：Satisfiability modulo theory

SAT + Theory Solvers = SMT

SMT的意义在于：CS中的终极大杀器。针对非常非常复杂的问题（如NPC问题），有没有一套通用范式来解决这类难题吗？那就是SMT。如果一个问题很难，我不知道该怎么解，那就上SMT，大概率就有用；如果SMT都没用，那估计你用其他方法也解不了。