22.3 深度优先搜索 深度优先搜索所使用的策略就像其名字所隐含的:只要可能，就在图中尽量“深入”。深度优先搜索总是对最近才发现的结点v的出发边进行探索，直到该结点的所有出发边都被发现为止。一旦结点v的所有出发边都被发现，搜索则“回溯”到v的前驱结点(v是经过该结点才被发现的)，来搜索该前驱结点的出发边。该过程一直持续到从源结点可以达到的所有结点都被发现为止。如果还存在尚未发现的结点，则深度优先搜索将从这些未被发现的结点中任选一个作为新的源结点，并重复同样的搜索过程。该算法重复整个过程，直到图中的所有结点都被发现为止。 前驱子图 深度优先树 深度优先森林 树边  发现 完成  时间戳   DF...

22.2 广度优先搜索 广度优先搜索   发现  前驱 父节点   BFS(G,s) for each vertx u ∈ G.V - {s} u.color = WHITE u.d = ∞ u.Π = NIL s.color = GRAY s.d = 0 s.Π = NIL Q = Ø ENQUEUE(Q,s) while Q ≠ Ø u = DEQUEUE(Q) for each v ∈ G.Adj[u] if v.color == WHITE v.color = GRAY v.d = u.d + 1 v.Π = u ENQUEUE(Q,v) u. color = BLACK  图 22-...

本章将介绍图的表示和图的搜索。图的搜索指的是系统化地跟随图中的边来访问图中的每个结点。图搜索算法可以用来发现图的结构。许多的图算法在一开始都会先通过搜索来获得图的结构，其他的一些图算法则是对基本的搜索加以优化。可以说，图的搜系技巧是整个图算法领域的核心。  22.1节对图的两种最常见的计算机表示法进行讨论。这两种表示法分别是邻接链表和邻接矩阵。 22.2节讲解一种简单的图搜索算法，称为广度优先搜索，并演示如何创建一棵广度优先树。 22.3节讲解深度优先搜索，同时对此种搜索所访问的结点之间的次序进行讨论，并对这方面的一些标准结果进行证明。 22.4节给出深度优先搜索的一个实际应用有向无环图中的拓...

26.2 Ford-Fulkerson方法 本节讨论用来解决最大流问题的Ford-Fulkerson方法。之所以称其为“方法”而不是“算法”，是因为它包含了几种运行时间各不相同的具体实现。Ford-Fulkerson方法依赖于三种重要思想，它们与许多的流算法和问题有关，如残存网络、增广路径和切割。这些思想是最大流最小切割定理(定理26.6)的精髓，该定理以流网络的切割来表述最大流的值。在本节的末尾，我们将给出Ford-Fulkerson方法的一种具体实现，并分析其运行时间。 Ford-Fulkerson方法循环增加流的值。在开始的时候，对于所有的结点u，v∈V，f(u，v)=0,给出的初始流值...

正如可以通过将道路交通图模型化为有向图来找到从一个城市到另一个城市之间的最短路径，我们也可以将一个有向图看做是一个“流网络”并使用它来回答关于物料流动方面的问题。设想一种物料从产生它的源结点经过一个系统，流向消耗该物料的汇点这样一个过程。源结点以某种稳定的速率生成物料，汇点则以同样的速率消耗物料。从直观上看，物料在系统中任何一个点上的“流量”就是物料移动的速率。这种流网络可以用来建模很多实际问题，包括液体在管道中的流动、装配线上部件的流动、电网中电流的流动和通信网络中信息的流动。 我们可以把流网络中每条有向边看做是物料的一个流通通道。每条通道有限定的容量，是物料流经该通道时的最大速率，如一条管...

自反传递闭包 Reflexive, Transitive Closure 关系R的自反传递闭包是包含R的最小关系，它既是自反的又是传递的。形式上，在Coq标准库的关系模块中定义如下： Inductive clos_refl_trans {A: Type} (R: relation A) Inductive clos_refl_trans {A: Type} (R: relation A) : relation A := | rt_step x y (H : R x y) : clos_refl_trans R x y | rt_refl x : clos_refl_trans R x x | ...

