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

• Конев, Борис Юрьевич
• кандидат физико-математических наук
• 1998

Оглавление диссертации кандидат физико-математических наук Конев, Борис Юрьевич

Оглавление

Введение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Литература

Введение диссертации (часть автореферата) на тему «Оценки высоты термов в наиболее общем унификаторе»

Введение

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

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

В наиболее общем виде задача унификации является задачей, формулируемой следующим образом. По двум описаниям 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 параграфов. Нумерация разделов, формул, примеров, лемм и теорем ведется отдельно для каждой главы.

В первой главе строятся верхние и нижние оценки высоты наиболее общего унификатора системы пар термов.

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

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

В параграфе 1.2 строятся нижние и верхние оценки высоты наиболее общего унификатора относительно разности глубин неизвестных. Нижняя оценка доказывается путем построения семейства примеров, для которых высота наиболее общего унификатора велика относительно разностей глубин неизвестных, входящих в систему. Для доказательства верхней оценки используется замеченная в работах [2, 39] связь между унификаторами системы пар термов и отношениями эквивалентности на вершинах ориентированных ациклических мультиграфов, представляющих данные термы.

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

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

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

Основные результаты главы диссертации опубликованы в работах [3, 32, 4, 33].

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

Заключение диссертации по теме «Математическая логика, алгебра и теория чисел», Конев, Борис Юрьевич

Выводы в исчислениях КОЬ и ЮЬ представляются в форме деревьев с корнем. Каждая секвенция вывода либо является аксиомой, либо получается в результате применения одного из правил вывода к секвенциям, стоящим непосредственно над ней в дереве. Каждая секвенция в выводе, кроме самой нижней является посылкой некоторого применения правила вывода, заключение которого также принадлежит выводу. В вершины дерева, представляющего вывод помимо секвенций пишутся анализы аксиом и применений правил вывода. Анализ аксиомы содержит слово "аксиома" вместе с индексами главных вхождений. Анализ применения правила содержит название правила, по которому получена данная секвенция, и индекс главного вхождения, если главное вхождение определено для данного правила. Секвенция называется выводимой, если существует вывод, последней секвенцией которого является данная секвенция. Формула А называется выводимой, если выводима секвенция —» А.

Пример 2.1. Рассмотрим вывод формулы А Р (В Р А). Главные формулы аксиом и применений правил выделены подчеркиванием.

А-+ А, В р А, А Р (В Р А) [аксиома, - 1,1] А-+ В Р ДАР (В Р А) [-02,1] ->ВрА,Ар (В Р А) [-01,1] АР (В Р А) [~02,1]

Анализы аксиом и правил вывода мы пишем справа от секвенций в квадратных скобках. □

Схемой вывода называется последовательность анализов аксиом и правил вывода. Для систем КО; и ЮЬ схемы вывода записывают в виде деревьев с корнем. Анализы аксиом приписываются листьям, анализ /с-посылочного правила приписывается вершине, имеющей в точности к входящих дуг (к > 0).

Пример 2.2. Схемой вывода, приведенного в примере 2.1, является аксиома, —1,1] [-Ю2.1] Иэ 1,1] Ир 2,1]

Выводом в соответствии со схемой II называется любой вывод, для которого список анализов аксиом и правил вывода в точности совпадает с V. Высотой схемы II назовем высоту представляющего её дерева.

Рассмотрим произвольный вывод V в исчислении КСЬ (ЮЬ). Переменная а, участвующая в применении Ь одного из правил —> V или 3 —называется собственной переменной применения Ь. Терм участвующий в применении Ь одного из правил V —> или —> 3, называется собственным термом применения Ь.

Сформулируем в виде леммы доказанное в [37] свойство исчислений КСЬ и ЮЬ, которое нам понадобится в дальнейшем.

Лемма 2.1. Пусть V — некоторый список предметных переменных. Тогда произвольный вывод V можно перестроить путем переименования собственных переменных применений правил —>- V и 3 —в вывод V той же самой секвенции, в котором собственные переменные применений правил —У V и 3 —> не встречаются в списке V и не входят связано ни в одну формулу вывода.

