Введение. 
Исследование и оптимизация условных систем переписывания на основе продукционно-логической модели

Системы переписывания термов (СПТ) применяются при решении таких известных задач как автоматическое доказательство теорем [Hsiang, 1985], символьное упрощение алгебраических выражений [Buchberger et al., 1982], верификация компьютерных программ [Воробьев, 1987] и других. Важными вопросами СПТ являются эквивалентные преобразования и упрощение их множеств правил. Для обычных СПТ подобные задачи решались в ряде работ (например, [Toyama, 1986]), для условных СПТ они еще остаются открытыми. Данное обстоятельство объясняется более сложной структурой правил условных СПТ. Для обычных систем задача минимизации множества правил сводится к транзитивной редукции бинарного отношения. Для условных систем можно говорить о более сложной задаче нахождения логической редукции.

При определении системы переписывания отправной точкой является эквациональная теория, множество правил которой состоит из равенств термов. Правила СПТ получаются путем «ориентации» равенств и, возможно, пополнения для достижения свойства конфлюэнтности [Klop, 1992]. Аналогичный подход используется и для условных СПТ [Dershowitz et al., 1988]. Поскольку обычно именно эквациональная теория дает критерий эквивалентности систем переписывания, исследование в этом плане условных СПТ может быть начато с рассмотрения эквивалентности самих условных эквациональных теорий.

В работе [Махортов, 2009] представлена методология исследования условных СПТ на основе «решеточных» продукционно-логических структур (LP-структур). Полученные результаты, в частности, впервые решают задачу построения логической редукции условной эквациональной теории. Однако рассмотренная там алгебраическая модель оперирует равенствами как атомами, не учитывая некоторые их транзитивные свойства. Данное обстоятельство приводит в общем случае к незавершенной минимизации множества условных правил при построении его логической редукции. В настоящей работе вводится и исследуется более сложная LP-структура, в результате чего отмеченный недостаток устраняется. Некоторые из полученных здесь результатов были анонсированы в сообщении [Махортов и др., 2010].

Исходная эквациональная теория состоит из условных соотношений вида («если имеют место равенства термов, то выполнены и все «). Будем называть такие соотношения (условными) эквациональными правилами, или просто правилами там, где это не будет вызывать недоразумений. Равенства между термами интерпретируются обычным для эквациональных теорий способом:, если данное равенство можно получить из имеющегося набора равенств с помощью рассматриваемой эквациональной дедукции. Соответствующие ей аксиомы и правила вывода определяются в п. 1. Они естественным образом расширяют набор аксиом и правил вывода, описанный в [Klop, 1992] для условных равенств вида .

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

Кроме разработки самой модели, основные результаты статьи (сформулированы в п.2) состоят в следующем. Представлено утверждение о существовании логического замыкания (теорема 2.1) бинарного отношения, что в приложении приводит к понятию эквивалентных эквациональных теорий. Обоснована возможность локально-эквивалентных преобразований исходного отношения (теорема 2.2), соответственно и преобразования множества правил. Исследована структура логического замыкания (теорема 2.3), что позволяет при его построении использовать эффективные алгоритмы. Изучены вопросы существования и построения логической редукции бинарного отношения (теорема 2.4). Это исследование дает теоретическую основу для минимизации условной эквациональной теории. Под минимизацией подразумевается получение такой эквивалентной системы, из которой невозможно удалить ни одного правила без нарушения эквивалентности.

В п. 3 подводятся итоги и указываются некоторые перспективы. Ввиду ограничения на объем статьи доказательства сформулированных теорем планируются к опубликованию в отдельной работе.