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

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

алгебраический модель эквациональный правило

Системы переписывания термов (СПТ) применяются при решении таких известных задач как автоматическое доказательство теорем [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 подводятся итоги и указываются некоторые перспективы. Ввиду ограничения на объем статьи доказательства сформулированных теорем планируются к опубликованию в отдельной работе.

1. Основные понятия и обозначения

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

Как известно, множество всех конечных подмножеств универсума образует решетку. В настоящей статье рассматривается именно такой вид решеток. Чтобы подчеркнуть данное обстоятельство, вместо символов , , и будем использовать знаки теоретико-множественных операций , , и . Однако термин «решетка» сохраняется, поскольку в дальнейшем результаты могут быть распространены и на другие виды решеток.

Приведем некоторые базовые определения, связанные с термами [Klop, 1992]. Пусть - алфавит, образованный объединением непересекающихся множеств: - множество переменных; , - множества -арных функций (функциональных символов); -арные функции называются также константами. Множество термов определяется рекурсивно: · ; ;

если и , то .

Отображение называется подстановкой. Это понятие распространяется на все следующим образом: если , то ;

если , то ;

если , и , то .

Эквациональной теорией называется пара , где

· - алфавит, состоящий из счетного множества переменных и непустого множества функциональных символов (сигнатура);

· - множество равенств вида .

Определяется понятие выводимости равенства из ( ) на основе следующих правил: 1) если , то ;

2) если , то для любого ;

3) если , то для всех подстановок ;

4) ;

5) если , то ;

6) если , то .

Для множества равенств введем решетку конечных подмножеств . На основании правила 6) будем в этой решетке отождествлять пары элементов вида и . В заданы отношения , , а также «решеточные» операции и - теоретико-множественные пересечение и объединение. Кроме них потребуются еще три группы операций, связанных соответственно с функциями, подстановками и транзитивностью равенств термов: 1) если и , то ;

2) если , то для подстановки ;

3) если , то .

Определение 2.1. Пусть задана теория . Эквациональной решеткой будем называть решетку, полученную пополнением относительно определенных выше дополнительных операций 1)-3).

Как уже подчеркивалось во Введении, рассматривается условная эквациональная теория, содержащая условные правила вида . Таким образом, предпосылка и заключение правила являются элементами .

Используя в качестве основы аксиомы и правила, определенные в [Klop, 1992], сформулируем их аналоги для условной эквациональной дедукции. Аксиомы порождаются перечисленными выше правилами вывода равенств. Правило 2) означает наличие условного правила (аксиомы) для любых и ; из 3) следует аксиома для любых и подстановки . Правило 5) порождает аксиому для каждого подходящего . Еще одной очевидной аксиомой является правило при .

Заметим, что правило 6) было учтено при определении множества . Что касается правила 4), то в соответствии с ним можно было бы ввести множество аксиом вида . Однако роль таких «вырожденных» аксиом для рассматриваемых в настоящей работе задач несущественна, поскольку трудно оправдать наличие равенства в предпосылке или заключении условной продукции.

Правила вывода в условной эквациональной дедукции таковы: 1) для любой подстановки (см. аналогичное правило в [5] с исходными обозначениями);

2) (возможность вывода по частям);

3) (транзитивность).

2. LP-структура для условной эквациональной теории

Согласно [Махортов, 2009], LP-структурой (Lattice Production Structure) называется решетка с дополнительно заданным на ней бинарным отношением, которое обладает рядом продукционно-логических свойств. В этом разделе рассматриваются отношения на эквациональной решетке. Вводится понятие логического отношения, которое соответствует множеству правил условной эквациональной теории. Свойства такого отношения должны отражать сформулированные в п.1 аксиомы и правила условной эквациональной дедукции.

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

Определение 2.1. Отношение назовем применимым, если для любой подстановки из следует .

Определение 2.2. Отношение назовем -дистрибутивным, если для любых выполнено .

Следующее определение суммирует рассмотренные свойства.

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

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

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

1) : 1.1) или 1.2) или 1.3) или 1.4) ;

2) существуют такие и подстановка , что , причем ;

3) существуют такие , что , причем ;

4) существует элемент такой, что и .

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

Следствие 2.1. Пусть - бинарное отношение на эквациональной решетке и ( конечно). Тогда отношение эквивалентно .

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

Теорема 2.2. Пусть - отношения на общей эквациональной решетке. Если при этом и , то .

Следствие 2.2. Пусть - отношения на общей эквациональной решетке. Если при этом , то .

Следствия 2.1 и 2.2 обосновывают принцип локальности эквивалентных преобразований отношений: если часть данного отношения заменить эквивалентной частью, то и в целом новое отношение будет эквивалентным исходному. Эти результаты открывают возможности автоматических преобразований условных эквациональных теорий.