2.2. Верхняя оценка высоты термов в выводе с сечениями в исчислении КСЬ и ЮЬ

Будем говорить, что формула А отобразима в формулу В, если формула В получается из А одновременным замещением свободных вхождений предметных переменных на некоторые термы, В = [А]^''"'^, при этом предполагается, что для всех г терм Т* свободен для XI в А.

Схемой вывода с типами сечений [37] называется схема вывода, в которой к анализу каждого применения правила сечения добавляется некоторая формула таким образом, чтобы каждая предметная переменная входила свободно в совокупность добавленных формул не более одного раза. Добавленные формулы называются типами анализов правил сечения. Рассмотрим секвенцию 5, список ¿1,. , ¿п попарно различных предметных переменных, схему вывода с типами сечений и и вывод V. Говорят, что V является (¿1,. , -выводом секвенции Б в соответствии со схемой и, если выполняются следующие условия.

1) Т> является выводом в соответствии со схемой, получаемой из II выкидыванием всех формул.

2) Типы анализов всех применений правил сечения в выводе Т> отобразимы в соответствующие боковые формулы сечений V. При этом, термы, участвующие в подстановке, называются собственными термами применения правила сечения.

3) Переменные ¿1,. , ¿п не входят свободно в типы анализов применений правил сечения в схеме и.

4) Переменные ¿1,. , Ьп не входят связанно в вывод V.

5) Существуют термы Т\,. ,Тп такие, что для всех г терм Т\ свободен для ^ в и последней секвенцией вывода V является

Г ¿п

Термы, участвующие в подстановке, преобразующей Б в последнюю секвенцию Т>, называются собственными термами вывода V.

Говорят, что схема вывода с типами сечений корректна, если существует какой-либо вывод в соответствии с этой схемой.

Вывод V называется универсальным (¿1,. ,£п)-выводом секвенции 5 в соответствии со схемой и, если V является (¿1,. , ¿п)-выводом секвенции Б в соответствии со схемой 17, и любой другой (¿1,. , ¿„)-вывод секвенции Б в соответствии со схемой 17 может быть получен из V заменой свободных вхождений предметных переменных на некоторые термы.

Для того чтобы получить оценку высоты термов в выводе, нам потребуется определить задачу унификации для системы пар термов с ограничениями (ОТ-системы) (подобные системы вводятся в работах [11, 37, 24, 35]). Термы такой системы строятся из функциональных знаков произвольной арности /ь . • • , и предметных переменных ¿1,. , ¿п, . , хр. ОТ-система Е состоит из трёх частей, Н = {Г; П; V}, первая — это обычная система пар термов г = тег)}1ь вторая — множество ограничений вида а У — множество предметных переменных, где являются термами, — предметная переменная, не принадлежащая V.

Отображение г из множества V в множество термов данного языка называется решением системы {Г;П; V}, если оно является унификатором Г и для всех у. 1 < у < М результат применения подстановки г к терму Щ не содержит х^. Таким образом, из множества предметных переменных выделяется подмножество V, элементы которого, с точки зрения задачи унификации, рассматриваются как неизвестные; остальные предметные переменные рассматриваются как функциональные константы. Решение <т системы {Г; П; V} называется универсальным решением, если а является наиболее общим унификатором Г (при этом все подстановки, участвующие в определении наиболее общего унификатора, являются отображениями из множества V в множество термов указанного языка). Очевидно, выполняется следующая лемма.

Лемма 2.2. Если некоторый унификатор Г удовлетворяет множеству ограничений П, то наиболее общий унификатор Г также удовлетворяет множеству ограничений П. То есть, если система

Г; П; V} имеет решение, то она имеет и универсальное решение.

