图、树与状态转移

文件依赖、友谊、道路与程序转移都能画成点与连线，但线的含义不同。依赖有方向，友谊可能对称，道路有成本，转移取决于完整状态。仅有好看的图并不能建立正确推论所需的数学模型。

本模块从有限图和明确约定开始：计算关联次数，证明树定理，解释遍历证书，排列先修依赖，检查有界重试协议。每个结果都声明保证与所需信息。这些思想随后用于计算图、图数据、有限自动机和依赖系统。

回忆检查：用有序对描述关系，区分不变式与终止，解释线性操作计数。按需复习模块 03、模块 04与模块 06。实验列表与字典表示有限对象，数学结论不依赖某种 Python 容器。

有限简单无向图包含有限顶点集 V，以及边集 E；每条边是 V 的二元子集。{u,v} 有两个不同端点，没有方向。简单表示无自环、无平行重复边。AB 与 BA 表示同一无序对，因此把它们作为两条边存储会重复计数。

有向图使用有序对 (u,v)，常写 u→v。u→v 不蕴涵 v→u。本模块例子排除自环和重复有序对，其他图约定可以允许。自环、重复边、带权边各有用途，但应用按端点或不同邻居计数的定理前，必须说明约定。

顶点是标签，不必是数字或位置。绘图坐标只是显示结构，交叉线不会自动产生顶点，除非已声明。移动点但保持 V,E 不变，图不变；删除孤立顶点却会改变 V，即使边未变。统计状态或报告不可达对象时，这一区别很重要。

无向顶点的度是关联边数，简单图中也等于邻居数。有向图的入度计进入边，出度计离开边。顶点可出度很高、入度为零，把两者混用会颠倒依赖。有向自环若允许，对入度与出度各贡献一。

游走是连续顶点间都有适当边的序列，长度为经过边数，比顶点序列长度少一。这里的路径指不重复顶点的游走。环闭合且除首尾外不重复顶点；按简单无向约定至少三条边。零长度路径只有一个顶点，证明该点从自身可达。

邻接列表存每个顶点的邻居，F 也要有空列表。无向边出现在两个列表；有向列表通常只存出邻居。这个区别影响解释与存储计数。排序邻居让实验跟踪可复现，但排序是实现选择，不是图的数学定义。

邻接矩阵使用声明的顶点顺序，Aᵢⱼ 在对应边存在时为一，否则零。简单无向矩阵对称、对角零，行和为度。有向出边约定下，行和是出度，列和是入度。没有行列标签的矩阵，其关系含义不明确。

v 点、e 边的列表占 O(v+e) 项，无向邻居关联为 2e。稠密矩阵即使多数零也有 v² 项。列表扫描邻居的工作随度变化，矩阵每行查 v 项；矩阵支持直接索引查边，普通未排序列表可能需逐项查。应按操作与稀疏程度选择表示，不能笼统说某种永远更快。

这里假设固定大小标签、恒成本索引，字典操作服从声明的实现模型，并非证明每次散列表查找都有确定常数最坏成本。可变长标签或巨大整数标识还会增加表示工作。与模块 06 一样，O(v+e) 属于成本模型，不能覆盖同一抽象图的任意编码。

有限无环边无向图有度数和恒等式 $\sum_{v\in V}\deg(v)=2|E|$。对同一关联集合双重计数：按顶点分组得到左边，按边分组每边两个端点得到右边。这是覆盖约定域的证明，不是由几个计算样例外推。若允许自环，每自环计两次关联仍保恒等式。

有向图中 $\sum_v\operatorname{outdeg}(v)=|E|$，$\sum_v\operatorname{indeg}(v)=|E|$，每边一个源与一个目标。两个和相加是 2|E|，单独一个是 e。这些是输入检查，不证明连通或无环；不同图可有同一度序列。

无向两点连通表示存在路径。允许游走得相同可达条件：有限游走若重复点，删除中间闭合段直到无重复。连通通过零路径自反，通过反向路径对称，通过拼接游走再删重复传递。因此它是等价关系，与模块 03 相接。

