Специализация функциональных программ методами суперкомпиляции (по материалам диссертации) Андрей Петрович Немытых Институт Программных Систем РАН.

Реализация функционального языка

Задача специализации

Исторические замечания 70-е годы XX века –А.П. Ершов (смешанные вычисления). –В.Ф. Турчин (суперкомпиляция). –Ё. Футамура (generalized partial computation). 80-е годы XX века –Н.Д. Джонс (частичные вычисления)

Суперкомпиляция и частичные вычисления Частичные вычисления: –разделение алгоритмически разрешимой части подзадач и алгоритмически неразрешимой (аппроксимирующей) части подзадач; –сохранение определения частичной функции определяемой специализированной программы. Суперкомпиляция: –трудности в неразделённости алгоритмически разрешимых и неразрешимых частей; они же дают потенциально существенно более сильные методы специализации.

Блок схема алгоритма суперкомпиляции

Прогонка –Мета-аналог одного шага РЕФАЛ машины a x + b = 0 driving a x + b = 0 x = -b/a; a 0 b = 0 any x Ø a =? 0 a ? 0 b =? 0 b ? 0

Глобальный анализ по ходу дела (online) специализации – компоненты факторизации с пустой областью определения; – построение выходных форматов; – частично рекурсивные константы; – частично рекурсивные проекции; – частично рекурсивные тождественные функции; – частично рекурсивные мономы конкатенации;

Специализация компонент факторизации по глобальным свойствам (использование результатов глобального анализа) $ENTRY Go { e.n = ; } Fact1 { () = (I); (e.n) = ( )>>); } Times { (e.u) ( ) = ; (e.u) (I e.v) = ) (e.u)>; }

Пример вычисления выходного формата $ENTRY Go { e.n = ; } UnarySum { (e.n) (I e.m) = I ; (e.n) ( ) = e.n; } * I e.k

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

Достоточное условие тождественности

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

Пример программы на языке Refal n * Частичный моном приписывания. * = e.x e.x $ENTRY Copy { e.x = ; } Double { s.1 e.x, e.y = s.1 ;, e.y = e.y; }

Формальный повышатель арности

Пример формального повышения арности

Синтаксические мономы приписывания

Достаточное условие мономиальности

Пример синтаксического монома * = e.x e.y e.x $ENTRY Double { s.1 e.x, e.y = s.1 ;, e.y = e.y; }

Стратегия выбора гипотезы мономиальности На основании пассивных правых частей: они являются базисными случаями выхода из рекурсии. Пассивные правые части не меняются при определённых ранее преобразованиях. В Double (пример на пред. слайде) существует бесконечно много гипотез вида: e.x k e.y e.x m

Достаточное условие конечности числа гипотез

Применение Динамическая типизация данных. Задачи самоприменения: – холостые проходы функции подстановки и т.п. – пример (поиск вызова функции):

Математическая индукция и свойства обобщения конфигураций Выбор конфигураций для обобщения: –вариант упрощающего предпорядка Higman-Kruskal-а; –монотонность по функциям-конструкторам: F 1 (t 1,t 2 ) = t 1 t 2, F 2 (t 1 ) = (t 1 ), F f (t 1 ) = t 1 F 1 (t 1,t 2 ), t 2 F 1 (t 1,t 2 ), t 1 F 2 (t 1 ), t 1 F f (t 1 ) –согласованность с функциями-конструкторами: t 1 t 2 F 2 (t 1 ) F 2 (t 2 ), F f (t 1 ) F f (t 2 ) t 1 t 2 F 1 (t, t 1 ) F 1 (t, t 2 ), F 1 (t 1, t) F 1 (t 2, t) –отделение базисных случаев индукции от регулярных: () (SYMBOL), () (s.variable) Основное свойство: –Для любой бесконечной последовательности термов t 1, t 2, … существует пара t i, t k, такая что i < k и t i t k.

