Содержание к диссертации
Введение
1 Решение систем уравнений в языке первого порядка 12
1.1 Язык первого порядка 12
1.2 Канонизатор 13
1.3 Алгоритм решения уравнений 17
2 Решение систем уравнений в языке второго порядка 25
2.1 Язык второго порядка 25
2.2 Канонизатор для языка второго порядка 29
2.3 Канонизатор для языка первого порядка в расширенной сигнатуре 34
2.4 Решения уравнений с функциональными переменными 38
2.5 Построение согласованных подстановок 43
2.6 Алгоритм унификации 48
2.7 Вычисление а 57
2.8 Условная унификация 64
3 Выполнимость и унифицируемость 68
3.1 Модели первого порядка 68
3.2 Модели второго порядка 70
3.3 Операция mod
Введение к работе
Развитие систем проверки правильности программ и доказательств (program verification, proof checking) потребовало создания эффективных разрешающих процедур (decision procedures) для различных подтеорий, а также для их комбинации Под разрешающей процедурой здесь понимается алгоритм, который для любой формулы из некоторого фиксированного класса определяет ее выполнимость в данной теории, причем он всегда останавливается с положительным или отрицательным ответом. Разрешающие процедуры улучшают эффективность системы верификации и освобождают пользователя от многих однообразных и утомительных действий Разрешающие процедуры существуют для многих практически используемых теорий — для линейной арифметики над кольцом целых [9] и рациональных чисел [10], для теорий структур данных, которые часто используются в программах — для списков [11], массивов [12], множеств [13], мультимножеств [14].
Комбинация теорий — это множество формул в объединенной сигнатуре, являющееся дедуктивным замыканием их объединения. Методы разрешения некоторых видов формул в комбинации теорий были предложены, например, в [15], [16], [17], [18], [5], [6], [1], И, И, [4], [7]
Пусть Тг, г Є / — конечное множество теорий с равенством, сигнатуры Пг которых попарно не пересекаются Нельсон и Оппен [17] предложили общий метод разрешения бескванторных формул в комбинации теорий Т% Для применения этого метода необходимо, чтобы каждая теория была стабильно бесконечной Последнее требование означает, что для каждой бескванторной формулы, выполнимой в некоторой модели теории, существует бесконечная модель, в которой она выполнима
На первом шаге проблема выполнимости бескванторных формул общего вида с помощью приведения к ДНФ сводится к ее частному случаю для формул F, являющихся конъюнкцией атомарных формул и их отрицаний, выполнимость исходной формулы эквивалентна выполнимости хотя бы одной из элементарных конъюнкций, составляющих ДНФ
Следующий шаг — абстракция — за счет введения новых переменных преобразует формулу F в конъюнкцию формул AlFl так, что каждый член конъюнкции составлен из символов сигнатуры только одной теории, и каждой теории соответствует только одна формула Fu причем выполнимость F эквивалентна выполнимости AIFI Для этого каждое вхождение терма вида f(t), где / Є Q3, в атомарную формулу P(s) для заменяется на новую переменную ж, и к формуле F добавляется новый конъюнктивный член
Последний шаг — проверка — рассматривает множество "общих переменных" W, т.е переменных, которые встречаются в более чем одной формуле конъюнкции Л і . Для каждого отношения эквивалентности Е на множестве W рассматривается формула -) — конъюнкция равенств и неравенств всех возможных пар переменных из W, причем если хЕу, то 1 содержит х = у, а если (хЕу)ь то FE содержит х ф у Формула F выполнима в некоторой модели комбинации теорий Тг тогда и только тогда, когда найдется такое отношение эквивалентности Е, которое было бы совместно с каждой формулой Рг Это означает, что для каждого г формула Ег Л FE выполнима в теории Тг
Основная трудность построения быстро работающей разрешающей процедуры методом Нельсона-Оппена заключается в реализации последнего шага, т.е. в выборе эффективной стратегии поиска соответствующего отношения эквивалентности Е. Прин ципиаяьным становится выявление специальных теорий, которые позволяют эффективно распознавать выводимость равенств или неравенств переменных из заданного набора атомарных формул и их отрицаний.
Таким образом, метод Нельсона-Оппена — скорее подход к решению задачи, нежели законченное описание процедуры Он используется в таких системах, как CVC [19], ESC [20], EVES [21], SDVS [22], SPV (Stanford Pascal Verifier) [23], Simplify [8] Детальное описание и строгий анализ метода можно найти в [24], [25], [26].
Шостак [6] предложил ограничиться теориями специального вида. Единственным допустимым предикатом является равенство, а сама теория должна описываться с помощью двух алгоритмов: алгоритма приведения к нормальной форме и алгоритма решения уравнений. Класс разрешаемых методом Шостака формул — хор-новские предложения, т.е. формулы вида S — с = d, где S — система уравнений, понимаемая как конъюнкция равенств, а с, d — термы. Метод Шостака применяется в таких системах верификации, как ICS [27], PVS [28], SVC [29], STeP (Stanford Temporal Prover) [ЗО].
Алгоритм приведения термов к нормальной форме (канониза-тор) по данному терму выбирает в классе равных термов канонического представителя При этом накладывается ряд условий на поведение этого алгоритма (определение 1.2.1). В частности, алгоритм приведения к нормальной форме 7г определяет теорию Тъ, в которой он задан- эта теория аксиоматизируется множеством всех равенств вида t — rrt, где t — терм
Алгоритм решения уравнений — это процедура, которая определяет выполнимость равенства в теории. Для выполнимого равенства, рассматриваемого как уравнение на индивидные переменные,
процедура строит решение в виде эквивалентной ему идемпотент-ной подстановки Допускаются также параметрические решения, поэтому подстановка может содержать переменные, которых изначально не было в системе. С помощью метода исключения переменных алгоритм решения уравнений может быть использован для решения конечных систем уравнений (параграф 1 3)
Теории, обладающие алгоритмами приведения к нормальной форме и решения уравнений, называются теориями Шостака. Такими теориями будут, например, линейная арифметика над кольцом целых и рациональных чисел, выпуклая (без nil) теория списков, теория массивов, теория диаграмм Венна ([6], [2])
Шостак полагал, что его метод распознает принадлежность бескванторной хорновской формулы S — а = Ъ комбинации теорий, для каждой из которых заданы канонизатор и алгоритм решения уравнений Он предложил конструкцию объединения нескольких канонизаторов и алгоритмов решения уравнений для разных теорий в единые канонизатор и алгоритм решения уравнений для комбинации теорий С помощью этих средств предполагалось решать S как систему уравнений и подставлять найденные решения в обе части равенства а Ь. Если в результате подстановки обе части равенства оказались идентичными, то исходная формула принадлежит комбинации теорий, в противном случае — нет
На самом деле выяснилось ([4]), что предложенный алгоритм решения уравнений в комбинации теории в некоторых случаях приводит к не идемпотентным подстановкам, т е не является корректным в смысле определения алгоритма решения уравнений. Более того, как показано в [31], комбинация любых двух нетривиальных теорий Шостака не может иметь корректный в смысле определения алгоритм решения уравнений Поэтому в настоящее время единственной общей разрешающей процедурой для комбинации теорий остается процедура Нельсона-Оппена.
На самом деле алгоритм решения уравнений для теории Шостака допускает использование на последнем шаге процедуры Нельсона-Оппена, поскольку позволяет эффективно рассуждать о равенствах переменных Так, один вызов разрешающей процедуры в методе Нельсона-Оппена может установить равенство (неравенство) одной пары переменных. Алгоритм решения уравнений Шостака за один вызов возвращает идемпотентную подстановку, которая позволяет судить о всех вытекающих равенствах, если после применения подстановки к некоторой паре переменных получаются равные термы, то равенство этих переменных выводится из системы. Ускорение достигается за счет сокращения перебора возможных отношений эквивалентности на множестве общих переменных. Такой подход описан, например, в [2], [7], [4]
В работе [6] Шостак рассматривает следующее языковое расширение базовой теории. Множество термов расширяется за счет введения новых "неинтерпретированных" функциональных символов д1} по существу, переменных второго порядка, причем термы вида дг(ї) рассматриваются (анализируются канонизатором) как отдельные переменные первого порядка. Мы показываем, что можно распространить алгоритм канонизации на термы второго порядка с сохранением аналогов свойств канонизатора, что также дает аксиоматизацию указанного расширения (параграф 2 2).
Обобщение процедуры решения уравнений базовой теории на расширенную теорию является более сложной задачей. Основная трудность при решении системы уравнений в языке второго порядка состоит в необходимости обеспечить функциональную зависимость неизвестного значения дг(ї) от значений t, которые также являются неизвестными. Это обстоятельство приводит к добавле нию в систему условных равенств вида
h = = 9i{ti) = дг( г),
в результате чего "первопорядковый" алгоритм решения уравнений становится неприменимым
Варианты алгоритма Шостака (например, [3], [1]) при верификации формул вида S — а = 6 реализуют процедуру конгруэнтного замыкания и фактически оперируют с S как с системой уравнений на неизвестные вида g{t) (рассматриваемые как отдельные переменные) В случае заведомо ложного равенства с = d мы имеем метод проверки совместности системы S. Этот подход проверяет выводимость хорновских предложений в комбинации одной теории Шостака с теориями без собственных нелогических аксиом. Когда одна из теорий, комбинируемых в методе Нельсона—Оппєна, — теория Шостака, алгоритм решения уравнений может быть использован на последнем шаге метода Нельсона-Оппена в качестве эффективного теста, проверяющего достаточное условие принадлежности хорновских предложений комбинированной теории. Так, формула заведомо принадлежит комбинации теорий, если ее справедливость удается установить без использования части нелогических аксиом.
Но до настоящего времени не было известно ни описание множества решений систем, ни даже точное определение понятия решения, что делало практически невозможным доказательство полноты метода. Первоначальное доказательство Шостака [6] содержало существенные пробелы, обоснования в более поздних вариантах алгоритмов в [3], [4] также не являются удовлетворительными Попытка прояснения ситуации была также предпринята в [7], где метод Шостака изложен в виде системы вывода равенств. Однако, как указывают в [8] разработчики системы Simplify (HP Labs, система доказательства теорем для проверки программ), им пришлось отказаться от метода Шостака, т.к. приведенных выше работ оказывается недостаточно для практического применения
Цель настоящей работы — развитие математической теории функциональных уравнений в теориях Шостака Предлагается точное определение понятия решения и дается явное описание множества решении системы уравнений. Также разработан метод построения решений.
Мы предлагаем задавать допустимые значения второпорядко-вых неизвестных д.ь с помощью бесконечных идемпотентных подстановок, оперирующих с термами вида g3(t) как с переменными. Подстановка а называется функционально согласованной, если она удовлетворяет условию сгЬ\ = 7 = о дг(їі) — .() Подстановка называется 7г-согласованной, если адг(ї) ag Trt), где v — отношение эквивалентности на термах, порожденное канонизатором
Унификатором системы 3 = {аг = Ьг} называется такая идем-потентная функционально согласованная и 7г-согласованная подстановка р, для которой верно раг п рЬг, Слабым наиболее общим унификатором (слабым ноу) системы S называется такой унификатор р, что для любого унификатора в найдется подстановка ту, что 9 ж г)р
Основные результаты работы таковы
1) Предложен алгоритм, который для данной системы уравнений S в теории Шостака Тж с функциональными переменными дг распознает наличие унификатора, то есть разрешимость системы S в классе бесконечных согласованных подстановок (теорема 2 6 14)
2) Показано, что для унифицируемой системы существует слабый наиболее общий унификатор, допускающий конечное предста влєние (теорема 2 6.14)
3) Предложен полиномиальный алгоритм вычисления для унифицируемых систем значения слабого наиболее общего унификатора на термах (определение 2 5.2, теорема 2 7 6).
4) Найдена модельная характеризация понятия унифицируемости в теориях Шостака Показано, что унифицируемость системы эквивалентна ее выполнимости в канонической модели второпо-рядковой теории Шостака (теорема 3 2 6)
5) Построен алгоритм, который для каждой унифицируемой системы S и терма і строит (t mod 8) -— каноническую форму терма і по модулю S. При этом синтаксическое равенство (a mod S) = ( mod S) оказывается эквивалентным истинности в канонической модели S —? а = Ъ, что дает еще один метод верификации утверждений такого вида (теорема 3.3.4).
Дальнейшее изложение придерживается следующего плана. Глава 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 и показывает корректность применения этой операции для проверки хорновских выражений.
Канонизатор
Унификатором системы 3 = {аг = Ьг} называется такая идем-потентная функционально согласованная и 7г-согласованная подстановка р, для которой верно раг п рЬг, Слабым наиболее общим унификатором (слабым ноу) системы S называется такой унификатор р, что для любого унификатора в найдется подстановка ту, что 9 ж г)р
Основные результаты работы таковы
1) Предложен алгоритм, который для данной системы уравнений S в теории Шостака Тж с функциональными переменными дг распознает наличие унификатора, то есть разрешимость системы S в классе бесконечных согласованных подстановок (теорема 2 6 14)
2) Показано, что для унифицируемой системы существует слабый наиболее общий унификатор, допускающий конечное предста влєние (теорема 2 6.14)
3) Предложен полиномиальный алгоритм вычисления для унифицируемых систем значения слабого наиболее общего унификатора на термах (определение 2 5.2, теорема 2 7 6).
4) Найдена модельная характеризация понятия унифицируемости в теориях Шостака Показано, что унифицируемость системы эквивалентна ее выполнимости в канонической модели второпо-рядковой теории Шостака (теорема 3 2 6)
5) Построен алгоритм, который для каждой унифицируемой системы S и терма і строит (t mod 8) -— каноническую форму терма і по модулю S. При этом синтаксическое равенство (a mod S) = ( mod S) оказывается эквивалентным истинности в канонической модели S —? а = Ъ, что дает еще один метод верификации утверждений такого вида (теорема 3.3.4).
Дальнейшее изложение придерживается следующего плана. Глава 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 и показывает корректность применения этой операции для проверки хорновских выражений.
Алгоритм решения уравнений
В этом параграфе мы опишем алгоритм решения уравнений и распространим его на случай конечных систем уравнений.
Пусть є [%/хъ] — (конечная) подстановка. Ей соответствует формула /\Хгват(е){хг = А) которую условимся обозначать тем же символом є Конечную систему равенств 3 = { аг = Ьъ} будем представлять аналогично - формулой 5 = Дг(аг = 6г) Для каждого конечного множества переменных W и формулы (р обозначим через (3W) р формулу (Зх) р, получающуюся из р замыканием кванторами существования по всем переменным из W Пусть также (3) (р = (3W) (р, где W — множество всех свободных переменных формулы (р. Аналогично определим (yw)(p и (V)(/?.
Определение 1.3.1 Пусть задан канонизатор ТГ. Мы будем говорить, что задан алгоритм решения уравнений, если задана следующая вычислимая функция solve, принимающая в качестве аргументов бесконечное разрешимое множество переменных U ж уравнение a — Ь в языке первого порядка, причем f/П Var(a = 6) = 0. Множество U передается на вход solve своим разрешающим алгоритмом Функция solve возвращает значение _L, если Тп \/ (3) (а — Ь), в противном случае значение равно такой конечной идемпотентной подстановке є7 что Dom(e) С Var(a — 6); W = Var(e) \ Var(a = b)CU} Tv Ь (3 ) є н- а = Ь
Пример. Для языка линейной арифметики алгоритм решения уравнений можно задать так. Пусть дано уравнение а = Ъ. Рассмотрим эквивалентное уравнение -к[а — Ъ) = 0 Если его левая часть есть константа г, то возвращаем id, при г = 0и1 при г ф 0. В оставшемся случае слева есть хотя бы одна переменная. Пусть ж, — переменная из левой части с минимальным индексом. Перенесем все остальное в правую часть и домножим обе части на рациональный множитель так, чтобы слева коэффициент при хг стал единицей Получим эквивалентное уравнение вида хг = , где переменная х% не входит в терм t Положим solve(U, a = b) = [і/хг]. Поскольку solve не вводит новых неизвестных, то результат не зависит от первого аргумента.
Например, solve(U, Ахі — 2ж5 + 5 = 2х1+3х±) = [ (ж4 + ж5-)/жі] Пример. Действие алгоритма решения уравнений для теории пар можно продемонстрировать на примере Рассмотрим бесконечное разрешимое множество переменных U и уравнение hd(x) = tl(y), причем ж, у :1/. Пусть и Є U Поскольку Тж Ь hd{x) = tl(y) + (Би х = cons(tl(у), и)), то solve(U,hd(x) = ti{y)) — [cons(tl(y),u)/x] Заметим, что эквивалентной исходному уравнению идемпотентной подстановки є с условием Var(e) С {х, у} не существует
Определение 1.3.2 Пусть U — некоторое бесконечное разрешимое множество переменных, S = {at = Ьг} — конечная система уравнений, Var(S) П U — 0 Мы будем называть подстановку е решением системы S в присутствии U, если 1 б — конечная идемпотентная подстановка, 2 Dom(e) QVar{S), 3 W = Var(e) \ Var(S) С [/, 4. 7; h (3W) є + 5 Отметим, что при Var(S) П W = 0 условие Тж Ь (3№)е — 5 эквивалентно 7 h є —У S Лемма 1.3.3 Пусть задан канонизатор п. Тогда длл любой конечной системы равенств S — {аг = Ьг} и конечной идемпотент-ной подстановки е имеет место: Т \т (є — S) еаъ Ъг. (В частности, еа% еЬ% длл каждого решения є системы S.) Доказательство. Условие (Vic)(є — аг = Ьг) равносильно (Ух)(еаг = еЬг). Отсюда Тп Ь (є — аг = Ьг) =$ Tw Ь еаъ = еЬг Ф еаг "тг еЬ( по лемме 1.2.4 ш Алгоритм решения уравнений строит решения систем, состоящих из одного уравнения Следующая конструкция позволяет распространить алгоритм solve на случай нескольких уравнений. Пусть є — решение системы уравнений S в присутствии бесконечного разрешимого множества переменных U Пусть также Єї — решение уравнения {ее — ed} в присутствии U \ Var(e). Положим е = (ei)\Yarw\u Лемма 1.3.4 Подстановка е1 является решением системы, S U {с = d} в присутствии U.
Канонизатор для языка второго порядка
В этом параграфе мы обобщим понятие канонизатор а, т е построим отображение (обобщенный канонизатор) на термах языка второго порядка, обладающего свойствами, аналогичными свойствам канонизатора. Мы показываем, что отношение эквивалентности, порожденное обобщенным канонизатором на множестве термов первого порядка, будет совпадать с отношением эквивалентности, порожденным (простым) канонизатором.
Пусть на множестве термов первого порядка задан канонизатор 7Г. Фиксируем некоторое вычислимое биективное отображение z (- vz, сопоставляющие неизвестным z Є Var первопорядковые переменные vz Є Var Пусть A TmP -і- Tm — подстановка, порожденная этим отображением Она обратима.
Определим отображение и : Тш - Тт№ рекурсией л о второ-порядковой VDit) глубине терма. Для термов t Є Тт№ положим yd — А-17гА. Пусть жЬ для і Є Тт 2\ VD{i) ъ уже определено Возьмем терм і Є ТтУ\ VD(t) — г + 1. Рассмотрим подстановку /іг+і, которая заменяет неизвестные g(ti) глубины, не превосходя щей і + 1, на g{xti) /І,+І - { g( ti)/g{ti) I 9(h) Є Var 2\ VD[g(h)) + 1 }, (действие и на t\ определено ранее). Положим xt = А- ттХ(лг+іі. Полученное таким образом отображение и мы будем называть обобщенным канонизатором Легко видеть, что yd = \-\Xtit, где ц = { sr(xti)/g(ti) g(t{) Є Уаг(2) }
Замечание 2.2.1 Обобщенный канонизатор х порождает отно-піение эквивалентности „ на термах из Тт 2\ Ограничение этого отношения на Тт совпадает с (см лемму 2 2 2). В то же время ж может и не оказаться продолжением 7г Чтобы обеспечить это свойство, достаточно выбрать отображение А на коммутирующим с 7Г Так, для линейной арифметики можно выбрать А, сохраняющее упорядочение переменных Var \ например, А = [х2г/хг \ г Є Щ U [х2х\9к(Щ+і/gkfy], где \t] — произвольная биективная нумерация термов.
Лемма 2.2.2 Пусть і\,і і Є Тт \ Тогда t± Тt i О ti иt%. Доказательство. Так как ограничение подстановки А на мно жество Trrv-1 есть обратимая подстановка, то, по свойству 3 ка нонизатора, i „2 Ф Xi\ Xi Последнее равносильно irXti — irXt2 О X wXti = Х 1жХі2 44 ti „t2 Лемма 2.2.3 1) Для любого терма t Є ТтУ имеет место Уаг(Х-г7тХі) С Var{t). 2) Обобщенный канонизатор не увеличивает второпорядковую глубину терма, т.е. VD{?ct) VD[t). Доказательство. 1) По свойству 3 канонизатора Var (тгХЬ) С Var{Xt), откуда Var nXt) С Far(A_1Ai) = Kar(t) 2) Индукция по второпорядковои глубине терма. База индук ции. Для t Є iW1) утверждение тривиально. Шаг индукции. Для t Є Тпг№\ VD(t) = г + 1 множество Var(ju) состоит из неизвест ных глубины не больпіе г + 1 по предположению индукции. В силу 1) получаем Var{ d) — Var(X 17rXfj,t) С Var{jii) и Теорема 2.2.4 Пусть 7г — канонизатор. Для соответствующего обобщенного канонизатора ж выполняются свойства, аналогичные свойствам 1-5 канонизатора: 1. жх = х, где х Є Var -\ 2. Varmint) С Var (i), где Var (t) = Var(t) П Var \ 3. a о7 ж для любой х-согласованной подстановки и Тт 2 —Y Тт, 4- Если жі = /(ii, .. ,tn), то жЬг = i%) Эта теорема вытекает из лемм, приводимых ниже. Лемма 2.2.5 1) Для любого терма і Є Ттп№ имеет место жЬ = \іжі. 2) Обобщенный канонизатор ж — идемпотентное, простое функционально согласованное отображение.
Доказательство. Покажем жЬ = \ixt, а также идемпотентность ж индукцией по второпорядковои глубине терма. База индукции. Для t Є Тт в силу пункта 1) леммы 2 2 3 имеем Var(xt) = Var(X litXi) С Var{t) С Var Поскольку fix = ж для х є Var \ имеем {мжі = жЬ Кроме того, жН = (А 17гЛ)2і = A 1?r2At = жЬ.
Модели второго порядка
Пусть теперь кроме обобщенного канонизатора н задана функция solve, которая решает системы уравнений, составленные из термов первого порядка (в смысле параграфа 1 3) Мы хотим распространить этот метод решения на системы уравнений, составленные из термов второго порядка.
Самый простой способ — применить подстановку А к левым и правым частям уравнений и полученную систему подать на вход первопорядкового solve, затем решение преобразовать обратно с помощью А 1. А именно, пусть S — { а% — Ъг } — система уравнений, U — бесконечное разрешимое множество переменных с условием U Л Var(S) — 0 и U = XU После применения А в системе S — { Хаг = ХЬЪ } не остается второпорядковых неизвестных. Решим систему; пусть solve(U , 3і) = [г/ л] После возвращения к исходным неизвестным получится подстановка а = А_1[ / г]А = [X Hl/X 1vl]i действующая на термах второго порядка. Будем обозначать ее так же, solve(U,S) Исследуем свойства полученной подстановки. Лемма 2.4.1 Пусть S = {аг — Ьг} — система уравнений, U — бесконечное разрешимое мноокество переменных с условием U П Var{S) = 0. Обозначим V Var \U, а = solve(U, S). Тогда 1) aat хО-Ъг; 2) а — идемпотентная подстановка; 3) для любой -согласованной и идемпотентной подстановки в, для которой ваъг :вЪ11 найдется подстановка п, для которой Доказательство. Имеем a = X lsolve(XU, XS)X. Обозначим a = solve(XU, XS), fjf = А/ІА-1 — первопорядковые подстановки. 1) По теореме 1 3.6 имеет место о Хаг - v о ХЬг Имеет место цепочка следствий & Хаъ п а ХЬг = Хааг х ХаЬг = р/Хо аг fj,1\аЪг лемма 1.2 5 для р! =Ф Х{лааг ж Хр,о Ьг = 7гАрсгаг = 7гХ{іаЬг = Х 1жХііаа1 = А 17гАдсг6г = ааг х аЬъ. 2) Подстановка а1 идемпотентна, поскольку является решением системы XS в присутствии XU (теорема 1.3.6). Имеем цепочку равенств о-о- = A-VAA-VA = A4aVA - A" VA = а. 3) Можно ограничиться рассмотрением только таких подстано вок 0, для которых KQV = 9v. Действительно, возьмем подстановку 0\ = {хв) В силу леммы 2 19 выполняется в\ В. Отсюда сле дует, что В\ — -согласованная подстановка и что выполняется #1 с 0\Ъ%. По лемме 2.2.9 подстановка д\ — идемпотентная. Если найдется подстановка г\ с условием В\ VK тусг, то и 9 У. т]а. Таким образом, можно считать, что для подстановки 9 = [s /v,,] выполняется жЭг = зг. Отсюда для любой неизвестной v, используя 1) леммы 2.2.5, получим fi9v = \і сву — H9V = 9v, что означает равенство подстановок /10 = в. (6) Из биективности Л будет следовать равенство подстановок в — Х 1[Хзг/Хьг]Х. Обозначим в = [Asj/AuJ — первопорядковую подстановку. Имеем цепочку следствий. жва% = ж9Ь% =Ф- X 1ivXfi9ai. = Х 1укХ 9Ьг =Ф А_17гА0аг = Х 1ттХ9Ьг по (6) = жХ9аг = ттХ9Ьг = тг9 Хаг = ттв ХЬ, = e Xat e Xbt. Поскольку а — решение XS в присутствии XU, а & — идемпо-тентна (проверяется непосредственно), из леммы 1.3 6 вытекает, что найдется подстановка rj, для которой 9 "Цо , откуда, в силу XV С VarW \ XU, имеем 9 rfa Поскольку // — первопорядковая подстановка, для v Є Varv имеем цепочку следствий 9 Xv jr rfa Xv =$f/9 Xv ж n rj a Xv по лемме 12 5 для // = jJX9v к [j/rfXav =$ Xfj,9v г к {Л ХГ)СГУ для rj = А-Іт/А = Xjidv n Xiirjav =4 irX(i9v — TrXjjrjav = X 1TTXJJ9V = X -KXji-qav =Ф- 9v f x T} JV. Тем самым установлено, что 9 г/а РОССИЙСКАЯ ГОСУДАРСТВЕН ! Ай БИБЛИОТЕКА В то же время, этот метод решения не учитывает функциональную природу переменных д, т е для функциональной переменной д значение а на неизвестных g(t) никак не связано со значением at Например, для линейной арифметики метод может возвратить подстановку а — [1/д(х), 2/х, 3/д(2)], для которой нарушается свойство функциональной согласованности отображения жа ах хОІ, но тд(х) 3 ад(2) Более того, результат работы такого solve — конечные подстановки, а каждая не тождественная функционально согласованная подстановка обязательно бесконечна Имеются алгоритмы, основанные на процедуре конгруэнтного замыкания ([6], [3]), которые позволяют проверять утверждения вида г Но они не предлагают конструкции построения функционально согласованных решений и не описывают структуру множества всех таких решений системы.
Мы предлагаем метод построения функционально согласованного решения (унификатора) для систем с функциональными переменными и показываем, что полученный унификатор оказывается наиболее общим.
Определение 2.4.2 Пусть даны конечная система уравнений S = { аъ = Ъг }, термы аг,Ьг Є Тт№ и обобщенный канонизатор ж Унификатором этой системы называется такая идемпотентная функционально согласованная и х-согласованная подстановка р, для которой верно раг г я рЬг
