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

На правах рукописи УДК 510.53

Шлепаков Сергей Петрович

О РЕШЕНИЯХ ФУНКЦИОНАЛЬНЫХ УРАВНЕНИЙ В НЕКОТОРЫХ РАЗРЕШИМЫХ ТЕОРИЯХ

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

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

Москва — 2005

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

Научные руководители:

Официальные оппоненты:

Ведущая организация:

доктор физико-математических наук, профессор Успенский Владимир Андреевич, кандидат физико-математических наук, доцент Крупский Владимир Николаевич доктор физико-математических наук, профессор Тайцлин Михаил Абрамович, кандидат физико-математических наук Яворский Ростислав Эдуардович Московский государственный университет путей сообщения (МИИТ)

Защита диссертации состоится 18 ноября 2005 г. в 16 ч. 15 мин. на заседании диссертационного совета Д.501.001.84 в Московском государственном университете им. М. В. Ломоносова по адресу 119992, ГСП-2, Москва, Ленинские горы, МГУ, Механико-математический факультет, аудитория 14-08.

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

Автореферат разослан 18 октября 2005 г.

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

В. Н. Чубариков

mi гшш

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

Актуальность темы

В 1984 году Шостак [I]1 ввел в рассмотрение специальный класс разрешимых теорий первого порядка, впоследствии названных теориями Шостака. Сигнатура такой теории содержит единственный предикатный символ — равенство, а сама теория описывается с помощью двух алгоритмов: алгоритма приведения к нормальной форме и алгоритма решенья уравнений. Требования, предъявляемые к этим алгоритмам, сформулированы в виде фиксированного набора свойств и являются их абстрактной спецификацией. Описание теорий посредством абстрактной спецификации указанных алгоритмов позволяет использовать теории Шостака в программных реализациях различных разрешающих процедур модульно, не вдаваясь в детали теории. Примером такого "равномерного" использования служит единый для всех теорий Шостака алгоритм распознавания следствий из заданной системы равенств, который используется в целях ускорения разрешающих процедур для комбинации теорий по методу Нельсона-Оппена ([2]2, [З)3, [4]4).

Алгоритм приведения термов к нормальной форме (канонизатор) по данному терму выбирает в классе равных термов канонического представителя. Алгоритм приведения к нормальной форме я- определяет теорию Т„, в которой он задан: эта теория аксиоматизируется множеством всех равенств вида t = тгё, где £ — терм.

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

'¡IJShostak Я Е. Deciding combinations of theories // ACM. 1984. V 31(1) P. 1-12

'pjMANNA Z., Zarba C. G Combining decision procedures // Formal Methods at the Cross Roads: From Panacea to Foundational Support, LNCS. 2004.

3|3]Barrett C. W., Dill D. L., Stump A A generalization of Shostak's method for combining decision procedures // FroCoS. 2002.

4|4]Shankar N, Ruess H. Combining Shostak theories // International Conference Rewriting Techniques and Applications. 2003. V 2378 LNCS. P. 1-18.

РОС. НАЦИОНАЛЬНАЯ г БИБЛИОТЕКА , !

1 ¿"-CTf I

'""■ I ii ■.■» i*

ik

1*

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

Примером теории Шостака будет линейная арифметика над кольцом целых и рациональных чисел, выпуклая (без nil) теория списков, теория массивов, теория диаграмм Венна ([1], [2]).

Упомянутая выше задача распознавания следствий из заданной системы равенств S для теории Шостака имеет естественное решение. Достаточно рассмотреть 5 как систему уравнений на входящие в нее переменные и найти ее общее решение в виде подстановки е. Равенство а = Ь является следствием S тогда и только тогда, когда нормальные формы термов еа и еЬ совпадают.

Попытки обобщить этот метод на случай комбинации нескольких (даже двух) теорий Шостака сталкиваются с существенными трудностями. В работе [1] Шостак предложил обобщение метода на случай комбинации теории Шостака с теорией без собственных нелогических аксиом, известное как алгоритм Шостака. Он рассматривал следующее языковое расширение базовой теории. Множество термов расширяется за счет введения новых "неинтерпре-тированных" функциональных символов дг, по существу, переменных второго порядка, причем термы вида gi(t) рассматриваются (анализируются канони-затором) как отдельные переменные первого порядка.

Обобщение процедуры решения уравнений базовой теории на расширенную теорию оказывается сложной задачей. Основная трудность при решении системы уравнений в языке второго порядка состоит в необходимости обеспечить функциональную зависимость неизвестного значения g,(f) от значений t, которые также являются неизвестными. Это обстоятельство приводит к добавлению в систему условных равенств вида

9i{h) = 9i(h),

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

Варианты алгоритма Шостака (например, [5]5, [б]6) при верификации формул вида S —У а = Ь реализуют процедуру конгруэнтного замыкания и фактически оперируют с S как с системой уравнений на неизвестные вида g%(t).

5|5)Shankar N., Ruess Н Deconstructing Shostak // Proceedings of the Sixteenth IEEE Symposium LICS, IEEE Computer Society Press. 2001. P. 19-28

'(6|GanzWGER H. Shostak Light // Automated Deduction CADE-18 2002. V 2392 LNCS P. 332-346

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

