Введение в функциональное программирование (стр. 11 )

Комбинатор Тёрнера S′ полезен при трансляции λ-выражений вида

λVn … V2 V1. E1 E2 (скоро будет показано, почему удобно нумеровать связанные переменные в убывающем порядке). Для того, чтобы это показать, определим по Тёрнеру [35]:

  E′  означает λ*V1. E

  E′′  означает λ*V2. (λ*V1. E)

  E′′′  означает λ*V3. (λ*V2. (λ*V1. E))

Напомним, что:

  (λVn … V2 V1. E1 E2) c = λ*Vn. ( … (λ*V2. (λ*V1. (E1 E2)c))) … )

Следующее упражнение показывает, что выражение

  λ*Vn. … λ*V2. λ*V1. (E1 E2)

становится очень сложным при увеличении n.

Упражнение 43

Показать,  что:

λ*x1. E1 E2 = S E1′ E2′ λ*x2. (λ*x1. E1 E2) = S (B S E1′′) E2′′ λ*x3. (λ*x2. (λ*x1. E1 E2)) = S ( B S ( B ( B S) E1′′′)) E2′′′ λ*x4. (λ*x3. (λ*x2. (λ*x1. E1 E2))) =

S ( B S ( B ( B S) (B (B (B S))) E1′′′′)) E2′′′′

Размерность  λ*Vn. … λ*V2. λ*V1. (E1 E2)  пропорциональна  квадрату n. Используя S′ можно добиться линейной зависимости  между размерностью и  n :

  λ*x2.( λ*x1. E1 E2) = λ*x2. S E1′ E2′

  = S’ S (λ*x2. E1′) (λ*x2. E2′)

  = S’ S E1′′ E2′′

  λ*x3.(λ*x2.( λ*x1. E1 E2)) = λ*x3. S′ S E1′′ E2′′

  = S′ ( S′ S) (λ*x3. E1′′)((λ*x3. E2′′)

  = S′ ( S′ S) E1′′′ E2′′′

  λ*x4(λ*x3.(λ*x2.( λ*x1. E1 E2))) =  λ*x4. S′ ( S′ S) E1′′′ E2′′′

  = S′ (S′ ( S′ S)) (λ*x4. E1′′′) ( λ*x4. E2′′′)

  = S′  (S′ ( S′ S)) E1′′′′ E2′′′′

Также как B и С были введены чтобы упростить комбинаторные выражения вида S ( K E1 ) E2  и S E1 (K E2) соответственно, Тёрнер ввел B′ и С′ для той же цели что и  S′ . Требуются такие свойства:

  S′  C (K E1) E2 = B′ C E1 E2

  S′ C E1 ( K E2) = C′ C E1 E2 

(где С – произвольный  комбинатор,  а  Е1  и  Е2  произвольные  комбинаторные выражения). Это достигается если B′ и C′ определены следующим образом:

LET B′ = λc f g x. c f (g x)   LET C′ = λc f g x. c(f x) g

Очевидно, что B′ и C′  будут иметь следующие свойства для произвольных λ-выражений С, Е1, Е2  и  Е3: 

  B′ C E1 E2 E3 → C E1 (E2 E3)

  c

  C′ C E1 E2 E3 → C ( E1 E3) E2

  c

Упражнение 44

Показать, что для произвольных λ-выражений Е1, Е2  и  Е3:

S′ E1 (K E2) E3 = B′ E1 E2 E3 S′ E1 E2 (K E3) = C′ E1 E2 E3 S ( B  E1 E2) E3 = S′ E1 E2 E3 B ( E1 E2) E3 = B′ E1 E2 E3 C ( B E1 E2) E3 = C′ E1 E2 E3

€

Алгоритм Тёрнера для трансляции λ-выражений в комбинаторные выражения описан им [35] следующим образом:

В общем случае используйте алгоритм Карри, но каждый  раз  когда формируется терм начинающийся с S, B и C, используйте одну из следующий трансформаций, если возможно:

  S ( B K A) B →  S′ K A B,

  B (K A) B → B′ K A B,

  C (B K A ) B  →  C′ K A B.

Здесь А и B обозначают произвольные термы как обычно, а К – любой терм, созданный  из  констант. Правильность нового алгоритма  может  быть доказана  из  правильности алгоритма  Карри  демонстрацией  того,  что в каждой  из  вышеприведенных  трансформаций  левые  и правые  части  экстенсионально  равны. В  каждом  случае  это  напрямую  следует  из  определений  соответствующих  комбинаторов.

Со времени появления трудов Тёрнера, множество людей работало над улучшением его базовой идеи. Например, Джон Хагес  ввел схему для динамической  генерации  оптимального  набора  примитивных комбинаторов ( суперкомбинаторов ) для  каждой  программы [20]. Идея состоит в том, что компилятор будет генерировать комбинаторные выражения построенные на  суперкомбинаторах  для  компилируемой программы. Он будет также динамически генерировать микрокод для применения правил редукции для этих суперкомбинаторов. В результате каждая  программа  работает  на  редукционной  машине, созданной специально под неё. Большинство  современных  высокопроизводительных применений  языков  функционального  программирования  используют суперкомбинаторы [1, 11]. Другой способ – использовать комбинаторы основанные на нотации Де  Брейна краткое описание которой приводилось в  разделе  1.8 .  “ Категориальная абстрактная машина “ [26]  использует именно  этот  подход. 

Лист регистрации изменений
Всего листов (страниц) в докум.	№ докумен- та	Входящий № сопрово- дительно- го докум. и дата	Подп.	Да- та
Изм.	изменён- ных	заменён- ных	новых	аннули- рован- ных