 |
Порядок редукций и нормальные формы
|
|
|
|
Говорят, что l-выражение находится в нормальной форме, если к нему нельзя применить никакое правило редукции. Другими словами, l-выражение - в нормальной форме, если оно не содержит редексов. Нормальная форма, таким образом, соответствует понятию конца вычислений в традиционном программировании. Отсюда немедленно вытекает наивная схема вычислений:
while существует хотя бы один редекс
do преобразовывать один из редексов
end
(выражение теперь в нормальной форме).
Какие выбирать редексы?
Пример:
(lx. ly. y) ((lz. z z) (lz. z z))
® (lx. ly. y) ((lz. z z) (lz. z z))
® (lx. ly. y) ((lz. z z) (lz. z z))
®...
(бесконечный процесс редукции)
(lx. ly. y) ((lz. z z) (lz. z z))
®ly. y
(редукция закончилась)
Порядок редукций (стратегия выбора редексов).
Самым левым редексом называется редекс, символ l которого (или идентификатор примитивной функции в случае d-редекса) текстуально расположен в l-выражении левее всех остальных редексов. (Аналогично определяется самый правый редекс.)
Самым внешним редексом называется редекс, который не содержится внутри никакого другого редекса.
Самым внутренним редексом называется редекс, не содержащий других редексов.
В контексте функциональных языков и l-исчисления существуют два важных порядка редукций.
Аппликативный порядок редукций (АПР), который предписывает вначале преобразовывать самый левый из самых внутренних редексов.
Нормальный порядок редукций (НПР), который предписывает вначале преобразовывать самый левый из самых внешних редексов.
(lx. ly. y) ((lz. z z) (lz. z z)) - самый левый из самых внутренних редексов - вычисление никогда не закончится.
(lx. ly. y) ((lz. z z) (lz. z z)) - самый левый из самых внешних редексов - вычисление закончится за один шаг.
|
|
|
Функция lx. ly. y - это классический пример функции, которая отбрасывает свой аргумент. НПР в таких случаях эффективно откладывает вычисление любых редексов внутри выражения аргумента до тех пор, пока это возможно, в расчете на то, что такое вычисление может оказаться ненужным.
АПР оказывается значительно более эффективным при реализации на обычных компьютерах.
НПР - ленивые вычисления. “Не делай ничего, пока это не потребуется” - механизм вызова по необходимости (все аргументы передаются функции в не вычисленном виде и вычисляются только тогда, когда в них возникает необходимость внутри тела функции).
АПР - энергичные вычисления. “Делай все, что можешь”; другими словами, не надо заботиться о том, пригодится ли, в конечном счете, полученный результат - механизм вызова по значению (значение аргумента передается в тело функции).
Теорема Чёрча-Россера (следствие). Если выражение E может быть приведено двумя различными способами к двум нормальным формам, то эти нормальные формы являются алфавитно-эквивалентными.
Теорема стандартизации. Если выражение E имеет нормальную форму, то НПР гарантирует достижение этой нормальной формы (с точностью до алфавитной эквивалентности).
Рекурсивные выражения
Проблема рекурсивных функций в l-исчислении, где функции не имеют имени: необходимо придумать метод, позволяющий функциям вызывать себя не по имени, а каким-то другим образом.
Представим рекурсивную функцию как функцию, имеющуюе себя в качестве аргумента. В этом случае функция может оказаться связанной с одной из её собственных переменных и будет, таким образом, содержать в своем теле ссылки на самое себя.
Рассмотрим, например, рекурсивную функцию sum, определенную на языке Лисп следующим образом:
(defun sum (n)
(if (= n 0) 0 (+ n (sum (1- n))))
)
Это выражение может быть представлено в виде l-абстракции, имеющей дополнительный параметр, который при применении этой абстракции связывается с самой функцией. Мы запишем эту промежуточную версию функции sum:
|
|
|
sum = ls. ln. IF (= 0 n) 0 (+ n (s (1- n)))
Все, что нам осталось сделать теперь, - это связать переменную s со значением функции sum, которую пытаемся определить. Это можно сделать, использовав специальную функцию, называемую Y-комбинатором, которая удовлетворяет следующему уравнению:
Y f = f (Y f)
Y также известен как комбинатор неподвижной точки. “Неподвижная точка” функции f - это выражение, которое не изменяется при применении к нему функции f. (Заметим, что функция может иметь несколько неподвижных точек. Например, функция тождества lx. x, имеет бесконечное их число.) Выражение Y f дает наименьшую неподвижную точку функции f.
Y sum
= Y(ls. ln. IF (= 0 n) 0 (+ n (s (1- n))))
® (ls. ln. IF (= 0 n) 0 (+ n (s (1- n)))) (Y sum)
® ln. IF (= 0 n) 0 (+ n ((Y sum) (1- n)))
® ln. IF (= 0 n) 0
(+ n ((lm. IF (= 0 m) 0 (+ m ((Y sum) (1- m))))
(1- n))))
Данное выражение ведет себя точно так же, как исходное рекурсивное определение sum. Внутреннее вхождение Y sum конструирует копию исходной функции sum, помещая само себя (т. е. Y sum) вместо s в тело копии.
Таким образом, функция sum выражается в l-исчислении в виде
Y(ls. ln. IF (= 0 n) 0 (+ n (s (1- n))))
Проверим:
(Y(ls. ln. IF (= 0 n) 0 (+ n (s (1- n))))) 1
® ln. IF (= 0 n) 0 (+ n ((Y(ls. ln. IF (= 0 n) 0 (+ n (s (1- n)))))
(1- n))) 1
® IF (= 0 1) 0 (+ 1 ((Y(ls. ln. IF (= 0 n) 0 (+ n (s (1- n)))))
(1- 1)))
® (+ 1 ((Y(ls. ln. IF (= 0 n) 0 (+ n (s (1- n))))) 0))
® (+ 1 (ln. IF (= 0 n) 0
(+ n ((Y(ls. ln....))))) 0)
® (+ 1 (IF (= 0 0) 0 (+ 0 ((Y (ls. ln....))))))
® (+ 1 0)
® 1
В общем случае рекурсивная функция f с телом, задаваемым выражением E, записывается в l-исчислении в виде Y (lf. E).
Определение Y
Y = lh. (lx. h (x x)) (lx. h (x x))
Проверим:
Yf=
(lh. (lx. h (x x)) (lx. h (x x))) f
® (lx. f (x x)) (lx. f (x x))
® f ((lx. f (x x)) (lx. f (x x)))
® f (Y f)
Чистое l-исчисление
Удалив константы и d-правила, мы получаем чистое l-исчисление. В нем можно выразить любые константы и функции.
Булевы константы и условное выражение
TRUE = lx. ly. x TRUE A B ® A
FALSE = lx. ly. y FALSE A B ® B
IF = lp. lq. lr. p q r
IF TRUE A B =
(lp. lq. lr. p q r) (lx. ly. x) A B
® (lq. lr. (lx. ly. x) q r) A B
® (lq. lr. (ly. q) r) A B
® (lq. lr. q) A B
® (lr. A) B
® A
Конструктор списков и функции-селекторы. Определим список как выражение CONS A B, где
CONS = lh. lt. ls s h t
FIRST = lL. L TRUE
REST = lL. L FALSE
FIRST (CONS A B) =
(lL. L TRUE) (CONS A B)
® (CONS A B) TRUE
® ((lh. lt. ls s h t) A B) TRUE
|
|
|
® ((lt. ls s A t) B) TRUE
® (ls s A B) TRUE
® TRUE A B
= (lx. ly. x) A B
® ly. A B
® A
Натуральные числа. Натуральное число n часто представляется термом n -кратной композиции (обозначение x^n(y) служит сокращением для x(x(...(xy)...)), x повторяется раз).
Для каждого натурального числа n положим
<0> = lx. ly. y, <n> = lx. ly. x^n (y)
Тогда сложение чисел определяется ламбда-выражением
+ x y = lp. lq. x p (y p q)
Проверим, что определение удачно.
+ 1 1 = lp. lq. <1> p (<1> p q)
= lp. (lq. ((lx. ly. x y) p ((lx. ly. x y) p q)))
® lp. (lq. ((lx. ly. x y) p p q))
® lp. (lq. (p p q))
= <2>
Ламбда-абстракции в Лиспе
Лисп заимствовал из l-исчисления три основных идеи.
· Для определения функций используются l-термы.
· Основное правило вычисления b-редукция.
· Определения функций являются полноправными данными.
Отличия Лиспа от l-исчисления. Существуют функции, которые при вызове не вычисляют сразу значения своих аргументов (Quote, Cond и т. д.). Благодаря этому можно отличить списки, воспринимаемые как от списков, воспринимаемых как указания к вычислению функций. «Для того чтобы некоторая сугубо логическая концепция могла найти применение в реальном программировании, ее надо основательно «подпортить»».
В Лиспе ламбда-абстракция имеет вид
(lambda (x1 x2 … xn) <body>)
l-вызов соответствует вызову функции
(ламбда-выражение a1 a2 … an)
((lambda (x y) (+ (* x x) (* y y))) 6 7) ® 85
Вычисление ламбда-вызова или применение ламбда-выражения к фактическим параметрам производится в два этапа. Сначала вычисляются значения фактических параметров и соответствующие формальные параметры связываются с полученными значениями. Этот этап называется связыванием параметров. На следующем этапе с учетом новых связей вычисляется форма, являющаяся телом ламбда-выражения, и полученное значение возвращается в качестве значения ламбда-вызова.
Композиция ламбда-вызовов
У ламбда-вызова тело вновь ламбда-вызов
((lambda (y)
((lambda (x) (list x y)) 0))
1)
® (0 1)
Ламбда-вызов, у которого аргументом является новый ламбда-вызов
((lambda (x) (list 2 x))
|
|
|
((lambda (y) (list y)) 1))
® (2 (1))
Ламбда-выражение - это безымянная функция, которая пропадает тотчас после вычисления значения формы. Ее трудно использовать снова, так как нельзя вызывать по имени, хотя ранее выражение было доступно как списочный объект. Безымянные функции используются как фактические параметры в функциях высших порядков (в чем собственно и состоит сила функционального программирования).
|
|
|