Центральным моментом всех вариантов алгоритма Шостака является интерпретация системы равенств как системы символических уравнений на входящие в нее переменные, включая переменные второго порядка (g,). Но до настоящего времени не было известно ни описания множества решений произвольной системы, ни даже точного определения понятия решения, что делало практически невозможным доказательство полноты метода. Первоначальное доказательство Шостака [1| содержало существенные пробелы, обоснования в более поздних вариантах алгоритмов в [5], (4] также не являются удовлетворительными. Попытка прояснения ситуации была предпринята в (6], где метод Шостака изложен упрощенно в виде стратегии построения вывода в некотором специальном исчислении равенств. Однако, как указывают в [7]7 разработчики системы Simplify (HP Labs, система доказательства теорем для проверки программ), им пришлось отказаться от метода Шостака, т.к. приведенных выше работ оказалось недостаточно для эффективного практического применения метода.

Цель работы

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

7|7]Detlefs D , Nelson G., Saxe J B. Simplify- A Theorem Prever for Program Checking // Systems Research Center, HP Laboratories Palo Alto. HPL-2003-148. 2003

Основные методы исследования

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

Научная новизна

Результаты работы являются новыми. Основными из них являются следующие:

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

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

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

4. Найдена модельная характеризация понятия унифицируемости в теориях Шостака. Показано, что унифицируемость системы эквивалентна ее выполнимости в канонической модели второпорядковой теории Шостака.

5. Построен алгоритм, который для каждой унифицируемой системы S и терма t строит (t mod 5) — каноническую форму терма t по модулю S. При этом синтаксическое равенство (о mod S) = {b mod S) оказывается эквивалентным истинности в канонической модели формулы S —» а = Ь, что дает еще один метод верификации утверждений такого вида.

Практическая и теоретическая ценность

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

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

Апробация работы

Результаты диссертации докладывались на XXIV Конференции молодых ученых Механико-математического факультета МГУ (2002 г.), XXVI Конференции молодых ученых Механико-математического факультета МГУ (2004 г.), семинаре "Логические проблемы информатики "(руководители семинара -профессора С.Н. Артемов, М.Р. Пентус и доценты В.Н. Крупский, Т.Л. Яворская, неоднократно), а также на научно-исследовательском семинаре кафедры математической логики и теории алгоритмов Механико-математического факультета МГУ.

Публикации

Результаты диссертации опубликованы в работах [1-4], список которых приводится в конце реферата.

Структура и объем работы

Работа состоит из введения, трех глав и списка литературы Объем диссертации — 85 страниц, список литературы содержит 31 наименование

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

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

Глава 1 носит вспомогательный характер и посвящена решениям систем уравнений в теории первого порядка с равенством, сигнатура С1 которой состоит из констант с3 и функциональных символов }3 В параграфе 1.1 определяется множество термов первого порядка ТтМ с переменными из множества Уат^1' и вводятся основные понятия для языка первого порядка сигнатуры П. Параграф 1 2 вводит понятие канонизатора для языка первого порядка.

