6.12. УНИФИКАЦИЯ

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

Термы литерала могут быть переменными буквами, константными буквами и выражениями, состоящими из функциональных букв и термов. (Подстановочный) частный случай литерала получается при подстановке в литералы термов вместо переменных. Например, для литерала частными случаями будут

Первый частный случай называется алфавитным вариантом исходного литерала, поскольку здесь вместо переменных, входящих в подставлены лишь другие переменные. Последний из перечисленных четырех частных случаев называется константным частным случаем, или атомом, так как ни в одном из термов этого литерала нет переменных.

В общем случае любую подстановку можно представить в виде множества упорядоченных пар Пара означает, что повсюду переменная у, заменяется термом Существенно, что переменная в каждом ее вхождении заменяется одним и тем же термом, т. е. Из следует, что Для получения частных случаев литерала были использованы четыре подстановки

Обозначим через частный случай литерала Р, получающийся при использовании подстановки 0. Например, Композицией двух подстановок называется результат применения к термам подстановки а с последующим добавлением любых пар из содержащих переменные, не входящие в число переменных из а. Например,

Можно показать, что применение к литералу Р последовательно подстановок дает тот же результат, что и применение к Р подстановки Можно также показать, что композиция подстановок ассоциативна:

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

Унификатор для множества в некотором смысле не является простейшим.

Заметим, что для унификации нет необходимости подставлять а вместо х. Наиболее общим (или простейшим) унификатором для будет такой унификатор К, что если 0 — какой-нибудь унификатор для дающий то найдется подстановка 6, для которой . «Общий» частный случай, соответствующий наиболее общему унификатору, единствен с точностью до алфавитных вариантов.

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

будет

Далее алгоритм пытается так модифицировать подстановку чтобы сделать равным два элемента из множества рассогласования. Это можно сделать только тогда, когда множество рассогласования содержит переменную, которую можно положить равной одному из его термов. (Если множество рассогласования вообще не содержит переменных, то множество унифицировать нельзя. Например, на первом шаге работы алгоритма множество рассогласования может оказаться самим и тогда ясно, что ни один из элементов будет переменной.)

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

Можно доказать (Робинсон, 1965а и Лакхэм, 1967), что описанный алгоритм находит наиболее общий унификатор для множества унифицируемых литералов и сообщает о неудаче, если литералы неунифицируемы. Мы не будем давать здесь доказательство этого утверждения.

В качестве примеров приведем «общие» частные случаи, соответствующие наиболее общему унификатору для ряда множеств литералов.

Принято рассматривать предложения как множества литералов. Тогда предложение, содержащее множество литералов, можно также обозначить

Если подмножество литералов в некотором предложении унифицируемо с помощью , то предложение называют фактором предложения Факторами предложения

являются, например, предложения

и

В первом факторе унифицированы только два последних вхождения литерала а во втором все три. Заметим, что в этом предложении два вхождения литерала Р нельзя унифицировать. Вообще предложение может иметь более одного фактора, но, во всяком случае, число факторов конечно.