Моделирование вычислительных процессов средствами пропозициональных логик тема диссертации и автореферата по ВАК РФ 05.13.17, доктор физико-математических наук Чагров, Александр Васильевич

• Чагров, Александр Васильевич
• доктор физико-математических наук
• 1998

Оглавление диссертации доктор физико-математических наук Чагров, Александр Васильевич

ОГЛАВЛЕНИЕ

ВВЕДЕНИЕ

Общая характеристика работы

Краткий исторический очерк

1 ИСХОДНЫЕ ОПРЕДЕЛЕНИЯ И ФАКТЫ

1.1 Модальные и суперинтуиционистские логики.

1.2 Полнота по Посту.

1.3 Табличные логики.

1.4 Машины Минского

2 О РАЗРЕШИМОСТИ ЛОГИК

2.1 Об обобщениях критерия Харропа разрешимости логик.

2.2 Моделирование машин Минского модальными средствами с использованием константных формул.

2.2.1 Случай временных логик.

2.2.2 Случай расширений К4.

2.2.3 Случай расширений вГ

2.3 Метод контекстных подстановок.

2.4 Моделирование машин Минского средствами супер интуиционистских логик

2.5 «Экономные» неразрешимые суперинтуиционистское исчисление и неразрешимая формула.

2.6 «Экономные» неразрешимые исчисление и неразрешимая формула в NExtS4.

3 АЛГОРИТМИЧЕСКИЕ ПРОБЛЕМЫ СЛЕДОВАНИЯ

3.1 Разрешимая модальная логика с неразрешимой проблемой допустимости правил вывода.

3.2 Проблема семантического следования модальных формул на конечных шкалах.

3.3 О первопорядковой определимости модальных формул на конечных модальных шкалах

3.4 О финитарном семантическом следования на конечных интуиционистских шкалах.

4 ОБ АЛГОРИТМИЧЕСКОМ ОПИСАНИИ СВОЙСТВ ЛОГИК: РАЗРЕШИМЫЕ СВОЙСТВА

4.1 Табличность в NExtGL.

4.2 Разрешимые свойства в ExtGL

4.3 К проблеме табличности в NExtK4.

4.4 Еще несколько примеров разрешимых свойств

5 ОБ АЛГОРИТМИЧЕСКОМ ОПИСАНИИ СВОЙСТВ ЛОГИК: НЕРАЗРЕШИМЫЕ СВОЙСТВА

5.1 Неразрешимые свойства суперинтуиционистских логик.

5.1.1 Схема доказательств неразрешимости свойств исчислений. Разрешимость и финитная аппроксимируемость

5.1.2 Полнота по Крипке.

5.1.3 Полнота по Холдену, полнота по Максимовой и дизъюнктивное свойство.

5.1.4 Допустимость дизъюнктивного свойства.

5.1.5 О нормальных модальных напарниках суперинтуиционистских логик.

5.2 Неразрешимые свойства в расширениях логики СЬ

5.2.1 Неразрешимые свойства в МЕх1СЬ.

5.2.2 Неразрешимые свойства в Ех1СЬ.

5.2.3 Неразрешимые свойства в Ех18.

5.3 Неразрешимые свойства нормальных модальных логик.

5.3.1 Логики, не содержащие ОТ.

5.3.2 Непротиворечивые логики, содержащие ОТ.

5.3.3 Проблема аксиоматизируемости константными формулами

5.3.4 Нормальные модальные логики с конечным числом несводимых модальностей.

5.4 Неразрешимые свойства логик в ЕхЖ4 и в ИЕхЖ^ при п > 1.

Введение диссертации (часть автореферата) на тему «Моделирование вычислительных процессов средствами пропозициональных логик»

Актуальность темы исследования В 70——80— годы было досрочно подтверждено предвидение создателя языка лисп Дж.Маккарти, высказанное им в 1967 году: «Разумно ожидать, что связи между вычислительной техникой и математической логикой окажутся столь же плодотворными в следующем столетии, какими были связи между математическим анализом и физикой в столетии предыдущем». Оказалось, что в плодотворности этих связей можно убедиться уже в наши дни1. Методы математической логики дали возможность осуществить многие новые подходы к созданию вычислительных средств, баз данных, экспертных систем, языков программирования, синтезу и верификации программ и пр. При этом действенной оказалась и обратная связь: возникли новые разделы математической логики, оказались по

