Сошников Дмитрий Валерьевич к.ф.-м.н., доцент Сошников Д.В. Факультет инноваций и высоких технологий Московский физико-технический институт

2 Лекция 15 Нормальный и аппликативный порядок редукции. Теорема Чёрча-Россера

©2008 Сошников Д.В. 3 Рассмотрим выражение: (λx.λy.y) ((λz.z z) (λz.z z)) (λx.λy.y) ((λz.z z) (λz.z z)) λy.y (λx.λy.y) ((λz.z z) (λz.z z)) (λx.λy.y) ((λz.z z) (λz.z z)) (λx.λy.y) ((λz.z z) (λz.z z)) … Первый порядок редукции соответствует случаю, когда аргумент функции не вычисляется до того момента, когда он действительно понадобится. Это называется вызовом по имени (или по текстовой замене), и соответствует ленивым вычислениям. Во втором случае аргумент вычисляется первым. Это – вызов по значению.

©2008 Сошников Д.В. 4 Самый левый (правый) редекс – символ λ которого находится самым левым (правым) в выражении Самый внешний редекс – не содержится внутри никакого другого редиска Самый внутренний редекс – не содержит в себе никакого другого редиска * - рефлексивно-транзитивное замыкание операции редукции

©2008 Сошников Д.В. 5 (λx.λy.y) ((λz.z z) (λz.z z)) Внутренний редекс Внешний редекс

©2008 Сошников Д.В. 6 Аппликативный порядок (АПР) – сначала преобразуется самый левый из самых внутренних редексов Соответствует энергичным вычислениям Более эффективен в машинной реализации Нормальный порядок (НПР) – сначала преобразуется самый левый из самых внешних редексов Соответствует ленивым вычислениям При реализации «в лоб» вычисляет выражения повторно

©2008 Сошников Д.В. 7 (λx.x+x)(2+3) АПР: (λx.x+x) НПР: (2+3)+(2+3) 5+(2+3) При НПР одни и те же выражения могут вычисляться повторно (эффект разделения) Для устранения этого недостатка используют различные техники: Мемоизация, вычисление с контекстом Редукция графов с циклическими ссылками

©2008 Сошников Д.В. 8 (λx.x+x)(2+3) x+x, где x=2+3 5+x, где x=

©2008 Сошников Д.В. 9 (λx.E1)E2 Вычисляем E2, подставляем результат в E1 Соответствует АПР Вызов по значению (энергичные вычисления) НПР без замены переменных для устранения конфликта имен Вызов по текстовой замене НПР с обходом конфликта имен с помощью переименования, но с повторным вычислением выражения Вызов по имени Вызов по имени + мемоизация В функциональных языках без побочных эффектов эквивалентен вызову по имени Вызов по необходимости (ленивые вычисления)

©2008 Сошников Д.В. 10 Редукция заканчивается, когда в выражении больше нет редексов Такая форма выражения называется нормальной формой Два выражения называются α-эквивалентными ( ), если они эквивалентны с точностью до α-преобразования (имен переменных) Два выражения называются α-эквивалентными ( ), если они эквивалентны с точностью до α-преобразования (имен переменных)

©2008 Сошников Д.В. 11 Если выражение E * E 1 и E * E 2, где E 1,E 2 – нормальные формы, то E 1 E 2 Ромбическое свойство (обобщение) E E1E1 E2E2 N Есть ли противоречие с «зацикливающимся» примером? Если E * E 1 и E * E 2, то N : E 1 * N и E 2 * N В этом случае редукция называется редукцией Черча-Россера ** * *

©2008 Сошников Д.В. 12 Другая формулировка: E 1 * E 2 N : E 1 * N и E 2 * N Из теоремы следует единственность нормальной формы Мораль: Если нам удается получить нормальную форму, то она не зависит от порядка редукции Однако некоторые порядки редукции не позволяют придти к нормальной форме

©2008 Сошников Д.В. 13 Если выражение E имеет нормальную форму N, то применение НПР на каждом этапе приводит к M : N M Использование ленивых вычислений гарантирует вычислимость выражений

©2008 Сошников Д.В. 14 (λx.Ex)A = EA (если x FV(E)) λx.Ex E ( x) f x = g x f = g Экстенсиональность - это выведение равенства функции из равенства значений функции на множестве всех аргументов

©2008 Сошников Д.В. 15 При β-преобразовании возникает проблема конфликта имен Замена переменных с помощью α-преобразования - неэффективна Возможные решения: Не редуцировать выражение до тех пор, пока у функции не будут известны все аргументы λx.((λy.λx.y+x)x) – не редуцируем, ждем аргумента λx.((λy.λx.y+x)x)4 (λy.λx.y+x)4 λx.4+x Избавиться от имен переменных вообще, заменив их номерами

©2008 Сошников Д.В. 16 Избежать проблемы конфликта имен можно, на каждом шаге редуцируя выражения до СЗНФ (а не до НФ) Выражение E находится в СЗНФ, если: E – константа или переменная E = λx.E E = PE 1 E 2 …E n для константной функции P арности k>n

©2008 Сошников Д.В. 17 Для структуры выражения имена переменных несущественны Можно избавиться от переменных, заменив их номером – глубиной связывания Глубина связывания – количество символов λ от начала выражения до указанной переменной Пример: λx.λy.λf.f(λx.x)(x+y) λ.λ.λ.0(λ.0)(2+1) Имена переменных после λ удаляются, подчеркнутые числа означают переменные с соответствующей глубиной связывания λx.λy.λf.f(λx.x)(x+y) 2 1