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

• Автор: Шлепаков, Сергей Петрович
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2005
• Место защиты: Москва
• Количество страниц: 86 с.

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 Операция той

0.1 Введение
Развитие систем проверки правильности программ и доказательств (program verification, proof checking) потребовало создания эффективных разрешающих процедур (decision procedures) для различных подтеорий, а также для их комбинации Под разрешающей процедурой здесь понимается алгоритм, который для любой формулы из некоторого фиксированного класса определяет ее выполнимость в данной теории, причем он всегда останавливается с положительным или отрицательным ответом. Разрешающие процедуры улучшают эффективность системы верификации и освобождают пользователя от многих однообразных и утомительных действий Разрешающие процедуры существуют для многих практически используемых теорий — для линейной арифметики над кольцом целых [9] и рациональных чисел [10], для теорий структур данных, которые часто используются в программах — для списков [11], массивов [12], множеств [13], мультимножеств [14].
Комбинация теорий — это множество формул в объединенной сигнатуре, являющееся дедуктивным замыканием их объединения. Методы разрешения некоторых видов формул в комбинации теорий были предложены, например, в [15], [16], [17], [18], [5], [6], [1], И, [3], [4], [7]
Пусть Тг, г G I — конечное множество теорий с равенством, сигнатуры которых попарно не пересекаются Нельсон и Оппен [17] предложили общий метод разрешения бескванторных формул в комбинации теорий Г, Для применения этого метода необходимо, чтобы каждая теория была стабильно бесконечной Последнее требование означает, что для каждой бескванторной формулы, выполнимой в некоторой модели теории, существует бесконечная модель, в которой она выполнима

На первом шаге проблема выполнимости бескванторных формул общего вида с помощью приведения к ДНФ сводится к ее частному случаю для формул Н, являющихся конъюнкцией атомарных формул и их отрицаний, выполнимость исходной формулы эквивалентна выполнимости хотя бы одной из элементарных конъюнкций, составляющих ДНФ
Следующий шаг — абстракция — за счет введения новых переменных преобразует формулу Е в конъюнкцию формул АгРг так, что каждый член конъюнкции составлен из символов сигнатуры только одной теории, и каждой теории соответствует только одна формула Рг, причем выполнимость Р эквивалентна выполнимости АЛ Для этого каждое вхождение терма вида f(F), где / £ Ц, в атомарную формулу Р(з) для Р ^ 0,3 заменяется на новую переменную ж, и к формуле Р добавляется новый конъюнктивный член х
Последний шаг — проверка — рассматривает множество ’’общих переменных” IV, т.е переменных, которые встречаются в более чем одной формуле конъюнкции АгРг. Для каждого отношения эквивалентности Е на множестве IV рассматривается формула Ре, — конъюнкция равенств и неравенств всех возможных пар переменных из 1¥, причем если хЕу, то Ее содержит х = у, а если -|(хЕу), то Де содержит х ф у Формула выполнима в некоторой модели комбинации теорий Тг тогда и только тогда, когда найдется такое отношение эквивалентности Е, которое было бы совместно с каждой формулой Ег Это означает, что для каждого г формула Ег А Ее выполнима в теории Тг
Основная трудность построения быстро работающей разрешающей процедуры методом Нельсона-Оппена заключается в реализации последнего шага, т.е. в выборе эффективной стратегии поиска соответствующего отношения эквивалентности Е. Прин-

1 Пусть S = {аг = 6j} Положим г = 0, Sq = xS — {ха,
2. Если solve(U,St) = -L, останавливаемся с результатом _L Иначе положим аг — solve(U, S,j
3. Если найдутся такие неизвестные <7Дй), <7*(й) € AVar(So), что й й, но <7,0* (й) °i9k(h), то полагаем Sl+i = 5ги{^(й) = 9k{h)}, г = г + 1 и переходим к шагу 2 Если такой пары не существует, переходим к шагу 4.
4 Пусть <т, = [£,/г>*] Останавливаемся с результатом а = [х£4/Ч]
Следующие леммы посвящены доказательству некоторых свойств процедуры umfyQ. Зафиксируем некоторую систему уравнений S = {а, = Ьг}, такое бесконечное разрешимое множество переменных U, что AVar(S) П U — 0, обозначим а = unify(U, S), V = Var^ U Пусть N — последнее значение, которое принимает г в процессе выполнения процедуры. В случае umfy(U, S) ф _L зафиксируем параметр W = AVar(xS)UVar^(a) и обозначим через <7 продолжение а по множеству W (определение 2.5.2).
Лемма 2.6.1 Процедура umfy(U, S) закончит свою работу.
Доказательство. Количество шагов процедуры ограничено количеством различных пар неизвестных дДй), <7&(й) в множестве AVar(S0) т
Лемма 2.6.2 Для всех подстановок аг и систем 5,
1) имеют место включения Var (сгг) С Var(St)l)U С AVar(xS)U
2) любая неизвестная v Е AVar(8t) имеет канонический вид, т е. ни = и,
3) любая неизвестная из AVar[cг,) имеет канонический вид Кроме того,
4) Vаг(а) С AVar(xS) U U.