Конгруэнции на термах и унификация Гавриленко, Юрий Вячеславович

Введение к работе

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

Метод решения уравнений в термах - унификация - был найден Э. Постом и Ж. Эрбраном уже на раннем этапе развития математической логики. Однако интенсивное изучение приемов унификации и их широкое применение началось лишь после знаменитой работы Дж. Робинсона [і], положившей начало машинному алгоритму автоматического поиска доказательств теорем. - принципу резолюций, стержнем которого стала унификация.

Усилия исследователей в этом направлении привели к созданию теории унификации или точнее теории уравнений в термах - новой математической дисциплины, использующей методы алгебры и логики. Исчерпывающий обзор основных достижений и ретроспективный анализ истории развития этой теории представлен в ста^-, ье Й. Зикмана [2].

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

полный перечень дисциплин, где приложения унификации оказались плодотворны. Глубоки и интересны "внутриматематические" применения унификации, например, в теории доказательств [3].

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

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

Задача унификации в исчислениях равенств заключается в следующем. Фиксируем n = < var, con, Fn, " ) - произвольную алгебраическую сигнатуру, содержащую счетное множество переменных, множество констант, множество функциональных символов и символ равенства. Совокупность Тт(П) термов рассматриваемой сигнатуры задается обычными индуктивными правилами:

1. Если t - переменная или константа, то teTm(n).

2. Если feFn - функциональный символ валентности п>о, t_lf t₂,..., t_neTm(n), то f(t₁₍ t₂,...,t_n)eTm(n).

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

Пусть е - произвольное исчисление равенств, т.е. совокупность аксиом, каждая из которых имеет вид Vx_x—x_m(p=q), где

p,qeTm(n), a x_lr , - полный список переменных, входящих в р

и q. Два терма t и s связаны в Е отношением эквивалентности =_к, если формула t=s выводима из аксиом Е в логике первого порядка с равенством. Если Г - конечная система уравнений в термах: '

Г - { t_A - Sj. | ISiSn, t_L, B_L ТЮ(П) },

то финитная (т.е. имеющая конечную оОласть определения) подстановка a: Var -» Та(П) называется унификатором (т.е.решением) Г, если оЬ± =_г оз± для всех 15І5П.

Унификатор о называется самым общим унификатором Г (в другой терминологии - наиболее общим унификатором), если a <_Е о' для любого ее унификатора а' (т.е. если существует такая подстановка X, что a't =_в Xat для всех teTm(n)).

Основные вопросы, связанные с унификацией в Е, таковы:

1. всякая пи система уравнений г имеет унификатор ?

2. всегда пи разрешимая система уравь.зний имеет самый общий унификатор ?

3. как устроено многообразие самых общих унификаторов г (т.е. как они связаны друг с другом ) ?

4. какие системы уравнений в термах Е-эквивапентны, т.е.имеют одни и те же решения ?

Если для исчисления Е отношение =-. совпадает с графическим равенством термов, то задача унификации для Б называется классической.

Группа французских математиков, возглавляемая создателем языка ПРОЛОГ Д.-Копмероэ, исспецовапа обобщение классической задачи на спучаї: алгебры регулярных деревьев R(F) [4 -7]. При таком обобщении решение системы уравнений в термах Г ищется не в свободной алгебре конечных термов та(П), а среди регулярных дереоь-ес, т.е. унификаторами г яогяотся отображения о: Var - R(F),

приравнивающие все пары термов из Г. В более общем случае и сама система г тоже может состоять из равенств регулярных деревьев.

Такое "нестандартное" определение унифицируемости помимо своей математической естественности мотивируется уже тем, что все ' практические версии языка ПРОЛОГ используют не оригинальный алгоритм унификации [1], а- лишь его "урезанный" вариант (без проверок вхождения переменных), реализующий (некорректное) понятие унифицируемости, близко напоминающее унификацию в R(F) (см. [1*, 8]).

Исследования группы Копмероэ увенчались разработкой нового языка логического программирования ПРОПОГ-ІІІ, основанного на унификации в бесконечных регулярных деревьях [7].

Однако унификацию в регулярных деревьях вряд ли можно признать вполне удовлетворительной хотя бы потому, что уравнения x-=f(x) и x=f(f(x)), интуитивно воспринимаемые как Ьезусповно различные, оказываются эквивалентными в алгебре R(F), так как имеют одно и то же (единственное) бесконечное решение: х = f(f(f( ... f(...) ... ))) .

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

Между тем, осуществить поставленные ш л средствами,- .уже имевшимися в арсенале теории унификации, оказалось невозможным, поскольку все хорошо известные методы решения систем уравнений в термах, изложенные, например, в работах [і, 9 - 12), существенно опирались на конечность рассматриваемых систем и непосредственно не 'обобщались на бесконечный случай.

Попытки -преодолеть указанную трудность привели к мысли о том.

7 .

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

Кроме таких конгруэнций-модепей бескон жых систем уравнений в термах п диссертаци исследованы и обычные унификаторы-подстановки (естественно, нефинитные, для которых также пришлось-создать нов'ый математический аппарат [4*.- б*]).

Был выделен и иследован важный в приложениях подкласс самых общих решений систем уравнений в термах - главные решения, удовлетворяющие свойству идемпотентности [2*, 3*].

В заключение кратко сформулируем основные цели предлагаемого исследования:

1) исследовать конгруэнции на тепмах в качестве-

алгебраических модепей-унификаторов для Систем уравнений в термах,

2) изучить свойства решений произвольных - как конечных, так
и зсконечных - систем уравнений в термах,

3) описать строение главных решений произвольной системы
уравнений в термах.

НАУЧНАЯ ' НОВИЗНА.

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

генетически связано с понятием упрощаемого и когерентного бинарного отношения, вскользь упоминаемого в работе [4]. Заметим также, что употребление термина "конгруэнция" в диссертации не вполне соответствует апгебраической традиции (см., например, [14]). Частный случай утверждения з.ю.14 для конечных систем уравнений в термах установлен в-[13] и независимо автором в работе [2*].

Результаты диссертации могут быть использованы в исследованиях по логическому программированию. Наиболее перспективным представляется применение унификации бесконечных систем уравнений в термах к проблемам -теории неограниченно продолжающихся логических вычислений [12].

Отдельные части исследования докладывались -в 1988 г. на Всесоюзном семинаре "Семиотические аспекты формализации интеллектуальной деятельности. Боржоми-88" [1*] и на Второй всесоюзной конференции "Прикладная логика" [2*]. В 1991 г. результаты диссертации были доложены на Вторых математических чтениях памяти М. Суспина [4*].

Отдельные результаты диссертации излагались в 1989 г. на семинаре по математической логике кафедры математической логики МГУ. В попном виде доказательства всех результатов диссертации были заслушаны в 1988 - 1992 гг. на семинаре "Математическая логика й информатика" (Вычислительный центр РАН, Москва).

По теме диссертации, автором опубликовано б работ [1*.- 6*]. Основные результаты изложены в [3*], [5*] и [6*].

Диссертация состоит из введения, трех глав, .заключения, списка литературы (24 наименования) и приложения, включающего индекс ключевых слов и обозначений. Диссертация содержит'' 147 страниц основного текста и 7 страниц приложений.