等价类称连通分量。例图有 {A,B,C,D,E} 与 {F} 两分量。所有顶点在一个分量中称连通；后面的树另要求非空。空图需另选约定，不在树定理域内。一个图可以既有环，又在其他部分不连通，本例即如此。

方向改变可达。u 可到 v，不一定 v 可回 u。强连通要求双向可达，其类是强连通分量；弱连通先忽略方向。单向链 A→B→C 弱连通，但三个点各成强连通分量。应用要有向可达时，不加限定的“连通”不够精确。

删除后增加分量数的边称桥。DE 是桥，删除会分离 E；AB 不是，因为仍可经 C,D 从 A 到 B。环上的无向边不是桥，因为其余环段提供替代路线。反过来，非桥的两端有替代路径，与该边组合成环。

环检测必须适合图类型。有向遍历遇到指向活动祖先的边，可给有向环见证。无向遍历中，父边反向出现是正常的，不是简单图的二边环。把每个已见邻居都报环的程序，若未正确处理父节点与发现状态，会连单独一条边也误判。

度恒等式只是必要检查，并不完全识别图。度和为偶的序列仍可能不实现为简单图，例如三点中某点度三不可能。e=v−1 单独也不能保证树；三角形加一个孤立点有四点三边，却既不连通又有环。

树是有限、非空、连通且无环的无向图。森林是无环无向图，可有多个分量，包括孤立点。有限森林每个连通分量都是树。单点零边图也是树：零路径给连通，且无环。声称覆盖所有正规模的证明必须含这一例。

树中任意两点恰有一条路径。连通给存在；若有不同路径，从第一次分离到再次会合，两段组成环。反过来，连通且端点路径唯一的图不可能有环，因为环上两段给所选端点两条不同路径。

至少两点的无根树中，叶子度一。为证明叶存在，选择最长路径；图有限，最长者存在。端点不能有路径外邻居，否则可延长；不能有路径上更远邻居，否则成环。故它只有下一点这一邻居。两个端点都是叶。

v 点、c 分量的森林按分量求和得 e=v−c。孤立点贡献一点零边，因此正确处理。空森林 v=e=c=0 也满足恒等式，虽按本定义不是树。这是逐分量应用定理，不是把非连通图直接代入树公式。

有根树选择根。根到顶点的路径决定每个非根的父节点，其余邻居为子节点。深度为从根计边距离，高度为最大深度，因此单节点高度零。其他书可能按点数计高度，对比公式要先看约定。选择根会改变深度、父节点，却不改无根树。

有根叶是没有子节点的点。至少两点时，度一根有一个子节点，所以不是有根叶，虽是无根叶。单节点根无子节点，是有根叶，但无根度零。先解决这些边界，再用模块 04 的满二叉树恒等式。

生成树使用连通图所有顶点与部分边。遍历发现父边形成生成树：每可达非根恰一父，父链回源，连接分量且无环。原图不连通时，遍历各分量得生成森林。从 A 搜索不能生成含 F 的生成树，因为不存在连接边。

边定理还说明最小性。树删任一边会失去连通，因为两端唯一道路用该边。有环连通图可删环边保持连通，反复删除最终得生成树，有限性保证过程终止。故连通图至少 v−1 边，连通简单图恰 v−1 边即为树。

广度优先搜索（BFS）用先进先出队列。标源已发现、距离零并入队。反复取队首，扫描出邻居；对未发现者立即标记，记父节点，赋当前距离加一，再入队。发现时标记保证每点只入队一次，即使多条前驱边指向它。

队列按非递减已赋距离处理。距离 d 点的新邻居赋 d+1，排在所有等待点之后，因此前沿逐边层推进。不变式含：每发现标记是具体父路径长度，已处理点全部出边已扫描。父路径提供最短距离的一个上界。

一般最短证明：假设某可达点存在比 BFS 标签短的路径。沿最短路选首个标签超过路径前缀长度的点，其前驱有正确较小标签，且在更大距离点前处理。扫描连接边会以不大于前缀长度发现下一点，或它已获这样的标签；都矛盾。因此发现的父路径边数最小。

