计算模型：语言、机器与逻辑

运行一个完整示例 · 01

找到区分两个 DFA 的最短单词

两位同学制作文本过滤器：一个接受任意位置含 ab 的单词，另一个只接受以 ab 结尾的单词。ab 和 aab 的测试都通过，于是他们以为两个过滤器等价。米娜不再猜测试字符串，而是同时运行两个自动机，搜索恰好只有一个接受的状态对。最终找到 aba，直接说明二者为何不同。

from collections import deque
from itertools import product

def witness(a, accepting_a, b, accepting_b):
    alphabet = ("a", "b")
    start = (0, 0)
    parents = {start: None}
    queue = deque([start])
    while queue:
        pair = queue.popleft()
        x, y = pair
        if (x in accepting_a) != (y in accepting_b):
            letters = []
            while parents[pair] is not None:
                previous, letter = parents[pair]
                letters.append(letter)
                pair = previous
            return "".join(reversed(letters))
        for letter in alphabet:
            nxt = (a[x][letter], b[y][letter])
            if nxt not in parents:
                parents[nxt] = (pair, letter)
                queue.append(nxt)
    return None

def accepts(table, word):
    state = 0
    for letter in word:
        state = table[state][letter]
    return state == 2

contains = [{"a": 1, "b": 0}, {"a": 1, "b": 2}, {"a": 2, "b": 2}]
ends = [{"a": 1, "b": 0}, {"a": 1, "b": 2}, {"a": 1, "b": 0}]
word = witness(contains, {2}, ends, {2})
assert word == "aba" and witness(contains, {2}, contains, {2}) is None
for size in range(len(word)):
    for letters in product("ab", repeat=size):
        test = "".join(letters)
        assert accepts(contains, test) == accepts(ends, test)
print("shortest witness:", repr(word))
print("contains ab:", accepts(contains, word))
print("ends in ab:", accepts(ends, word))

python regular-decision-problems-shortest-dfa-counterexample.py

shortest witness: 'aba'
contains ab: True
ends in ab: False

按执行顺序理解

1. 乘积状态 (x,y) 记录两个自动机读完同一前缀后的状态。

2. 状态对入队时标记；图中最多有 |Q_A|×|Q_B| 个状态对。

3. 恰好一个分量接受时，将乘积状态视为目标。这是对称差，而非交集。

4. 用父指针恢复字符串。BFS 保证首次找到的反例按符号数最短。

逐步读懂代码

两个语言不同，当且仅当对称差非空：L(A)≠L(B) 等价于存在 w，使 accept_A(w) 与 accept_B(w) 恰好一真一假。完整乘积搜索可以判定给定有限自动机的这一条件。若找不到可达的分歧状态对，任何单词都会到达判断一致的状态对。

状态数分别为 q_A、q_B，字母表大小为 s 时，时间为 O(s×q_A×q_B)，存储状态需要 O(q_A×q_B) 空间。自动机必须完整：每个状态对每个字母都有转移。缺失转移应先补到明确的拒绝汇点。

若初始状态就有分歧，返回空字符串也是合法反例。None 才表示不存在反例。这里的小规模穷举检查核实样例中没有更短反例；乘积状态的访问论证解释一般搜索为何终止。本方法比较 DFA，不能用于判定任意程序等价。

运行一个完整示例 · 01

数清语法树，不要默认只有一种解析

计算器接受 n+n+n+n。米娜先合并第一对操作数，朋友却先合并最后一对。两种做法都符合 E→E+E | n。字符串合法，但结构并不唯一。米娜枚举根节点的所有切分，再组合左右子树，最终找到五棵树，也理解了解析器为什么需要结合性规则。

from functools import lru_cache

def count_trees(operands):
    if operands < 1:
        raise ValueError("at least one operand required")
    ways = [0] * (operands + 1)
    ways[1] = 1
    for size in range(2, operands + 1):
        ways[size] = sum(ways[left] * ways[size - left]
                         for left in range(1, size))
    return ways[operands]

@lru_cache(None)
def trees(operands):
    if operands == 1:
        return ("n",)
    return tuple(f"({left}+{right})"
                 for cut in range(1, operands)
                 for left in trees(cut)
                 for right in trees(operands - cut))

assert [count_trees(n) for n in range(1, 6)] == [1, 1, 2, 5, 14]
assert len(set(trees(4))) == count_trees(4)
print("four operands:", count_trees(4), "parse trees")
for tree in trees(4):
    print(tree)

python parse-trees-ambiguity-count-expression-trees.py

four operands: 5 parse trees
(n+(n+(n+n)))
(n+((n+n)+n))
((n+n)+(n+n))
((n+(n+n))+n)
(((n+n)+n)+n)

按执行顺序理解

1. 一个操作数对应一棵叶子树，基础值是一，不是零。

2. 根在 left 个操作数之后切分时，左右树数量相乘，每对左右树构成一棵树。

3. 对不同根切分求和；根的划分不同，不会得到同一棵有序树。

4. 只枚举四个操作数用于展示。计数与实际生成全部树，输出成本差别很大。

