Аннотация Программы в парадигме реляционного программирования представляют собой математические отношения. Программы-отношения можно исполнять в различных направлениях: зафиксировав часть аргументов программы, находить значение остальных. Не всегда исполнение программы в заданном направлении эффективно. Одним из способов улучшения производительности является трансляция реляционных программ в функциональные. Для генерации функции по отношению необходимо определить порядок связывания имен в программе с учётом заданного направления. Для этого традиционно применяется анализ времени связывания, однако для реляционных языков ранее его разработано не было. В статье мы предлагаем алгоритм анализа времени связывания для языка реляционного программирования miniKanren. Ключевые понятия Реляционное программирование, анализ времени связывания, статический анализ
Реляционное программирование парадигма, в которой любая программа описывает математическое отношение на её аргументах. Имея программуотношение, можно выполнять запросы: указывая некоторые известные аргументы, получать значения остальных. Например, addo ⊆ Int×Int×Int описывает отношение, третий аргумент которого является суммой первых двух. Рассмотрим возможные направления вычисления этого отношения (здесь и далее искомый аргумент будем обозначать знаком “?”). Выполнение отношения addo x y ? с зафиксированными (входными) первым и вторым аргументом найдет их сумму, а addo ? y z найдет такие числа, которые в сумме с y дадут z. Также можно найти одновременно значения нескольких аргументов: addo ? ? z найдет такие пары чисел, что в сумме они равны z, а addo ? ? ? перечислит все тройки из отношения.
Таким образом, мы можем говорить о выборе направления вычисления. Часто при написании программы подразумевается конкретное направление, называемое прямым (например, addo x y ?), все остальные направления обычно называются обратными. Возможность выполнения в различных направлениях основное преимущество реляционного программирования. Это своеобразный шаг к декларативности: достаточно написать одну программу для получения множества целевых функций.
Реляционному программированию родственно логическое, представленное такими языками, как Prolog и Mercury1 [1]. Основным представителем парадигмы реляционного программирования является семейство интерпретируемых языков miniKanren2. Языки семейства miniKanren компактны и встраиваются в языки общего назначения, за счёт чего их проще использовать в проектах. Для встраивания достаточно реализовать интерпретатор языка miniKanren: ядро языка, реализованное на Scheme занимает не более, чем 40 строк [2]. Помимо этого, miniKanren реализует полный поиск со стратегией interleaving, поэтому любая программа, написанная на нем, найдет все существующие ответы, в то время как Prolog может никогда не завершить поиск. В этой статье мы будем говорить про miniKanren.
Возможность выполнения программ на miniKanren в различных направлениях позволяет решать задачи поиска посредством решения задачи распознавания [3]. Так, имея интерпретатор языка, можно решать задачу синтеза программ на этом языке по набору тестов [4]; имея функцию, проверяющую, что некоторая последовательность вершин в графе формирует путь с желаемыми свойствами, получать генератор таких путей и так далее. N -местную функцию-распознаватель, реализованную на некотором языке программирования, можно автоматически транслировать на miniKanren, получив N + 1-местное отношение, связывающее аргументы функции с булевым значением [3] (истина соответствует успешному распознаванию). Зафиксировав значение N + 1-ого булевого аргумента, можно выполнять поиск. Ценность такого подхода в его простоте: решение задачи поиска всегда труднее, чем реализация распознавателя.
К сожалению, выполнение отношения в обратном направлении обычно крайне не эффективно. В [3] для решения этой проблемы используется специализация.
1Официальный сайт языка Mercury: https://mercurylang. org/, дата последнего посещения: 15.02.2020
2Официальный сайт языка miniKanren: http://minikanren. org/, дата последнего посещения: 15.02.2020 В статье показано, что специализация приводит к су- miniKanren же является чистым: все языковые конщественному приросту скорости работы программы. струкции обратимы. Однако чтобы избавиться от всех накладных расходов, Программа на miniKanren состоит из набора опресвязанных с интерпретацией программы, необходим делений отношений и цели. Определение имеет имя, Джонс-оптимальный специализатор [5]. К сожалению, список аргументов и тело. Тело отношения является реализация такого специализатора нетривиальная целью, которая может содержать унификацию термов задача. и вызовы отношений, скомбинированные при помощи В данное время авторами ведется работа над аль- дизъюнкций и конъюнкций. Терм представляет собой тернативным подходом улучшения производительно- или переменную, или конструктор с именем и списком сти программы в заданном направлении. Для этого подтермов. Свободные переменные вводятся в область по отношению с фиксированным направлением гене- видимости при помощи конструкции f resh. Абстрактрируется функция на функциональном языке програм- ный синтаксис языка приведен ниже: мирования Haskell. Таким образом можно избежать Goal : Goal ∨ Goal затрат на интерпретацию. Особенностью реляционного программирования является отсутствие строго поряд- | Goal ∧ Goal ка исполнения программы: особенно сильно он может | T erm ≡ T erm отличаться для разных направлений. Это затрудняет | call N ame [T erm] трансляцию в функциональные языки программирова- | f resh [V ar] Goal ния. Для успешной трансляции необходимо определить порядок исполнения программ с учётом направления. T erm : V ar Для решения такой задачи используется анализ време- | cons N ame [T erm] ни связывания (binding time analysis). Функционально- Пример программы на языке miniKanren, связывалогический язык программирования Mercury исполь- ющей три списка, где третий является конкатенацией зует анализ времени связывания как шаг компиля- первых двух, приведен на рис. 1. Для краткости [] ции [6], однако для реляционных языков такой анализ заменяет пустой список (cons N il []); h : t обозначает ранее не применялся. В данной статье мы представ- список с головой h и хвостом t (cons Cons [h, t]), а ляем алгоритм времени связывания для реляционного [x0, x1, . . . , xn] список с элементами x0, x1, . . . , xn. программирования. Вызов отношения call relation [t0, . . . tk] записывается В разделе II мы описываем язык miniKanren, ис- как relation t0 . . . tk. пользуемый в статье. Раздел III описывает схему его трансляции в функциональный язык и возникающие appendo x y z = при этом трудности. Алгоритм анализа времени связы- ( x ≡ [ ] ∧ y ≡ z ) ∨ вания для miniKanren приведен в разделе IV. Обзор ( f r e s h [ h , t , r ] ( литературы в разделе V. В заключении (раздел x ≡ h : t ∧ VI) подведены итоги и описаны планы на дальнейшую z ≡ h : r ∧ работу. appendo t y r Семейство языков miniKanren дало рождение парадигме реляционного программирования. Это минималистичные языки, встраиваемые в языки программирования общего назначения. Помимо простоты использования при разработке конечных приложений, miniKanren реализует полный поиск: все существующие решения будут найдены, пусть и за длительное время. Классический представитель родственной парадигмы логического программирования Prolog этим свойством не обладает: исполнение программы может не завершиться, даже если не все решения были вычислены. Незавершаемость программ на Prolog свойство стратегии поиска решения. Для устранения потенциальной нетерминируемости используются нереляционные конструкции, такие как cut. Эта особенность существенно усложняет и часто делает невозможным исполнение в обратном направлении. Язык Рис. 1. Пример программы на miniKanren Исполнение этого отношения в прямом направлении на двух заданных списках appendo [1, 2] [3] ? вернёт их конкатенацию [1, 2, 3]. Если исполнить его в обратном направлении, оставив первые два аргумента неизвестными, мы получим все возможные разбиения данного списка на два: результатом appendo ? ? [1, 2, 3] является множество пар {([], [1, 2, 3]), ([1], [2, 3]), ([1, 2], [3]), ([1, 2, 3], [])}.
III. Трансляция в функциональный язык В этом разделе мы кратко опишем разрабатываемую авторами трансляцию miniKanren в функциональный язык программирования, чтобы продемонстрировать, на решение каких проблем нацелен анализ времени связывания. Мы будем использовать Haskell в качестве целевого языка. татов F : Xi0 → · · · → Xik → [Xj0 × · · · × Xjl].
Любое отношение можно преобразовать в нормальную форму (для упрощения повествования мы будем считать, что все цели нормализованы). Нормальной формой будем называть дизъюнкцию конъюнкций вызовов отношений или унификаций термов, в которой все свободные переменные введены в область видимости в самом начале:
Goal : f resh [N ame] (_ ^ Goal0) Goal0 : call N ame [T erm]
| T erm ≡ T erm Транслятор строит одну функцию для каждого дизъюнкта. Дизъюнкты в программе на miniKanren независимы, то есть все ответы из каждого дизъюнкта объединяются для получения результата выполнения Рис. 3. Результат трансляции appendo ? ? z Нетрудно заметить, что порядок вычислений в функциях нередко не совпадает с порядком конъюнктов в исходном отношении. Например, рекурсивный вызов отношения appendo производится в последнем конъюнкте (см. рис. 1, строка 6), в то время как в функциях выполняется в первую очередь. Если отношение вызывает более одного отношения, то необходимо не только определить порядок, в котором необходимо вызывать функции в результате трансляции, но и в каком направлении это делать. Примером может служить отношение reverso (см. рис. 4), связывающее список со списком его элементов в обратном порядке. Это отношение имеет рекурсивный вызов, а также вызов отношения appendo. Порядок вызовов здесь влияет на направления функций, построенных по этим отношениям. Выбранные направления также могут влиять на то, в каком порядке необходимо вызывать функции.
Эти особенности диктуют необходимость использования некоторого статического анализа, позволяющего упорядочить вычисления в заданном направлении.
3Описание do-нотации языка Haskell: https://en.wikibooks. org/wiki/Haskell/do_notation, дата последнего посещения: 15.02.2020 Анализ времени связывания часто используется при построении offline-специализаторов языков программирования. Его задачей является определить, являются ли данные, используемые в программах, статическими (известными заранее) или динамическими (известными только во время вычисления). Использование анализа времени связывания при функциональной трансляции может также определить порядок вычисления, а по нему направления, в которых необходимо транслировать используемые отношения.
IV. Анализ времени связывания для
miniKanren Цель анализа времени связывания указать порядок, в котором имена связываются со значениями. Алгоритм принимает на вход программу на miniKanren и данные о том, какие переменные считаются входными. В результате работы алгоритма каждой переменной ставится в соответствие положительное число, обозначающее время связывания этой переменной. Мы будем называть процесс подбора чисел аннотированием.
Если о переменной ничего неизвестно, она аннотируется U ndef ; иначе указывается время связывания: целое положительное число. В начале работы алгоритма известными являются переменные, указанные как входные они аннотируются числом 0. Если переменная унифицируется с константой (термом, не содержащим свободных переменных), то мы считаем 1 её временем связывания. Если переменная унифицируется с термом, каждая свободная переменная которого аннотирована, мы аннотируем эту переменную числом 1 + n, где n максимальная аннотация свободных переменных терма. Таким образом мы распространяем информацию о времени связывания на непроаннотированные переменные.
На аннотациях имеется порядок: естественный порядок на положительных числах, при этом U ndef считается меньше любой числовой аннотации. Ранее проаннотированная переменная может получить другую аннотацию, если появилась какая-то новая информация о её времени связывания. При этом аннотация никогда не заменяется на меньшую. Рис. 5. Полурешетка на аннотациях A. Алгоритм анализа времени связывания
Реализация разработанного алгоритма доступна на сайте GitHub4. Ниже приведено описание алгоритма.
Входные данные алгоритма: программа на miniKanren (цель) и список входных переменных. Выходные данные пара из проаннотированной нормализованной (приведенной к дизъюнктивной нормальной форме) цели и списка проаннотированных определений отношений, вызываемых целью. Мы будем называть этот список стеком вызова, потому что в нем будут находиться вызываемые отношения.
При инициализации алгоритма выполняются следующие действия: • все f resh-переменные уникально переименовыва
ются, чтобы избежать перекрытия имен; • цель приводится в дизъюнктивную нормальную
форму; • все входные переменные аннотируются 0; • создается пустой стек вызовов.
Каждый раз при обработке вызова отношения анализуруется его тело, при этом: • f resh-переменные уникально переименовываются; • цель приводится в нормальную форму; • производится первичное аннотирование цели дан
ными о входных переменных.
Аннотация цели осуществляется итеративно, пока не будет достигнута неподвижная точка функции, описывающей шаг аннотирования. За один шаг мы аннотируем либо одну унификацию, либо один вызов отношения. Для аннотации цели в нормальной форме необходимо проаннотировать все её дизъюнкты. Аннотации переменных в дизъюнкте должны согласовываться: одна и та же переменная в конъюнктах одного дизъюнкта должна иметь одну и ту же аннотацию. Конъюнкты аннотируются в заранее определенном порядке. Сначала мы аннотируем унификации, а затем вызовы отношений. Каждый раз при аннотации новой переменной необходимо установить ту же аннотацию всем другим вхождениям этой переменной в дизъюнкте.
4Исходный код алгоритма аннотирования: https://github. com/Pluralia/uKanren_translator, дата последнего посещения: 15.02.2020 При аннотировании унификаций возможны следующие случаи. Здесь и далее аннотация переменной указывается в верхнем индексе.
• Вызов с таким именем и согласованным направлением уже есть в стеке вызовов заменить U ndef аннотации переменных на n + 1, где n максимальная аннотация переменных согласованного направления. • Вызова с таким именем и направлением нет в стеке вызовов. В этом случае мы сначала добавляем его и направление в стек вызовов. Затем аннотируем тело вызываемого отношения с учётом обновленного стека. По завершении аннотации добавляем в стек проаннотированную цель.
Помимо унификации конъюнкт может быть вызовом некоторого отношения на частично проаннотированных термах. Для аннотации вызова мы рассматриваем тело соответствующего отношения и аннотируем его. Для избежания повторного аннотирования информация о ранее проаннотированных в конкретных направлениях отношениях сохраняется в стеке вызовов. Если частично определенное направление текущего вызова согласовано с ранее проаннотированным, анализировать его не нужно. Два направления назовем согласованными, если при попарном сравнении аннотаций их аргументов аннотации одного направления будут всегда не меньше соответствующих аннотаций другого.
Для иллюстрации понятия согласованных направлений рассмотрим следующие примеры. Пусть есть отношение ro с частично определенными направлениями: ro x0 y0 zUndef и ro x1 y0 zUndef . Они являются согласованными, так как аннотации переменной x упорядочены правильно (0 < 1), а для y и z аннотации совпадают. При этом, направление ro x3 y2 z0 не согласовано с направлением ro x0 y0 z2, так как аннотации x и y больше в первом направлении, а z во втором.
При аннотации вызовов отношений возможны следующие случаи.
• Переменные всех аргументов проаннотированы
U ndef . В этом случае для аннотирования не достаточно информации, поэтому следует перейти к аннотации следующего конъюнкта. • Вызов полностью проаннотирован, то есть аннотация всех переменных числа. Здесь дальнейшая аннотация не требуется.
При получении такого отношения алгоритм аннотирования возвращает частично проаннотированную цель (некоторые переменные будут иметь аннотацию U ndef ). В этом случае мы запускаем алгоритм еще раз, изменив порядок вызова отношений в соответствующем дизъюнкте. Если и при другом порядке в аннотированной цели останутся U ndef -переменные, цель считается неаннотируемой.
Предложенный алгоритм терминируется, так как повторное аннотирование отношений не производится. Имеющиеся в стеке вызовов отношения не аннотируются снова, а в каждом отношении используется конечное количество уникальных переменных. Это значит, что каждому отношению можно сопоставить конечное количество уникальных аннотаций.
B. Примеры аннотирования
В этом разделе приведено несколько примеров аннотирования отношений. Числа над переменными обозначают аннотации. 1) Отношение appendo в прямом направлении: В данном случае переменные x и y являются входными. При начале работы алгоритма, таких отношения и направления нет в стеке вызовов, поэтому добавим их и запустим рекурсивно аннотирование цели appendo. Проаннотированное appendo приведено на рис. 7. Так как x и y входные переменные, их аннотации нам известны. Аннотация первого дизъюнкта тривиальна, поэтому рассмотрим второй. Аннотации h и t в строке 40 можно установить, так как известна аннотация x. Аннотация h распространяется на 41 строку, а аннотация t на 42 строку. Рекурсивный вызов отношения в строке 42 согласован с имеющимся в стеке, поэтому можно проаннотировать переменную r. Распространяем аннотацию r в строке 41. На последнем шаге аннотируем z в строке 40.
После аннотации обоих дизъюнктов остается определить аннотации исходного отношения. Для этого каждому аргументу мы присваиваем аннотацию, равную максимальной его аннотации среди всех дизъюнктов. В первом дизъюнкте переменная z имеет аннотацию 1, а во втором 3, поэтому результирующая аннотация равна 3. 2) Отношение appendo в обратном направлении: В этом случае мы считаем переменную z входной (см. рис. 8). Пусть appendo уже в стеке и z проаннотирована. В первом дизъюнкте x и y имеют аннотацию 1: y унифицируется со входной переменной z, а x с константой. Во втором дизъюнкте на первом шаге становятся известны аннотации h и r (строка 48). Аннотация r распространяется на строку 49. Отношение с согласованным направлением есть в стеке, поэтому можно аннотировать t и y. Далее аннотация t распространяется на строку 47, и на последнем шаге аннотируется x.
3) Отношение reverso в обратном направлении: Отношение reverso связывает два списка, получающиеся переворачиванием друг друга. Его определение приведено на рис. 9.
Добавим reverso по обратному направлению в стек вызовов и проинициализируем y как входную переменную. Рассмотрим второй дизъюнкт. На первом шаге можно попытаться проаннотировать только вызов appendo в строке 56 известна y. Такого отношения в Рис. 9. Аннотирование reverso в обратном направлении
V. Обзор существующих решений Анализ времени связывания часто используется при offline-специализации программ [5]. В этом случае он используется для определения того, какие данные известны статически и должны быть учтены при специализации, а какие неизвестны. Также часто определяется, какие функции вообще следует специализировать и каким образом. В зависимости от цели применения могут выбираться разные домены времен связывания. Анализ времени связывания существует для логического языка Prolog [7] и функционального-логического языка Mercury [6] представителей родственных реляционному программированию парадигм.
В языке Mercury анализ времени связывания [6] используется для эффективной компиляции. При этом используются только аннотации in и out статические и динамические переменные. Этого недостаточно, чтобы определить порядок вычислений при трансляции в функциональный язык. Определение порядка вычислений в Mercury осуществляется во время более трудоемкого анализа модов (mode analysis), не существующего для miniKanren. При этом непосредственное использование этого подхода для miniKanren невозможно, так как не все языки семейства типизируемы, а
Рис. 8. Аннотирование appendo в обратном направлении стеке вызовов нет добавляем и вызываем аннотирование. Это и есть вызов appendo в обратном направлении, рассмотренный выше (см. рис. 8). Аннотирование appendo позволяет определить аннотации переменных r и h распространяем их по другим конъюнктам. На следующем шаге вычисляем аннотацию переменной t рекурсивного вызова reverso, так как он уже есть в стеке (см. строку 55). Распространяем аннотацию t и аннотируем x на следующем шаге в строке 54.
reverso x5 y0 = ( x1 ≡ [ ] ∧ y1 ≡ [ ] ) ∨ ( f r e s h [ h , t , r ] ( x5 2 : t4 ∧ reve≡rsoh t4 r3 ∧ appendo r3 [h2] y0 ) ) анализ времени связывания Mercury осуществляется направления вычисления отношений, что влияет на с учётом графа типов, построенного по программе. эффективность алгоритма.
Система LOGEN реализует анализ времени связы- По проаннотированной программе можно получить вания для чистого подмножества Prolog [7]. Основное порядок, в котором необходимо привести определения предназначение анализа в этой работе улучшение переменных и вызовы функций в сгенерированном кокачества специализации, это решение нельзя исполь- де. В дальнейшем мы планируем интегрировать анализ зовать для определения правильного порядка вызовов времени связывания в транслятор в функциональный отношений. язык.
Работа [8] описывает анализ времени связывания для лямбда-исчисления с функциями высшего порядка. Его Список литературы цель также в том, чтобы определить порядок связыва- [1] Z. Somogyi, F. Henderson, and T. Conway, “The execution ния переменных, поэтому авторы используют отрезок aplrgoogrriathmmminogf lmanegrcuuargye,,” aTnheeffiJcoiuernntalpuorfelLyogidcecPlarroagtriavmemloinggic, натурального ряда {0, 1, . . . , N }. Мы использовали эту vol. 29, no. 1, pp. 17 – 64, 1996, high-Performance идею в нашей работе. Помимо этого работа [8] описыва- Implementations of Logic Programming Systems. ет локальный подход для анализа времени связывания, [2] cJo.rHeefmorarnenlaatniodnaDl.pPr.ogFrraiemdmmianng,,”“u2k0a1n3r.en: A minimal functional который дает более точные результаты. Адаптация это- [3] P. Lozov, E. Verbitskaia, and D. Boulytchev, “Relational го подхода для miniKanren предмет дальнейшего interpreters for search problems,” in Relational Programming исследования. [4] WWo.rkEs.hoBpy,r2d0,19U, .p.B4a3l.lantyne, U. Rosenblatt, and M. Might, VI. Заключение “A unified approach to solving seven programming problems (functional pearl),” in Relational Programming Workshop, 2017.
В статье мы представили алгоритм анализа времени [5] N. D. Jones, C. K. Gomard, and P. Sestoft, Partial evaluation связывания для miniKanren. Он определяет порядок, and automatic program generation. Peter Sestoft, 1993. в котором связываются переменные данного отноше- [6] aWn.alVysainshfoorofm, eMrc.urByr,u”yinnoPorgohgrea,manDdevMel.opLmeuesncthienl,C“oBmipnudtiantgi-otnimale ния с учётом направления его вычисления. Logic. Springer, 2004, pp. 189–232.
Основной его недостаток полный перебор при ан- [7] M. Leuschel, S.-J. Craig, M. Bruynooghe, and W. Vanhoof, нотации не аннотированных ранее переменных в слу- 3“0S4p9e,c0ia1li2si0n0g4,ipnpte.r3p4r0et–e3r7s5.using offline partial deduction,” vol. чае их использования только в вызовах отношений. [8] P. Thiemann, “A unified framework for binding-time analysis,” in В этом случае необходимо перебрать все возможные TAPSOFT, 1997.
Binding-Time Analysis for Relational Programs
Abstract Programs in relational programming are mathematical relations. Such relations can be run in different directions: by providing some arguments of a program, one can compute the values of the others. The execution of a program in the given direction is not always efficient. One way to improve the performance of a relational program is to convert it into a functional program. To create a function by a relation, it is necessary to determine the order in which names within the input program are bound with respect to the given direction. Binding-time analysis is used to solve this problem in the area of program specialization, but it has not been created for relational programming before. In this paper we propose a binding-time analysis algorithm for the relational programming language miniKanren.
Index Terms Relational programming, binding-time analysis, static analysis