Определение 1.2.1 Пусть Тт- множество термов первого порядка Назовем канонизатором такую вычислимую функцию п : Тт''' —> Тт^.

что 1) 7гх = х; 2) Var{-Kt) С Var(t); 3) для любой подстановки а выполнено crt~x<nrt-, 4) если 7ri = f(t\,..., tn), то 7rt, = i,-, 5) f(t) /(wî).

С данным канонизатором ж связывается теория Тж, заданная набором аксиом t = nt, t € TmSl\ ее каноническая модель - интерпретация сигнатуры fi с носителем М„ = { rrt 11 G Tm(1) }, для которой с** = тге,, /'* (?) = -rrf} (t), и отношение эквивалентности на термах: 7га = ттЬ Если

V С УаИ1), a а,/3 — два отображения множества всех термов в себя, то запись означает, что at fit выполняется для всех термов t таких,

что Var{t) С V.

Параграф 1.3 посвящен спецификации алгоритма решения уравнений и его распространению на случай конечных систем. Ниже (3й') ц> означает замыкание формулы ¡р кванторами существования по переменным из множества W, а (3) ip - аналогичное замыкание по всем свободным переменным формулы

Мы будем говорить, что задан алгоритм решения уравнений, если задана следующая вычислимая функция solve(U,a = b), зависящая от бесконечного разрешимого множества переменных U и уравнения а — Ъ в языке первого порядка, причем U П Var{a = Ь) = 0. Функция solve возвращает значение X, если Тж I/ (3) (а = 6); в противном случае значение равно такой конечной идемпотентной подстановке е, что 1) Dom(e) Ç Var{a = Ь); 2) W = Var(e) \ Var{a = b)Ç U; 3) Т„ h (3^) е a = Ь.

Теории вида для которых существует алгоритм решения уравнений, называются теориями Шостака. В дальнейшем предполагается, что фиксирована некоторая теория Шостака Т„.

Предлагается единый (не зависящий от выбора теории Шостака) способ преобразования алгоритма solve(U, а = Ь) решения одного уравнения в языке первого порядка в алгоритм solve(U, S) решения конечных систем S таких уравнений. Он возвращает _L или решение системы в смысле следующего определения.

Определение 1.3.2 Пусть U — некоторое бесконечное разрешимое множество переменных, S = { a, = Ь*} — конечная система уравнений, Var{S) П U = 0. Мы будем называть подстановку е решением системы S в присутствии U, если 1) б — конечная идемпотентная подстановка; 2) Dom(е) С Var(S); 3) W = Var(e) \ Var(S) С U; 4) h (3^) 6 о S.

Мы показываем, что solve строит наиболее общее решение системы: Лем-

ма 1.3.6 Пусть ж — канонизатор, S = {а, = 6, | г = 1,... ,п} — система уравнений, U ■— бесконечное разрешимое множество переменных, причем Var(S) П U = 0, V = VarW \ U. Если е = solve{U,S) ф 1, то для любой идемпотпентной подстановки с условием е\а, eib, найдется такая подстановка а, что ei сге. Если solve(U, S) = _L, то не существует подстановки еь для которой eia, ~„6ib,. В этом случае также Тп I/ (3)5.

Глава 2 посвящена системам уравнений на неизвестные вида &(£), появляющиеся в результате добавления к языку множества функциональных переменных второго порядка G =

В параграфе 2.1 определяется множество термов второго порядка 7W2' и множество неизвестных Var® = Var^ U {<?;(£ ъ... ,£„) | U € Tm®}. Через AVar{t) обозначено множество всех подтермов терма t, которые являются неизвестными. Если V С Var^l\ то

Tmf = {te Tm(2) | AVar(t) П Var'1) Ç V}, Varf = Tmf П Var{2\

Определение 2.1.4 Подстановкой на множестве термов второго порядка называется такое отображение а : Тп№ —>■ ТтР\ которое оставляет на месте константы, то есть acj = с}, и коммутирует с функциональными символа^ ми, то есть crfj(ti, ...,£„) = f3{at\,..., <rt„). Такое отображение определяется своим действием на неизвестных.

Определение 2.1.5 Отображение на термах а : Тгг№ Ттп® называется функционально согласованным, если

1. il ~a h => /,(tl) fi(h).

2. il ~a t2 =*■ g,(il) ~a 9i{t2).

Определение 2.1.11 Пусть x — функционально согласованное отображение. Подстановка а называется н-согласованной, если для любой неизвестной g{t) Е Var1-2) выполнено равенство ag(t) crg(xt).

Определение 2.1.14 Для некоторого множества переменных V С Var'1', отображений a,ß : Tm® Tm® обозначим через a ß условие at ~xßt для всех t € Ттпу'.

Параграф 2.2 посвящен построению обобщенного канонизатора, т.е. отображения и, заданного на термах языка второго порядка и обладающего свойствами, аналогичными свойствам канонизатора тт.

Фиксируем некоторое вычислимое биективное отображение z vz, сопоставляющие неизвестным z £ Var® первопорядковые переменные vz €

Var^ Пусть Л : Тгг№ -л Тгг№ — подстановка, порожденная этим отображением. Она обратима.

Определим отображение и : TW2' —> Tm'2' рекурсией по второпорядко-вой VD(t) глубине терма t. Для термов t 6 7W1' положим >rf = Х~1жМ Пусть >rf для t € Tm'2', VD(t) < i уже определено Возьмем терм t € TmSr>, VD(t) = i + 1. Рассмотрим подстановку которая заменяет неизвестные g(ti) глубины, не превосходящей t + 1, на g(xti)

ft+i = { $(**i)/ff(ii) I 9(ii) e Kar«2), < i + 1 },

(действие x на t\ определено ранее). Положим yd = Л-17гЛ^+11. Полученное таким образом отображение х мы будем называть обобщенным канонизатпо-ром.

Лемма 2.2.2 Пусть t\, tz е Tm(1>. Тогда t\ t2 ii

Лемма 2.2.4 Пусть ж — канонизатор. Для соответствующего обобщенного канонизатора х выполняются свойства, аналогичные свойствам 1-5 канонизатора: 1) хх — х, где х £ Var2) Var^\xt) С Var^(t), где Var'1^) = Var(t) П Var(1); 3) а ~хах для любой н-согласованной подстановки а : Тт(2) -4 Тт®; 4) Если xt = f(tu... ,<„), то xtx = tx; 5)№~„f(xi).

Параграф 2 3 рассматривает язык первого порядка в расширенной сигнатуре П', в которой функциональные символы д, добавлены в качестве дополнительных сигнатурных символов. Множество термов 7W1'' в этом языке совпадает с множеством термов в языке второго порядка с неизвестными второго порядка gt, но соответствующее ему понятие подстановки — уже.

Следствие 2.3.2 Обобщенный канонизатор х является каноньзатором первопорядковых термов в сигнатуре О,'.

В параграфе 2.4 демонстрируется неудачность непосредственного переноса алгоритма решения уравнений на случай языка второго порядка и дается формальное определение решения (унификатора) системы функциональных уравнений.

Определение 2.4.2 Пусть даны конечная система уравнений 5" = { а, = Ь, }, термы а.{, Ь, е TmW и обобщенный канонизатор х. Унификатором этой системы называется такая идемпотентная функционально согласованная и х-согласованная подстановка р, для которой верно ра, рЬ, Пусть также задано U — такое множество переменных, что AVar(S) П U = 0, пусть

V — УаИ1' \ и Слабым наиболее общим унификатором (слабым ноу) системы Б в присутствии и называется такой унификатор р, что для любого унификатора в существует подстановка г), для которой верно ограниченное разложение в г)р. Стабильным слабым наиболее общим унификатором системы Б в присутствии и называется такой слабый ноу р, что подстановка цр также будет являться слабым ноу 5 в присутствии [/, где ц — подстановка, для которой — XV для всех неизвестных V € Уаг^.

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

Определение 2.5.1 Пусть IV — некоторое множество неизвестных. Подстановку а назовем {х, У/)-согласованной, если для любой пары неизвестных Як(й),9к(Ь) 6 И^ выполняются условия о\ 1~х<т?2 => о'Як^г) = <тдк(12) и

Определение 2.5.2 Пусть даны подстановка а и множество неизвестных ИЛ Мы будем называть продолжением а по множеству V/ подстановку а, заданную рекурсивно:

ах = ах, если х е Уаг

09k(t)

agk(t), если gk{t) е W,

<79k{h), если gk(t) £ W и существует gk(ti) е W ^

такая, что t~xgti, gk{x<ft), если gk(i) ^ W и не существует gk(ti) 6 W такой, что t •

Множество неизвестных W называется замкнутым, если AVar(t) С W для каждого терма t G W.

Лемма 2.5.3 Пусть W — конечное замкнутое множество неизвестных, а — (x,W)-согласованная подстановка. Пусть также AVar(a) С W. Тогда существует единственная подстановка а, удовлетворяющая условию (1). Она является х-согласованным продолжением a\w на Vor'2'. Если а — идемпотентна, то а идемпотентна, функционально согласована и является наиболее общим идемпотентным, функционально согласованным и х-согласованным продолжением a\w на Var^2\ то есть для любой в — идем-потентной, функционально согласованной и х-согласованной подстановки,

для которой 9\w -- <r\w, имеет место 9~хва.

В параграфе 2.6 описывается процедура unify(U, S), которая принимает в качестве входных параметров бесконечное разрешимое множество вспомогательных переменных U и систему уравнений S с условием AVar(S) П U = 0. Процедура unify(U, S).

1. Пусть S = {о, = Ь,}. Положим i = 0, So = xS - {ха, = xb,}.

2. Если solve(U,St) = -L, останавливаемся с результатом 1. Иначе положим <Т{ = solve(U, S,).

3. Если найдутся такие неизвестные gk{ti),gk(t2) £ AVar(So), что h^xa.h, но crlgk(ti)'/'xatgk(t2), то полагаем S1+1 = 5, U {gk{ti) = (£2)}, г = г + 1 и переходим к шагу 2. Если такой пары не существует, переходим к шагу 4.

4. Пусть <т, = [i,/u,-]. Останавливаемся с результатом с — [xi,/u,].

Теорема 2.6.14 Пусть задан алгоритм решения уравнений solve, обобщенный канонизатор ус. Процедура unify распознает унифицируемость произвольной системы уравнений S и для унифицируемой системы и бесконечного разрешимого множества переменных U с условием AVar{S)C\U = 0 строит подстановку а, для которой а — продолжение а по множеству AVar(xS) U VarW{ff) — является стабильным слабым ноу этой системы в присутствии U.

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

Определение 2.7.1 Для произвольной подстановки а определим подстановку [а]. Для этого определим ее действие на неизвестных индукцией по второпорядковой глубине неизвестной. А именно, для х g Var^ положим [<т]х — ах, а для g(t) € Var(2) положим [cr]g(i) — ag(x[cr}t).

Определение 2.7.4 Пусть даны конечное замкнутое множество неизвестных W и идемпотентная, (н, И^-согласованная подстановка а с условием AVar{&) С W. Мы будем называть коррекцией подстановки а по множеству W подстановку а*:

а* = {x<jxt/xt | х{ € WnVar^}u{xagk(t)/gk(xai) | gk{t) € W\Var(1)}.

Теорема 2.7.6 Пусть даны конечное замкнутое множество неизвестных W и идемпотентная, {x,W)-согласованная подстановка <т, причем

AVar(a) С IV. Тогда для любой неизвестной v € Var^2' имеет место [<j*)v = xa v.

Глава 3 посвящена модельным аспектам понятия унифицируемости В параграфе 3.1 по данной системе уравнений в языке второго порядка строится формула в языке первого порядка, выполнимость которой в канонической модели теории Шостака эквивалентна унифицируемости исходной системы

Определение 3.1.1 Пусть некоторая система уравнений S такова, что Var(S) состоит из неизвестных в каноническом виде, те. таких v. что v = xv Назовем замыканием S такую формулу

Cs = S Л Д (<i = <2 gk(tг) = gk(t2)).

9t(h),gk(Í2)eAVar(S)

Теорема 3.1.2 Пусть S = {а, = 6j}, a,, b, € 7W2' - система уравнений Формула ACxs выполнима в интерпретации 1п тогда и только тогда, когда S унифицируема.

Параграф 3.2 посвящен доказательству эквивалентности унифицируемости системы уравнений и ее выполнимости в канонической модели теории Шостака второго порядка.

Определение 3.2.1 Для языка второго порядка сигнатуры П канонической интерпретацией /2 будем называть соответствующее обеднение интерпретации 1Х сигнатуры ГУ. Ее носитель М2 = { xt 11 € Trn'2' }, а с" = хс},

i!1® =

Теорема 3.2.6 Система уравнений S = {а, = Ь,-}, а,,6, 6 Тт'2' выполнима в канонической интерпретации /2 тогда и только тогда, когда она унифицируема.

Параграф 3.3 вводит операцию mod и показывает корректность применения этой операции для проверки хорновских выражений.

Определение 3.3.1 Пусть S — унифицируемая система уравнений, U — бесконечное разрешимое множество переменных с условием AVar(S) П [/ — 0 и С — некоторый стабильный слабый ноу системы S в присутствии U. Определим операцию mod и таким образом: t mod у S = x(t.

Теорема 3.3.4 Пусть S = {щ = í»<} — унифицируемая система уравнений, U — бесконечное разрешимое множество переменных с условием AVar(S) П U = 0. Обозначим V = Var(1> \ U. Для каждых a,b € Tmj?' выполнено: (S а = Ь) a moda S = b mode/ S.

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

Работы автора по теме диссертации

1. С. П Шлепаков. О решениях систем уравнений в первопорядковых теориях Шостака // Вестник московского университета, серия 1 математика. механика. 2005. №3. 55-57.

2. С. П. Шлепаков. Задачи унификации и функциональные уравнения в свободных алгебрах // Труды XXIV Конференции молодых ученых Механико-математического факультета МГУ им. М.В.Ломоносова. 2002. 196-198.

3. С. П. Шлепаков. О решениях функциональных уравнений в теориях Шостака // Труды XXVI Конференции молодых ученых Механико-математического факультета МГУ им М.В.Ломоносова 2004 250-253

4. С. П. Шлепаков. Второпорядковая унификация в теориях Шостака // Деп. в ВИНИТИ. ЛП767-В2004. М. ВИНИТИ. 2004. 39 с.

»18847

РНБ Русский фонд

2006-4 21602

Издательство ЦПИ при механико-математическом факультете МГУ им М В. Ломоносова.

Подписано в печать 0£ с

Формат 60 х 90 1 /16 . ' Уел печ. л. 0,

Тираж 100 экз. Заказ ¿2

0.1 Введение.

1 Решение систем уравнений в языке первого порядка

1.1 Язык первого порядка

1.2 Канонизатор.

1.3 Алгоритм решения уравнений.

2 Решение систем уравнений в языке второго порядка

2.1 Язык второго порядка.

2.2 Канонизатор для языка второго порядка.

2.3 Канонизатор для языка первого порядка в расширенной сигнатуре.

2.4 Решения уравнений с функциональными переменными

2.5 Построение согласованных подстановок.

2.6 Алгоритм унификации.

2.7 Вычисление а.

2.8 Условная унификация.

3 Выполнимость и унифицируемость

3.1 Модели первого порядка.

3.2 Модели второго порядка.

3.3 Операция mod.

Развитие систем проверки правильности программ и доказательств (program verification, proof checking) потребовало создания эффективных разрешающих процедур (decision procedures) для различных подтеорий, а также для их комбинации Под разрешающей процедурой здесь понимается алгоритм, который для любой формулы из некоторого фиксированного класса определяет ее выполнимость в данной теории, причем он всегда останавливается с положительным или отрицательным ответом. Разрешающие процедуры улучшают эффективность системы верификации и освобождают пользователя от многих однообразных и утомительных действий Разрешающие процедуры существуют для многих практически используемых теорий — для линейной арифметики над кольцом целых [9] и рациональных чисел [10], для теорий структур данных, которые часто используются в программах — для списков [11], массивов [12], множеств [13], мультимножеств [14].

Комбинация теорий — это множество формул в объединенной сигнатуре, являющееся дедуктивным замыканием их объединения. Методы разрешения некоторых видов формул в комбинации теорий были предложены, например, в [15], [16], [17], [18], [5], [6], [1],

2], [3], [4], [7]

Пусть Тг, г G I — конечное множество теорий с равенством, сигнатуры Пг которых попарно не пересекаются Нельсон и Оппен [17] предложили общий метод разрешения бескванторных формул в комбинации теорий Тг Для применения этого метода необходимо, чтобы каждая теория была стабильно бесконечной Последнее требование означает, что для каждой бескванторной формулы, выполнимой в некоторой модели теории, существует бесконечная модель, в которой она выполнима

На первом шаге проблема выполнимости бескванторных формул общего вида с помощью приведения к ДНФ сводится к ее частному случаю для формул F, являющихся конъюнкцией атомарных формул и их отрицаний, выполнимость исходной формулы эквивалентна выполнимости хотя бы одной из элементарных конъюнкций, составляющих ДНФ

Следующий шаг — абстракция — за счет введения новых переменных преобразует формулу F в конъюнкцию формул АгРг так, что каждый член конъюнкции составлен из символов сигнатуры только одной теории, и каждой теории соответствует только одна формула Fu причем выполнимость F эквивалентна выполнимости AtFi Для этого каждое вхождение терма вида /(£), где / Е П3, в атомарную формулу P(s) для Р ^ Qj заменяется на новую переменную ж, и к формуле F добавляется новый конъюнктивный член = №

Последний шаг — проверка — рассматривает множество "общих переменных" W, т.е переменных, которые встречаются в более чем одной формуле конъюнкции ЛгРг. Для каждого отношения эквивалентности Е на множестве W рассматривается формула Ре, — конъюнкция равенств и неравенств всех возможных пар переменных из W, причем если хЕу, то Fe содержит х = у, а если -*(хЕу), то Fe содержит х ^ у Формула F выполнима в некоторой модели комбинации теорий Тг тогда и только тогда, когда найдется такое отношение эквивалентности Е, которое было бы совместно с каждой формулой Fz Это означает, что для каждого г формула F% A Fe выполнима в теории Тг

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

Таким образом, метод Нельсона-Оппена — скорее подход к решению задачи, нежели законченное описание процедуры Он используется в таких системах, как CVC [19], ESG [20], EVES [21], SDVS [22], SPV (Stanford Pascal Verifier) [23], Simplify [8] Детальное описание и строгий анализ метода можно найти в [24], [25], [26].

Шостак [6] предложил ограничиться теориями специального вида. Единственным допустимым предикатом является равенство, а сама теория должна описываться с помощью двух алгоритмов: алгоритма приведения к нормальной форме и алгоритма решения уравнений. Класс разрешаемых методом Шостака формул — хор-новские предложения, т.е. формулы вида S -> с = d, где S — система уравнений, понимаемая как конъюнкция равенств, a c,d — термы. Метод Шостака применяется в таких системах верификации, как ICS [27], PVS [28], SVC [29], STeP (Stanford Temporal Prover) [30].

Алгоритм приведения термов к нормальной форме (канониза-тор) по данному терму выбирает в классе равных термов канонического представителя При этом накладывается ряд условий на поведение этого алгоритма (определение 1.2.1). В частности, алгоритм приведения к нормальной форме тт определяет теорию в которой он задан- эта теория аксиоматизируется множеством всех равенств вида t = irt, где t — терм

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

Теории, обладающие алгоритмами приведения к нормальной форме и решения уравнений, называются теориями Шостака. Такими теориями будут, например, линейная арифметика над кольцом целых и рациональных чисел, выпуклая (без ml) теория списков, теория массивов, теория диаграмм Венна ([6], [2])

Шостак полагал, что его метод распознает принадлежность бескванторной хорновской формулы S —а = Ъ комбинации теорий, для каждой из которых заданы канонизатор и алгоритм решения уравнений Он предложил конструкцию объединения нескольких канонизаторов и алгоритмов решения уравнений для разных теорий в единые канонизатор и алгоритм решения уравнений для комбинации теорий С помощью этих средств предполагалось решать S как систему уравнений и подставлять найденные решения в обе части равенства а = Ъ. Если в результате подстановки обе части равенства оказались идентичными, то исходная формула принадлежит комбинации теорий, в противном случае — нет

На самом деле выяснилось ([4]), что предложенный алгоритм решения уравнений в комбинации теории в некоторых случаях приводит к не идемпотентным подстановкам, т е не является корректным в смысле определения алгоритма решения уравнений. Более того, как показано в [31], комбинация любых двух нетривиальных теорий Шостака не может иметь корректный в смысле определения алгоритм решения уравнений Поэтому в настоящее время единственной общей разрешающей процедурой для комбинации теорий остается процедура Нельсона-Оппена.

На самом деле алгоритм решения уравнений для теории Шо-стака допускает использование на последнем шаге процедуры Нельсона-Оппена, поскольку позволяет эффективно рассуждать о равенствах переменных Так, один вызов разрешающей процедуры в методе Нельсона-Оппена может установить равенство (неравенство) одной пары переменных. Алгоритм решения уравнений Шо-стака за один вызов возвращает идемпотентную подстановку, которая позволяет судить о всех вытекающих равенствах, если после применения подстановки к некоторой паре переменных получаются равные термы, то равенство этих переменных выводится из системы. Ускорение достигается за счет сокращения перебора возможных отношений эквивалентности на множестве общих переменных. Такой подход описан, например, в [2], [7], [4]

В работе [6] Шостак рассматривает следующее языковое расширение базовой теории. Множество термов расширяется за счет введения новых "неинтерпретированных" функциональных символов дг, по существу, переменных второго порядка, причем термы вида gx(t) рассматриваются (анализируются канонизатором) как отдельные переменные первого порядка. Мы показываем, что можно распространить алгоритм канонизации на термы второго порядка с сохранением аналогов свойств канонизатора, что также дает аксиоматизацию указанного расширения (параграф 2 2).

Обобщение процедуры решения уравнений базовой теории на расширенную теорию является более сложной задачей. Основная трудность при решении системы уравнений в языке второго порядка состоит в необходимости обеспечить функциональную зависимость неизвестного значения gt(t) от значений t, которые также являются неизвестными. Это обстоятельство приводит к добавлению в систему условных равенств вида h = h =>■ 9i(ti) = 9%(h), в результате чего "первопорядковый" алгоритм решения уравнений становится неприменимым

Варианты алгоритма Шостака (например, [3], [1]) при верификации формул вида S —У а — Ъ реализуют процедуру конгруэнтного замыкания и фактически оперируют с S как с системой уравнений на неизвестные вида g(t) (рассматриваемые как отдельные переменные) В случае заведомо ложного равенства с = d мы имеем метод проверки совместности системы S. Этот подход проверяет выводимость хорновских предложений в комбинации одной теории Шостака с теориями без собственных нелогических аксиом. Когда одна из теорий, комбинируемых в методе Нельсона-Оппена, — теория Шостака, алгоритм решения уравнений может быть использован на последнем шаге метода Нельсона-Оппена в качестве эффективного теста, проверяющего достаточное условие принадлежности хорновских предложений комбинированной теории. Так, формула заведомо принадлежит комбинации теорий, если ее справедливость удается установить без использования части нелогических аксиом.

Но до настоящего времени не было известно ни описание множества решений систем, ни даже точное определение понятия решения, что делало практически невозможным доказательство полноты метода. Первоначальное доказательство Шостака [6] содержало существенные пробелы, обоснования в более поздних вариантах алгоритмов в [3], [4] также не являются удовлетворительными Попытка прояснения ситуации была также предпринята в [7], где метод Шостака изложен в виде системы вывода равенств. Однако, как указывают в [8] разработчики системы Simplify (HP

Labs, система доказательства теорем для проверки программ), им пришлось отказаться от метода Шостака, т.к. приведенных выше работ оказывается недостаточно для практического применения

Цель настоящей работы — развитие математической теории функциональных уравнений в теориях Шостака Предлагается точное определение понятия решения и дается явное описание множества решений системы уравнений. Также разработан метод построения решений.

Мы предлагаем задавать допустимые значения второпорядко-вых неизвестных дг с помощью бесконечных идемпотентных подстановок, оперирующих с термами вида д3 (t) как с переменными. Подстановка а называется функционально согласованной, если она удовлетворяет условию crt\ = аЦ => agt(ti) = ag^tz). Подстановка называется ж-согласованной, если адг(Г) стдг(7г£), где — отношение эквивалентности на термах, порожденное канонизатором

7г

Унификатором системы S = {аг = Ьг} называется такая идем-потентная функционально согласованная и 7г-согласованная подстановка р, для которой верно раг рЪг. Слабым наиболее общим унификатором (слабым ноу) системы S называется такой унификатор р, что для любого унификатора в найдется подстановка ту, что в -"^тт г\р

Основные результаты работы таковы

1) Предложен алгоритм, который для данной системы уравнений S в теории Шостака Тж с функциональными переменными дг распознает наличие унификатора, то есть разрешимость системы S в классе бесконечных согласованных подстановок (теорема 2 6 14)

2) Показано, что для унифицируемой системы существует слабый наиболее общий унификатор, допускающий конечное представление (теорема 2 6.14)

3) Предложен полиномиальный алгоритм вычисления для унифицируемых систем значения слабого наиболее общего унификатора на термах (определение 2 5.2, теорема 2 7 6).

4) Найдена модельная характеризация понятия унифицируемости в теориях Шостака Показано, что унифицируемость системы эквивалентна ее выполнимости в канонической модели второпо-рядковой теории Шостака (теорема 3 2 6)

5) Построен алгоритм, который для каждой унифицируемой системы S и терма t строит (t mod S) — каноническую форму терма t по модулю S. При этом синтаксическое равенство (a mod S) — (b mod S) оказывается эквивалентным истинности в канонической модели S —У а = Ъ, что дает еще один метод верификации утверждений такого вида (теорема 3.3.4).

Дальнейшее изложение придерживается следующего плана. Глава 1 носит вспомогательный характер и посвящена решениям систем уравнений в языке первого порядка. В параграфах 1.1 и 1 2 даются основные определения, вводится понятие канонизатора и канонической интерпретации для языка первого порядка. Параграф 1.3 посвящен спецификации алгоритма решения уравнений и его распространению на случай конечных систем. В нем доказывается, что существует единый (не зависящий от выбора теории Шостака) способ преобразования алгоритма решения одного уравнения в языке первого порядка в алгоритм решения конечных систем таких уравнений

Глава 2 посвящена системам уравнений на неизвестные вида gt(t}- В параграфе 2.1 приведены основные определения для языка второго порядка (язык обогащается переменными второго порядка дг). Также вводится понятие второпорядковой подстановки, и определяются различные виды согласованных второпорядковых подстановок. Параграф 2.2 посвящен обобщению понятия кано-низатора, т е. построению отображения (обобщенного канониза-тора) на термах языка второго порядка, обладающего свойствами, аналогичными свойствам канонизатора Показывается, что отношение эквивалентности, порожденное обобщенным канонизатором на множестве термов первого порядка, будет совпадать с отношением эквивалентности, порожденным (простым) канонизатором. Параграф 2.3 рассматривает язык первого порядка, построенный в расширенной сигнатуре, — добавляются функциональные символы дг Множество термов в этом языке совпадает с множеством термов в языке второго порядка с неизвестными второго порядка дг Показывается, что обобщенный канонизатор для термов второго порядка является (простым) канонизатором на множестве термов первого порядка в расширенной сигнатуре Параграф 2 4 демонстрирует сложности непосредственного обобщения алгоритма решения уравнений на случай второго порядка и вводит понятие решения (унификатора) для системы уравнений второго порядка. Параграф 2.5 вводит конструкцию продолжения ограниченно согласованных конечных подстановок до бесконечных согласованных В параграфе 2.6 приводится процедура, которая определяет унифицируемость заданной системы и для унифицируемой системы строит подстановку, допускающую продолжение до стабильного слабого наиболее общего унификатора этой системы. Более компактная конструкция бесконечной функционально согласованной подстановки, продолжающей заданную конечную, приводится в параграфе 2.7. Алгоритм унификации систем хорновских предложений предложен в параграфе 2 8.

Глава 3 посвящена модельным аспектам понятия унифицируемости. В параграфе 3.1 по данной системе уравнений в языке второго порядка строится формула в языке первого порядка, выполнимость которой в канонической модели теории Шостака эквивалентна унифицируемости исходной системы. Параграф 3.2 посвящен доказательству эквивалентности унифицируемости системы уравнений и ее выполнимости в канонической модели теории Шостака второго порядка Параграф 3 3 вводит операцию mod и показывает корректность применения этой операции для проверки хорновских выражений.

1. Ganzmger Н Shostak Light — Automated Deduction, CADE-18, volume 2392 of Lecture Notes in Computer Science, —332-346. — Springer, 2002.

2. Manna Z., Zarba С G Combining decision procedures. — Formal Methods at the Cross Roads: From Panacea to Foundational Support, Lecture Notes m Computer Science. — Springer, 2004.

3. Shankar N , Ruess H Deconstructing Shostak — Proceedings of the Sixteenth IEEE Symposium On Logic In Computer Science (LICS'01), IEEE Computer Society Press, — 2001. — 19-28.

4. Shankar N, Ruess H. Combining Shostak theories — International Conference Rewriting Techniques and Applications (RTA '02), volume 2378 of Lecture Notes m Computer Science, pages 1-18, Springer, 2002.

5. Shostak R. E. A practical decision procedure for arithmetic with function symbols. Journal of the Association for Computing Machinery, 26(2) 351-360, 1979

6. Shostak R. E Deciding combinations of theories — Association for Computing Machinery — 1984 — 31(1) — 1-12.

7. Barrett С W , Dill D L , Stump A A generalization of Shostak's method for combining decision procedures — FroCoS'02

8. Detlefs D , Nelson G., Saxe J.B. Simplify A Theorem Prover for Program Checking — Systems Research Center, HP Laboratories Palo Alto, HPL-2003-148, 2003 — http://wwwhpl.hp.com/techreports/2003/HPL-2003-148.html

9. Presburger. M. Uber die vollstandigkeit eines gewissen systems der arithmetik ganzer zahlen, m welchen die addition als emzige operation hervortritt — Comptes Rendus du Premier Congres des Mathematicienes des Pays Slaves, pages 92-101, 1929.

10. Tarski. A A Decision Method for Elementary Algebra and Geometry — University of California Press, 1951.

11. Oppen D C. Reasoning about recursively defined data structures Journal of the Association for Computing Machinery , 27(3).403-411, 1980.

12. Stump A., Barret C. W., Dill D. L., Levitt J A decision procedure for an extensional theory of arrays — Sixteenth Annual IEEE Symposium on Logic m Computer Science, pages 29-37 IEEE Computer Society, 2001.

13. Cantone D., Zarba С G. A new fast tableau-based decision procedure for an unquantified fragment of set theory — Automated Deduction m Classical and Non-Classical Logics, volume 1761 of Lecture Notes m Computer Science, pages 127-137 Springer, 2000.

14. Zarba C. G. Combining multisets with integers — Automated Deduction, — CADE-18, volume 2392 of Lecture Notes in Computer Science, pages 363-376 Springer, 2002.

15. Nelson G. Techniques for program verification — Technical Report CSL-81-10, Xerox Palo Alto Research Center, 1981

16. Nelson G. Combining satisfiability procedures by equality sharing — Automated Theorem Proving: After 25 Years, volume 29 of Contemporary Mathematics, pages 201-211 American Mathematical Society, 1984.

17. Nelson G , Oppen D. C. Simplification by cooperating decision procedures — ACM Transactions on Programming Languages and Systems, 1(2).245-257, 1979.

18. Oppen D. C. Complexity, convexity and combinations of theories — Theoretical Computer Science, 12-291-302, 1980.

19. Stump A , Barret С W , Dill D L CVC A cooperating validity checker — Computer Aided Verification, volume 2404 of Lecture Notes in Computer Science, pages 500-504, 2002

20. Detlefs D. L , Rustan K., Leino M., Nelson G., Saxe J. B. Extended static checking — Technical Report 159, Compaq System Research Center, 1998.

21. Craigen D , Kromodimoeljo S., Meisels I , Pase В., Saaltink M. EVES. An overview — Formal Software Development Methods, volume 552 of Lecture Notes m Computer Science, pages 389-405. Springer, 1991.

22. Levy В., Filippenko I., Marcus L , Menas T. Using the state delta verification system (SDVS) for hardware verification — Theorem Prover in Circuit Design: Theory, Practice and Experience, pages 337-360. Elsevier Science, 1992.

23. Luckham D С , German S M , von Henke F. W., Karp R. A., Milne P W , Oppen D. C., Polak W , Scherlis W. L. Stanford pascal verifier user manual — Technical Report STAN-CS-79-731, Stanford University, 1979

24. Baader F , Schulz K. U Combining constraint solving — Constraints in Computational Logics, volume 2002 of Lecture Notes in Computer Science, pages 104-158, 2001

25. Ringeissen С Cooperation of decision procedures for the satis-ability problem — Frontiers of Combining Systems, volume 3 of Applied Logic Series, pages 121-140. Kluwer Academic Publishers, 1996.

26. Tinelli C., Harandi M T A new correctness proof of the Nelson-Oppen combination procedure — Frontiers of Combining Systems, volume 3 of Applied Logic Series, pages 103-120. Kluwer Academic Publishers, 1996.

27. Filliatre J.-C , Owre S , Ruess H., Shankar N. ICS: Integrated Can-onizer and Solver — Computer Aided Verification, volume 2102 of Lecture Notes m Computer Science, pages 246-249, 2001.

28. Owre S., Raj an S., Rushby J M , Shankar N , Snvas M. K. PVS-Combining specification, proof checking and model checking — Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 411-414. Springer, 1996

29. Barrett C. W , Dill D. L., Levitt J. L. Validity checking for combinations of theories with equality — Formal Methods in Computer-Aided Design, volume 1166 of Lecture Notes m Computer Science, pages 187-201, 1996.

30. Bj0rner N S , Browne A , Colon M., Fmkbemer В., Manna Z., Sipma H. В., Uribe Т. E Verifying temporal properties of reactive systems- A STeP tutorial — Formal Methods m System Design, 16(3).227-270, 2000.

31. Krstic S., Conchon S. Canonization for disjoint unions of theories. Proceedings of the 19th International Conference on Automated Deduction, LNAI. Springer-Verlag, 2003.Работы автора по теме диссертации

32. С. П. Шлепаков. О решениях систем уравнений в первопо-рядковых теориях Шостака // Вестник московского университета, серия 1. математика, механика. 2005. №3, 55-57.

33. С. П. Шлепаков. Задачи унификации и функциональные уравнения в свободных алгебрах // Труды XXIV Конференции молодых ученых механико-математического факультета МГУ им. М.В.Ломоносова, 2002, 196-198.

34. С П. Шлепаков. О решениях функциональных уравнений в теориях Шостака // Труды XXVI Конференции молодых ученых механико-математического факультета МГУ им. М.В Ломоносова, 2004, 250-253.

35. С П. Шлепаков. Второпорядковая унификация в теориях Шостака // Деп. в ВИНИТИ; №1767-В2004; М. ВИНИТИ, 2004, 39 с.