"Алгоритмические вопросы для субструктурных логик с итерацией Клини" тема диссертации и автореферата по ВАК РФ 00.00.00, доктор наук Кузнецов Степан Львович

• Кузнецов Степан Львович
• доктор наук
• 2024

Оглавление диссертации доктор наук Кузнецов Степан Львович

1.5 Выводимые правила

1.6 Вопросы алгоритмической сложности

1.7 Правило декомпозиции и моноиды Клини с делениями

1.8 Секвенция, различающая ACT и ACT^

1.9 Исчисления с непустыми антецедентами

1.10 Правило декомпозиции в присутствии ламбекова ограничения

1.11 Линейная логика и экспоненциал

2 Сложность в коммутативном случае

2.1 П? -трудность CommACT^

2.1.1 Счётчиковые машины

2.1.2 Кодирование инструкций счётчиковой машины

2.1.3 Вычисления и выводы

2.2 Х?-полнота CommACT

2.2.1 Циклические выводы для циклических вычислений

2.2.2 Эффективная неотделимость

2.2.3 Доказательство Х0-полноты CommACT

3 Сложность в некоммутативном случае

3.1 Грамматики и автоматы

3.2 Бесконечные вычисления и тотальность контекстно-свободных грамматик

3.3 Кодирование грамматик в ACT^ и ACT

3.4 ^-трудность ACT

4 Реляционная полнота и итерированные деления

4.1 Реляционная полнота и препятствия к ней

4.1.1 R-модели и релятивизованные R-модели

4.1.2 Препятствия, связанные с дистрибутивностью

4.1.3 Трудности с константами 0 и

4.2 Итерированные деления

4.3 Результаты о полноте и неполноте

4.3.1 Ранее известные результаты

4.3.2 R-модели с нестандартной интерпретацией констант, слабая полнота

4.3.3 Контрпример к сильной полноте

4.3.4 Результаты о сильной полноте

5 Фрагменты с ограниченным набором операций

5.1 Грамматики Ламбека и сложность ACT^

5.2 Грамматики с однозначным присвоением типов

5.2.1 Техника анализа выводов

5.2.2 Формула-сторож и её свойства

5.2.3 Конструкция is(^)

5.2.4 Построение грамматики Ламбека

5.2.5 Доказательство корректности построенной грамматики

5.3 П0-трудность исчислений L1^ и L+

5.4 ^-трудность исчислений с правилом декомпозиции

5.5 Сложность фрагментов с итерированными делениями . . 205 5.5.1 Двойное псевдоотрицание

5.5.2 П] -трудность исчислений и

6 Логики с субэкспоненциальными модальностями

6.1 Исчисление !ХАСТ^

6.2 Устранение сечения

6.2.1 Устранение сечения в !ХЛСТ^

6.2.2 Следствия теоремы об устранении сечения

6.3 П]-трудность в присутствии сокращения

6.4 Фрагмент с ограничением на взаимодействие модальностей

6.5 Фрагмент без правила сокращения

Заключение

Литература

Введение диссертации (часть автореферата) на тему «"Алгоритмические вопросы для субструктурных логик с итерацией Клини"»

Введение

Эта диссертация посвящена вопросам алгоритмической сложности субструктурных логических систем с итерацией, или звёздочкой Клини. С точки зрения алгебраической семантики, такие системы задают теории частично упорядоченных структур с итерацией Клини, операцией умножения и согласованными с частичным порядком операциями деления:

b < а\с a - b < с а <с / Ь.

Если частичный порядок вдобавок является решёткой, то такие структуры называются решётками Клини с делениями.

Конкретные естественные примеры решёток Клини с делениями — решётки бинарных отношений и решётки множеств слов (формальных языков) — мотивируют интерес к этому классу алгебраических структур как с чисто теоретической точки зрения, так и с точки зрения приложений в теоретической информатике (при моделировании и исследовании вычислительных процессов) и математической лингвистике. Решётки Клини с делениями из упомянутых двух классов являются *-непрерывными: в них итерация Клини определяется как точная верхняя грань множества степеней данного элемента:

а* = sup {ап | п> 0}.

В произвольных решётках Клини с делениями опеределение итерации более слабое — как наименьшей неподвижной точки некоторого отображения, а именно х ^ 1 v а- х:

а* = min {b | 1 v a - b < b}.

Звёздочка (итерация) Клини была введена в статье Клини [42]; к этой же работе восходит и абстрактное понятие алгебры Клини. В алгебрах Клини имеются операции умножения, дизъюнкции (супремума двух элементов, что задаёт структуру верхней полурешётки) и итерации. Мотивацией служит понимание этих операций как операций над действиями, или переходами в некоторой системе. Умножение соответствует композиции (последовательному совершению действий), дизъюнкция — недетерминированному выбору, а итерация — повторению действия конечное (но заранее не зафиксированное) количество раз, возможно, ноль раз.

Интересно, что Клини [42] избегал пустого, или тождественного, действия (т.е. единицы относительно умножения), и рассматривал вместо звёздочки составную операцию А * В = А* • В. Частным случаем этой операции является положительная итерация, при которой действие необходимо совершить хотя бы единожды: А+ = А* • А. Положительная итерация используется вместо звёздочки Клини в системах без единицы.

Идея алгебраических структур, в которых операции деления согласованы с частичным порядком (а не с равенством), восходит к работе Крулля [51]. Понятие решётки с делениями введено в статье Варда и Дилворта [95]. Если частичный порядок не образует структуру решётки, то говорят о моноидах с делениями, а если вдобавок в структуре может не быть единицы — о полугруппах с делениями.

Инэквациональной теорией (теорией атомарных неравенств, также называемой атомарной теорией) полугрупп с делениями является исчисление Ламбека, введённое у Ламбека [66] для математического описания структуры предложений на естественных языках. Впоследствии Ламбек также предложил варианты исчисления Ламбека, соответствующие теориям моноидов с делениями [67,68]. Расширение исчисления Ламбека с помощью аддитивных конъюнкции и дизъюнкции (в терминологии линейной логики Жирара [29]) называется мультипликативно-аддитивным исчислением Ламбека [14,33]. Это исчисление задаёт

инэквациональную теорию решёток с делениями.

