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

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

2 2 Реализация функционального языка Определение 1. Реализацией функционального языка программирования R назовём четвёрку, где множество P называется множеством R-программ, множество D называется множеством R-данных; частично рекурсивные функции U: P D D и T: P D N называются соответственно универсальной функцией (или семантикой) и сигнализирующей функцией времени языка R. Здесь N – множество натуральных чисел. Рассмотрим реализацию функционального языка программирования R = где D = n N M n для некоторого непустого множества M.

3 3 Задача специализации Пусть программа p(x,y) из P, определяет функцию F(x,y): X Y D, где X D, Y D. Зафиксируем значение первого аргумента этой функции x 0 X. В задаче специализации требуется построить другую программу q p (y) P такую, что y Y. (q p (y) = p(x 0, y)) (T(q p,y) T(p,x 0, y)). Таким образом, программа q p определяет некоторое продолжение функции F(x 0,y) по второй компоненте. Программу q p называют остаточной программой.

4 4 Простейший пример специализации Специализатор n 0 =10 p(n,m) q p (m) p(n,m) -- умножение натуральных чисел q p (m) = p(10,m) = m0

5 5 Пример специализации p(x,n) = x n, = 3*3 14 = 3*9 7 = 3*(3*9 6 ) = 3*(3*81 3 ) = 3*(3*(81*81 2 )) = 3*(3*(81*6561)) = в прямом алгоритме 14 умножений; в данном алгоритме 6 умножений; p(x, n 0 ) = p(x,2), n 0 = 2; p(x, 0) = 1; p(x, 2*n+1) = x*p(x, 2*n); p(x, 2*n+2) = p(x*x, n+1); Остаточная программа: q(x) = x*x

6 6 История вопроса 70-е годы XX века –А.П. Ершов (смешанные вычисления). –В.Ф. Турчин (суперкомпиляция). –Y. Futamura (generalized partial computation). 80-е годы XX века –N.D. Jones (частичные вычисления)

7 7Суперкомпиляция Основная цель суперкомпиляции: –выполнить как можно больше действий параметризованного применения программы равномерно по значениям параметров предыдущий узел...

8 8 Пример дерева развёртки программы (дерева конфигураций) S( n, 1+m) = 1+S( n, m ); S( n, 0 ) = n; S(n,m)1+S(n,m-1) m > 0 m =? 0 n 1+(1+S(n,m-2)) m-1 > 0 m-2 > 0..… m-1 =? 0 m-2 =? 0 1+n 2+n

9 9 Аппроксимация образа функции вычисление выходных форматов функций F(x,y) = g(h(x,y)), h(x,y) = x; F( x 0,y) = g( x 0 );.

10 10 Введение в РЕФАЛ (данные) РЕФАЛ (В.Ф. Турчин) строгий функциональный язык первого порядка, в котором конкатенация ассоциативна. Имеется также унарный конструктор для построения структура дерева. Семантика языка базируется на отождествлении по образцу и модели вычислений – алгорифмах Маркова. Данные РЕФАЛа определяются следующей грамматикой: d ::= (d 1 ) | d 1 d 2 | SYMBOL | empty empty ::= /* nothing */ Example:(A + B) * (C – D) * +-ABCD

11 11 Введение в РЕФАЛ (ассоциативность конкатенации) Palindrome { = True; s.1 = True; -- application constr. s.1 e.2 s.1 = ; e.1 = False; } * The palindrome predicate: Example 1: Example 2: (Refal style reversing) * Reversing a list of terms: rev { t.x e.ys = t.x; = ; -- empty expression } -- on the both sides. /* Reversing a list of terms: we may concatenate a term taken by the variable t.x right on the end of the list. The blank is used to denote the concatenation. */ /* Pattern may be split from both sides: a symbol-variable s.1 is split from the left and right sides. */

12 12 SCP4 как простой theorem prover Задача: $ENTRY Go { e.ls = >; } palindrome { = True; s.x = True; s.x e.ls s.x = ; s.x e.ls s.y = False; } rev { = ; t.x e.ls = t.x; } Результата специализации: доказано простое утверждение. $ENTRY Go { = True ; s.102 e.41 = True ; }

