2 Постановка задачи: о связном предъявлении теории информатики и практики программирования в теме исполнения для теоретического мышления. 13 (стр. 9 из 25)
Важно заметить, что при вычислении комбинаторы однообразно применяются к переменным и к комбинаторам. К тому же они позволяют избежать проблемы свободных и связанных переменных. Это те факты, которые учитывались при создании аппликативного программирования.
При комбинаторной реализации (реализации на основе комбинаторов) каждое l-выражение преобразуется в эквивалентное выражение, построенное только из применений примитивных функций и комбинаторов, каждый из которых является замкнутым выражением, то есть выражением без свободных переменных. В основе такого преобразования лежит функция, которая абстрагирует свободные переменные, оставляя после этого цепочку применений комбинаторов.
Комбинаторная логика.
Рассмотрим теорию, которая лежит в основе этого типа реализации, - комбинаторную логику. Теоретически только два комбинатора, называемые K и S, требуются для представления любого l-выражения. Но надо сказать, что результирующая комбинация является неэффективной из-за того, что требуется очень большое число таких комбинаторов (и связанных с ним применений).
Комбинатором называется l-выражение, не содержащее свободных переменных. Например, функция тождества lx. x является комбинатором и обозначается обычно буквой I. Другим примером является комбинатор фиксированной точки Y = l h. (l x. h(xx))(l x. h(xx)). Двумя следующими примерами являются вычеркиватель K, задаваемый в виде K=lx.ly.x, и распределитель S, задаваемый S=lf.lg.lx. fx (gx).
Любое l-выражение может быть преобразовано в аппликативное выражение, то есть в выражение, построенное целиком на применениях функций, где, таким образом, отсутствуют l-абстракции. Чтобы добиться этого нам достаточно включить в синтаксис выражения два комбинатора S и K в качестве дополнительных констант.
| Комбинаторная логика (КЛ). Созидается теория, в которой фиксируется, что значит равенство термов. Равенство фиксируется посредством доказательства. Подразумеваемая структура: A = <A, *, c1,¼,cm> - алгебраическая структура с непустым носителем А; выделенными в нем элементами c1, c2,¼, cm, m³0; двуместной операцией *. {А - множество имен} Язык: термы, построенные из переменных, K, S посредством операции *. Формулы: равенства термов. Аксиомы: t = t для атомарных термов. St1t2t3 = t1t3(t2t3) Kt1t2 = t1 для произвольных термов. Правила вывода: |
Доказуемость: последовательность равенств a1, a2,¼, an называется доказательством an, если ai - аксиома, либо имеются j, k < i такие, что ai получается из aj и ak по правилу вывода. Фактически l-исчисление и КЛ, определенная выше, являются эквивалентными в следующем смысле. Предлагаемый набор аксиом устанавливает эквивалентность двух комбинаторных выражений MКЛ и NКЛ, обозначаемую MКЛ =КЛ NКЛ. Подобным образом и в l-исчислении эквивалентность выражений =l, задается как рефлексивное, симметричное, транзитивное замыкание правил преобразования.
Тогда, если El и EКЛ представляют одно и то же выражение в этих двух логиках, то можно показать, что
MКЛ =КЛ NКЛ Û Ml =l Nl
(если выполняется правило экстенсиональности Mx=Nx®M=N или правило h-конверсии lx. Mx=M).
В этом смысле комбинаторная логика может рассматриваться как модель l-исчисления.
В нашем представлении мы будем также использовать тождественный комбинатор I (его можно выразить через K и S). Заметим, что единственным механизмом сочетания выражений является применение функций - отсюда термин “аппликативное выражение”.
В этом синтаксисе каждое выражение находится в чисто аппликативной форме и поэтому может быть представлено графом, в котором единственным типом внутренних вершин являются @-вершины. В этом случае не существует l-вершин.
Сначала заметим, что l-выражения можно транслировать в комбинаторную форму путем последовательного абстрагирования (выделения) переменных из подвыражения. Функция comb, осуществляющая отображение l-выражений в комбинаторную форму, подробно описана в книге “Функциональное программирование” [24, стр. 294-295]. Так, например, применяя функцию трансляции comb к выражению lx.(ly. + x y), мы получим ее комбинаторную форму S (S(KS)(S (S(KS)(S(KK)(K+)) )(S(KK) I) )) (KI). В данном случае мы приходим к “программированию без переменных”. Так как переменные отсутствуют, то нет необходимости рассматривать вопрос об их именах и контексте. Таким образом, проблема свободных переменных оказывается решенной.
Основная привлекательность комбинаторного подхода заключается в его математической элегантности и простоте вычислений, вытекающей из наличия только трех правил преобразования графов (исключая те, что связаны с примитивными функциями). Итак, все, что нам нужно сделать - это определить правила преобразования графов, соответствующее применениям S, K и I, и объединить их с правилами применения примитивных функций. Но, к сожалению, даже очень простое l-выражение имеет очень сложный эквивалент в КЛ. Поэтому проведем оптимизацию путем расширения набора примитивных комбинаторов S, K и I.
3.2.4 Комбинаторная редукция с помощью графов.
Введем дополнительные комбинаторы B, C (композитор, перестановщик)
B f x y ® f (x y)
C f x y ® f y x.
Тогда в КЛ, имеющей примитивные комбинаторы K, S, I, C, B, выполняются следующие равенства:
S (K t1)(K t2) =КЛ K (t1 t2)
S (K t1) I =КЛ t1
S (K t1) t2 =КЛ B t1 t2
S t1(K t2) =КЛ C t1 t2.
Каждое из этих равенств дает правило для упрощения применения S.
Тогда применение функции comb приводит к оптимизированной форме:
comb (lx.(+ 2 (- x 3))) = B (+ 2) (C - 3).
Теперь рассмотрим представление комбинаторных функций графами. Существует 2 правила.
1) Константу мы представляем в виде дерева с одной вершиной соответствующей самой константе.
2) Применения функций вида A B в виде:
Пример: + 1 3 = (+ 1) 3
Пример: B (+ 2) (C - 3) 4
Для каждого комбинатора существует правило редукции, которое можно отобразить с помощью графов.
1) Редукция тождественного комбинатора
2) Редукция вычеркивателя
3) Редукция распределителя
4) Редукция перестановщика
5) Редукция композитора
Ïðèìåð êîìáèíàòîðíîé ðåäóêöèè:
B (+ 2) (C - 3) 4
B-ðåäóêöèÿ:
2.Ïîñòðîåíèå ãðàôîâ äëÿ âçàèìíî-ðåêóðñèâíûõ ôóíêöèé:
Ïóñòü èìååòñÿ ñèñòåìà ôóíêöèé
f1 = E1
f2 = E2
...
fn = En
Ïðè÷åì Å1...Ån ìîãóò çàâèñÿòü îò f1...fn, òîãäà íàäî íàðèñîâàòü ãðàô äëÿ êàæäîé ôóíêöèè è ñîåäèíèòü äóãàìè îáðàùåíèÿ ê äðóãèì ôóíêöèÿì ñ âõîäàìè â íèõ.
Ïðèìåð: f = comb( lx.cons x ( g x)) = S cons g
g = comb( lx.cons( * x x) ( f x)) = S ( B cons square) f
Îáðàùåíèå f 2 âûäàñò ïîñëåäîâàòåëüíîñòü 2 4 2 4 2 4...
Ãðàô âûãëÿäèò ñëåäóþùèì îáðàçîì:
Ïîñëåäíåå, ÷òî ìû ðàññìîòðèì ýòî ïðåäñòàâëåíèå ðåêóðñèâíûõ ôóíêöèé ñ ïîìîùüþ ãðàôîâ íà ïðèìåðå ôóíêöèè factorial.
Ôóíêöèÿ factorial â êîìáèíàòîðíîì ïðåäñòàâëåíèå èìååò âèä
factorial = S ( C ( B cond ( = 2)) 2) ( S * ( B factorial ( C - 1))).
Ãðàô âûãëÿäèò ñëåäóþùèì îáðàçîì.