Деления и итерация Клини были «собраны вместе» в работах Прат-та [85] и Козена [48]. Пратт ввёл алгебры Клини с делениями (в которых частичный порядок образует структуру верхней полурешётки), а Козен — решётки Клини с делениями. В терминологии Пратта и Козена они назывались алгебрами и решётками действий соответственно. Инэква-циональная теория решёток Клини с делениями называется «логика действий» и обозначается ACT. Более узкому классу ^-непрерывных решёток Клини с делениями соответствует инфинитарная логика действий ACT,,.

Добавление к алгебрам Клини операций деления было мотивировано лучшими свойствами соответствующих классов алгебр: так, алгебры и решётки Клини с делениями образуют конечно определённые многообразия [85], а обычные алгебры Клини — нет [7,24]. Кроме того, естественные примеры алгебр Клини, прежде всего алгебра формальных языков, на самом деле являются решётками Клини с делениями.

Мультипликативно-аддитивное исчисление Ламбека, т.е. теория решёток с делениями, разрешимо и PSPACE-полно [36,40]. Такова же и инэквациональная теория алгебр Клини (без делений) [47,93]. Вопрос о разрешимости и алгоритмической сложности инэквациональных теорий алгебр и решёток Клини с делениями поставил Козен [48].

Интерес именно к инэквациональным теориям, т.е. теориям в крайне бедном логическом языке, обусловлен тем, что сложность более выразительных теорий практически сразу достигает наивысшего возможного уровня. Действительно, следующей по выразительной силе после инэквациональных являются хорновы теории, описывающие следование одного неравенства из конечного множества неравенств. Однако для минимального языка, где есть умножение и константа «единица», задача разрешения хорновой теории по сути совпадает с проблемой равенства слов в моноидах. Последняя же £0-полна [5, 84], и этот результат переносится на хорновы теории решёток с делениями, алгебр Клини и, наконец, решёток Клини с делениями. Все эти теории перечис-

лимы (это следует из вида их аксиоматизации), так что X0 — это наивысшая сложность. Для хорновой же теории ^-непрерывных решёток Клини с делениями уровень сложности намного выше — она является П]-полной [50], и это опять же наивысший возможный уровень сложности [65].

С логической точки зрения, инэквациональные теории структур с делениями представляют собой субструктурные логики (см. [27]), отличающиеся от классической или интуиционистской логик отсутствием структурных правил — ослабления, сокращения и даже перестановки. Мультипликативно-аддитивное исчисление Ламбека можно рассматривать как базовую ассоциативную субструктурную логику, а звёздочку Клини — как добавляемую к ней одноместную связку (модальность). Другой интересной модальностью является экспоненциал из линейной логики Жирара [29] (исчисление Ламбека можно рассматривать как некоммутативный вариант линейной логики, см. [9]). Для формул под знаком экспоненциала структурные правила разрешены. Более тонкий контроль использования структурных правил дают субэкспоненциальные модальности [25,75].

Вернёмся к вопросам алгоритмической сложности, поставленным в работе Козена [48]. Оказывается, что сочетание делений и звёздочки Клини делает неразрешимыми не только хорновы, но и инэквациональ-ные теории. Бушковский и Палька [21, 23, 77] установили П0-полноту логики ACT^, т.е. инэквациональной теории ^-непрерывных решёток Клини с делениями. Заметим, что здесь нетривиальны обе оценки, и нижняя, и верхняя.

Основные результаты диссертации

Вопрос о разрешимости и сложности логики ACT, т.е. инэквацио-нальной теории всех решёток Клини с делениями, оставался с 1994 г. открытым. Его решение составляет центральный результат настоящей диссертации. А именно, доказано, что логика ACT неразрешима, точ-

нее, Х]-полна.

Этот результат окружён серией смежных результатов об алгоритмических и семантических свойствах субструктурных логик с итерацией Клини. А именно, основные результаты диссертации суть следующие:

1. доказана неразрешимость и установлена алгоритмическая сложность инэквациональных теорий коммутативных решёток Клини с делениями, как в ^-непрерывном, так и с общем случае: П°-полнота

vO

и Х]-полнота соответственно;

2. доказана неразрешимость и, точнее, £°-полнота инэквациональной теории всех решёток Клини с делениями (логики ACT);

3. приведён явный пример секвенции, выводимой в ACT^,, но не ACT;

4. доказана слабая полнота относительно моделей на алгебрах бинарных отношений для фрагмента логики ACT^ без аддитивной дизъюнкции, в котором итерацию разрешено использовать только в знаменателях (итерированные деления);

5. доказано отсутствие слабой полноты относительно моделей на алгебрах бинарных отношений для фрагмента логики ACT^ без аддитивной дизъюнкции, но с итерацией Клини;

6. доказана неразрешимость и П]-трудность фрагмента логики ACT^, без аддитивных операций и с итерированными делениями, т.е. расширения исчисления Ламбека с помощью итерированных делений в инфинитарном случае (в частности, П°-трудность исчисления Ламбека с итерацией, аксиоматизированной омега-правилом);

7. доказана неразрешимость и Х°-полнота исчисления Ламбека с итерацией (в индуктивной аксиоматизации), расширенного так называемым правилом декомпозиции итерации;

8. установлена невыводимость правила декомпозиции итерации в исчислении Ламбека с итерацией;

9. доказана П]-трудность расширения логики ACT^ с помощью субэкспоненциальной модальности, допускающей правило сокращения (в его нелокальной форме) и построен фрагмент данного исчисления с промежуточной сложностью, между П0 и Д];

10. доказана П0-полнота для логики ACT^ с двумя субэкспоненциальными модальностями, одна из которых допускает правило ослабления, а вторая — правило перестановки, во фрагменте с одним делением, умножением и итерацией.

Также диссертация содержит несколько второстепенных результатов. Эти результаты перечислены, наряду с основными, в начале каждой главы.

Структура и содержание диссертации

Диссертация состоит из введения, шести глав, заключения и списка литературы.

