KMP算法中的next函数的证明

KMP算法的next函数的证明

1.1 Next函数定义与代码

1.1.1 定义

1.1.2 实现代码

/*代码摘自《大话数据结构》*/

/*t为字串，next为int数组，存储next值*/

void getnext(string T,int *next)

{

int i,j;

i=1;j=0;next[1]=0;

while(i<T[0]) //T[0]表示字符串T的长度

{

if(j==0 || T[i]==T[j])

{

++i;

++j;

next[i]=j;

}

else

j=next[j];

}

}

1.2 证明思路

采取分段证明的办法，证明j往区间(m,k)移动是不正确的，验证移动到m（next[j]=m）的正确性。

在证明的过程中，都是假设j移动到某个位置之后，讨论if判断条件会成立。因为如果是不成立的话，程序流程又会转移到j的移动，这样我们就会陷入死循环。而且，这种假设，即if成立，在逻辑上也是成立的，就像递归函数一样，只要一层是正确的，递归的肯定也没问题。

1.3 证明

首先观察这个函数的代码，我们可以获得如下信息：

(1) 若if成立，则i、j都加1；

(2) i的值为k，则next[k]已经有了结果，且在下一轮if之前j= next[k]；

(3) 当要求next[k]的时候，if中的判断条件是i=k-1；

证明：

前提条件：假设next[k]=s,

即T[1]…[s-1]=T[k-s+1]…[k-1]（1）

现求next[k+1]=?根据前面的结论，此时i=k，j=s。令next[s]=m.

现进行if判断：

(1) 若条件成立，

即T[i]=T[j]，也即T[k]=T[s]，结合式（1），则有

T[1]…[s-1][s]=T[k-s+1]…[k-1][k] （2）

则next[k+1]=s+1，即代码中的next[i]=j;继续下一次if判断。

(2) 若条件不成立，

即T[i] != T[j]，则我们需要移动j。

假设向区间 (s , k) 移动，假使使j=s+1，满足if条件，即T[k]=T[s+1]，

根据代码，则next[k+1]=s+2，意味着

T[1]…[s-1][s][s+1]=T[k-s]…[k-1][k] （3）

等式两边去掉末位，

T[1]…[s-1][s] =T[k-s]…[k-1] （4）

从这可以推出next[k]=s+1，与前面矛盾，所以j不能向前移（假若向前移动更多位的话，就会推出next[k]比s+1更大的值）

下面证明j向（m，s）区间移动是不行的。

已知条件：i=k,j=s,next(s)=m,next(k)=s,T[k]!=T[s]，需证明移动到m+1是不行的。

现我们假设把j移动到m+1，而不是代码中的m。

根据已知条件可以得到：

next(k)=s =>T[1]…[s-1]=T[k-s+1]…[k-1] (5)

next(s)=m =>T[1]…[m-1]=T[s-m+1]…[s-1] (6)

if判断成立，T[k]=T[m+1]，则得到next(k+1)=m+2,

T[1]…[m+1]=T[k-m]…[k] (7)

两边去掉右边一位，则有T[1]…[m] =T[k-m]…[k-1] (8)

观察（5），因为s>=m+1,所以k-m>=k-s+1，

所以T[1]…[m] =T[k-m]…[k-1]

= T[s-m]…[s-1] （由5）

从这里可以推出，next(s)至少为m+1，与已知矛盾。

显然，若移动到m+2等就可以得到更大的next(s)的值了。

接下来，我们证明移动j到next[j]的正确性。

设next[j]=m，此时j=s，next[s]=m，移动j到next[s]后，即j=m。

由next[s]=m有：

T[1]…[m-1] =T[s-m+1]…[s-1] （9）

判断T[i]==T[j]，即T[k]==T[m]，条件成立之后，因为s>=m+1,所以

k-m+1>k-s+1，即T[k-m+1]在T[k-s+1]…[k-1][k]中。

取（1）中等式两边右边的m-1项，得到：

T[s-m+1]…[s-1] =T[(k-1)-(m-1)+1]…[k-1]= T[k-m+1]…[k-1] (10)

又结合（9）（10）有

T[1]…[m-1] =T[k-m+1]…[k-1] （11）

结合T[k]==T[m]，有

T[1]…[m-1][m]=T[k-m+1]…[k-1][k] (12)

从而next[k+1]=m+1，即代码中的next[i]=j。由next的定义可知，j向(0,m)区间移动的话就得不到正确的next值，应为已经找到了j=m满足要求，j值只能增大，减少就不符合定义。

至此，我们证明了把j回溯到大于m的任何位置都会得到错误的结论，且验证了移动到m可以得到正确的结论。