нормальную форму.
(iii) Если Е = Е' и Е и Е′ оба находятся в нормальной форме, тогда
Е и Е′ идентичны вплоть до α-конверсии.
Доказательство
Если Е имеет нормальную форму, тогда Е = E′ для какого - то Е′ в нормальной форме. По теореме Чёрча-Россера существует E′′ , такое что Е → E′′ и E′ → E′′. Т. к. E′ находится в нормальной форме, единственные редексы которые оно может содержать - α-редексы, а отсюда следует что редукция E′ → E′′ должна состоять из последовательности α-конверсий. Таким образом, E′′ должно быть идентично с E′ , за исключением имен некоторых связанных переменных; также оно должно быть в нормальной форме, как и E′. Предположим что Е имеет нормальную форму и Е = E'. Т. к. Е имеет нормальную форму, Е = E′′, где Е′′ находится в нормальной форме. Следовательно, Е′ = E′′ в следствии транзитивности = , и значит Е′ имеет нормальную форму. Доказано выше.
Упражнение 33
Для каждого из следующих λ-выражений найдите либо его нормальную форму, либо покажите что оно не имеет нормальной формы.
add 3 add 3 5 (λx. x x) (λx. x) (λx. x x) (λx. x x) Y Y (λy. y) Y (λf x. ( iszero x → 0 | f ( pre x))) 7
€
Необходимо отметить, что λ-выражение Е может иметь нормальную форму даже если существует бесконечная последовательность Е → Е1 → Е2 … . Например, (λx. 1)(Y f) имеет нормальную форму 1 , хотя и :
(λх. 1) (Y f) → (λx. 1 ) (f (Y f)) → … (λx. 1 ) (fn (Y f)) → …
Теорема нормализации, приведенная ниже, утверждает, что можно избежать таких слепых переходов, редукцией крайних слева β- или η- редексов, где “ крайний слева” означает редекс у которого начало λ находится так далеко слева, насколько это возможно.
Другой важный момент, который следует отметить – это то, что Е1 может не иметь нормальную форму, даже если Е1 Е2 имеет нормальную форму.
Например, Y не имеет нормальной формы, но Y (λx. 1 ) → 1. Частой ошибкой - считать, что λ-выражения без нормальной формы означают “неопределенные” функции. Y не имеет нормальной формы, но означает вполне определенную функцию( математическую характеристику функции Y можно найти в книге Стоя). Анализ, оставшийся за рамками данной работы ( [37]), показывает, что λ-выражение соответствует неопределенной функции тогда и только тогда, когда оно не может быть обращено в выражение в головной нормальной форме, где Е находится в головной нормальной форме, если оно имеет форму
λV1 … Vm. V E1 … En
где V1 … Vm и V переменные, а Е1, …, Еn - λ-выражения (V может быть либо эквивалентно Vi для какого-то i, либо отличаться от всех). Следовательно оператор неподвижной точки Y не является неопределенным, потому что он может быть обращен в
λf. f ((λx. f(x x)) (λx. f(x x))) ,
а это –головная нормальная форма.
Можно показать, что выражение Е имеет головную нормальную форму тогда и только тогда когда существуют выражения E1, … , En такие что
E E1 … En имеют нормальную форму. Этот факт также поддерживает интерпретацию выражений без головной нормальной формы как неопределенные функции: если Е неопределенно, это означает, что
Е Е1 … Еn никогда не завершится для любых Е1, …, Еn. Полную информацию насчет головных нормальных форм и их отношений с определенностью можно найти в книге Баредгрета [2].
Теорема нормализации
Если Е имеет нормальную форму, тогда повторяя редукцию крайних
слева β- или η- редексов ( если возможно после α-конверсии для того
чтобы избежать неправильных замен) можно превратить исходное
выражение в выражение в нормальной форме.
Пояснение насчет α-конверсий в формулировке теоремы призвано покрыть случаи подобные следующему :
(λx. (λy. x y)) y → λy′ . y y′
где была произведена α-конверсия λy. x y → λy′. x y′ для того, чтобы исбежать неправильной замены (λy. x y)[y/x] = λy. y y.
Последовательность редукций, в которых производится редукция крайнего слева редекса называется нормальной последовательностью редукций.
В теореме нормализации говорится о том, что если Е имеет нормальную форму ( т. е. для какого-то Е′ в нормальной форме Е = E′), тогда она может быть найдена нормальной последовательностью редукций. Но зачастую это не самый эффективный способ её нахождения. Например, для последовательности нормальных редукций требуется редуцировать
(λx. ~~x~~x~~)E
к
~~E~~E~~
Если Е не находится в нормальной форме, тогда будет более эффективно сперва редуцировать Е к, скажем, Е′ (где Е′ находится в нормальной форме) , а затем редуцировать
(λx. ~~ x ~~ x~~ ) E′
к
~~E′~~E′~~
таким образом избежав необходимости редуцировать Е дважды.
Необходимо заметить, что так называемая схема “вызова-по-значению”
не работает в случаях вроде такого:
(λx. 1) ((λx. x x)( λx. x x))
Нахождение оптимального алгоритма для выбора следующего редекса для редукции является сложной проблемой. Последние разработки в этой области изложены в работе Ли [25].
Из-за того, что нормальная последовательность редукций оказалась неэффективной, некоторые языки программирования основанные на
λ-исчислении, например LISP, используют вызов по значению, даже не смотря на то, что он не всегда выполняется. Вообще говоря, кроме эффективности, у вызова по значению имеется ряд других преимуществ, особенно когда язык “нечист”, т. е. имеет конструкции со сторонними эффектами (напр. присваиваниями). С другой стороны, в последних разработках предпологается, что вычисление нормальной последовательности редукций может оказаться не настолько неэффективным, как представлялось раньше, если использовать хитрые
приёмы, наподобие редукции по графу (см. далее). Вопрос о том, следует ли в функциональных языках программирования использовать нормальную последовательность или вызов по значению до сих пор остаётся открытым.
2.10 Вызов по значению и Y
Произведем вызов Y:
LET Y = λf. (λx. f(x x))( λx. f(x x))
К сожалению, с Y не работает вызов по значению, потому что получается цикл из-за порядка аппликаций.
Y f → f (Y f)
→ f (f (Y f))
→ f (f (f (Y f)))
.
.
.
Для того, чтобы это избежать, определим:
∧
LET Y = λf. (λx. f(λy. x x y)) (λx. f(λy. x x y))
∧
Обратите внимание, что Y это Y, в котором произведена η- конверсия
∧
“x x” в “λy. x x y”. Y не входит в цикл при вызове по значению:
∧ ∧
Y f → f (λy. Y f y)
Вызов по значению не вычисляет λs, и, таким образом, удаётся избежать цикличности.
Глава 3. Комбинаторы.
Комбинаторы лежат в основе альтернативной к λ-исчислению теории функций. Первоначально, они были введены логиками как способ изучения замен. Позднее, Тёрнер показал, что комбинаторы дают хороший “машинный код”, в который можно компилировать функциональные программы [34]. На основании идей Тёрнера были построены несколько эксперементальных компьютеров (например см. [8]), и результаты обнадёживают. Как работают эти машины, объяснено в разделе 3.3. Комбинаторы также дают хороший промежуточный код для конверсионных машин; некоторые из лучших компиляторов для функциональных языков основаны именно на нём
( например см. [11,1]).
Также существуют два эквивалентных способа формулирования теории комбинаторов:
через λ-исчисление, как отдельная теория.В данной работе используется первый подход, т. к. он немного проще, но исторически сначала был использован второй подход1.
|
Из за большого объема этот материал размещен на нескольких страницах:
1 2 3 4 5 6 7 8 9 10 11 |
