Доказательство свойств функциональных программ методом насыщения равенствами тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат наук Гречаник Сергей Александрович

• Гречаник Сергей Александрович
• кандидат наук
• 2018

Оглавление диссертации кандидат наук Гречаник Сергей Александрович

Цели и задачи работы

Научная новизна работы

Практическая значимость работы

Апробация работы и публикации

1 Смежные работы

1.1 Обзор смежных работ

1.1.1 Система преобразования Бёрстолла-Дарлингтона

1.1.2 Насыщение равенствами

1.1.3 Переписывание графов и джунгли

1.1.4 Пруверы первого порядка

1.1.5 Индуктивные пруверы

1.1.6 Суперкомпиляция

1.2 Выводы

2 Основная идея метода: полипрограммы и преобразования над ними

2.1 Используемые обозначения

2.2 Синтаксис

2.3 Семантика

2.3.1 Формальная постановка задачи

2.4 Правила преобразования полипрограмм

2.5 Слияние по бисимуляции

2.6 Обобщения

2.7 Выводы

53

3 Расчленённая форма и бесточечное представление полипро-

грамм

3.1 Расчленённая форма

3.2 Бесточечное представление полипрограмм

3.2.1 Перестановки параметров

3.2.2 Полипрограмма в бесточечно-расчленённом представлении

3.2.3 Семантика бесточечно-расчленённого представления

3.3 Каноническая форма определений

3.4 Категория полипрограмм

3.5 Неоднозначность применения правил

3.6 Выводы

4 Локальные правила преобразования

4.1 Упрощающие правила

4.1.1 Транзитивность

4.1.2 Удаление дубликатов

4.1.3 Дублирование определения

4.1.4 Симметричность равенства

4.1.5 Рефлексивность равенства

4.1.6 Понижение арности

4.1.7 Преобразование вызова в перестановку параметров

4.1.8 Насыщение по коммутативности

4.1.9 Инъективность конструкторов

4.1.10 Инъективность сопоставления с образцом

4.1.11 Редукция вызова тождественной функции

4.1.12 Редукция сопоставления с образцом

4.1.13 Сопоставление с образцом незнакомого конструктора

4.2 Конгруэнтность

4.3 Завершаемость упрощающих правил

4.4 Насыщающие правила

4.4.1 Редукция вызова функции

4.4.2 Преобразования сопоставлений с образцом

4.4.3 Применение насыщающих правил

4.5 Выводы

117

5 Слияние по бисимуляции

5.1 Понятие бисимуляции полипрограмм

5.2 Описание алгоритма слияния по бисимуляции

5.2.1 Частичные перестановки параметров

5.2.2 Дополнение перестановками параметров и обоснование факта бисимуляции

5.3 Обеспечение единственности модели

5.3.1 Выражение защищённой рекурсии через структурную

5.3.2 Достаточное условие структурной рекурсии

5.3.3 Доказательство единственности модели

5.4 Выводы

6 Реализация и экспериментальные результаты

6.1 Практическая реализация прувера

6.1.1 Представление полипрограммы

6.1.2 Процесс насыщения полипрограммы

6.1.3 Процесс слияния по бисимуляции

6.2 Результаты сравнения с другими пруверами

6.2.1 Набор примеров

6.2.2 Сравниваемые инструменты

6.2.3 Результаты

6.2.4 Эксперименты с Graphsc

6.2.5 Эффективность полипрограмм по сравнению с прямым представлением

6.3 Выводы

Заключение

Список литературы

А Дополнительные примеры

Б Доказательства некоторых утверждений

О Дополнительные экспериментальные результаты

Введение

Объект исследования и актуальность работы

Одним из декларируемых преимуществ функциональных языков программирования является простота преобразований, а также формулирования и доказательства свойств программ, что достигается главным образом за счёт отсутствия побочных эффектов или более явного контроля за ними. Например, если мы знаем, что (щ) = д(Щ) для каких-то функций / и д, то мы всегда можем заменить /(ёЦ) на д(ё1) и наоборот в любом месте программы, сохранив при этом её семантику (в императивном языке подобные свойства сформулировать сложнее, т.к. функции могут не только возвращать значения, но и производить побочные эффекты, а также не только использовать свои аргументы, но и читать данные из изменяемой памяти).

Среди функциональных языков программирования наилучшим образом для выявления и доказательства равенств подходят тотальные языки [83], поскольку в них выполняется больше равенств. В тотальных языках все функции тотальны, т.е. определены для всех возможных значений параметров (подходящих по типу), в частности невозможно зацикливание, а значит они не могут быть тьюринг-полными. Такие языки, однако, меньше используются на практике для обычного программирования. Среди оставшихся (нетотальных) функциональных языков можно выделить два класса: строгие языки и нестрогие языки. В строгих языках все определённые пользователем функции являются строгими, то есть значение выражения вызова функции /(а, Ь, с) не определено (зацикливается), если значение хотя бы одного из аргументов а, Ь или с не определено. Операционный смысл строгости состоит в том, что значения аргументов вычисляются перед вызовом функции.

Большинство языков являются строгими, однако такая семантика вызовов функций считается менее удобной для анализа и преобразования программ. В нестрогих же языках функции по умолчанию нестрогие. При вызове нестрогой функции даже если среди аргументов есть такой, что его вычисление зацикливается, значение всего вызова f (а, b, с) может быть определено, если этот аргумент не используется (простейший пример — константная функция f (х) = С). Обычно это реализуется при помощи вычислений по необходимости (ленивых вычислений). Примером нестрогого языка является Haskell. Нестрогие языки считаются более удобными для анализа и преобразования, поэтому в данной диссертации в качестве входного языка был выбран нестрогий функциональный язык первого порядка.

Среди задач доказательства свойств программ выделим задачу доказательство эквивалентности функций программ, то есть утверждений, имеющих вид Vxlf (xi) = g(xi). Данная задача имеет следующие применения:

• Верификация: многие желательные свойства функций над алгебраическими структурами данных можно сформулировать в таком виде. Широко известным примером являются законы, которые должны выполняться (хотя это и не проверяется в настоящее время компилятором GHC) для реализаций различных классов типов в языке Haskell, таких, как монады, аппликативные функторы и многие другие [84].

• Преобразование программ (в частности, оптимизация): равенства такого вида можно использовать как правила переписывания, например, в GHC, компиляторе языка Haskell, существует возможность использовать правила переписывания, задаваемые пользователем [38].

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

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

Среди методов решения данной задачи отметим такой класс методов, которые применимы не только непосредственно к задаче доказательства эквивалентности, но и к задаче преобразования программ, например, с целью

оптимизации или анализа для выявления и доказательства свойств другого вида. Одним из таких методов является суперкомпиляция [82]. Суперкомпиляция состоит в построении программы, эквивалентной исходной (иногда в некотором слабом смысле, например, на общей области определения) при помощи правил переписывания (прогонка, обобщение) в сочетании со свёрткой (подробнее суперкомпиляция будет рассмотрена в Разделе 1.1.6). Часто суперкомпиляция рассматривается как метод оптимизации, однако суперкомпиляцию можно использовать и для других задач, в частности для доказательства эквивалентности (например, для этого можно сравнить на синтаксическое совпадение результат суперкомпиляции левой и правой частей [45; 49]). Одно из направлений развития суперкомпиляции — многорезультатная суперкомпиляция, позволяющая строить не одну программу, а целое множество различных программ, эквивалентных исходной [44]. Это позволяет использовать вместо эвристик, управляющих процессом переписывания, более точные метода выбора подходящей программы, работающие уже после суперкомпиляции и имеющие в своём распоряжении уже полностью построенные программы (например, в этом случае для выбора наиболее быстрой программы можно просто измерить производительность всех полученных программ).

Ещё один метод, применимый как к задаче доказательства эквивалентности, так и к задаче преобразования программ — насыщение равенствами (equality saturation). Насыщения равенствами — метод преобразования программ, заключающийся в применении преобразований к структуре данных, представляющей не одну программу, а целое множество семантически эквивалентных программ. Сам термин был введён в работе "Equality Saturation: A New Approach to Optimization" Тейта и других [21], где этот метод использовался для преобразования императивных программ, хотя схожие идеи применялись и задолго до этого. В насыщении равенствами каждое преобразование применяется недеструктивно, то есть исходная программа остаётся во множестве, и ко множеству добавляется новая преобразованная программа. При этом потребление памяти уменьшается за счёт совмещения общих частей программ. В итоге строится множество всех возможных программ, полученных из исходной применением преобразований в различном порядке. После этого из построенного множества выделяется одна наилучшая программа, если целью было преобразование программы. Если же целью было доказательство эквивалентности, то построение одной программы не требу-

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

Таким образом, насыщение равенствами и многорезультатная суперкомпиляцию имеют одинаковую мотивацию, однако использование структуры данных для компактного представления множества программ является характерной чертой насыщения равенствами, но совершенно не обязательно для многорезультатной суперкомпиляции. И хотя в предшествующих работах по многорезультатной суперкомпиляции использовались некоторые приёмы для оптимизации использования памяти [26; 43], они уступали в этом смысле насыщению равенствами. С другой стороны, насыщение равенствами применялось для императивных языков, но не для функциональных в то время, как суперкомпиляция в первую очередь предназначена для функциональных языков. Поэтому представляется актуальным исследование применения комбинации методов насыщения равенствами и многорезультатной суперкомпиляции к задачам выявления и доказательства свойств программ на функциональных языках (главным образом к задачам доказательства эквивалентности).

Цели и задачи работы

Цель работы — исследовать возможность применения комбинации методов насыщения равенствами и многорезультатной суперкомпиляции для выявления и доказательства свойств программ на нестрогом функциональном языке первого порядка.

Были поставлены следующие задачи:

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

• На основе методов насыщения равенствами и суперкомпиляции разработать метод преобразования компактного представления множеств функциональных программ.

• На основе метода преобразования разработать метод доказательства эквивалентности функций, включающий в себя в том числе доказательство по индукции и коиндукции.

• Реализовать разработанный метод в экспериментальном средстве доказательства эквивалентности и протестировать его на наборе модельных задач.

Научная новизна работы

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