返回的距离映射也可作为证书检查：源零；每个其他有标签点有合法父边、距离比父多一；每条从有标签 u 出发的边满足 d(v)≤d(u)+1，且所有后继都有标签。父链给报告长度的路径，沿任意源路径串联不等式则报告值不超过路径长度。两者合起来证明最优，无需重跑相同队列跟踪。

深度优先搜索（DFS）先递归探索未发现邻居，再回来处理下一邻居。发现序为前序，完成序为后序。按本列表字母序，递归前序 A,B,D,C,E，后序 C,E,D,B,A。它与 BFS 达到同一分量，但 DFS 到 C 的发现路径是 A,B,D,C，虽有边 AC。因此 DFS 父深度不一定最短距离。

DFS 的概念递归调用栈维护活动路径。有向边指向当前活动点会闭合有向环；指向已完成点则不证明环。区分未发现、活动、已完成状态：单个 visited 布尔值可用于可达性，却不足以支持所有环检测结论。调用栈或显式栈还需要随最大探索深度增长的内存。

邻接列表中，每发现点处理一次，每出邻居项扫描一次。遍历全部分量在声明模型下 O(v+e)；单源只扫描可达部分，另加若有的全局初始化。矩阵全遍历 O(v²)。Python deque 移除队首不移动剩余元素，反复 list.pop(0) 会增加简单队列模型未计工作。

BFS 最小化边数；每边有同一正常权时，也最小总成本。不等权时，一条成本十的边可能比两条各一的边差。普通 BFS 原样运行不最小化权和。带权最短算法需要其他假设与不变式，不能仅因都有前沿就借用无权证明。

有向无环图（DAG）不含有向环。这里 u→v 表示 u 必须先完成，其他应用可能存反向依赖查询；必须声明含义，不能由箭头风格猜。拓扑序把每点恰列一次，对每边 u→v 都使 u 在 v 前。

每有限非空 DAG 有入度零点。否则从任一点反复选入前驱，有限图不可能一直供不同点，重复就给有向环，矛盾。这说明初始点存在。无限向后链可能既无入度零点又无有限环，因此证明不自动覆盖无限图。

Kahn 算法反复选剩余入度零点、输出它，移其出边并减少相应剩余入度。不变式为已输出点满足已输出依赖，剩余入度恰计未输出前驱。所选点无未完成前驱。删点保持 DAG，零入度引理使过程持续直到全部输出。

若还有点但无零入度者，前驱论证证明剩余图有环。阻塞集合也可含环下游点，并非精确环点列表。加 D→A 后，B 可处理，A,C,D,E 阻塞；E 因 C 未完成而阻塞，却不在任何有向环上。环证书要实际闭合边序列，如 A,C,D,A。

拓扑序不一定唯一。队列按插入顺序选就绪点，实验堆按字母打破平局。可复现也有成本：堆入出带对数因子，不能称为普通队列 O(v+e) 实现。验证拓扑序要先检查它是 V 的排列，再逐边查 position(u)<position(v)。遗漏孤立点会违反排列条件。

拓扑序支持依赖归纳。若 v 的值只从已完成前驱算，先证明零入度点性质，再在处理 v 时假设各前驱性质并证明更新保持。这是按有效序位置的普通归纳，边说明哪些较早假设可用，支撑无环计算图与动态规划。

简单调度给任务非负固定时长、无限并行工作人员。最早完成为自身时长加前驱完成最大值，无前驱最大值取零。本 DAG 时长 A=2,B=5,C=3,D=4,E=1，完成时间 2,5,8,12,9，总完工十二。时长和十五是串行工作总量，不是无限并行完工时间。

递推假设依赖完成立即开工、时长固定、资源不冲突。一个工作者、内存限制、共享设备或不确定时长时，结果不一定可实现。DAG 只建模先后约束，不包含所有调度限制。明确假设才能迁移到构建系统或 AI 计算而不承诺不现实吞吐。

状态转移系统指定状态集 S、初始状态与有向转移关系。事件标允许变化，但状态必须含决定合法后继的信息。相同控制位置可因计数或标志不同而有不同未来。模型顶点是完整状态，不只是当前执行代码行。

