Оценки высоты термов в наиболее общем унификаторе тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

61' п-Цбог-н

а

РОССИЙСКАЯ АКАДЕМИЯ НАУК САНКТ-ПЕТЕРБУРГСКОЕ ОТДЕЛЕНИЕ МАТЕМАТИЧЕСКОГО ИНСТИТУТА ИМ. В. А. СТЕКЛОВА

На правах рукописи

Конев Борис Юрьевич

ОЦЕНКИ ВЫСОТЫ ТЕРМОВ В НАИБОЛЕЕ ОБЩЕМ

УНИФИКАТОРЕ

01.01.06 — математическая логика, алгебра и теория чисел

Диссертация на соискание учёной степени кандидата физико-математических наук

Научный руководитель

доктор физико-математических наук

профессор В. П. Оревков

Санкт-Петербург — 1998

Оглавление

Введение 3

1 Оденки высоты термов в наиболее общем унификаторе 14

1.1 Основные понятия............................................14

1.1.1 Термы и меры сложности ..........................14

1.1.2 Подстановки и задача унификации................16

1.1.3 Процедуры унификации............................19

1.2 Оценки относительно разности глубин....................31

1.2.1 Нижняя оценка ......................................32

1.2.2 Верхняя оценка......................................44

1.3 Оценки относительно количества неизвестных не типа сечения........................................................55

1.3.1 Нижняя оценка ......................................56

1.3.2 Верхняя оценка......................................61

1.4 Оценки относительно количества неизвестных с различными путями..............................................68

1.4.1 Нижняя оценка ......................................69

2 Верхняя оценка высоты термов в выводах с сечениями 76

2.1 Исчисления КвЬ и ЮЬ......................................76

2.2 Верхняя оценка высоты термов в выводе с сечениями

в исчислении КО/ и ЮЬ......................82

Литература 95

Введение

Задача и алгоритм унификации

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

В наиболее общем виде задача унификации является задачей, формулируемой следующим образом. По двум описаниям X и У определить, можно ли найти объект удовлетворяющий обоим описаниям? Эта задача обычно уточняется как задача определения по двум термам первого порядка, существует ли подстановка термов вместо переменных, которая превращает исходные термы в идентичные. Такая подстановка называется унификатором. Помимо задачи определения, существует ли такая подстановка, ставится задача поиска алгоритма унификации, строящего унификаторы для заданной пары термов. Унификатор а называется более общим, чем унификатор г, если т может быть представлен в виде композиции т = Л о <т для некоторой подстановки Л. Унификатор называется наиболее общим, если любой другой унификатор может быть представлен в виде его композиции с некоторой подстановкой.

Первое упоминание о концепции унифицирующего алгоритма, выдающего наиболее общий представитель множества всевозможных примеров, может быть найдено в дневниках и записках Э. Поста, относящихся к 20-м годам и опубликованных в 60-е годы в [17]. Явное описание алгоритма унификации впервые встречается в диссертации

Ж. Эрбрана [27], в которой он вводит три концепции допустимости формул. Он называет их А, В и С. Концепции В и С лежат в основе известной теоремы Эрбрана. Для проверки того, что формула удовлетворяет концепции А, Эрбран приводит вычисляющий её алгоритм. В этой работе употреблялась техника, переоткрытая позднее А. Мартелли и У. Монтанари [36], которая используется и по сей день.

Основываясь на идеях Эрбрана о конечном опровергающем примере, Д. Правиц [41] в 1960 году предложил алгоритм, основанный на последовательном переборе выводимых формул, позднее получивший название "Алгоритм Британского Музея", в котором используется процедура, вычисляющая наиболее общий представитель множества всевозможных примеров. Однако, поскольку в его логике не содержалось функциональных знаков, реальных вычислений было не так уж много. В 1963 г. М. Девис [16] опубликовал процедуру вывода, объединяющую достоинства процедуры Правица и процедуры Девиса-Патнема [19, 18]. В реализации этой новой процедуры был использован алгоритм унификации, что явилось первым практическим воплощением данного алгоритма.