13 13 Использование SCP4 для упрощения определений Задача: Решить уравнение 'a' X = X 'a', где область допустимых значений переменной X есть множество конечных строк. $ENTRY Go { e.x = ; } Eq { (s.1 e.x) (s.1 e.y) = ; ((e.1) e.x) ((e.2) e.y) = ; () () = True; (e.x) (e.y) = False; } Упрощённое определение: построенное SCP4. Доказана простая теорема, описывающая множество решений исходного уравнения. $ENTRY Go { e.41 = ; } F7 { 'a' e.41 = ; = True ; e.41 = False ; }

14 14 Алгоритм Маканина и суперкомпиляция Задача: Решить уравнение сопряжения x y = z x в свободном моноиде. x y = z x x ' y = z x ' y = z ' x |x| |z| x z x ' |x| < |z| z x z ' x ' x Параметризация: z' = s, x = r, z = r s, y = s r, x = z n x' = (r s) n r.

15 15 Частично рекурсивные тождественные функции Частично рекурсивная функция F(x): D D тождественная на её области определения: x О.Д.З. F(x) = x

16 16 Достаточное условие тождественности F:, - множество пропозициональных формул. F( x ) = F(F( x )); F( x y ) = F( x ) F( F( y )); F( x y ) = F(F( F( x ))) F( y ); F( x y ) = F(F( x )) F(F( F( F( y )))); F( ) = ; После стирания всех метасимволов левые части равенств должны совпадать с правыми частями. Здесь переменные x, y пробегают множество пропозицио- нальных формул; переменная пробегает множество про- позициональных переменных.

17 17 Частично рекурсивные мономы приписывания Определение. Пусть D – множество конечных последова- тельностей символов (конечных строк символов). Частично рекурсивную функцию F:D n D назовём частичным моно- мом приписывания, если k 1, k 2,…, k m и j 1, j 2,…, j m такие, что k i N, s. j s N, n j s > 0 и (x 1, x 2,…, x n ) О.Д.З. Здесь операция умножения – приписывание строк; возведение в степень относится к той же операции.

18 18 Примеры рекуррентных определений частичных мономов приписывания F(x) = g(x, ); g( x, y) = g(x, y ); g(, y) = y; Здесь переменные x, y пробегают множество конечных строк символов; переменная пробегает множество символов. F(x) = x x g(x,y) = x y x

19 19 Пример формального повышения местности Переменные x, y пробегают множество g( x, y) = g(x, y ); конечных строк символов; переменная g(, y) = y; пробегает множество символов. g 2,1 ( x 1, x 2, y) g 2,1 ( x, x, y) = g 2,1 (x, x, y ); g 2,1 (,, y) = y; g(x,y) = g 2,1 ( x, x, y)

20 20Пример Переменные x, y пробегают множество g( x, y) = g(x, y ); конечных строк символов; переменная g(, y) = y; пробегает множество символов. (1) = 1, (2) = 3, (3) = 2 g 2,1 ( x, y, x) = g 2,1 (x, y, x); g 2,1 (, y, ) = y; g(x,y) = g 2,1 (x, y, x) = x y x g 2,1 ( x, y, x) = g 2,1 (x, y, x); g 2,1 (, y, ) = y;

21 21 Достаточное условие мономиальности Теорема. Пусть D – множество конечных строк символов. Пусть дано рекуррентное определение P частично рекурси- вной функции F:D n D. Предположим, что k 1, k 2,…, k m такие, что k i N и перестановка параметров определе- ния такая, что определение (программа) Q, полу- ченная из формальным стиранием запятых раз- деляющих аргументы, определяет частично рекурсивную тождественную функцию, тогда определение P определят частично рекурсивный моном приписывания.

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

23 23 Достаточное условие конечности числа гипотез Утверждение. Пусть в программе g существует хотя бы одно предложение g(p 1,..., p n ) =... такое, что правая часть не содержит g(...) и для всех k p k отличны от пустых строк. Тогда может существовать лишь конечное число гипотез, которые можно построить в рамках описанной выше стратегии.

