数理逻辑及其 python 实现:2
Notes on 「Mathematical logic through python」
二、命题逻辑的语义
回顾上一节中对语法的定义：
- 构词法：哪些词汇是合法的（类似 python 变量规则，例如 8zbc 是不合法的 python 变量名， false 是不合法的 python 常量）
- 词的组合规则：单目和双目运算符
从创造者角度，它们是人的需求驱动，是目的和语义驱动下打磨出来的，但作为学习者，目前我们不知道它们代表什么，也就是说除了排列组合上的限制我们不知道这些符号的意义是什么。
不过仅仅围绕以上纯形式的东西，要用计算机去替代人脑来理解，就涉及到了 parsing, 树遍历, 递归，context free 等算法和概念。
给这些形式的内容中注入外部的解释，这种解释是二元的，是一种划分，可以把它们叫做上和下，左和右或者 0 和 1, 由于逻辑是人们是对现实中真和假概念进行建模，因此这里用了真和假这对概念，注意真和假已经丢弃了大部分外部的意义，它需要结合更强的故事解释器才能真正去解决问题，比如 "今天下雨了" 的意义并不会被逻辑系统处理，它只处理对这个陈述的真假，如果推理出这个句子是真，人或机器再用其他的方式去理解 “今天下雨了是真的”所代表的意义。
T2.1 - T2.4 模型和真值表
模型定义如下：
Let S be the set of variable names. A model M over S is a function that assigns a truth value to every variable name in S. That is, M : S → {True, False}.
definition 2.1 (Model)
它是对公式中命题的一组赋值，比如 {p:True, q: False}，在 python 中就是一个变量名到真值的字典：
from typing import AbstractSet, Iterable, Iterator, Mapping, Sequence, Tuple
Model = Mapping[str, bool]
以上 Mapping[str, bool] 类型很好地展示了 "模型" 是什么。
检查模型是否合法就是检查模型中变量名是否满足语法规则：
def is_model(model: Model) -> bool:
for key in model:
if not is_variable(key):
return False
return True
def variables(model: Model) -> AbstractSet[str]:
assert is_model(model)
return model.keys()
模型是对变量的语义，由外部提供，而为了得到公式的语义，则需要给符号赋予组合语义的计算规则：
Given a formula φ and a model M over a set of variable names that contains (at least) all those used in φ, we define the (truth) value of the formula φ in the model M recursively in the natural way:
- value(T) is True, value(F) is False
- value(p) is M(p)
- then use truth table to find the value of compond formulas
definition 2.2 (Truth Value of Formula in Model)
从代码上看，就可以计算 value(formula) 了，不过我们用 evaluate(formula), 注意这不是 Formula 类里的函数。
def evaluate(formula: Formula, model: Model) -> bool:
assert is_model(model)
assert formula.variables().issubset(variables(model))
# Task 2.1
if formula.root == "T":
return True
if formula.root == "F":
return False
if is_unary(formula.root):
return not evaluate(formula.first, model)
if is_variable(formula.root):
return model[formula.root]
if formula.root == "&":
return evaluate(formula.first, model) and evaluate(formula.second, model)
if formula.root == "|":
return evaluate(formula.first, model) or evaluate(formula.second, model)
if formula.root == "+":
return xor(evaluate(formula.first, model), evaluate(formula.second, model))
if formula.root == "<->":
return evaluate(formula.first, model) == evaluate(formula.second, model)
if formula.root == "-&":
return not (evaluate(formula.first, model) and evaluate(formula.second, model))
if formula.root == "-|":
return not (evaluate(formula.first, model) or evaluate(formula.second, model))
if formula.root == "->":
return not evaluate(formula.first, model) or evaluate(formula.second, model)
def xor(a, b):
return (a or b) and (not a or not b)
以上可以看作一种树上的后序遍历算法，从计算结构上它和语法分析里的 repr 或者 polish 函数是一样的。
另外： 以上实现中加入了对额外的符号，比如 -|, <-> 的语义计算规则，这个在下一章中会提到。
当前最重要的是 \( p\to q \) 的语义， 只有 p 为真 q 为假的时候被计算为假，其他情况都是真，它实际代表了一种推理的"压缩"表达。
给定 n 个变量，可以构造出 \( 2^n \) 个不同的模型，以下函数根据变量集合生成所有该变量上的可能模型：
def all_models(variables: Sequence[str]) -> Iterable[Model]:
n = len(variables)
for v in variables:
assert is_variable(v)
# Task 2.2
def bin2model(num):
return {key: value == "1" for key, value in zip(variables, bin(num)[2:].zfill(n))}
for i in range(2 ** n):
yield bin2model(i)
list(all_models(['p', 'q']))
| p | : | False | q | : | False |
| p | : | False | q | : | True |
| p | : | True | q | : | False |
| p | : | True | q | : | True |
给定一个公式，对每一个模型能计算出一个语义，这种方式可以构造真值表
def truth_values(formula: Formula, models: Iterable[Model]) -> Iterable[bool]:
# Task 2.3
for model in models:
yield evaluate(formula, model)
list(truth_values(Formula.parse('~(p&q76)'), all_models(['p', 'q76'])))
| True | True | True | False |
def print_truth_table(formula: Formula) -> None:
# Task 2.4
vars = sorted(list(formula.variables()))
models = list(all_models(vars))
vars = vars + [repr(formula)]
length = [len(v) for v in vars]
print("|", end="")
for v in vars:
print(f" {v} |", end="")
print()
print("|", end="")
for v, n in zip(vars, length):
print(f"-"*(n+2) + "|", end="")
print()
values = list(truth_values(formula, models))
for model, res in zip(models, values):
print("|", end="")
for i, v in enumerate(sorted(model.keys())):
value = "T" if model[v] else "F"
print(f" {value.ljust(length[i] + 1, ' ')}|", end="")
exp_value = "T" if res else "F"
print(f" {exp_value.ljust(length[-1] + 1, ' ')}|")
print_truth_table(Formula.parse('~(p&q76)'))
| p | q76 | ~(p&q76) | |---|-----|----------| | F | F | T | | F | T | T | | T | F | T | | T | T | F |
T2.5 根据语义对公式分类：重言、矛盾和可满足
Tautologies, Contradictions, and Satisfiability
由于每个式子有了真假两种属性，那么可以根据这个属性对公式分类，有两种最特殊的公式：
- 在任何 model 下，都是真
- 在任何 model 下，都是假
- 除以上公式之外的属于第三种，它们的正式定义如下：
• A formula is said to be satisfiable if it gets the value True in some (at least one) model. A formula that is not satisfiable is said to be a contradiction. • A formula is said to be a tautology if it gets the value True in all models over its variable names.
definition 2.3 (Satisfiable Formula; Contradiction; Tautology)
以下是按语义对公式进行分类的代码实现，需要遍历所有模型来确定分类，复杂度是指数级别：
def is_tautology(formula: Formula) -> bool:
# Task 2.5a
return all(truth_values(formula, all_models(formula.variables())))
def is_contradiction(formula: Formula) -> bool:
# Task 2.5b
return not any(truth_values(formula, all_models(formula.variables())))
def is_satisfiable(formula: Formula) -> bool:
# Task 2.5c
return not is_contradiction(formula)
print(is_tautology(my_formula), is_contradiction(my_formula), is_satisfiable(my_formula))
False False True
T2.6 - T2.9 公式拟合：根据语义构造公式
正如上一章中， parsing 和 repr 类似一对互逆操作，本节讨论的函数与 evaluate 又是互逆的：
- evaluate 是给定公式和模型计算其（真值）语义
- _synthesize_for_model 是给定一个模型，构造出一个在该模型下为真的公式，也就是人先要求提出输入和输出的语义需求，要求返回一个满足输入输出的公式（这种需求在数字电路设计里很常见，比如要实现加法器，那么要求输入和输出满足加法求和关系，但本文之所以需要是出于理论目的的，即一种语义规范而构造语法对象的能力，这是证明完备性的重要一环）
def _synthesize_for_model(model: Model) -> Formula:
assert is_model(model)
assert len(model.keys()) > 0
# Task 2.6
vars = list(model.keys())
var = vars[0]
base = Formula(var) if model[var] else Formula("~", Formula(var))
for var in vars[1:]:
f = Formula(var) if model[var] else Formula("~", Formula(var))
base = Formula("&", f, base)
return base
比如给定 {p:True, q:False}, 那么 p|q, p&~q, q->p 都是 True, 都是合法的。
一个类比是，给定平面上两个点，找出能够穿过这些点的函数，如果不做规范，函数会有无穷个，因此可以限制只能用直线函数拟合，找到的方程就是唯一的了。同样地，为了返回唯一的逻辑表达式，对表达式的形式限制为 conjunctive clause 形式，只通过 & 来连接变量或者变量的否定
实现思路是：
如果模型中变量 p 的语义是 True, 那么公式中使用 p 本身，如果 q 对应的语义是 False, 那么公式中使用 ~q, 这样它们的 & 的结果就还是 True
这种方法构造出的 conjunctive clause 是唯一的，因为任何只有 & 作为二元连接符号的 conjunctive clause 公式的输出空间只有一行是 True，因此给定公式后，从输出映射到输入模型是唯一的，给定模型，从输出映射到公式也是唯一的。 & 具有一种逆向工程友好性。
由于表达式的语义允许有多个 True，因此把 conjunctive clause 用 or 连接起来，组成 disjunctive normal form (DNF):
def synthesize(variables: Sequence[str], values: Iterable[bool]) -> Formula:
assert len(variables) > 0
# Task 2.7
p = variables[0]
dnf = Formula("&", Formula(p), Formula("~" , Formula(p))) #placeholder
for model, value in zip(all_models(variables), values):
if value:
cclause = _synthesize_for_model(model)
dnf = Formula("|", dnf, cclause)
return dnf
formula = synthesize(['p', 'q'], [True, True, True, False])
print(formula)
for model in all_models(['p', 'q']):
print(evaluate(formula, model))
((((p&~p)|(~q&~p))|(q&~p))|(~q&p)) True True True False
以上给定的 ['p', 'q'], [True, True, True, False] 表示输入 (False,False) 对应 True， (False,True) 对应 True, (True, False) 对应 True, (False, False) 对应 False.
它是 ~(p&q) 或者 NAND 关系。 但在 DNF 的限制下，得到的是一个相对复杂的表达式：
((((p&~p)|(~q&~p))|(q&~p))|(~q&p))
这里第一个 p&~p 恒为假，是代码实现上作为初始占位符而设置的。
牺牲部分表达式的简洁性是追求形式统一付出的代价，好处是可以用一个通用的算法，根据语义模型构造出确定的符合语法的句子。
如果从第一章构词法的视角来看，DNF 是对公式 再进行了一次划分（分类）：
- 给定任何一个随机的字符串，根据命题逻辑语法规则，其中一小部分称为命题（proposition）或公式（formula）
- 对于这些合法的公式，从语义上看，有些公式是恒真的，有些公式是矛盾，还有些是没有可满足的。
- 给定任何模型，有无数个在该模型上为真的合法公式。
- 但我们还可以制定更细的语法规则，通过 DNF 语法规则筛选后，有些公式是 DNF, 有些并不是。
- 给定任何模型，一定有一个在该模型上为真的 DNF 公式。
符合某个模型的 DNF 公式也不一定是唯一的，比如以下式也等价于 p|q
((((~q&~p))|(q&~p))|(~q&p))
但它们在结构是相似的。
总结：
以上代码是根据给定的输入输出，用 DNF 形式构造一个 formula, 它需要遍历指数的语义空间，但这理论上证明了 The DNF Theorem:
Let S be a nonempty finite set of variable names. For every Boolean function f over the variable names in S (i.e., f arbitrarily assigns a truth value to every tuple of truth values for the variable names in S) there exists a formula in disjunctive normal form whose truth table is exactly the Boolean function f 。
theorem 2.1 (The DNF Theorem)
T2.8 - T2.9 Conjunctive Normal Form
在所有符合语法的句子中，除了 DNF 外，还有别的形式的句子，比如 CNF, 它和 DNF 是对偶的；
def _synthesize_for_all_except_model(model: Model) -> Formula:
assert is_model(model)
assert len(model.keys()) > 0
# Optional Task 2.8
vars = list(model.keys())
var = vars[0]
base = Formula(var)
base = base if not model[var] else Formula("~", base)
for var in vars[1:]:
f = Formula(var)
f = f if not model[var] else Formula("~", f)
base = Formula("|", base, f)
return base
def synthesize_cnf(
variables: Sequence[str], values: Iterable[bool]
) -> Formula:
assert len(variables) > 0
# Optional Task 2.9
p = Formula(variables[0])
f = Formula("|", p, Formula("~", p))
for model, value in zip(all_models(variables), values):
if not value:
dclause = _synthesize_for_all_except_model(model)
f = Formula("&", f, dclause)
return f
formula = synthesize_cnf(['p', 'q'], [True, True, True, False])
print(formula)
for model in all_models(['p', 'q']):
print(evaluate(formula, model))
((p|~p)&(~p|~q)) True True True False
这些代码证明了：
Let S be a nonempty finite set of variable names. For every Boolean function f over the variable names in S (i.e., f arbitrarily assigns a truth value to every tuple of truth values for the variable names in S) there exists a formula in Conjunctive Normal Form whose truth table is exactly the Boolean function f .
theorem 2.2 (The CNF Theorem)
CNF 和 DNF 都是语义相同的公式的不同形式表现，它们相对于其他等价形式的好处可以类比于多项式代数里的因式分解：
将多项式 \( x^2 + 3x + 2 \) 分解为因式 \( (x+1)(x+2) \)，我们得到了两个简单式子的乘积，在求根时，根据乘法的性质： ab=0, 那么 a 或 b 为 0, 这样直接得到 x+1=0 或 x+2=0, 一个全局球根的问题被乘法性质转成了两个局部的简单式子同时求根问题。
同样的 DNF 和 CNF 形式将复杂的逻辑表达式分解为更简单的结构相同的部分，并且各个部分都是用同一个连接词串联起来， 类似的，以 DNF 形式 (p|~r)&(~p|~q) 为例，它被拆分成了两个简单的式子，更重要的是，根据 & 的性质，只有两个同时为 True 结果才为 True, 在求值时一旦检查到 p 为真，第一个子句就为真， ~r 不需要检查了，而一旦知道 (~p|~q) 为假，那么整个式子就为假，也就不需要继续检查了。
反过来，在逆向求解 (p|~r)&(~p|~q) = 1 方程时（检查可满足性），只要求各个子项同时为 1 ，这样，一个整体的约束变成了多个局部约束，在语义检查时，一旦某个局部子公式不为 True 就可以马上停止验证，这是搜索的一种剪枝，使得搜索更为高效。
另外，这种多个局部约束的问题是一种通用模式，下一节就是一个具体的例子，可以把其他搜索问题（约束满足问题）看作对 CNF 公式可满足性检查等价。从而用同一套方式来解决问题，或者把一类问题在抽象层面归为同一类里进行研究。
T2.10 将 3-color 转成命题逻辑表达式
T2.10: 将三色问题用命题逻辑表达式写出来（一般形式，而不是 DNF 也 不是 CNF 形式），这里涉及对一个点的颜色用多个逻辑变量来编码， 例如每个结点 i 要用两个变量来编码颜色：
| p[i] | q[i] | |
|---|---|---|
| 颜色1:红 | 1 | 1 |
| 颜色2:绿 | 1 | 0 |
| 颜色3:蓝 | 0 | 1 |
剩下的是冗余编码（四色问题则刚好两个变量可以完全表示）
把三色问题用命题逻辑表达出来的算法是一种 reduce 算法，该算法是 O(n) 级别的， n 是逻辑表达式中子句的数量。
比如给定要给图，只有两个节点，问是否可以用三种颜色上色，问题就转为以下三类约束组成的表达式：
1. 节点 1 的颜色唯一性约束： (p[1] & q[1]) | (p[1] & ~q[1]) | (~p[1] & q[1]) 2. 节点 2 的颜色唯一性约束： (p[2] & q[2]) | (p[2] & ~q[2]) | (~p[2] & q[2]) 3. 相邻节点不同色约束： (~(p[1] & q[1]) | ~(p[2] & q[2])) & (~(p[1] & ~q[1]) | ~(p[2] & ~q[2])) & (~(~p[1] & q[1]) | ~(~p[2] & q[1]))
算法实现为：
"""Reduction between computational search problems."""
from __future__ import annotations
from typing import AbstractSet, Mapping, Tuple, Union
#: A graph on a vertex set of the form ``(1,``...\ ``,``\ `n_vertices`\ ``)``,
#: represented by the number of vertices `n_vertices` and a set of edges over
#: the vertices.
Graph = Tuple[int, AbstractSet[Tuple[int, int]]]
def is_graph(graph: Graph) -> bool:
(n_vertices, edges) = graph
for edge in edges:
for vertex in edge:
if not 1 <= vertex <= n_vertices:
return False
if edge[0] == edge[1]:
return False
return True
def is_valid_3coloring(graph: Graph, coloring: Mapping[int, int]) -> bool:
assert is_graph(graph)
(n_vertices, edges) = graph
for vertex in range(1, n_vertices + 1):
if vertex not in coloring.keys() or coloring[vertex] not in {1, 2, 3}:
return False
for edge in edges:
if coloring[edge[0]] == coloring[edge[1]]:
return False
return True
def graph3coloring_to_formula(graph: Graph) -> Formula:
assert is_graph(graph)
# Optional Task 2.10a
(n_vertices, edges) = graph
variables = [["x" + str(n), "y" + str(n)] for n in list(range(1, n_vertices + 1))]
variables = sum(variables, [])
valid_color = Formula("T")
for i in range(1, n_vertices + 1):
f = Formula("|", Formula("x" + str(i)), Formula("y" + str(i)))
valid_color = Formula("&", f, valid_color)
res = valid_color
for i, j in edges:
xi = Formula("x" + str(i))
nxi = Formula("~", xi)
yi = Formula("y" + str(i))
nyi = Formula("~", yi)
xj = Formula("x" + str(j))
nxj = Formula("~", xj)
yj = Formula("y" + str(j))
nyj = Formula("~", yj)
xi_not_xj = Formula("&", Formula("|", xi, xj), Formula("|", nxi, nxj))
yi_not_yj = Formula("&", Formula("|", yi, yj), Formula("|", nyi, nyj))
i_not_j = Formula("|", xi_not_xj, yi_not_yj)
res = Formula("&", i_not_j, res)
return res
def assignment_to_3coloring(graph: Graph, assignment: Model) -> \
Mapping[int, int]:
assert is_graph(graph)
formula = graph3coloring_to_formula(graph)
assert evaluate(formula, assignment)
# Optional Task 2.10b
n_vertices, edges = graph
colors = {}
for i in range(1, n_vertices + 1):
colors[i] = boolean2color(assignment["x" + str(i)], assignment["y" + str(i)])
return colors
def boolean2color(x1, y1):
if x1 and y1:
return 1
if x1 and not y1:
return 2
if not x1 and y1:
return 3
def tricolor_graph(graph: Graph) -> Union[Mapping[int, int], None]:
assert is_graph(graph)
formula = graph3coloring_to_formula(graph)
for assignment in all_models(list(formula.variables())):
if evaluate(formula, assignment):
return assignment_to_3coloring(graph, assignment)
return None
有了该式子后，可以遍历整个指数空间找到满足该式子的一个 model （可满足性问题检查），有了 model, 马上就可以根据编码规则确定各个结点的颜色，于是就找到了三色问题的一个可满足解。
注意以上可满足的检查用的是 O(2**n) 算法，但如果一旦找到更快的可满足性算法，整个过程就可以加速。
反过来，要把命题公式转成 3 color 则充满 trick(需要很巧妙思考), 参考 SATto3color - YouTube
也就是说，归约可以是不对称的（难度上不对称，或者只有单向可以归约，最极端是 0 知识证明，即便解出了新问题的答案，最后也无法解出原问题，但可以知道原问题是否可解）
最后一点总结：
- DNF 是形如(x&y)|(x&z) 形式的公式，它是多个子句共同取 | 的结果。因此要检查可满足性，只需要检查 任意子句是否可能为真，而由于每个子句都是多个变量（或其否定）求 & 的形式，因此只需要检查每个变量（或其否定）是否为真，因此只需要扫描一遍公式就可以得到结论，属于 P 问题（多项式内求解）。但要询问某个 DNF 是否是恒真，就需要检查所有子句是否可能为假，这是 NP 问题。
- CNF 是形如 (x|y)&(x|z) 的公式，它和 DNF 对偶，多个子句取 & 的结果。因此要检查该公式是否恒真，只需要检查任意子句是否可能为假，也就是检查任意子句是否可能为假， 这是 P 问题，但它的可满足性检查则是 NP 问题。
- 3-CNF 公式是 CNF 的特例，要求 CNF 每个子句里有三个变量，如果不足，可以添加一个 placeholder 类型变量（比如 False），如果多于三个，比如 (x|y|z|w) 则可以拆成 (x|y|u)&(z|w|~u) 。
- 以上习题证明，三色问题可以用相对直接的方式（多项式复杂度算法）转为一般的命题逻辑形式，从而转为一般 逻辑形式的可满足性问题（SAT 问题或称为 GSAT 问题）。
- 而把公式形式限定为 CNF 形式从而可以转为 3-CNF 形式，则称为 3-SAT 问题，这个问题也是 NP 的，并且是 NPC 。（CNF 可以在多项式时间内转换为 3-CNF ，因此 SAT 可以规约到 3-SAT，参考 16. Cook-Levin Theorem - YouTube）
Modern SAT solvers: fast, neat and underused (part 1 of N) — The Coding Nest