| Известия Российской академии наук. Серия математическая |
|
|
|
|
|
Эта публикация цитируется в 1 научной статье (всего в 1 статье) Алгоритмическая сложность теорий коммутативных алгебр Клини С. Л. Кузнецов Математический институт им. В. А. Стеклова Российской академии наук, г. Москва
Англоязычная версия:
Izvestiya: Mathematics, 2024, Volume 88, Issue 2, Pages DOI: https://doi.org/10.4213/im9480e 
Реферативные базы данных:
     § 1. Введение1.1. Алгебры КлиниПонятие алгебры Клини восходит к работе Клини [1]. Сигнатура алгебр Клини состоит из бинарных операций сложения и умножения, унарной операции итерации (“звездочка Клини”) и констант $0$ и $1$. В алгебрах Клини (см. определение ниже) операция сложения является идемпотентной, и с ее помощью определяется частичный порядок: $a \leqslant b$ понимается как $a+b=b$. Определение 1. Алгеброй Клини называется такая алгебраическая структура $(\mathcal{A}; +, {\cdot}\,, {}^*, 0, 1)$, что Далее алгебры Клини будем иногда называть просто “алгебрами”. Естественным примером алгебры Клини является алгебра формальных языков над некоторым алфавитом $\Sigma$, носителем которой является множество всех подмножеств множества слов над $\Sigma$, т. е. $\mathcal{A}=\mathcal{P}(\Sigma^*)$. Умножение определяется как поэлементное приписывание слов: сложение – как объединение языков, а звездочка Клини – следующим образом:
