Недетерминированные конечные автоматы
Приведённое в конце прошлого раздела доказательство корректности автомата Кнута-Морриса-Пратта было весьма сложным (и, мягко говоря, очень наброскообразным). Оказывается, обобщив понятие детерминированного автомата, можно кардинально упростить подобные доказательства.
Недетерминированные автоматы
Недетерминированным автоматом (далее НДА) называется отображение \(t:S\times A\to PA\), где \(PA\) — множество всех подмножеств множества \(A\). Результатом работы НДА (на начальном множестве \(S_0\) и тексте \(a\)) является последний элемент последовательности
\[ S_{n+1} = \cup \{ t(s)\,|\, s\in S_n \} \]
Результат работы НДА можно вычислить функцией
def run_nda(nda, s0, text):
s = set(s0)
for a in text: s = set([y for x in s for y in nda(x,a)])
return s
Нетрудно заметить, что НДА можно превратить в ДА вида \(PS\times A\to PA\) функцией
def determinize_nda(nda):
def da(s,a):
return set([y for x in s for y in nda(x,a)])
return da
Корректность автомата КМП
Теперь приведём простое (и существенно более формальное) доказательство
корректности работы автомата КМП. Нам потребуется лишь одинарная
индукция (по длине needle
). Пусть \(T\) — ДКА для слова needle[:N-1]
,
а также пусть \(Z\) — последний символ needle
.
Рассмотрим НДА, определённый следующим образом:
\[ t(x,a) = \{ T(x,a) \},\; x \lt N-1 \]
\[ t(N-1,x) = \{ T(N-1,x) \},\; x\ne Z \]
\[ t(N-1,Z) = \{ T(N-1,Z), N \} \]
\[ t(N,x) = \{\} \]
Если этот автомат запустить на начальном состоянии \(\{0\}\), то про его результат очевидно, что искомая длина префикса является наибольшим из состояний результата.
При этом единственный результат, содержащий более одного состояния,
выглядит как \(R=\{ T(N-1,Z), N \}\). Нетрудно заметить, что по символу
x
такое состояние переходит в \(t(T(N-1,Z),x)\). Поэтому, если
мы назовём состояние R
числом \(N\), мы получим детерминированный
автомат
\[ t(x,a) = T(x,a),\; x \lt N-1 \]
\[ t(N-1,x) = T(N-1,x),\; x\ne Z \]
\[ t(N-1,Z) = N \]
\[ t(N,x) = t(T(N-1,Z), x) \]
Именно такой автомат и строится функцией kmp_dfa
.