Задача 19.1 Для выражения:
let x = plus in x (4,(x where x = 3)); ;
построить λ-выражение и выражение комбинаторной логики, а
также вычислить их значение.
Решение.
dc--1. Фиксируем выражение:
let x = plus in x (4,(x where x = 3)); ;
dc--2. Выразим его в виде λ-выражения:
M = (λx.x(4,(λx.x)3)) +.
dc--3. Подготовим выражение к переводу на язык комбинаторной
логики (КЛ), то есть произведем каррирование:
N = (λx.x 4((λx.x)3))⊕,
где знак сложения “⊕” отличается от знака “+”. Отло-
жим пока обсуждение их различия до рассмотрения вопро-
сов, связанных с вычислением выражений на категориальной
абстрактной машине.
dc--4. Напомним, что процедура перевода в КЛ задается по индук-
ции:
(i) λx.x = I,
(ii) λx.c = Kc, c 6= x,
(iii) λx.P Q = S(λx.P)(λx.Q).
Таким образом,
N = (λx.x 4((λx.x)3))⊕
= S(λx.x 4)(λx.((λx.x)3))⊕
= S(S(λx.x)(λx.4))(S(λx.(λx.x))(λx.3))⊕
= S(SI(K 4))(S(λx.I)(K3))⊕
= S(SI(K 4))(S(K I)(K 3))⊕.
dc--5. Пользуясь этой процедурой, получили
N = S(SI(K 4))(S(K I)(K 3))⊕,
где Sxyz = xz(yz), Kxy = x, Ix = x.
dc--6. Используя какой-либо способ вычисления, получаем в резуль-
тате число “7”:
S(SI(K4))(S(KI)(K3))⊕ →
→ (SI(K 4)⊕)(S(K I)(K 3)⊕)
→ (I⊕)(K 4⊕)(S(K I)(K 3)⊕) → ⊕(K 4⊕)(S(K I)(K 3)⊕)
→ ⊕4(S(K I)(K 3)⊕) → ⊕4(K I⊕)(K3⊕)
→ ⊕4(I(K 3⊕)) → ⊕4 3 → 7.
Проверить результат легко прямым выполнением β-редукции для λ
-выражения:
M = (λx.x(4,(λx.x)3))+ → +(4,(λx.x)3) → +(4,3) → 7,
(еще раз обращаем внимание на использование другого символа опе-
рации сложения - “+” вместо “⊕”).
Контрольные вопросы.
1. Выпишите комбинаторные характеристики K, I, S, B, W, C
(стандартных комбинаторов).
2. Почему для реализации β-редукции показался удобным пере-
ход к комбинаторной логике?
Упражнения.
1. Выразите через комбинаторы K и S объект I с комбинаторной
характеристикой Ia = a.
Указание. Воспользуйтесь тем, что I = λz.z. Получите λz.z =
(λxyz.xz(yz))(λxy.x)(λxy.x)и вспомните, чтоK = λxy.x, S =
λxyz.xz(yz).
Ответ. I = SKK.
2. Для выражения:
let x = π/2 in let z = sin in sqr(z x); ;
постройте выражение комбинаторной логики и вычислите его
значение.
Указания.
(a) λ -выражение имеет вид:
(λx.(λz.sqr(z x))sin)π/2
= (λx.sqr(sin x))π/2, (β)
= sqr(sin π/2). (β)
(b) Воспользуйтесь тем, что
f(gx) = (f ◦ g)x = S(KS)K f g x.
Ответ. S(KS)K sqr sin π/2 = 1.
|
Главная
Каталог файлов