В 1965 г. в работе [42] Дж.А. Робинсон ввел формальное определение алгоритма унификации для термов первого порядка, вычисляющего наиболее общий унификатор. Именно в этой работе была установлена роль унификации как части процедуры автоматического вывода. Примерно в это же время, в 1965-69 гг., в Ленинградском отделении Математического института им. В.А. Стеклова велись работы по разработке алгоритмов автоматического вывода на основе обратного метода С.Ю. Маслова [2]. В реализации этого метода была использована процедура унификации, однако она не была отдель-

но опубликована. Построенный алгоритм унификации был полным и корректным; оценка на время его работы от размера входа была квадратичной. М. Патерсон и М. Вегман, используя эти же идеи, в работе [39] независимо построили линейный алгоритм унификации.

Как было отмечено выше, алгоритм унификации играет ключевую роль для многих процедур автоматического вывода; зачастую его рассматривают как один шаг процедуры вывода. Разработка эффективного алгоритма унификации представляла, тем самым, особый интерес. Оригинальный алгоритм Робинсона был недетерминированным и экспоненциальным. С конца 60-х гг. был получен ряд результатов по улучшению времени работы алгоритма унификации [13, 45, 28]. К наиболее значительным следует отнести процедуру Мартелли и Монтанари [36], имеющую почти линейную временную сложность, и процедуру Патерсона и Вегмана [39], которая, как уже упоминалось, линейна. В то же время, последняя процедура использует достаточно сложные структуры данных, реализация которых во многих приложениях требует слишком больших затрат. Дальнейшие улучшения упомянутых алгоритмов и их специальные реализации были опубликованы в работах [30, 14, 22]. Отметим, что в предположении, что сложностные классы Р и N0 не совпадают (а их совпадение считается крайне маловероятным), не существует эффективного параллельного алгоритма унификации, поскольку в работах [20, 21] доказана Р-полнота задачи унификации.

В 1967 г. Робинсон предложил встраивать некоторые нелогические аксиомы непосредственно в механизм процедуры вывода, и в 1972 г. Дж. Плоткин [40] показал, что это можно сделать без потери полноты. Эта идея привела к концепции ^-унификации для теории Е. Так, например, если допустить коммутативность (С-

унификация), термы /(6, а) и /(а, я), будут унифицируемы с унификатором х —У Ъ . В зависимости от теории Е, получающаяся задача унификации может быть разрешимой или нет; кроме того, может иметься или не иметься наиболее общий унификатор. Отметим ассоциативный случай, когда задача унификации есть задача о решении систем уравнений в словах [5]. В обзорах [43] и [31] можно найти ссылки на алгоритмы и задачи унификации для различных теорий.

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

Сведение задач исчисления предикатов к задаче унификации

К задаче унификации сводится ряд задач, возникающих в исчислениях первого порядка. Впервые такое сведение было неявно использовано в работе Р. Париха [38] применительно к известной гипотезе Крайзеля (см., например, [25]). В этой работе проблема решается для аксиоматической теории РА*, варианта арифметики Пеано, в котором сложение и умножение представлено предикатами. В дальнейшем эта техника получила развитие в работах В. Фармера [23, 24], который применил её к задаче ^-выводимости, то есть задаче определения по данной формуле, существует ли её вывод длины не более к. В работах [23, 24] построены семейства исчислений Париха, для которых задача /¿-выводимости разрешима, а также исчисление, для которого эта задача алгоритмически неразрешима.

Основным механизмом сведения задач исчисления предикатов к задаче унификации являются схемы вывода (иногда называемые скелетами вывода) — конструкции, которые отличаются от самих