Лемма 2.3. Каковы бы ни были корректная схема вывода с типами сечений II и секвенция Б, если существует (¿1,. , £п)-вывод V секвенции S в соответствии со схемой U, то существует универсальный (¿1,. ,tn)-вывод V* секвенции S в соответствии со схемой U, в котором для любого терма Т, являющегося собственным термом вывода V*, собственным термом правил —3 , V —У или собственным термом правила сечения, выполняется неравенство h[T} < ar[D]hl ■ (q-[D] + п) ■ hx + (q~[V] + n)-h2 + h0, где ar[D] — максимальная арность функциональных знаков, входящих в секвенцию Sue типы анализов правил сечения, hi — максимальная глубина свободных вхождений предметных переменных в типы анализов правил сечения, h2 — максимальная глубина вхождений ¿1,. ,tn в S и связанных вхождений переменных в секвенцию Sue типы анализов правил сечения, ho — максимальная высота термов, входящих в секвенцию Sue типы анализов правил сечений, q~ [D] — количество анализов применений правил —> 3 ; V —> в схеме U.

Доказательство. Пусть секвенция S и корректная схема вывода с типами сечений U в исчислении KGL или IGL удовлетворяют условиям леммы. Для того чтобы полностью восстановить (ii. , tn)-вывод секвенции S в соответствии со схемой £/, достаточно построить собственные термы доказательства, применений правил —> 3, V —>• и правил сечения, (см. [37]). Для этого мы построим ОТ-систему индукцией по высоте схемы таким образом, что решение данной системы даст значения всех собственных термов указанных правил. В случае, если высота схемы больше нуля, мы строим ОТ-систему так же, как и в [37], и меняем конструкцию для случая, когда высота схемы равна нулю.

Обозначим через П{5; ¿1,. ,tn} список всех выражений вида х tj, 1 < j < п, где х является предметной переменной, входящей в кванторный комплекс, в области действия которого находится некоторое свободное вхождение переменной ^ в секвенцию 5.

Не умаляя общности, все собственные переменные правил —>■ V и 3 —> попарно различны (по лемме 2.1, всегда можно перестроить вывод V таким образом, чтобы списки собственных переменных правил введения кванторов удовлетворяли этому требованию).

Схема вывода и представляет собой помеченное дерево. Применяя индукцию по высоте схемы, построим ОТ-систему £([/; . , ¿п) и пометим каждый узел этого дерева секвенцией. Обозначим полученное помеченное дерево V. Пусть V — множество неизвестных системы 5(^7; £',¿1,. , ¿п). Индукционное предположение состоит в том, что

1) вывод V, с точностью до переименования собственных переменных правил —)■ V и 3 —>-, получается применением к секвенциям, входящим в V, некоторого отображения г из множества V в множество термов. При этом предполагается, что все подставляемые термы свободны для подстановки;

2) подстановка г является решением ОТ-системы

Щи-, . ,£„);

3) Пусть подстановка а — универсальное решение ОТ-системы Н(?7; 5; ¿1,. ,£п). Тогда для каждого х € V терм а(х) свободен для х во всех секвенциях, в которые х входит свободно, и применение к секвенциям, входящим в V, подстановки а дает универсальный (¿1,. , ¿п)-вывод V* секвенции Б.

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

База индукции (высота схемы равна нулю). Тогда в схему входит единственный анализ, и это — анализ аксиомы; вывод V состоит из единственной секвенции

Ах, А, Д2 Аз, А, Д4, где А — явно указанная главная формула аксиомы (для исчисления ЮЬ списки формул Д3 и Д4 пусты). Пометим единственный узел дерева V секвенцией 5. Анализ аксиомы содержит индексы главных вхождений формулы А в антецедент и сукцедент, п\ и п2 соответственно. Рассмотрим формулы А\ и А2, входящие в антецедент и сукцедент секвенции 5 на позициях щ и п2 соответственно. По определению (¿1,. ,£п)-вывода и анализа аксиомы, формулы А\ и А2 отобразимы в формулу А.

Построим множество пар термов Г (А, Ах, А2) индукцией по построению формул А, Ах и А2.

