Интерполяционные свойства логик доказуемости и нормализация термов рефлексивной комбинаторной логики тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

Московский государственный университет имени М.В. Ломоносова

На правах рукописи

005018660

Шамканов Данияр Салкарбекович

Интерполяционные свойства логик доказуемости и нормализация термов рефлексивной комбинаторной логики

01.01.06 - математическая логика, алгебра и теория чисел

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

1 ^ мИР 2312

Москва - 2012

005018660

Работа выполнена на кафедре математической логики и теории алгоритмов Механико-математического факультета Московского государственного университета имени М.В. Ломоносова.

Научные руководители: член-корреспондент РАН,

доктор физико-математических наук Беклемишев Лев Дмитриевич кандидат физико-математических наук, доцент Крупский Владимир Николаевич Официальны оппоненты: доктор физико-математических наук,

с.н.с. Оревков Владимир Павлович ПОМИ РАН, в.н.с.

кандидат физико-математических наук, Шапировский Илья Борисович ИППИ РАН, с.н.с

Ведущая организация: Институт математики имени С.Л. Соболева

СОРАН

Защита диссертации состоится 27 апреля 2012 г. в 16:45 на заседании диссертационного совета Д 501.001.84 при Московском государственном университете имени М.В. Ломоносова по адресу: Р.Ф., 119991, Москва, ГСП-1, Ленинские горы, д. 1, МГУ, Механико-математический факультет, аудитория 14-08.

С диссертацией можно ознакомиться в библиотеке Механико-математического факультета МГУ (Главное здание, сектор А, 14 этаж).

Автореферат разослан 27 марта 2012 г.

Ученый секретарь диссертационного совета Д 501.001.84 при МГУ, д.ф-м.н., профессор

Иванов А.О.

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

Диссертация посвящена исследованию формальных систем, описывающих понятие доказуемости. В первой части диссертации проводится изучение интерполяционных свойств логик доказуемости GL и GLP, вторая часть посвящена исследованию рефлексивной комбинаторной логики RCL.

Актуальность работы. Формулы логики доказуемости Геделя-Леба GL строятся из пропозициональных переменных {pi}, булевых связок и унарного оператора модальности □. Арифметический перевод таких формул заключается в замене пропозициональных переменных предложениями арифметики, а модальности □ — геделевской формулой доказуемости. Как доказал Р. Соловей1, логика Геделя-Леба GL является корректной и полной относительно данной арифметической семантики: GL h у тогда и только тогда, когда любой арифметический перевод формулы tp доказуем в арифметике Пеано РА.

Г. Джапаридзе2 сформулировал полимодальный вариант логики доказуемости GLP, рассмотрев язык пропозициональной логики, снабженный счетным числом модальностей [0], [1],.... Для каждого п арифметическим переводом модальности [п] является формула, выражающая доказуемость в теории РА, обогащенной всеми истинными Пп-предложениями. Аналогично случаю GL, система GLP корректна и полна относительно данной арифметической семантик2,3. Поскольку арифметические значения модальностей □ и [0] сов-

1. Solovay R. Provability interpretation of modal logic // Israel Journal of Mathematics. — 1976. — Vol. 25. — P. 287-304.

2. Джапаридзе Г. К. Модально-логические средства исследования доказуемости : Диссертация на соискание ученой степени кандидата филосовских наук : 09.00.07 / Георгий Кохтаевич Джапаридзе ; Тбилисский государственный университет. — Тбилиси, 1986. — 177 с.

3. Ignatiev К. On strong provability predicates and the associated modal logics // The Journal of Symbolic Logic. - 1993. - Vol. 58. - P. 249-290.

падают, при их отождествлении система GLP становится консервативным расширением GL.

Система L обладает интерполяционным свойством Крейга, если для любых формул ip и ф таких, что L Ь ip -4 гр, найдется формула в, составленная из общих для <р и ip переменных, для которой