выводов только тем, что в них представлена вся информация о выводе, кроме термов и переменных, используемых в правилах введения кванторов (более точное определение дается в параграфе 2.1). Идеи, близкие к идеям восстановления вывода по его схеме, содержатся в работе С. Кангера [29], которая оказала большое влияние на развитие исследований по разработке автоматических процедур вывода. Понятие схемы вывода вводится и используется в работах В. Фармера [23, 24], Е.С. Божича [1], Я. Крайчека и П. Пудлака [35], Я. Крайчека [34] и В.П. Оревкова [9, 37].

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

В работе Оревкова [6] получена верхняя оценка на размер термов в доказательствах в секвенциальном исчислении, в котором сечения допускаются только по бескванторным формулам. А именно, любой вывод V без кванторных сечений может быть перестроен в вывод V* той же секвенции, причем высота термов, участвующих в применениях правил 3 и V —в выводе V*, не превосходит произведения максимальной высоты термов последней секвенции и числа применений правил введения кванторов -> 3 и V —> выводе V. Аналогичная оценка для выводов без сечений была независимо получена Крайчеком и Пудлаком [35]. В этих работах, по схеме вывода и по его последней секвенции, строится система пар термов (в работе [6] система уравнений в термах), и оценка на размер наиболее общего унификатора для системы пар термов переносится на исходную задачу.

В случае выводов с сечениями по произвольным формулам такая конструкция не применима, поскольку, как показали Орев-

ков [8, 12] и, независимо, Крайчек и Пудлак[35], задача определения, существует ли вывод данной секвенции по данной схеме с сечениями, является алгоритмически неразрешимой. Тем не менее, если не заботиться о сохранении схемы, возможно получить верхнюю оценку на размер термов в доказательстве, применив процедуру устранения сечений; в работе [37] разработана техника устранения сечений на уровне схем вывода. Однако, как было доказано Р. Стетменом [44] и, независимо, Оревковым [6], удлинение вывода, в случае устранения всех сечений, не может быть оценено сверху элементарной по Кальмару функцией.

Для случая выводов с сечениями по формулам, не содержащим связанных вхождений переменных ненулевой глубины, в работе [37] были получены оценки на размер свободных термов в выводе. Для этого использовалась техника схем выводов с типами сечений. В этих схемах каждому анализу применения правила сечения приписана некоторая формула, во многом определяющая вид формулы, по которой производится сечение (точное определение дается в параграфе 2.2). Любой вывод V с сечениями по формулам, не содержащим вхождений связанных переменных ненулевой глубины, может быть перестроен в вывод V* той же самой секвенции, причем высота термов, участвующих в применениях правил —3 и V —а также высота свободных термов в формулах сечения в выводе V*, не превосходят

^С[5].д-[Р] + Д[5], (1)

где 5е [5] — максимальная глубина связанных вхождений переменных в последнюю секвенцию, д~[Т>] — число применений правил -» 3 и V /г[5] — высота последней секвенции.

Оденки высоты термов в наиболее общем унификаторе

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

Пусть Г — система (т.е. множество) пар термов. Максимальную высоту термов в результате применения унификатора а к неизвестным системы назовем высотой унификатора и обозначим к [<т]. Пусть а — наиболее общий унификатор. Известны следующие оценки:

%] < |Уаг[Г]|.ВД, (2)

%] < £ ВД + МГ], (3)

жеУаг[Г]

где Н[Г] — высота системы (максимальная высота термов системы), Уаг[Г] — совокупность неизвестных системы, /г* [Г] — максимальная глубина вхождений неизвестной х в систему Г. Оценка (2) была получена в работах [7, 35], оценка (3) была получена в работе [7].

В процессе сведения задач теории первого порядка к задаче унификации, множество неизвестных естественным образом распадается на типы. Например, в работе [6] получена оценка

%]<|Уаг0[Г]|-/1[Г], (4)

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

Кроме оценок относительно количества неизвестных также известны оценки высоты наиболее общего унификатора относительно

