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

Будет показано, что любое λ-выражение эквивалентно выражению, построенному из переменных и двух определенных выражений, K и S, используя только аппликацию функций. Это  делается  имитацией

λ-абстракций  с  помощью комбинаторов  K  и  S. Будет показано, как

β-редукции могут быть произведены с помощью более простых операций, используя  K  и  S. Именно  эти  более  простые  операции  комбинаторная машина  передаёт  непосредственно  в  компьютер.

Опредения K и S таковы: 

  LET K = λx y. x

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

Из этих определений очевидно, что β-редукция для всех Е1, Е2 и Е3:

  K E1 E2 = E1

  S E1 E2 E3 = ( E1 E3) (E2 E3)

Любое выражение, построенное аппликацией (т. е. комбинацией) из  K  и  S называется  комбинатором,  K  и  S –  примитивные комбинаторы.

__________

  1Наиболее  полный  курс  это двухтомник  Комбинаторной  Логики [9,10].

  Но лучше  начать с  более поздних  учебников [19, 2] 

В БНФ, комбинаторы имеют следующий синтаксис:

  <комбинатор>  : =  K  | S |  (<комбинатор> <комбинатор>)

Комбинаторное выражение – это выражение, построенное из K и S и нуля или других переменных. Таким образом, комбинатор – это комбинаторное выражение, не содержащее переменных. В БНФ, синтаксис комбинаторных  выражений  следующий:

  <комбинаторное выражение>

  :: = K  | S

  | <переменная>

  | (<комбинаторное выражение> <комбинаторное выражение>)

Упражнение 34

Определим  I  как :

  LET I = λx. x

Показать, что I = S K K.

Функция идентичности I, определенная в последнем упражнении, часто берется как примитивный комбинатор, но, как показано в упражнении, это не является необходимым, поскольку её можно определить через K и S.

3.1 Редукция комбинаторов

Если Е и Е′ – комбинаторные выражения тогда обозначение  E → E′

  с

используется, если E ≡ E′  или если E′  можно получить из Е 

последовательностью  переписываний  вида:

K E1 E2 → E1

  c

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

  c

I E → E

  c

Обратите  внимание, что редукция  I E → E  получается  из  (i)  и  (ii).

Пример

  S K K x → K x (K x)  из (ii)

  c

  → x  из (i)

  c

Этот  пример  показывает, что  для  любого  Е :  I E → E.

  c

Любая  последовательность  комбинаторных  редукций, т. е.  редукций

вида → , может  быть  расширена  в  последовательность β-конверсий.

  с

Этот  факт  очевиден,  т. к.  K E1 E2  и  S E1 E2 E3  редуцируется последовательностью  β-конверсий  к  E1  и  E1 E3) (E2 E3)  соответственно.

3.2  Функциональная  полнота.

Неожиданным является тот факт, что любое λ-выражение может быть переведено в эквивалентное комбинаторное выражение. Результат такого приведения называется функциональной полнотой комбинаторов и является основой для компиляции функциональных языков в машинный код комбинаторных машин.

Сперва определим, что для произвольной переменной V и комбинаторного выражения E, существует другое комбинаторное выражение λ*V. E имитирующее  λV. E  так  что  λ*V. E = λV. E. Это даёт способ использования K и S для имитации, добавляя  ‘λV’  к  выражению.

Если V переменная, а Е – комбинаторное выражение, тогда комбинаторное выражение  λ*V. E  индуктивно  определяется  на  основе  следующим образом:

λ*V. V = I  λ*V. V′  = K V′  ( если V ≠ V′ ) λ*V. C = K C ( если C комбинатор) λ*V.(E1 E2) = S (λ*V. E1) (λ*V. E2)

Обратите  внимание  на  то, что  λ*V. E  –  комбинаторное  выражение,

не содержащее V.

Пример

Если f и x переменные, и f ≠ x, тогда

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

  = S (K f) I

Следующая теорема показывает, что λ*V. E имитирует λ-абстракцию.

Теорема  (λ*V. E) = λV. E
Доказательство

Покажем, что  (λ*V. E) V = E.  Отсюда  следует, что  λV. (λ*V. E) V = λV. E

и  по  η-редукции  получим, что  λ*V. E = λV. E.

Доказательство того, что  (λ*V. E) V = E  осуществляется  математической индукцией  на  основе  “размера” Е.