В [21] для представления множеств программ используется структура данных называемая E-PEG (PEG расшифровывается как Program Expression Graph), основанная на Е-графах (графах, вершины которого разбиты на классы эквивалентности). В данной диссертации для представления множества функциональных программ мы вводим понятие полипрограммы, которое аналогично E-PEG, но концептуально проще: неформально полипрограмма — это программа, в которой разрешены множественные определения одной и той же функции. Главное содержательное отличие состоит в том, что в полипрограмме работа ведётся с функциями со своими собственными входными параметрами, в то время как в E-PEG работа идёт со значениями (точнее, с массивами значений для представления результата работы циклов), а входные параметры являются общими для всего E-PEG.

Кроме того, мы исключаем дублирование в полипрограмме функций, отличающихся только порядком аргументов, что делается впервые в рамках работы со структурами, подобными Е-графам (самый близкий из предшествующих результатов — исключение дублирования вершин, обозначающих

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

значения, отличающиеся некоторым целочисленным смещением [56]).

Мы также вводим специальное преобразование, которое называем слиянием по бисимуляции, работающее как доказательство равенств по индукции или коиндукции. Его предшественником можно считать специализированную версию слияния по конгруэнтности, способную сливать одинаковые циклы, реализованную в системе насыщения равенствами Peggy, созданной в рамках оригинальных работ по насыщению равенствами, однако она менее мощная и не упоминается в публикациях. Слияние по бисимуляции играет роль аналогичную выявлению, доказательству и применению лемм в многоуровневой суперкомпиляции [46], однако для обеспечения корректности в данной диссертации используются признаки структурной и защищённой рекурсии вместо теории улучшения Сэндса.

Практическая значимость работы

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

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

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

Апробация работы и публикации

По результатам работы были сделаны доклады на следующих семинарах и конференциях:

1. Международный семинар "Third International Valentin Turchin Workshop on Metacomputation", Россия, Переславль-Залесский, 5-9 июля

2. Международная конференция памяти Андрея Ершова "Ershov Informatics Conference", Россия, Санкт-Петербург, 24-27 июня

3. Международный семинар "Fourth International Valentin Turchin Workshop on Metacomputation", Россия, Переславль-Залесский, 29 июня - 3 июля

4. Семинар ИПС им. А.К. Айламазяна под рук. член-корр. С.М. Абрамова, 20 мая

5. Международный семинар "Fifth International Valentin Turchin Workshop on Metacomputation", Россия, Переславль-Залесский, 27 июня - 1 июля

6. Семинар "Теоретические проблемы программирования" под рук. д.ф.-м.н. В.А. Захарова, ВМиК МГУ, 11 ноября

7. Семинар "Теоретическое и экспериментальное программирование" под рук. к.ф.-м.н. В.А. Непомнящего, ИСИ СО РАН, 22 ноября

8. Семинар "Системное программирование" под рук. к.ф.-м.н. М.А. Бу-льонкова и д.ф.-м.н. А.Г. Марчука, ИСИ СО РАН, 24 ноября

9. Семинар группы "Технологии программирования" под рук. д.ф.-м.н. А.К. Петренко, ИСП РАН, 16 марта

Также были опубликованы следующие статьи, включая две в научных журналах из списка ВАК:

1. Grechanik S. A. Overgraph Representation for Multi-Result Supercompilation // Proceedings of the Third International Valentin Turchin Workshop on Metacomputation / ed. by A. Klimov, S. Romanenko. Pereslavl-Zalessky, Russia : Pereslavl-Zalessky: Ailamazyan University of Pereslavl, July 2012. Pp. 48-65. ISBN 978-5-901795-28-6. URL: http://pat.keldysh.ru/ ~grechanik/doc/overgraph.pdf

2. Grechanik S. A. Supercompilation by Hypergraph Transformation: Preprint / Keldysh Institute of Applied Mathematics. 2013. 24 pp. No

URL: http://library.keldysh.ru/preprint.asp?id=2013-26&lg=e

3. Grechanik S. A. Inductive Prover Based on Equality Saturation for a Lazy Functional Language // Perspectives of System Informatics: 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014. Revised Selected Papers. Vol. 8974 / ed. by A. Voronkov, I. Virbitskaite. Springer, 2014. Pp. 127-141. (Lecture Notes in Computer Science). ISBN 978-3-662-46822-7. URL: http://dx.doi.org/10.1007/

4. Grechanik S. Inductive Prover Based on Equality Saturation (Extended Version) // Proceedings of the Fourth International Valentin Turchin Workshop on Metacomputation / ed. by A. Klimov, S. Romanenko. Pereslavl-Zalessky, Russia : Pereslavl Zalessky: Publishing House "University of Pereslavl", July 2014. Pp. 26-53. ISBN

5. (ВАК) Гречаник С. А. Доказательство свойств функциональных программ методом насыщения равенствами // Программирование. 2015. № 3. с. 44—61

6. Grechanik S. A. Proving properties of functional programs by equality saturation // Programming and Computer Software. 2015. Vol. 41, no. 3. Pp.149-161. URL: http://dx.doi.org/10.1134/S0361768815030056

7. (ВАК) Гречаник С. А. Полипрограммы как представление множеств функциональных программ и преобразования над ними // Препринты ИПМ им. М.В.Келдыша. 2017. № 5. DOI: 10.20948/prepr-2017-5. URL: http://library.keldysh.ru/preprint.asp?id=2017-5

Глава

Введение диссертации (часть автореферата) на тему «Доказательство свойств функциональных программ методом насыщения равенствами»

Смежные работы

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

1.1 Обзор смежных работ

1.1.1 Система преобразования Бёрстолла-Дарлингтона

Многие методы преобразования программ можно рассматривать в качестве частных случаев общей схемы преобразования программ Бёрстолла и Дарлингтона [10] (в том числе насыщение равенствами, суперкомпиляцию и наш метод). Данная схема состоит в том, что программа рассматривается как набор уравнений, после чего при помощи некоторых преобразований данный набор уравнений пополняется новыми уравнениями, и в результате какое-то подмножество этих новых уравнений можно рассматривать как новую программу. Среди преобразований можно отметить следующие три:

• Раскрытие (unfolding) — подстановка тела функции (правой части) вместо вызова функции.

• Свёртка (folding) — обратная операция, подстановка вызова функции вместо тела.

• Переопределение (redefinition) — замена одной функции на другую, если обе функции определяются двумя одинаковыми с точностью до переименования функций подмножествами уравнений. Это преобразование мало изучено в оригинальной работе, однако оно перечислено здесь, потому что соответствует важному преобразованию слияния по биси-муляции из нашего метода.

Схема Бёрстолла и Дарлингтона очень общая, она допускает различные стратегии применения правил и оставляет открытым вопрос о корректности преобразований. Как будет видно в Главе 2, наш метод очень близок к данной схеме, однако мы явно вводим отдельное понятие полипрограммы для множества уравнений, и явно вводим семантику для полипрограмм. Это позволяет нам разобраться с корректностью преобразований, особенно с тонким вопросом корректности слияния по бисимуляции. Кроме того, на уровне реализации и формальной работы с полипрограммами мы вводим ограничения на вид определений, что сближает наш метод с насыщением равенствами.

1.1.2 Насыщение равенствами

Насыщение равенствами — термин, введённый в работе "Equality Saturation: A New Approach to Optimization" Тейта и других [21], где этот метод использовался для преобразования императивных программ. Представленный в этой работе оптимизатор называется Peggy. Суть метода насыщения равенствами заключается в использовании структуры данных, компактно представляющей не одну программу, а целое множество программ. В [21] эта структура данных называется E-PEG, PEG расшифровывается как Program Expression Graph. E-PEG основана на понятии Е-графа — графа, вершины которого разбиты на классы эквивалентности (буква Е от equality). Е-графы и подобные им структуры данных эффективно представляют множества равенств над термами (например, как на Рис. 1.1). Они используются в средствах доказательства теорем, в частности для анализа и доказательства свойств программ [15; 20]. Обычно Е-графы применяются в сочетании с алгоритмом конгруэнтного замыкания [55], позволяющим поддерживать представляемое Е-графом множество равенств замкнутым относительно аксиомы монотонности (a,i = bi ^ f (щ) = f (bi) для всех функциональных символов f) — данный алгоритм собственно является решателем для теории неинтерпрети-

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

Рис. 1.1 Е-граф, представляющий множество равенств над термами, а именно Ъ + (с + ¿) = (Ъ + с) + d и а + (Ъ + (с + ¿)) = а + ((Ъ + с) + ¿). Первое равенство изображено пунктирной линией, соединяющей две вершины, находящиеся в одном классе эквивалентности. Второе равенство является следствием первого по аксиоме монотонности. На рисунке можно видеть, как обеспечивается компактность представления за счёт обобществления общих подтермов (а именно вершин Ь, с, и ¿) и обобществления общего подтерма "с дыркой", а именно а + _. Последнее возможно только для эквивалентных выражений, поэтому является особенностью Е-графа (обобществление подтермов без дырок осуществляется и в обычных графах, представляющих термы).

Кроме задачи доказательства эквивалентности Е-графы могут быть использованы для других задач, например, для оптимизации программ. Данное применение основано на том, что при помощи Е-графа можно компактно представить множество эквивалентных программ (например, можно считать, что Е-граф на Рис. 1.1 представляет множество термов {a+(b+(c+d)), a+((b+ с) + d)}). Компактность представления осуществляется за счёт объединения общих подвыражений (sharing). При этом над Е-графом можно осуществлять различные преобразования, что даёт эффект одновременного преобразования всего множества программ. Данный подход применяется, например, в супероптимизаторе Denali [39] для поиска оптимальной последовательности инструкций для выполнения небольших программ.

В уже упомянутой работе [21] этот подход под названием насыщение равенствами был использован для оптимизации императивных программ, а кроме того было показано, что тот же метод применим и для доказательства

эквивалентности программ [74]. Общая схема насыщения равенствами в этой работе выглядит следующим образом:

• Исходная программа преобразуется в Е-РЕС.

• Производится насыщение: к Е-РЕС применяются преобразования, которые могут добавлять новые вершина и рёбра и сливать классы эквивалентности. Удаление же вершин и рёбер (и разбиение классов) запрещено. Насыщение завершается либо когда больше нельзя применить ни одно преобразование, либо когда достигается некоторый лимит количества преобразований.

