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

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

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

Приведем некоторые базовые определения, связанные с термами [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) (транзитивность).