1В предисловии редакторов сборника переводов [30] сказано, например: «Чтобы представить себе, хотя бы в общих чертах, те направления, в которых развивается современная вычислительная наука, полезно взглянуть на названия сборников широко известной серии Lecture Notes in Computer Science, выпускаемой западногерманским издательством Springer-Verlag и содержащей материалы многих международных конференций по информатике. . чуть ли не на каждой пятой обложке можно увидеть термины «логический вывод», «логическое программирование», «компьютерная логика», «логики программ» и т.д. ». Ещё раньше плодотворность применения средств математической логики в программировании была блестяще продемонстрирована в [120]. новому расставленными акценты в ряде её традиционных разделов. Практически в каждом справочном пособии и многих монографиях по информатике или искусственному интеллекту математическая логика выступает и в качестве языка обсуждения предмета, и в качестве необходимой компоненты представления результатов, и в качестве инструмента для их получения2. Сейчас происходит переосмысление всего здания логики с учетом этой новой реальности: те её части, которые до того считались неклассическими и представляли собой нечто экзотическое, становятся едва ли не главными объектами исследований и приложений3. При этом особый интерес представляют логические системы, имеющие реляционное истолкование (в частности, и в форме семантики): программные и динамические логики, модальные и многомодальные (особенно временные), интуиционистская4 и близкие к ней логики.

Выбор предмета исследования — модальные и суперинтуиционистские логики и представление с их помощью вычислений — обусловлен тем, что они находятся в центре практически всех вновь создаваемых для приложений в информатике логических систем, либо непосредственно ими являясь, либо являясь отправной точкой для подходящих модификаций5. При этом пропозициональный уровень оказывается

2См., например, [79], [126], [128], [127], [153].

3Авторы [33] говорят по этому поводу: «С точки зрения названных задач перспективной кажется и разработка математических исчислений так называемой модальной логики, оперирующей, наряду с традиционными для классической логики оценками «истинно» и «ложно», также и такими оценками, как «возможно», «необходимо», «правдоподобно», «произойдёт в будущем» и т.д.».

4 Интуиционистская логика оказалась пригодной для описания свойств вычислений даже в тех случаях, когда логики на классической основе не давали непосредственной возможности для их использования, например: синтеза программ [2], [29], для описания альтернирующих вычислений [58], моделирования немонотонных рассуждений [118].

5Рост значения модальной логики для информатики можно охарактеризовать таким фактом.

Авторы монографии [149] отвели модальной логике в первом томе своего сочинения около 5% достаточным для проявления практически всех «неклассических» эффектов, полезных для приложений, и для подходящего развития логических систем на базе более богатых по выразительным возможностям логических языков — первого и более высоких порядков.

В соответствии с подразумеваемыми приложениями представляется весьма актуальным изучение эффективных представлений вычислений в пропозициональных логиках, причем эти представления имеют два диаметрально противоположных аспекта — «положительный», связанный с построением конкретных алгоритмов, решающих массовые задачи, связанные с логиками, такие как выводимость формулы в исчислении, допустимость и/или производность правила вывода в логике, выяснение выполнимости свойства в логике и т.д., и «отрицательный», характеризующийся отсутствием соответствующих алгоритмов. Кавычки здесь поставлены потому, что на самом деле оба аспекта положительны: «положительный» — ввиду предоставления конкретных алгоритмов, которые в определённых случаях можно применять для решения прикладных задач, а «отрицательный» — ввиду того, что при доказательстве неразрешимости как составная часть используется непосредственное представление алгоритмов в исчислениях, то есть разрабатываются выразительные возможности языка пропозициональных логик, чем расширяется область их приложений6. объёма текста, а второй том снабдили подзаголовком «От модальной логики к логике баз данных».

6Кроме того, стоит иметь в виду и другой очевидный аспект «отрицательных» результатов, см. [33]: «Понимание, что в принципе невозможно сделать что-то, имеет для программирования не меньшее значение, чем для техники невозможность нарушить второе начало термодинамики или для физики невозможность превысить скорость света».