• Из Е-РЕС, представляющего множество программ, выделяется одна наилучшая программа. Для этого формулируется и решается задача целочисленного линейного программирования: каждой вершине Е-графа ставится в соответствие переменная, равная 1, если вершина войдёт в программу и 0, если не войдёт, и производится поиск программы наименьшей стоимости при ограничениях на согласованность (например, если вершина входит в программу, то в программу входят какие-то представители классов эквивалентностей дочерних вершин).

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

1.1.3 Переписывание графов и джунгли

Переписывание графов — это обобщение переписывания термов на графы. Система переписывания графов состоит из набора правил вида Ь ^ Д, подразумевающих, что если в графе С есть подграф вида Ь, то он может быть заменён на подграф вида Д. В теории переписывания графов возникают трудности с такими операциями, как удаление вершин, поэтому существует множество подходов к переписыванию графов: подход двойного кодекарто-ва квадрата [19], одинарного кодекартова квадрата [50] и т.д. Переписывание графов также обобщается на гиперграфы (графы, в которых рёбра, называемые гиперрёбрами, могут соединять более двух вершин, гиперграфы часто удобнее графов для некоторых приложений). Е-графы можно представлять в

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

Джунгли [35; 58] — ориентированные гиперграфы без циклов, у которых каждая вершина имеет не более одного исходящего гиперребра. Джунгли удобны для представления термов с учётом обобществления (sharing) одинаковых подвыражений. Джунгли очень похожи на Е-графы из насыщения равенствами (представленными гиперграфами) и полипрограммы из настоящей работы, по существу отличаясь от них только ограничением на количество исходящих гиперрёбер и ацикличностью, что не позволяет джунглям представлять множество эквивалентных выражений. На джунглях определяется правило преобразование, называемое свёрткой, которое позволяет сливать подграфы, представляющие равные термы. Это преобразование соответствует конгруэнтному замыканию, позволяющему сливать классы эквивалентности в Е-графах.

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

1.1.4 Пруверы первого порядка

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

Одним из подходов к решению данной задачи является метод насыщения [22] (в частности, метод резолюций [62]). Идея насыщения (которое не следует путать с насыщением равенствами, хотя идеи похожи) состоит в том, чтобы применять ко множеству формул правила вывода до тех пор, пока не будет достигнуто противоречие (при использовании доказательства от противного). В отличие от насыщения равенствами этот метод не подразумевает использование компактного представления равенств в виде Е-графа — обычно в пруверах первого порядка к равенствам используется другой подход, в частности, основанный на парамодуляции [63] и суперпозиции [4]. Данный метод реализован во многих пруверах, в частности, в E [66], Vampire [60], SPASS [71]. Существует обширный сборник задач для пруверов первого порядка TPTP (Thousands of Problems for Theorem Provers) [77], также регулярно проводятся соревнования.

Одной из вариаций задачи доказательства истинности формулы является задача выполнимости в теориях (SMT, satisfiability modulo theories). Отличие в том, что в этой задаче подразумевается, что есть некоторые встроенные теории, аксиомы для которых не нужно задавать в формулировке задачи. Это такие теории, как теории целых и вещественных чисел, списков, массивов и т.п. Для этих теорий должны быть специализированные разрешающие процедуры, которые используются в SMT-решателях (SMT-солверах), что позволяет решать задачу эффективнее, чем общими методами, использующимися в пруверах первого порядка. Заметим, что одна из теорий (наиболее простая) — теория неинтерпретированных функций с конгруэнтным равенством — решается как раз при помощи алгоритма конгруэнтного замыкания на Е-графах [55]). Формулы, к которым применяются SMT-солверы часто не содержат кванторов (свободные переменные можно считать связанными квантором существования на верхнем уровне, т.к. решается задача выполнимости) — в этом случае SMT-солверы за конечное время могут выдать ответ, является формула выполнимой или нет. Однако современные SMT-солверы поддерживают кванторы, что позволяет использовать их в качестве общих пруверов для логики первого порядка.

Сейчас большинство SMT-солверов основаны на алгоритме DPLL(T) [16], являющимся модификацией алгоритма решения задачи выполнимости булевых формул DPLL [14]. Суть алгоритма состоит в поиске с возвратом интерпретаций атомарных формул. Упрощённо, решатель теории получает на

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

Поддержка кванторов в SMT-решателях обычно осуществляется следующим эвристическим методом. Каждой универсально-квантифицированной формуле сопоставляется некоторый образец, представляющий из себя обычно подтерм этой формулы. Как только в состоянии солвера встречается терм, соответствующий этому образцу, производится инстанцирование формулы. Сопоставление с образцом должно при этом осуществляться с точностью до известных равенств между термами (E-matching, [52; 53]) — эта же проблема возникает и в насыщении равенствами при применении правил.

В качестве примеров SMT-решателей можно назвать Simplify [15], Yices [17], Z3 [54], CVC3 [6], Alt-Ergo [79]. Для SMT-решателей также существует сборник задач [80]

1.1.5 Индуктивные пруверы

Доказательство свойств программ при помощи структурной индукции известно ещё с 50-60-х годов [11]. Впоследствии появились полностью автоматические индуктивные пруверы, одним из первых был прувер Бойера и Мура [8] для языка LISP. Этот прувер был предшественником ACL2 [40], успешным индуктивным прувером, широко применяемым в индустрии. Большинство современных пруверов, как и ACL2 и его предшественники, используют метод явной индукции, суть которого в том, что аксиома индукции применяется явно, точно так же, как и все остальные правила вывода. У этого подхода есть некоторые недостатки, такие как необходимость угадывать подходящую схему индукции и гипотезу индукции до проведения самого рассуждения. Существуют альтернативные подходы, например, "индукция без индукции" [36], основанная на алгоритме Кнута-Бендикса [47]. Есть также подход, заключающийся в том, что допускаются циклические доказательства, для которых потом производится проверка корректности — все циклы должны быть убывающими относительно некоторого фундированного отношения на формулах — при этом схема индукции также применяется неявно [72; 75]. Отметим, что подход с циклическими доказательствами также обычно (хотя и не всегда) применяется в суперкомпиляции, которую мы рассмотрим в следующем разделе, а также он применяется в данной диссертации в форме слияния по

бисимуляции (Глава 5).

Обычно индуктивные пруверы работают следующим образом: к целевому утверждению применяются правила вывода (в обратном порядке) пока не будет построено завершённое дерево доказательства. В случае явного применения индукции индукция применяется как обычное правило вывода. При этом возникает огромное количество точек ветвления, что связано с неоднозначностью выбора правил вывода, применимых к утверждению, в частности очень большое множество вариантов даёт обобщение доказываемого утверждения. Эта проблема решается сочетанием эвристик и перебора. Среди эвристик стоит отметить рипплинг [9; 61]. Рипплинг управляет применением правил переписываний таким образом, чтобы к утверждению можно было применить гипотезу индукции, сдвинув мешающие части выражения наружу или к переменным. Кроме того, отметим индуктивный прувер Zeno [69] для языка Haskell, который использует более свободный подход к применению правил переписывания (внутри Zeno очень похож на суперкомпилятор, хотя и использует явную индукцию).

Существуют также способы использовать пруверы для логики первого порядка и SMT-решатели для доказательства по индукции. Для этого производится инстанцирование схемы индукции для целевого утверждения, после чего база индукции и шаг индукции доказываются отдельно прувером первого порядка [48]. В частности, таким образом работает HipSpec [3], индуктивный прувер для языка Haskell. Отметим, что HipSpec также использует разведку теории (theory exploration): сначала он генерирует набор гипотез при помощи тестирования [13], затем доказывает их по одной, при этом для доказательства гипотез используются уже доказанные гипотезы. Это позволяет находить необходимые обобщения и леммы даже в очень нетривиальных случаях.

1.1.6 Суперкомпиляция

Суперкомпиляция — метод преобразования программ, разработанный Тур-чиным [82]. Суперкомпиляция похожа на автоматическое доказательство по индукции, однако эти области развивались довольно независимо. Изначально суперкомпиляция была сформулирована для языка Рефал, но потом появились формулировки и для других языков. В частности, в работе Андрея Климова и Роберта Глюка [23] используется язык, похожий на Lisp, работающий

с S-выражениями. В работе Сёренсена [70] используется функциональный язык первого порядка с семантикой вызова по имени и данными, построенными из конструкторов, основанный на языке Miranda. В работе Митчелла [51] используется подмножество языка Haskell. Подмножество Haskell^ используется также в работе Ключникова [87].

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

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

• Если вычисление произвести нельзя, потому что этому мешает свободная переменная, значение которой неизвестно, то производится разбор случаев — к вершине подвешиваются дочерние вершины, в которых значение упомянутой переменной ограничено значениями определённого вида (например, для переменной типа Nat это может быть S(x) и Z). В доказательствах по индукции это соответствует применению аксиомы индукции (для пруверов, использующих метод явной индукции) или разбору случаев для пруверов, использующих циклические доказательства без явного применения индукции.

• По решению некоторых эвристик возможно применение обобщения — замену некоторых подвыражений на новые свободные переменные. Например, f (g(h(x))) можно обобщить до f (у), где у = g(h(x)), после чего f (у) и g(h(x)) рассматриваются по отдельности. В доказательствах по индукции это соответствует усилению гипотезы индукции при помощи обобщения или некоторым случаям введения лемм.

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

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

Одним из усовершенствований суперкомпиляции является возможность применения лемм в процессе суперкомпиляции. Например, в дистилляции, предложенной Гамильтоном [31-34], при зацикливании и обобщении производится работа не с самими конфигурациями, а с их суперкомпилированными версиями, что соответствует применению лемм, доказанных суперкомпилятором. В работах Ключникова и Романенко [42; 46] описана суперкомпиляция высшего уровня, заключающаяся в применении нижнего суперкомпилятора верхним (в частности, для доказательства лемм). Отметим, что в случае применения лемм возникает проблема с корректностью суперкомпиляции — дело в том, что традиционно суперкомпиляторы не совершают проверку того, что внутри циклов построенного графа происходит убывание относительно некоторого фундированного отношения, однако суперкомпиляция устроена так, что в этом нет необходимости. Но при произвольном применении лемм данное свойство суперкомпиляции теряется. В [46] показано, что если применяемые леммы ограничивать улучшающими леммами (в смысле теории Сэндса [64; 65]), то корректность сохраняется. Тот факт, что лемма улучшающая, можно проверить при помощи суперкомпилятора в процессе доказательства леммы.

