Алгоритм унификации термов с использованием стека

Теории первого порядка

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

Теории первого порядка возникли с целью формализации и строгого обоснования математики. В 1901 году Дедекинд предложил первое обоснование арифметики, известное теперь под названием системы аксиом Пеано. В 1908 году Цермело сформулировал аксиомы теории множеств. Так было установлено, что множество натуральных чисел и класс всех множеств тоже являются моделями теорий первого порядка. Это стимулировало развитие теории моделей, основные теоремы которой были доказаны Лёвенгеймом (1915 г.), Скулемом (1920 г.), Гёделем (1930 г.), Мальцевым (1936 г.).

Главное внимание в данной главе будет уделено доказательствам теоремы Мальцева о компактности, теорем Гёделя о непротиворечивости исчисления предикатов и о полноте теории первого порядка. Отметим теоремы Лёвенгейма-Скулема, из которых следует существование счётной модели теории множеств и несчётной модели теории натуральных чисел. Рассмотрим метод резолюций Робинсона (1965 г.) автоматического доказательства предложений исчисления предикатов.

Термы и предикаты

Термы и их унификация

Упрощённо можно сказать, что термы – это алгебраические выражения, определяющие функции, значения которых вычисляются с помощью операций. Например, в булевой алгебре А определены операции: , , , и из этих операций можно составлять термы, например, , , . Перейдём к точным определениям.

Пусть – счётное множество, элементы которого будут называться переменными, F – произвольное множество, элементы которого будут называться функциональными символами, – произвольная функция. Элементы f Î F, для которых , называются n-арными операциями. Например, для булевой алгебры множество функциональных символов будет равно: F = {Ç, È, Ø}, значения функции # равны #(Ç) = 2, #(È) = 2, #(Ø) = 1, поэтому все элементы из F – операции. Символы c Î F, для которых #(с) = 0, называются символами констант. Термы определим по индукции:

1) переменные и символы констант являются термами;

2) если – термы и f – n-арная операция, то – терм;

3) кроме построенных с помощью правил 1 – 2, других термов нет.

В определении терма участвует префиксная форма операции. Заметим, что бинарные операции записываются обычно в инфиксной форме. Например, вместо применяется запись: . Учитывая приоритеты операций, скобки часто опускают, в частности, приведённая запись равносильна выражению: , ибо приоритет операции Ç выше приоритета È.

Согласно определению терма, множество всех термов T(F) содержит множество переменных X. Подстановкой называется отображение такое, что для всех x Î X, за исключением элементов некоторого конечного подмножества из X, имеет место v(x) = x. Распространим подстановку v до некоторой функции , полагая

1) если t Î X, то v¢(t) = v(t);

2) если t – символ константы, то v¢(t) = t;

3) если для некоторой n-арной операции f и термов , то .

Терм v¢(t) называется результатом применения подстановки v к терму t. Например, результатом подстановки

, ,

в терм будет терм: . Если значения не указаны, то по умолчанию . Подстановку записывают как множество пар , например: .

Пусть заданы два терма s и t, и пусть надо найти подстановку, делающую эти термы равными. Эта задача решается следующим образом.

Подстановка v называется унификатором термов s и t, если v¢ (s) = v¢ (t). Унификатор v называется наибольшим общим унификатором термов s и t и обозначается: m.g.u.(s, t) = v, если для любого другого унификатора w термов s и t существует такая подстановка a, что a¢ _° v¢ = w¢. Если для термов s и t существует хотя бы один унификатор, то среди унификаторов существует наибольший общий. Для его нахождения предлагается следующий алгоритм.

Алгоритм унификации термов с использованием стека

Вход: термы s, t.

Выход: подстановка h, записанная как список пар , если t и s обладают наибольшим общим унификатором. Процедура возвращает отказ, если унификаторов нет.

Действия: h = Æ; запомнить пару (s = t) в стек;

Пока стек не пуст, выполнять цикл:

Тело цикла: Извлечь из стека пару термов (s = t) и произвести одно из следующих действий, в зависимости от выполнения одного из условий

I если s – переменная, t – терм, не содержащий вхождений s, то все вхождения переменной s в стеке заменяются на t и все вхождения s в h заменяются на t, затем подстановка s = t добавляется к списку подстановок в h;

II если t – переменная, а s – терм, то произвести действия, как в I, поменяв ролями s и t (к h добавляется пара t = s);

III если s и t – составные термы, и , то все пары , 1 £ i £ n, запоминаются в стек;

IV если s и t – одинаковые символы констант или переменных, то ничего не делать;

V во всех остальных случаях производится выход из цикла и возвращается отказ.

Конец тела цикла.

Если выход из цикла произошёл не после выполнения условия V, то h содержит элементы искомой подстановки.

Пример

s = (a Ç b) È ((a Ç b) Ç d), t = (a Ç b) È (c Ç (a Ç b)).

1) Устанавливаем h = Æ; запоминаем в стек пару (s = t);

2) извлекаем (s = t) из стека, имеет место случай III, запоминаем в стек пары и ((a Ç b) Ç d = c Ç (a Ç b));

3) извлекаем из стека ((a Ç b) Ç d = c Ç (a Ç b)), имеет место случай III, запоминаем в стек (a Ç b = c) и (d = a Ç b);

4) извлекаем из стека (d = a Ç b), имеет место случай I, h = {(d = a Ç b)};

5) извлекаем из стека (a Ç b = c), имеет место случай II, ;

6) извлекаем из стека , изменений в h нет;

7) стек пуст, возвращаем .

Система уравнений

Пусть задано несколько пар термов и необходимо найти подстановку w, которая превращает все пары термов в равные . Эта задача называется системой уравнений: .

Унификатором системы уравнений называется подстановка v, которая является унификатором пар для всех 1 £ i £ n. Система уравнений , 1 £ i £ n, называется находящейся в разрешённой форме, если каждое из этих уравнений имеет вид: для некоторого элемента , причём переменная не входит в терм ни при каком i. Такая система имеет унификатором подстановку: , которая будет наиболее общим унификатором этой системы. Редукцией термов называется замена уравнения системой уравнений: .