数理逻辑及其 python 实现:3
Notes on 「Mathematical logic through python」
三、更多逻辑运算符
本节引入更多的算子，或者讨论删除算子后对公式的语义表达能力是否减弱的问题
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), 这是个树遍历算法，只有在找到叶子节点的变量才会进行真正的替换，并且替换完后直接返回，不会继续对替换后的子树继续递归，从而防止无限递归地替换（比如以上例子中，p 替换后出现了 r, 而 r 替换后出现了 p, 如果允许继续替换则会无限递归）。
另外如果某个要被替换成 q 的变量 p 出现了多次，那么它们都会被替换成同一个 q, 因此从数据结构上看，替换后的结构不再是树，而是一个有向无环图，但由于 formula 对象是不可修改的，因此不会影响后续操作。
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)
T3.4 替换树：对子树的操作符替换
在能够替换叶子节点后，考虑替换"更大"的操作对象，也就是对子树进行替换。替换子树的原因是，许多算子是可以用其他算子代替的，例如公式 p&q 在语义上等价于公式 ~((~p|~q)), p->q 语义上等价于 ~p|q, 等价公式之间的替换就是子树之间替换
注意，这种替换提供了把公式缩减的手段（也可以增大），这是变量替换无法做到的。
替换表是如下格式，可以看到，字典里 value 部分中出现了 p 和 q 变量，它指代的是子树的左右节点，因此对于这类问题，我们需要在找到待替换的运算符 & 后，根据其左右子树具体的值构建出 p 和 q 变量的替换表，然后把 '~(~p|~q)' 中的 p 和 q 应用上一节实现的叶子节点替换算法，再把结果表达式去替换整个子树。
这里需要用到 substitute_variables, 采用后序遍历的思路，从叶子节点开始
{'&': Formula.parse('~(~p|~q)')}
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 我们可以替换出无穷个具体结论。
注意：尽管以上算法都是 syntax 上的变化，但我们使用的都是通过语义等价获得的"合理"的规则，比如我们可以把 p|q 替换成 p&q, 但这在语义上是错误的，因此讨论它并没有什么太多意义，我们更关心的是 p->q 变成 ~p|q 这种语义等价形式的替换
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)
本节核心就是构造替换映射表：
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)
Task3.6 则是提到更多的完备运算符号集合 : {not, and}, {nand}, {not, or}, {imply, not}, {imply, False}.
结论是，最小的完备的运算符集合（之一）是 {NAND}, 以至于本书作者之一还开了另外一门 NAND2Teris 的课程
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
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)
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)
其他完备集合：
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)
逻辑连接词集合的不完备性
书本 3.4 节比较偏理论了，证明哪些集合是不完备的，例如证明只有异或和等价两个算子是不完备的，这里要引入一些性质，比如仿射性质。
课后思考是，证明以下集合是不完备的， {→, F, &, |, ⊕, and mux}
这部分需要巧思，感觉和课程核心脉络关系不是很大。
最后总结，本章核心在于引入了公式替换和以及第一种 "完备性" 的定义，后者表明的是替换规则的完备性（与后文整个逻辑系统完备性不一样）。
替换规则是什么呢？
每个连接符集合（连同 p,q 变量作为 placeholder, 例如 {->} 集合应该写成 {p->q}）可以看作初始公式（类比于公理），如果给出的集合里命题都是真的，比如 {p->p, p|~p, T} 那么通过替换规则构造出的所有表达式都会是真的，这是替换规则的可靠性（soundness），目前为止几乎没有提到要证明替换规则 的 soundness 这会在后文证明推理规则的 soundness 一起进行（T5.1），
不过在此想要说明的是逻辑系统中有两类很不一样的生成新对象的规则 – 替换和生成。
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