Ещё одно развитие идеи суперкомпиляции — многорезультатная суперкомпиляция, предложенная Ключниковым и Романенко [44]. Традиционно суперкомпилятор выдаёт на выходе только одну программу, но многорезультатный суперкомпилятор выдаёт целое множество остаточных программ. Это бывает полезно, когда суперкомпиляция используется для анализа программ — при этом суперкомпилятор упрощает остаточную программу, делая её более доступной для дальнейшей обработки анализаторами. Один из примеров

такого использования суперкомпилятора — доказательство эквивалентности программ — при этом входные программы суперкомпилируются, после чего производится синтаксическое сравнение остаточных программ [45; 49]. В случае многорезультатной суперкомпиляции нужно сравнить результирующие множества на пересечение, что позволяет доказывать эквивалентности в большем числе случаев.

Для большинства приложений многорезультатной суперкомпиляции выдавать непосредственно множества остаточных программ не очень эффективно. Эффективнее генерировать некоторое компактное представление множества остаточных программ, которое потом анализируется также быстрее. Например, в работе [26] описано такое представление множеств остаточных программ в виде деревьев, компактность при этом достигается за счёт совмещения общих начальных частей программ, а дальнейшая фильтрация этого множества по некоторому условию может быть произведена эффективнее, чем фильтрация обычного множества программ за счёт того, что в процессе разом могут выбрасываться целые подмножества программ, не соответствующих условию. В работе [28] используется ещё более компактное представление множества программ в виде графа, подобного Е-графу, но при этом сохраняется общая схема суперкомпиляции — фактически эта работа является промежуточной между суперкомпиляцией и насыщением равенствами. Настоящая диссертационная работа является следующим шагом по направлению к насыщению равенствами — фактически мы используем преобразования из суперкомпиляции, но в рамках насыщения равенствами.

1.2 Выводы

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

Глава 2

Основная идея метода: полипрограммы и преобразования над ними

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

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

2.1 Используемые обозначения

Во всей оставшейся части диссертации будем использовать символ = для разделения частей определений функций программ и полипрограмм, чтобы отличить его от метатеоретического равенства =. Кроме того, часто будем использовать запись ё1 для обозначения списков вида е\,е<2,... ,еп для неко-

торого натурального п (определяется из контекста). Значение п будем также обозначать как тах 1,. Также будем вкладывать такие конструкции друг в друга, например, /¿(ё^) обозначает

/1(611, ..., е1к1), .. ., /„(е„1, ..., епкп)

для некоторого п и некоторых к1,... ,кп. То, какой индекс к какой верхней черте относится, определяется из контекста. Отметим, что нумерацию мы в таких конструкциях ведём всегда с 1.

Списки будем обозначать квадратными скобками [а,Ь,с], нумерацию элементов будем вести с 1, т.е. [а, Ь, с][1] = а. Будем также использовать генераторы списков [х + у | х € хя ,у € уя].

Кортежи будем обозначать как в угловых скобках {а, Ь, с), так и в круглых (а,Ь,с). Первую запись мы предпочитаем использовать для целостных объектов (полипрограмма, граф), а вторую для простого возврата нескольких значений из функции. Доступ к элементам кортежа будем осуществлять при помощи функций щ, например, ,К2({а, Ъ, с)) = Ь.

Для функций и морфизмов ф : А ^ В домен будем обозначать как йот(ф) = А, а кодомен как вой(ф) = В. Область значений функции / будем обозначать как 1т(/).