Цель и задачи исследования Из весьма обширного списка задач, вытекающих из предыдущего пункта, для рассмотрения в диссертации выбраны следующие ключевые:

• представление вычислений средствами логического следования: в виде выводов в исчислениях; в виде семантического следования (то есть содержательного следования, когда формулы описывают строение реляционных структур, представляющих собой формализацию совокупности стадий вычисления в их программной взаимосвязи), в частности, финитарного следования, когда все рассматриваемые реляционные структуры предполагаются конечными, что является отражением свойств реальных вычислительных сред; в виде допустимых в данной логике правил вывода; их наличие может существенно ускорить алгоритмы, распознающие принадлежность формул этой логике;

• алгоритмическое описание свойств реляционных структур средствами пропозициональных языков: построение алгоритмов, отвечающих по произвольно заданной формуле на вопросы о выполнении для семантически ей адекватных реляционных структур желаемых свойств; или доказательство невозможности таких алгоритмов; выяснение возможности переопределения реляционных свойств модальных, интуиционистских пропозициональных формул в терминах классических формул первого порядка, реализация которой предоставляет для приложений в рассматриваемой совокупности задач средства хорошо разработанной теории моделей классической логики первого порядка;

• алгоритмическое описание свойств логик:

- выяснение по аксиоматизации логики ее семантических свойств, таких как: финитная аппроксимируемость, то есть возможность ограничения класса адекватных для логики структур конечными; реляционная полнота, то есть точность соответствия логики и класса моделирующих её реляционных структур; табличность логики, то есть её адекватность по отношению к одной конечной реляционной структуре; выяснение по аксиоматизации логики ее внутренних свойств, таких как7: непротиворечивость, то есть нетривиальность логики для дальнейших приложений; разрешимость самой логики, разрешимость проблем допустимости, производности в ней правил вывода; дизъюнктивное свойство, являющееся методологической основой построения большинства алгоритмов, синтезирующих программы по доказательству их существования, и близкие к нему (полнота по Хол-дену, полнота по Максимовой); интерполяционное свойство, дающее во многих интересных случаях возможность явных определений по существованию неявных, то есть

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

Целью работы являются:

• изучение феномена алгоритмической разрешимости/неразрешимости пропозициональных логик, в частности — выяснение границ применимости известных критериев разрешимости, например — критерия Харропа;

• создание простых в некотором смысле (удобных для приложений, экономных по числу используемых в аксиоматике переменных) неразрешимых исчислений;

• решение известных проблем, связанных с правилами вывода (в частности, всякая ли разрешимая логика имеет разрешимую проблему допустимости правил вывода) и с вариантами семантического следования (например, следования на конечных реляционных структурах);

• выяснение возможностей алгоритмического описания свойств логик (точнее, исчислений, ввиду известной теоремы А.В.Кузнецова об алгоритмической неразрешимости нетривиальных свойств рекурсивно задаваемых логик), то есть обоснование разрешимости или неразрешимости интересующего нас по каким-либо причинам свойства логик.

Методы исследования Основные методы исследования — семантические методы теории модальных и суперинтуиционистских логик, методы теории моделей классической логики первого порядка, методы теории алгоритмов.

Научная новизна В диссертации получены следующие основные новые результаты:

• Построены примеры неразрешимых логик, задаваемых разрешимыми классами конечных шкал (алгебр, моделей); обосновано существование неразрешимых рекурсивно аксиоматизируемых финитно аппроксимируемых логик; показано, что не все логики можно аппроксимировать рекурсивными алгебрами.

• В следующей таблице приведены обнаруженные в диссертации факты о суо ществовании в рассматриваемых классах логик неразрешимых исчислении с малым числом переменных: первая строка, например, означает, что существует неразрешимое суперинтуиционистское исчисление, аксиомы которого используют 4 переменные, а в формулах, для которых неразрешима проблема выводимости в нем, используются 2 переменные; знак = около числа означает, что оценка числа переменных не понижаема, а < — вопрос о понижении числа переменных открыт.

83десь и далее используются стандартизированные в [116] обозначения: (1Ч)Ех^ — класс (нормальных) расширений логики так, ЕхИг^ обозначает класс суперинтуиционистских логик, NExtS4 — класс нормальных расширений модальной логики 84.