• Если А — атомарная формула, формулы А\ и А2 также атомарные. Пусть

Ах = Р(ТЬ. ,Т5),

А2 - р(еь. ,©5), где Р — ¿-местный предикатный знак. Определим множество пар термов Г(А, Ах, А2) как {(Т*, Ог)}|=1

• Если формула А имеет А = -^А', формулы А\ и А2 имеют вид

Ах - -А'х, А2 = -^А!2.

Построим множество пар термов Г(А',А'1,А2) и положим Т(А,А1,А2)=Т(А',А'1,А'2).

• Если формула А имеет вид А = А' 0 А", где О является одной из пропозициональных связок &, V, I), формулы А\ и А2 имеют вид

- А[ © А", а2 =

Построим по индукции два множества Т(А,А'1,А'2) и Г(А, А",А2) и определим множество пар термов Г(А, Ах,А2) следующим образом: Г(А, Аъ А2) = Г (А', А[, А!2) и Г (А", А'/, А'2').

• Если формула А имеет вид А = С^х А', где — один из кванторов, то формулы А1 и А2 имеют вид

А\ = фсА^,

А2 = ф:А2.

Построим множество пар термов Г (А', А[, А2) и положим Г(А, Ах, А2) = Г(А', А[, А2).

Окончательно, мы определяем ОТ-систему £([/;£;¿1,. как {Г(А,АьА2);П{5;^,.

Как было отмечено выше, формулы Ах и А2 отобразимы в формулу А. Нетрудно видеть, что подстановка, отображающая секвенцию 5 в последнюю секвенцию вывода V, унифицирует полученную систему пар термов Г(А,Ах,А2). По определению (¿1,. , £п)-вывода, термы Т^ свободны для ¿г- в 5, что означает, что ограничения П{£; ¿1,. , ¿п} выполняются. Наиболее общий унификатор а множества пар термов Г(А, Ах, А2), по лемме 2.2, удовлетворяет множеству ограничений Tl{S;ti,. ,tn} и, как нетрудно видеть, это означает, что термы cr(ii),. , o-(tn) свободны для h,. , tn в секвенции S. Поскольку произвольный вывод V порождает некоторое решение ОТ-системы S(U; S; h,. , tn), универсальному выводу V* соответствует универсальное решение данной системы. Таким образом, индукционное предположение выполняется.

Индукционный переход (высота схемы больше нуля). Тогда вывод завершается применением какого-либо ¿-посылочного правила L {I — 1, 2). Обозначим через С7г- схему вывода, входящую в U над г-ой посылкой последнего анализа, и через £>г- вывод, входящий в Т> над г-ой посылкой последнего применения правила. Пометим корень дерева U секвенцией S. В зависимости от типа правила L, ОТ-система Е(£/; S; ti,. , tn) строится следующим образом.

• Предположим, что L является правилом введения пропозициональной связки. Поскольку секвенция S отобразима в последнюю секвенцию вывода V, можно построить секвенции Si,. Si, из которых S получается по правилу L. Заметим, что вывод T>i является (ti,. ,tn)~выводом секвенции Si- По индукционному предположению, существуют ОТ-системы E(Uf, Sf, t\,. ,tn) = {Г^; Пг-, Vi} и пометка соответствующих поддеревьев U\,. ,Ui, для которых выполняются свойства 1)—3). Не умаляя общности, множества неизвестных V\,. , Ц не содержат общих переменных помимо . ,tn.

Определим ОТ-систему S(U; S] t\,. , tn) как {Гх U Г/; Пх U П; U П{5'; ti,. , tn}; ViUVi}. Соображения, аналогичные тем, что мы приводили в доказательстве базы индукции, показывают, что индукционное предположение выполняется.

• Предположим, что Ь является правилом сечения, тогда оно имеет две посылки. Рассмотрим А — тип последнего анализа схемы и и множество V предметных переменных, входящих свободно в формулу А. Поскольку секвенция 5 отобра-зима в последнюю секвенцию вывода V и формула А отобра-зима в боковую формулу применения Ь правила сечения, можно построить секвенции 51 и 52 , из которых 5 получается по правилу сечения с формулой А в качестве боковой формулы. Тогда, вывод Т>г является (¿1,. , ¿п, У)-выводом секвенции 5* (список ¿1,. ,гп,У следует понимать как объединение списка всех неизвестных, входящих в множество V, и списка ¿1,. , ¿п). По индукционному предположению, существуют ОТ-системы

5^; ¿1,. , ¿п, У) = {ГУ, П^; Уг}, и пометка соответствующих поддеревьев 111,1/2, для которых выполняются свойства 1)-3). Не умаляя общности, множества неизвестных VI, У2 не содержат общих неизвестных помимо . . . , ¿п, V .

Определим ОТ-систему 5(С/; 5; ¿1,. , ¿п) как {Г1 и Г2; Щ и П2 и П{5; ¿1,. , ¿п}; VI и и У}. Ясно, что индукционное предположение выполняется.

• Предположим, что Ь является правилом —>• V или 3 —к Тогда оно однопосылочное, 1 = 1. Рассмотрим предметную переменную Ь, не встречающуюся в 5 и отличную от ¿1,. , ¿п. Поскольку секвенция 5 отобразима в последнюю секвенцию вывода V, можно построить секвенцию 51, из которой 5 получается по правилу Ь и для которой Ь является собственной переменной. Заменим в выводе Т>\ все свободные вхождения собственной переменной последнего применения правила вывода Т> на Ъ. Ясно, что полученный вывод Р[ является (¿1,. , ¿п)-выводом секвенции ¿>х. По индукционному предположению, существует ОТ-система 5(С/х; 5х; £х,• • • ,£п) = {Гх; П1? У\} и пометка поддерева иъ для которых выполняются свойства 1)-3). В качестве ОТ-системы Н(£7; ¿г, ¿х, • • • , £п) мы берем

Гх; Пх и П{5; ¿х, . . , 1п} и {6 £ . , 6 £ *<р}; К}, где ^,. иг — список тех предметных переменных из ¿х, • • • , ¿п> которые входят свободно в 5. Дополнительные ограничения обеспечивают, что ъ не входит в заключение применения ь. Нетрудно видеть, что индукционное предположение выполняется.

• Предположим, что Ь является правилом V или 3. Тогда оно однопосылочное, 1 = 1. Пусть предметная переменная £ не входит в 5 и отлична от ¿1,. , ¿п. Поскольку секвенция 5 отобразима в последнюю секвенцию вывода V, можно построить секвенцию 5х, из которой 5 получается по правилу Ь, причем £ является собственным термом правила X. Заметим, что вывод £>х является (¿1?. £)-выводом секвенции 5х- По индукционному предположению, существует ОТ-система 5(£/х; ^ь ¿ъ ■ • • > ¿п) — {Гх; Пх, Ух}, и пометка дерева £/х, для которых выполняются свойства 1)-3). В качестве ОТ-системы Н(17; 5; ¿1,. , £п) мы берем ОТ-систему {Гх;Пх и П{5; ¿1,. , ¿п}; . , ¿п, £}. Нетрудно видеть, что индукционное предположение выполняется.