Приложение Удачные эксперименты по верификации протоколов когерентности кэш-памяти (cache coherence) с глобальными свойствами: –IEEE Futurebus+, MOESI, MESI, MSI, The University of Illinois, DEC Firefly, Berkeley, Xerox PARC Dragon. А также параметризованных протоколов: –Java Meta-Locking Algorithm, Reader-Writer protocol, Steve German's directory-based consistency protocol. Ряд успешных экспериментов по верификации по постусловию модельных протоколов описанных в формализме сетей Петри.

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

Основные результаты-II Разработан и реализован алгоритм построения выходных форматов компоненты факторизации F метадерева возможных вычислений в режиме online (по ходу дела суперкомпиляции); что позволяет сразу использовать построенный формат для специализации по нему как других компонент-функций, вызывающих функцию F, так и самой функции F. Показано, что на некоторых примерах этот алгоритм способен понижать временную сложность программы. Предложено понятие частично рекурсивного монома конкатенации. Доказана теорема о достаточном условии частично рекурсивного монома конкатенации. Разработана стратегия выбора гипотезы мономиальности. На основании этих теоремы и стратегии разработан и реализован алгоритм, распознающий частично рекурсивные синтаксические мономы конкатенации. Показано, что на некоторых примерах этот алгоритм способен понижать временную сложность программы с экспоненциальной до константной O(1). Показано, что этот алгоритм может быть использован в решении задачи самоприменения для понижения порядка временной сложности результата самоприменения.

Основные результаты-III Разработан и реализован экспериментальный автоматический суперкомпилятор SCP4, предметной областью которого является функциональный язык программирования РЕФАЛ-5. Демонстрация суперкомпилятора доступна на Web-странице в режиме on-line. Исследованы характеристики суперкомпилятора SCP4.

Характеристики суперкомпилятора SCP4.

Литература [1] Лисица А.П. и Немытых А.П., Работа над ошибками, Программные системы: теория и приложения, Физматлит, Том 1, стр , [2] Лисица А.П. и Немытых А.П., Верификация как параметризованное тестирование (Эксперименты с суперкомпилятором SCP4). ЖурналПрограммирование, 1, [3] Немытых А.П., Суперкомпилятор SCP4: Общая структура. Монография. Издательство УРСС, стр. [4] Korlyukov A.V. and Nemytykh A.P., Supercompilation of Double Interpretation. (How One Hour of the Machines Time Can Be Turned to One Second). Вестник национального технического университета Харьковского политехнического института, Том 1, стр , [5] Lisitsa A. P., and Nemytykh A.P., Verification of parameterized systems using supercompilation. In Proc. of the APPSEM05, Fraunchiemsee, Germany, September 2005.

Литература-II [6] Lisitsa A.P. and Nemytykh A.P., Towards verification via supercompilation. In Proc. of the COMPSAC2005, [7] Lisitsa A.P. and Nemytykh A.P., Reachability Analysis in Verification via Supercompilation, The Proc. of the Satellite Workshops of DTL 2007 / TUCS General Publication, No. 45, Part 2, pp Turku, Finland [8] Lisitsa A.P., and Nemytykh A.P., A Note on Specialization of Interpreters, LNCS, Vol. 4649, pp , The Proc. of CSR [9] Nemytykh A.P., Supercompiler SCP4: Use of quasi-distributive laws in program transformation, Wuhan University Journal of Natural Sciences, Vol. 95(1-2), pp , [10] Nemytykh A.P., A Note on Elimination of Simplest Recursions, The Proc. of Asia- PEPM02, pp ACM Press. Aizu, Japan

Литература-III [11] Nemytykh A.P., The Supercompiler SCP4: General Structure (extended abstract), LNCS, Vol. 2890, pp , The Proc. of the Perspectives of System Informatics [12] Nemytykh A.P., Playing on REFAL / The Proc. of the International Workshop on Program Understanding, pp Novosibirsk - Altai Mountains, [13] Nemytykh A.P., The Supercompiler SCP4: General Structure, Программные системы: теория и приложения, Физматлит, Том 1, стр , [14] Nemytykh A.P. and Turchin V.F., The Supercompiler SCP4: sources, on-line demonstration, [15] Turchin V.F. and Nemytykh A.P., Metavariables: Their implementation and use in Program Transformation // Technical Report CSc. TR , City College of the City University of New York, 1995.

Спасибо!