Задача 22.1 Для выражения:
let x = 5 in let z y = y +x in let x = 1 in (zx)×2; ;
составить КАМ-программу вычисления значения и по возможности
оптимизировать ее.
Решение.
opt--1. Запишем исходное выражение:
P = let x = 5 in let z y = y +x in let x = 1 in (zx)×2.
Его сведение к λ -выражению дает:
P = (λx.(λz.(λx.(zx)×2)1)(λy.y +x))5.
Заметим, что эта форма записи приводит к простой опти-
мизации во время компиляции. Дело в том, что код, соот-
ветствующий выражению (λ.M)N, представляет собой ин-
струкцию “push”, за которой следует “cur C” (где - код ),
за которой следует “swap”, за которой следует код 1 для N,
за которым следует “cons” и “ε”. Предполагая, что означи-
вание 1 на терме s дает значение w, приведем основные шаги
вычисления:
код ((λ.M)N) = push.cur C.swap.C1@[cons;ε],
Таблица 22.1: Вычисление значения подстановки
C = код(M), C1 = код(N).
В табл. 22.1 представлены вычисления значения.
Заметим, что
k (λ.M)N k = < Λ(k M k),k N k> ε.
Рассмотрим средства получения оптимизированного кода. Кро-
ме возможности означивания выражений относительно сре-
ды, как это уже рассматривалось, в рамках категориальной
комбинаторной логики возможно весьма естественно смо-
делировать β-редукцию. Для этого используется множество
правил, отличающихся от рассмотренных ранее, причем ис-
пользуются только чистые “категориальные” комбинаторы,
то есть исключаются составление совокупностей и апплици-
рование. Отправной точкой служит правило:
(Beta) ε◦ < Λ(x), y >= x◦ < Id, y > .
Это правило обосновывается следующим образом:
(ε◦ < Λ(x), y >)t = ε(< Λ(x), y > t)
= ε(Λ(x)t, yt)
= x(t, yt) = x(Id t, yt)
= (x◦ < Id, y >)t,
откуда следует принцип свертывания (Beta). Отметим, что
Id x = x. По правилу (Beta) выражению “let x = N in M”
сопоставляется код push.skip.swap@C1@cons.C, где skip
замещает Id (с пустым действием). Действие конструкции
[push.skip.swap] точно такое же, как и у [push], то есть
у рассмотренной оптимизации кода имеется теоретическое
обоснование.
opt--2. Покажем, что оптимизация [push.skip.swap] путем за-
мены на [push] правомерна. Действительно, в терминах λ -
исчисления получаем:
< f, g >= λt.λr.r(f t)(gt) = λt.(f t, gt),
а также получаем:
< g > = λt.λr.r(t)(gt) = λt.(t, gt) = λt.(Id t, gt).
Замещая в первом равенстве f на Id, получаем:
< Id, g >=< g >,
что обосновывает употребление символа “< · >” для един-
ственного выражения (вырожденный случай). Далее,
< Id, g >= [push;skip;swap;g; cons], < g >= [push;g; cons].
Отсюда требуемая оптимизация получается как графиче-
ское равенство.
opt--3. Введем еще одно правило оптимизации кода [⊕]
1. Обоснование такой оптимизации трудности не представляет. Дей-
ствительно, справедливы следующие равенства:
[⊕] ε◦ < Λ(+◦Snd), < M, N >>=
= (+◦Snd)◦ < Id, < M, N >>
= +◦ < M, N >=< M, N > +.
Более подробно:
(ε◦ < Λ(+◦Snd), < M, N >)t = ε(Λ(+◦Snd)t, < M, N > t)
= (Λ(+◦Snd)t)(< M, N > t)
= (+◦Snd)(t, < M, N > t)
= (+(Snd(t, < M, N > t)
= (+◦ < M, N >)t,
Оказывается, что, например, можно провести оптимизацию, скомпилировав
M + N в код hM, Ni, за которым следует “plus”.
откуда и следует требуемое равенство. Кроме того, после-
довательность [cons;plus] можно заменить на [plus], если
считать что “plus” представляет собой двухместную функ-
цию, а в качестве аргументов обрабатывает терм и вершину
стека. Следует отметить, что при этом частично теряется
апплицируемость операции “plus” к ее аргументам (так как
осуществлен переход отλ-терма(λx.λy.+xy) к двухместно-
му оператору x+y, требующему сразу оба операнда), однако
эта потеря общности для операций компенсируется возмож-
ностью аналогичного проведения оптимизации для частных
случаев трех- и вообще, n-местных функций. Это обосновы-
вается использованием следующих правил (случай трехмест-
ных функций):
λt.(f t, gt, kt) = λtλr0
.r0
(λr.r(f t)(gt))(kt) =
= λt.(< f, g > t, kt) = << f, g >, k >,
следовательно:
+(M, N, O) = + << M, N >, O > .
Действительно,
ε◦ < Λ(+◦Snd), ε◦ < Λ(Snd), << M, N >, O >>> =
= +◦Snd◦ < Id, ε◦ < Λ(Snd), << M, N >, O >>>
= +◦ (ε◦ < Λ(Snd), << M, N >, O >>>)
= +◦Snd◦ < Id, << M, N >, O >>)
= +◦ << M, N >, O > .
Таким образом, для исходной задачи можно выделить следу-
ющие основные шаги вычисления:
s push.C1@cons.C S
s C1@cons.C s.S
w cons.C s.S
(s, w) C S
Такое оптимизированное вычисление использует комбинатор
тождества, без которого используемую комбинаторную ло-
гику трудно назвать категориальной.
opt--4. Вернемся к вычислению на КАМ терма P. Воспользуемся
обозначением x | y = y ◦ x для упрощения компилируемой
записи. Введем сокращения:
F st = F, Snd = S,
Изложение сделаем замкнутым, приведя все подробности вы-
кладок. Формулировку принципа оптимизации (Beta) возьмем
в виде:
(Beta) < Λ(X), Y >| ε = x◦ < Id, y >=< y >| x.
Формулировку принципа оптимизации [⊕] возьмем в виде:
[⊕] < Λ(+◦Snd), < M, N >>| ε = (+◦Snd)◦ < Id, < M, N >> .
Кодирование по де Брейну дает:
P = (λx.(λz.(λx.(z x)×2)1)(λy.y +x))5,
затем
P0 = (λ.(λ.(λ.(1 0)×2)1)(λ.0 +1))5
= (λ.(λ.(λ.×((1 0),2))1)(λ.+(0,1)))5.
Далее вычисление значения P0 дает:
Для экономичной записи вычислений введены сокращения. С
учетом сокращений для D, где D = (< S, F | S >| +) и для
C, где C = < F | S, S >| ε, получим:
k P0 k = <0 5 >|< Λ(D) >|<0 1 >|< C0
,2 >| ×.
Для сокращения громоздкости КАМ-вычислений в порядке со-
глашения обозначим:
B =< C,0 2 >| ×, C =< F | S, S >| ε, D =< S, F | S >| +.
Обращаем внимание, что приводимые переобозначения, оче-
видно, имеют связь с суперкомбинаторами. Действительно,
каждый объект, введенный в употребление в виде матема-
тического соглашения об обозначениях, представляет собой
вполне определенный набор КАМ-инструкций. Этот набор
может быть вычислен (заранее скомпилирован) на КАМ, и
при необходимости достаточно в нужном месте использо-
вать именно результат предварительного вычисления. Не-
трудно заметить, что эти предварительные вычисления луч-
ше производить не бессистемно, но придерживаясь вполне
определенной “дисциплины” вычислений2 . Сама по себе ка-
тегориальная абстрактная машина является относительно
удачно сбалансированной системой “математических” вы-
числений. Эти вычисления с большой наглядностью можно
расположить в виде таблицы с тремя столбцами, отража-
ющими текущее значение терма, кода и стека. Напомним,
что именно текущая тройка <терм, код, стек > является
в точности текущим состоянием (вычисления). Поэтому по-
следовательность строк в таблице КАМ-вычислений задает
последовательность состояний процесса вычисления3. При-
Методы оптимизации вычислений, когда удается выделить относительно неза-
висимые параметры, получили развитие не только в различных вариантах “супер-
комбинаторного” программирования, но и широко используются в функциональном
программировании. Сами подходы разнятся по использумой семантике вычисле-
ний: как правило, используется денотационная семантика “с продолжениями”. Это
означает, что для всякого правильного в некотором смысле вычисления известен
“остаток программы”. 3
Вычисление может с математической точки зрения рассматриваться как после-
довательность состояний, то есть как процесс в точном понимании этого термина.
Эта точка зрения вполне в духе теории вычислений Д. Скотта.
ведем полную последовательность КАМ-вычислений:
Если вы устали от учебы тогда посмотрите телевизор, что бы купить качественный телевизор необходимо изучить отзывы тут - http://gadgetss.info/threads/10134/.
Контрольные вопросы.
1. Сформулируйте основные правила оптимизации.
2. Какое преимущество дает использование принципов (Beta) и
[⊕] при написании КАМ-программ ?
Упражнение.
Напишите оптимизированную КАМ-программу для вычисления вы-
ражения:
let x = 3 in let z = x+y in fz where y = 1 where f = sqr.
Указание. Переходим к λ-выражению:
(λx.(λz.(λf.fz)sqr)((λy.+xy)1))3,
получаем код де Брейна:
(λ.(λ.(λ.0 1)sqr)((λ.+ 1 0) 1))3.
Далее,
S k λ.(. . .)(· · ·),3 k= S(Λ(k (. . .)(· · ·) k),
0 3);
k (. . .)(· · ·) k= S(k (. . .) k,k (· · ·) k);
k (. . .) k= Λ(S(Λ(S(0!,1!)),k sqr k));
k (· · ·) k= S(Λ(S(S(k + k,1!),0!)),
0 1);
S0(Λ1(S2(Λ3(S4(Λ5(S6(0!,1!)6)5,k sqr k)4)3,
S3(Λ4(S5(S6(k + k,1!)6,0!)5)4,
0 1)3)2)1,
0 3)0 ≡ R.
Проделаем проверку, выполнив прямые вычисления:
R ρ ≡ S0(. . . ,0 3)0ρ = (Λ1(. . .)1ρ)(0
3 ρ) =1 (. . .)1(ρ,3) ≡1 (. . .)1ρ0
;
1(. . .)1ρ0 ≡ S2(. . . , . . .)2ρ0 = S4(. . . , . . .)4(ρ0
,4 (. . .)4(ρ0
,1));
4(. . .)4(ρ0
,1) = S5(. . . , . . .)5(ρ0
,1) = S6(. . . , . . .)6(ρ0
,1)1 =
= Λ(+◦Snd)(ρ0
,1)ρ0 1 = (+◦Snd)((ρ0
,1),3)1 = + 3 1 = 4;
S4(. . . , . . .)4(ρ0
,4) = Λ5(. . .)5(ρ0
,4)(Λ5(· · ·)5(ρ0
,4)) =
=5 (. . .)5((ρ0
,4),(Λ5(· · ·)5(ρ0
,4))) ≡
S(0!,1!)(. . . , . . .) = Λ5(· · ·)5(ρ0
,4)4 =5 (· · ·)5((ρ0
,4),4) ≡
≡ (sqr ◦Snd)((ρ0
,4),4) = sqr(4) = 16.
Полученное выражение R следует предварительно оптимизировать
по правилам (Beta) и [⊕]. Для этого полезно предварительно ис-
пользовать равенство:
S(x, y) = ε◦ < x, y > .
Ответ. sqr(4) = 16. |
Главная
Каталог файлов
