数理逻辑及其 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)
这里介绍的模型是与命题的变量绑定的（而与公式本身无关），是给变量的一组赋值，有多少变量，模型中就需要给多少变量进行赋值，并且只能赋真或者假，因此可以把模型看作是从变量到真值的映射函数，在 python 中表示就是一个变量名到真值的字典：
from typing import AbstractSet, Iterable, Iterator, Mapping, Sequence, Tuple
Model = Mapping[str, bool]
以上用 typing 中 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 是给定公式和模型计算其真值
- 本节里的函数是给定一个模型，构造出一个在该模型下为真的公式
这个过程类似建模，给定数据，构造一个能够拟合这些数据的函数，由于这种函数可能不止一个，因此我们需要对函数的形式再进行限制，使得能够根据数据，在找出唯一的符合某个形式的函数，本节选择的就是 conjunctive clause 形式，也就是只通过 & 来连接变量或者变量的否定的式子。
一个类比是，给定平面上两个点，找出能够穿过这些点的函数，如果不做规范，这种函数有无穷个，因此我们可以限制只能用直线函数拟合，这样找到的方程就是唯一的了。
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&q&r 形式，那么这个算法写起来很简单：
var_list = [k if v else "~" + k for k, v in model.items()]
return Formula.parse("&".join(var_list))
其描述是：对于模型中任何为 True 的变量，使用该变量的原始形式，否则使用它的否定形式
为什么以上方法构造出的 conjunctive clause 能够保证唯一性？为什么 & 和 ~ 有这种魔力？
因为这种公式的真值表中只有一行是 True, 并且直接与变量前是否有否定符号一一对应：
如果公式中存在 ~q, 那么整个式子要为为 True, q 一定是 True. 这在于 & 操作的"选择性", 任何只有 & 作为二元连接符号的公式，其输出空间里只有唯一的一个 True，& 具有一种逆向工程友好性，甚至有点像 one-hot 编码
所以在 conjunctive clause 式子的范围内，语义到语法的映射是唯一的（不考虑顺序，或者把变量按字典序排列）
接着由于表达式是允许有多个 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 的模型，但在 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 + 2x + 1 \) 分解为因式 \( (x+1)^2 \)，CNF 形式将复杂的逻辑表达式分解为更简单的部分，使得处理更加高效和明确。
- 解耦和局部化：复杂的逻辑表达式解耦为多个独立的子句，每个子句可以独立分析和处理。 通过这种局部化处理，可以有效减少整体问题的复杂度。
- 例如，当要检查 (p|~r)&(~p|~q) 的语义时，一旦检查到 p 为真，第一个子句就为真， ~r 不需要检查了，而一旦知道 (~p|~q) 为假，那么整个式子就为假，也就不需要继续检查了。
- 这种局部分解，使得可以用搜索的方式来做语义检查，即对通过局部检查不断逼近最终结果 （也可能涉及回溯），从而可以把公式的语义检查放在同意的搜索场景下看待。
- 这种分解或解耦和可能失去一些全局信息，因此会用启发式方法，启发公式往往就是用与目标直接有关的公式 来提供一种全局信息作为搜索中的引导。
下一节就是一个具体的例子，可以把其他搜索问题（约束满足问题）看作对 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