Если / : А ^ В — функция, то её сужение на подмножество X С А будем обозначать как (/. Тождественные функции и морфизмы будем обозначать как гй, иногда с указанием объекта или множества гйЕсли А С В, то будем использовать обозначение гйа^в = {гйв .

Список литературы диссертационного исследования кандидат наук Гречаник Сергей Александрович, 2018 год

Список литературы

1. Abel A. foetus - Termination Checker for Simple Functional Programs: Programming Lab Report / LMU Miinchen. — July 1998.

2. Abel A., Altenkrich T. A Predicative Analysis of Structural Recursion // Journal of Functional Programming. — 2002. — Vol. 12, no. 1. — Pp. 141. —URL: http://www.cs.cmu.edu/~abel/foetuswf.ps.gz.

3. Automating Inductive Proofs Using Theory Exploration / K. Claessen, M. Johansson, D. Rosen, N. Smallbone // Automated Deduction - CADE-24 -24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings. Vol. 7898 / ed. by M. P. Bonacina. — Springer, 2013. — Pp. 392-406. — (Lecture Notes in Computer Science). — ISBN 978-3-642-38573-5. — URL: http://dx.doi.org/10.1007/978-3-642-38574-2.

4. Bachmair L., Ganzinger H. Equational Reasoning in Saturation-Based Theorem Proving // Automated Deduction: A Basis for Applications. Volume I, Foundations: Calculi and Methods / ed. by W. Bibel, P. H. Schmidt. — Dordrecht : Kluwer Academic Publishers, 1998.

5. Banerjee, Heintze, Riecke Design and Correctness of Program Transformations Based on Control-Flow Analysis // TACS: 4th International Conference on Theoretical Aspects of Computer Software. — 2001.

6. Barrett C., Tinelli C. CVC3 // Proceedings of the International Conference on Computer Aided Verification (CAV '07). Vol. 4590 / ed. by W. Damm, H. Hermanns. — Springer-Verlag, July 2007. — Pp. 298-302. — (Lecture Notes in Computer Science). — Berlin, Germany.

7. Barwise J., Moss L. S. Vicious Circles: On the Mathematics of Non-wellfounded Phenomena. — CSLI, 1996.

8. Boyer R. S., Moore J. S. Proving theorems about LISP functions // Journal of the ACM (JACM). — 1975. — Vol. 22, no. 1. — Pp. 129-144.

9. Bundy A. The use of explicit plans to guide inductive proofs // Conf. on Automated Deduction (CADE 9). — 1987.

10. Burstall R. M., Darlington J. A transformational system for developing recursive programs // Journal of the ACM. — 1977. — Jan. — Vol. 24, no. 1. — Pp. 44-67.

11. Burstall R. M. Proving properties of programs by structural induction // The Computer Journal. — 1969. — Vol. 12, no. 1. — Pp. 41-48.

12. Claessen K., Hughes J. QuickCheck: a lightweight tool for random testing of Haskell programs // ACM SIGPLAN Notices. — 2011. — Apr. — Vol. 46, no. 4. — Pp. 53-64. — ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic). — DOI: http://dx.doi.org/10.1145/1988042.1988046.

13. Claessen K., Smallbone N., Hughes J. QuickSpec: Guessing Formal Specifications Using Testing // Tests and Proofs, 4th International Conference, TAP 2010, Malaga, Spain, July 1-2, 2010. Proceedings. Vol. 6143 / ed. by G. Fraser, A. Gargantini. — Springer, 2010. — Pp. 6-21. — (Lecture Notes in Computer Science). — ISBN 978-3-642-13976-5. — URL: http://dx.doi.org/10.1007/978-3-642-13977-2.

14. Davis M., Logemann G., Loveland D. W. A machine program for theoremproving // Commun. ACM. — 1962. — Vol. 5, no. 7. — Pp. 394-397. — URL: http://doi.acm.org/10.1145/368273.368557.

15. Detlefs, Nelson, Saxe Simplify: A Theorem Prover for Program Checking // JACM: Journal of the ACM. — 2005. — Vol. 52.

16. DPLL(T): Fast Decision Procedures / H. Ganzinger, G. Hagen, R. Nieuwen-huis, A. Oliveras, C. Tinelli // Proceedings of the 16th International Conference on Computer Aided Verification, CAV'04 (Boston, Massachusetts). Vol. 3114 / ed. by R. Alur, D. Peled. — Springer, 2004. — Pp. 175-188. — (Lecture Notes in Computer Science).

17. Dutertre B., De Moura L. The yices smt solver // Tool paper at http://yices. csl. sri. com/tool-paper. pdf. — 2006. — Vol. 2, no. 2.

18. Ehrig H., Kreowski H.-J. Parallelism of Manipulations in Multidimensional Information Structures // Mathematical Foundations of Computer Science. Vol. 45 / ed. by A. Mazurkiewicz. — 1976. — Pp. 284-293. — (Lecture Notes in Computer Science).

19. Ehrig, Pfender, Schneider Graph Grammars: An Algebraic Approach // FOCS: IEEE Symposium on Foundations of Computer Science (FOCS). — 1973.

20. Emelianov P. G. Analysis of the Equality Relations for the Program Terms // Lecture Notes in Computer Science. — 1996. — Vol. 1145. — Pp. 174188. — ISSN 0302-9743.

21. Equality saturation: a new approach to optimization / R. Tate, M. Stepp, Z. Tatlock, S. Lerner // SIGPLAN Not. — New York, NY, USA, 2009. — Jan. — Vol. 44, issue 1. — Pp. 264-276. — ISSN 0362-1340. — URL: http://doi.acm.org/10.1145/1594834.1480915.

22. Ganzinger H. Saturation-Based Theorem Proving // Lecture Notes in Computer Science. — 1996. — Vol. 1099. — ISSN 0302-9743.

23. Gluck R., Klimov A. V. Occam's Razor in Metacomputation: the Notion of a Perfect Process Tree // Static Analysis, Third International Workshop, WSA'93, Padova, Italy, September 22-24, 1993, Proceedings. Vol. 724 / ed. by P. Cousot, M. Falaschi, G. File, A. Rauzy. — Springer, 1993. — Pp. 112123. — (Lecture Notes in Computer Science). — ISBN 3-540-57264-3. — URL: http://dx.doi.org/10.1007/3-540-57264-3_34.

24. Graphsc source code and the test suite. — https://github.com/sergei-grechanik/supercompilation-hypergraph.

25. Grechanik S. Inductive Prover Based on Equality Saturation (Extended Version) // Proceedings of the Fourth International Valentin Turchin Workshop on Metacomputation / ed. by A. Klimov, S. Romanenko. — Pereslavl-Zalessky, Russia : Pereslavl Zalessky: Publishing House "University of Pere-slavl", July 2014. — Pp. 26-53. — ISBN 978-5-901795-31-6.

26. Grechanik S., Klyuchnikov I., Romanenko S. Staged Multi-Result Supercompilation: Filtering by Transformation // Proceedings of the Fourth International Valentin Turchin Workshop on Metacomputation / ed. by A. Klimov, S. Romanenko. — Pereslavl-Zalessky, Russia : Pereslavl Zalessky:

Publishing House "University of Pereslavl", July 2014. — Pp. 54-78. — ISBN 978-5-901795-31-6.

27. Grechanik S. A. Inductive Prover Based on Equality Saturation for a Lazy Functional Language // Perspectives of System Informatics: 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014. Revised Selected Papers. Vol. 8974 / ed. by A. Voronkov, I. Virbitskaite. — Springer, 2014. — Pp. 127-141. — (Lecture Notes in Computer Science). — ISBN 978-3-662-46822-7. — URL: http://dx.doi. org/10.1007/978-3-662-46823-4.

28. Grechanik S. A. Overgraph Representation for Multi-Result Supercompilation // Proceedings of the Third International Valentin Turchin Workshop on Metacomputation / ed. by A. Klimov, S. Romanenko. — Pereslavl-Zalessky, Russia : Pereslavl-Zalessky: Ailamazyan University of Pereslavl, July 2012. — Pp. 48-65. — ISBN 978-5-901795-28-6. — URL: http: //pat.keldysh.ru/~grechanik/doc/overgraph.pdf.

29. Grechanik S. A. Proving properties of functional programs by equality saturation // Programming and Computer Software. — 2015. — Vol. 41, no. 3. — Pp. 149-161. —URL: http://dx.doi.org/10.1134/ S0361768815030056.

30. Grechanik S. A. Supercompilation by Hypergraph Transformation: Preprint / Keldysh Institute of Applied Mathematics. — 2013. — 24 pp. — No. 26. — URL: http://library.keldysh.ru/preprint.asp?id=2013-26&lg=e.

31. Hamilton G. W. A Graph-Based Definition of Distillation // Second International Workshop on Metacomputation in Russia. — 2010.

32. Hamilton G. W. Distillation: extracting the essence of programs // Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation. — ACM Press New York, NY, USA. 2007. — Pp. 61-70.

33. Hamilton G. W. A Hierarchy of Program Transformers // Proceedings of the Third International Valentin Turchin Workshop on Metacomputation / ed. by A. Klimov, S. Romanenko. — Pereslavl-Zalessky, Russia : Pereslavl-Zalessky: Ailamazyan University of Pereslavl, July 2012. — Pp. 66-86. — ISBN 978-5-901795-28-6.

34. Hamilton G. W., Jones N. D. Distillation with labelled transition systems // Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, PEPM 2012, Philadelphia, Pennsylvania, USA, January 23-24, 2012 / ed. by O. Kiselyov, S. Thompson. — ACM, 2012. — Pp. 15-24. — ISBN 978-1-4503-1118-2. — URL: http://dl.acm.org/ citation.cfm?id=2103746.

35. Hoffmann B., Plump D. Implementing term rewriting by jungle evaluation // ITA. — 1991. — Vol. 25. — Pp. 445-472.

36. Huet G., Hullot J.-M. Proofs by Induction of Equational Theories with Constructors // Journal of Computer and System Sciences 25. — 1982. — Pp. 239-266.

37. Hutton G., Gibbons J. The Generic Approximation Lemma // Information Processing Letters. — 2001. — Vol. 79, no. 4. — Pp. 197-201.

38. Jones S. P., Tolmach A., Hoare T. Playing by the rules: rewriting as a practical optimisation technique in GHC // Haskell workshop. Vol. 1. — 2001. — Pp. 203-233.

39. Joshi R., Nelson G., Randall K. Denali: a goal-directed superoptimizer // ACM SIGPLAN Notices. — 2002. — May. — Vol. 37, no. 5. — Pp. 304314. — ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

40. Kaufmann M., Moore J. S. An Industrial Strength Theorem Prover for a Logic Based on Common Lisp // IEEE Transactions on Software Engineering. — 1997. — Apr. — Vol. 23, no. 4. — Pp. 203-213.

41. Klyuchnikov I. Supercompiler HOSC 1.0: under the hood: Preprint / Keldysh Institute of Applied Mathematics. — Moscow, 2009. — No. 63.

42. Klyuchnikov I. Towards effective two-level supercompilation: Preprint / Keldysh Institute of Applied Mathematics. — 2010. — 28 pp. — No. 81. — URL: http://library.keldysh.ru/preprint.asp?id=2010-81&lg=e.

43. Klyuchnikov I. G., Romanenko S. A. MRSC: a toolkit for building multi-result supercompilers: Preprint / Keldysh Institute of Applied Mathematics. — 2011. —No. 77. —URL: http://library.keldysh.ru/preprint. asp?lg=e&id=2011-77.

44. Klyuchnikov I. G., Romanenko S. A. Multi-Result Supercompilation as Branching Growth of the Penultimate Level in Metasystem Transitions // Perspectives of Systems Informatics, 8th Andrei Ershov Informatics Conference, PSI 2011, Akademgorodok, Novosibirsk, Russia, June 27 - July 01,

2011. Vol. 7162 / ed. by E. Clarke, I. Virbitskaite, A. Voronkov. — Springer,

2012. — Pp. 210-226. — (Lecture Notes in Computer Science). — ISBN 978-3-642-11485-4.

45. Klyuchnikov I., Romanenko S'. Proving the Equivalence of Higher-Order Terms by Means of Supercompilation // Perspectives of Systems Informatics. Vol. 5947. — 2010. — Pp. 193-205. — (LNCS).

46. Klyuchnikov I., Romanenko S'. Towards Higher-Level Supercompilation // Second International Workshop on Metacomputation in Russia. — 2010.

47. Knuth D. E., Bendix P. Simple Word Problems in Universal Algebras // Computational Problems in Abstract Algebra / ed. by J. Leech. — Perga-mon Press, 1970. — Pp. 263-297.

48. Leino K. R. M. Automating Induction with an SMT Solver // Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings. Vol. 7148 / ed. by V. Kuncak, A. Rybalchenko. — Springer, 2012. — Pp. 315-331. — (Lecture Notes in Computer Science). — ISBN 978-3-64227939-3. — URL: http://dx.doi.org/10.1007/978-3-642-27940-9.

49. Lisitsa A., Webster M. Supercompilation for Equivalence Testing in Meta-morphic Computer Viruses Detection // Proceedings of the First International Workshop on Metacomputation in Russia. — 2008.

50. Lowe, Ehrig Algebraic Approach to Graph Transformation Based on Single Pushout Derivations // WG: Graph-Theoretic Concepts in Computer Science, International Workshop WG. — 1990.

51. Mitchell N., Runciman C. A Supercompiler for Core Haskell // Implementation and Application of Functional Languages. Vol. 5083. — Berlin, Heidelberg : Springer-Verlag, 2008. — Pp. 147-164. — (Lecture Notes In Computer Science). — ISBN 978-3-540-85372-5. — DOI: http://dx.doi. org/10.1007/978-3-540-85373-2_9.

52. Moskal M., Lopuszanski J., Kiniry J. R. E-matching for Fun and Profit // Electr. Notes Theor. Comput. Sci. — 2008. — Vol. 198, no. 2. — Pp. 1935. — URL: http://dx.doi.Org/10.1016/j.entcs.2008.04.078.

53. Moura L. M. de, Bj0rner N. Efficient E-Matching for SMT Solvers // Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings. Vol. 4603 / ed. by F. Pfenning. — Springer, 2007. — Pp. 183-198. — (Lecture Notes in Computer Science). — ISBN 978-3-540-73594-6. — URL: http://dx. doi.org/10.1007/978-3-540-73595-3_13.

54. Moura L. de, Bj0rner N. Z3: An Efficient SMT Solver // Tools and Algorithms for the Construction and Analysis (TACAS). Vol. 4963. — Berlin : Springer-Verlag, 2008. — Pp. 337-340. — (Lecture Notes in Computer Science). — URL: http://dx.doi.org/10.1007/978-3-540-78800-3_24.

55. Nelson, Oppen Fast Decision Procedures Based on Congruence Closure // JACM: Journal of the ACM. — 1980. — Vol. 27, no. 2. — Pp. 356-364.

56. Nieuwenhuis R., Oliveras A. Congruence Closure with Integer Offsets // Logic for Programming, Artificial Intelligence, and Reasoning, 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 22-26, 2003, Proceedings. Vol. 2850 / ed. by M. Y. Vardi, A. Voronkov. — Springer, 2003. — Pp. 78-90. — (Lecture Notes in Computer Science). — ISBN 3540-20101-7. — URL: http://dx.doi.org/10.1007/978-3-540-39813-4_5.

57. Nieuwenhuis, Oliveras Proof-Producing Congruence Closure//RTA: Rewriting Techniques and Applications, 1987, LNCS 256. — 2005.

58. Plump D. Evaluation of Functional Expressions by Hypergraph Rewriting: PhD thesis / Plump D. — Univ. Bremen, 1993.

59. Reynolds J. Definitional Interpreters for Higher Order Programming Languages // ACM Conference Proceedings. — ACM, 1972. — Pp. 717-740.

60. Riazanov A., Voronkov A. Vampire // Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings. Vol. 1632 / ed. by H. Ganzinger. — Springer, 1999. — Pp. 292-296. — (Lecture Notes in Computer Science). — ISBN 3540-66222-7. — URL: http://dx.doi.org/10.1007/3-540-48660-7_26.

61. Rippling: A Heuristic for Guiding Inductive Proofs / A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, A. Smaill // Artificial Intelligence. — 1993. — Aug. — Vol. 62, no. 2. — Pp. 185-253.

62. Robinson J. A. A Machine Oriented Logic Based on the Resolution Principle // JACM. — 1965. — Vol. 12, no. 1. — Pp. 23-41.

63. Robinson G., Wos L. Paramodulation and theorem-proving in first-order theories with equality // Automation of Reasoning. — Springer, 1983. — Pp. 298-313.

64. Sands D. Total correctness by local improvement in the transformation of functional programs // ACM Trans. Program. Lang. Syst. — 1996. — Vol. 18, no. 2. — Pp. 175-234.

65. Sands D. Proving the correctness of recursion-based automatic program transformations // Theor. Comput. Sci. — Amsterdam-London-New York-Oxford-Paris-Shannon-Tokyo, 1996. — Vol. 167, no. 1-2. — Pp. 193-233.

66. Schulz S. E - a brainiac theorem prover //AI Commun. — 2002. — Vol. 15, no. 2-3. —Pp. 111-126. —URL: http://content.iospress.com/ articles/ai-communications/aic260.

67. Scott D., Strachey C. Towards a Mathematical Semantics for Computer Languages: Technical Report / Oxford University Computer Laboratory. — 1971. — PRG-6.

68. Scott D. S. Domains for Denotational Semantics // Automata, Languages, and Programming: 9th Colloquium, Aarhus, Denmark / ed. by M. Nielson, E. M. Schmidt. — Springer-Verlag, 1982. — Pp. 577-613. — (Lecture Notes in Computer Science ; 140).

69. Sonnex W., Drossopoulou S., Eisenbach S. Zeno: An automated prover for properties of recursive data structures // TACAS. — Mar. 2012. — (Lecture Notes in Computer Science). — URL: http://pubs.doc.ic.ac. uk/zenoTwo/.

70. S0rensen M. H. Turchin's Supercompiler Revisited: an Operational Theory of Positive Information Propagation: MA thesis / S0rensen M. H. — K0benhavns Universitet, Datalogisk Institut, 1994.

71. SPASS Version 3.5 / C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. S. 0001, P. Wischnewski // Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. Vol. 5663 / ed. by R. A. Schmidt. — Springer, 2009. — Pp. 140-145. — (Lecture Notes in Computer Science). — ISBN 978-3-642-02958-5. — URL: http : //dx . doi . org/10 .1007/978-3-64202959-2.

72. Sprenger C., Dam M. On global induction mechanisms in a ^-calculus with explicit approximations // ITA. — 2003. — Vol. 37, no. 4. — Pp. 365391. — URL: http://dx.doi.org/10.1051/ita:2003024.

73. Stepp M. B. Equality saturation : engineering challenges and applications. — Jan. 2011.

74. Stepp M., Tate R., Lerner S. Equality-Based Translation Validator for LLVM // Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Vol. 6806 / ed. by G. Gopalakrishnan, S. Qadeer. — Springer, 2011. — Pp. 737-742. — (Lecture Notes in Computer Science). — ISBN 978-3-642-22109-5. — URL: http://dx.doi.org/10.1007/978-3-642-22110-1.

75. Stratulat S'. A Unified View of Induction Reasoning for First-Order Logic // Turing-100 - The Alan Turing Centenary, Manchester, UK, June 22-25, 2012. Vol. 10 / ed. by A. Voronkov. — EasyChair, 2012. — Pp. 326-352. — (EPiC Series). — URL: http : //www . easychair . org/publications/ ?page=1900403647.

76. Streicher T. Domain-theoretic foundations of functional programming. — World Scientific, 2006. — ISBN 978-981-270-142-8.

77. Sutcliffe G. The TPTP Problem Library and Associated Infrastructure // J. Autom. Reasoning. — 2009. — Vol. 43, no. 4. — Pp. 337-362. — URL: http://dx.doi.org/10.1007/s10817-009-9143-8.

78. Tate R. Equality saturation: using equational reasoning to optimize imperative functions. — Jan. 2012.

79. The Alt-Ergo Theorem Prover. — http://alt-ergo.lri.fr/.

80. The Satisfiability Modulo Theories Library. — http://smtlib.cs.uiowa. edu/.

81. TIP: Tons of Inductive Problems / K. Claessen, M. Johansson, D. Rosen, N. Smallbone.

82. Turchin V. The concept of a supercompiler // ACM Transactions on Programming Languages and Systems (TOPLAS). — 1986. — Vol. 8, no. 3. — Pp. 292-325.

83. Turner D. Total Functional Programming // Journal of Universal Computer Science. — 2004. — Vol. 10, no. 7. — Pp. 751-768.

84. Yorgey B. The typeclassopedia // The Monad. Reader Issue 13. — 2009. — P. 17.

85. Гречаник С. А. Доказательство свойств функциональных программ методом насыщения равенствами // Программирование. — 2015. — № 3. — с. 44—61.

86. Гречаник С. А. Полипрограммы как представление множеств функциональных программ и преобразования над ними // Препринты ИПМ им. М.В.Келдыша. — 2017. — № 5. — DOI: 10.20948/prepr-2017-5. — URL: http://library.keldysh.ru/preprint.asp?id=2017-5.

87. Ключников И. Г. Выявление и доказательство свойств функциональных программ методами суперкомпиляции / Ключников Илья Григорьевич. — Институт прикладной математики им М.В. Келдыша РАН, 2010.

88. Ключников И. Г. Суперкомпиляция: идеи и методы // Практика функционального программирования. — 2011. — т. 7.

Приложение A Дополнительные примеры

В данном приложении будут рассмотрены дополнительные примеры.

Пример 12. Слияние по бисимуляции обычно применяется для завершения доказательства, однако иногда его имеет смысл применять и в середине процесса преобразования полипрограммы, что соответствует обнаружению и применению леммы. Рассмотрим следующую полипрограмму:

(1) f(х) = case х of {Z ч Z; S(y) ч f (f (у))}

(2) g(x) = case x of {Z ч Z; S(у) ч g(x)}

Требуется доказать, что f и g эквивалентны. Для удобства вынесем подвыражение f (f (у)) в отдельную функцию при помощи правила расчленения:

(3) f (х) = case ж of {Z ч Z; S(y) ч h(y)}

(4) h(x) = f (f (x))

Раскроем внешний вызов f в определении (4), получится следующее определение:

(5) h(x) = case f (х) of{Z ч Z; S(y) ч h(y)}

Теперь раскроем f (ж) в разбираемой позиции:

(6) h(x) =

case (case х of {Z ч Z; S(y) ч h(y)}) of Z ч Z S(y) ч h(y)

Теперь применим правило сопоставления с образцом результата сопоставления с образцом:

(7) h(x) =

case х of

Z ч case Z of {Z ч Z; S(у) ч h(y)} S(y) ч case h(y) of {Z ч Z; S(y) ч h(y)}

В ветви Z произведём редукцию сопоставления с образцом:

(8) h(x) =

case х of Z ч Z

S(y) ч case h(y) of {Z ч Z; S(y) ч h(y)} Теперь возьмём определение (3) и раскроем в нём h(x) по определению (5):

(9) f (х) =

case х of Z ч Z

S(y) ч case f (у) of {Z ч Z; S(у) ч h(y)}

Определения (8) и (9) очень похожи, и действительно, к ним можно применить слияние по бисимуляции. Полипрограмма бисимуляции выглядит сле-

дующим образом:

f И =

case x of

Z ч Z

S(y) ч case f (y) of {Z ч Z; S(y) ч h(y)}

При этом = {f ч f,h ч h} и ф2 = {f ч h,h ч h}. Это как раз пример, когда фрагменты не изоморфны. Нетрудно видеть, что рекурсия в полипрограмме бисимуляции структурная, поэтому можно добавить следующее определение к нашей полипрограмме:

(10) f (х) = h(x)

Теперь применим конгруэнтность, заменив h на f в определении (3):

(11) f (х) = case х of {Z ч Z; S(y) ч f (у)}

Теперь можно применить ещё одно слияние по бисимуляции для определений (11) и (2), что даст нам требуемое f (х) = д(х) А

Пример 13. Рассмотрим пример доказательства того, что эффективная реализация функции чётности эквивалентна неэффективной реализации:

(1) even(x) = case х of {Z ч Т; S(y) ч odd(y)}

(2) odd(x) = case x of {Z ч F; S(у) ч even(y)}

(3) not(t) = case t of {F ч T; T ч F}

(4) evenSlow(x) = case x of {Z ч T; S(у) ч oddSlow(y)}

(5) oddSlow(x) = not(evenSlow(x))

Надо доказать, что evenSlow(x) = even(x). Раскроем вызов функции not в определении (5):

(6) oddSlow(x) = case evenSlow(x) of {F ч T; T ч F}

Теперь раскроем вызов evenSlow:

(7) oddSlow(x) =

case (case x of {Z ч T; S(у) ч oddSlow(y)}) of F ч T T ч F

Применим правило сопоставления с образцом результата сопоставления с образцом:

(8) oddSlow(x) =

case x of

Z ч case T of {F ч T; T ч F}

S(y) ч case oddSlow(y) of {F ч T; T ч F}

Теперь произведём редукцию в ветви Z:

(9) oddSlow(x) =

case х of Z ч F

S(y) ч case oddSlow(y) of {F ч T; T ч F} Ветвь S вынесем в качестве отдельной функции:

(10) oddSlow(x) = case ж of {Z ч F; S(y) ч f (у)}

(11) f (x) = case oddSlow(x) of {F ч T; T ч F}

Раскроем в (11) вызов oddSlow с использованием определения (10), применим сопоставление с образцом результата сопоставлении с образцом и произведём

редукцию в ветви Z (сделаем это в одно действие для краткости):

(12) f (х) =

case х of Z ч Т

S(y) ч case f (у) of {F ч T; Т ч F} Теперь в определении (4) раскроем oddSlow по определению (6):

(13) evenSlow(x) =

case х of Z ч T

S(y) ч case evenSlow(y) of {F ч T; T ч F}

Теперь можно применить слияние по бисимуляции к определениям (13) и (12):

(14) f (x) = evenSlow(x)

Теперь по конгруэнтности заменим f на evenSlow в (10):

(15) oddSlow(x) = case x of {Z ч F; S(y) ч evenSlow(y)}

Определения (1) и (2) совпадают с определениями (4) и (15) с точностью до переименования функций, поэтому применяем слияние по бисимуляции и получаем

(16) oddSlow(x) = odd(x)

(17) evenSlow(x) = even(x)

Л

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

торые виды обобщений. Начало преобразования будет таким же как и в том примере:

(1) even(x) = case x of {Z ч T; S(у) ч odd(y)}

(2) odd(x) = case x of {Z ч F; S(y) ч even(y)}

(3) not(t) = case t of {F ч T; T ч F}

(4) evenSlow(x) = case x of {Z ч T; S(y) ч oddSlow(y)}

(5) oddSlow(x) = not(evenSlow(x))

(6) oddSlow(x) = case evenSlow(x) of {F ч T; T ч F}

(7) oddSlow(x) =

case (case x of {Z ч T; S(y) ч oddSlow(y)}) of F ч T T ч F

(8) oddSlow(x) =

case x of

Z ч case T of {F ч T; T ч F}

S(y) ч case oddSlow(y) of {F ч T; T ч F}

(9) oddSlow(x) =

case x of Z ч F

S(y) ч case oddSlow(y) of {F ч T; T ч F}

(10) oddSlow(x) = case ж of {Z ч F; S(y) ч f (y)}

(11) f (x) = case oddSlow(x) of {F ч T; T ч F}

(12) f (x) =

case x of Z ч T

S(y) ч case f (y) of {F ч T; T ч F}

Теперь в ветви S определения (12) раскроем вызов функции f по определению (11), и сразу после этого раскроем вызов oddSlow по определению (6):

(13) f (х) = case х of

Z ч Т

/case (case evenSlow(x) of {F ч T;T ч F}) of\ S(у) ч case F ч Т

V Т ч F J

of{F ч Т; Т ч F}

Фактически в ветви S записано тройное отрицание выражения evenSlow(x), которое эквивалентно одинарному отрицанию этого выражения. Применим в ветви S правило сопоставления с образцом результата сопоставления с образцом два раза (возможность такого применения ключевая в этом примере), а в ветвях получившегося выражения произведём редукцию сопоставления с образцом, и получим в точности одинарное отрицание:

(14) f И =

case х of

Z ч Т

S(y) ч case evenSlow(y) of {F ч T; T ч F}

Теперь заметим, что правые части определений (9) и (14) совпадают, а значит по транзитивности:

(15) f (х) = evenSlow(x)

Дальнейшее происходит как в прошлом примере. По конгруэнтности заменяем f на evenSlow в (10):

(16) oddSlow(x) = case х of {Z ч F; S(y) ч evenSlow(y)}

Определения (1) и (2) совпадают с определениями (4) и (16) с точностью до переименования функций, поэтому применяем слияние по бисимуляции и

получаем

(17) oddSlow(x) = odd(x)

(18) evenSlow(x) = even(x)

Отметим, что ключевой момент состоял в применении правила сопоставления с образцом результата сопоставления с образцом к выражению вида case case е of{...} of{...}, где е — произвольное выражение. Интересный нюанс заключается в том, что для реализации прогонки (как в суперкомпиляции) нам достаточно того, чтобы это правило было применимо только в случае, когда е = х, т.е. некоторая переменная. Но когда е может быть произвольным, это правило становится более мощным и способным на эффекты, подобные нетривиальным обобщениям. А

Пример 15. Рассмотрим пример применения правила (trans) к следующей полипрограмме:

fi(x,y) = g(h(x,y),h(y,x))

/2Ы = 9(h(x,y),h(y,x))

В бесточечно-расчленённом представлении она записывается следующим образом:

id2/i = Called2д, id2h, {1 ч 2, 2 ч 1}h)

{1 ч 2}i^2/2 = Call(id29, id2h, {1 ч 2, 2 ч 1}h)

Существует четыре способа отобразить определения образца L в полипрограмму G. Первые два способа отображают оба определения L в какое-то одно определение G, и в результате применения правила с такими отображениями получатся тривиальные определения fi = Id(/i) и /2 = Id(/2), что эквивалентно применению (eq-refl). Рассмотрим более интересные случаи, когда определения L отображаются в различные определения G, например, первое в первое и второе во второе. Соответствующее отображение функциональных символов выглядит как {f ч fi,g ч /2, hi ч g,h2 ч h,h% ч h,h ч произвольная функция}. Т.к. в образце L есть лишние функции hi,i > 3, то их тоже надо куда-то отобразить, но совершенно не важно, куда, поскольку

это ни на что не повлияет. Теперь дополним данные отображения до морфиз-ма ф : Ь ч С. На функциональных символах одно из возможных дополнений выглядит следующим образом (здесь Nf, Мд,... обозначают арности функций в образце Ь):

Ф(!) = ^/1

ф(д) = {1 ч 2}^ ¡2

Ф(к1) = гй д

ф(Ь,2) = гйк

ф(к3) = {1 ч 2, 2 ч 1}2^3 к

Получаем, что С ^^гап8),0 Н, где Н имеет следующий вид:

гй2/1 = Са11(гй2д, гй2к, {1 ч 2, 2 ч 1}к)

{1 ч 2} 1^2/2 = Са11( гй29, гй2к {1 ч 2, 2 ч 1}к)

гй/1 = гйId({1 ч 2}^^/2)

Новое (последнее) определение записано не в канонической форме, в канонической форме оно выглядит так:

{1 ч 2, 2 ч 1Ы2/1 = гй1/2)

Или, в более удобном для чтения виде:

¡1(У,х) = 12 И

Проделывая то же самое для случая, когда первое определение отображается во второе, а второе в первое, получим симметричное определение (с тем же смыслом):

/2Ы = ¡1(х,У)

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

Если рассмотреть другое дополнение отображений определений и функ-

ций перестановками параметров до морфизма, то получится тот же самый результат. Например, возьмём следующий морфизм:

ФИ) = {1 ч 2, 2 ч 1}2^ /1

ф(д) = гй /2

ф(М = {1 Ч 2, 2 Ч д

ф(Ь,2) = гй2^мН2 к

ф(к3) = {1 ч 2, 2 ч 1}2^3 к

Здесь отличаются перестановки при вызываемой функции д, что возможно только благодаря тому, что оба аргумента представлены одинаковыми функциями к. Формулы определений Ь отобразятся в следующие определения (до приведения к каноническому виду):

{1 Ч 2, 2 ч 1}2^ /1 = гй^ Са11({1 Ч 2, 2 ч 9,

гйк,

{1 ч 2,2 ч 1}2^3 к) гй 1 ¡2 = гймН2^М; Са11({1 ч 2, 2 ч 1}2^мН1 9,

гй2^иН2 к,

{1 ч 2,2 ч 1}2^3 к)

Или, в более читаемой форме:

Ыу, х) = д(к(у, х), к(х, у)) 12(х) = д(к(у,х), к(х,у))

После приведения к каноническому виду получится в точности С.

При применении правила добавляемое определение будет иметь также немного другой вид до приведения к каноническому виду:

{1 Ч 2, 2 ч 1}2^М;/1 = гйМдЫ(гй 1 /2)

Однако после приведения к каноническому виду оно будет в точности совпа-

дать с определением, добавленным при помощи предыдущего морфизма: {1 ч 2, 2 ч 1Ы2/1 = гй1^Ы(гй 1/2)

Л

Пример 16. Рассмотрим пример применения правила (агйу-ге^сйоп). Пусть полипрограмма имеет следующий вид (важный нюанс — ] и слева, и справа):

/ (х,у) = ] (д1(),д2(х))

Или, в бесточечно-расчленённом представлении:

гй2/ = гй 1^2Са11(гй2/, гй0^191, гйш)

Применим правило понижения арности для т =1. При этом морфизм ф : Ь ч С на функциях действует следующим образом:

Ф(!) = гй ]