Усилением этого условия является интерполяционное свойство Линдона, добавляющее требование, чтобы переменные, входящие позитивно в в, входили бы позитивно как в <р, так и в ■ф, и аналогично для переменных, которые входят негативно.

Интерполяционное свойство Крейга для логики GL было установлено К. Сморинским4 и немного позже Дж. Булосом5. Вопрос о справедливости интерполяционного свойства Линдона для логики GL. насколько нам известно, до настоящего исследования был открыт5.

Интерполяционное свойство Крейга в случае системы GLP установлено К. Игнатьевым3, однако доказательство К. Игнатьева не формализуемо в арифметике Пеано. Л. Беклемишев предъявил другое (финитное) доказательство того же факта7.

Одним из существенных усилений интерполяционного свойства Крейга является свойство равномерной интерполяции. Впервые оно было сформулировано А. Питтсом, установившим свойство равномерной интерполяции для

4. Smoryiski С. Beth's theorem and self-referential sentences // Logic Colloquium'77 / Ed. by A. Macintyre, L. Pacholski, J. Paris. - Amsterdam : North Holland, 1978.

5. Boolos G. The Unprovability of Consistency: An Essay in Modal Logic. — Cambridge : Cambridge University Press, 1979.

6. Artemov S., Beklemishev L. Provability logic // Handbook of Philosophical Logic, 2nd ed. / Ed. by D. Gabbay, F. Guenthner. - Dordrecht: Kluwer, 2004.- Vol. 13. — P. 229-403.

7. Beklemishev L. On the Craig interpolation and the fixed point, property for GLP // In: Proofs, Categories and Computations. Essays in honor of G. Mints / Ed. by S. Fefermari, W. Sieg. - London : College Publications, 2010. — Tributes series no. 13. — P. 49-60.

интуиционистской логики высказываний8. Независимо это же понятие сформулировал В. Шавруков, доказавший аналогичный результат для логики GL9. Изучение равномерного интерполяционного свойства было продолжено С. Ги-лярди и М. Завадовски10, а также А. Виссером11. К настоящему моменту это свойство изучено для многих модальных логик. Например, такие логики как К, Grz и Т обладают этим свойством, в то время как К4, S4 им не обладают.

Через v(f) обозначим множество пропозициональных переменных формулы (р. Пусть р — произвольная пропозициональная переменная. Формула в называется р-проекцией формулы tp в логике L, если v{0) С v{ip) \ {р} и для всякой ф, не содержащей р, имеем Lb <р ip L 1- в -Ъч}). Отметим, что р-проекция ip единственна с точностью до отношения эквивалентности в логике L. Если в L существуют р-проекции для всех формул и для всех пропозициональных переменных р, то говорят, что L обладает свойством равномерной интерполяции. Обычное интерполяционное евойстово Крейга является следствием свойства равномерной интерполяции.

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

8. Pitts A. On an interpretation of second-order quantification in first order intuitionistic prepositional logic // The Journal of Symbolic Logic. - 1992. - Vol. 57. - P. 33-52.

9. Shavrukov V. Subalgebras of diagonalizable algebras of theories containing arithmetic // Dissertationes Mathematicae. — 1993. — Vol. 323.

10. Ghilardi S., Zawadowski M. A sheaf representation and duality for finitely presented Heyting algebras // The Journal of Symbolic Logic. - 1995. — Vol. 60. - P. 911-939.

11. Visser A. Uniform interpolation and layered bisimulation // Logical foundations of Mathematics, Computer Science and Physics - Kurt Godel's Legacy, Godel '96, Brno, Chech Republic, Proceedings / Ed. by P. H/Sjek.- Berlin : Springer-Verlag, 1996.- Vol. 6 of Lecture Notes in Logic. — P. 139-164.

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

(ku)v b4CL и, ((su)v)w i->a (uw){vw).