24 24 Приложения. Доказательство свойств программ Верифицированы параметризованные протоколы когерентности кэш-памяти (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.

25 25 Структура доказательства корректности протокола MOESI (индукция по структуре данных) Theorem 1 Theorem 2 True2 Lemma $# # # $ $ $$$ True

26 26 Структура доказательства корректности программной модели протокола Dragon (индукция по структуре данных)

27 27 Структура доказательства корректности программной модели протокола Dragon (индукция по структуре данных)

28 28 Математическая индукция и свойства обобщения конфигураций Выбор конфигураций для обобщения: –вариант упрощающего отношения 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.

29 29 Верификация Xerox PARC Dragon cache coherence протокола В результате анализа остаточной программы обнаружена ошибка описания протокола: –G. Delzanno, Automatic Verification of Parameterized Cache Coherence Protocols. и построен тест, указывающий на ошибку. Удачно проверифицирована корректная версия описания этого протокола: –

30 30 Почему это происходит? (по поводу тезиса Чёрча) Конечный набор простейших операций, допускаемых в машине Тьюринга: –многообразие их композиций дает все алгоритмы. и в это трудно поверить. Аналогичная ситуация с суперкомпиляцией.

31 31 История вопроса 70-е годы XX века –А.П. Ершов (смешанные вычисления). –В.Ф. Турчин (суперкомпиляция). –Y. Futamura (generalized partial computation). 80-е годы XX века –N.D. Jones (частичные вычисления)

32 32 SCP4 as a simple theorem prover (идея Александра Корлюкова) Задача (по мотивам Л. Ф. Магнитцкого): Летит стая гусей. Навстречу ей гусь: Привет сотня гусей!. Вожак отвечает: Нас не сотня. Если всех нас сосчитать и прибавить ещё столько же, и пол-столько, и четверть-столько, да ещё и тебя, Гусь, тогда получится сотня. Вопрос: Сколько гусей в стае? $ENTRY Go { e.n = ) ( )>; } Eq { ( ) ( ) = TRUE; ('g' e.xs) ('g' e.ys) = ; (e.xs) (e.ys) = FALSE; } Hundred { = 'gggggggggggggggggggggggggggggggggggggggggggggggggg' 'gggggggggggggggggggggggggggggggggggggggggggggggggg' ; } Counter { 'gggg' e.n = 'gggg' 'gggg' 'gg' 'g' ; = 'g'; } Здесь 'gg' := 'g' 'g'

33 33 Вопрос: Сколько гусей в стае? Ответ данный суперкомпилятором SCP4: $ENTRY Go { 'gggggggggggggggggggggggggggggggggggggggg' e.n = FALSE ; * The following string has 36 of 'g' (of geese). 'gggggggggggggggggggggggggggggggggggg' = TRUE ; 'gggggggggggggggggggggggggggggggg' = FALSE ; * The length of the (n+3)-th left side is 36-4(n+1), * while the right side is FALSE.... = FALSE ; } Мы не только ответили на поставленный вопрос, но и доказали что других решений не существует. В процессе суперкомпиляции произошла индукция по e.n и рекурсия рекурсия данная в исходной программе удалена.

34 34 Более адекватная кодировка Counter { e.n = 'g'; } All { e.n = e.n; } Half { = ; 'gg' e.n = 'g' ; } Quoter { = ; 'gggg' e.n = 'g' ; } Остаточная программа подобна предыдущей, но содержит сто предложений.

35 35 Головоломка (Эйнштейн): ( идея использования Александра Корлюкова ) Имеются 5 домов раскрашенные в разные цвета, в каждом доме живёт один человек. Все они разной национальности, предпочтения к напиткам у всех разные, все они курят разные сорта сигарет и имеют слабость к совершенно разным животным. Дано: 1. Англичанин живёт в красном доме. 2. У шведа живёт собака. 3. Датчанин пьёт чай. 4. Зелёный дом – ближайший слева от белого дома. 5. Хозяин зелёного дома пьёт кофе. 6. Курящий сигареты PallMall держит птицу. 7. Жилец центрального дома пьёт молоко. 8. Хозяин жёлтого дома курит Dunhill. 9. Норвежец живёт в первом доме. 10. Поклонник Marlboro – сосед любителя кошек. 11. Любитель покататься на лошади – сосед фаната сигарет Dunhill. 12. Один из них предпочитает курить Winfield потягивая пиво. 13. Дом норвежца – соседний к синему дому. 14. Немец курит Rothmans. 15. Поклонник Marlboro соседствует с поклонником чистой водички. КТО Д Е Р Ж И Т Р Ы Б У ?

