3.7.6. Незамещаемые переменные

До сих пор предполагалось, что переменные в выражении теореме Т играют одну и ту же роль, однако это не всегда так. Действительно, какова бы ни была рассматриваемая формальная система, уже по определению переменные теоремы являются во всех случаях замещаемыми. Это вытекает из того, что с самого начала предполагается, что эти переменные являются универсально Г-квантифицированными и становятся свободными в силу аксиомы спецификации. Однако часто встречаются и ситуации, когда “переменные” в Е не являются замещаемыми.

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

переменные становятся в результате все более ограниченными (связанными) и их нельзя законным образом замещать каким-либо термом. В частности, возможно, что различные “переменные” становятся взаимозависимыми.

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

является вполне допустимым. Когда же пытаются его применить к какому-то текущему выражению, например

то первая подстановка, когда а замещается на х, является допустимой. Теорема Т переходит в П:

Однако вторая подстановка, при которой переменная у замещалась бы термом здесь в принципе недопустима, так как, например, при решении какой-то системы уравнений относительно неизвестных х и у эта система связывает “переменные” х и у между собой. (Если, однако, желательно выполнить эту подстановку, то следовало бы ввести преобразование

(у заменяется на

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

Рассмотрим более конкретный пример.

В поле вещественных чисел правило переписывания, приведенное ниже, ярляется допустимым:

Это правило может быть использовано для упрощения следующего выражения:

Первая подстановка заменяет на в теореме Т, которая принимает вид

Вторая подстановка замещает х на в теореме унификация является успешной и заключительная формула теоремы

Т имеет вид

Однако здесь неявно использовано дополнительное условие при последней подстановке.

В свою очередь при решении уравнения мы получаем либо (и, следовательно, ). Однако на самом деле выражение может быть решено непосредственно без использования теоремы и тогда либо

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

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

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