Простейшим шагом вычисления терма и является замена произвольного вхождения левой части правила на соответствующую правую. Если терм v получается из терма и с помощью конечной (возможно пустой) последовательности таких замен, то говорят, что и редуцируется к v, и записывают и -»*L v.

Оказывается, что порядок, в котором применяются правила преобразования термов, в каком-то смысле не имеет значения, а именно имеет место свойство конфлюэнтности (свойство Черча-Россера): если и —>*L v и и —>*L v', то существует терм w такой, что v ->*L w и v' —w.

Еще раз отметим, что система комбинаторной логики CL представляет собой полную по Тыорингу вычислительную модель.

Хорошо известно, что проблема распознавания свойств вычислимых функций по их программам в нетривиальных случаях алгоритмически неразрешима. С практической точки зрения необходим инструмент, дающий возможность удобно выражать и фиксировать хотя бы некоторые свойства программ. Одним из таких инструментов является типизация — механизм при-писываения термам типов. Сформулируем самый простой вариант типовой комбинаторной логики CL^12. снабженный так называемыми простыми типами. Операции, с помощью которых строятся типы этой системы, мы будем называть конструкторами. Вхистеме CL_> типы строятся из типовых пере-

12. Troelstra A., Schwichtenberg Н. Basic Proof Theory. — Cambridge : Cambridge Univerist.y Press, 1996. — Vol. 43 of Cambridge Tracts in Theoretical Computer Science.

менных р; с помощью бинарного конструктора —)■; а типизированные термы определяются по следующим правилам:

• для каждого типа Р имеется счетный набор переменных х[;

• в каждом из типов указанного в верхних индексах вида есть свои константы:

• если и Vе — термы, типы которых указаны в верхних индексах, то (ир^сур)С тоже терм (типа С);

• терм ир имеет тип Р.

Неформально говоря, объекты типа С -¥ Р соответствуют функциям из множества объектов типа С в множество объектов типа Р.

В отличие от бестиповой системы С1. все типизированные термы обладают свойством сильной нормализуемое™: процесс вычисления терма завершается за конечное число шагов независимо от порядка применения правил преобразования термов.

Если к терму и нельзя применить никакое правило, то говорят, что он находится в нормальной форме. Из свойств сильной нормализуемости и кон-флюэнтиостн олодуот, что каждый типизированный терм С1—+ независимо от порядка применения правил преобразования вычисляется к своей единственной нормальной форме.

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

Поскольку выразительная сила системы простых типов сравнительно невелика, часто её обогащают дополнительными конструкциями, многие из которых имеют логические аналоги (декартово произведение — конъюнкция, дизъюнктное объединение — дизъюнкция, зависимое произведение — интуиционистский квантор всеобщности, и т.п.). Одним из подобных расширений является введенная С. Артемовым система рефлексивной комбинаторной логики RCL6'13. Она расширяет типовую комбинаторную логику новым конструктором для типов и : F, выражающим суждение <гтерм и имеет тип F» («и есть доказательство формулы F»). Также добавляются новые константы d, с и о, смысл которых будет объяснен ниже.

Поскольку типизированные термы типовой комбинаторной логики CI__>

соответствуют выводам в интуиционистском ичислении высказываний, естественно представить себе систему следующего уровня, типизированные термы которой соответствуют выводам в логике CL.+. В такой системе типизированный терм должен иметь тип, соответствующий выводимому в CL_+ утверждению «терм и имеет тип F». Можно продолжить это рассуждение и представить себе систему более высокого уровня, типизированные термы которой представляют выводы в предыдущей системе, и т.д.. Неформально говоря, рефлексивная комбинаторная логика была сформулирована, как простейшая система типов и термов, содержащая все эти уровни, а также позволяющая внутри себя переходить от термов одного уровня к термам другого уровня. Естественно, что введенная таким образом система позволеят представлять свои собственные выводы с помощью своих собственных типизированных термов (так называемое свойство интернализации выводов).

Перейдем к формальным определениям. Множества типов и типизированных термов RCL определяются совместной индукцией по следующим пра-

13. Krupski N. Typing in reflective combinatory logic // Annals of Pure and Applied Logic. - 2006. — Vol.

141, no. 1-2.- P. 243-256.

вилам:

• стандартные правила типовой комбинаторной логики С1__>:

1. имеется счетный набор типовых переменных р*;

2. если ^ и б - типы, то Р в — тоже тип;

3. для каждого типа имеется счетный набор переменных^ (типа Р)-,

4. для любых типов Р, б и Я имеются константы к типа Р (С? —»

и в типа (С? -> Я)) -> ((^ -> С) -> Я));

