1 Кубенский А.А. Функциональное программирование. Глава 7. Комбинаторная редукция. Глава 7. Комбинаторная редукция Задача: избавиться от имен переменных. - презентация

1 1 Кубенский А.А. Функциональное программирование. Глава 7. Комбинаторная редукция. Глава 7. Комбинаторная редукция Задача: избавиться от имен переменных (и, соответственно, лямбда-выражений) введением чистого комбинаторного программирования, подобно тому, как это делалось в FP-системе. Введем следующие комбинаторы: Вычеркиватель (K): На самом деле тождественный комбинатор – лишний, легко убедиться, что I = S K K. S K K = λx.K x (K x) = λx.x = I K = λx.λy.x Распределитель (S): S = λf.λg.λx.f x (g x) Тождество (I): I = λx.x Для определения семантики этих комбинаторов нет нужды опираться на лямбда-выражения, лучше просто определить правила применения: S f g x = f x (g x) K x y = x I x = x Теперь можно определить правила редукции графов, в которых нет лямбда выражений, а есть только применения конструкторов и комбинаторов. Важно, что при этом можно избежать копирования, однако интенсивно используются вершины-синонимы, так как по крайней мере два из трех введенных комбинаторов являются чистыми селекторами.

2 2 Кубенский А.А. Функциональное программирование. Покажем, что в самом деле можно любое замкнутое лямбда-выражение представить в комбинаторной форме. Для этого сначала введем функцию абстрагирования abs(x, E) для комбинаторных выражений E такую, что Правила абстрагирования от переменных Глава 7. Комбинаторная редукция. abs(x, E) x = E Другими словами, abs(x, E) ведет себя точно так же, как λx.E. Сокращенная запись для abs(x, E) – [x]E. Очевидно, что: [x]x = I [x]c = K c [x]y = K y [x]e1 e2 = S ([x]e1) ([x]e2) S ([x]e1) ([x]e2) x = ([x]e1) x (([x]e2) x) = e1 e2 Теперь перевод любого лямбда выражения в комбинаторную форму можно производить по следующим правилам: comb(c) = c comb(v) = v comb(λx.e) = [x]comb(e) comb(e1 e2) = comb(e1) comb(e2)

3 3 Кубенский А.А. Функциональное программирование. Пример перевода выражения в комбинаторную форму Глава 7. Комбинаторная редукция. Рассмотрим следующую функцию: λx.λy.+ x y. Заметим, что для этой функции существует очень простая комбинаторная форма: +. Проведем преобразование этого лямбда-выражения. comb(λx.λy.+ x y) = [x][y]comb(+ x y) = [x][y]comb(+) comb(x) comb(y) = [x][y]+ x y = [x]S ([y]+ x) ([y]y) = [x]S (S ([y]+) ([y]x)) ([y]y) = [x]S (S (K +) (K x)) I = S ([x]S (S (K +) (K x))) ([x]I) = S (S ([x]S) ([x](S (K +) (K x)))) (K I) = S (S (K S) (S ([x](S (K +)) ([x](K x))))) (K I) = S (S (K S) (S (S ([x]S) ([x](K +))) (S ([x]K) ([x]x)))) (K I) = S (S (K S) (S (S (K S) (S ([x]K) ([x]+))) (S (K K) I))) (K I) = S (S (K S) (S (S (K S) (S (K K) (K +))) (S (K K) I))) (K I) Это самое сложное выражение для функции сложения в курсе. Проверим, что при применении этого выражения к константам, скажем, 2 и 3, мы действительно получим 5

4 4 Кубенский А.А. Функциональное программирование. Проверка правильности преобразования в комбинаторную форму. Глава 7. Комбинаторная редукция. S (S (K S) (S (S (K S) (S (K K) (K +))) (S (K K) I))) (K I) 2 = (S (K S) (S (S (K S) (S (K K) (K +))) (S (K K) I))) 2 ((K I) 2) = S (K S) (S (S (K S) (S (K K) (K +))) (S (K K) I)) 2 (K I 2) = (K S) 2 (S (S (K S) (S (K K) (K +))) (S (K K) I) 2) I = K S 2 ((S (K S) (S (K K) (K +))) 2 (S (K K) I 2)) I = S (S (K S) (S (K K) (K +)) 2 (K K 2 (I 2))) I = S (K S 2 (S (K K) (K +) 2) (K 2)) I = S (S (K K 2 (K + 2)) (K 2)) I = S (S (K +) (K 2)) I Здесь видно, как атомы «+» и «2» привязаны к комбинаторам K, «ожидая» применения их ко второму аргументу. S (S (K +) (K 2)) I 3 = S (K +) (K 2) 3 (I 3) = K + 3 (K 2 3) 3 = = 5