Глава 1 является вводной, но, в отличие от настоящего введения, более технической. В ней даны определения основных алгебраических структур, рассматриваемых в работе, и связанных с ними логических систем. В частности, в главе 1 сформулированы исчисления MALC (мультипликативно-аддитивное исчисление Ламбека), ACT, ACT^, и их коммутативные варианты, сформулировано и доказано несколько вспомогательных технических лемм. Приведены несколько новых примеров алгебраических структур с итерацией и делениями, а также построена секвенция, различающая логики ACT и ACT^. Рассмотрены фрагменты исчислений ACT и ACT^ без аддитивных операций — системы L1* и L1*. Для системы L1* установлена невыводимость правила декомпозиции итерации. Наконец, введено ламбеково ограничение непустоты левых частей секвенций и соответствующие варианты введённых ранее исчислений.

Глава 2 посвящена коммутативному случаю. В ней доказана П^-трудность коммутативного варианта логики ACT^ и Х^-трудность коммутативного варианта логики ACT. Эти логики обозначаются CommACT^ и CommACT соответственно. Для доказательства этих результатов построено кодирование неостанова счётчиковой машины секвенцией, выводимой в CommACT^. Отсюда следует П0-трудность данной логики. При этом в случае циклической работы машины дан-

ная секвенция выводима в CommACT. С помощью техники эффективной неотделимости это даёт Х]-трудность CommACT. Необходимость использования эффективной неотделимости связано с тем, что кодирование в случае CommACT работает «в одну сторону»: выводимость секвенции не влечёт цикличности работы машины.

В главе 3 изложен центральный результат диссертации — доказана неразрешимость и Х°-трудность логики ACT. Идея доказательства здесь такая же, как и для CommACT в главе 2 — кодирование циклической работы счётчиковой машины. Однако в некоммутативном случае осуществить такое кодирование напрямую не получается, поэтому используется разработанный Бушковским косвенный подход, через задачу тотальности для контекстно-свободных грамматик.

Результаты главы 4, в отличие от остальных глав, связаны не с алгоритмической сложностью, а с семантикой исчисления ACT^ и его фрагментов, а именно, с интерпретациями на алгебрах бинарных отношений. Само исчисление ACT^ относительно таких интерпретаций неполно. Введён фрагмент исчисления ACT^, в котором отсутствует аддитивная дизъюнкция, а итерация заменена на итерированные деления, т.е. составные операции вида А*\В и В / А*. Для этого фрагмента доказана полнота в слабом смысле (для выводимости без гипотез) и установлено, что полнота в сильном смысле (для выводимости из множеств гипотез, даже конечных) не имеет места. Также установлена сильная полнота для некоторых модификаций данного исчисления. При этом константы 0 и 1 также создают препятствия к полноте, и поэтому используются модифицированные интепретации этих констант на алгебрах бинарных отношений.

В главе 5 изложены доказательства более тонких, чем в главе 3, результатов о неразрешимости и сложности в некоммутативном случае. А именно, доказана П°-полнота для фрагмента ACT^ без аддитивных операций, т.е. исчисления Ламбека с единицей и итерацией. Тем самым решена проблема, поставленная в работе Бушковского [21]. Для соответствующего фрагмента логики ACT этот вопрос остаётся откры-

тым, однако £1 -полнота доказана для его варианта, расширенного правилом декомпозиции. (Это правило невыводимо, однако его допустимость остаётся открытым вопросом.) Наконец, результат о П0-полноте в инфинитарном случае усилен посредством переноса на фрагмент без операции умножения и с заменой итерации на введённые в главе 4 итерированные деления.

Глава 6 посвящена расширениям исчисления АСТ^ семейством субэкспоненциальных модальностей (субэкспоненциалов). Под знаком таких модальностей разрешены все или некоторые из структурных правил — сокращение, ослабление, перестановка, причём сокращение понимается в более общем, нелокальном смысле. Правила для самих субэкспоненциалов и для их взаимодействия задаются субэкспоненциальной сигнатурой £; соответственно, само исчисление обозначается !^АСТ^. Для интересного случая, когда хотя бы один из субэкспоненциалов допускает правило нелокального сокращения, доказана П]-полнота исчисления !^АСТ^. Также определён его фрагмент, в котором под знаками субэкспоненциалов, допускающих правило сокращения, запрещено использовать итерацию Клини. Для этого фрагмента установлены верхняя и нижняя оценки сложности — принадлежность классу Д] и П^-трудность. В случае, когда ни один субэкспоненциал не допускает правило сокращения, сложность остаётся на уровне П0. При этом П]-трудность имеет место уже во фрагменте с умножением, одним делением, итерацией и двумя субэкспоненциалами, один из которых допускает правило ослабления, а второй — правило перестановки.

Заключение содержит краткое изложение основных результатов диссертации и перечисление нескольких открытых проблем для дальнейших исследований.

Публикации

Основные результаты диссертации изложены в 12 статьях [3,53-58, 60-63,65], опубликованных в изданиях, индексируемых в ведущих международных базах научного цитирования. Также результатам диссертации посвящён препринт [64] и тезисы доклада [2]. В работе [3] С. Л. Кузнецову принадлежат результаты о полноте относительно реляционных моделей и о П]-полноте исчисления с итерированными делениями, а Н. С. Рыжковой — результат о полноте относительно языковых моделей. В работе [65] С. Л. Кузнецову принадлежит нижняя оценка, т.е. П]-трудность, для задачи выводимости в расширении АСТ^ субэкспоненциалами, а также теорема об устранении сечения; С. О. Сперанскому принадлежит верхняя П]-оценка, результаты о замыкающих ординалах и основанное на этих результатах доказательство верхней П0-оценки для случая без правила сокращения. В обоих случаях в диссертацию включены только результаты С. Л. Кузнецова. Остальные работы написаны С. Л. Кузнецовым лично.

Благодарности

В профессиональном плане автор благодарит А. Даса, М. И. Кано-вича, Д. Козена, Ф. Н. Пахомова, Д. Д. Рогозина, С. О. Сперанского и А. О. Щедрова за ценные обсуждения, а также коллектив отдела математической логики МИАН во главе с академиком Л. Д. Беклемишевым за тёплую атмосферу и отличные условия для работы. В персональном плане автор благодарен Н. Ю. Кузнецовой и Е. А. Петренёвой за всестороннюю поддержку во время подготовки диссертации.

Глава 1

Решётки Клини с делениями и их логики

Эта глава также является вводной, но, в отличие от введения выше, более технической. Здесь мы дадим определения алгебраических структур и связанных с ними логик, о которых пойдёт речь в дальнейшем. Кроме определений, базовых свойств и стандартных примеров, однако, в этой главе также изложены несколько новых результатов, а именно:

1. построен пример решётки Клини с делениями, не являющейся ^-непрерывной;

2. построен пример моноида Клини с делениями, для которого не выполняется принцип декомпозиции итерации; таким образом, соответствующее правило вывода не является выводимым в исчислении Ламбека с итерацией Клини;

3. предъявлена секвенция, выводимая в логике ^-непрерывных, но не в логике произвольных решёток Клини с делениями.

1.1 Алгебраические определения

Начнём с определений алгебраических структур, логики которых будут рассматриваться далее.

Определение. Решёткой с делениями называется алгебраическая структура ^ = (^; 4, •, 1,0, V, л, /), где

1. •, 1) — моноид;

2. 4, V, л) — решётка;

3. 0 — наименьший элемент решётки;

4. \ и / — операции деления относительно умножения • и частичного порядка 4 в следующем смысле:

Ь 4 а\с а^Ь 4 с а4с/Ь.

Заметим, что операции V, л, \ и / определяются однозначно через операцию умножения и частичный порядок:

avb = Бир4 {а, Ь}; алЬ = т^ {а, Ь};

а\с = тах4{Ь | а^Ь 4 с}; с/Ь = тах4{а | а^Ь 4 с}.

Константы 0 и 1 также определяются единственным образом. Значит, для задания решётки с делениями достаточно определить частичный порядок 4 и операцию умножения, а потом проверить, что остальные операции определены (т.е. что соответствующие супремумы, инфиму-мы и максимумы всегда существуют).

Определение. Решёткой Клини с делениями (РКД) называется алгебраическая структура % = 4, •, 1,0, V, л, /, *), где

1. 4, •, 1,0, V, л, /) — решётка с делениями;

2. для каждого а £ $ его итерация а* (называемая также звёздочкой Клини) определяется так:

а* = тт4 {Ь £ ^ | 1 4Ь и а^Ь 4 Ь}.

Итерация, опять же, определена однозначно через умножение и частичный порядок (как наименьшая неподвижная точка), но существование а* для каждого а в произвольной решётке с делениями не гарантировано.

В присутствии делений многие естественные свойства операций, используемых в РКД, получаются автоматически из определения, и их не требуется дополнительно постулировать:

• монотонность: если а <Ь и с < d, то а • с < b • d, b\c < a\d и с / b < d / a

— доказано в работе Ламбека [66];

• «левая» звёздочка Клини также является «правой»:

а* = min^. [b е d \ 1 <b и b^ a<b}

— доказано в работе Пратта [85]; в отсутствие операций деления существуют «левые» алгебры Клини, не являющиеся «правыми» [46];

• наименьший элемент 0 является нулём для операции умножения: а • 0 = 0 • а = 0 для любого а;

• в любой РКД существует наибольший элемент Т = 0 / 0.

Последние два свойства проверяются непосредственно по определению. Определим два важных семейства РКД.

Определение. Решётка с делениями (в частности, решётка Клини с делениями) называется коммутативной, если такова её операция умножения.

В коммутативном случае левое и правое деление совпадают, и мы введём для них новое обозначение: a\b = b/а = а ^ Ь.

Определение. Решётка Клини с делениями называется *-непрерывной, если для любого а е d выполняется условие

а* = sup^ [ап \ п > °},

где, как обычно, а° = 1 и ап+1 = а^ ап.

Оказывается, что само существование супремумов такого вида достаточно для *-непрерывности:

Предложение 1.1. Если существует супремум d = sup^[a" \ п^ °}, то d = а*, т.е. d = min^ [bed \ 1 <b и a^b <b}.

Это несложное утверждение Ресталл [86] приписывает Пратту, называя его теоремой Пратта о нормальности. Для полноты изложения приведём его доказательство:

Доказательство. Пусть d = Бир4 {ап | п > 0}. Сначала установим, что 1 4 d и а^ й 4 й. Первое очевидно, поскольку 1 = а0. Для доказательства второго заметим, что а^ ап = ап+1 4 d для любого п. Отсюда ап 4 , и поскольку п произвольно, получаем d 4 a\d. Следовательно, а^ й 4 й. Пусть теперь 1 4 Ь и а • Ь 4 Ь для некоторого Ь. По индукции легко доказать, что ап 4 Ь для любого п. Следовательно, й 4Ь, т.е. d — искомый минимум. □

Отметим, что наличие делений здесь существенно. А именно, есть пример алгебры Клини без делений, в которой существует как супремум d = Бир4 {ап | п > 0}, так и наименьшая неподвижная точка а* = тт4 {Ь | 1 4 Ь и а • Ь 4 Ь}, но они не совпадают, т.к. для d нарушается условие а • й 4 й [46]. Для РКД такого невозможно, и становится неочевидным, как построить не *-непрерывную РКД. В частности, всякая полная (как решётка) РКД является *-непрерывной. Пример РКД, не являющейся *-непрерывной, приведён в следующем разделе (теорема 1.2).

1.2 Примеры решёток Клини с делениями

Известны два класса естественных примеров РКД — решётки формальных языков (над некоторым алфавитом) и решётки бинарных отношений (на некотором множестве).

Определение. Пусть £ — конечное непустое множество (алфавит). Через £* обозначается множество всех слов (включая пустое слово г) над алфавитом £, а через &(£*) — множество всех формальных языков, т.е. множеств слов. Структура РКД на &(£*) задаётся следующим образом (А, В — формальные языки):

• А 4 В тогда и только тогда, когда АС В;

• А - В = [uv | и £ A, v £ В} (произведение есть поэлементное приписывание слов);

• 1 = [г}; 0 = 0;

• аув = А и В; АлВ = А П В;

• А\В = [и el* | (W £ A) VU £ В}; В/А = [ие1* | (w £ A) uve В};

• Л* = [щ ...ип | п > 0;щ, ... ,ип £ А}.

Определение. Пусть W — произвольное непустое множество. Тогда &(WxW) есть множество бинарных отношений на множестве W. Структура РКД на &(W х W) задаётся следующим образом (R, S — бинарные отношения):

• R < S тогда и только тогда, когда RC S;

• RS = R°S = [(х, z)eWxW | (lyeW) (х, у) £ R, (у, z) £ S} (произведение есть композиция отношений);

• 1 = 5 = [(х, х) | х £ W} (единица есть диагональное отношение);

0 = 0;

• RvS = R U S; ras = r П S;

• R\S = [(у, z)eWxW | (VxeW) ((х, у) £r^ (х, z) £ S)}; S/R = [(х, у) £WxW | (VzeW) ((у, z)eR^ (х, z) е 5)};

• отношение R* есть рефлексивно-транзитивное замыкание отношения R.

Непосредственно проверяется, что таким образом заданные структуры — это действительно решётки Клини с делениями. Более того, эти РКД — и решётка формальных языков, и решётка бинарных отношений — являются *-непрерывными.

С другой стороны, существуют и не *-непрерывные РКД. Их существование можно доказать неконструктивно, например, с помощью теоремы Мальцева о компактности, либо используя тот факт, что алгебраические логики класса всех РКД и класса всех *-непрерывных РКД имеют разную алгоритмическую сложность (см. раздел 1.6 ниже). Приведём явный пример РКД, не являющейся *-непрерывной.

Теорема 1.2. Зададим на множестве $ = {±}и({0}хМ)и({1,2, ..}хЪ)и{т} линейный порядок следующим образом:

• •-> <-> <-> • •• •

± {0} х N {i}x Z {2} х Z Т

(± — наименьший, Т — наибольший, а на парах (а, Ь) порядок лексикографический); зададим операцию умножения так: ± • х = х • ± = ± для всех х е d, Т •у = у^Т = Т для всех у ф ±, (а1, b-[) • (а2, b2) = (a1 +b1,a2 + Ь2). (Поскольку порядок линейный, то он заведомо образует структуру решётки: а лЬ = min {a, b}, av b = max {a, b}.) Тогда на d можно определить также операции деления, звёздочку Клини, ноль и единицу так, что получится РКД, при этом не *-непрерывная.

Доказательство. Поскольку умножение на $ коммутативно, левое и правое деления будут совпадать: у\х = х / у = у ^ х = max {z \ z • у < х} (см. выше). Легко видеть, что ± ^ х = Т (для всех х), у ^ Т = Т (для всех у), у ^ ± = ± (для у ф ±), Т ^ х = ± (для х ф Т). Остаётся случай у ^ х, где х = (аь Ьг) и у = (аъ Ь2).

Назовём множество {i}x Z, где i > 0, i-й галактикой d; нулевой, «урезанной», галактикой считаем {0} х N. Рассмотрим четыре возможных случая:

1. а\ <а2. Тогда у ^ х = ±. Действительно, для любого z = (а, Ь) имеем z • у = (а + a2,b + Ь2), причём а + а2 > а2 > а1, поэтому z^ у 4 х; также Т • у = Т 4 х. Для z = ± условие выполнено: z • у = ± 4 х.

2. ai > а2. Тогда условие z • у 4 х для z = (a,b) равносильно условию (а,Ь) 4 (о\-q.2, b\—Ь2). Поскольку а\—02 > 0, галактика с номером (щ-а.2) не является «урезанной», и данный элемент в ней существует. Значит, искомое максимальное значение z, т.е. у ^ х, равно (ai — Ü2,b\ — ^2). (Элемент Т не подходит по тем же причинам, что и в первом случае.)

3. а.\ = а,2, bi > &2. Аналогично предыдущему случаю, имеем (ai — a2>b\ — Ь2) = (0,bi — b-¿) е {0} х N, и этот элемент является искомым максимальным значением z.

4. а1 = а.2, Ъ1 < В этом случае, как и в самом первом, у ^ х = ±. Действительно, если х-у = (а + а,2,Ь + Ь2) < (а^Ьх) = х, то а = 0 (иначе а + а2 = а + а1 > а1) и Ь + Ь2 < Ь1, откуда Ь = Ь1 — Ь2 < 0. Элемента (0,Ь1 — Ь2) в $ нет (нулевая галактика — «урезанная»). Элемент Т также не подходит. Для г = ± условие выполнено: г - у = ± < х. Нулевой и единичный элемент суть следующие: 0 = ±, 1 = (0,0). Проверим существование х* для каждого х. Для х = ± и х = (0,0) имеем х* = (0,0) (проверяется по определению). Для остальных значений х имеем х* = Т. Действительно, 1 = (0,0) ^ х*, поэтому х* Ф ±. Для каждого 2 = (а,Ь) имеем х - г 4 г, как в случае х = (а1,Ь1) Ф (0,0), так и в случае х = Т. Остаётся только элемент Т, и он подходит под определение: 1 = (0,0) ^ Т и х - Т = Т < Т.

Наконец, убедимся, что построенная РКД не является *-непрерыв-ной. Действительно, для элемента 2 = (0,1) имеем хп = (0,п). Значит, множество [хп \ п ^ 0} есть нулевая галактика {0} х М, и у неё нет супремума: всякий элемент первой галактики {1} х X является её верхней гранью, и среди них нет наименьшего. □

Построенный пример во многом похож на предложенный в работе Козена [46] пример не *-непрерывной алгебры Клини без делений. Существенное отличие, однако, в следующем: в примере Козена все галактики устроены по типу М, и для элементов 2, скажем, из первой галактики, существует зир^г" \ п^ 0} (наименьший элемент следующей галактики), который, однако, не является а*. В присутствии делений так быть не может, и поэтому галактики (кроме первой) в нашем примере устроены по типу X и не имеют наименьших элементов.

Список литературы диссертационного исследования доктор наук Кузнецов Степан Львович, 2024 год

Литература

[1] Л. Д. Беклемишев, А. А. Оноприенко. О некоторых медленно сходящихся системах преобразований термов. // Матем. сборник. — 2015.

— Т. 206, № 9. — С. 3-20.

[2] С. Л. Кузнецов. Принцип декомпозиции и алгоритмическая неразрешимость для моноидов Клини с делениями. // В сб.: Всероссийская научная конференция «Математические основы информатики и информационно-коммуникационных систем». Сборник трудов.

— Тверь: ТвГУ, 2021. — С. 176-180.

[3] С. Л. Кузнецов, Н. С. Рыжкова. Ограниченный фрагмент исчисления Ламбека с операциями итерации и пересечения. // Алгебра и логика. — 2020. — Т. 59, № 2. — С. 190-214.

[4] К. О. Куценок. Неразрешимость эквациональной теории *-непре-рывных решёток Клини с делениями в языке с двумя делениями и итерацией. — Курсовая работа. — М.: МГУ, кафедра математической логики и теории алгоритмов, 2020.

[5] А. А. Марков. Невозможность некоторых алгорифмов в теории ассоциативных систем. // Докл. АН СССР. — 1947. — Т. 55, № 7. — С. 587590.

[6] М. Р. Пентус. Полнота синтаксического исчисления Ламбека. // Фун-дам. прикл. матем. — 1999. — Т. 5, № 1. — С. 193-219.

[7] В. Н. Редько. Об определяющей совокупности соотношений алгебры регулярных событий. // Укр. матем. журн. — 1964. — Т. 16, № 1. — С. 120-126.

[8] А. Н. Сафиуллин. Выводимость допустимых правил с простыми посылками в исчислении Ламбека. // Вестн. Моск. ун-та. Сер. 1. Матем. механ. - 2007. - Вып. 4. - С. 73-77.

[9] V. M. Abrusci. A comparison between Lambek syntactic calculus and intuitionistic linear propositional logic. // Z. math. Logik Grundl. Math. - 1990.-Bd. 36.-S. 11-15.

[10] P. Aczel. An introduction to inductive definitions. // In: J. Barwise (ed.). Handbook of Mathematical Logic. - Elsevier, 1977. - P. 739-782.

[11] H. Andréka, Sz. Mikulás. Lambek calculus and its relational semantics: completeness and incompleteness. // J. Logic Lang. Inform. - 1994. -Vol. 3, N. 1.-P. 1-37.

[12] Y. Bar-Hillel, C. Gaifman, E. Shamir. On the categorial and phrase-structure grammars. // Bull. Res. Council Israel Sect. F. - 1960. - Vol. 9F. -P. 1-16.

[13] L. D. Beklemishev. Provability algebras and proof-theoretic ordinals, I. // Ann. Pure Appl. Logic. - 2004. - Vol. 128, N. 1-3. - P. 103-123.

[14] J. van Benthem. Language in action: categories, lambdas and dynamic logic. - Amsterdam: North Holland, 1991.

[15] W.J. Blok, D. Pigozzi. Algebraizable logics. - AMS, 1989. - Vol. 77(396) of Memoirs of the American Mathematical Society.

[16] W. Buchholz. Explaining Gentzen's consistency proof within infinitary proof theory. // In: G. Gottlob et al. (eds.). KGC 1997: Computational Logic and Proof Theory. / Lect. Notes Comput. Sci., Vol. 1289. - Springer, 1997. -P. 4-17.

[17] W. Buszkowski. Compatibility of a categorial grammar with an associated category system. // Z. math. Logik Grundl. Math. - 1982. - Bd. 28. -S. 229-238.

[18] W. Buszkowski. Some decision problems in the theory of syntactic categories. // Z. math. Logik Grundl. Math. - 1982. - Bd. 28. - S. 539-548.

[19] W. Buszkowski. Lambek calculus with nonlogical axioms. // In: C. Casa-dio et al. (eds.). Language and Grammar. / CSLI Lect. Notes, Vol. 168. -Stanford: CSLI, 2005. - P. 77-93.

[20] W. Buszkowski. On the complexity of the equational theory of relational action algebras. // In: R. A. Schmidt. RelMiCS 2006: Relations and Kleene Algebra in Computer Science / Lect. Notes Comput. Sci., Vol. 4136. — Springer, 2006. — P. 106-119.

[21] W. Buszkowski. On action logic: equational theories of action algebras. //J. Logic Comput. — 2007. — Vol. 17, N. 1. — P. 199-217.

[22] W. Buszkowski. Lambek calculus and substructural logics. // Linguistic Analysis. — 2010. — Vol. 36, N. 1-4. — P. 15-48.

[23] W. Buszkowski, E. Palka. Infinitary action logic: complexity, models and grammars. // Studia Logica. — 2008. — Vol. 89, N. 1. — P. 1-18.

[24] J. H. Conway. Regular algebra and finite machines. — London: Chapman and Hall, 1971.

[25] V. Danos, J.-B. Joinet, H. Schellinx. The structure of exponentials: Uncovering the dynamics of linear logic proofs. // In: G. Gottlob et al. (eds.). KGC 1993: Computational Logic and Proof Theory, Kurt Gödel Colloquium / Lect. Notes Comput. Sci., Vol. 713. — Springer, 1993. — P. 159-171.

[26] A. Das, D. Pous. Non-wellfounded proof theory for (Kleene+action) (al-gebras+lattices). // In: D. Ghica, A. Jung (eds.). Proc. 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) / Leibniz Internat. Proc. Inform., Vol. 119. — Dagstuhl: Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2018. — P. 19:1-19:18.

[27] N. Galatos, P. Jipsen, T. Kowalski, H. Ono. Residuated Lattices: An Algebraic Glimpse at Substructural Logics. — Elsevier, 2007. — Vol. 151 of Studies in Logic and the Foundations of Mathematics.

[28] G. Gentzen. Untersuchungen über das logische Schließen. I. // Math. Z.

— 1935. — Bd. 39, N. 1. — P. 176-210.

[29] J.-Y. Girard. Linear logic. // Theor. Comput. Sci. — 1987. — Vol. 50, N. 1.

— P. 1-101.

[30] K. Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. // Monatshefte für Mathematik und Physik.

— 1931. — Bd. 38. — P. 173-198.

[31] S. A. Greibach. A new normal-form theorem for context-free phrase structure grammars. //J. ACM. - 1965. - Vol. 12, N. 1. - P. 42-52.

[32] P. Jipsen. From residuated semirings to Kleene algebras. // Studia Logica.

- 2004. - Vol. 76, N. 2. - P. 291-303.

[33] M. Kanazawa. The Lambek calculus enriched with additional connectives. //J. Logic Lang. Inform. - 1992. - Vol. 1, N. 2. - P. 141-171.

[34] M. Kanazawa. Lambek calculus: Recognizing power and complexity. // In: J. Gerbrandy et al. (eds.). JFAK. Essays Dedicated to Johan van Ben-them on the Occasion of his 50th Birthday. - Vossiuspers, Amsterdam University Press, 1999.

[35] M. Kanovich, S. Kuznetsov, V. Nigam, A. Scedrov. Subexponentials in non-commutative linear logic. // Math. Struct. Comput. Sci. - 2019. -Vol. 29, N. 8. - P. 1217-1249.

[36] M. Kanovich, S. Kuznetsov, A. Scedrov. The complexity of multiplicative-additive Lambek calculus: 25 years later. // In: R. Iemhoff et al. (eds.). WoL-LIC 2019: Logic, Language, Information, and Computation / Lect. Notes Comput. Sci., Vol. 11541. - Springer, 2019. - P. 356-372.

[37] M. Kanovich, S. Kuznetsov, A. Scedrov. Reconciling Lambek's restriction, cut-elimination, and substitution in the presence of exponential modalities. //J. Logic Comput. - 2020. - Vol. 30, N. 1. - P. 239-256.

[38] M. Kanovich, S. Kuznetsov, A. Scedrov. Language models for some extensions of the Lambek calculus. // Inform. Comput. - 2022. - Vol. 287.

- Art. 104760.

[39] M. I. Kanovich. Horn programming in linear logic is NP-complete. // In: Proc. 7th Annual IEEE Symposium on Logic in Computer Science. - IEEE, 1992. - P. 200-210.

[40] M. I. Kanovich. Horn fragments of non-commutative logics with additives are PSPACE-complete. // In: 1994 Annual Conference of the European Association for Computer Science Logic. - Kazimierz, 1994.

[41] L. Kirby, J. Paris. Accessible independence results for Peano arithmetic. // Bull. London Math. Soc. - 1982. - Vol. 14. - P. 285-293.

[42] S. C. Kleene. Representation of events in nerve nets and finite automata. In: C. E. Shannon, J. McCarthy (eds.). Automata Studies. — Princeton University Press, 1956. — P. 3-41. / Рус. пер.: С. К. Клини. Представление событий в нервных сетях и конечных автоматах // В сб.: Автоматы. Сб. статей, ред. К. Э. Шеннон, Дж. Маккарти. — М.: ИЛ, 1956. — С. 1567.

[43] D. König. Über eine Schlusselweise aus dem Endlichen ins Unendliche. // Acta Scientiarum Mathematicarum (Szeged). — 1927. — Vol. 3, N. 2-3. — P. 121-130.

[44] M. Kozak. Distributive full Lambek calculus has the finite model property. // Studia Logica. — 2009. — Vol. 91, N. 2. — P. 201-216.

[45] D. Kozen. On induction vs. ^-continuity. // In: D. Kozen (ed.). Logic of Programs 1981 / Lect. Notes Comput. Sci., Vol. 131. — Springer, 1982. — P. 167-176.

[46] D. Kozen. On Kleene algebras and closed semirings. // In: B. Rovan (ed.). MFCS 1990: Mathematical Foundations of Computer Science / Lect. Notes Comput. Sci., Vol. 452. — Springer, 1990. — P. 26-47.

[47] D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. // Inform. Comput. — 1994. — Vol. 110, N. 2. — P. 366-390.

[48] D. Kozen. On action algebras. // In: J. van Eijck, A. Visser (eds.). Logic and Information Flow. — MIT Press, 1994. — P. 78-88.

[49] D. Kozen. Automata and Complexity. — New York: Springer-Verlag, 1997.

[50] D. Kozen. On the complexity of reasoning in Kleene algebra. // Inform. Comput. — 2002. — Vol. 179. — P. 152-162.

[51] W. Krull. Axiomatische Begründung der algemeinen Idealtheorie. // Sitzungsberichte der physikalischmedizinischen Societät zu Erlangen. — 1924. — Bd. 56. — S. 47-63.

[52] S. Kuznetsov. The Lambek calculus with iteration: two variants. // In: J. Kennedy, R. de Queiroz (eds.). WoLLIC 2017: Logic, Language, Information, and Computation / Lect. Notes Comput. Sci., Vol. 10388. — Springer, 2017. — P. 182-198.

[53] S. Kuznetsov. ^-continuity vs. induction: divide and conquer. // In: G. Bezhanishvili et al. (eds.). Proceedings of AiML 2018. / Advances in Modal Logic, Vol. 12. - London: College Publications, 2018. - P. 493510.

[54] S. Kuznetsov. The logic of action lattices is undecidable. // In: Proc. 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019). - IEEE, 2019.

[55] S. Kuznetsov. Complexity of commutative infinitary action logic. In: M. A. Martins, I. Sedlar (eds.). DaLi 2020: Dynamic Logic. New Trends and Applications. / Lect. Notes Comput. Sci., Vol. 12569. — Springer, 2020. -P. 155-169.

[56] S. Kuznetsov. The 'long rule' in the Lambek calculus with iteration: un-decidability without meets and joins. In: N. Olivetti et al. (eds.). Proceedings of AiML 2020. / Advances in Modal Logic, Vol. 13. — London: College Publications, 2020. — P. 425-449.

[57] S. Kuznetsov. Action logic is undecidable. // ACM Trans. Comput. Logic. — 2021. — Vol. 22, N. 2. — Art. 10.

[58] S. Kuznetsov. Complexity of the infinitary Lambek calculus with Kleene star. // Rev. Symb. Logic. — 2021. — Vol. 14, N. 4. — P. 946-972.

[59] S. L. Kuznetsov. Trivalent logics arising from L-models for the Lambek calculus with constants. //J. Appl. Non-Class. Logics. — 2013. — Vol. 24, N. 1-2. — P. 132-137.

[60] S. L. Kuznetsov. Complexity of a fragment of infinitary action logic with exponential via non-well-founded proofs. // In: A. Das, S. Negri (eds.). Tableaux 2021: Automated Reasoning with Analytic Tableaux and Related Methods / Lect. Notes Comput. Sci., Vol. 12842. — Springer, 2021. — P. 317-334.

[61] S. L. Kuznetsov. Kleene star, subexponentials without contraction, and infinite computations. // Сиб. электрон. матем. изв. — 2021. — Т. 18, № 2. — С. 905-922.

[62] S. L. Kuznetsov. Relational models for the Lambek calculus with intersection and unit. In: U. Fahrenberg et al. (eds.). RAMiCS 2021: Relational

and Algebraic Methods in Computer Science / Lect. Notes Comput. Sci., Vol. 13027. - Springer, 2021. - P. 258-274.

[63] S. L. Kuznetsov. Commutative action logic. //J. Logic Comput. — 2022. — Vol. 33, N. 6. — P. 1437-1462.

[64] S. L. Kuznetsov. Relational models for the Lambek calculus with intersection and constants. — 2022. — arXiv preprint 2210.00645.

[65] S. L. Kuznetsov, S. O. Speranski. Infinitary action logic with exponentiation. // Ann. Pure Appl. Logic. — 2022. — Vol. 173, N. 2. — Art. 103057.

[66] J. Lambek. The mathematics of sentence structure. // Amer. Math. Monthly. — 1958. — Vol. 65. — P. 154-170.

[67] J. Lambek. On the calculus of syntactic types. // In: R. Jakobson (ed.). Structure of Language and Its Mathematical Aspects. / Proc. Symposia in Applied Mathematics, Vol. 12. — AMS, 1961. — P. 166-178.

[68] J. Lambek. Deductive systems and categories II: standard constructions and closed categories. // In: P. Hilton (ed.) Category Theory, Homology Theory, and Their Applications I / Lect. Notes Math., Vol. 86. — Springer, 1969. — P. 76-122.

[69] P. Lincoln, J. Mitchell, A. Scedrov, N. Shankar. Decision problems for propositional linear logic. // Ann. Pure Appl. Logic. — 1992. — Vol. 56, N. 1-3. — P. 239-311.

[70] Sz. Mikulas. The equational theories of representable residuated semigroups. // Synthese. — 2015. — Vol. 192, N. 7. — P. 2151-2158.

[71] Sz. Mikulas. Lower semilattice-ordered residuated semigroups and substructural logics. // Studia Logica. — 2015. — Vol. 103, N. 3. — P. 453-478.

[72] M. L. Minsky. Recursive unsolvability of Post's problem of "Tag" and other topics in theory ofTuring machines. // Ann. Math. — 1961. — Vol. 74, N. 3. — P. 437-455.

[73] R. Moot, C. Retoré. The Logic of Categorial Grammars. A Deductive Account of Natural Language Syntax and Semantics. — Springer, 2012. — Lect. Notes Comput. Sci., Vol. 6850.

[74] J. Myhill. Creative sets. // Z. math. Logik Grundl. Math. — 1955. — Bd. 1. — S. 97-108.

[75] V. Nigam, D. Miller. Algorithmic specifications in linear logic with subex-ponentials. In: PPDP '09: Proc. 11th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. — ACM, 2009. — P. 129140.

[76] H. Ono, Y. Komori. Logics without the contraction rule. //J. Symb. Logic.

— 1985. — Vol. 50, N. 1. — P. 169-201.

[77] E. Palka. An infinitary sequent system for the equational theory of *-continuous action lattices. // Fundam. Inform. — 2007. — Vol. 78, N. 2. — P. 295-309.

[78] M. Pentus. Lambek grammars are context-free. // In: Proc. 8th Annual IEEE Symposium on Logic in Computer Science (LICS 1993). — IEEE, 1993. — P. 429-433.

[79] M. Pentus. The conjoinability relation in Lambek calculus and linear logic. //J. Logic Lang. Inform. — 1994. — Vol. 3, N. 2. — P. 121-140.

[80] M. Pentus. Models for the Lambek calculus. // Ann. Pure Appl. Logic. — 1995. — Vol. 75, N. 1-2. — P. 179-213.

[81] M. Pentus. Product-free Lambek calculus and context-free grammars. // J. Symb. Logic. — 1997. — Vol. 62, N. 2. — P. 648-660.

[82] M. Pentus. Free monoid completeness of the Lambek calculus allowing empty premises. In: J. M. Larrazabal et al. (eds.). Proc. Logic Colloquium '96 / Lect. Notes Logic, Vol. 12. — Cambridge University Press, 1998. — P. 171-209.

[83] M. Pentus. Lambek calculus is NP-complete. // Theor. Comput. Sci. — 2006. — Vol. 357, N. 1-3. — P. 186-201.

[84] E. L. Post. Recursive unsolvability of a problem of Thue. //J. Symb. Logic.

— 1947. — Vol. 12, N. 1. — P. 1-11.

[85] V. Pratt. Action logic and pure induction. // In: J. van Eijck (ed.). JELIA 1990: Logics in AI / Lect. Notes Artif. Intell., Vol. 478. — Springer, 1991. — P. 97-120.

[86] G. Restall. An Introduction to Substructural Logics. — Routledge, 2000.

[87] H. Rogers. Theory of Recursive Functions and Effective Computability.

— MIT Press, 1987.

[88] Yu. Savateev. Product-free Lambek calculus is NP-complete. // Ann. Pure Appl. Logic. - 2012. - Vol. 163, N. 7. - P. 775-788.

[89] H. Schellinx. Some syntactical observations on linear logic. // J. Logic Comput. - 1991. - Vol. 1, N. 4. - P. 537-559.

[90] R. Schroeppel. A two counter machine cannot calculate 2N. - 1972. -Massachusets Institute of Technology A.I. Laboratory, Artificial Intelligence Memo #257.

[91] I. Sedlar. Iterative division in the distributive full non-associative Lambek calculus. // In: L. S. Barbosa, A. Baltag (eds.). DaLi 2019: Dynamic Logic. New Trends and Applications / Lect. Notes Comput. Sci., Vol. 12005. -Springer, 2020. - P. 141-154.

[92] S. O. Speranski. A note on hereditarily n0- and Y®-complete sets of sentences. //J. Logic Comput. - 2016. - Vol. 26, N. 5. - P. 1729-1741.

[93] L.J. Stockmeyer, A. R. Meyer. Word problems requiring exponential time: Preliminary report. In:Conference Record of 5th Annual ACM Symposium on Theory of Computing. - ACM, 1973. - P. 1-9.

[94] L. Straßburger. On the decision problem for MELL. // Theor. Comput. Sci. - 2019. - Vol. 768. - P. 91-98.

[95] M. Ward, R. P. Dilworth. Residuated lattices. // Trans. AMS. - 1939. -Vol. 45, N. 3. - P. 335-354.