WWW.DISSERS.RU

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА

   Добро пожаловать!

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

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

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

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

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

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

Москва – 2012

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

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

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

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

Защита диссертации состоится 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 тогда и то лько тогда, когда любой ариф ме тический перевод формулы доказуе м в арифметике Пеано PA.

Г. Джапаридзе2 сформулировал полимодальный вариант логики доказу­ емости GLP, рассмотрев язык пропозициональной логики, снабженный счет­ ным числом модальностей [0], [1],.... Для каждого n арифметическим перево­ дом модальности [n] является формула, выражающая доказуемость в теории PA, обогащенной всеми истинными n-предложениями. Аналогично случаю 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 K. On strong provability predicates and the associated modal logics // The Journal of Symbolic Logic. — 1993. — Vol. 58. — P. 249–290.

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

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

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

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

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

Одним из существенных усилений интерполяционного свойства Крейга является свойство равномерной интерполяции. Впервые оно было сформули­ ровано А. Питтсом, установившим свойство равномерной интерполяции для 4. Smorynski C. 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 Univer­ sity 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. Feferman, W. Sieg. — London : College Publications, 2010. — Tributes series no. 13. — P. 49–60.

интуиционистской логики высказываний8. Независимо это же понятие сфор­ мулировал В. Шавруков, доказавший аналогичный результат для логики GL9.

Изучение равномерного интерполяционного свойства было продолжено С. Ги­ лярди и М. Завадовски10, а также А. Виссером11. К настоящему моменту это свойство изучено для многих модальных логик. Например, такие логики как K, Grz и T обладают этим свойством, в то время как K4, S4 им не обладают.

Через () обозначим множество пропозициональных переменных фор­ мулы . Пусть p — произвольная пропозициональная переменная. Формула называется p-проекцией формулы в логике L, если () () {p} и для всякой , не содержащей p, имеем L L . Отметим, что p-проекция единственна с точностью до отношения эквивалентности в логике L. Если в L существуют p-проекции для всех формул и для всех пропо­ зициональных переменных p, то говорят, что L обладает свойством равно мер­ ной интерпо ляции. Обычное интерполяционное свойстово Крейга является следствием свойства равномерной интерполяции.

Вторая часть диссертации посвящена исследованию так называемой ре­ флексивной комбинаторной логики. Среди различных вычислительных мо­ делей особое место занимают системы, являющиеся прототипами функци­ ональных языков программирования. Простейшими системами такого рода являются комбинаторная логика и лямбда-исчисление. Напомним, что тер­ 8. Pitts A. On an interpretation of second-order quantification in first order intuitionistic propositional 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, Com­ puter Science and Physics – Kurt G Legacy, G ’96, Brno, Chech Republic, Proceedings / Ed. by odel’s odel P. H — Berlin : Springer-Verlag, 1996. — Vol. 6 of Lecture Notes in Logic. — P. 139–164.

ajek.

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

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

(ku)v u, ((su)v)w (uw)(vw).

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

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

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

Хорошо известно, что проблема распознавания свойств вычислимых функ­ ций по их программам в нетривиальных случаях алгоритмически неразре­ шима. С практической точки зрения необходим инструмент, дающий воз­ можность удобно выражать и фиксировать хотя бы некоторые свойства про­ грамм. Одним из таких инструментов является типизация — механизм при­ писываения термам типов. Сформулируем самый простой вариант типовой комбинаторной логики CL12, снабженный так называемыми простыми ти­ пами. Операции, с помощью которых строятся типы этой системы, мы будем называть конструкторами. В системе CL типы строятся из типовых пере­ 12. Troelstra A., Schwichtenberg H. Basic Proof Theory. — Cambridge : Cambridge Univeristy Press, 1996. — Vol. 43 of Cambridge Tracts in Theoretical Computer Science.

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

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

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

kF (GF ) и s(F (GH))((F G)(F H));

если uF G и vF –– термы, типы которых указаны в верхних индексах, то (uF GvF )G тоже терм (типа G);

терм uF имеет тип F.

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

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

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

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

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

