3.7.2. Идея алгоритма

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

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

имен” переменных из Е или Т, каковы бы были их начальные имена.

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

Фундаментальная идея, лежащая в основе алгоритма, связана с процедурой просмотра выражения: вначале основной оператор, затем каждый из подтермов, которыми он управляет, начиная, например, с самого левого. Каждый подтерм при этом просматривается параллельно: основной оператор, подтерм и так далее до переменной или константы. Удобным для этого является представление выражения в виде дерева (рис. 3.5).

Рис. 3.5. Представление выражения и порядок его просмотра в соответствии с алгоритмом унификации.

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

Используя этот порядок просмотра (вначале вглубь), для задания последовательности просмотра введем индексы ей — индекс текущего символа в выражении Е и — индекс текущего символа в выражении Н.

В общем случае принцип рекуррентности формулируется следующим образом: пусть все символы в выражениях Е и Н совпадают вплоть до символов с индексами и не включая их; попытаемся привести к совпадению символы с индексами и соответственно в Е и Н. Имеются четыре возможных варианта ситуаций, при которых каждый из символов с индексами и соответствует (либо нет) какой-то замещаемой переменной. Если подстановка должна быть сделана, она выполняется с помощью определенной процедуры, называемой Ниже описана эта процедура подстановки.