# Bellman-Ford算法证明

# 算法回顾

Bellman-Ford是寻找加权无向图（weighted undirected graph）中两个顶点之间最短路径的算法。用表示图，和分别表示图中所有顶点和边的集合，记作，用表示起点。那么Bellman-Ford算法的伪代码形式如下：

bellman_ford(V, E, s)
	// v.d表示从s到v的最短路径长度，初始化为Infinity
	// v.p表示最短路径上该顶点的前一个顶点，即该顶点对应的parent（p）节点
	for v in V:
	    v.d = Infinity
	    v.p = None

	s.d = 0

	// |V|表示所有顶点的数量
	for i from 1 to |V| - 1:
			// u和v对应一条有向边的起点和终点
	    for (u, v) in E:
	        relax(u, v)

	// 执行完relax操作后，可以通过v.p回溯找到包含最短路径的所有边

其中用到的relax方法的伪代码定义如下：

relax(u, v):
	// w(u,v)表示顶点u和v之间边的权值
	if v.d > u.d + w(u,v):
	  v.d = u.d + w(u,v)
    v.p = u

简单来说，Bellman-Ford算法就是对图中的所有边进行次relax操作，从而得顶点之间的最短路。该算法的好处在于，在执行完算法后，我们得到的不仅仅是到某一个顶点之间的最短路径，而是到所有其它顶点之间的最短路径。值得注意的是，在遍历所有边进行relax操作时，可以是任意遍历顺序。

# 算法证明

# 证明

这里我们假设图中没有negative cycle，主要关注怎么用数学归纳法（mathematical induction）来进行证明。

我们用表示到之间边数不超过的最短路径长度，用表示和之间所有路径中最短的那一条的长度。因为到任意顶点的简单路径（simple path）最多包含条边，我们只需要证明，便可完成对Bellman-Ford算法的证明。

首先证明base case。当循环次时，即进入relax操作的循环前，为，即起点到它自己的最短路径为。而对于其它顶点，为无穷大，即不存在一条和之间且边数为的最短路径。显然这是正确的。

然后假设循环次进行relax操作后满足，即循环次后，若不为无穷大，表示能够在和之间找到不超过条边的最短路径。

最后我们来分析循环次后，的取值。将和之间不超过条边的最短路径记为，用来表示一条路径的长度或者两个顶点间边的权值，且为上处在之前的一个顶点，那么和之间的路径最多包含条边。

shortest-path

必然是和之间的最短路径，否则假若有更短的路径，那么，这与为最短路径的定义相悖。

通过前面的假设，我们知道。根据算法，在第次循环中，即。而表示和之间边数不超过的最短路径，其长度至少也是和一样长，即，所以。不难看出，relax操作具有单调递减的性质，即。

所以当算法循环次后，，命题得证。

# Bellman-Ford算法证明

# 算法回顾

# 算法证明

# 证明

# 参考