数理逻辑及其 python 实现:3
Notes on 「Mathematical logic through python」
三、更多逻辑运算符
上节 DNF 和 CNF 定理已经说明，给定任何语义需求，都可以通过 ~ & | 三种运算符来构造公式，从这个角度看，这三个运算符在语义表达上已经完备了。 那么就有两个问题，一是，是否还可以继续精简呢，比如是否可以只用一个 ~ 运算符？这显然是不行的，因为它缺乏组合能力，比如两个变量 p,q 如何用 ~ 连起来呢，因此只使用 ~ 不单不是语义完备，在语法上就不能构造出包含所有变量的公式。 那么 ~ 和 & 呢？这是本文讨论的
这是往少的方面想，也可以往多的方面想，既然 {~,&,|} 已经完备了，那么可以根据表达的方便性引入更多连接词，这些连接词可能有更直观地语义（比如异或是一种语义是否相同的比较），而分析性质或推理的时候把它们统一规约到 ~ & | 形式。那么就要考虑其他的连接词比如 -> 如何规约到 ~ & | 上的算法实现问题
T3.1 - T3.2 新的连接词的语义
引入更多二元运算符，需要修改判断函数以及 evaluate 函数，但在第 2 章已经对 evaluate 函数处理过了，因此这里只需补充二元运算的判断
def is_binary(string: str) -> bool:
return string in {"&", "|", "->", "+", "<->", "-&", "-|"}
二元运算符连接两个变量，因此真值表有 4 行，这四行可对应不同结果，因此共有 \( 2^{4} \) 种连接词。 问题是，为什么最常谈论的是 & | 和 -> ？
个人猜测这来自于集合论或者说是对类的概念的常用模式，对应集合的交集，并集和子集关系，也就是概念的组合（马和驴得到新的骡子），扩展（猫和老虎变成猫科）以及属于关系（人是动物）。
T3.3 扩充树：对叶子节点的变量替换
为了能够实现运算符的等价规约，本节引入了一个语法层面的规则，把命题中的变量名替换成其他名字或者其他公式。例如 p&p 替换成 q&q 或者 (p|q)&(p|q), 这是个树遍历算法，在遍历到叶子节点的变量后进行替换，并且替换完后直接返回，不会继续对替换后的子树继续递归，从而防止无限递归地替换（比如以下函数的 docstring 中的例子，p 替换后出现了 r, 而 r 替换后出现了 p, 如果允许继续替换则会无限递归）。
def substitute_variables(
self, substitution_map: Mapping[str, Formula]
) -> Formula:
"""
>>> Formula.parse('((p->p)|r)').substitute_variables(
... {'p': Formula.parse('(q&r)'), 'r': Formula.parse('p')})
(((q&r)->(q&r))|p)
"""
for variable in substitution_map:
assert is_variable(variable)
# Task 3.3
if is_variable(self.root) and self.root in substitution_map:
return substitution_map[self.root]
if is_binary(self.root):
first = self.first.substitute_variables(substitution_map)
second = self.second.substitute_variables(substitution_map)
return Formula(self.root, first, second)
elif is_unary(self.root):
first = self.first.substitute_variables(substitution_map)
return Formula(self.root, first)
return self
Formula.substitute_variables = substitute_variables
print(Formula.parse('((p->p)|r)').substitute_variables({'p': Formula.parse('(q&r)'), 'r': Formula.parse('p')}))
(((q&r)->(q&r))|p)
如果某个要被替换成 q 的变量 p 出现了多次，那么它们都会被替换成同一个 q, 因此从数据结构上看，替换后的结构不再是树，而是一个有向无环图，但由于 formula 对象是不可修改的，因此不会影响后续操作。
T3.4 替换树：对子树的操作符替换
在能够替换叶子节点后，考虑替换"更大"的操作对象，也就是对子树进行替换。
公式 p&q 在语义上等价于公式 ~((~p|~q)), p->q 语义上等价于 ~p|q, 等价公式之间的替换就是子树之间替换
替换表是如下格式，
{'&': Formula.parse('~(~p|~q)')}
字典里 value 部分中出现了 p 和 q 变量，它指代的是子树的左右节点，是一个占位符，或者用函数的视角，p,q 只是函数的形参。
实现中，遍历公式的语法树，找到待替换的运算符 & 后，根据其左右子树具体的值构建出 p 和 q 变量的替换表 {p:left_tree, q:right_three}，然后对 Formula('~(~p|~q)') 中的 p 和 q 应用上一节实现的叶子节点替换算法得到 & 表达式的具体子树，再用子树替换现有的 & 子树。
如果类比于编程语言，相当于遍历语法树，找到 &(left,right) 函数调用点，由于函数定义中形参是 p,q ，因此构建形参到实参的映射表 {p:left, q:right}, 称为环境绑定, 根据映射表对函数的内容 '~(~p|~q)' 进行替换，变成 ~(~left|~right), 然后把 &(left,right) 整个替换成具体的语句 ~(~left|~right) 。这几乎就是编译器中的 inline 优化（内联优化），或者宏展开
这里需要用到 substitute_variables, 采用后序遍历的思路，从叶子节点开始
def substitute_operators(
self, substitution_map: Mapping[str, Formula]
) -> Formula:
for operator in substitution_map:
assert (
is_constant(operator)
or is_unary(operator)
or is_binary(operator)
)
assert substitution_map[operator].variables().issubset({"p", "q"})
# Task 3.4
if is_constant(self.root):
if self.root in substitution_map:
return substitution_map[self.root]
return self
elif is_unary(self.root):
if self.root in substitution_map:
var_map = {
"p": self.first.substitute_operators(substitution_map)
}
return substitution_map[self.root].substitute_variables(
var_map
)
else:
return Formula(
self.root,
self.first.substitute_operators(substitution_map),
)
elif is_binary(self.root):
if self.root in substitution_map:
first = self.first.substitute_operators(substitution_map)
second = self.second.substitute_operators(substitution_map)
var_map = {"p": first, "q": second}
return substitution_map[self.root].substitute_variables(
var_map
)
else:
return Formula(
self.root,
self.first.substitute_operators(substitution_map),
self.second.substitute_operators(substitution_map),
)
elif is_variable(self.root):
return self
Formula.substitute_operators = substitute_operators
Formula.parse('((x&y)&~z)').substitute_operators({'&': Formula.parse('~(~p|~q)')})
~(~~(~x|~y)|~~z)
以上功能不单用于等价运算符之间的替换，它还使得公式拥有了实例化的能力，公式从此变成了模版，给定 p|q 我们可以替换出无穷个具体结论，比如 (x|y) ， ((x&y)|(x&y))。
注意：尽管以上算法都是 syntax 上的变化，但遵循的是语义等价获得的"合理"的规则，你也可以把 p|q 替换成 p&q, 但这在语义上是错误的，现实中有用的是 p->q 变成 ~p|q 这种语义等价形式的替换，所以纯语法的变换（AST 解析树的修剪）虽然是机械的，但并非无意义，它的意义一方面是维持了局部的语义等价，另一方面，这种等价有无数种，但选择朝哪个方向去等价是人类需求所赋予的，即它为什么选择这种变换而非另一种，是来自外部语义驱动的。
T3.5 - T3.6 逻辑连接词集合的完备性
Task 3.5 是对 substitute 的应用，由于运算符之间有语义等价性，例如以上提到的 p->q 等价于 ~p|q, 那么就可以不需要 -> 算子，只用 ~ 和 | ，这正式引出了逻辑连接词完备性的概念，以及寻找完备逻辑连接词集合的探索。
A set of logical operators is called complete if every Boolean function (of any arity) can be expressed using only the operators in the set.
definition 3.1 (Complete Set of Operators)
由于 DNF/CNF 表明 ~ & | 已经完备，于是以下实现中把大部分运算符（这里并没有全部列出来）转成 {~,&,|} 所表达的公式，比如把常量 T 转成 (p|~p), F 转成 (p&~p)…
def to_not_and_or(formula: Formula) -> Formula:
# Task 3.5
substitution_map =
{"F": Formula("&", Formula("p"),
Formula("~", Formula("p"))),
"T": Formula("|", Formula("p"),
Formula("~", Formula("p"))),
"+": Formula("&",
Formula("|",
Formula("p"),
Formula("q")),
Formula("|",
Formula("~", Formula("p")),
Formula("~", Formula("q")))),
"<->": Formula("|",
Formula("&",
Formula("p"),
Formula("q")),
Formula("&",
Formula("~", Formula("p")),
Formula("~", Formula("q")))),
"-&": Formula("~", Formula("&",
Formula("p"),
Formula("q"))),
"-|": Formula("~", Formula("|",
Formula("p"),
Formula("q"))),
"->": Formula("|", Formula("~", Formula("p")),
Formula("q"))
}
return formula.substitute_operators(substitution_map)
这个函数可以更好地进行规约，比如给定 (p->q), 一种做法是列出它的真值表，然后用上一节的 synthesize 函数合成 DNF 公式，这样就只包含 {~,|,&}, 但有了以上函数可以直接语法上替换，绕过遍历真值表这一步。
Task3.6 则是提到更多的完备运算符号集合 : {not, and}, {nand}, {not, or}, {imply, not}, {imply, False}.
首先对于 | 可以转成只包含 & 和 ~ 的公式：
def to_not_and(formula: Formula) -> Formula:
# Task 3.6a
substitution_map =
{
"|": Formula("~",
Formula("&",
Formula("~", Formula("p")),
Formula("~", Formula("q"))))
}
return to_not_and_or(formula).substitute_operators(substitution_map)
因此 {&,~} 是更小的语义表达上完备的运算符集合。
而 & 和 ~ 都可以转成 -&, 即 NAND 运算符：
def to_nand(formula: Formula) -> Formula:
# Task 3.6b
to_not_nand_map =
{
"&": Formula("~", Formula("-&", Formula("p"), Formula("q")))
}
substitution_map =
{
"~": Formula("-&", Formula("p"), Formula("p")),
}
return to_not_and(formula).substitute_operators(to_not_nand_map).substitute_operators(substitution_map)
因此最小的完备的运算符集合（之一）是 {NAND}, 以至于本书作者之一还开了另外一门 NAND2Teris 的课程。
也可以把 & 规约到 ~ 和 ->, 再把 ~ 规约到 -> 和常量 F:
def to_implies_not(formula: Formula) -> Formula:
# Task 3.6c
substitution_map =
{
"&": Formula("~", Formula("->", Formula("p"),
Formula("~", Formula("q"))))
}
return to_not_and(formula).substitute_operators(substitution_map)
def to_implies_false(formula: Formula) -> Formula:
# Task 3.6d
substitution_map =
{
"~": Formula("->", Formula("p"), Formula("F")),
}
return to_implies_not(formula).substitute_operators(substitution_map)
因此以下四个很小的运算符集合在语义表达上都是完备的（这不是全部，还有其他小集合也是完备的）：
The following four sets of operators are each (separately) a complete set of operators: a. The set containing only ‘~’ (not) and ‘&’ (and). b. The singleton set containing only ‘&’ (nand). c. The set containing only ‘→’ (implies) and ‘~’ (not). d. The set containing only ‘→’ (implies) and ‘F’ (False).
theorem 3.1
逻辑连接词集合的不完备性
书本 3.4 节比较偏理论了，证明哪些集合是不完备的，例如证明只有异或和等价两个算子是不完备的，这里要引入一些性质，比如仿射性质。课后思考是证明以下集合是不完备的， {→, F, &, |, ⊕, and mux} ；这部分需要巧思，和课程核心脉络关系不是很大，不多赘述。
The set of operators containing ‘T’, ‘F’, ‘~’ , ‘⊕’, and ‘↔’ is not complete. In particular it cannot represent the conjunction (“and”) function or the disjunction (“or”) function.
theorem 3.4