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

  c

в соответствие  правилам  комбинаторной  редукции.

Например, дерево, приведенное выше, может быть преобразовано в: 

используя  следующее  преобразование:

  3 

  2 

  1  3  2  3

S  1

Которое  соответствует  редукции

S E1 E2 E3 → (E1 E3) (E2 E3).

  c

Упражнение 36

Какое преобразование дерева  соответствует  K E1 E2 → E1 ?

  с

Как это преобразование изменит приведенное выше дерево?

Заметьте, что только  что  приведенное  преобразование  дерева  для  S

дублирует  поддерево. Это  приводит  к  расходу  места; переход лучше осуществлять  генерируя  одно  поддерево  с  двумя  указателями, т. е: 

  3 

  2  1  2

  1 

  3

Этот  способ создаёт граф, а не дерево. Для  более детального анализа такой редукции  по  графу, рекомендуется  работа  Тёрнера [34].

Из теоремы, описанной выше, следует, что эффективный способ  редукции  λ-выражения состоит в следующем:

Преобразование к комбинаторам  (т. е. E → (E)c). Применение переписи

  K E1 E2 → E1

  c

  S E1 E2 E3 → (E1 E3) (E2 E3)

  с 

пока это возможно.

Интересный вопрос – будут ли выражения в результате этого процесса “полностью вычисляться”? Если какое-то выражение Е преобразуется в комбинаторы, а  затем  редуцируется  используя →, будет  ли  результат 

  с

выражения  настолько  же  “полностью вычисленным”  как  и  результат прямого  λ-редуцирования  Е,  или  будет  частично вычисленным? Удивительно,  но  этот  важный  вопрос  не  рассмотрен в литературе

(наиболее важная работа – это работа Хиндлей [18]. Там производится сравнение  λ-редукции  с комбинаторной  редукцией, но  не  тем  способом, который  на  первый  взгляд  важен  для  работы комбинаторных машин). Но несмотря  на  это, комбинаторные  машины  были построены и  работают [8]!

Известно, что если  Е1 → Е2  в  λ-исчислении, тогда  не  обязательно, что

(Е1)с → (Е2)с.  Например, возьмем:

  с

  Е1 = λy. (λz. y) (x y)

  E2 = λy. Y 

Упражнение 37

С Е1 и Е2, определенными выше, показать, что Е1 → Е2 в λ-исчислении, но неверно что (Е1)с → (Е2)с. 

  с 

Комбинаторное выражение называется комбинаторной нормальной формой если не содержит подвыражений вида  K E1 E2  или  S E1 E2 E3.  Тогда теорема нормализации  выполняется  для  комбинаторных  выражений, т. е. редукции  крайнего слева  комбинаторного редекса  приведет к нахождению комбинаторной  нормальной формы, если она существует.

Заметьте, что если  Е  комбинаторная  нормальная форма,  тогда необязательно  следует, что это  λ-выражение  в  нормальной  форме.

Пример