5. если и^0 и / — термы, типы которых указаны в верхних индексах, то (ир~>ауЕ)° — тоже терм (типа С):

• новые правила:

6. если терм и имеет тип Р, то выражение и : Р является типом;

7. если и — терм типа Р, то !и — терм типа и : .Р;

8. для каждого терма и типа Р имеется константа (1 типа [и : -4 Г;

9. для любых термов и типа Р О и V типа Р имеется константа о типа и : (Р (?) ->■ (и : Р -» (да) : С);

10. для каждого терма и типа Р имеется константа с типа (и : Р) —> !и : (и : Р).

Поскольку первые пять правил пришли в это определение из типовой комбинаторной логики С1._>, их значение не меняется. Шестое правило выражает смысл типов вида и : Р. Оно означает, что терм и имеет тип Р тогда и только тогда, когда выражение и : Р является типом. Следующее правило, неформально говоря, утверждает, что если терм и представляет доказательство для Р, то для и : Р существует доказательство более высокого уровня.

Поскольку термы типа и: .Р, интуитивно, могут содержать больше информации, нежели терм и, мы также называем их метаописаниями и. Оставшиеся три правила вводят новые комбинаторы: комбинатор д, типа (и : Р) —> Р представляет функцию, отображающую метаописание терма и в сам терм и, комбинатор о реализует аппликацию на уровне метаописаний, и с представляет функцию, отображающую метаописание заданного объекта в описание более высокого уровня.

Выражение ИСХ называется правильно построенным, если оно является типом или типизированным термом.

Чтобы сформулировать понятие редукции в случае системы естественно рассмотреть правила преобразования термов следующего вида:

(,ки)у н- и, ((зи)у)ги (ши)(ьи)),

с1(\и) и, с(!и) (->!(!и), о(!и)(!г;)

Каждое из этих пяти правил выражает интуитивное значение соответствующего комбинатора. В то же время результат применения какого-либо из этих правил к правильно построенному выражению РСЬ может не оказаться правильно построенным. Например, тип !(кху) : (кху : рг) может быть редуцирован к формуле !х : (кху : рг), но последняя, согласно нашему определению, не является типом.

Данный пример наводит на мысль, что в процессе редукции правильно построенного выражения следует одновременно применять заданное правило ко всем вхождениям её левой части. Пусть применение правила а Ь к выражению е означает одновременную замену всех вхождений а в е на Ь; результат этой операции обозначим через е[а и- Ь].

Данное определение обеспечивает сохранение правильной построенности относительно редукций для всех выражений, не содержащих комбинатор</.

Чтобы обеспечить сохранение правильной построенности для псех выражений, В. Крупский предложил расширить систему RCL до системы RCL+, добавив два дополнительных условия:

— если oF — комбинатор и а ь* b — правило преобразования термов, то 0г[(мь] тоже является комбинатором,

— если аи6ис!->с1- правила преобразования термов и а графически не равно с, то а[с ь» â\ и- Ь[с н* ci] также является правилом преобразования термов.

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

Цель диссертационной работы состоит в изучении интерполяционных свойств логик доказуемости GL и GLP и исследовании свойств отношения редукции системы RCL+.

Основные результаты, представленные в работе, являются новыми и состоят в доказательстве следующих фактов:

• логика GL обладает интерполяционным свойством Линдона;

• логика GLP обладает равномерным интерполяционным свойством;

• расширенная система RCL+ обладает свойствами сильной нормализуе-мости и конфлюэнтности.

Апробация работы. Результаты диссертации докладывались на следующих конференциях и семинарах: XVII Международная конференция студентов, аспирантов и молодых учёных «Ломоносов» (Москва, МГУ, 2010); International Workshop «Proof, Computation, Complexity» (Швейцария, 2010); Workshop on Logic, Language, Information and Computation (США, 2011); семинары кафедры математической логики и теории алгоритмов механико-математического факультета МГУ (Москва, МГУ, 2009, 2010).

Публикации. Материал диссертации опубликован в трех работах, список которых приведен в конце автореферата [1-3].

Структура и объем диссертации. Диссертация состоит из введения, двух глав и списка литературы. Объем диссертации составляет 63 страницы, включая 3 рисунка. Список литературы содержит 27 наименований.

Содержание работы

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

Первая глава посвящена исследованию интерполяционных свойств логик доказуемости GL и GLP. Полимодальная логика доказуемости GLP является пропозициональной модальной логикой в языке со счетным числом модальностей [0],[1],[2] и т.д.. Мы обозначаем символом (п) двойственнную к [п] модальность, то есть {п)(р = ->[п]->(£>. Следующий список аксиом и правил вывода задает систему GLP.

Схемы аксиом:

(i) Тавтологии логики высказываний;

(ii) V) [пЩ]

(iii) [n]([n]^ —>• tp) ->■ [п]<р (аксиома Лёба);

(iv) {т)(р —»• \п](т)tp, при т < п\

(v) \m\ip -)• [тг]у>, при т <п (аксиома монотонности). Правила вывода: modus ponens, ip/[n\ip.

Первые три схемы аксиом в языке с единственной модальностью [0] определяют логику доказуемости Геделя-Леба GL. Всякая формула в языке логики GL, выводимая в GLP, будет выводима уже в GL.

Для доказательства свойства равномерной интерполяции системы GLP, в работе рассматривается логика М, фрагмент GLP, получающийся отбрасыванием схемы аксиом (iv).

Обозначим через v+(<p) множество пропозициональных переменных, имеющих позитивное вхождение в формулу^, через v~(ip) — множество переменных, имеющих негативное вхождение. Пусть т(ф) — номер максимальной модальности, входящей в формулу ф. Если ф не содержит модальностей, то т(ф) = —1.

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

Теорема 2 (Интерполяционное свойство) Если M H <р ф, то существует формула в такая, что v+(6) С v+(ip) П У+(ф), ь~(в) С v~(tp) П ь~(ф), т(9) < min{m(ip), т(ф)} и

M Ь ^ 0, M \-6^ф.

Из этой теоремы, используя консервативность логики M над GL, непосредственно следует наличие интерполяционного свойства Линдона в случае GL. Заметим, что вопрос о наличии свойства Линдона для системы GLP, по-видимому, пока отрыт.

Равномерное интерполяционне свойство системы GLP установлено сведением к фрагментам логики M, а затем погружением этих фрагментов в модальное ^-исчисление. Используя результат Дж. Д'Агостино и М. Холленберга14

14. D'Agostino G., Hollenberg M. Logical questions concerning the mu-calculus: Interpolation, Lyndon and Los-Tarski // J. Symb. Log. — 2000. — Vol. 65, no. 1. — P. 310-332.

о том, что модальное /^-исчисление обладает свойством равномерной интерполяции, выводится наличие данного свойства также для системы GLP.

Первая глава завершается рассмотрением системы J15, важного фрагмента GLP, получающегося заменой схемы аксиом (v) на следующие две выводимые в GLP схемы:

(vi) [m]ip [m)[n]ip, при m < n;

(vii) [m]if [n][m]y, при m < n.

Доказано, что J обладает свойством Линдона и не обладает свойством равномерной интерполяции.

Результаты первой главы опубликованы в работе [1]. Во второй главе изучаются свойства отношения редукции системы RCL+. Установлено, что система RCL+ обладает свойствами сильной нормализуемое™ и конфлюэнтности. Доказательство этого факта носит достаточно техническое характер и проводится сведением к случаю двух более простых систем выражений и редукций.

Сперва изучается система CL-— вариант типовой комбинаторной логики, соответствующий интуиционистской модальной логике IS416'17'18. Для этой системы установлены свойства сильной нормализуемое™ и конфлюэнтности. Доказательство свойства сильной нормализуемое™ получается с по-

15. Beklemishev L. Kripke semantics for provability logic GLP // Annals of Pure and Applied Loeic - 2010. — Vol. 161.-P. 756-774.

16. Bierman G., de Paiva V. On an intuitionistic modal logic // Studia Logiea. — 2000. — Vol. 65, no. 3. — P. 383-416.

17. Martini S., Masini A. A computational interpretation of modal proofs // Proof Theory of Modal Logics / Ed. by H. Wansing. - Kluwer, Dordrndit, 1996. - P. 213-241.

18. Pfenning F., Wong H. On a modal lambda-calculus for S4 // Proceedings of the Eleventh Conference . on Mathematical Foundations of Programming Semantics, New Orleans, Louisiana, March 1995 / Ed. by S. Brookes, M. Main.— Vol. 1 of Electronic Notes in Theoretical Computer Science. - Elsevier, 1995,— P. 515-534.

мощью интерпретации С1__в типовом лямбда-исчислении с отношением

/3-редукции. Свойство конфлюэнтности непосредственно следует из сильной нормализуемости и отсутствия у данной системы критических пар.

После этого изучается специфическое множество выражений, содержащее все правильно построенные выражения ИС1.+. На этом множестве вводится вспомагаетльное отношение редукции Затем, используя уже установленные свойства системы С1__>п, доказывается, что отношение обладает свойствами сильной нормализуемости и конфлюэнтности.

Возвращаясь к системе КС1_+, мы показываем, что отношение редукции системы содержится в транзитивном зымыкании отношения Отсюда непосредственно следует свойство сильной нормализуемое™ для системы РС!--. Конфлюэнтность системы ИСЬ1 следует из конфлюэнтности отношения —> и простого наблюдения, состоящего в том, что каждое выражение, находящееся в нормальной форме с точки зрения КС1-+, находится в нормальной форме также с точки зрения отношения Данное наблюдение позволяет завершаить доказательство.

Результаты второй главы опубликованы в работах [2, 3].

Автор выражает глубокую благодарность своим научным руководителям, члену-корреспонденту РАН Л.Д. Беклемишеву и кандидату физико-математических наук, доценту В.Н. Крупскому, за постановку задач и всестороннюю поддержку.

Список публикаций

[1] Шамканов Д. Интерполяционные свойства логик доказуемости СЬ и

СЬР // Труды МИАН.- 2011. - Т. 274. - С. 329-342.

[2] Shamkanov D. Strong normalization and confluence for reflexive combinatory logic // Proof, Computation, Complexity, PCC 2010, International Workshop, Proceedings / Ed. by K. Brünnler, T. Studer ; Technical Report IAM-10-01, Institut für Informatik und angewandte Mathematik, University of Bern. — 2010. - P. 31-32.

[3] Shamkanov D. Strong normalization and confluence for reflexive combinatory logic // Logic, Language, Information and Computation, 18th International Workshop, WoLLIC 2011, Philadelphia, PA, USA, May 2011, Proceedings / Ed. by Lev D. Beklemishev, Ruy de Queiroz. - Vol. 6642 of Lecture Notes in Computer Science. — Springer, 2011. — P. 228-238.

Отпечатано в отделе оперативной печати Геологического ф-та МГУ Тираж |£>0 экз. Заказ № /¡Г