ф(Ьл) = гй 2^2/ ф(Ь,2) = гй 0^191 ф(к3) = гй 1^192

В результате функция ] полипрограммы С отобразится в гй 1^2/' и получится следующая полипрограмма:

гй 1^2/' = гй 1^2Са11(гй 1^2/', гй0^1 д1, гй 132)

Что после приведения к каноническому виду превратится в

гй 1/' = гйо^1Са11(гй 1/', гй091)

Или, иначе

/ 'И = / 'Ы))

Получившаяся полипрограмма не находится в полностью канонической форме, и так произошло именно потому, что ] находится слева и справа. Ещё

одно применение правила приведёт данную полипрограмму к полностью каноническому виду:

Г () = /''()

Это определение выражено при помощи конструкции Са11:

гй с/'' = гй оСа11(гй о/'')

Оно может быть превращено в конструкцию Ы при помощи применения правила (саП^о-регт^аНоп). Д

Пример 17. Рассмотрим пример применения правила (саП^о-регт^айоп) к следующей полипрограмме:

/(х, у, г, и) = д(ю(у), ю(х), ю(и)) у(х) = X

Она же в бесточечно-расчленённом представлении:

гй4/ = гй4Са11(гй3д, {1 ч 2}у, {1 ч 1}^, {1 Ч 4}у) гй 1« = гй 1Уаг

Её первое определение эквивалентно следующему (неиспользуемый аргумент {1 Ч 3}-у добавлен для наглядности):

гй4/ = гй4Са11({1 ч 2, 2 ч 1, 3 ч 4}д,

{1 ч 1}^, {1 ч 2}-у, {1 ч 3}-у, {1 ч 4}-у)

Отсюда сразу очевидно, что применимо правило с ф, действующим на функции так:

ф(у) = гй 1« ф(/) = гй /

ф(д) = {1 Ч 2, 2 ч 1, 3 ч 4}з^д

Получаем в итоге следующую полипрограмму (не в канонической форме):

гй4/ = гй4И({1 ч 2, 2 ч 1, 3 ч 4}д) гй 1« = гй 1Уаг

Или:

/ (х,у,г,и) = д(у,х,и) у(х) = X

Л

Пример 18. Рассмотрим пример применения правил из Главы 4 для слияния функций, представленных изоморфными деревьями.

ЛИ = а Ы),к(х)) 31 () = ^ ()

/2(х) = С (д2(),к(х))

{92() = г ()

' /1(х) = С(91(),к(х))

91 () = ^ () ^гапв) < /2(ж) = С(92(),к(х))

92 () = ^() 91() = 92()

' /1(х) = С(91(),к(х)) 91 () = ^ () ^32=31 < 12(х) = С (д1(),к(х)) 91 () = ^ () () = 91()

=ф

(trans) *

^/2 = /l <

remove-

-dups)

201

/i(x) = С (gi(),h(x)) 91 () = ^ ()

h(x) = С (gi(),h(x)) 91 () = ^ () 91() = gi()

„ ЛИ = ЛИ

h(x) = С (ffl(),h(x))

31 () = 2 ()

/l(x) = С (ff1(),h(x))