Далее выясним вопрос о возможности в процессе построения логического замыкания выделить этап, соответствующий транзитивному замыканию. Положительный ответ позволит свести изучение некоторых важных вопросов, касающихся логических отношений, к соответствующим проблемам транзитивных отношений. В частности, построение логического замыкания или редукции можно будет осуществлять с помощью быстрых алгоритмов (типа Уоршолла [Aho et al., 1972]).

Для произвольного отношения на эквациональной решетке рассмотрим отношение , построенное последовательным выполнением следующих шагов: 1) добавить к все пары , для которых , либо , и обозначить новое отношение ;

2) добавить к всевозможные пары вида , для которых , и обозначить новое отношение ;

3) добавить к всевозможные пары вида , где , и обозначить новое отношение ;

4) объединить с отношением .

Заметим, что шаги 1) и 4) относятся ко всем теоретически возможным элементам эквациональной решетки и соответственно не зависят от данного . В силу бесконечности множества описанный процесс построения отношения носит теоретический характер. В приложениях вместо можно взять конечное подмножество эквациональной решетки, построенное при ограничении уровня вложенности термов.

Теорема 2.3. Логическое замыкание отношения совпадает с транзитивным замыканием соответствующего отношения .

Выясним вопрос о существовании и построении логической редукции бинарных отношений. Для отношения на эквациональной решетке рассмотрим отношение , построенное по данному последовательным выполнением шагов, обратных построению , а именно: 1) исключить из все пары , для которых , и обозначить новое отношение .

2) исключить из все пары вида , где , причем не совпадает ни с одной парой , и обозначить новое отношение ;

3) исключить из всевозможные пары вида , для которых , причем не совпадает с парой , и обозначить новое отношение ;

4) исключить из все пары , для которых , , либо .

Вновь подчеркнем, что выполнение шагов 1), 4) связано с «универсальными» тавтологиями, и поэтому алгоритмы их выполнения существенно не зависят от исходного отношения . Следующая теорема указывает достаточное условие существования и способ построения логической редукции бинарного отношения.

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

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

В дальнейшем можно рассмотреть более общую модель LP-структуры, если в качестве ее основы вместо использовать решетку Линденбаума-Тарского [Расева и др., 1972]. Тогда моделируемые условные правила смогут в качестве предпосылок и заключений содержать формулы пропозиционального исчисления. При этом общая методология исследования останется прежней.

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

[Воробьев, 1987] Воробьев С. Г. Условные системы подстановок термов и их применение в проблемно-ориентированной верификации программ: автореф. дис. к. ф.-м. н. - Новосибирск: ВЦ СО АН СССР, 1987.

[Махортов, 2009] Махортов С. Д. Основанный на решетках подход к исследованию и оптимизации множества правил условной системы переписывания термов // Интеллектуальные системы. - 2009. - Т. 13, вып. 1-4.

[Махортов и др., 2010] Махортов С. Д., Баранов Д. В. LP-структуры в условных системах переписывания // Современные проблемы информатизации в моделировании и социальных технологиях: сб. трудов / под ред. О. Я. Кравца. - Воронеж: Научная книга, 2010. - Вып. 15.

[Расева и др., 1972] Расева Е., Сикорский Р. Математика метаматематики. - М.: Наука, 1972.

[Aho et al., 1972] Aho A. V. The transitive reduction of a directed graph. SIAM J. Computing 1 : 2 / A. V. Aho, M. R. Garey, J. D. Ulman, 1972.

[Buchberger et al., 1982] Buchberger B., Loos R.. Algebraic Simplification // Computer Algebra - Symbolic and Algebraic Computation / eds. B. Buchberger, G. E. Collins, R. Loos. - Vienna - New York : Springer-Verlag, 1982.

[Dershowitz et al., 1988] Dershowitz N., Okada M., Sivakumar G. Canonical Conditional Rewrite Systems // Proceedings of the 9th international Conference on Automated Deduction (May 23-26, 1988) / eds E. L. Lusk, R. A. Overbeek // Lecture Notes In Computer Science. - London : Springer-Verlag. - 1988.

[Hsiang, 1985] Hsiang J. Refutational theorem proving using term-rewriting systems // Artif. Intell. - 1985.

[Klop, 1992] Klop J. W. Term rewriting systems // Handbook of Logic in Computer Science (Vol. 2): Background: Computational Structures / eds S. Abramsky, D. M. Gabbay and S. E. Maibaum // Osborne Handbooks of Logic In Computer Science. - New York : Oxford University Press. - 1992.

[Toyama, 1986] Toyama Y. On Equivalence Transformations for Term Rewriting Systems// Proceedings of the 1983 and 1984 RIMS Symposia on Software Science and Engineering II / eds E. Goto, K. Araki and T. Yuasa // Lecture Notes In Computer Science. - London : Springer-Verlag. - 1986.

Размещено на .ru