双控制状态重试协议使用 idle 与 waiting，发送使 idle→waiting，确认使 waiting→idle。为讨论有界实现，还记发送次数与是否看到确认，这是乘积状态元组。两个控制值、零到二计数、两标志值给十二个潜在元组，按规则只有部分可达。

探索有限模型从初始点用 BFS 或 DFS，生成恰好声明的后继，visited 存完整元组，新发现点存父事件。BFS 首次到坏状态给最少转移数反例。跟踪必须给允许事件序列与违反状态，仅报断言失败缺少修复证据。

安全谓词 I 的归纳不变式证明检查所有初始态满足 I，以及任意 I 态的允许转移保持 I。按有限执行长度归纳，可证明所有可达态，包括任意长执行。穷尽检查则计算可达集合并逐态测 I；完整有限模型中可判定该模型的可达安全。符号不变式可能覆盖更大或无界系统。

实验错误模型六个可达态，其中一个不安全；修复模型五个。(idle,2,false) 仍属于环境乘积域，是因修复规则不可达，不是元组语法不可能。不可达元组违反 I 不影响可达安全。若它们让归纳的转移保持义务失败，可以加强 I 排除相关元组。

安全性说禁止事件或状态从不发生，活性问期望事件最终发生。修复的超时自环安全，却允许无限等待、从不确认。有限可达检查与无坏状态均不能建立最终送达。活性需额外环境假设，例如合理且有依据的公平性条件，再证明这些假设带来进展。

穷尽程度取决于模型完整性。本模型至多两次发送、单请求、无取消、无迟到消息或并发。检查这些状态不证明无限重试网络实现正确。省略计数会合并合法重试不同的情形，省略消息内容可能隐藏确认错收件人。抽象需要自己说明代表哪些真实行为。

组合状态分量会迅速增大潜在域。标志、计数、进程数量在生成转移前就相乘。小教学模型的可达搜索可行，真实软件可能昂贵。有界测试提供有用反例或精确范围的已检查结论，更广结论需要证明、可靠抽象或其他分析。

脚本仅用 Python 标准库，本地无 GPU。先预测图事实与见证。下载脚本与产生显示输出的执行源完全相同。

实验 A 列表、矩阵与错误图输入

预测：写 F 列表与矩阵行，算度和。运行：查看两表示，并拒绝自环、重复无向边、未知顶点。解释：为何 AB,BA 重复，而全零 F 行必须保留。修改：删 AC，预测消失的环，更新边数检查后重跑。

下载 lab1_representations.py

"""Represent one finite simple undirected graph, including an isolated vertex."""
VERTICES = tuple("ABCDEF")
EDGES = ("AB", "AC", "BD", "CD", "DE")

def build_graph(vertices, edges):
    graph = {v: [] for v in vertices}
    seen = set()
    for u, v in edges:
        if u not in graph or v not in graph or u == v:
            raise ValueError("Edges need two distinct declared vertices")
        key = frozenset((u, v))
        if key in seen:
            raise ValueError("Repeated undirected edge")
        seen.add(key)
        graph[u].append(v)
        graph[v].append(u)
    return {v: sorted(neighbours) for v, neighbours in graph.items()}

graph = build_graph(VERTICES, EDGES)
matrix = [[int(v in graph[u]) for v in VERTICES] for u in VERTICES]
print("Adjacency lists:", graph)
print("Matrix order:", " ".join(VERTICES))
for v, row in zip(VERTICES, matrix):
    print(v, " ".join(map(str, row)))
degrees = [len(graph[v]) for v in VERTICES]
assert sum(degrees) == 2 * len(EDGES)
assert all(matrix[i][j] == matrix[j][i] for i in range(6) for j in range(6))
print("Degrees:", degrees, "; sum =", sum(degrees), "; 2|E| =", 2 * len(EDGES))
print("Isolated vertices:", [v for v in VERTICES if not graph[v]])
for label, edges in [("loop", ("AA",)), ("duplicate", ("AB", "BA")), ("unknown", ("AZ",))]:
    try:
        build_graph(VERTICES, edges)
    except ValueError as error:
        print("Rejected", label + ":", error)

