3.7.5. Завершение работы алгоритма унификации

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

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

Приведем примеры работы алгоритма.

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

Таким образом можно унифицировать функции но затем необходимо сделать подстановку , а это запрещено (случай неудачи 1 в процедуре

4) Рассмотрим вновь пример из исчисления высказываний,

который уже встречался нам выше:

При этом будем использовать для наглядности древовидную структуру представления выражений (рис. 3.8-3.10).

Два первых символа в выражениях Е и являются одним и тем же оператором продвигаются вперед по обоим деревьям. В Е встречается какая-то переменная (пусть это будет тогда как в знак указывает на начало некоторого терма Следовательно, нужно изменить в где есть поддерево (рис. 3.9).

Рис. 3.8. Унификация в исчислении высказываний.

Рис. 3.9. Унификация (продолжение).

Уже исследованные символы представлены точками.

Рис. 3.10. Унификация (окончание).

В выражении Е встречается связка в той позиции, в которой в выражении Т встречается Р. На рис. 3.10 показан дальнейший ход унификации.

Как видно из рис. 3.10, унификация в данном случае прошла успешно. Выражение Е преобразуется в выражение

при помощи подстановок Другими словами, выражение Е и часть гипотезы Н теоремы Т приведены к виду

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

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