научная статья по теме ДОКАЗАТЕЛЬСТВО СВОЙСТВ ФУНКЦИОНАЛЬНЫХ ПРОГРАММ МЕТОДОМ НАСЫЩЕНИЯ РАВЕНСТВАМИ Математика

Текст научной статьи на тему «ДОКАЗАТЕЛЬСТВО СВОЙСТВ ФУНКЦИОНАЛЬНЫХ ПРОГРАММ МЕТОДОМ НАСЫЩЕНИЯ РАВЕНСТВАМИ»

- ПЕРСПЕКТИВЫ СИСТЕМ ИНФОРМАТИКИ

У V ; 004.032.24, 512

ДОКАЗАТЕЛЬСТВО СВОЙСТВ ФУНКЦИОНАЛЬНЫХ ПРОГРАММ МЕТОДОМ НАСЫЩЕНИЯ РАВЕНСТВАМИ

© 2015 г. С.А. Гречаник

Институт прикладной математики им. М.В.Келдыша РАН 125047 Москва, Миусская пл., 4 E-mail: sergei.grechanik@gmail. com Поступила в редакцию 01.12.2014

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

1. ВВЕДЕНИЕ

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

Существуют различные применения насыщение равенствами. Его можно использовать для оптимизации программ — в этом случае после за* Работа выполнена при поддержке гранта РФФИ № 12-01-00972-а и гранта Президента РФ для ведущих научных школ № НШ-4307.2012.9.

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

В статье Тейта и других [1] насыщение равенствами описано в применении к императивным языкам, а именно к байт-коду Java и LLVM, хотя само их промежуточное представление, основанное на Е-графах, по сути функционально. В данной статье мы опишем как насыщение равенствами может быть применено к доказательству эквивалентности функций на функциональном языке с нестрогой семантикой. Мы адаптируем насыщение равенствами к этой задаче за счёт заимствования преобразований из суперкомпиляции [5, 6]. Так как для доказательства многих свойств алгебраических типов данных требуется индукция, мы вводим специальное преобразование, называемое слиянием по бисимуляции, которое по сути доказывает по индукции, что два терма (изображаемые двумя вершинами в Е-графе) эквивалентны. Это преобразование можно применять много раз, что даёт эффект выявления и доказательства лемм, нужных для доказательства целевого утверждения.

В отличие от таких инструментов, как HipSpec [7] или Zeno [8], мы не инстанцируем схему индукции, а вместо этого проверяем корректность графа доказательства подобно тому, как это это делается в языке Агда [9, 10]. Мы также полностью поддерживаем бесконечные и частичные данные, не делая предположения, что язык тотальный. Доказательство утверждений, верных только в условиях тотальности, возможно при помощи нашего инструмента, если включить некоторые дополнительные преобразования, но не очень эффективно.

Дальнейшее изложение построено следующим образом: в разделе 2 мы кратко опишем метод насыщения равенствами и то, как множества функциональных программ представляются при помощи Е-графов, затем в разделе 3 мы рассмотрим основные преобразования, которые мы применяем к Е-графу. В разделе 4 мы опишем слияние по бисимуляции. В разделе 5 мы обсудим, в каком порядке применять преобразования. В разделе 6 мы представим результаты экспериментальной оценки нашего прувера. В разделе 7 мы обсудим работы, связанные с нашей, а раздел 8 является заключением.

Исходный код нашей экспериментальной реализации прувера можно найти в репозитории на сайте GitHub [11].

2. ПРОГРАММЫ И Е-ГРАФЫ

Е-граф — это граф, вершины которого разбиты на классы эквивалентности. В нашем случае Е-граф представляет множество термов (возможно, рекурсивных) и множество равенств над этими термами, замкнутое относительно рефлексивности, транзитивности и симметричности. Можно также поддерживать это множество равенств замкнутым относительно конгруэнтности при помощи алгоритма конгруэнтного замыкания [3]. Е-графовое представление равенств над термами очень эффективно и часто используется для решения задачи эквивалентности термов.

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

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

В качестве языка мы будем использовать нети-пизированное подмножество Haskell первого порядка (для того, чтобы наш прувер мог работать и с функциями высших порядков, мы применяем дефункционализацию). В качестве примера того, как программы отображаются в графы, рассмотрим следующую программу: not b = case b of {T ^ F; F ^ T} even n = case n of {Z ^ T; S m ^ odd m} odd n = not (even n)

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

Рис. 1. Представление программы в виде графа.

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

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

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

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

Если графы естественным образом соответствуют программам, то Е-графы естественным образом соответствуют программам с множественными определениями функций (но смысл заключается в том, что разные определения одной и той же функции должны быть семантически эквивалентны). Рассмотрим следующую "недетерминированную" программу: not b = case b of {T ^ F; F ^ T}

even n = case n of {Z ^ T; S m ^ odd m} odd n = case n of {Z ^ F; S m ^ even m}

odd n = not (even n) even n = not (odd n)

Программа содержим множественные определения функций even и odd, но все они эквивалентны. Эта программа может быть представлена как граф, но она будет содержать более од-

even

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

Е-графы также можно использовать для компактного предс

Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.

Показать целиком