Adjacency lists: {'A': ['B', 'C'], 'B': ['A', 'D'], 'C': ['A', 'D'], 'D': ['B', 'C', 'E'], 'E': ['D'], 'F': []}
Matrix order: A B C D E F
A 0 1 1 0 0 0
B 1 0 0 1 0 0
C 1 0 0 1 0 0
D 0 1 1 0 1 0
E 0 0 0 1 0 0
F 0 0 0 0 0 0
Degrees: [2, 2, 2, 3, 1, 0] ; sum = 10 ; 2|E| = 10
Isolated vertices: ['F']
Rejected loop: Edges need two distinct declared vertices
Rejected duplicate: Repeated undirected edge
Rejected unknown: Edges need two distinct declared vertices

实验 B 遍历与拓扑证书

预测：A 源 BFS 距离、递归 DFS 前序、有效依赖序。运行：读父节点与局部距离不等式断言。解释：为何 C 的 DFS 父路可长于 BFS，E 可阻塞却不在环。修改：逆邻居顺序，区分变动父选择与不变最短距离。堆按字母选就绪点，另有开销。

下载 lab2_traversals.py

"""Deterministic traversal certificates and dependency orders, not weighted paths."""
from collections import deque
from heapq import heapify, heappop, heappush

GRAPH = {"A": ["B", "C"], "B": ["A", "D"], "C": ["A", "D"],
         "D": ["B", "C", "E"], "E": ["D"], "F": []}

def bfs(graph, source):
    distance, parent, order = {source: 0}, {source: None}, []
    queue = deque([source])
    while queue:
        u = queue.popleft()
        order.append(u)
        for v in graph[u]:
            if v not in distance:  # Mark at discovery, before queueing.
                distance[v], parent[v] = distance[u] + 1, u
                queue.append(v)
    return order, distance, parent

def dfs(graph, source):
    seen, preorder, postorder = set(), [], []
    def visit(u):
        seen.add(u)
        preorder.append(u)
        for v in graph[u]:
            if v not in seen:
                visit(v)
        postorder.append(u)
    visit(source)
    return preorder, postorder

def topological(graph):
    indegree = dict.fromkeys(graph, 0)
    for neighbours in graph.values():
        for v in neighbours:
            indegree[v] += 1
    ready = [v for v in graph if indegree[v] == 0]
    heapify(ready)  # Alphabetic tie-breaking, with heap overhead.
    order = []
    while ready:
        u = heappop(ready)
        order.append(u)
        for v in graph[u]:
            indegree[v] -= 1
            if indegree[v] == 0:
                heappush(ready, v)
    return order, sorted(v for v in graph if indegree[v] > 0)

order, distance, parent = bfs(GRAPH, "A")
assert distance == {"A": 0, "B": 1, "C": 1, "D": 2, "E": 3}
for u, neighbours in GRAPH.items():
    if u in distance:
        for v in neighbours:
            assert v in distance and distance[v] <= distance[u] + 1
for v, p in parent.items():
    if p is not None:
        assert v in GRAPH[p] and distance[v] == distance[p] + 1
print("BFS order:", order)
print("Distances:", distance, "; F is unreachable")
print("Parents:", parent)
print("DFS preorder/postorder:", dfs(GRAPH, "A"))
dag = {"A": ["C"], "B": ["C"], "C": ["D", "E"], "D": [], "E": []}
order, blocked = topological(dag)
position = {v: i for i, v in enumerate(order)}
assert not blocked and all(position[u] < position[v] for u in dag for v in dag[u])
print("DAG topological order:", order)
cyclic = {v: neighbours[:] for v, neighbours in dag.items()}
cyclic["D"].append("A")
print("After adding D->A, processed/blocked:", topological(cyclic))
cycle = ["A", "C", "D", "A"]
assert all(v in cyclic[u] for u, v in zip(cycle, cycle[1:]))
print("Cycle witness:", " -> ".join(cycle))
print("Weighted trap: direct A->E costs 10; A->B->E costs 2. Fewest edges is not cheapest.")

