Изменения

Перейти к: навигация, поиск
Нет описания правки
|proof=
Обозначим язык всех общезначимых формул <tex>L = \{w | w</tex> {{---}} общезначимая формула исчисления предикатов первого порядка<tex>\}</tex>. Покажем, что [[Разрешимые (рекурсивные) языки#uni | универсальный язык]] <tex>U</tex> [[m-сводимость | m-сводится]] к <tex>L</tex>. Для этого нужно построить вычислимую функцию <tex>f</tex>, которая принимает на вход пару из [[ Машина Тьюринга | машины Тьюринга ]] <tex>M = \langle \Sigma, \Pi, B, Q, Y, N, S, \delta \rangle</tex> и слова <tex>w</tex> и возвращает некоторую формулу исчисления предикатов, причём:
* :<tex>f(\langle M, w \rangle) \in L \iff M</tex> попадает в допускающее состояние <tex>Y</tex> на входе <tex>w</tex>.
Введём двухместный предикат <tex>=</tex> со следующими аксиомами равенства (для удобства будем использовать инфиксную запись):
* <tex>\forall x (x = x)</tex> {{---}} [[Рефлексивное отношение | рефлексивность;]],* <tex>\forall x \forall y (x = y \rightarrow y = x)</tex> {{---}} [[Симметричное отношение | симметричность;]],* <tex>\forall x \forall y \forall z ((x = y \& wedge y = z) \rightarrow x = z)</tex> {{---}} [[Транзитивное отношение | транзитивность;]],* для каждой функции <tex>f</tex> от <tex>n</tex> аргументов <tex>\forall x_1 \ldots \forall x_n \forall y_1 \ldots \forall y_n ((x_1 = y_1 \& wedge \ldots \& wedge x_n = y_n) \rightarrow f(x_1, \ldots x_n) = f(y_1, \ldots y_n)</tex> {{---}} согласованность с функциональными символами;,* для каждого предиката <tex>p</tex> от <tex>n</tex> аргументов <tex>\forall x_1 \ldots \forall x_n \forall y_1 \ldots \forall y_n ((x_1 = y_1 \& wedge \ldots \& wedge x_n = y_n) \rightarrow (p(x_1, \ldots x_n) \rightarrow p(y_1, \ldots y_n))</tex> {{---}} согласованность с предикатными символами.
Для каждого символа <tex>s \in \Pi</tex> заведём константу <tex>s</tex>, для каждого состояния <tex>q \in Q</tex> заведём константу <tex>q</tex>. Чтобы специальным образом кодировать ленту, введём две двухместные функции: <tex>|</tex> и <tex>\cdot</tex>, а также одноместную функцию <tex>g</tex>. [[ Машина Тьюринга#conf | Конфигурацию ]] <tex>\langle c_0 c_1 \ldots c_{l - 1}, q, c_l \ldots c_m \rangle</tex> теперь можно представить следующей формулой (опять же будем использовать инфиксную запись для удобства):
* :<tex>q | c_0 \cdot c_1 \cdot \ldots \cdot c_{l - 1} \cdot g(c_l) \cdot c_{l + 1} \cdot \ldots \cdot c_m</tex>
Заведём множество формул <tex>A</tex>. Для каждого перехода, сдвигающего головку влево, <tex>\delta(q, c_1) = \langle p, c_2, \leftarrow \rangle</tex> добавим в <tex>A</tex> формулу <tex>\forall x \forall y ((q | x \cdot c_0 \cdot g(c_1) \cdot y) = (p | x \cdot g(c_0) \cdot c_2 \cdot y))</tex>. Для переходов, сдвигающих головку вправо или оставляющих на месте, аналогичным образом добавим соответствующие формулы в <tex>A</tex>.
Теперь можно построить формулу <tex>f(\langle M, w \rangle)</tex>:
* :<tex>(A_0 \& wedge A_1 \& wedge \ldots \& wedge A_n) \rightarrow yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex>, где <tex>x_0 x_1 \ldots x_k = w</tex>.Заметим, что по построению из <tex>A_0 \& wedge A_1 \& wedge \ldots \& wedge A_n</tex> следует равенство двух формул, кодирующих любые две конфигурации <tex>C_1</tex> и <tex>C_2</tex>, такие что <tex>C_1 \vdash^* C_2</tex>. Поскольку предикат равенства согласован с предикатными символами (в частности с <tex>yes</tex>), то оценка <tex>yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex> совпадает с оценкой <tex>yes(u)</tex>, где <tex>u</tex> {{---}} формула, кодирующая некую конфигурацию <tex>C</tex>, что <tex>C_0 \vdash^* C</tex>, где <tex>C_0</tex> {{---}} начальная конфигурация, опять же при условии <tex>A_0 \& wedge A_1 \& wedge \ldots \& wedge A_n</tex>.
Если <tex>M</tex> допускает <tex>w</tex>, то <tex>C_0 \vdash^* \langle u, Y, v \rangle</tex>, поэтому оценка <tex>yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex> совпадает с оценкой <tex>yes(Y|x)</tex> для какого-то <tex>x</tex>. По построению из <tex>A_0 \& wedge A_1 \& wedge \ldots \& wedge A_n</tex> в частности следует, что <tex>\forall x (yes(Y | x))</tex>, а значит, в этом случае <tex>f(\langle M, w \rangle)</tex> оказывается общезначима.
Если же <tex>M</tex> не допускает <tex>w</tex>, то и доказательства для <tex>f(\langle M, w \rangle)</tex> существовать не будет. Это вытекает из того факта, что во всём множестве <tex>A</tex> присутствует лишь одна формула, содержащая предикат <tex>yes</tex> {{---}} <tex>\forall x (yes(Y | x))</tex>. Поэтому доказать следование <tex>yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex> можно лишь через эту формулу. Для подмены аргументов в предикатах существуют только аксиомы равенства, а <tex>(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex> не равна никакой другой формуле вида <tex>(Y | x)</tex>, поэтому от <tex>\forall x (yes(Y | x)</tex> не перейти к <tex>yes(S | x_0 \cdot x_1 \cdot \ldots \cdot x_k)</tex>, а значит, и доказательство <tex>f(\langle M, w \rangle)</tex> построить не удастся. Поэтому эта формула не будет общезначимой.
== См. также ==
* [http://neerc.ifmo.ru/wiki/index.php?title=%D0%98%D1%81%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5_%D0%BF%D1%80%D0%B5%D0%B4%D0%B8%D0%BA%D0%B0%D1%82%D0%BE%D0%B2 [Исчисление предикатов]]* [http://neerc.ifmo.ru/wiki/index.php?title=%D0%A0%D0%B0%D0%B7%D1%80%D0%B5%D1%88%D0%B8%D0%BC%D1%8B%D0%B5_[Разрешимые (%D1%80%D0%B5%D0%BA%D1%83%D1%80%D1%81%D0%B8%D0%B2%D0%BD%D1%8B%D0%B5рекурсивные)_%D1%8F%D0%B7%D1%8B%D0%BA%D0%B8 языки | Разрешимые языки]]* [http://neerc.ifmo.ru/wiki/index.php?title=M-%D1%81%D0%B2%D0%BE%D0%B4%D0%B8%D0%BC%D0%BE%D1%81%D1%82%D1%8C [m-сводимость]]* [http[Примеры неразрешимых задач://neerc.ifmo.ru/wiki/index.php?title=%D0%9F%D1%80%D0%B8%D0%BC%D0%B5%D1%80%D1%8B_%D0%BD%D0%B5%D1%80%D0%B0%D0%B7%D1%80%D0%B5%D1%88%D0%B8%D0%BC%D1%8B%D1%85_%D0%B7%D0%B0%D0%B4%D0%B0%D1%87:_%D0%BF%D1%80%D0%BE%D0%B1%D0%BB%D0%B5%D0%BC%D0%B0_%D1%81%D0%BE%D0%BE%D1%82%D0%B2%D0%B5%D1%82%D1%81%D1%82%D0%B2%D0%B8%D0%B9_%D0%9F%D0%BE%D1%81%D1%82%D0%B0 проблема соответствий Поста | Проблема соответствий Поста]]
== Источники информации ==
25
правок

Навигация