基本性质 Basic Properties 任何人都知道，上过离散数学本科课程的人，一般来说，关于关系有很多话要说，包括对关系进行分类的方法（如自反、传递等），关于某些类型的关系可以一般证明的定理，从一个关系到另一个关系的构造，等等。例如。。。 偏函数 Partial Functions 集合X上的关系R是一个偏函数，如果对于每个X，至多有一个y，使得 R x y ——即R x y1和 R x y2 一起表示y1=y2。 Definition partial_function {X: Type} (R: relation X) Definition partial_function {X: T...

这一短小的（可选的）章节发展了一些关于Coq中二元关系的基本定义和几个定理。关键定义在实际使用的地方重复（在编程语言基础的Smallstep一章中），因此已经熟悉这些概念的读者可以安全地浏览或跳过本章。然而，关系也是使用Coq的基本推理工具开发工具的一个很好的练习来源，因此在IndProp一章之后查看此材料可能会很有用。 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality". From LF Require Export IndProp.  关系 Relations 集合X上的二元关系是由X...

Chap 10 定义 + 定理   10.1 环     10.1.1 基本定义  定义 10.1.1 环 交换环 单位元环 定理 10.1.1 环R中元素的运算性质 定理 10.1.2 （有单位元的环）    10.1.2 零因子环  定义 10.1.4 （左/右）零因子 有零因子环 定义 10.1.5 （左/右）逆元 【左/右】逆    10.1.3 整环及域  定义 10.1.4 整环 （有单位元但没有零因子的交换环） 性质 10.1.1 （整环有消去律成立） 定义 10.1.5 域（有单位元且每个非零元都是可逆元的交换环）    10.1.4 交换环上的整除  定义 10.1.6 整除...

Chap 10 环与理想 - 环   10.1 环     10.1.1 基本定义  定义 10.1.1 环 交换环 单位元环 定理 10.1.1 环R中元素的运算性质 定理 10.1.2 （有单位元的环）    10.1.2 零因子环  定义 10.1.4 （左/右）零因子 有零因子环 定义 10.1.5 （左/右）逆元 【左/右】逆    10.1.3 整环及域  定义 10.1.4 整环 （有单位元但没有零因子的交换环） 性质 10.1.1 （整环有消去律成立） 定义 10.1.5 域（有单位元且每个非零元都是可逆元的交换环）    10.1.4 交换环上的整除  定义 10.1.6 整...

11.1 多项式整环  整环R上的全体多项式组成的集合R[X]（11.1）  R[X]上的加法（11.2）  R[X]上的乘法（11.3）   定理 11.1.1 整环R上的多项式环符合式R[X]对于多项式的加（乘）法式是一个整环  11.2 多项式整除与不可约多项式 本节考虑多项式的整除性。 前面考虑了多项式整除和因式,现在考虑对于乘法的次数最小的多项式,也就是不能继续分解的多项式，即下面的不可约多项式。 多项式是否可约与所在的环或域相关。 定义11.2.1 整除 因式 倍式  定理 11.2.1 多项式整除具有传递性  定理 11.2.2 在多项式f(x)， g(x)的线性组合中,整除的性...

Verification Methods 验证方法可根据以下主要标准进行分类：   基于证明与基于模型-如果可靠性和完整性定理成立，则：   证明=有效公式=在所有模型中均为真；   基于模型=检查一个模型中的可满足性     自动化程度-完全自动化、部分自动化或手动   完整-与属性-验证-单个属性与完整行为   应用领域-硬件或软件；连续的或并发的；反应的或终止的；等   前期开发与后期开发   Model Checking  模型检查是一种验证方法，即：  基于模型、自动化、使用属性验证方法，主要用于验证并发程序和反应式系统，通常在后开发阶段。  程序验证（稍后研究）是：  基于证明的计...

总地图 本章中我们的主要工作是建立一个部分映射的定义，该定义在行为上与我们在列表一章中看到的部分映射相似，另外还有关于其行为的伴随引理。 不过，这次我们将使用函数而不是键值对列表来构建映射。这种表示法的优点是它提供了一个更为扩展的映射视图，其中以相同方式响应查询的两个映射将被表示为字面上相同的东西（非常相同的函数），而不仅仅是“等效”的数据结构。这反过来又简化了使用地图的证明。 我们分两步构建部分映射。首先，我们定义一种类型的total maps，当我们查找map中不存在的键时，它将返回一个默认值。 Definition total_map (A : Type) := string ->...

标识符 首先，我们需要一个用于索引到地图中的键的类型。在Lists.v中，我们为类似的目的引入了一个新的类型id；在这里以及其他软件基础中，我们将使用Coq标准库中的字符串类型。 为了比较字符串，我们定义了函数eqb_string，它在内部使用Coq的字符串库中的函数string_dec。 Definition eqb_string (x y : string) : bool := if string_dec x y then true else false.  （函数string_dec来自Coq的字符串库。如果您检查string_dec的结果类型，您将看到它实际上并没有返回bool，而是返...