О решениях функциональных уравнений в некоторых разрешимых теориях

Развитие систем проверки правильности программ и доказательств (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 systemsA 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 с.