Доказательство  построим  следующим  образом: 

Если E = V тогда:

  (λ*V. E) V = I V = (λx. x) V = V = E

Если E= V′ , где V′ ≠ V, тогда:

  (λ*V. E) V = K V′ V = (λx y. x) V′ V = V′ = E

Если Е = С, где С – комбинатор, тогда:

  (λ*V. E) V = K C = (λx y. x) C V = C = E

Если Е = (Е1 Е2), тогда по индукции можно предположить, что:

  (λ*V. E1) V = E1

  (λ*V. E2) V = E2

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

  (λ*V. E) V = (λ*V. ( E1 E2)) V

  = (S (λ*V. E1) (λ*V. E2)) V

  =  (λf g x. f x (g x)) (λ*V. E1) (λ*V. E2) V

  =  (λ* V. E1) V ((λ*V. E2) V)

  =  E1 E2  ( по индуктивному  допущению)

  =  E

Запись

  λ*V1 V2 … Vn. E

обычно  значит

  λ*V1. λ*V2.  …  λ*Vn. E

Теперь  определим  переход  от  произвольного  λ-выражения  Е  к комбинаторному  выражению (Е)с:

(V)c  = V (E1 E2)c = (E1)c (E2)c (λV. E)c = λ*V. (E)c
Теорема  Для любого λ-выражения Е верно, что Е = (Е)с

Доказательство.

Доказательство производится по индукции на основе размера Е.

Если Е= V, тогда (Е)с = (V)c = V Если Е = (Е1 Е2) по индукции мы может предположить, что

  Е1 = (Е1)с

  Е2 = (Е2)с

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

  (Е)с = (Е1 Е2)с = (Е1)с (Е2)с = Е1 Е2 = Е

Если Е = λV. E′  тогда по индукции можно предположить, что:

  (E′)c = E′

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

  (E)c  = (λV. E′)c

  = λ*V. (E′)c  ( по правилам перехода)

  = λ*V. E′  ( по индуктивному  допущению)

  = λV. E′  (из предыдущей теоремы)

  = E

Эта теорема показывает, что любое  λ-выражение эквивалентно λ-выражению построенному аппликацией из K, S  и  переменных, т. е. класс λ-выражений Е определенный на БНФ следующим образом:

  E :: = V | K | S | E1 E2

эквивалентен полному λ-исчислению.

Множество  n  комбинаторов  С1, …, Сn  называется  базисом  n  элементов

( Барендрехт [2], Часть 8) , если любое  λ-выражение  Е  эквивалентно выражению построенному аппликацией  функций  из  Ci  и  переменных. Теорема, описанная выше, показывает  что  K  и  S  формируют  2-х элементный базис. Следующие  упражнение ( из раздела 8.1.5 книги Бахендрехта ) показывает, что  существует  одно-элементный  базис. 

Упражнение 35 Найдите комбинатор, предположим Х, такой, что λ-выражение эквивалентно выражению построенному из Х и переменных аппликацией. Подсказка:  Пусть  < E1, E2, E3> = λp. p E1 E2 E3  и  предположим,  что  < K, S, K > < K, S, K > < K, S, K >  и  <K, S, K> <<K, S, K> <K, S, K>>  Примеры

  λ*f. λ*x. f (x x)  = λ*f. (λ*x. f (x x))

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

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

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

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

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

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

  = S ( S ( K S) ( S (K K) I)) (K (S I I))

  (Y)c = (λf. (λx. f(x x)) (λx. f(x x)))c

  = λ*f. ((λx. f(x x)) (λx. f(x x)))c

  = λ*f. ((λx. f(x x))c (λx. f(x x))c )

  = λ*f. (λ*x. (f( x x))c) (λ*x. (f(x x))c)

  = λ*f. (λ*x. f(x x)) (λ*x. f(x x))

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

  = S(S(S(KS)(S(KK)I))(K(SII)))(S(S(KS)(S(KK)I))(K(SII)))

Машины редукций

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

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

Идея Тёрнера – представление комбинаторов деревьями. Например,

S ( f x) ( K y) z может быть представлена так: 

В памяти такие деревья отображаются как  структуры  указателей. Могут быть применены  спецальные  аппаратные  и  программно-аппаратные средства  и  определив →, можено добиться преобразования таких деревьев