S K находятся в нормальной комбинаторной форме, но содержит β-редекс, т. е.

  (λf. (λg x. (f x (g x))) (λx y. x)

Упражнение 38

Придумайте комбинаторное выражение Е в комбинаторной норальной форме, но не имеет  нормальной формы.   

3.4  Улучшенная  трасляция  в  комбинаторы

Примеры, приведенные  выше,  показывают,  что  простые  λ-выражения могут  быть  транслированы  в  достаточно  сложные  комбинаторные выражения  с  помощью  правил  из  пункта 3.2.

Применяются  различные  оптимизации  для  того, чтобы  сделать “код” исполняемый  машинами  редукции  более  компактным.

Примеры

Пусть E  комбинаторное выражение, а  х – переменная  не имеющая вхождений в Е. Тогда:

  S ( K E) I x → (K E x) (I x) → E x 

  c  c

и, следовательно  S ( K E) I x = E x  ( потому  что  E1 → E2  подразумевает

  с

Е1 → Е2),  и  по  экстенсиональности  (см. пункт 1.7):

  S ( K E ) I = E

Пусть  Е1  и  Е2  комбинаторные  выражения  и  x - переменная  не имеющая  вхождений  ни  в  одно  из  выражений. Тогда :

  S ( K E1) (K E2) x → K E1 x (K E2) x → E1 E2

  c  c

Таким образом:

  S ( K E1) (K E2) x = E1 E2

Теперь:

  K ( E1 E2) x → E1 E2

  c

и, следовательно  K (E1 E2) x = E1 E2. Таким образом

  S ( K E1) (K E2) x = E1 E2 = K (E1 E2) x

Из  экстенсиональности  следует, что:

  S ( K E1) (K E2) = K (E1 E2)

Т. к.  S (K E) I = E  для любого  Е,  каждый  раз  когда  генерируется  комбинаторное выражение вида  S ( K E) I, оно  может быть оптимизировано  просто  к  Е.  Похожим  образом,  каждый  раз  когда генерируется  выражение  вида  S ( K E1) (K E2) оно может  быть оптимизировано  к  K (E1 E2).

Пример

Выше было показано  (раздел 3.2), что

  λ*f. λ*x. f (x x) = S ( S (K S) (S (K K) I)) (K (S I I))

Использование  оптимизации  S (K E) I = E  упрощает выражение до:

  λ*f. λ*x. f(x x) = S (S (K S) K) (K (S I I))

3.5  Комбинаторы

Легче  распознать  применимость  оптимизации  S ( K E ) I = E, если I  не была расширена до S K K, т. е. I  берется  как  примитивный комбинатор. Другие  комбинаторы  также  могут  быть  полезны. Например  B  и  C, определенные  так:

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

имеют следующие  правила  редукции:

  B E1 E2 E3 → E1 (E2 E3)

  c

  C E1 E2 E3 → E1 E3 E2

  c

Упражнение 39

Показать, что  с  B  и  C  определенными  выше,  верно  что:

  S ( K E1) E2 = B E1 E2

  S E1 (K E2) = C E1 E2 

( где Е1 и Е2 – любые два комбинаторных выражения ). 

Используя B и C можно провести дальнейшую оптимизацию трансляции

λ-выражений в комбинаторы  заменой  выражений  вида  S ( K E1) E2  и 

S E1 (K E2)  на  B E1 E2  и  C E1 E2.

3.6  Алгоритм  Карри

Комбинирование  различных  оптимизаций, описанных в предыдущем разделе, ведет к Алгоритму Карри для трасляции λ-выражений в комбинаторные выражения. Этот алгоритм состоит из использования определения (Е) с  (данного в  разделе  3.2), но каждый  раз когда генерируется  выражение  формы  S E1 E2  требуется  применить  следующие  правила  переписи: 

S ( K E1) (K E2) → K (E1 E2) S( K E) I → E S (K E1) E2 → B E1 E2 S E1 (K E2) → C E1 E2

Если  применимо  больше  чем  одно  правило, то  используется  правило  с меньшим  порядковым  номером. Например, S (K E1) (K E2) транслируется в  K (E1 E2) , а  не  в  B E1(K E2).

Упражнение 40

Показать, что используя алгоритм  Карри, Y  траслируется  в  комбинатор :

  S(C B(S I I)) (C B (S I I))

Упражнение 41

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

  S (S (K S) (S (K K) I)) (K (S I I)) = C B (S I I)

3.7  Алгоритм Тёрнера.

В своей  второй  работе Тёрнер  предложил  расширить  алгоритм  Карри используя другой новый примитивный комбинатор S′ [35]. Он определяется следующим образом:

LET S′ = λc f g x. c(f x) (g x)

И имеет такое правило редукции:

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

где  С, Е1, Е2, Е3  произвольные  комбинаторные  выражения. 

“C”  используется  потому  что  S′  имеет  такое  свойство, что  если  С - это 

комбинатор  (т. е.  не  содержит  переменных)  тогда  для  любого  E1  и  E2:

  λ*x. С E1 E2 = S′ C (λ*x. E1) (λ*x. E2) 

Это  можно  показать используя  экстенсиональность.  Очевидно, что  x-

это  переменная,  не  имеющая  вхождений  в  λ*x. C E1 E2  или 

S′ C (λ*x. E1) (λ*x. E2)  (как вы думаете, почему?)  и  значит достаточно показать: 

( λ*x. C E1 E2) x = (S′ C (λ*x. E1) (λ*x. E2)) x

Из определения  λ*х  следует, что:

  λ*x. C E1 E2 = S ( S (K C) (λ*x. E1)) (λ*x. E2)

и следовательно

(λ*x. C E1 E2) x = (S (S (K C) (λ*x. E1)) (λ*x. E2)x

  = S( K C)( λ*x. E1) x ((λ*x. E2)) x)

  = K C x ((λ*x. E1) x) ((λ*x. E2) x)

  = C ((λ*x. E1) x) ((λ*x. E2)) x)

Но  (S’ C (λ*x. E1) (λ*x. E2) x = C ((λ*x. E1) x) ((λ*x. E2)) x)

и  поэтому :

  (λ*x. C E1 E2) x = ( S’ C(λ*x. E1)( λ*x. E2)) x

Упражнение 42

Где в описанном доказательстве мы использовали допущение, что С – комбинатор?