других параметров. Разностью глубин неизвестной х в системе Г назовем разность между максимальной и минимальной глубиной вхождений х в Г. Шириной терма Т в Г назовем число вхождений неизвестных в Т. В работе [10] доказана оценка

Н[а] < ¿[Г] • р[Г]1 • |Уаг[Г]| + Л[Г], (5)

где 5[Г] означает максимальную разность глубин неизвестных в системе Г, р[Г] — максимальную ширину термов системы Г.

В случае, если в систему Г входят лишь нуль- и одноместные функциональные знаки, существует линейная оценка относительно данных параметров, к[а] < Х^€Уаг[Г] <УГ] + МГ] < I Уаг[Г]| -5[Г] + /г[Г], где 8Х есть разность глубин вхождений неизвестной х (результат сообщен автору В.П. Оревковым).

Основные результаты

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

В разделах 1.2.1 и 1.3.1 доказывается, что дальнейшее улучшение оценки (4) путем устранения из неё неизвестных с нулевой разностью глубин невозможно. Эти же примеры доказывают невозможность исключения из суммирования оценки (3) членов, соответствующих неизвестным с нулевой разностью глубин. А именно, строятся

других параметров. Разностью глубин неизвестной х в системе Г назовем разность между максимальной и минимальной глубиной вхождений ж в Г. Шириной терма Т в Г назовем число вхождений неизвестных в Т. В работе [10] доказана оценка

Ща] < ¿[Г] • р[Г]1УагИ1 • | Уаг[Г]| + Л[Г], (5)

где ¿[Г] означает максимальную разность глубин неизвестных в системе Г, /о[Г] — максимальную ширину термов системы Г.

В случае, если в систему Г входят лишь нуль- и одноместные функциональные знаки, существует линейная оценка относительно данных параметров, Ца] < Х^еУаг[г] <УГ] + МП ^ I Уаг[Г]|-<5[Г] + /г[Г], где 5Х есть разность глубин вхождений неизвестной х (результат сообщен автору В.П. Оревковым).

Основные результаты

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

В разделах 1.2.1 и 1.3.1 доказывается, что дальнейшее улучшение оценки (4) путем устранения из неё неизвестных с нулевой разностью глубин невозможно. Эти же примеры доказывают невозможность исключения из суммирования оценки (3) членов, соответствующих неизвестным с нулевой разностью глубин. А именно, строятся

семейства примеров, для которых

h[a] > | Vari [Г] | • /i[Г]

т > Евд+мп,

<5^0

где Vari — совокупность неизвестных, имеющих вхождения разной глубины в систему Г. Также в разделе 1.2.1 доказывается невозможность улучшения оценки (5). В отличие от случая одноместных функциональных знаков, в общем случае зависимость высоты наиболее общего унификатора от разности глубин содержит экспоненциальный член.

В разделах 1.2.2 и 1.3.2 получены верхние оценки высоты наиболее общего унификатора системы пар термов относительно разности глубин и количества неизвестных, имеющих вхождения различной глубины, (неизвестных не типа сечения), соответственно. Полученная в разделе 1.3.1 нижняя оценка показывает, что верхняя оценка относительно количества неизвестных не типа сечения является достаточно точной. В разделе 1.4.1 получена нижняя оценка, показывающая невозможность дальнейшего улучшения верхней оценки раздела 1.3.2 для неизвестных с различными путями (определение дается в параграфе 1.4).

В главе 2 на основании верхней оценки относительно количества неизвестных не типа сечения строится верхняя оценка высоты термов в выводе в секвенциальном исчислении с сечениями по произвольным формулам. В случае, если глубины связанных вхождений предметных переменных в формулы сечения равны нулю, то полученная оценка совпадает с оценкой Оревкова (1). Для доказательства используется несколько модифицированная техника схем вывода с типами сечений.

Структура диссертации

Диссертация состоит из введения и двух глав, разделенных на 6 параграфов. Нумерация разд