BFS order: ['A', 'B', 'C', 'D', 'E']
Distances: {'A': 0, 'B': 1, 'C': 1, 'D': 2, 'E': 3} ; F is unreachable
Parents: {'A': None, 'B': 'A', 'C': 'A', 'D': 'B', 'E': 'D'}
DFS preorder/postorder: (['A', 'B', 'D', 'C', 'E'], ['C', 'E', 'D', 'B', 'A'])
DAG topological order: ['A', 'B', 'C', 'D', 'E']
After adding D->A, processed/blocked: (['B'], ['A', 'C', 'D', 'E'])
Cycle witness: A -> C -> D -> A
Weighted trap: direct A->E costs 10; A->B->E costs 2. Fewest edges is not cheapest.

实验 C 有界协议修复

预测：send,retry,timeout 后评安全谓词。运行：比较错误与修复可达态。解释：五态结论范围，以及无限超时执行。修改：允许第三次发送，一致扩计数域与后继规则，再检查相同修复。不能把此玩具模型说成已验证的网络协议。

下载 lab3_protocol.py

"""Exhaustively explore a deliberately bounded, two-control-state retry model."""
from collections import deque

START = ("idle", 0, False)  # control, number of sends, acknowledgement seen

def successors(state, faulty):
    mode, count, ack = state
    if mode == "idle" and count == 0 and not ack:
        yield "send", ("waiting", 1, False)
    if mode == "waiting":
        if count < 2:
            yield "retry", ("waiting", count + 1, ack)
        yield "ack", ("idle", count, True)
        if count == 2:
            yield "timeout", ("idle", count, ack) if faulty else state

def safe(state):
    mode, count, ack = state
    return mode != "idle" or count == 0 or ack

def explore(faulty):
    queue, paths = deque([START]), {START: []}
    while queue:
        state = queue.popleft()
        for event, target in successors(state, faulty):
            if target not in paths:
                paths[target] = paths[state] + [event]
                queue.append(target)
    return paths

for faulty in (True, False):
    paths = explore(faulty)
    bad = [(state, path) for state, path in paths.items() if not safe(state)]
    print("faulty =", faulty, "; reachable =", len(paths), "; unsafe =", len(bad))
    for state, path in bad:
        print("Witness:", " -> ".join(path), "; state =", state)
    assert bool(bad) == faulty
    if not faulty:
        assert len(paths) == 5 and ("idle", 2, False) not in paths
print("Repair: timeout stays waiting; safety does not guarantee acknowledgement or termination.")
print("Scope: two sends maximum, no cancellation, one request, no delayed messages or concurrency.")

faulty = True ; reachable = 6 ; unsafe = 1
Witness: send -> retry -> timeout ; state = ('idle', 2, False)
faulty = False ; reachable = 5 ; unsafe = 0
Repair: timeout stays waiting; safety does not guarantee acknowledgement or termination.
Scope: two sends maximum, no cancellation, one request, no delayed messages or concurrency.

1–12 必做，13–14 扩展。按声明图约定证明，环见证要实际边序列。

自动分数覆盖 1–9，10 书面自评。两活动要求的证据类型不同。

用 MIT Mathematics for Computer Science 的图、树、状态机选段。用 MIT 握手、连通与树讲义 比约定。在 MIT 6.006 讲义 读 BFS、DFS 与拓扑排序。这些是外部一手阅读，本课与必做练习原创。

阅读用于比较定义与论证。先协调路径、叶、高度约定差异，再迁移公式。

不看笔记定义本课树、证边数、描述 BFS 发现规则，给有效拓扑序与环见证。解释最少边证书不优化任意权，为何安全有限协议不一定最终送达。

结业任务：加孤立 G，给新度和与分量数，解释 A 距离不变及全图生成森林。遍历森林有七点三分量，故四条发现边。原图仍五边、度和十，非森林环边不属于发现边。

前进标准：可区分抽象图、表示、遍历见证与正确性结论范围。离散分支下一步学模运算与可逆性，见课程总览了解可用课程。