Поскольку типизированные термы типовой комбинаторной логики CL соответствуют выводам в интуиционистском ичислении высказываний, есте­ ственно представить себе систему следующего уровня, типизированные тер­ мы которой соответствуют выводам в логике CL. В такой системе типи­ зированный терм должен иметь тип, соответствующий выводимому в CL утверждению «терм u имеет тип 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.

вилам:

стандартные правила типовой комбинаторной логики CL:

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

2. если F и G — типы, то F G — тоже тип;

3. для каждого типа имеется счетный набор переменных xF (типа F );

i 4. для любых типов F, G и H имеются константы k типа F (G F ) и s типа (F (G H)) ((F G) (F H));

5. если uF G и vF –– термы, типы которых указаны в верхних индек­ сах, то (uF GvF )G — тоже терм (типа G);

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

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

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

8. для каждого терма u типа F имеется константа d типа (u : F ) F ;

9. для любых термов u типа F G и v типа F имеется константа o типа u : (F G) (v : F (uv) : G);

10. для каждого терма u типа F имеется константа c типа (u : F ) !u : (u : F ).

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

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

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

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

(ku)v u, ((su)v)w (uw)(vw), d(!u) u, c(!u) !(!u), o(!u)(!v) !(uv).

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

Данный пример наводит на мысль, что в процессе редукции правильно построенного выражения следует одновременно применять заданное правило ко всем вхождениям её левой части. Пусть применение правила a b к выражению e означает одновременную замену всех вхождений a в e на b;

результат этой операции обозначим через e[a b].

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

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

— если oF — комбинатор и a b — правило преобразования термов, то oF [ab] тоже является комбинатором, — если a b и c d — правила преобразования термов и a графически не равно c, то a[c d] b[c d] также является правилом преобразования термов.

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

Цель диссертационной работы состоит в изучении интерполяцион­ ных свойств логик доказуемости 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] и т.д.. Мы обозначаем символом n двойственнную к [n] модальность, то есть n ¬[n]¬. Следующий список аксиом и пра­ вил вывода задает систему GLP.

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

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

(ii) [n]( ) ([n] [n]);

(iii) [n]([n] ) [n] (аксиома Лёба);

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

(v) [m] [n], при m < n (аксиома монотонности).

Правила вывода: modus ponens, /[n].

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

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

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

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

Теорема 2 (Интерполяционное свойство) Если M , то существу­ ет формула такая, что +() +() +(), -() -() -(), m() min{m(), m()} и M , M .

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

Равномерное интерполяционне свойство системы GLP установлено сведе­ нием к фрагментам логики M, а затем погружением этих фрагментов в мо­ дальное µ-исчисление. Используя результат Дж. Д’Агостино и М. Холленберга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] [m][n], при m n;

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

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

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

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

Сперва изучается система CL — вариант типовой комбинаторной ло­ гики, соответствующий интуиционистской модальной логике IS416,17,18. Для этой системы установлены свойства сильной нормализуемости и конфлюэнт­ ности. Доказательство свойства сильной нормализуемости получается с по­ 15. Beklemishev L. Kripke semantics for provability logic GLP // Annals of Pure and Applied Logic. — 2010. — Vol. 161. — P. 756–774.

16. Bierman G., de Paiva V. On an intuitionistic modal logic // Studia Logica. — 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, Dordrecht, 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.

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

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

Возвращаясь к системе RCL+, мы показываем, что отношение редукции системы RCL+ содержится в транзитивном зымыкании отношения. Отсю­ да непосредственно следует свойство сильной нормализуемости для системы RCL+. Конфлюэнтность системы RCL+ следует из конфлюэнтности отноше­ ния и простого наблюдения, состоящего в том, что каждое выражение, находящееся в нормальной форме с точки зрения RCL+, находится в нор­ мальной форме также с точки зрения отношения. Данное наблюдение поз­ воляет завершаить доказательство.

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

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

Список публикаций [1] Шамканов Д. Интерполяционные свойства логик доказуемости GL и GLP // Труды МИАН. — 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. Brunnler, T. Studer ; Technical Report IAM-10-01, Institut f Informatik und angewandte Mathematik, University of Bern. — ur 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.






© 2011 www.dissers.ru - «Бесплатная электронная библиотека»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.