3.7.7. Реализация алгоритма унификации

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

При унификации этот алгоритм применяется к каждой теореме рассматриваемой предметной области; при заданной теореме он применяется к каждому подвыражению исследуемого при этом выражения. Ниже представлена общая форма процедуры доказательства.

Общая процедура доказательства

ПРОЧЕСТЬ — множество допустимых продукций или правил переписывания в данной предметной области; представляет собой данные, связанные с процедурой в самом общем смысле}.

(см. скан)

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

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

На самом деле то же явление зацикливания может порождаться и одним единственным правилом, таким, например, как

или

Правило такого типа вызывает бесконечные преобразования двух термов из следующих друг за другом, например,

при таком наборе правил: и

где происходит зацикливание по выражению

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

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

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

Возможен случай, когда применение некоторых правил оказывает влияние и на использование каких-то других правил, применение которых до этого было запрещено. Это тот случай, когда в результате применения некоторого правила структура рассматриваемого выражения изменяется в такой “достаточной” степени, что вероятность возврата к предшествующему состоянию становится несущественной.

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

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

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

Таблица 3.3. Правила переписывания для упрощения алгебраических выражений

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