Число переменных в

Класс неразрешимых отделяемых логик исчислениях формулах

ЕхШ1 < 4 = 2

КЕх184 < з = 1

Ех184 < з = 1 1 = 1

Ех1СЬ = 1 = 1

ExtS = 1 = 1 хЖ4 = 1 = 0

ЕхЖ4 = 1 = 0

• Предложено понятие разрешимой/неразрешимой в данном классе логик формулы, которое является двойственным понятию разрешимой/неразрешимой логики, и найдены простые (по числу переменных, используемым связкам, длине) для рассматриваемых классов логик примеры неразрешимых формул.

• Построена разрешимая модальная логика с неразрешимой проблемой допустимости правил вывода, что обосновывает нетривиальность решения задачи доказательства разрешимости проблемы допустимости правил вывода, полученного В.В.Рыбаковым для многих конкретных модальных и суперинтуиционистских логик.

• Доказана неразрешимость семантического следования на конечных шкалах Крипке в различных вариантах (локальном, глобальном) и в разных классах шкал (вЬ-шкалы, 1^-шкалы и др.). Получена также неразрешимость проблемы первопорядковой определимости модальных формул на классе конечных шкал9.

• Обоснована разрешимость некоторых свойств логик в некоторых классах — в частности, свойство табличности и непротиворечивости расширений СЬ, а для значительного количества стандартных свойств логик, таких как разрешимость, финитная аппроксимируемость, полнота, интерполяционное и дизъюнктивное свойства и т.д., доказана алгоритмическая неразрешимость практически во всех рассматриваемых классах логик, кроме того, установлена граница (не)разрешимости таких свойств, как непротиворечивость, полнота по Холдену.

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

Апробация По результатам диссертации делались доклады на Всесоюзных конференциях по математической логике (Тбилиси, 1982; Новосибирск, 1984; Москва, 1986; Ленинград, 1988; Алма-Ата, 1990, приглашённый доклад), на Всесоюзных алгебраических конференциях (Кишинёв, 1985, Львов, 1987), на IX Всесоюзном совещании по логике, методологии и философии науки (Харьков, 1986), на Ме

9Результат получен совместно с Л.А.Чагровой; см. сноску на странице 128. ждународных конгрессах по логике, методологии и философии науки (Москва, 1987; Italy, 1995), на X Всесоюзной конференции по логике, методологии и философии науки (Минск, 1990), на II Всесоюзной конференции по прикладной логике (Новосибирск, 1988), на Международной конференции по алгебре (Новосибирск, 1989), на Логическом Коллоквиуме Европейской Ассоциации Символической логики (ASL Logic Colloquium 'Berlin 89'; The 1992 Europian Summer Meeting of the ASL, 1992; Logic Colloquium'94, 1994), на логических конференциях в Болгарии (Second Logical Biennial, Summer school&conference, Bulgaria, 1988), (Third Logical Biennial, Summer school&conference, Bulgaria, 1990), на Азиатской логической конференции (The Fourth Asian Logic Conference, Japan, 1990), на конференции по логике в информатике (Annual Conference of the European Association for Computer Science Logic, Poland, 1994), на научных семинарах Московского (1989, 1991, 1994), Новосибирского (1988, 1991) и Тверского госуниверситетов (1985-1996), Амстердамского (1993) и Берлинского (1995) математических институтов.

Публикации Основные результаты диссертации содержатся в [6], [7], [8], [35], [40], [41], [45], [46], [47], [50], [51], [52], [53], [54], [55], [56], [57], [58], [59], [60], [61], [62], [63], [64], [65], [66], [90], [91], [92], [93], [94], [95], [96], [98], [99], [100], [101], [102], [103], [104], [105], [106], [107], [108], [109], [110], [111], [112], [113], [114], [115], [97], [116], [154]; в том числе, большая их часть представлена в монографическом виде в [116].

Структура и объём работы Диссертация состоит из введения (на 14 страницах) и пяти глав, структурированных по разделам и, в некоторых случаях, по подразделам. Общий объем текста — 292страницы, в тексте содержится 45 рисунков. Список литературы (на 18 страницах) содержит 154 наименования.