Таким образом, нами построена ОТ-система Н(?У; ¿>; ¿х,. , такая, что список собственных термов вывода , а также собственных термов применений правил сечения, правил —> 3 и V —»• является её решением, и универсальное решение ОТ-системы Н(^7;5;£х,. , £п) порождает универсальный (¿х, • • • ,£п)-вывод 2)* секвенции 5 в соответствии со схемой и.

Если схема и содержит анализы применений правил V —» и —> 3, а также правил сечения, ОТ-система 5(С7; 5; ¿1,. , £п) помимо неизвестных ¿1,. , ¿п может содержать дополнительные неизвестные. Нетрудно видеть, что если некоторая неизвестная была добавлена при рассмотрении правила сечения, она имеет не более двух вхождений в систему пар термов Г, причем глубины этих вхождений совпадают. Таким образом, все неизвестные, добавленные при рассмотрении правил сечения, являются неизвестными типа сечения. Не умаляя общности, можно считать, что остальные неизвестные ОТ-системы Е(1/; 5; ¿1,. , ¿п) являются неизвестными не типа сечения. В самом деле, либо разность глубин множества пар термов ОТ-системы Б(11; 5; ¿1,. , 1п) равна нулю, тогда, по теореме 1.2, оценка леммы 2.3 выполнена, либо для каждой неизвестной х помимо неизвестных, введенных при рассмотрении правил сечения, в систему всегда можно добавить уравнение вида /(/(• • • /(%)) = /(/(• • • 1{х)) я я таким образом, чтобы разность глубин неизвестной х была ненулевой, не изменив при этом значений ко, к\ и к2.

Общее количество неизвестных не типа сечения равняется п + Я~\Р\- Таким образом, мы можем воспользоваться оценкой теоремы 1.4, чтобы получить оценку высоты универсального решения ОТ-системы £(£/; 5; ¿1,. , ¿п). □

Теорема 2.1. Пусть V является выводом секвенции Э в исчислении КСЬ (или ЮЬ). Тогда, заменяя некоторые свободные термы на предметные переменные, можно преобразовать вывод Т> в вывод V* той же самой секвенции Б в исчислении КйЬ (или ЮЬ, соответственно), обладающий следующим свойством. Высота собственных термов применений правил —У 3 и V —в выводе Т>*, а также высота термов, входящих свободно в боковые формулы применений правила сечения в выводе V*, не превосходит ar[£>f• q~[V] • 5C[D] + q'[V] ■ max{Jc[S], 5C[V}} + max{h[S], S°[V]}, где гх\р\ — максимальная арность функциональных знаков, входящих в секвенцию Sue боковые формулы применений правил сечения, 8C[D] — максимальная глубина связанных вхождений предметных переменных в боковые формулы применений правил сечения, ^[S*] — максимальная глубина связанных вхождений предметных переменных в S, /i[5] — максимальная высота термов, входящих в секвенцию S, q~[D] — количество анализов применений правил —3 , V —> в схеме U.

Доказательство. Мы доказываем теорему, основываясь на оценке леммы 2.3, тем же способом, каким в [37] аналогичная теорема следует из оценки на высоту (¿1,. , ¿п)-вывода. Для произвольной формулы А определим формулу А* такую, что

• А* не содержит функциональных констант;

• каждая предметная переменная входит свободно в формулу А* не более одного раза;

• если некоторый терм входит в формулу А* свободно, то этот терм является предметной переменной;

• формула А* отобразима в формулу А.

В [37] формула А* называется q*-типом формулы А. Построим по выводу V его схему U и допишем в схеме U ко всем применениям правил сечения д*-типы их боковых формул, переименовывая, если необходимо, предметные переменные, входящие свободно в типы анализов формул сечения так, чтобы типы не имели общих переменных.

Обозначим полученную схему вывода с типами сечений 17*. Ясно, что V является ()-выводом секвенции Б в соответствии со схемой и*. Из определения д*-типа формулы следует, что максимум глубин свободных вхождений предметных переменных в формулу А* не превосходит максимума глубин связанных вхождений предметных переменных в формулу А*. Применим оценку леммы 2.3 для завершения доказательства теоремы. □

Замечание 2.2. В случае, если сечения осуществляются по формулам, не содержащим связанных вхождений переменных ненулевой глубины, полученная оценка совпадает с оценкой (1) Оревкова [37], стр. 8.

Список литературы диссертационного исследования кандидат физико-математических наук Конев, Борис Юрьевич, 1998 год

Литература

1. Божич Е.С. Об арифметике с понятием "достижимого числа" // Изв. АН СССР. Сер. мат. — 1986. — Т. 50, № 6. — С. 1123-1155.

2. Давыдов Г.В., Маслов С.Ю., Минц Г.Е., Оревков В.П., Слисен-ко А.О. Машинный алгоритм установления выводимости на основе обратного метода // Зап. научн. сем. ЛОМИ. — 1969. — Т. 16. — С. 8-15.

3. Конев Б.Ю. Уточнение оценок высоты термов в наиболее общем унификаторе // Зап. научн. сем. ПОМИ. — 1997. — Т. 241. — С. 117-134.

4. Конев Б.Ю. Нижняя оценка на высоту термов в наиболее общем унификаторе: Препринт ПОМИ 21/1998. — 1998. — 8 с. — С.-Петербургское отделение математического института им. В.А. Стеклова. — Доступен по http://www.pdmi.ras.ru/preprint/1998/index.html.

5. Маканин Г.С. Проблемы разрешимости уравнений в свободной полугруппе // Мат. сб. — 1977. — Т. 103, № 2. — С. 147-236.

6. Оревков В.П. Нижние оценки увеличения сложности выводов после устранения сечений // Зап. научн. сем. ЛОМИ. — 1979. — Т. 88. — С. 137-162.

7. Оревков В.П. Алгоритм Британского музея может быть эффективнее метода резолюций // Ли Р., Чень Ч. Математическая логика и автоматическое доказательство теорем. — М.: Наука, 1983. — Приложение Б. — С. 314-325.

-968. Оревков В.П. Верхние оценки удлинения выводов при устранении сечений // Зап. научн. сем. ЛОМИ. — 1984. — Т. 137. — С. 87-98.

9. Оревков В.П. Восстановление доказательства по его схеме // Докл. АН СССР. — 1987. — Т. 293, № 2. — С. 313-316.

10. Оревков В.П. Одна оценка сложности термов в доказательствах // Семиотические аспекты формализации интеллектуальной деятельности: Тезисы докладов и сообщений / Всесоюзная школа-семинар "Боржоми-88". — Москва, 1988. — № 17. — С. 108-110.

11. Оревков В. П. Системы уравнений в термах с подстановками //В сб.: Вопросы кибернетики / Сложность вычислений и прикладная математическая логика. — М.: Наука, 1998. — С. 127-148.

12. Оревков В.П. Схемы доказательств в аксиоматических теориях гильбертовского типа // Зап. научн. сем. ЛОМИ. — 1988. — Т. 176. — С. 132-146.

13. Baxter L.D. An efficient unification algorithm: Report cs-77-23. — 1973. — University of Waterloo, Department of Analysis and Computer Science.

14. Bidoit M., Corbin J. A rehabilitation of robinson's unification algorithm // Information Processing. — North Holland, 1983. — Vol. 83. — P. 909-914.

15. Dantsin E., Voronkov A. Bag and set unification: Technical Report 150. — 1997. — Uppsala University, Computing Science Department.

16. Davis M. Eliminating the irrelevant from mechanical proofs // Symposia of Applied Math. — 1963. — Vol. 25.

17. Davis M. The Undecidable. Basic papers on undecidable propositions, unsolvable problems and computable functions. — New York, Raven Press, 1965.

18. Davis M., Logemann G., Loveland D. A machine program for theorem-proving // Comm. ACM. — 1962. — Vol. 5. — P. 394397.

19. Davis M., Putnam H. A computing procedure for quantification theory //J. Assoc. Comp. Mach. — 1960. — Vol. 7. — P. 201-215.

20. Dwork C., Kanellakis P., Mitchel J. On the sequential nature of unification //J. Logic Programming. — 1984. — Vol. 1. — P. 35-50.

21. Dwork C., Kanellakis P., Stockmeyer L. Parallel algorithms for term matching // SIAM J. Computing. — 1988. — Vol. 17, № 4. — P. 711731.

22. Escalada G., Ghallab M. A practically efficient and almost linear unification algorithm // Artificial Intelligence.— 1988. — Vol. 36, № 2. — P.249-263.

23. Farmer W.M. Length of proofs and unification theory: PhD dissertation. — Univ. of Wisconsin—Madison, 1984.

24. Farmer W.M. A unification-theoretic method for investigating the k-provability problem // Annals of Pure and Applied Logic. — 1991. — Vol. 51. — P. 173-214.

25. Friedman H. One hundred and two problems in mathematical logic // J. Symb. Logic. — 1975. — Vol. 40, № 2. — P. 131-174.

26. Gentzen G. Untersuchungen über das logische Schließen // Mathematische Zeitschrift. — 1934. — Vol. 39. — P. 176-210, 405433.

27. Herbrand J. Recherches sur la théorie de la démonstration: Thesis // Logical writings. — Cambridge, 1977. — W. Goldfarb, editor.

28. Huet G.P. Résolution d'équations dans des langage d'ordre 1, 2,... , w: Thèse d'état. — Université de Paris VII, 1976.

29. Ranger C. A simplified proof method for elementary logic // Computer Programming and Formal Systems / Studies in Logic and Foundations of Mathematics. — North-Holland. — 1963. — P. 87-93.

30. Kapur D., Krishnamoorthy M.S., Narendran P. A new linear algorithm for unification: Internal Report № 82CRD-100. — 1982. — General Electric, New York.

31. Knight K. Unification: a multidisciplinary survey // ACM Comput. Surveys. — 1989. — Vol. 21. — P. 93-124.

32. Konev B. Upper bound on the height of terms in proofs with cuts: PDMI Preprint 17/1998. — 1998. — 8 p. — Steklov Institute of Mathematics at St.Petersburg. — Доступен no http ://www.pdmi.ras.ru/preprint/1998/index.html.

33. Konev B. Upper bound on the height of terms in proofs with cuts // Proceedings of First-order Theorem Proving—FTP'98 / 2nd International Workshop on First-order Theorem Proving, Vienna, Austria: Technical Report E1852-GS-981, Technische Universität Wien. — 1998. — P. 162-172.

-9934. Krajicek J. Generalizations of proofs // Proc. 5th Easter Conf. on Model Theory. — Seminarber, 1987. — Vol. 93. — P. 82-99. — Berlin, Sekt. Math.

35. Krajicek J., Pudlak P. The number of proof lines and size of proofs in first logic // Arch. Math. Logic. — 1988. — Vol. 27. — P. 69-84.

36. Martelli A., Montanary U. An efficient unification algorithm // ACM transactions on Programming Languages and Systems. — 1982. — Vol. 4, № 2. — P. 258-282.

37. Orevkov V.P. Complexity of Proofs and Their Transformations an Axiomatic Theories / American Mathematical Society. — 1991. — (Translations of Mathematical Monographs).

38. Parikh R.J. Some results on the length of proofs // Trans. Amer. Math. Soc. — 1973. — Vol. 117. — P. 29-36.

39. Paterson M.S., Wegman M.N. Linear unification // Journal of computer and system science. — 1978. — Vol. 16, № 2. — P. 158-167.

40. Plotkin G. Building in equational theories // Machine Intelligence. — 1972. — Vol. 7. — P. 73-90.

41. Prawitz D. An improved proof procerure // Theoria. — 1960. — Vol. 26. — P.102-139.

42. Robinson J.A. A machine oriented logic based on the resolution principle //J. Assoc. Comput. Mach. — 1965. — Vol. 12, № 1. — P. 23-41.

43. Siekmann J.H. Unification theory //J. Symbolic Computation. — 1989. — Vol. 7. — P. 207-274.

44. Statman R. Bounds for proof-search and speed-up in the predicate calculus // Ann. Math. Logic. — 1978. — Vol. 15, № 3. — R 225-287.

45. Venturini-Zilli M. Complexity of the unification algorithm for first order expressions // Calcolo. — 1975. — Vol. 12, № 4. — P. 361-371.