36 36 Вопрос: кто держит рыбку? Определение Z i есть переформулировка i-ого утверждения в терминах РЕФАЛа. LookForFish { (s.1 s.2 s.3 Fish s.5) e.b = s.1 ; (s.1 s.2 s.3 s.4 s.5) e.b = ; } * 1. Англичанин живёт в красном доме. Z1 { (Englishman Red s.3 s.4 s.5) e.b = (Englishman Red s.3 s.4 s.5) e.b; (e.1) e.b = (e.1) ; } * 2. У шведа живёт собака. Z2 { (Swede s.2 s.3 Dog s.5) e.b = (Swede s.2 s.3 Dog s.5) e.b; (e.1) e.b = (e.1) ; } * 3. Датчанин пьёт чай. Z3 { (Dane s.2 s.3 s.4 Tea) e.b = (Dane s.2 s.3 s.4 Tea) e.b; (e.1) e.b = (e.1) ; } …

37 37 Входная точка программы: $ENTRY Puzzle { e.buildings = >>> >; } Программа проверяет удовлетворяют ли выбранные входные данные условиям головоломки или нет. Если данные удовлетворяют условиям, То программа возвращает ответ на поставленный в головоломке вопрос, иначе программа попадает в ситуацию аварийной остановки (Отождествление невозможно).

38 38 Формулировка задачи и результат суперкомпиляции Параметризованная входная конфигурация: Параметр s.ij соответствует одному объекту в i-ом доме, каждая пара скобок представляет дом. Остаточная программа: $ENTRY Puzzle { (Norwegian Yellow Dunhill Cat Water ) (Dane Blue Marlboro Horse Tea ) (Englishman Red PallMall Bird Milk ) (German Green Rothmans Fish Coffee) (Swede White Winfield Dog Beer ) = German ; }

39 39 Фильтрация $ENTRY Puzzle { e.buildings = >>> >; } Порядок фильтров Z i может быть изменён. Время суперкомпиляции зависит от этого порядка. Число всех возможных вариантов перебора в Головоломке равно 5 25 (примерно ). Если компьютер будет перебирать со скоростью миллиард вариантов в секунду, то ему понадобится 9 лет. Суперкомпилятор (подобно PROLOG интерпретатору) сужает входные Параметры согласно образцам, данным в фильтрах, и обнаруживает что область определения состоит из одной точки; она и является ответом на вопрос. Дополнительный эксперимент показывает, что подсказку Z 15 можно убрать из описания головоломки: ответ тот же самый (немец).

40 40 Аппроксимация цикла в стеке функций: Обнинское условие Турчина Предполагаемое развитие стека функций: Top; Middle n ; Context Имена вызовов функций в стеке помечаются временем их создания - Previous и Current. Скажем, что эта пара стеков указывает на цикл, если стеки можно представить в виде: Previous = PreviousTop; Context; Current = CurrentTop; Middle; Context; где дно стеков есть совпадающий отрезок наибольшей длины, т.е. эта часть не участвовала в вычислении вдоль пути от одного стека до другого, а вершины стеков ( PreviousTop = F1 ptime_1, …, FN ptime_n CurrentTop = F1 ctime_1, …, FN ctime_n ) совпадают с точностью до времен создания. Context определяет вычисления сразу за циклом. Previous topContext Current topMiddle

41 41 Обнинское условие Турчина (пример) Определение унарного факториала. $ENTRY IncFact {e.n = )>; } Fact { ( ) = I; (e.n) = )>)>; } Times { (e.u) ( ) = ; (e.u) (I e.v) = ) (e.u)>; } Plus { (e.u) ( ) = e.u; (e.u) (I e.v) = I ; } Minus { (I e.u) (I e.v) = ; (e.u) ( ) = e.u; } Ленивое развитие стека вдоль главной ветви дает последовательность: [1]: IncFact 1 ; [2]: Plus 2 ; Гипотеза состоит в том, что стек [3]: Fact 4 ; Plus 3 ; далее будет иметь вид: [4]: Times 5 ; Plus 3 ; Fact; Times n ; Plus 3 ; [5]: Fact 7 ; Times 6 ; Plus 3 ; … Здесь стек, созданный на пятом шаге, "походит" на стек третьего шага.

42 42 Спасибо!