$$
\begin{equation*}
A^*=\bigcup_{n \geqslant 0} A^n=\{ u_1 \cdots u_n \mid n \geqslant 0, u_1,\dots, u_n \in A \}.
\end{equation*}
\notag
$$
Константам $0$ и $1$ отвечают пустой язык $\varnothing$ и синглетон пустого слова $\{\varepsilon\}$ соответственно. Другой естественный пример алгебры Клини – алгебра бинарных отношений на некотором множестве $W$ с носителем $\mathcal{A}=\mathcal{P}(W \times W)$. Здесь умножение определяется как композиция отношений, сумма – как объединение, а звездочка Клини – как рефлексивно-транзитивное замыкание; $0=\varnothing$, $1=\{ (x,x) \mid x \in W \}$. Если рассматривать элементы множества $W$ как состояния некоторой системы, то бинарные отношения моделируют недетерминированные действия (операции) на этом множестве состояний, например, переходы в конечном автомате. Такое понимание родственно исходной мотивации Клини [1]. И алгебра языков, и алгебра отношений принадлежат к специальному классу алгебр Клини, называемых $*$-непрерывными. Определение 2. Алгебра Клини называется $*$-непрерывной, если для любых $a,b,c \in \mathcal{A}$ верно следующее: (где $a^0=1$, $a^{n+1}=a \cdot a^n$). Новое условие на итерацию сильнее соответствующего условия из определения 1, причем в строгом смысле: существуют алгебры Клини, не являющиеся $*$-непрерывными. Последнее можно доказать косвенно, пользуясь различием уровня сложности связанных с данными классами алгебр логических теорий (см. ниже), либо используя теорему о компактности. Явный пример не-$*$-непрерывной алгебры Клини построил Козен [2; § 3]. Настоящая работа посвящена коммутативному случаю. Определение 3. Алгебра Клини называется коммутативной, если такова ее операция умножения: $a \cdot b=b \cdot a$ для любых $a, b \in \mathcal{A}$. Пратт [3] мотивирует рассмотрение коммутативных алгебр Клини следующим образом. Если воспринимать элементы алгебры Клини как действия, то коммутативный случай соответствует параллельной (а не последовательной, как в некоммутативном случае) композиции действий. Что же касается алгебр формальных языков, то ее коммутативный вариант появляется в работе Редько [4], где он назван алгеброй коммутативных событий. Обыкновенные (некоммутативные) формальные языки можно рассматривать как подмножества свободного моноида, порожденного алфавитом $\Sigma$. По аналогии коммутативные “языки” (в терминологии Глушкова и Редько – события) суть подмножества свободного коммутативного моноида, порожденного множеством $\Sigma$. Аналогом слова в коммутативном случае является конечное мультимножество элементов $\Sigma$. Если алфавит конечен: $\Sigma=\{a_1, \dots, a_n \}$, то коммутативные “слова” можно эквивалентно представлять в виде париховых векторов [5]: $w \mapsto (|w|_{a_1}, \dots, |w|_{a_n}) \in \mathbb{N}^n$, где $|w|_{a_i}$ – кратность вхождения буквы $a_i$ в мультимножество $w$. 1.2. Теории классов алгебр КлиниДля данного класса $\mathcal{K}$ алгебраических структур – например, класс коммутативных $*$-непрерывных алгебр Клини – определяются логические теории данного класса, состоящие из всех общезначимых на данном классе $\mathcal{K}$ формул. Такие теории для одного и того же класса различаются в зависимости от выразительных возможностей используемого языка формул. Напомним основные определения. Определение 4. Зафиксируем счетное множество $\mathrm{Var}=\{ x_1, x_2, \dots \}$ предметных переменных. Множество термов в языке алгебр Клини, обозначаемое $\mathrm{Tm}$, есть наименьшее по включению множество, удовлетворяющее следующим условиям: В дальнейшем при записи термов мы будем опускать скобки, считая, что умножение связывает сильнее сложения, а итерация приоритетнее умножения; сложение и умножение ассоциируются влево. Определение 5. Атомарной (или эквациональной) формулой называется выражение вида $A=B$, где $A, B \in \mathrm{Tm}$. Заметим, что “инэквациональная” формула вида $A \leqslant B$ понимается как альтернативная запись $A+B=B$, и таким образом является частным случаем эквациональной формулы. Определение 6. Пусть $\mathcal{H}=\{ A_1=B_1, \dots, A_n=B_n \}$ – конечное множество атомарных формул, а $C= D$ – еще одна атомарная формула. Выражение вида $\mathcal{H} \Rightarrow C=D$ называется хорновой формулой. Атомарные формулы из множества $\mathcal{H}$ называются гипотезами, а $C=D$ – заключением данной хорновой формулы. Атомарная формула может рассматриваться как частный случай хорновой (с $\mathcal{H}= \varnothing$). Также можно рассматривать намного более выразительный язык первопорядковых формул, которые строятся из атомарных стандартным образом: с помощью булевых операций и кванторов по предметным переменным. В частности, на первопорядковом языке хорнова формула записывается в виде $(A_1=B_1 \mathop{\&} \cdots \mathop{\&} A_n=B_n) \Rightarrow C=D$. Однако, как мы увидим далее, уже в языке хорновых формул теории интересных нам классов алгебр достигают максимально возможных уровней алгоритмической сложности, поэтому рассматривать более выразительные языки с точки зрения сложности не имеет смысла. Зафиксировав алгебру Клини с носителем $\mathcal{A}$ и функцию означивания переменных $\alpha \colon \mathrm{Var} \to \mathcal{A}$, можно стандартным образом определить означивание термов (т. е. продолжить функцию означивания до $\overline{\alpha} \colon \mathrm{Tm} \to \mathcal{A}$) и истинность атомарных и хорновых формул. Формула (атомарная или хорнова) общезначима на данном классе алгебр $\mathcal{K}$, если она истинна при любом означивании на любой алгебре из данного класса. Определение 7. Эквациональной теорией класса алгебр $\mathcal{K}$ называется множество всех атомарных формул, общезначимых на классе $\mathcal{K}$; хорновой теорией – множество всех таковых хорновых формул. Также рассматриваются более слабые хорновы теории с ограничениями на множества гипотез. 1.3. Сложность теорий в некоммутативном и в коммутативном случаяхРабота Козена [6] посвящена алгоритмической сложности теорий алгебр Клини в некоммутативном случае: в качестве $\mathcal{K}$ рассматривается либо класс всех алгебр Клини, либо класс всех $*$-непрерывных алгебр Клини. Интересные нам результаты о сложности (как принадлежащие Козену, так и более ранние), изложенные в упомянутой работе, можно собрать в следующую таблицу:
В настоящей статье изложены результаты о сложности в коммутативном случае. Оказывается, что они аналогичны некоммутативному случаю:
Интерес здесь представляют результаты о сложности для хорновых теорий в $*$-непрерывном случае, т. е. о $\Pi^0_2$-полноте и $\Pi^1_1$-полноте – они изложены в § 7 и § 8 соответственно. Остальные результаты сводятся к ранее известным (см. предложения 3 и 4 ниже) и приведены для полноты картины. Верхние оценки (§ 2) также легко получаются из известных результатов для некоммутативного случая. Результат о $\Pi^0_2$-полноте для хорновых теорий с гипотезами, не содержащими итерации, докладывался на конференции Logica 2021 (Гейнице, Чехия, 27 сентября–1 октября 2021 г.) и опубликован в сборнике трудов конференции [8]. Результат о $\Pi_1^1$-полноте для случая хорновых теорий без ограничений новый и ранее не публиковался. Идеи доказательств в целом восходят к построениям Козена в некоммутативном случае [6]. Существенным отличием, однако, является использование счетчиковых машин (машин Минского) вместо машин Тьюринга и использование синтаксических методов вместо семантических. Кроме того, в отличие от работы Козена, доказано, что существуют конкретные фиксированные множества гипотез $\mathcal{H}$, для которых имеют место результаты o $\Pi^0_2$-трудности и $\Pi^1_1$-трудности (теоремы 7 и 11 ниже). Это усиление результатов о сложности достигнуто за счет использования универсальной вычислимой функции. Такие усиленные нижние оценки переносятся и на некоммутативный случай (следствия 1 и 4 ниже). § 2. Верхние оценки сложности2.1. Погружение коммутативных теорий в некоммутативныеПокажем, что коммутативные хорновы теории для $*$-непрерывных алгебр Клини по сути являются частным случаем некоммутативных. За счет этого верхние оценки переносятся на коммутативный случай с некоммутативного. Пусть $V \subset \mathrm{Var}$ – некоторое конечное множество переменных. Зададим следующее множество гипотез:
$$
\begin{equation*}
\mathcal{C}_V=\{ x \cdot y=y \cdot x \mid x,y \in V \}.
\end{equation*}
\notag
$$
Предложение 1. Пусть $V$ – конечное множество переменных, содержащее все переменные, входящие в атомарные формулы из множества $\mathcal{H} \cup \{ C= D \}$. Хорнова формула $\mathcal{H} \Rightarrow C=D$ общезначима на классе всех коммутативных $*$-непрерывных алгебр Клини тогда и только тогда, когда хорнова формула $\mathcal{H} \cup \mathcal{C}_V \Rightarrow C=D$ общезначима на классе всех $*$-непрерывных алгебр Клини. Доказательство. Направление “тогда” практически очевидно. Пусть формула $\mathcal{H} \cup \mathcal{C}_V \Rightarrow C=D$ общезначима на классе всех $*$-непрерывных алгебр Клини. Возьмем хорнову формулу $\mathcal{H} \Rightarrow C=D$ и рассмотрим произвольное означивание на коммутативной $*$-непрерывной алгебре Клини, при котором формулы из $\mathcal{H}$ истинны. Поскольку данная алгебра коммутативна, формулы из $\mathcal{C}_V$ также будут истинными, и в силу общезначимости $\mathcal{H} \cup \mathcal{C}_V \Rightarrow C=D$ истинна будет также формула $C=D$. Это и дает общезначимость хорновой формулы $\mathcal{H} \Rightarrow C=D$ на классе коммутативных $*$-непрерывных алгебр Клини.
Для доказательства в направлении “только тогда” рассуждаем от противного. Пусть хорнова формула $\mathcal{H} \cup \mathcal{C}_V \Rightarrow C=D$ опровергается при некоторой интерпретации $\alpha$ на $*$-непрерывной алгебре Клини $\mathcal{A}$. Обозначим через $\mathrm{Tm}_V$ множество термов, в которых используются переменные только из множества $V$. Зададим внутри $\mathcal{A}$ подалгебру $\mathcal{A}|_V$ с носителем $\{ \overline{\alpha}(B) \mid B \in \mathrm{Tm}_V \}$. Легко видеть, что это множество замкнуто относительно операций алгебр Клини. Кроме того, означивание $\overline{\alpha}$ любого терма из $\mathrm{Tm}_V$ по определению попадает в $\mathcal{A}|_V$ (а другие термы, с переменными не из $V$, нас не интересуют). При переходе к подалгебре истинность атомарных формул не изменяется, поэтому в $\mathcal{A}|_V$, как и в $\mathcal{A}$, при том же означивании $\alpha$, истинны формулы из $\mathcal{H}$ и ложна формула $C=D$. Остается доказать, что $\mathcal{A}|_V$ коммутативна; тогда это и будет искомый контрпример, показывающий, что хорнова формула $\mathcal{H} \Rightarrow C=D$ не общезначима на классе коммутативных $*$-непрерывных алгебр Клини. Пусть $a=\overline{\alpha}(A)$ и $b=\overline{\alpha}(B)$, где $A, B \in \mathrm{Tm}_V$ – два произвольных элемента $\mathcal{A}|_V$. Докажем, что $a \cdot b=b \cdot a$ индукцией по суммарной сложности термов $A$ и $B$. Если $A=x$ и $B=y$ – переменные, то по условию при означивании $\alpha$ на алгебре $\mathcal{A}|_V$ истинна формула $x \cdot y=y \cdot x$ из множества $\mathcal{C}_V$. Значит, $a \cdot b=\overline{\alpha}(x \cdot y)=\overline{\alpha}(y \cdot x)= b \cdot a$. Выделенные элементы $0$ и $1$ также коммутируют с любыми элементами алгебры. Пусть теперь $A$ – составной терм; случай составного $B$ рассматривается симметрично. Рассмотрим возможные варианты. Если $A=A_1 \cdot A_2$, то по предположению индукции $a_1 \cdot b=b \cdot a_1$ и $a_2 \cdot b=b \cdot a_2$ (где $a_i=\overline{\alpha}(A_i)$). Имеем, в силу ассоциативности, $a \cdot b=a_1 \cdot a_2 \cdot b=a_1 \cdot b \cdot a_2=b \cdot a_1 \cdot a_2= b \cdot a$, что и требовалось. При $A=A_1+A_2$ пользуемся дистрибутивностью: $a \cdot b= (a_1+ a_2) \cdot b=a_1 \cdot b+a_2 \cdot b=b \cdot a_1+b \cdot a_2=b \cdot (a_1+a_2)=b \cdot a$. Наконец, если $A=A_1^*$, то по предположению индукции имеем $a_1 \cdot b=b \cdot a_1$. Отсюда $a^n_1 \cdot b=b \cdot a_1^n$ для любого натурального $n$ (индукция по $n$). По условию $*$-непрерывности имеем $a \cdot b=a_1^* \cdot b=\sup_{\leqslant} \{ a_1^n \cdot b \mid n \geqslant 0 \}= \sup_{\leqslant} \{ b \cdot a_1^n \mid n \geqslant 0 \}=b \cdot a_1^*=b \cdot a$. Коммутативность алгебры $\mathcal{A}|_V$ доказана. $\Box$ 2.2. Верхние оценки сложностиПредложение 1 позволяет сводить хорновы теории для коммутативных $*$-непрерывных алгебр Клини к хорновым теориям всех (в том числе некоммутативных) $*$-непрерывных алгебр Клини. А именно, каждая хорнова формула $\mathcal{H} \Rightarrow C=D$ заменяется на $\mathcal{H} \cup \mathcal{C}_V \Rightarrow C= D$, где $V$ – множество переменных, встречающихся в атомарных формулах из множества $\mathcal{H} \cup \{ C=D \}$. Заметим, что формулы из $\mathcal{C}_V$ не содержат итерации. Таким образом, получаем следующие верхние оценки. Предложение 2. Хорнова теория коммутативных $*$-непрерывных алгебр Клини принадлежит классу сложности $\Pi_1^1$, а ее фрагмент с гипотезами, не содержащими итерации, – классу сложности $\Pi_2^0$. В дальнейшем мы докажем, что эти оценки точны. Для случая эквациональной теории (или, что то же, теории с гипотезами вида $A \cdot B=B \cdot A$, которые в коммутативном случае общезначимы) имеем следующее предложение. Предложение 3. Эквациональная теория коммутативных $*$-непрерывных алгебр Клини алгоритмически разрешима и совпадает с эквациональной теорией всех коммутативных алгебр Клини. Доказательство. Здесь ситуация немного сложнее. Эквациональная теория коммутативных $*$-непрерывных алгебр Клини сводится к некоммутативной хорновой теории с множествами гипотез вида $\mathcal{C}_V$. Поскольку все гипотезы в этих множествах имеют вид $A \cdot B=B \cdot A$, получаем верхнюю оценку $\Pi^0_1$ [6; теорема 4.1(i)].
С другой стороны, Редько [4] построил конечную полную систему тождеств, задающую эквациональную теорию конкретного семейства $*$-непрерывных коммутативных алгебр Клини, а именно, алгебры коммутативных формальных языков (в терминологии Редько – коммутативных событий, см. выше). Оказывается, что все тождества из работы Редько общезначимы вообще на всех коммутативных алгебрах Клини, в том числе не $*$-непрерывных. Отсюда следует, что любое тождество (атомарная формула), общезначимое на всех $*$-непрерывных коммутативных алгебрах Клини, общезначимо и на всех алгебрах Клини, а обратное всегда верно, потому что сужение класса алгебр может разве что расширить теорию. Получаем, что эквациональная теория коммутативных $*$-непрерывных алгебр Клини совпадает с эквациональной теорией всех коммутативных алгебр Клини. Кроме того, эта теория перечислима в силу данной в работе Редько конечной аксиоматизации. Будучи при этом ко-перечислимой (т. е. принадлежащей $\Pi_1^0$), эта теория разрешима по теореме Поста. $\Box$ § 3. Коммутативная инфинитарная логика действий с экспоненциаломВведем вспомогательное исчисление, аксиоматизирующее некоторое расширение эквациональной теории коммутативных $*$-непрерывных алгебр Клини. А именно, добавим операцию деления (линейную импликацию, $\multimap$) и экспоненциальную модальность, обозначаемую $!$ . Добавление деления дает эквациональную теорию коммутативных $*$-непрерывных алгебр Клини с делением (residuated Kleene algebras) или коммутативный вариант инфинитарной логики действий (infinitary action logic) [9], [10]. Добавление экспоненциальной модальности в духе линейной логики Жирара [11] дает коммутативный вариант инфинитарной логики действий с экспоненциалом [12]. Цель введения такого расширенного исчисления следующая. С помощью деления можно интернализовать неравенства2 в исходном языке алгебр Клини, записывая их как термы: $A \multimap B$ вместо $A \leqslant B$. Далее, экспоненциальная модальность позволяет сформулировать модализированную версию теоремы о дедукции, за счет чего хорновы гипотезы размещаются внутри формулы: $A \leqslant B \Rightarrow C \leqslant D$ заменяется на ${!}(A \multimap B) \cdot C \leqslant D$. Таким образом, следование (выводимость) из гипотез заменяется на “чистую” выводимость формул, но в расширенном языке. Наконец, для последнего разработано удобное секвенциальное (генценовское) исчисление [12] с устранимым правилом сечения, что упрощает анализ выводов. Термы, также называемые линейными формулами, в расширенном языке строятся из переменных и констант $0$ и $1$ с помощью бинарных операций ${\cdot}\,$, $+$, $\multimap$ и унарных операций $^*$ и $!$ . (Обычно добавляется также аддитивная конъюнкция (пересечение) $\wedge$, нам она не нужна. Для объединения (аддитивной дизъюнкции) мы сохраняем обозначение $+$, вместо $\vee$ или $\oplus$ .) По традиции, итерация записывается в постфиксной форме: $A^*$, а экспоненциальная модальность – в префиксной: ${!}A$. Конечные мультимножества линейных формул обозначаются греческими буквами (в том числе пустое), отдельные линейные формулы – латинскими. Напомним, что в мультимножестве играет роль кратность вхождения элементов, но не их порядок. Секвенциями называются выражения вида $\Gamma \to B$. Секвенция вида $A_1, \dots, A_n \to B$ соответствует атомарной формуле $A_1 \cdot \ldots \cdot A_n \leqslant B$, а в случае пустой левой части ($n=0$) – формуле $1 \leqslant B$. Аксиомы и правила вывода данного исчисления, которое обозначается как $\boldsymbol{!}\mathbf{CommACT}_\omega$, суть следующие: Правила ${!}\mathrm{W}$ и ${!}\mathrm{C}$ вместе называются структурными правилами для модальности, а по отдельности – правилами ослабления и сокращения соответственно. Отдельно обсудим правило ${}^*\mathrm{L}$. Через $A^n$ в нем (и далее по тексту) обозначается последовательность, составленная из $n$ копий формулы $A$ (в частности, $A^0$ – это пустая последовательность). Правило ${}^* \mathrm{L}$, имея бесконечно много посылок, является омега-правилом. В присутствии омега-правила выводы могут быть бесконечными, однако сохраняется требование фундированности: всякая цепочка секвенций, идущая вверх по дереву вывода от целевой секвенции, должна за конечное число шагов достичь аксиомы. Каждому выводу сопоставляется ординал, называемый его рангом. Определение 8. Если вывод состоит из одной лишь аксиомы, то его ранг равен $1$. Если же вывод сложнее, то берется его заключительное правило, и ранг вычисляется как супремум (во всех случаях, кроме ${}^*\mathrm{L}$, это фактически максимум) рангов выводов его посылок плюс $1$. Условие фундированности гарантирует, что у любого вывода ранг корректно определен. Из работы [12] следует, что всякая выводимая секвенция имеет вывод ранга меньше, чем ординал Чёрча–Клини $\omega_1^{\mathrm{CK}}$. Отметим также, что в формулировке аксиомы $\mathrm{Id}$ требуется, чтобы левая (она же правая) часть была переменной. Для сложных формул $A$, однако, секвенции $A \to A$ являются выводимыми (но для дальнейшего удобства анализа выводов не объявляются аксиомами). Построенное исчисление $\boldsymbol{!}\mathbf{CommACT}_\omega$ очень близко к исчислению $\boldsymbol{!}\mathbf{ACT}_\omega$ из статьи [12]. Отличие состоит в коммутативности, в отсутствии аддитивной конъюнкции $\wedge$ и в использовании только одной экспоненциальной модальности вместо семейства субэкспоненциальных. За счет этого на систему $\boldsymbol{!}\mathbf{CommACT}_\omega$ переносятся, с практически теми же доказательствами, свойства системы $\boldsymbol{!}\mathbf{ACT}_\omega$ – устранимость правила сечения [12; теорема 4.2] и верхняя $\Pi_1^1$-оценка на сложность задачи выводимости [12; теорема 5.2]. Теорема 1. Любая секвенция, выводимая в исчислении $\boldsymbol{!}\mathbf{CommACT}_\omega$, выводима без использования правила $\mathrm{Cut}$. Теорема 2. Сложность задачи выводимости в исчислении $\boldsymbol{!}\mathbf{CommACT}_\omega$ принадлежит классу $\Pi_1^1$. Далее будет доказано (следствие 2), что эта оценка точна: задача выводимости в исчислении $\boldsymbol{!}\mathbf{CommACT}_\omega$ является $\Pi_1^1$-полной, т. е. имеет ту же сложность, что и $\boldsymbol{!}\mathbf{ACT}_\omega$ [12]. На самом деле, в семейство субэкспоненциальных модальностей исчисления $\boldsymbol{!}\mathbf{ACT}_\omega$ можно включить модальность, допускающую правило перестановки (и только его), и с помощью такой модальности построить консервативное вложение исчисления $\boldsymbol{!}\mathbf{CommACT}_\omega$ в $\boldsymbol{!}\mathbf{ACT}_\omega$ (при этом экспоненциальная модальность отобразится в другую субэкспоненциальную, которая допускает правила перестановки, ослабления и сокращения). Это вложение для модальности мультиплексирования вместо экспоненциальной дано в [13]. С помощью такого вложения можно получить сформулированные выше результаты как непосредственные следствия (а не аналоги) соответствующих теорем статьи [12]. Наконец, нам понадобится вложение хорновой теории коммутативных $*$-непрерывных алгебр Клини в исчисление $\boldsymbol{!}\mathbf{CommACT}_\omega$. Для этого по данному конечному множеству атомарных формул $\mathcal{H}=\{ A_1 \leqslant B_1, \dots, A_n \leqslant B_n \}$ определим мультимножество линейных формул
$$
\begin{equation*}
{!}\mathcal{H}={!} (A_1 \multimap B_1), \dots, {!} (A_n \multimap B_n).
\end{equation*}
\notag
$$
(Если в $\mathcal{H}$ встречается формула $A=B$, не имеющая вида неравенства, то ее можно эквивалентно заменить на две формулы: $A \leqslant B$ и $B \leqslant A$.) Теорема 3. Хорнова формула $\mathcal{H} \Rightarrow C_1 \cdot \ldots \cdot C_n \leqslant D$ общезначима на классе всех коммутативных $*$-непрерывных алгебр Клини тогда и только тогда, когда секвенция ${!}\mathcal{H}, C_1, \dots, C_n \to D$ выводима в исчислении $\boldsymbol{!}\mathbf{CommACT}_\omega$. (Если заключение хорновой формулы не имеет вид неравенства, то ее общезначимость можно свести к выводимости в $\boldsymbol{!}\mathbf{CommACT}_\omega$ двух секвенций: ${!}\mathcal{H}, C \to D$ и ${!}\mathcal{H}, D \to C$. Для изложенных далее доказательств нижних оценок сложности это не понадобится.) Доказательство теоремы 3 повторяет лемму 5.3 и теорему 5.7 из статьи [12] с точностью до коммутативности. Кроме того, в лемме 5.3 из [12] следует опустить п. 2, связанный с ограниченной (“релевантной”) модальностью ${!}^c$, и переходить от п. 1 сразу к п. 3. § 4. $\Sigma_1^0$-полнота хорновой теории всех коммутативных алгебр КлиниНастоящая работа в основном посвящена сложности теорий для класса коммутативных $*$-непрерывных алгебр Клини. Как отмечено в предыдущем параграфе, условие $*$-непрерывности на синтаксическом уровне транслируется в омега-правило. За счет этого выводы становятся бесконечными, что дает интересные высокие уровни алгоритмической сложности (вплоть до $\Pi_1^1$). В этом параграфе, однако, мы разберемся с намного более простым случаем класса произвольных коммутативных алгебр Клини. Определение алгебры Клини (в общем, не $*$-непрерывном случае) формулируется на языке логики первого порядка конечным множеством аксиом, и поэтому не только хорнова, но и первопорядковая теория класса всех коммутативных алгебр Клини перечислима, т. е. лежит в классе сложности $\Sigma^0_1$. Оказывается, что эта оценка точна. Более того, $\Sigma^0_1$-полнота достигается уже для хорновых формул, вообще не содержащих итерации (ни в гипотезах, ни в заключении). Предложение 4. Задача общезначимости хорновых формул без итерации на классе всех коммутативных алгебр Клини $\Sigma_1^0$-полна. Следовательно, такова и вся хорнова теория класса всех коммутативных алгебр Клини. Доказательство. Как отмечено выше, нетривиальна здесь нижняя оценка. Покажем, что эта оценка непосредственно следует из результата Линкольна и др. [14; следствие 3.8] о неразрешимости интуиционистской пропозициональной линейной логики, обозначаемой $\mathbf{ILL}$. В наших обозначениях $\mathbf{ILL}$, точнее ее фрагмент без аддитивной конъюнкции, получается из исчисления $\boldsymbol{!}\mathbf{CommACT}_\omega$ удалением правил для итерации Клини, т. е. ${}^*\mathrm{L}$ и ${}^*\mathrm{R}$ (после чего все выводы будут конечными). Из конструкции Линкольна и др. [14; § 3] следует, что задача проверки выводимости в $\mathbf{ILL}$ секвенций вида ${!}\mathcal{H}, C_1, \dots, C_n \to D$ (где внутри формул используются операции $\cdot$ и $+$) является $\Sigma^0_1$-полной.
Теперь докажем, что выводимость данной секвенции в $\mathbf{ILL}$ равносильна общезначимости хорновой формулы $\mathcal{H} \Rightarrow C_1 \cdot \ldots \cdot C_n \leqslant D$ на классе всех коммутативных алгебр Клини. Действительно, если данная хорнова формула общезначима на классе всех коммутативных алгебр Клини, то она тем более общезначима на классе коммутативных $*$-непрерывных алгебр Клини. По теореме 3 секвенция ${!}\mathcal{H}, C_1, \dots, C_n \to D$ выводима в $\boldsymbol{!}\mathbf{CommACT}_\omega$. Осталось заметить, что за счет теоремы об устранении сечения имеет место консервативность: если целевая секвенция не содержит итерации Клини, то итерация не может встречаться и в выводе (без сечения). Поэтому данная секвенция выводима в $\mathbf{ILL}$. В обратную сторону: пусть дана выводимость секвенции ${!}\mathcal{H}, C_1, \dots, C_n \to D$ в исчислении $\mathbf{ILL}$. Повторяя рассуждение из доказательства теоремы 3, а именно, индукцию по выводу в $\mathbf{ILL}$, получим, что хорнова формулы $\mathcal{H} \Rightarrow C_1 \cdot \ldots \cdot C_n \leqslant D$ общезначима на классе всех коммутативных алгебр Клини, а не только $*$-непрерывных. Действительно, поскольку вывод в $\mathbf{ILL}$ не содержит итерации Клини, рассуждение сработает и для не-$*$-непрерывной алгебры. Таким образом, доказана $\Sigma^0_1$-трудность задачи общезначимости хорновых формул без итерации на классе всех коммутативных алгебр Клини. $\Box$ § 5. Разбалансировка выводов в $\boldsymbol{!}\mathbf{CommACT}_\omega$Исчисление $\boldsymbol{!}\mathbf{CommACT}_\omega$ в дальнейшем (§ 6–§ 8) будет использовано для кодирования различных свойств вычислений на счетчиковых машинах (машинах Минского, п. 6.1). При этом переход от вычисления на счетчиковой машине к выводу соответствующей секвенции в $\boldsymbol{!}\mathbf{CommACT}_\omega$ осуществляется достаточно просто, а вот обратное преобразование – от вывода к вычислению – не столь прямолинейно. А именно, произвольный вывод, даже не содержащий правила сечения, не всегда в точности соответствует некоторому вычислению на счетчиковой машине. Для упрощения перехода от вывода к вычислению будем рассматривать не произвольные выводы, а выводы определенного вида, называемые разбалансированными. Преобразования разбалансировки, приводящие произвольные выводы к разбалансированным, введены в работе [15]. Техника разбалансировки является упрощенной версией фокусирования выводов [16] и призвана сделать структуру вывода без сечения более регулярной и удобной для анализа. В рамках этого параграфа считаем, что в выводах не используется правило сечения – в силу теоремы 1 у всякой выводимой секвенции существует вывод без сечения. Кроме того, мы рассматриваем только выводы, в которых не используются правила ${\multimap} \mathrm{R}$ и ${!}\mathrm{R}$. Это обстоятельство делает разбалансировку намного проще, чем фокусирование выводов, в которых могут использоваться произвольные правила исчисления. С другой стороны, излагаемая ниже техника разбалансировки применяется к потенциально бесконечным выводам, поскольку использование омега-правила ${}^{*}\mathrm{L}$ не запрещено. Это существенно отличает данную технику от разбалансировки [15] или фокусирования [16] конечных выводов. Отсутствие правил ${\multimap}\mathrm{R}$ и ${!}\mathrm{R}$ в выводе без сечения можно гарантировать простым синтаксическим свойством целевой секвенции. А именно, в ней не должны встречаться формулы вида $A \multimap B$ и формулы вида ${!}A$ в положительной полярности. (Полярность вхождения формулы определяется стандартным образом: полярность формулы как подформулы самой себя всегда положительна, далее же полярность меняется при помещении формулы в посылку линейной импликации ($\multimap$) либо в левую часть секвенции, а в остальных случаях – сохраняется.) Все секвенции, используемые далее для кодирования счетчиковых машин, будут удовлетворять этому условию, таким образом, будут выводимы без использования правил $\mathrm{Cut}$, ${\multimap}\mathrm{R}$ и ${!}\mathrm{R}$. Правыми правилами будем называть правила, вводящие операции в правую часть секвенции (в обозначении таких правил используется буква $\mathrm{R}$). Левые правила – это правила, вводящие операции в левую часть секвенции (обозначения с буквой $\mathrm{L}$), а также структурные правила ${!}\mathrm{W}$ и ${!}\mathrm{C}$. Аксиома $0\mathrm{L}$ считается левым правилом, аксиома $1\mathrm{R}$ – правым правилом. Определение 9. Вывод (в исчислении $\boldsymbol{!}\mathbf{CommACT}_\omega$), в котором не используются правила $\mathrm{Cut}$, ${\multimap}\mathrm{R}$ и ${!}\mathrm{R}$, назовем разбалансированным, если он удовлетворяет следующим условиям.
Второе условие объясняет термин “разбалансированный”: основное направление вывода, использующее левые правила, в том числе для экспоненциальной модальности, в таком выводе при ветвлении на правиле ${\multimap}\mathrm{L}$ идет только направо. Выводы же левых посылок оказываются короткими и относительно тривиальными. Таким образом, дерево вывода оказывается далеким от сбалансированного дерева, в котором все пути от корня к листу имеют примерно одинаковую длину. Теорема 4. Если у секвенции есть вывод в исчислении $\boldsymbol{!}\mathbf{CommACT}_\omega$, не использующий правила $\mathrm{Cut}$, ${\multimap}\mathrm{R}$ и ${!}\mathrm{R}$, то у этой секвенции есть разбалансированный вывод. Доказательство. Переход от произвольного вывода (без запрещенных правил) к разбалансированному достигается посредством серии преобразований, нацеленных на выполнение условий 1–3. Рассматриваемые выводы, однако, могут быть бесконечными, поэтому рассуждение нужно аккуратно оформить в виде трансфинитной индукции.
Сначала добьемся выполнения условия 1. Если вывод не удовлетворяет условию 1, то в нем найдется левое правило, непосредственно после (ниже) которого применено правое правило. В таком случае правила можно переставить. Например, так это делается для правил ${\multimap} \mathrm{L}$ и ${\cdot}\mathrm{R}$: преобразуется вДругой пример – правила ${}^*\mathrm{L}$ и ${}^*\mathrm{R}$: преобразуется в применение правила ${}^* \mathrm{L}$: а каждая из бесконечного числа его посылок выводится по правилу ${}^*\mathrm{R}$:Остальные пары левого и правого правил рассматриваются аналогично4. Докажем, что такими преобразованиями можно привести вывод к виду, удовлетворяющему условию 1. Сначала докажем вспомогательное утверждение (частный случай): если в выводе секвенции заключительным является правое правило, причем выводы его посылок удовлетворяют условию 1, то целевая секвенция также имеет вывод, удовлетворяющий условию 1. (Иначе говоря, если условие 1 могло быть нарушено только в самом конце вывода, то это нарушение можно устранить.) Назовем посылку заключительного правого правила “плохой” (т. е. нарушающей условие 1), если заключительное правило в ее выводе – левое. Рассуждаем трансфинитной индукцией по лексикографическому порядку на парах $(\beta, k)$, где $\beta$ – максимальный ранг вывода “плохой” посылки, а $k$ – число “плохих” посылок с выводами ранга5 $\beta$. Применим подходящее преобразование, из описанных выше, к одной из “плохих” посылок с выводом ранга $\beta$. Это преобразование переставляет правое правило с левым. При этом правое правило может “размножиться”, даже в бесконечное количество раз. У каждого из новых применений правого правила ранг “плохой” посылки, к которой было применено преобразование, – назовем ее активной – уменьшился как минимум на $1$. Остальные же посылки (в том числе “плохие”), как и ранги их выводов, не изменились. Если у правого правила были другие “плохие” посылки ранга $\beta$, кроме активной, то параметр $\beta$ не изменился, зато уменьшился на $1$ параметр $k$. Если же все остальные “плохие” посылки имели ранг меньше $\beta$, то уменьшается параметр $\beta$. (При этом не имеет значения, осталась ли активная посылка после преобразования “плохой”.) В обоих случаях можно применить предположение индукции. Получаем, что все посылки левого правила, которое после преобразования стало заключительным в выводе целевой секвенции, имеют выводы, удовлетворяющие условию 1. Присоединение к таким выводам снизу применения левого правила не нарушит условие 1. Вспомогательное утверждение доказано. Теперь докажем, что любой вывод (не использующий запрещенных правил) можно привести к виду, удовлетворяющему условию 1. Рассуждаем трансфинитной индукцией по рангу вывода, рассматривая возможные случаи для заключительного правила; по предположению индукции, его посылки уже имеют выводы, удовлетворяющие условию 1. Если заключительное правило левое или (тривиальный случай) является аксиомой, то его добавление не нарушит условие 1. Если же это правое правило, применяем доказанное выше вспомогательное утверждение. Теперь добьемся выполнения условия 2, сохраняя при этом условие 1. Для этого нужно избавиться от “неправильных” применений правила ${\multimap}\mathrm{L}$, у которых левая посылка выведена с помощью левого правила. Опять же, для начала докажем вспомогательное утверждение: если в выводе секвенции заключительным является правило ${\multimap}\mathrm{L}$, причем выводы его посылок удовлетворяют условиям 1 и 2, то целевая секвенция также имеет вывод, удовлетворяющий условиям 1 и 2. (Опять же, здесь условие 2 может быть нарушено только в самом конце вывода, и мы хотим устранить это нарушение.) Рассуждаем трансфинитной индукцией по рангу вывода левой посылки заключительного правила ${\multimap}\mathrm{L}$. Рассмотрим три случая. 1-й случай: эта левая посылка выведена с помощью правого правила. Тогда по условию 1 все правила в ее выводе правые, и вывод целевой секвенции уже удовлетворяет условию 2, а также условию 1 (добавление левого правила не нарушает условия 1). 2-й случай: левая посылка заключительного правила ${\multimap}\mathrm{L}$ выведена также с помощью правила ${\multimap}\mathrm{L}$: Преобразуем вывод следующим разбалансирующим преобразованием: Вывод $\Phi \to E$ не содержит левых правил, поскольку изначально все применения ${\multimap}\mathrm{L}$, кроме самого последнего, были “правильными”, т. е. не нарушали условия 2. Ранг вывода секвенции $\Pi, F \to A$ меньше, чем ранг вывода секвенции $\Pi, \Phi, E \multimap F \to A$, поэтому применимо предположение: секвенция $\Gamma, \Pi, F, A \multimap B \to C$ имеет вывод, удовлетворяющий условию 2. Присовокупляя к этому выводу вывод $\Phi \to E$ и заключительное применение правила ${\multimap}\mathrm{L}$, получаем искомый вывод целевой секвенции $\Gamma, \Pi, \Phi, E \multimap F, A \multimap B \to C$.3-й случай: левая посылка активного применения ${\multimap}\mathrm{L}$ выведена с помощью другого левого правила (логического или структурного). Все такие правила имеют единый вид: они действуют только внутри левой части секвенции, выводя секвенцию вида $\Pi \to A$ из секвенции или секвенций вида $\widetilde{\Pi} \to A$. В случае, если посылка только одна: вывод преобразуется следующим образом: Опять же, ранг левой посылки уменьшился, и мы можем применить предположение индукции. Случаи, когда у рассматриваемого правила ноль (правило $0\mathrm{L}$), две (правило ${+}\mathrm{L}$) или бесконечно много (правило ${}^*\mathrm{L}$) посылок, рассматриваются аналогично.Теперь докажем, что любой вывод (без запрещенных правил), удовлетворяющий условию 1, можно привести к виду, удовлетворяющему условиям 1 и 2, рассуждая трансфинитной индукцией по рангу вывода. Рассмотрим заключительное правило вывода. Случай аксиомы тривиален. В случае правого правила по условию 1 весь вывод состоит из правых правил, и поэтому автоматически удовлетворяет условию 2. Если заключительное правило – левое, но не ${\multimap}\mathrm{L}$, то по предположению индукции у каждой его посылки есть вывод, удовлетворяющий условиям 1 и 2, и добавление к нему заключительного правила не нарушит эти условия. Наконец, если заключительное правило – это ${\multimap}\mathrm{L}$, воспользуемся предположением индукции и вспомогательным утверждением. Наконец, достигнем выполнения условия 3. Пусть есть вывод без запрещенных правил, удовлетворяющий условиям 1 и 2. Введем добавочный параметр трансфинитной индукции – ординальную меру сложности. Эта мера введена в работе Пальки [9]. Мерой $\mu(\Pi\to A)$ секвенции $\Pi \to A$ назовем ординал $\dots+\omega^k \cdot c_k+\dots+\omega^2 \cdot c_2+\omega \cdot c_1+c_0$, где $c_i$ – число подформул сложности $i$ в секвенции $\Pi \to A$. (Сложность формулы измеряется как общее число вхождений связок и констант $0$ и $1$.) Будем вести индукцию по лексикографическому порядку на парах $(\beta,\mu)$, где $\beta$ – ранг вывода, а $\mu$ – мера целевой секвенции. Рассмотрим заключительное правило в данном выводе (случай аксиомы, в том числе $0\mathrm{L}$, тривиален). 1-й случай: применено правое правило. Тогда в силу условия 1 весь вывод состоит из правых правил, а левая часть состоит только из переменных и не содержит сложных формул и констант. Условие 3 выполнено автоматически. 2-й случай: применено одной из правил ${\cdot}\mathrm{L}$, ${+}\mathrm{L}$, ${}^* \mathrm{L}$ или $1\mathrm{L}$. В этом случае условие 3 также выполнено: заключительная секвенция его явно не нарушает, а секвенции в выводах посылок заключительного правила удовлетворяют ему по предположению индукции (эти выводы имеют меньший ранг). 3-й случай: применено правило ${\multimap}\mathrm{L}$ или одно из правил, работающих с ${!}$ : ${!}\mathrm{L}$, ${!}\mathrm{C}$, ${!}\mathrm{W}$. Если в левой части встречается константа 0, заменяем весь вывод на применение аксиомы $0\mathrm{L}$. Если в этой секвенции нет формул вида $B \cdot C$, $B+C$, $B^*$ или $1$, то вывод удовлетворяет условию 3, и доказательство завершено. Иначе все такие формулы также появляются в посылке заключительного правила ${!}\mathrm{L}$, ${!}\mathrm{C}$ или ${!}\mathrm{W}$, или в одной из посылок заключительного правила ${\multimap}\mathrm{L}$. Заметим, что в силу условия 2 во втором случае это обязательно вторая (правая) посылка ${\multimap}\mathrm{L}$. Поскольку вывод данной посылки удовлетворяют условиям 1–3, этот вывод завершается применением левого правила, вводящего данную формулу. Например, так выглядит завершение вывода для правил ${\multimap}\mathrm{L}$ и ${+}\mathrm{L}$: а вот так – для ${!}\mathrm{C}$ и ${+}\mathrm{L}$:Применим к каждой из этих посылок наше заключительное правило, например: Заметим, что ранг выводов этих секвенций не выше, чем ранг вывода исходной целевой секвенции. При этом ее ординальная мера $\mu$ строго меньше. (В частности, это верно и для правила ${}^* \mathrm{L}$: формулы $A^n$ вносят меньший вклад в $\mu$, чем $A^*$, поскольку последняя сложнее, и прибавляет $1$ к коэффиценту при более высокой степени $\omega$.) Таким образом, мы можем применить предположение индукции: либо строго уменьшился ранг, либо ранг сохранился, зато уменьшился второй параметр $\mu$. По предположению индукции полученные таким образом секвенции имеют выводы, удовлетворяющие условиям 1–3. Теперь применим правило, вводящее формулу нужного вида $B \cdot C$, $B+C$, $B^*$ или $1$, чтобы получить исходную целевую секвенцию. (В наших примерах это правило ${+}\mathrm{L}$.) Поскольку это левое правило, и при этом не ${\multimap}\mathrm{L}$, то для достроенного таким образом вывода сохраняются условия 1 и 2. Условие 3 теперь также выполнено внутри выводов посылок заключительного правила по предположению индукции, а заключительная секвенция выведена по требуемому правилу. Теорема 4 доказана. $\Box$ § 6. Кодирование счетчиковых машин6.1. Счетчиковые машиныВ отличие от некоммутативного случая [6], в коммутативном нет естественного способа кодировать упорядоченные последовательности символов (слова), что нужно для представления конфигураций машин Тьюринга. В связи с этим вместо машин Тьюринга или иных моделей вычислений, работающих со словами, мы используем счетчиковые машины, или машины Минского [17], которые оперируют натуральными числами. Идея использования счетчиковых машин не нова: в работе Линкольна и др. [14] они использовались для доказательства неразрешимости коммутативной линейной логики (с экспоненциальной модальностью), а в работе [18] – для коммутативной логики действий. Отметим, что для кодирования счетчиковых машин оказывается существенным использование операции сложения (также называемой дизъюнкцией или объединением). Кодирование же машин Тьюринга [6] использует по сути только умножение. То же наблюдается и для линейной логики [14], где вопрос о разрешимости мультипликативно-экспоненциального (т. е. без аддитивных дизъюнкции и конъюнкции) фрагмента в коммутативном случае остается открытым [19]. Напомним определение счетчиковых машин. Мы будем рассматривать только детерминированные машины. Определение 10. Зафиксируем конечное множество имен счетчиков $\mathcal{R}$ (например, $\mathcal{R}=\{ \mathsf{a}, \mathsf{b}, \mathsf{c} \}$ для машины с тремя счетчиками). Детерминированная счетчиковая машина $\mathtt{M}$ с множеством счетчиков $\mathcal{R}$ состоит из этого множества $\mathcal{R}$, конечного множества состояний $\mathcal{Q}$, в котором выделены начальное состояние $q_I \in \mathcal{Q}$ и множество конечных состояний $\mathcal{Q}_F \subset \mathcal{Q}$, и конечного множества инструкций $\mathcal{I}$ (т. е. $\mathtt{M}=(\mathcal{R}, \mathcal{Q}, q_I, \mathcal{Q}_F, \mathcal{I})$). Каждая инструкция имеет одну из следующих двух форм с соответствующим описанием ее действия (здесь $r \in \mathcal{R}$ – счетчик, $p,q,q_0 \in \mathcal{Q}$ – состояния):
Для каждого $p \in \mathcal{Q}-\mathcal{Q}_F$ множество $\mathcal{I}$ содержит ровно одну инструкцию с первым аргументом $p$; для $p \in \mathcal{Q}_F$ такой инструкции нет. (Это – условие детерминированности машины $\mathtt{M}$.) Определение 11. Конфигурацией счетчиковой машины $\mathtt{M}$ называется пара $\mathbf{c}=(p,v)$, где $p \in \mathcal{Q}$ – состояние, а $v \colon \mathcal{R} \to \mathbb{N}$ – функция, присваивающая значения счетчикам (поскольку $\mathcal{R}$ конечно, $v$ задается конечной таблицей). Конфигурация $\mathbf{c}_2$ является непосредственным последователем конфигурации $\mathbf{c}_1$, если $\mathbf{c}_2$ получается из $\mathbf{c}_1$ применением инструкции машины $\mathtt{M}$. За счет детерминированности, непосредственный последователь существует и единствен у любой конфигурации с $p \notin \mathcal{Q}_F$; у конфигурации вида $(q_F, v)$, где $q_F \in \mathcal{Q}_F$, непосредственного последователя нет. Машина $\mathtt{M}$ достигает конфигурации $\mathbf{c}_2$ из конфигурации $\mathbf{c}_1$, если существует цепочка конфигураций от $\mathbf{c}_1$ к $\mathbf{c}_2$, в которой каждая следующая является непосредственным последователем предыдущей. (В частности, цепочка может быть одноэлементной, т. е. машина достигает любую конфигурацию из нее же самой.) Конфигурацию счетчиковой машины будем записывать так:
$$
\begin{equation*}
(q, (\mathsf{a}_1 \mapsto k_1, \dots, \mathsf{a}_n \mapsto k_n)).
\end{equation*}
\notag
$$
При этом, если значение счетчика равно нулю, то в записи его можно опустить. Например, конфигурацию машины с $\mathcal{R}=\{ \mathsf{a}, \mathsf{b}, \mathsf{c}, \mathsf{d} \}$, при которой машина находится в состоянии $q$, а значения счетчиков $\mathsf{a}$, $\mathsf{b}$, $\mathsf{c}$, $\mathsf{d}$ равны $6$, $0$, $12$, $0$ соответственно, можно обозначить $(q, (\mathsf{a} \mapsto 6, \mathsf{c} \mapsto 12))$. В частности, запись $(q,())$ означает конфигурацию, в которой машина находится в состоянии $q$, а значения всех счетчиков равны нулю. Зафиксируем один из счетчиков $\mathsf{a} \in \mathcal{R}$, который будет использоваться для ввода-вывода. Определение 12. Машина $\mathtt{M}$ вычисляет частичную функцию $f \colon \mathbb{N} \dashrightarrow \mathbb{N}$, если для любого $x \in \mathbb{N}$ выполнено следующее. Аналогично можно определить вычисление функции нескольких переменных. Для этого фиксируется несколько счетчиков $\mathsf{a}_1, \dots, \mathsf{a}_n$, используемых для входных данных; при этом результат вычисления помещается в счетчик $\mathsf{a}=\mathsf{a}_1$. Определение 13. Машина $\mathtt{M}$ вычисляет частичную функцию $f \colon \mathbb{N}^n \dashrightarrow \mathbb{N}$, если для любых $x_1, \dots, x_n \in \mathbb{N}$ выполнено следующее. Для вычисления любой вычислимой (например, с помощью машины Тьюринга) частичной функции $f \colon \mathbb{N} \dashrightarrow \mathbb{N}$ одной переменной достаточно машин с тремя счетчиками ($\mathcal{R}=\{ \mathsf{a}, \mathsf{b}, \mathsf{c} \}$). Теорема 5 (М. Л. Минский, 1961; Р. Шрёппель, 1972). Частичная функция $f \colon \mathbb{N} \dashrightarrow \mathbb{N}$ вычислима тогда и только тогда, когда она вычисляется некоторой машиной $\mathtt{M}$ с тремя счетчиками и одноэлементным множеством завершающих состояний $\mathcal{Q}_F=\{q_F\}$. Идея этой теоремы, т. е. сведе́ния машин Тьюринга к счетчиковым машинам, принадлежит Минскому [17]. Более того, машины с двумя счетчиками также способны вычислять все вычислимые по Тьюрингу функции, однако для этого нужно специфическое кодирование входных и выходных значений. Поэтому удобнее использовать машины с тремя счетчиками. Детальное доказательство теоремы 5 дано в мемуаре Шрёппеля [20]. Теорему 5 легко обобщить на случай нескольких переменных: вычислимая функция $f \colon \mathbb{N}^n \dashrightarrow \mathbb{N}$ вычисляется машиной с $n+2$ счетчиками. Нам будет интересен случай $n=2$. Предложение 5. Частичная функция $h \colon \mathbb{N} \times \mathbb{N} \dashrightarrow \mathbb{N}$ вычислима тогда и только тогда, когда она вычисляется некоторой машиной с четырьмя счетчиками (два из которых используются для входных данных) и одноэлементным множеством завершающих состояний $\mathcal{Q}_F=\{q_F\}$. Зафиксируем следующее кодирование пар натуральных чисел (оно нам еще понадобится в дальнейшем): Легко видеть, что такое кодирование – это вычислимое в обе стороны взаимно однозначное соответствие между $\mathbb{N} \times \mathbb{N}$ и $\mathbb{N}$. Доказательство. Идея доказательства похожа на [18; лемма 2]. Пусть $\mathcal{R}=\{ \mathsf{a}, \mathsf{b}, \mathsf{c}, \mathsf{d} \}$, причем для входных данных используются первые два счетчика. По двум входным значениям $x$ и $y$, помещенным в счетчики $\mathsf{a}$ и $\mathsf{b}$, можно вычислить код их пары $[x,y]=(x+y) \cdot (x+y+1) / 2+x$. Это делается следующим образом. Будем уменьшать (jzdec) значение счетчика $\mathsf{a}$, пока он не обнулится, параллельно увеличивая (inc) значения счетчиков $\mathsf{b}$ и $\mathsf{d}$. Теперь счетчик $\mathsf{b}$ содержит значение $z=x+y$, счетчик $\mathsf{d}$ – значение $x$, остальные равны нулю. На трех счетчиках $\mathsf{a}$, $\mathsf{b}$, $\mathsf{c}$ вычисляем (по теореме 5, не трогая счетчик $\mathsf{d}$) значение $z \cdot (z+1) / 2$ в счетчике $\mathsf{a}$. Прибавляем к нему $x$, уменьшая значение $\mathsf{d}$ и параллельно увеличивая $\mathsf{a}$. Теперь все готово для вычисления функции $h' \colon [x,y] \mapsto h(x,y)$. (Если $h(x,y)$ не определено, то не определено и $h'([x,y])$. Напомним, что используемое кодирование пар является взаимно однозначным соответствием $\mathbb{N}$ и $\mathbb{N} \times \mathbb{N}$.) Действительно, счетчик $\mathsf{a}$ содержит значение $[x,y]$, остальные равны нулю. Функция $h'$ вычисляется на трех счетчиках $\mathsf{a}$, $\mathsf{b}$, $\mathsf{c}$ по теореме 5. $\Box$ Важным частным случаем функции двух переменных является универсальная функция. Чтобы ее определить, зафиксируем некоторое естественное кодирование трехсчетчиковых машин натуральными числами. Код машины $\mathtt{M}$ будем обозначать $\ulcorner\mathtt{M}\urcorner$. Универсальная функция $U \colon \mathbb{N} \times \mathbb{N} \dashrightarrow \mathbb{N}$ определяется так:
$$
\begin{equation*}
\begin{aligned} \, & U(\ulcorner\mathtt{M}\urcorner, x)=f_{{\mathtt{M}}}(x), && \text{если }f_{\mathtt{M}}(x)\text{ определено}; \\ & U(\ulcorner\mathtt{M}\urcorner, x)\text{ не определено}, && \text{если }f_{\mathtt{M}}(x)\text{ не определено}; \\ & U(w,x)\text{ не определено}, && \text{если }w\text{ не является корректным кодом} \\ & && \text{трехсчетчиковой машины}. \end{aligned}
\end{equation*}
\notag
$$
Эта функция вычислима, и в силу предложения 5 вычисляется некоторой фиксированной машиной $\mathtt{U}$ с четырьмя счетчиками и $\mathcal{Q}_F=\{ q_F \}$. Фиксация конкретной машины $\mathtt{U}$ позволит нам в дальнейшем получать результаты о сложности для фрагментов хорновых теорий с фиксированным множеством гипотез $\mathcal{H}$. Напомним связанные с функцией $U$ алгоритмические задачи, полные в соответствующих классах сложности. Задача останова – по данным $w$ и $x$ выяснить, определено ли $U(w,x)$ – является $\Sigma^0_1$-полной. Двойственная задача неостанова – выяснить, что $U(w,x)$ не определено – $\Pi^0_1$-полна. Более сложной является задача тотальности: по данному $w$ выяснить, верно ли, что $U(w,x)$ определено для всех $x$. Это известная $\Pi_2^0$-полная задача (см., например, [21; § B.II.3]). В дальнейшем (§ 8) нам понадобится также $\Pi^1_1$-полная задача проверки нётеровости графа на множестве $\mathbb{N}$, заданного вычислимым образом. 6.2. Кодирование четырехсчетчиковых машинОпишем теперь кодирование машины $\mathtt{M}$ с четырьмя счетчиками в языке коммутативных алгебр Клини. Считаем, что $\mathcal{R}=\{ \mathsf{a}, \mathsf{b}, \mathsf{c}, \mathsf{d} \}$, $\mathcal{Q}$ – множество состояний машины $\mathtt{M}$, и что множество переменных содержит все элементы $\mathcal{Q} \cup \mathcal{R}$ и дополнительно четыре элемента $z_\mathsf{a}$, $z_\mathsf{b}$, $z_\mathsf{c}$ и $z_\mathsf{d}$. Множество атомарных формул $\mathcal{H}_{\mathtt{M}}$ строится следующим образом:
Отметим, что множество $\mathcal{H}_{\mathtt{M}}$ не содержит итерации. В мультимножестве ${!}\mathcal{H}_{\mathtt{M}}$ окажутся, соответственно, линейные формулы следующих видов: ${!}(p \multimap (q \cdot r))$, ${!}((p \cdot r) \multimap q)$ и ${!}(p \multimap (q_0+ z_r))$. Введем также вспомогательный терм
$$
\begin{equation*}
Z=(z_\mathsf{a} \cdot \mathsf{b}^* \cdot \mathsf{c}^* \cdot \mathsf{d}^*) + (z_\mathsf{b} \cdot \mathsf{a}^* \cdot \mathsf{c}^* \cdot \mathsf{d}^*) + (z_\mathsf{c} \cdot \mathsf{a}^* \cdot \mathsf{b}^* \cdot \mathsf{d}^*) + (z_\mathsf{d} \cdot \mathsf{a}^* \cdot \mathsf{b}^* \cdot \mathsf{c}^*).
\end{equation*}
\notag
$$
Для удобства также введем обозначение $A^{{\bullet} n}=A \cdot \ldots \cdot A$ ($n$ раз), где $A$ – произвольная линейная формула. Это несколько странное обозначение связано с тем, что обозначение $A^n$ уже занято для последовательности из $n$ копий линейной формулы $A$. Запись $A^{{\bullet} 0}$ обозначает константу $1$, однако при умножении мы будем ее опускать: так, $B \cdot A^{{\bullet} 0}$ означает просто $B$. Сформулируем и докажем основное утверждение о кодировании работы четырехсчетчиковой машины. Теорема 6. Машина $\mathtt{M}$ достигает конфигурации $\mathbf{c}_2=(q_2, (\mathsf{a} \mapsto a_2, \mathsf{b} \mapsto b_2, \mathsf{c} \mapsto c_2, \mathsf{d} \mapsto d_2))$ из конфигурации $\mathbf{c}_1=(q_1, (\mathsf{a} \mapsto a_1, \mathsf{b} \mapsto b_1, \mathsf{c} \mapsto c_1, \mathsf{d} \mapsto d_1))$ тогда и только тогда, когда секвенция Наше кодирование сходно с использованным в работе Линкольна и др. [14]. В присутствии итерации Клини, однако, нам не нужно заниматься “сборкой мусора” при использовании инструкции jzdec и переменной $z_{r}$ ($r \in \mathcal{R}$). Эта переменная обозначает “псевдосостояние”, используемое для проверки равенства счетчика $r$ нулю. Остальные счетчики могут иметь произвольные значения (что соответствует итерации в формуле $Z$), и нам не нужно специально заботиться об их обнулении. 6.3. От вычисления к выводуНачнем с более простого направления “только тогда”, от вычисления на счетчиковой машине к выводимости секвенции. Для начала заметим, что секвенция
$$
\begin{equation*}
q, \mathsf{a}^a, \mathsf{b}^b, \mathsf{c}^c, \mathsf{d}^d \to q \cdot \mathsf{a}^{{\bullet} a} \cdot \mathsf{b}^{{\bullet} b} \cdot \mathsf{c}^{{\bullet} c} \cdot \mathsf{d}^{{\bullet} d}
\end{equation*}
\notag
$$
выводима (с помощью правила ${\cdot}\mathrm{R}$) для любой конфигурации $\mathbf{c}=(q, (\mathsf{a} \mapsto a, \mathsf{b} \mapsto b, \mathsf{c} \mapsto c, \mathsf{d} \mapsto d))$. Действуем индукцией по длине цепочки непосредственных последователей от $\mathbf{c}_1$ к $\mathbf{c}_2$. Если конфигурации $\mathbf{c}_1$ и $\mathbf{c}_2$ совпадают (основание индукции), имеем следующий вывод (здесь и далее двойная черта означает несколько применений правила): Шаг индукции: пусть цепочка от $\mathbf{c}_1$ к $\mathbf{c}_3$ начинается с шага от $\mathbf{c}_1$ к непосредственному последователю $\mathbf{c}_2$ и продолжается более короткой цепочкой от $\mathbf{c}_2$ к $\mathbf{c}_3$: Левая посылка правила сечения (от $\mathbf{c}_1$ к $\mathbf{c}_2$) будет обоснована ниже, а правая выводится следующим образом из предположения индукции (от $\mathbf{c}_2$ к $\mathbf{c}_3$):Итак, достаточно вывести данную секвенцию в случае, когда $\mathbf{c}_2$ – непосредственный последователь $\mathbf{c}_1$. Рассмотрим 3 случая, в зависимости от примененной инструкции. Во всех случаях будем без ограничения общности считать, что “активный” счетчик $r$ этой инструкции – это счетчик $\mathsf{a}$. Таким образом, $b_2=b_1$, $c_2=c_1$, $d_2=d_1$; обозначим эти значения $b$, $c$, $d$ соответственно. 1-й случай: $\mathbf{c}_2$ получается из $\mathbf{c}_1$ применением инструкции inc$(p, \mathsf{a}, q)$. В этом случае $q_1=p$, $q_2=q$, $a_2=a_1+1$. Мультимножество ${!}\mathcal{H}_\mathtt{M}$ содержит линейную формулу ${!}(p \multimap (q \cdot \mathsf{a}))$. Искомая секвенция выводится следующим образом: 2-й случай: $\mathbf{c}_2$ получается из $\mathbf{c}_1$ применением инструкции jzdec$(p, \mathsf{a}, q_0, q)$, причем $a_1 \ne 0$, т. е. $q_1=p$, $q_2=q$, $a_1= a_2+1$. Мультимножество ${!}\mathcal{H}_\mathtt{M}$ содержит линейную формулу ${!}((p \cdot \mathsf{a}) \multimap q)$, и искомая секвенция выводится так: 3-й случай (самый интересный): $\mathbf{c}_2$ получается из $\mathbf{c}_1$ применением инструкции jzdec$(p, \mathsf{a}, q_0, q)$, причем $a_1=0$. Тогда $q_1=p$, $q_2=q_0$ и $a_2=a_1=0$. Для начала выведем вспомогательную секвенцию: Теперь вспомним, что мультимножество ${!}\mathcal{H}_\mathtt{M}$ содержит линейную формулу ${!}(p \multimap (q_0+z_\mathsf{a}))$, и построим следующий вывод искомой секвенции: 6.4. От вывода к вычислениюДоказательству направления “тогда” в теореме 6 предпошлем следующее вспомогательное утверждение. Лемма 1. Пусть ${!}\mathcal{H}'$ – подмультимножество ${!}\mathcal{H}_\mathtt{M}$, а $\Pi$ – мультимножество линейных формул вида $A$, где ${!}A$ принадлежит ${!}\mathcal{H}_\mathtt{M}$. Тогда если секвенция где $C$ имеет вид $q_2 \cdot \mathsf{a}^{{\bullet} a_2} \cdot \mathsf{b}^{{\bullet} b_2} \cdot \mathsf{c}^{{\bullet} c_2} \cdot \mathsf{d}^{{\bullet} d_2}$, выводима, то $a=0$, и аналогично для $\mathsf{b}$, $\mathsf{c}$, $\mathsf{d}$. Доказательство. По теореме 4 у данной секвенции (так как она не содержит вхождений ${\multimap}$ и ${!}$ в положительной полярности) есть разбалансированный вывод. Рассуждаем индукцией по его длине7. Если заключительное правило этого вывода – это ${!}\mathrm{W}$, ${!}\mathrm{C}$ или ${!}\mathrm{L}$, сразу переходим к предположению индукции, потому что посылка такого правила имеет такой же вид, но при этом более короткий (меньшего ранга) вывод. Правила ${\cdot}\mathrm{L}$ и ${+} \mathrm{L}$ применены быть не могут, поскольку левая часть секвенции не содержит (“в чистом виде”) формул вида $E \cdot F$ и $E+F$.
Из левых правил остается ${\multimap}\mathrm{L}$, вводящее линейную формулу из мультимножества $\Pi$. Напомним, что формулы из $\Pi$ имеют вид $p \multimap (q \cdot r)$, $(p \cdot r) \multimap q_1$ или $p \multimap (q_0+z_r)$. В каждом из этих случаев левая посылка правила ${\multimap}\mathrm{L}$ будет иметь вид $\Phi \to p$ или $\Phi \to p \cdot r$, где $\Phi$ – подмультимножество ${!}\mathcal{H}'$, $\Pi$, $z_\mathsf{a}$, $\mathsf{a}^a$, $\mathsf{b}^b$, $\mathsf{c}^c$, $\mathsf{d}^d$. За счет условия 2 определения разбалансированного вывода, эта левая посылка выведена с использованием исключительно правых правил. Значит, $\Phi$ не может содержать сложных формул из ${!}\mathcal{H}'$ и $\Pi$. Но тогда $\Phi$ не содержит переменной $p$, и поэтому секвенция $\Phi \to p$ или $\Phi \to p \cdot r$ не может быть выводима (в выводе должна встретиться аксиома $p \to p$). Противоречие. Остается случай, когда секвенция ${!}\mathcal{H}', \Pi, z_\mathsf{a}, \mathsf{a}^a, \mathsf{b}^b, \mathsf{c}^c, \mathsf{d}^d \to C+Z$ выведена с использованием только правых правил. В этом случае ${!}\mathcal{H}'$ и $\Pi$ пусты. Заключительными правилами, в силу вида формулы $C+Z$, должны идти ${+}\mathrm{R}$. Более того, из суммы $C+Z$ нужно выбрать формулу $z_\mathsf{a} \cdot \mathsf{b}^* \cdot \mathsf{c}^* \cdot \mathsf{d}^*$, так как иначе не удастся получить аксиому $z_\mathsf{a} \to z_\mathsf{a}$. Таким образом, выводима секвенция
$$
\begin{equation*}
z_\mathsf{a}, \mathsf{a}^a, \mathsf{b}^b, \mathsf{c}^c, \mathsf{d}^d \to z_\mathsf{a} \cdot \mathsf{b}^* \cdot \mathsf{c}^* \cdot \mathsf{d}^*.
\end{equation*}
\notag
$$
Правая часть этой секвенции не содержит переменной $\mathsf{a}$, значит, ее не должно быть и слева (иначе не сможем получить аксиому $\mathsf{a} \to \mathsf{a}$), т. е. $a=0$, что и требовалось.
Случаи счетчиков $\mathsf{b}$, $\mathsf{c}$, $\mathsf{d}$ рассматриваются аналогично. $\Box$ Теперь мы готовы доказать направление “тогда” в теореме 6. Напомним, что нам дана выводимость секвенции
$$
\begin{equation*}
{!}\mathcal{H}_\mathtt{M}, q_1, \mathsf{a}^{a_1}, \mathsf{b}^{b_1}, \mathsf{c}^{c_1}, \mathsf{d}^{d_1} \to q_2 \cdot \mathsf{a}^{{\bullet} a_2} \cdot \mathsf{b}^{{\bullet} b_2} \cdot \mathsf{c}^{{\bullet} c_2} \cdot \mathsf{d}^{{\bullet} d_2}+Z,
\end{equation*}
\notag
$$
а требуется доказать, что машина $\mathtt{M}$ достигает конфигурации $\mathbf{c}_2=(q_2, (\mathsf{a} \mapsto a_2, \mathsf{b} \mapsto b_2, \mathsf{c} \mapsto c_2, \mathsf{d} \mapsto d_2))$ из конфигурации $\mathbf{c}_1=(q_1, (\mathsf{a} \mapsto a_1, \mathsf{b} \mapsto b_1, \mathsf{c} \mapsto c_1, \mathsf{d} \mapsto d_1))$. Для удобства рассуждения по индукции, как и в лемме 1, немного ослабим условие, предположив, что выводится секвенция вида
$$
\begin{equation*}
{!}\mathcal{H}', \Pi, q_1, \mathsf{a}^{a_1}, \mathsf{b}^{b_1}, \mathsf{c}^{c_1}, \mathsf{d}^{d_1} \to q_2 \cdot \mathsf{a}^{{\bullet} a_2} \cdot \mathsf{b}^{{\bullet} b_2} \cdot \mathsf{c}^{{\bullet} c_2} \cdot \mathsf{d}^{{\bullet} d_2}+Z,
\end{equation*}
\notag
$$
где ${!}\mathcal{H}'$ – подмультимножество ${!}\mathcal{H}_\mathtt{M}$, а формулы из $\Pi$ получаются из (некоторых) формул из ${!}\mathcal{H}_\mathtt{M}$ снятием знака ${!}$. Рассуждаем индукцией по длине разбалансированного вывода (вывод конечен) данной секвенции. Рассмотрим заключительное правило этого вывода. Как и в доказательстве леммы 1, случаи ${!}\mathrm{W}$, ${!}\mathrm{C}$ и ${!}\mathrm{L}$ сразу сводятся к предположению индукции, а случаи ${\cdot}\mathrm{L}$ и ${+}\mathrm{L}$ невозможны. Наиболее интересно правило ${\multimap}\mathrm{L}$, применение которого вводит некоторую формулу $A$ из $\Pi$. Рассмотрим три случая, в зависимости от вида формулы $A$. Без ограничения общности во всех случаях считаем, что $r=\mathsf{a}$. 1-й случай: $A=p \multimap (q \cdot \mathsf{a})$. Левая посылка правила ${\multimap} \mathrm{L}$ имеет вид $\Phi \to p$ и должна быть аксиомой: левые правила для ее вывода применять запрещено, а правые невозможно из-за тривиальности правой части. Отсюда следует, что $\Phi=p=q_1$, поскольку $q_1$ – единственная переменная в левой части, входящая в множество $\mathcal{Q}$. Кроме того, в силу разбалансированности (условие 3), правая посылка ${\multimap} \mathrm{L}$ выводится применением правила ${\cdot}\mathrm{L}$, вводящего формулу $q \cdot \mathsf{a}$. Таким образом, получаем следующий фрагмент вывода (здесь $\Pi=\Pi', q_1 \multimap (q \cdot \mathsf{a})$): Поскольку формула ${!}A={!}(q_1 \multimap (q \cdot \mathsf{a}))$ входит в мультимножество ${!}\mathcal{H}_0$, машина $\mathtt{M}$ содержит инструкцию inc$(q_1, \mathsf{a}, q)$. Следовательно, конфигурация $\mathbf{c}=(q, (\mathsf{a} \mapsto a_1+1, \mathsf{b} \mapsto b_1, \mathsf{c} \mapsto c_1, \mathsf{d} \mapsto d_1))$ является непосредственным последователем конфигурации $\mathbf{c}_1$. Кроме того, по предположению индукции из выводимости секвенции
$$
\begin{equation*}
{!}\mathcal{H}', \Pi, q, \mathsf{a}^{a_1+1}, \mathsf{b}^{b_1}, \mathsf{c}^{c_1}, \mathsf{d}^{d_1} \to q_2 \cdot \mathsf{a}^{{\bullet} a_2} \cdot \mathsf{b}^{{\bullet} b_2} \cdot \mathsf{c}^{{\bullet} c_2} \cdot \mathsf{d}^{{\bullet} d_2}+Z
\end{equation*}
\notag
$$
следует, что машина $\mathtt{M}$ достигает конфигурации $\mathbf{c}_2$ из конфигурации $\mathbf{c}$. Отсюда следует, что $\mathtt{M}$ достигает $\mathbf{c}_2$ из $\mathbf{c}_1$. 2-й случай: $A=(p \cdot \mathsf{a}) \multimap q$. Здесь левая посылка имеет вид $\Phi \to p \cdot \mathsf{a}$ и должна быть выведена с использованием только правых правил. Единственный возможный случай – $\Phi=p,\mathsf{a}$, т. е. левая посылка имеет вид $p,\mathsf{a} \to p \cdot \mathsf{a}$. В частности, имеем $p=q_1$, поскольку другие элементы $\mathcal{Q}$ не встречаются в левой части исходной секвенции. Кроме того, $a_1>0$, иначе в левой части не найдется переменной $\mathsf{a}$. Таким образом, получаем следующее применение правила ${\multimap}\mathrm{L}$: Это правило соответствует применению инструкции jzdec$(q_1, \mathsf{a}, q_0, q)$ (здесь $q_0$ – некое состояние, и оно не используется, так как $a_1>0$). Конфигурация $\mathbf{c}=(q, (\mathsf{a} \mapsto a_1-1, \mathsf{b} \mapsto b_1, \mathsf{c} \mapsto c_1, \mathsf{d} \mapsto d_1))$ является непосредственным последователем конфигурации $\mathbf{c}_1$, а из $\mathbf{c}$, в свою очередь, машина $\mathtt{M}$ достигает конфигурации $\mathbf{c}_2$ (предположение индукции). 3-й случай: $p \multimap (q_0+z_\mathsf{a})$. Здесь левая посылка ${\multimap}\mathrm{L}$ имеет вид $p \to p$, причем $p=q_1$, а за счет условия 3 разбалансированности вывода правая посылка выведена с помощью правила ${+}\mathrm{L}$: Здесь использовано сокращение $C_2=q_2 \cdot \mathsf{a}^{{\bullet} a_2} \cdot \mathsf{b}^{{\bullet} b_2} \cdot \mathsf{c}^{{\bullet} c_2} \cdot \mathsf{d}^{{\bullet} d_2}$.Применяем лемму 1: из выводимости секвенции ${!}\mathcal{H}', \Pi', z_\mathsf{a}, \mathsf{a}^{a_1}, \mathsf{b}^{b_1}, \mathsf{c}^{c_1}, \mathsf{d}^{d_1} \to C_2+ Z$ следует, что $a_1=0$. Значит, конфигурация $\mathbf{c}_1=(q_1, (\mathsf{a} \mapsto 0, \mathsf{b} \mapsto b_1, \mathsf{c} \mapsto c_1, \mathsf{d} \mapsto d_1))$ под действием инструкции jzdec$(q_1, \mathsf{a}, q_0, q)$ переходит в своего непосредственного последователя $\mathbf{c}=(q_0, (\mathsf{a} \mapsto 0, \mathsf{b} \mapsto b_1, \mathsf{c} \mapsto c_1, \mathsf{d} \mapsto d_1))$. С другой стороны, по предположению индукции из выводимости секвенции $\mathcal{H}', \Pi', q_0, \mathsf{b}^{b_1}, \mathsf{c}^{c_1}, \mathsf{d}^{d_1} \to C_2+Z$ получаем, что машина $\mathtt{M}$ достигает $\mathbf{c}_2$ из $\mathbf{c}$, а значит, и из $\mathbf{c}_1$. Теорема 6 полностью доказана. $\Box$ § 7. $\Pi_2^0$-полнота для случая гипотез без итерацииБудем применять наше кодирование (теорема 6) к универсальной машине $\mathtt{U}$ (см. п. 6.1). Считаем, что первый аргумент помещается в счетчик $\mathsf{a}$, а второй – в счетчик $\mathsf{b}$. Лемма 2. Пусть $w$ – натуральное число. Следующие утверждения равносильны. Доказательство. Равносильность утверждений 2 и 3 напрямую следует из теоремы 3. Докажем равносильность утверждений 1 и 2.
Сначала зафиксируем значение $x$. Утверждение, что $U(w,x)$ определено и равно нулю, равносильно (по определению вычисления функции на счетчиковой машине) тому, что машина $\mathtt{U}$ достигает конфигурации $(q_F, ())$ из конфигурации $(q_I, (\mathsf{a} \mapsto w, \mathsf{b} \mapsto x))$. По теореме 6 это равносильно выводимости секвенции
$$
\begin{equation*}
{!}\mathcal{H}_{\mathtt{U}}, q_I, \mathsf{a}^w, \mathsf{b}^x \to q_F+Z
\end{equation*}
\notag
$$
в исчислении $\boldsymbol{!}\mathbf{CommACT}_\omega$.
Если это верно для всех значений $x$, то по омега-правилу ${}^* \mathrm{L}$ получаем выводимость искомой секвенции ${!}\mathcal{H}_{\mathtt{U}}, q_I, \mathsf{a}^w, \mathsf{b}^* \to q_F+Z$. В обратную сторону: если эта секвенция выводима, то для произвольного значения $x$ с помощью правила сечения выводима ${!}\mathcal{H}_{\mathtt{U}}, q_I, \mathsf{a}^w, \mathsf{b}^x \to q_F+Z$: Отсюда получаем, что $U(w,x)$ определено и равно нулю. $\Box$ Теорема 7. Задача общезначимости хорновых формул с фиксированным не содержащим итерации множеством $\mathcal{H}=\mathcal{H}_{\mathtt{U}}$ на классе всех коммутативных $*$-непрерывных алгебр Клини $\Pi_2^0$-полна. Таков же и фрагмент хорновой теории коммутативных $*$-непрерывных алгебр Клини с гипотезами, не содержащими итерации. Доказательство. Верхняя оценка сложности следует из предложения 2, поскольку рассматриваемые множества гипотез не содержат итерации.
Для доказательства нижней оценки воспользуемся $\Pi^0_2$-трудностью задачи тотальности. Обычно задача тотальности формулируется так: по данному $w$ выяснить, верно ли, что $U(w,x)$ определено для всех $x$. Однако следующая задача также $\Pi^0_2$-трудна: по данному $w$ выяснить, верно ли, что $U(w,x)$ определено и равно нулю для всех $x$. Сведе́ние старой задачи к новой осуществляется с помощью функции, преобразующей код машины $w$ в код машины $w'$, в которую добавлена “сборка мусора” – обнуление счетчика $\mathsf{a}$ после достижения состояния $q_F$. Ясно, что эта функция вычислима, и имеет место следующая равносильность: $U(w,x)$ определено для всех $x$ тогда и только тогда, когда $U(w',x)$ определено и равно нулю для всех $x$. По лемме 2 для данного числа $w$ значение $U(w,x)$ определено и равно нулю для всех $x$ тогда и только тогда, когда хорнова формула $\mathcal{H}_\mathtt{U} \Rightarrow q_I \cdot \mathsf{a}^{{\bullet} w} \cdot \mathsf{b}^* \leqslant q_F+ Z$ общезначима на классе всех коммутативных $*$-непрерывных алгебр Клини. $\Box$ В качестве следствия получаем также новый результат о сложности в некоммутативном случае. Следствие 1. Существует такое конкретное конечное множество атомарных формул $\widetilde{\mathcal{H}}_0$ без итерации, что задача общезначимости хорновых формул с данным множеством $\widetilde{\mathcal{H}}_0$ как множеством гипотез на классе всех (не обязательно коммутативных) $*$-непрерывных алгебр $\Pi^0_2$-полна. Доказательство. Берем $\widetilde{\mathcal{H}}_0=\mathcal{H} \cup \mathcal{C}_V$, где $\mathcal{H}$ взято из предыдущей теоремы, а множество $\mathcal{C}_V$ строится, как описано в § 2, по множеству переменных $V=\mathcal{Q} \cup \{ \mathsf{a},\mathsf{b},\mathsf{c},\mathsf{d}, z_{\mathsf{a}}, z_{\mathsf{b}}, z_{\mathsf{c}}, z_{\mathsf{d}} \}$, где $\mathcal{Q}$ – множество состояний машины $\mathtt{U}$. По предложению 1 общезначимость хорновой формулы $\mathcal{H} \Rightarrow t \cdot \mathsf{a}^{{\bullet} n} \leqslant r+Z$ на классе всех коммутативных $*$-непрерывных алгебр Клини равносильна общезначимости хорновой формулы $\widetilde{\mathcal{H}}_0 \Rightarrow t \cdot \mathsf{a}^{{\bullet} n} \leqslant r+ Z$ на классе всех $*$-непрерывных алгебр Клини. $\Box$ Это следствие – вариант результата Козена [6; теорема 4.1(ii)], в котором вместо варьирующегося множества гипотез используется фиксированное. С другой стороны, результат Козена несколько сильнее, поскольку в нем в гипотезах нельзя использовать не только итерацию, но и операцию сложения. Получить усиление собственно результата Козена, т. е. $\Pi_2^0$-полноту с фиксированным множеством гипотез без итерации и сложения (в некоммутативном случае) также возможно. Для этого нужно повторить конструкцию Козена с использованием машин Тьюринга вместо счетчиковых машин (для кодирования машин Тьюринга не нужна операция сложения), применив ее к универсальной машине Тьюринга. Детальное изложение этого рассуждения, однако, выходит за рамки настоящей статьи. § 8. $\Pi^1_1$-полнота в общем случае8.1. Нётеровость для рекурсивно заданного графаДля доказательства $\Pi^1_1$-трудности хорновой теории (без ограничений) класса коммутативных $*$-непрерывных алгебр Клини мы, следуя идеям Козена [6], воспользуемся задачей о нётеровости для рекурсивно заданного бинарного отношения, или ориентированного графа без кратных ребер. (Далее понятия “бинарное отношение” и “граф” используются как взаимозаменяемые.) В качестве множества вершин такого графа используется множество натуральных чисел $\mathbb{N}$. Напомним основные определения. Определение 14. Бинарное отношение $R \subseteq \mathbb{N} \times \mathbb{N}$ называется фундированным (артиновым), если не существует бесконечно убывающей цепочки $(m_0, m_1,\dots)$ такой, что $(m_{i+1}, m_i) \in R$. Отношение $R$ называется нётеровым, если не существует бесконечной возрастающей цепочки $(m_0, m_1,\dots)$, где $(m_i, m_{i+1}) \in R$ (т. е. обратное отношение $R^{-1}$ артиново). Заметим, что такому определению могут удовлетворять только иррефлексивные отношения. В частности, если в качестве $R$ берется частичный порядок, то он должен быть строгим. Также нам понадобится “локальная” версия нётеровости для данного элемента. Определение 15. Для данного отношения $R \subseteq \mathbb{N} \times \mathbb{N}$ множество $\mathsf{WF}_R$ определяется так: $n \in \mathsf{WF}_R$, если не существует начинающейся с числа $n$ бесконечной возрастающей цепочки $(n, m_1, m_2, \dots)$. Нас будут интересовать рекурсивно заданные графы, т. е. такие, для которых существует алгоритм, проверяющий принадлежность пары $(n,m)$ соответствующему отношению. Классическое определение рекурсивного отношения следующее. Определение 16. Бинарное отношение $R \subseteq \mathbb{N} \times \mathbb{N}$ называется рекурсивным, если его характеристическая функция вычислима. Рекурсивные бинарные отношения задаются всюду определенными вычислимыми функциями $G \colon \mathbb{N} \times \mathbb{N} \to \{0,1\}$. В дальнейшем, однако, мы будем пользоваться универсальной вычислимой функцией $U$, для которой существенна ее частичность. (В частности, ее невозможно вычислимым образом достроить до всюду определенной.) Поэтому нам будет удобно обобщить понятие рекурсивного бинарного отношения на случай частичной функции $G \colon \mathbb{N} \times \mathbb{N} \dashrightarrow \{ 0,1 \}$. Такая функция определяет “нечеткий”, или трехзначный граф с множеством вершин $\mathbb{N}$. Определение 17. Пусть $G \colon \mathbb{N} \times \mathbb{N} \dashrightarrow \{0,1\}$ – вычислимая частичная функция. Будем говорить, что $G$ задает рекурсивный трехзначный граф (обозначаемый той же буквой) на множестве $\mathbb{N}$, и использовать следующую терминологию для его ребер. Обозначим множества определенно присутствующих, определенно отсутствующих и имеющих неопределенный статус ребер через $G^{+}$, $G^{-}$ и $G^{?}$ соответственно. Соответственно подправим и определение множества $\mathsf{WF}$ (локальная нётеровость). Определение 18. Пусть $G$ – рекурсивный трехзначный граф. Тогда $n \in \mathsf{WF}_G$, если не существует ни бесконечной цепочки $(n=m_0, m_1, \dots)$ такой, что $(m_i, m_{i+1}) \in G^{+}$ для всех $i$, ни цепочки $(n=m_0, m_1, \dots, m_s, k)$ такой, что $(m_i, m_{i+1}) \in G^{+}$ для $i<s$ и $(m_s, k) \in G^{?}$. Иначе говоря, любая бесконечная последовательность чисел, начинающаяся с $n$, имеет начало следующего вида: $(n,m_1) \in G^+$, …, $(m_{i-1}, m_i) \in G^+$, $(m_i, m_{i+1}) \in G^-$ (для некоторого $i \geqslant 0$) – проходит по ребрам из $G^+$ и “обрывается” ребром из $G^-$. (“Обрыв” может случиться и сразу, на первом шаге.) Теперь мы готовы сформулировать эталонную $\Pi_1^1$-полную задачу, которую мы будем сводить к хорновой теории коммутативных $*$-непрерывных алгебр Клини. Теорема 8. Существует такой рекурсивный трехзначный граф $G_0$, что множество $\mathsf{WF}_{G_0}$ (для данного конкретного $G_0$) является $\Pi_1^1$-полным. Напомним, что класс сложности $\Pi_1^1$ определяется следующим образом. Множество $A \subseteq \mathbb{N}$ принадлежит классу, если найдется такая арифметическая формула $\varphi(n, X)$ со свободными параметрами $n$ по числам и $X$ по множествам чисел, что
$$
\begin{equation*}
n \in A \quad\Longrightarrow\quad \mathbb{N} \vDash \forall X \, \varphi(n,X).
\end{equation*}
\notag
$$
Множество $\mathsf{WF}_{G_0}$ допускает такое описание: в качестве внешнего квантора “$\forall\, X$” берется квантор по всем бесконечным цепочкам, начинающимся с числа $n$ (такая цепочка может быть закодирована как множество пар $(i,m_i)$), а их требуемое свойство – существует такое натуральное $i$, что $(m_i, m_{i+1}) \in G^{-}_0$ и $(m_j, m_{j+1}) \in G^{+}_0$ для всех $j<i$ – уже является арифметическим за счет вычислимости $G_0$. Таким образом, верхняя оценка сложности $\mathsf{WF}_{G_0}$ получена, и интерес представляет нижняя оценка, т. е. $\Pi_1^1$-трудность. Для нижней оценки нам понадобится следующая теорема о характеризации $\Pi_1^1$-множеств, которая получается из результатов Клини [22] и Спектора [23] (формулировка дана по книге Одифредди [24; теорема IV.2.20]). Теорема 9 (С. К. Клини, К. Спектор, 1955). Множество $A \subseteq \mathbb{N}$ принадлежит классу сложности $\Pi_1^1$ тогда и только тогда, когда найдется такая рекурсивная последовательность $\{ \prec_x \mid x \in \mathbb{N} \}$ рекурсивных линейных порядков, что Уточним, что значит “рекурсивная последовательность рекурсивных линейных порядков”. Неформально это означает, что некоторая вычислимая функция $f$ по каждому $x \in \mathbb{N}$ возвращает код алгоритма, вычисляющий некоторую функцию $h_x \colon \mathbb{N} \times \mathbb{N} \to \{ 0,1 \}$; при этом (внешним образом) известно, что $h_x$ – это характеристическая функция линейного порядка. (В частности, $h$ всюду определена.) Более точное определение дается через универсальную функцию: (Заметим, для того чтобы использовать ранее введенную универсальную функцию от двух переменных, мы “упаковали” два аргумента $n$ и $m$ в код пары $[n,m]$.) При этом от функции $f$ внешним образом требуется, чтобы так определенные функции $h_x$ для всех $x \in \mathbb{N}$ были всюду определенными и являлись характеристическими функциями линейных порядков.Таким образом, теорема 9 (точнее, ее интересное направление “только тогда”) может быть переформулирована следующим образом. Пусть множество $A \in \mathbb{N}$ принадлежит классу сложности $\Pi_1^1$. Тогда найдется такая вычислимая всюду определенная функция $f \colon \mathbb{N} \to \mathbb{N}$, что:
Для удобства дальнейшего изложения перейдем от фундированности (артиновости) отношения $\prec_x$ к нётеровости отношения $\succ_{\! x}$, а также принудительно добавим к каждому из порядков наибольший элемент, численное значение которого равно нулю. Это достигается следующей модификацией функций $h_x$:
$$
\begin{equation*}
h'_x(n,m) = \begin{cases} h_x(m-1,n-1), &\text{если }m,n>0, \\ 1, &\text{если }n=0,m>0, \\ 0, &\text{если }m=0. \end{cases}
\end{equation*}
\notag
$$
Имеем $x \in A$ тогда и только тогда, когда отношение $\succ'_{\! x}$ с характеристической функцией $h'_x$ нётерово, причем это верно тогда и только тогда, когда в этом порядке не существует бесконечной цепочки $n_0 \succ'_{\! x} n_1 \succ'_{\! x} n_2 \succ'_{\! x} \cdots$, начинающейся с нуля ($n_0=0$), иначе говоря, когда $0 \in \mathsf{WF}_{\succ'_{\!x}}$. Теперь мы готовы определить искомый рекурсивный трехзначный граф $G_0$. А именно, он задается следующей функцией $G_0$ двух аргументов, причем оба аргумента воспринимаются как коды пар чисел (напомним, что кодирование пар задает вычислимую биекцию между $\mathbb{N}$ и $\mathbb{N} \times \mathbb{N}$):
$$
\begin{equation*}
G_0([w, n], [w', m]) = \begin{cases} U(w,[m-1,n-1]), &\text{если }w'=w\text{ и }m,n>0, \\ 1, &\text{если }w'=w\text{ и }n=0,\ m>0, \\ 0, &\text{если }m=0\text{ или }w' \ne w. \end{cases}
\end{equation*}
\notag
$$
Заметим, что эта функция уже не будет всюду определенной. Докажем, что множество $\mathsf{WF}_{G_0}$ является $\Pi_1^1$-трудным, для чего построим сведе́ние к нему произвольного множества $A$ из класса $\Pi_1^1$. По теореме 9, в приведенной выше переформулировке, найдем соответствующую множеству $A$ функцию $f$. Поскольку $f$ вычислима, существует такое $p \in \mathbb{N}$ (здесь $p$ зависит только от выбора $A$), что для любого $x \in \mathbb{N}$ имеем В качестве искомой сводящей функции выберем функцию $g$, заданную равенством Эта функция всюду определена и вычислима, поскольку такова $f$. Докажем, что
$$
\begin{equation*}
g(x) \in \mathsf{WF}_{G_0} \quad\Longrightarrow\quad x \in A.
\end{equation*}
\notag
$$
Действительно, при фиксированном $w=U(p,x)$ в графе $G_0$ имеется изолированная компонента $G_0^{(w)}$ с множеством вершин $\{ [w,n] \mid n \in \mathbb{N} \}$. “Наружу” из этой компоненты ребра определенно отсутствуют: $G_0([w,n], [w',m])=0$ при $w' \ne w$. Сама же компонента $G_0^{(w)}$, поскольку $G_0([w,n],[w,m])=h'_x(n,m)$, изоморфна графу $(\mathbb{N}, \succ'_{\! x})$. (В частности, если $w$ имеет вид $U(p,x)$, где $p$ найдено по множеству $A$ и теореме 9, то внутри $G_0^{(w)}$ нет неопределенных ребер.) Таким образом, $g(x)=[U(p,x),0]=[w,0] \in \mathsf{WF}_{G_0}$ тогда и только тогда, когда в $0 \in \mathsf{WF}_{\succ'_{\! x}}$, т. е. когда порядок $\succ'_{\! x}$ нётеров (так как $0$ – наибольший элемент). Это же, в свою очередь, равносильно $x \in A$. Теорема 8 доказана. $\Box$ 8.2. Кодирование принадлежности множеству $\mathsf{WF}_{G_0}$Теперь для доказательства нужных результатов о $\Pi_1^1$-трудности достаточно построить сведе́ние принадлежности множеству $\mathsf{WF}_{G_0}$ к выводимости специально построенной секвенции в $\boldsymbol{!}\mathbf{CommACT}_\omega$. Для удобства будем считать, следуя Козену [6], что четырехсчетчиковая машина $\mathtt{G}_0$ задает граф $G_0$ следующим образом. У машины $\mathtt{G}_0$ есть одно начальное состояние $q_I=s$ и два завершающих состояния: $\mathcal{Q}_F=\{ r, t \}$. Машина $\mathtt{G}_0$ стартует с конфигурации $(s, (\mathsf{a} \mapsto n, \mathsf{b} \mapsto m))$ и работает следующим образом:
Построить такую $\mathtt{G}_0$ несложно: если вычислима функция $G_0$, то вычислима и функция $G'_0$, задаваемая равенством $G'_0(n,m)=(m+1) \cdot G_0(n,m)$ (причем, если не определено $G_0(n,m)$, то не определено и $G'_0(n,m)$). По предложению 5 эта функция вычисляется некоторой четырехсчетчиковой машиной с единственным завершающим состоянием $q_F$. Искомая машина $\mathtt{G}_0$ получается добавлением новых состояний $r,t$ и проверки на равенство нулю (при этом в случае неравенства как раз получается $\mathsf{a} \mapsto m$): jzdec$(q_F, \mathsf{a}, r, t)$. Положим
$$
\begin{equation*}
\mathcal{H}=\mathcal{H}_{\mathtt{G}_0} \cup \{ t \leqslant s \cdot \mathsf{b}^* \}.
\end{equation*}
\notag
$$
Теорема 10. Пусть $n$ – натуральное число. Следующие условия равносильны. Доказательство. Как и в доказательстве леммы 2, интерес представляет равносильность первого и второго утверждений; второе же и третье равносильны по теореме 3.
Далее в рамках этого доказательства вместо $\mathsf{WF}_{G_0}$ будем писать просто $\mathsf{WF}$. Начнем с импликации $1 \Rightarrow 2$. Для начала отметим, что на множестве $\mathsf{WF}$ можно вести трансфинитную индукцию по трехзначному графу $G_0$ следующим образом. Пусть $\psi(x)$ – некоторое утверждение о натуральных числах. Тогда если
$$
\begin{equation*}
\forall\, n \in \mathsf{WF} \ \bigl((\forall\, m \in \mathbb{N} \ ((n,m) \in G_0^{+} \Rightarrow \psi(m))) \Rightarrow \psi(n) \bigr),
\end{equation*}
\notag
$$
то $\forall\, n \in \mathsf{WF} \;\; \psi(n)$. Иначе говоря, при доказательстве утверждения $\psi(n)$ для $n \in \mathsf{WF}$ можно пользоваться как предположением индукции, истинностью $\psi(m)$ для всех $m$, в которые из $n$ ведет определенно присутствующее в графе $G_0$ ребро.
Действительно, если бы такой принцип индукции был неверен, то нашлось бы $n \in \mathsf{WF}$, для которого неверно $\psi(n)$. Но тогда есть также $m_1$ такое, что $(n,m_1) \in G_0^{+}$ (и, значит, $m_1 \in \mathsf{WF}$) и неверно $\psi(m_1)$, и далее $m_2$, $m_3$, …, что дает бесконечную цепь, нарушающую определение $\mathsf{WF}$. Пусть $n \in \mathsf{WF}$. Докажем утверждение $\psi(n) =$ “секвенция ${!}\mathcal{H}, t, \mathsf{a}^n \to r+Z$ выводима” с помощью описанного выше принципа индукции по $G_0$ на $\mathsf{WF}$. Для любого натурального $m$ имеем либо $(n,m) \in G_0^{-}$ (ребро из $n$ в $m$ определенно отсутствует), либо $(n,m) \in G_0^{+}$ (ребро определенно есть), причем во втором случае мы можем пользоваться утверждением $\psi(m)$ как данным предположением индукции. В частности, по определению $\mathsf{WF}$ невозможно $(n,m) \in G_0^{?}$. (А также заведомо $(n,n) \in G_0^{-}$, иначе получается бесконечная цепочка $n,n,n,\dots$ – таким образом, не возникает ситуации “порочного круга”, когда $\psi(n)$ предлагается вывести из него же самого.) Мультимножество ${!}\mathcal{H}$ содержит линейную формулу $t \multimap (s \cdot \mathsf{b}^*)$. Начнем вывод искомой секвенции ${!}\mathcal{H}, t, \mathsf{a}^n \to r+Z$ следующим образом: Остается вывести секвенции ${!}\mathcal{H}, s, \mathsf{a}^n, \mathsf{b}^m \to r+Z$ для каждого $m$ (при фиксированном $n$). Как отмечено выше, возможны два случая. 1-й случай: $(n,m) \in G_0^{-}$ (ребра определенно нет). Тогда счетчиковая машина $\mathtt{G}_0$ достигает конфигурации $(r, ())$ из конфигурации $(s, (\mathsf{a} \mapsto n, \mathsf{b} \mapsto m))$. По теореме 6 выводима секвенция ${!}\mathcal{H}_{\mathtt{G}_0}, s, \mathsf{a}^n, \mathsf{b}^m \to r+Z$. Теперь требуемую секвенцию ${!}\mathcal{H}, s, \mathsf{a}^n, \mathsf{b}^m \to r+Z$ можно вывести по правилу ${!}\mathrm{W}$ (ослабления), добавив к ${!}\mathcal{H}_{\mathtt{G}_0}$ недостающую линейную формулу ${!}(t \multimap (s \cdot \mathsf{b}^*))$. 2-й случай: $(n,m) \in G_0^{+}$, причем в этом случае для $m$ выполнено предположение индукции – выводима секвенция Также по теореме 6 выводима секвенция поскольку машина $\mathtt{G}_0$ достигает конфигурации $(t, (\mathsf{a} \mapsto m))$ из конфигурации $(s, (\mathsf{a} \mapsto n, \mathsf{b} \mapsto m))$. Теперь требуемую секвенцию можно вывести следующим образом:Теперь докажем импликацию $2 \Rightarrow 1$. Для начала установим аналог леммы 1. Лемма 3. Пусть ${!}\mathcal{H}'$ – подмультимножество ${!}\mathcal{H}$, а $\Pi$ – мультимножество линейных формул, полученных снятием знака ${!}$ с (некоторых) формул из ${!}\mathcal{H}$. Тогда если секвенция где $C$ имеет вид $q_2 \cdot \mathsf{a}^{{\bullet} a_2} \cdot \mathsf{b}^{{\bullet} b_2} \cdot \mathsf{c}^{{\bullet} c_2} \cdot \mathsf{d}^{{\bullet} d_2}$, выводима, то $a=0$. Аналогично для $\mathsf{b}$, $\mathsf{c}$, $\mathsf{d}$. Доказательство. Рассуждение повторяет доказательство леммы 1 с точностью до небольшого изменения, связанного с возможным присутствием в ${!}\mathcal{H}'$ линейной формулы ${!}(t \multimap (s \cdot \mathsf{b}^*))$ или в $\Pi$ линейной формулы $t \multimap (s \cdot \mathsf{b}^*)$. За счет этого теоретически в выводе может использоваться правило ${}^* \mathrm{L}$, и вывод может стать бесконечным. Вместо обыкновенной индукции используем трансфинитную индукцию по рангу разбалансированного (теорема 4) вывода. Единственный добавочный, по сравнению с леммой 1, случай – это применение правила ${\multimap}\mathrm{L}$, вводящее формулу $t \multimap (s \cdot \mathsf{b}^*)$. Левая посылка этого правила (за счет разбалансировки) имеет вид $t \to t$, поэтому $t$ должна входить в левую часть исходной секвенции. Это, однако, не так. Остальные случаи рассматриваются так же, как и в доказательстве леммы 1. $\Box$ Вернемся к доказательству импликции $2 \Rightarrow 1$ в теореме 10. Будем доказывать трансфинитной индукцией по рангу разбалансированного (теорема 4) вывода одновременно следующие два утверждения. Здесь, как и в лемме 3, ${!}\mathcal{H}'$ – подмультимножество ${!}\mathcal{H}$ и $\Pi$ – мультимножество линейных формул, полученных снятием знака ${!}$ с формул из ${!}\mathcal{H}$.
За счет разбалансированности выводов данных секвенций их заключительные правила являются левыми, за исключением второго утверждения с $q=r$. Действительно, иначе ${!}\mathcal{H}'$ и $\Pi$ обязаны быть пустыми, и окажется, что переменная $t$ или $q$ слева не имеет пары справа. Как и ранее, случаи правил ${!}\mathrm{L}$, ${!}\mathrm{W}$, ${!}\mathrm{C}$ для обоих утверждений разбираются непосредственным переходом к предположению индукции. (Их посылки имеют тот же вид, что и заключение, и при этом меньший ранг.) Поскольку главной связкой всех составных формул из $\Pi$ является $\multimap$, остается только случай правила ${\multimap}\mathrm{L}$. Пусть это правило вводит некоторую формулу $A$. При этом ${!}A$ лежит в ${!}\mathcal{H}$. Начнем с утверждения 1. Покажем, что случаи $A=p \multimap (q \cdot u)$, $A=(p \cdot u) \multimap q$ и $A=p \multimap (q_0+z_{u})$, где $u \in \{ \mathsf{a}, \mathsf{b}, \mathsf{c}, \mathsf{d} \}$, невозможны. Действительно, $t$ является одним из завершающих состояний машины $\mathtt{G}_0$. Следовательно, у машины $\mathtt{G}_0$ нет инструкции с первым параметром $t$, откуда $p \ne t$. В силу разбалансировки левая посылка правила ${\multimap} \mathrm{L}$ должна иметь вид $p \to p$ или $p, u \to p \cdot u$, однако в левой части заключения нет переменной $p$. Противоречие. Остается случай $A=t \multimap (s \cdot \mathsf{b}^*)$. За счет разбалансировки (условие 2) левая посылка – это $t \to t$. Кроме того (условие 3), заключительные правила в выводе правой посылки – это ${}^*\mathrm{L}$ и ${\cdot}\mathrm{L}$: Каждая посылка омега-правила ${}^*\mathrm{L}$ имеет меньший ранг, чем целевая секвенция. Применим к каждой из них утверждение 2 предположения индукции. (Заметим, что конфигурация $\mathbf{c}_0=(s, (\mathsf{a} \mapsto n, \mathsf{b} \mapsto m))$ достижима из самой себя.) Получим, что для любого $m$ либо $(n,m) \in G_0^{-}$, либо $(n,m) \in G_0^{+}$ и $m \in \mathsf{WF}$. Отсюда получаем $n \in \mathsf{WF}$. Перейдем к утверждению 2. Дано, что выводима секвенция
$$
\begin{equation*}
{!}\mathcal{H}', \Pi, q, \mathsf{a}^a, \mathsf{b}^b, \mathsf{c}^c, \mathsf{d}^d \to r+Z,
\end{equation*}
\notag
$$
причем машина $\mathtt{G}_0$ достигает конфигурации $\mathbf{c}=(q, (\mathsf{a} \mapsto a, \mathsf{b} \mapsto b, \mathsf{c} \mapsto c, \mathsf{d} \mapsto d))$ из начальной конфигурации вида $\mathbf{c}_0=(s, (\mathsf{a} \mapsto n, \mathsf{b} \mapsto m))$. Рассмотрим три случая. 1-й случай: $q \notin \{ r,t \}$, т. е. $q$ – не завершающее состояние. Рассмотрим заключительное правило вывода – оно обязано быть левым (правые правила применяться не могут, поскольку в правой части секвенции нет $q$). Интерес представляет правило ${\multimap}\mathrm{L}$; случаи правил, оперирующих с ${!}$ , тривиальны. Кроме того, правило ${\multimap}\mathrm{L}$ не может ввести формулу $t \multimap (s \cdot \mathsf{b}^*)$, поскольку в левой части целевой секвенции нет переменной $t$. Значит, она вводит одну из формул из ${!}\mathcal{H}_{\mathtt{G}_0}$ (со снятым знаком ${!}$). Рассуждая, как в доказательстве теоремы 6 (п. 6.4), получаем, что целевая секвенция выведена из секвенции вида
$$
\begin{equation*}
{!}\mathcal{H}', \Pi', q', \mathsf{a}^{a'}, \mathsf{b}^{b'}, \mathsf{c}^{c'}, \mathsf{d}^{d'} \to r+Z,
\end{equation*}
\notag
$$
причем конфигурация $\mathbf{c}'=(q', (\mathsf{a} \mapsto a', \mathsf{b} \mapsto b', \mathsf{c} \mapsto c', \mathsf{d} \mapsto d'))$ является непосредственным последователем конфигурации $\mathbf{c}$. Применяем предположение трансфинитной индукции: ранг вывода новой секвенции меньше, чем исходной, а новая конфигурация $\mathbf{c}'$ достижима из $\mathbf{c}_0$ (посредством $\mathbf{c}$). Получаем, что из конфигурации $\mathbf{c}'$, а значит, и из $\mathbf{c}$, машина $\mathtt{G}_0$ достигает одной из финальных конфигураций – либо $(r,())$, либо $(t,(\mathsf{a} \mapsto m))$, причем во втором случае $m \in \mathsf{WF}$. 2-й случай: $q=r$. Поскольку машина $\mathtt{G}_0$ достигла конфигурации $\mathbf{c}= (r, (\mathsf{a} \mapsto a, \mathsf{b} \mapsto b, \mathsf{c} \mapsto c, \mathsf{d} \mapsto d))$ из начальной конфигурации $\mathbf{c}_0$, имеем $a=b=c=d=0$. Значит, рассматриваемая секвенция имеет вид ${!}\mathcal{H}', \Pi, r \to r+Z$. Машина $\mathtt{G}_0$ из конфигурации $\mathbf{c}=(r,())$ достигает $(r,())$, т. е. той же конфигурации, что и требовалось. 3-й случай: $q=t$. Опять же, поскольку $\mathtt{G}_0$ достигла конфигурации $\mathbf{c}=(t, (\mathsf{a} \mapsto a, \mathsf{b} \mapsto b, \mathsf{c} \mapsto c, \mathsf{d} \mapsto d))$ из $\mathbf{c}_0$, имеем $b=c=d=0$ и $a=m$. Рассматриваемая секвенция имеет вид По утверждению 1 (доказано выше) имеем $m \in \mathsf{WF}$. При этом машина $\mathtt{G}_0$ достигает конфигурации $\mathbf{c}=(t, (\mathsf{a} \mapsto m))$ из нее же самой.Импликация $2 \Rightarrow 1$ в теореме 10 получается применением утверждения 1 к $\mathcal{H}'=\mathcal{H}$ и пустому $\Pi$. $\Box$ 8.3. Результаты о $\Pi_1^1$-полнотеПрименим теперь изложенную выше конструкцию для доказательства результатов о $\Pi_1^1$-полноте. Теорема 11. Существует такое конкретное конечное множество атомарных формул $\mathcal{H}$, что задача общезначимости хорновых формул с данным множеством $\mathcal{H}$ как множеством гипотез на классе всех коммутативных $*$-непрерывных алгебр Клини $\Pi_1^1$-полна. Следовательно, такова и вся хорнова теория класса всех коммутативных $*$-непрерывных алгебр Клини. Доказательство. Возьмем в качестве искомого множество $\mathcal{H}$ из п. 8.2. В силу теоремы 10 общезначимость хорновой формулы $\mathcal{H} \Rightarrow t \,{\cdot}\, \mathsf{a}^{{\bullet} n} \leqslant r\,{+}\,Z$ равносильна $n \in \mathsf{WF}_{G_0}$. Задача же проверки принадлежности множеству $\mathsf{WF}_{G_0}$, при подходящем выборе рекурсивного трехзначного графа $G_0$, является $\Pi_1^1$-полной по теореме 8. Таким образом, устанавливается $\Pi_1^1$-трудность задачи общезначимости хорновых формул с данным $\mathcal{H}$. Верхняя же оценка устанавливается предложением 2. $\Box$ Следствие 2. Задача выводимости в исчислении $\boldsymbol{!}\mathbf{CommACT}_\omega$ $\Pi_1^1$-полна. Это следствие распространяет результат работы [12] на коммутативный случай. Отметим, однако, что в работе [12] рассматривались субэкспоненциальные модальности, и для $\Pi_1^1$-трудности достаточно было модальности с правилом сокращения (в нелокальной форме), а перестановки и ослабления не требовалось. Аналогичным образом и в коммутативном случае можно доказать $\Pi_1^1$ для варианта исчисления $\boldsymbol{!}\mathbf{CommACT}_\omega$ c “релевантной” модальностью ${!}$ , для которой есть правила ${!}\mathrm{L}$, ${!}\mathrm{R}$, ${!}\mathrm{C}$, но не ${!}\mathrm{W}$. Для этого достаточно в мультимножество ${!}\mathcal{H}$ добавить, в пару с каждой имеющейся там формулой ${!}A$, формулу ${!}(({!}A) \multimap 1)$. Правила ${\multimap}\mathrm{L}$ и ${1}\mathrm{L}$ будут симулировать правило ${!}\mathrm{W}$. Следствие 3. Первопорядковая (элементарная) теория класса коммутативных $*$-непрерывных алгебр Клини $\Pi_1^1$-полна. Здесь нижняя оценка следует из того, что хорнова теория является консервативным фрагментом первопорядковой. Верхняя же оценка получается из того факта, что первопорядковую теорию можно аксиоматизировать с помощью исчисления с омега-правилом, для которого есть общий результат о верхней $\Pi_1^1$-оценке (см. [12]; при этом конкретный вид исчисления несуществен). Следствие 4. Существует такое конкретное конечное множество атомарных формул $\widetilde{\mathcal{H}}$, что задача общезначимости хорновых формул с данным множеством $\widetilde{\mathcal{H}}$ как множеством гипотез на классе всех (не обязательно коммутативных) $*$-непрерывных алгебр Клини $\Pi_1^1$-полна. Последнее следствие усиливает соответствующий результат Козена [6; теорема 5.1], который утверждает $\Pi_1^1$-полноту только для изменяющегося множества гипотез.
Цитирование в формате AMSBIB
\RBibitem{Kuz24} |
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
Обратная связь: |
Пользовательское соглашение
|
Регистрация посетителей портала |
Логотипы |
|