逐步读懂代码

设 T(m) 表示 m 个相同操作数词元用加号连接时的语法树数量。T(1)=1，T(m)=对 k=1 到 m-1 求和 T(k)×T(m-k)。k 表示左子树的叶子数量。m=4 时，三种根切分分别贡献 1×2、1×1、2×1，总数为 5。

计数器需要 O(m²) 次算术操作，并保存 O(m) 个整数。大计数需要大整数，因此这里没有声称任意大 m 下算术仍是常数成本。枚举所有树至少要花费与输出字符数相关的时间，增长快得多。

算出的数值相同，不表示文法无歧义。歧义指同一词元字符串具有多棵语法树。对这个简单语言，E→E+n | n 可以规定左结合。本例假定已经分词且只有加号，并未实现词法分析、其他运算符优先级或通用文法解析器。

运行一个完整示例 · 01

找出全部反模型

穷举两个布尔原子，检查 p→q 是否推出 p∨q。

from itertools import product

rows = []
for p, q in product([False, True], repeat=2):
    premise = (not p) or q
    conclusion = q or p
    if premise and not conclusion:
        rows.append((p, q))
print("Countermodels:", rows)
assert rows == [(False, False)]

python logical-consequence-entailment-countermodels.py

Countermodels: [(False, False)]

按执行顺序理解

1. 枚举（假，假）、（假，真）、（真，假）、（真，真）。

2. 在（假，假）下蕴含真，而 p∨q 假。

3. 其他三行都不是反模型；保存的一个值对足以推翻后承。

逐步读懂代码

product 生成 p 与 q 的全部四种组合。for 循环把每对值分别赋给两个变量。Python 的 not 表示否定，or 表示包含“两者都真”的析取，因此 (not p) or q 表示蕴含。

if 只保留前提真而结论假的行。append 把该值对加到列表，print 显示完成的列表，assert 检查预期结果。这个有限穷举只检验此推理；原子更多时所需行也更多。

运行一个完整示例 · 01

在有限模型中寻找见证与反例

社团的每个学生都有导师。米娜听完，以为存在一位导师指导所有学生。一个小表就推翻了这个想法：Ana、Cy 跟 Ivy，Bo 跟 Noah。每个学生都有人指导，却没有一个导师覆盖三人。米娜用嵌套循环把两个量词的顺序具体展示出来。

students = ["Ana", "Bo", "Cy"]
mentors = ["Ivy", "Noah"]
relation = {("Ana", "Ivy"), ("Bo", "Noah"), ("Cy", "Ivy")}

def inspect(students, mentors, relation):
    witnesses = {x: [y for y in mentors if (x, y) in relation] for x in students}
    every_has_someone = all(witnesses[x] for x in students)
    shared = [y for y in mentors if all((x, y) in relation for x in students)]
    uncovered = [x for x in students if all((x, y) not in relation for y in mentors)]
    assert bool(uncovered) == (not every_has_someone)
    return witnesses, every_has_someone, shared, uncovered

witnesses, every, shared, uncovered = inspect(students, mentors, relation)
print("witnesses:", witnesses)
print("every student has a mentor:", every)
print("one mentor for everybody:", bool(shared))
assert every and not shared
broken = relation - {("Bo", "Noah")}
print("counterexample after removal:", inspect(students, mentors, broken)[3])
assert inspect([], mentors, relation)[1] is True
assert inspect(students, [], relation)[1] is False

python predicate-logic-finite-witness-search.py

witnesses: {'Ana': ['Ivy'], 'Bo': ['Noah'], 'Cy': ['Ivy']}
every student has a mentor: True
one mentor for everybody: False
counterexample after removal: ['Bo']

按执行顺序理解

1. 为每位学生建立见证列表；内层存在量词可以为不同外层学生选择不同导师。

2. 寻找共同导师时反过来：先选一个导师，再要求他覆盖每位学生。

3. 若某学生对所有候选导师都不满足关系，他就是未被覆盖者；这会构造否定命题的见证，而不只是打印 False。

4. 检查空集合情形。没有学生时全称命题为真；有学生却没有导师时，原命题为假。

逐步读懂代码

设 S 为学生集合、M 为导师集合，R(x,y) 表示 y 指导 x。第一个命题是“对每个 x∈S，存在 y∈M，使 R(x,y)”；第二个是“存在 y∈M，对每个 x∈S 都有 R(x,y)”。共同见证能证明第二个，进而证明第一个；各自的见证只能证明第一个。

否定第一个命题得到：“存在 x∈S，使每个 y∈M 都不满足 R(x,y)”。删掉 Bo–Noah 后，Bo 就成为这个反例。|S| 名学生、|M| 名导师的直接检查需要 O(|S||M|) 次关系查询，这里假定集合查询平均 O(1)。

程序检查的是一个指定的有限解释。在一张表上成立，并不证明公式在所有解释中都有效，也不能解决任意一阶逻辑有效性。论域假设应写在题目中，不能遇到不想要的结果后再临时改变空集规则。