= ВОСЬМАЯ ЕРШОВСКАЯ КОНФЕРЕНЦИЯ ПО ИНФОРМАТИКЕ (ПСИ'11) =
УДК 681.3.06
СУПЕРКОМПИЛЯЦИЯ ВЫСШЕГО УРОВНЯ КАК ПУТЬ К МЕТАСИСТЕМНОМУ ПЕРЕХОДУ
© 2012 г. И. Г. Ключников, С. А. Романенко,
Институт Прикладной Математики им. М. В. Келдыша РАН 125047 Москва, Миусская пл., 4 E-mail: ilya.klyuchnikov@gmail.com, romansa@keldysh.ru Поступила в редакцию 01.12.2011
Обсуждаются вопросы, связанные с метасистемными переходами в контексте суперкомпиляции. Рассматривается, как закон разрастания предпоследнего уровня проявляется в области суперкомпиляции высшего уровня, и предлагаются некоторые подходы к построению метасистем на базе суперкомпиляторов, использующие этот закон. В частности, показывается полезность многорезультатной суперкомпиляции в таких областях, как доказательство эквивалентности выражений и двухуровневая суперкомпиляции.
1. ВВЕДЕНИЕ
Суперкомпилятор представляет собой преобразователь программ БС, который основан на методе суперкомпиляции [1, 2, 3], и который для заданной программы р порождает остаточную программу р = БС[р]. Суперкомпиляция чаще всего рассматривается как метод оптимизации программ, однако может применяться и для выявления и доказательства свойств программ. Поскольку областью наших интересов является применение суперкомпиляции для анализа программ, мы в данной работе предполагаем, что все рассматриваемые суперкомпиляторы полностью сохраняют семантику программ (в том смысле, что для заданных исходных данных, исходная и преобразованная программы либо обе не завершаются, либо выдают один и тот же результат).
Общая идея метасистемного перехода была сформулирована В.Ф. Турчиным [4, Глава 3.1, "Метасистемный переход"]:
Систему, состоящую из управляющей подсистемы X и управляемых ею многих однородных подсистем А\, А2, А3, ..., мы назовем метасистемой по отношению к системам А1, А2, А3, .... Переход с этапа на этап мы назовем,
следовательно, метасистемным переходом.
В контексте суперкомпиляции метасистемный переход, в частности, возникает, когда акт суперкомпиляции SC начинает рассматриваться как "элементарная операция" и используется в качестве "строительного блока" для создания более сложных систем [5, 3].
Общепринятого термина для разнообразных систем, построенных из суперкомпиляторов на основе метасистемного перехода, пока не существует. За неимением лучшего, мы будем использовать термин суперкомпиляция высшего уровня (higher-level supercompilation).1
Суперкомпиляция высшего уровня - новая область исследования, и некоторые её аспекты пока недостаточно поняты и осознаны. Один из таких аспектов - закон разрастания предпоследнего уровня при метасистемном переходе. Конечно, законы потому и называются "законами", что они проявляются объективно, вне зависимости от того, осознаем мы их или нет. Однако, понимание и сознательное использование законов часто позволяет нахо-
1 Сам В.Ф. Турчин предлагал использовать термин "метавычисления" [3], который в настоящее время приобрёл более широкое значение, и применяется не только к суперкомпиляции.
дить более ясные и (концептуально) простые решения для конкретных задач, вместо того, чтобы действовать вслепую или методом проб и ошибок.
В последующих разделах мы рассматриваем, как закон разрастания предпоследнего уровня реально проявляется в области суперкомпиляции высшего уровня, и предлагаем новые подходы к построению метасистем на базе суперкомпиляторов, использующие этот закон.
2. ПРИНЦИПЫ ТРАДИЦИОННОЙ СУПЕРКОМПИЛЯЦИИ
Первоначально суперкомпиляция была разработана В.Ф. Турчиным для конкретного языка программирования Рефал (функциональный язык первого порядка с вызовом по имени) [2], и первые суперкомпиляторы разрабатывались и реализовыва-лись для языка Рефал [6, 7, 8].
Это создавало впечатление, что суперкомпиляция - это весьма специфический метод анализа и преобразования программ, предназначенный для языка Рефал (и близких к нему языков).
Дальнейшее развитие суперкомпиляции привело к более абстрактной переформулировке суперкомпиляции, что позволило выяснить, какие части первоначальной формулировки были обусловлены спецификой языка Рефал, а какие - применимы и к другим языкам программирования [9, 10, 11]. В частности, была показана применимость суперкомпиляции для нефункциональных (императивных и объектно-ориентированных) языков программирования [12].
В результате было осознано различие между "суперкомпиляцией" и "суперкомпилятором". Суперкомпиляция - это общий метод, который применим к широкому классу языков программирования, а суперкомпилятор -это конкретный преобразователь программ, основанный на принципах суперкомпиляции. При разработке конкретного суперкомпилятора требуется пройти через следующие этапы.
котором будут выдаваться остаточные программы, в случае, если входной язык суперкомпилятора не совпадает с его выходным языком.
• Для входного языка - выбрать некоторый вариант операционной семантики. Это необходимо вследствие того, что прогонка является формой "исполнения" программы в случае, когда обрабатываемые данные известны лишь частично, и вырождается в обычное исполнение программы, если данные полностью известны. Поэтому, прогонка является обобщением по отношению к конкретной форме операционной семантики.
• Разработать (или выбрать) язык конфигураций (для описания множеств состояний вычислительного процесса). Реализовать операции над конфигурациями (такие, как распознавание эквивалентности и вложенности множеств, изображаемых конфигурациями).
• Разработать алгоритм прогонки (обобщающий процесс вычислений над конкретными состояниями для вычислений над конфигурациями), в основе этого алгоритма прогонки лежит выбранный ранее вариант операционной семантики.
• Разработать (или выбрать) алгоритмы, обеспечивающие свёртку бесконечных (в общем случае) деревьев конфигураций (порождаемых прогонкой) в конечные графы конфигураций. Эти задачи в конкретном суперкомпиляторе должны решать свисток (распознающий потенциально бесконечные ветви в дереве конфигураций) и алгоритм обобщения (заменяющий конфигурации на более общие).
• Разработать алгоритм построения остаточной программы на основе конечного графа конфигураций.
• Выбрать объектный язык программирования, Таким образом, в то время как на начальных программы на котором будет обрабатывать этапах развития суперкомпиляции речь шла о суперкомпилятор. А также и язык на конкретном "суперкомпиляторе", в настоящее
время стало очевидно, что более правильно говорить о "суперкомпиляторах".
3. НОВЫЕ РАЗНОВИДНОСТИ СУПЕРКОМПИЛЯЦИИ
В последнее время, наряду с "классической" суперкомпиляцией, начали появляться новые разновидности суперкомпиляции: такие как дистилляция [13, 14], двухуровневая суперкомпиляция [15, 16] и многорезультатная суперкомпиляция [17, 18].
При этом следует отметить, что хотя изначально суперкомпиляция рассматривалась В.Ф. Турчиным и как средство оптимизации, и как средство анализа программ [1], работы в области суперкомпиляции долгое время были, главным образом, посящены применениям суперкомпиляции для оптимизации программ. В последнее время, однако, наблюдается возвращение интереса к применению суперкомпиляции в качестве средства выявления и доказательства свойств программ [19, 20, 21].
Таким образом, мы, вполне возможно, присутствуем при рождении таких направлений как языково-ориентированная (language-specific) и проблемно-ориентированная (domain-specific) суперкомпиляция. При этом подробности реализации общей идеи суперкомпиляции зависят как от обрабатываемого языка, так и от предполагаемой области применения суперкомпилятора.
В связи с этим меняется и сама парадигма исследований в области суперкомпиляции. До недавнего времени целью работы было изготовление конкретного суперкомпилятора и смысл работы состоял в том, чтобы найти "самый лучший" вариант для различных частей суперкомпилятора. Однако теперь выясняется, что то, что хорошо для одного языка или области применения, может не очень подходить для других языков и областей применения.
Возникает новая задача: систематическое исследование разнообразных форм и методов суперкомпиляции, а также их применимости (в различных комбинациях) в различных областях. В качестве примера можно привести исследование, в котором изучалось влияние различных деталей алгоритма суперкомпиляции на его способность доказывать эквивалентности
выражений высшего порядка [22]. При этом сравнивалось поведение 64-х вариантов суперкомпилятора.
4. РАЗНООБРАЗИЕ ФОРМ СУПЕРКОМПИЛЯЦИИ ВЫСШЕГО УРОВНЯ
Как мы упоминали выше, под суперкомпиляцией высшего уровня мы понимаем построение некоторой системы, в которой операция суперкомпиляции SC используется в качестве "первичной" (primitive). В качестве примеров суперкомпиляции высшего уровня можно привести:
• Самоприменение суперкомпиляторов [23] (в духе проекций Футамуры [24]), или, в более общем случае, применение суперкомпиляторов к суперкомпиляторам [25]. В таких случаях, по сути, один экземпляр суперкомпилятора контролирует исполнение другого экземпляра суперкомпилятора.
• Доказательство эквивалентности выражений с помощью суперкомпиляции [26, 20]. При этом суперкомпиляция используется в качестве средства "нормализации" программ, с последующей проверкой, что они синтаксически изоморфны.
• Двухуровневая суперкомпиляция [15], при которой "верхний" суперкомпилятор применяет улучшающие леммы, справедливость которых доказывается с помощью "нижнего" суперкомпилятора.
• Дистилляция [13, 27, 14], в процессе которой сопоставляются не выражения, а их рекурсивные (суперкомпилированные) представления (хотя разделение между основным уровнем и метауровнем при дистилляции является не столь очевидным, как при многоуровневой суперкомпиляции).
Из этого (заведомо неполного) списка хорошо видно, что построение метасистем на основе суперкомпиляции может делаться самыми различными способами. По историческим причинам, до недавнего времени, наибольшей популярностью пользовалась идея самоприменения суперкомпилятора (и
связанные с ней проекции Футамуры). Самоприменение можно рассматривать как особую форму исполнения одного экзем
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.