5 5 Кубенский А.А. Функциональное программирование. Оптимизация Карри Глава 7. Комбинаторная редукция. Если хочется упростить сложное комбинаторное выражение, то можно попробовать применить эквивалентные преобразования выражений. Введем следующие правила. S ( K E1) (K E2) = K (E1 E2) (правило 1) S ( K E1) I = E1 (правило 2) В корректности этих преобразований можно убедиться, установив, что при применении к одному и тому же аргументу получается один и тот же результат. S ( K E1) (K E2) X = K E1 X (K E2 X) = E1 E2 = K (E1 E2) X S ( K E1) I X = K E1 X (I X) = E1 X Еще один путь снизить сложность выражений – ввести дополнительные комбинаторы, например: B F G X = F (G X) (композитор) C F X Y = F Y X (перестановщик). S ( K E1) E2 = B E1 E2 (правило 3) S E1 ( K E2) = C E1 E2 (правило 4) и дополнительные оптимизационные правила: S ( K E1) E2 X = K E1 X (E2 X) = E1 (E2 X) = B E1 E2 X S E1 ( K E2) X = E1 X (K E2 X) = E1 X E2 = C E1 E2 X в справедливости которых можно убедиться путем следующих преобразований:

6 6 Кубенский А.А. Функциональное программирование. Оптимизация Карри Глава 7. Комбинаторная редукция. Попробуем проверить правила (1 – 4) на практике, преобразовав наше длинное выражение для функции сложения. S ( K E1) (K E2) = K (E1 E2) (правило 1) S ( K E1) I = E1 (правило 2) S ( K E1) E2 = B E1 E2 (правило 3) S E1 ( K E2) = C E1 E2 (правило 4) S (S (K S) (S (S (K S) (S (K K) (K +))) (S (K K) I))) (K I) = S (S (K S) (S (S (K S) (K (K +)) (S (K K) I))) (K I) (правило 1) (правило 2) = S (S (K S) (S (S (K S) (K (K +)) K)) (K I) (правило 1) = S (S (K S) (S (K (S (K +))) K)) (K I) (правило 4) = C (S (K S) (S (K (S (K +))) K)) I (правило 3) = C (B S (S (K (S (K +))) K)) I (правило 3) = C (B S (B (S (K +)) K)) I S (S (K +) (K 2)) I Это выражение уже значительно короче, хотя и далеко от оптимального «+». Проверьте, что после применения этого выражения к 2 получится то же, выражение, которое мы уже получали раньше

7 7 Кубенский А.А. Функциональное программирование. Оптимизация Карри (продолжение) Глава 7. Комбинаторная редукция. Правила оптимизации и новые комбинаторы можно ввести непосредственно в алгоритм преобразования лямбда-выражений в комбинаторную форму. При применении этих правил преобразования могут дать гораздо более простой результат. [x]x = I [x]c = K c [x]y = K y [x]e1 e2 | FST == K M && SND == I = M | FST == K M && SND == K N = K (M N) | FST == K M = B M SND | SND == K N = C FST N | otherwise = S FST SND where FST = [x]e1 SND = [x]e2 comb(λx.λy.+ x y)= [x][y]comb(+ x y) = [x][y]comb(+) comb(x) comb(y)= [x][y]+ x y [y]+ = K +, [y]x = K x поэтому [y]+ x = K (+ x) = K [x]+ x = + поскольку [x]+ = K +, [x]x = I

8 8 Кубенский А.А. Функциональное программирование. Аппликативные подвыражения Глава 7. Комбинаторная редукция. Заметим, что если в исходном лямбда-выражении уже имелись подвыражения, имеющие аппликативный вид ( e1 e2 ), то при его абстрагировании от переменной, не входящей в e1 e2 свободно, мы можем и не получить «естественную» форму e1 e2. Например, Лемма 1: при применении оптимизационного правила (1) для аппликативного выражения e comb(λx.+ 1 2)= [x]comb(+ 1 2)= [x]+ 1 2 = S (S (K +) (K 1)) (K 2) при неоптимизированных преобразованиях. Компоненты аппликативного подвыражения распределяются по всему выражению. Если применять правило (1) в оптимизации Карри, то выражение приобретет вид K (+ 1 2) Сохранение аппликативных подвыражений важно для оптимизации вычислений, поскольку позволяет разделять такие подвыражения более эффективно и сохранять «полную ленивость». при условии, что x не входит свободно в e. Доказательство (по индукции): если e – константа или переменная (не равная x ), то утверждение леммы справедливо по определению абстрагирования. [x]e = K e Если e = e1 e2, то [x]e = [x]e1 e2 = S ([x]e1) ([x]e2) = S (K e1) (K e2) = = K (e1 e2) = K e

9 9 Кубенский А.А. Функциональное программирование. Аппликативные подвыражения Глава 7. Комбинаторная редукция. Лемма 2: если e1 является подвыражением аппликативного выражения e, то при вычислении [x]e с применением оптимизационного правила (1) e1 будет также подвыражением [x]e при условии, что x не входит в e1 свободно. Таким образом, справедлива теорема: при применении только правила (1) сохраняются все аппликативные подвыражения исходного лямбда-выражения. Это утверждение также несложно доказать по индукции. Доказательство также несложно провести по индукции по структуре выражения e. Действительно, comb(e) = e, если e – переменная или константа, а также, если оно само является аппликативным выражением. Далее, comb(e1 e2) = comb(e1) comb(e2), и аппликативное подвыражение сохраняется по индукционному предположению. Наконец, comb(λx.e) = [x]comb(e), и аппликативное подвыражение сохраняется по лемме (2).

10 10 Кубенский А.А. Функциональное программирование. В графах для комбинаторных выражений не будет лямбда-вершин, только вершины-константы, вершины-примитивы (включая базовые комбинаторы), и вершины-конструкторы. Комбинаторная редукция графов Глава 7. Комбинаторная редукция. Преобразования таких графов (редукции) будут происходить с помощью применения «дельта- правил», которые надо определить в том числе и для всех базовых комбинаторов. Приятно, что при этом можно полностью избежать копирования. Если аргументов для применения «дельта-редукции» недостаточно, то граф уже находится в СЗНФ. Правила применения базовых комбинаторов выглядят Ie e2 e1

11 11 Кубенский А.А. Функциональное программирование. Комбинаторная редукция графов Глава 7. Комбинаторная редукция. Правила применения дополнительных базовых комбинаторов B и C выглядят Эти правила приведены в самом общем виде (без использования оптимизаций). Мы исключили копирование, но при применении функций проекторов (в частности, I и K ) придется по-прежнему создавать вершины-синонимы, если на аргументы есть ссылки.

12 12 Кубенский А.А. Функциональное программирование. Рекурсия Глава 7. Комбинаторная редукция. До сих пор мы рассматривали только выражения, не содержащие рекурсию. Рекурсию можно реализовать, если ввести в рассмотрение Y -комбинатор. Однако, если рассмотреть Y -комбинатор Карри в его лямбда-выражении Y = λh.(λx.h (x x)) (λx.h (x x)), то оказывается, что его комбинаторное представление comb(Y) слишком сложное. На самом деле рекурсия здесь использована «не по существу», но сути дела это не меняет. Теперь построим графы этих выражений и выражения f 2, соединяя в месте «рекурсивных» вызовов. Для непосредственно выраженной «плоской» рекурсии можно предложить два подхода: зацикливание графов для рекурсивных выражений; непосредственное введение правил преобразования графов для Y-комбинатора. Пусть имеются две взаимно рекурсивные функции в следующем выражении: letrec f = λx.cons x (g x) g = λx.cons (sqr x) (f x) in f 2 Прежде всего преобразуем все выражения в комбинаторную форму. f = comb(λx.cons x (g x)) = [x](cons x (g x)) = S cons g g = [x]cons (sqr x) (f x) = S (B cons sqr) f

13 13 Кубенский А.А. Функциональное программирование. Рекурсия Глава 7. Комбинаторная редукция. Этот граф содержит циклические связи, однако его преобразование происходит по введенным нами ранее правилам точно так же, как и для нециклических графов. f = comb(λx.cons x (g x)) = [x](cons x (g x)) = S cons g g = [x]cons (sqr x) (f x) = S (B cons sqr) f f S f 2 f 2 gf Заметим, впрочем, что результатом работы будет бесконечный список.

14 14 Кубенский А.А. Функциональное программирование. Пример преобразования циклического графа Глава 7. S @ : В ленивой схеме вычислений на этом вычисление заканчивается (получен циклический список)

15 15 Кубенский А.А. Функциональное программирование. Графическое представление Y-комбинатора Глава 7. Комбинаторная редукция. f = λx.letrec g = e1 in e2 Пусть имеем следующее определение функции. где в выражении e1 имеются рекурсивные ссылки на g, а в выражении e2 – как на f, так и на g. Из-за вложенной рекурсии трудно выполнить преобразование этого выражения в комбинаторную форму непосредственно, однако, можно воспользоваться Y-комбинатором. f = Y λf.λx.(λg.e2)(Y λg.e1) comb(f) = comb(Y λf.λx.(λg.e2)(Y λg.e1)) = Y [f][x]([g]comb(e2)) (Y [g]comb(e1)) Правило для «редукции» Y-комбинатора выглядит несколько необычно, так как создает циклический граф, однако, это вполне адекватная форма вычислений на e e Для прямой рекурсии в общем случае правило преобразования выглядит так: comb(f = e ) = Y [f]e