68
правок
Изменения
Нет описания правки
Общую длину получившейся формулы можно представить как <tex>L(t) = L(t-1)*2+const</tex>. Заметим, что из-за умножения на 2 на каждом шаге рекурсии <tex>L(t)</tex> будет иметь экспоненциальный размер относительно <tex>t</tex>. Нас это не устраивает, так как нам необходимо полиномиальное сведение. Поэтому воспользуемся квантором <tex>\forall</tex> и перепишем её следующим образом:
<tex>\phi(A, B, t) = \exists R \,\forall U \,\forall V \, \{\phi(U, V, t-1) \nRightarrow \negand [(U = A \land V = R) \lor (U = R \land V = B)]\}</tex>.
Получившаяся формула верна только когда верно <tex>\phi(U, V, t-1)</tex> и ложно <tex>\neg[(U = A \land V = R) \lor (U = R \land V = B)]</tex>. Это равносильно тому, что <tex>V</tex> достижима из <tex>U</tex> не более, чем за <tex>2^{t-1}</tex> шагов, и либо <tex>U = A \land V = R</tex>, либо <tex>U = R \land V = B</tex>. А если верно и то, и другое, то конфигурация <tex>B</tex> достижима из конфигурации <tex>A</tex> не более, чем за <tex>2^t</tex> шагов.
За один шаг рекурсии длина максимального пути между конфигурациями уменьшается в два раза. Поэтому общую длину получившейся формулы можно представить как <tex>L(t) = L(t-1)+const</tex>, где <tex>const = \|\exists R \,\forall U \,\forall V \, \{\| + \|\nRightarrow \negand [(U = A \land V = R) \lor (U = R \land V = B)]\}\|</tex>.
Следовательно, размер полученной функции <tex>\phi(A, B, t)</tex> полиномиален относительно <tex>t</tex>.
Докажем, что сведение <tex>f</tex> корректно.
Если <tex>w \in L</tex>, то существует путь из стартовой конфигурации в финишную, причём длины не более, чем <tex>2^{\Omega r(n)}</tex>, а значит формула <tex>f(M, w)</tex> верна.
Если формула <tex>f(M, w)</tex> оказалась верна, то существует путь из стартовой конфигурации в финишную длины не более, чем <tex>2^{\Omega r(n)}</tex>. Значит, ДМТ <tex>M</tex> допускает слово <tex>w</tex>. Тогда <tex>w \in L</tex>.