91 () = ^ () 91() = 91()

„ ЛИ = ЛИ ЛИ = С Ы)>И)

31 () = 2 () 31() = Ы)

ч ЛИ = f1(x)

A

Пример 19. Слияние по бисимуляции способно приводить к понижению арности функций. Рассмотрим следующую полипрограмму С:

/ (х) = Ь1 (1г(х)) Нх) = / (9(х))

Эта программа вычисляет бесконечное число Б(Б(Б(...))), но не очень эффективно, накапливая бесполезный вызов некоторой функции д:

f(х) ч S(f (д(х))) ч S(S(f (д(д(х))))) ч

Рассмотрим следующую полипрограмму Н:

f (х,у) = S (h(x,y)) h(x,y) = f (д(х),д(у))

Эта полипрограмма имеет единственную модель для каждой интерпретации д. Морфизмы ф\}2 : Н ч G возьмём такие:

ФЛf )(х,у) = f (х)

фх(К)(х,у) = h(x)

ФЛд) = д

Ф2(! )(х,у) = f (у) Ф2(Щх,у) = %) Ф2(д) = д

Тогда после применения последнего утверждения мы получим следующие дополнительные определения:

f (х) = f (У) h(x) = h(y)

Определения имеют такой вид, что можно применить понижение арности, в результате полипрограмма будет выглядеть так:

f () = S (h())

h = Call(/)

f () = f ()

h() = h()

Второе определение записано при помощи нотации бесточечного представления, чтобы подчеркнуть, что это всё ещё Call, а не Id. В h = Id(/) оно превращается при помощи преобразования (call-to-permutation). Далее, после применения конгруэнтности и удаления дубликатов, полипрограмма прини-

мает следующий вид:

/ () = ^ (/()) } () = I ()

Таким образом, слияние по бисимуляции позволило понизить арность рекурсивной функции и удалить бесполезный вызов. Д

Приложение Б Доказательства некоторых утверждений

Доказательство Утверждения 12, с. 75

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

Доказательство. Начальным объектом является пустое множество функциональных символов, а копроизведениями — обычные копроизведения (размеченные объединения) двух множеств функциональных символов как множеств.

Докажем существование коуравнителей. Пусть а, @ : Р ч С. Построим для этой пары морфизмов коуравнитель 6 : С ч Н. Пусть 6(д) = ,Нд). Во-первых, надо обеспечить 6 о а = 6 о р. Пусть ] € Р, введём обозначения:

«(/) = (^ ) Ж/) = (£/,9/)

В этих обозначениях нам надо обеспечить

в1 'Пд1 = О 'Пд'1 ъ = Ъ ,

Сначала построим коуравнитель только для самих функциональных символов, без учёта перестановок, т.е. для функций 0 & и 0 Р в категории множеств — получим функцию е : С ч Н такую, что

£ о -Ж2 О а = £ О -Ж2 О Р

И назначим кд = £(д), что обеспечит нам второе равенство (кд/ = кд').

Для обеспечения первого равенства нам надо решить конечную систему уравнений в^= ^цд' относительно Её можно разбить на непересекающиеся по искомым 'д.. подсистемы уравнений, для каждой из которых £(9f) = £(3/) = к для некоторого к. Для каждой из таких подсистем должны иметь общий домен атгЬу(к) (арность к мы ещё не знаем), а значит каждую такую подсистему можно решить, построив предел соответствующей диаграммы в категории перестановок параметров (конечных множеств с инъективными функциями в качестве морфизмов). К сожалению, в категории перестановок параметров нет произведений, хотя есть уравнители и декартовы квадраты, однако по крайней мере в конечном случае уравнителей и декартовых квадратов достаточно для построения данного предела. В итоге мы получим все необходимые перестановки параметров -д и арности всех к € Н (т.к. всем к соответствует некоторая подсистема уравнений).

Теперь необходимо доказать универсальность. Пусть существует некоторый 5' такой, что 5' о а = 5' о р. Нужно доказать существование и единственность морфизма функциональных символов ш такого, что 5' = ш о 3.

Для 5' будет выполнено

■Ж2 о 3' о -Ж2 о а = -К2 о 3' о -Ж2 о @

А значит существует единственная функция т такая, что ^2 о 3' = т о е, т.к. £ — коуравнитель -Ж2 о а и -ж2 о @ в категории множеств. т и будет являться второй компонентой искомого морфизма, т.е. -ж2 о ш = т.

Теперь для каждого к € Н нам надо найти такую перестановку а^, чтобы для всех д выполнялось я 1(6'(д)) = -дд о ае(д). Про ж^З'(д)) мы знаем, что

о Ъ1(5'(д{)) = ^ о -К1(5'(д'})) Т.е. они удовлетворяют рассматриваемой ранее системе уравнений, а значит

и рассматриваемым ранее подсистемам. Т.к. решение подсистем строилось как предел, то для каждой подсистемы (а каждая подсистема соответствует своему h € Н) существует единственная ah такая, что ^i(S'(g)) = оah, если е(д) = h, что нам и нужно. Таким образом утверждение доказано. □

Доказательство Утверждения 13, с. 76

Утверждение. Морфизмы функциональных символов хорошо взаимодействуют с понятием канонической формы, а именно если pi « р2, то a(pi) ~ а(р2).

Доказательство. Для доказательства утверждения достаточно доказать, что для любыхр и а выполняется canon(а(р)) = canon(a(canon(р))). Рассмотрим случай, когда р имеет вид 0-if-i = в Call(6ofo,Oifi,...), а a(fi) = (Ci,gi). Тогда, расписывая определения canon, canon-call и decompose, получаем:

canon (р) = (C-if-i = С Call (id fo,Ce0(i)fe0 (i))), где (^,Ce0(i)) = nspHt (0eo(i))

(_,C,C-i) = bisplit(в о 6,в-1)

a(canon (p)) = (C-iC-i3-i = С Call(Co3o,Cec(¿) Ce0(i)ge0(i)))

canon(a(canon(p))) = (a-ig-i = a Call(id go,&e0c0(i)9e0(0(i))), где (3',^во Co(i)) = nsPlit (СвоСо(Фо<0 (i))

(_,a,a-i) = bisplit(£ о ó^^-iC-i)

«Ы = (0-iC-ig-i = 0 Call(0oCoSo,6&))

canon (a(p)) = (X-i3-i = X Call(id go, ХвоСо(г)9воСо(г))), где (S",Xeo(o(i)) = nsplit (°eo(o(i)Ceo(o(i)) (_,X,X-i) = bisplit (в о ó",6-iC-i)

Воспользовавшись определением nsplit и Утверждением 6, перепишем некоторые из равенств в следующем виде:

о Ceo(i),C-i) = nsplit(в о Qeo(i) ,e-i)

(_,а о °воCo(i),a-i) = nsplitо boCo(i) о CeoCo(¿)^-i о C-i)

(_,Х°Хв0Ш,^-1) = nsplit(° о ^оСо« о Ceo(o(i),0-i о C-i)

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

0 о 9eo(i) = а о £ о 6—1 = а о

А значит, если переставить индексы, то

0 о 0eo(o(i) = « о С о 6oCo(¿) 9_i = а о £_i

Эти следствия из первого равенства используем для переписывания третьего равенства:

(_,Х о X0oCo(¿)>Х—i) = nspUt(а ° £ ° ^Co(i) о CeoCo(i),a о i о С—i)

В результате правая часть этого равенства становится такой же, как и правая часть второго из вышеуказанных равенств с точностью до а, поэтому по Утверждению 6 будет выполнено a_i = х_i и а о &eoco(i) = X о Xeoco(i). А значит, т.к. а и х на самом деле являются тривиальными вложениями, верно ai = Xi, а поэтому canon(а(р)) = canon(а(canon(р))).

Остальные случаи доказываются аналогично. □

Доказательство Утверждения 34, с. 132 Утверждение. Если для узла b пребисимуляции вида

Ъ = Cong(/L, fR, (£LfL = rhsL), (Ír fR = rhsR), 6¿)

выполняются неравенства вида

perm(b) □ (CLp о iperm(b) о £r)

iperm(b) □ (£l о perm(b) о ) ф lift-perms(rhsL, rhsR, perm(6¿)) perm(bi) □ push-perm(iperm(b), rhsL, rhsR)[i]

то выполняется равенства

perm(b) = Cl 0 iperm(b) о

perm(bi) = push-perm(iperm(b), rhsL, rhs°)[i]

Доказательство. Обозначим 9 = perm(b) и 6i = perm(bi), t = iperm(b). Начнём с первого равенства. По условию выполняется следующее соотношение:

т 3 (Cl о 9 о ) Ф lift-perms(rhsl, rhs°, 9i)

А значит

г з а о в о

По монотонности операции композиции получаем йР 3 С Иь о 9 о ^ ь = в

Таким образом, 9 С £ЬРа по условию также выполняется соотношение 0 3 СЬпоэтому 9 = Сь .

Теперь перейдём ко второму равенству. По условию выполняется соотношение 9г 3 push-perm(т, гНвь, тНвр,)[г], поэтому таким же образом остаётся доказать, что 9г С push-perm(т, гНвЬ, тНвв)^].

Для определённости будем считать, что конструкция в определениях имеет вид СаБе^ (остальные случаи аналогичны), т.е.

гквь = Саяе^Сгдг) тНви = СаБе^ (стгкг)

Обозначим кг = атгЬу (Сг-1) и к1 =0, чтобы работать со всеми дочерними узлами одинаковым образом. Далее будем сокращённо писать push-perm(9) вместо push-perm(в, , т^д)[г], lift-perms(в^) вместо lift-perms(rhsь, тН8п,вг), эЫА(в) вместо shift(в, кг) и unshift(в) вместо unshift(в, кг). Отметим также, что по дистрибутивности о относительно ф и по Утверждению 33 выполняется push-perm(9 ф в') = push-perm(9) ф push-perm(9') для любых 9, 9'.

Будем преобразовывать правую часть:

push-perm(т) □

(по выполняющимся по условию соотношениям и монотонности)

□ push-perm(CLOC0l Ф lift-perms(вi)) □

□ push-perm(lift-perms(вi)) =

= push-perm(... ф чизЬя^Ъ(Сгвга°р) Ф ...) □

□ push-perm(чnзЬift (С,гвг а°р)) =