1 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. Будем задавать функции с помощью «лямбда-выражений», которые будем преобразовывать по определенным правилам (правила «вычислений»). Основные типы лямбда-выражений: переменная константа применение функции определение функции x +3nilc ((+ 2) 3) (e1 e2) (λx.((+ 2) x)) (λx.e) + 2 x λx. Свободная переменная Связывающее вхождение (λx.+ x y) x Связанная переменная Этот x связан Этот x свободен 4.1. Основные понятия Замкнутое выражение – выражение, не содержащее свободных переменных. (λx.(x x))

2 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. Правила преобразований выражений. 1. δ-редукция f e1 e2... ek result or T F T 2. β-редукция (λx.e1) e2 e1{x|e2}(λx.+ 1 x) (λx.x x)(λx.x x) 3. α -преобразование λx.e1 λz.e1{x св. |z}λx.((λy.λx.+ x y) x) λz.((λy.λx.+ x y) z) 4. η-преобразование λx.E x Eλx.((λy.λx.+ x y) x) (λy.λx.+ x y)

3 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. Примеры преобразования выражений (λx.λy.+ x y) 2 5 (λy.+ 2 y) 5 ( β-редукция) ( β-редукция) 7 ( δ-редукция) (λx.λy.y)((λx.x x)(λx.x x)) Функция Аргумент (λy.y) ( β-редукция) (λx.λy.y)((λx.x x)(λx.x x))... От порядка применения редукций может зависеть результат!

4 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. Ромбическое свойство системы редукций α 0 α 1 … α k α 0 * α k Нормальная форма: лямбда-выражение, к которому не применимы β- и δ-редукции α0α0 * * β1β1 β2β2 ω * * Теорема (Черча – Россела): система преобразований, основанная на применении β-редукций обладает ромбическим свойством. Следствие: лямбда-выражение не может иметь более одной нормальной формы. Замечание: в некоторых случаях применение редукций может, в зависимости от порядка, либо приводить к нормальной форме, либо не приводить к ней. существует (?) форма ω Отношение * это рефлексивное транзитивное замыкание отношения

5 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. Стандартные порядки редукций. Редекс (redex) – выражение, к которому применима одна из редукций. Reducible Expression – редуцируемое выражение.β-редекс; δ-редекс… Выражение может содержать (или не содержать) один или несколько редексов. Выражение (λx.λy.y)((λx.x x)(λx.x x)) содержит два редекса. Внутренний редекс Внешний редекс Самый левый (самый правый) редекс – текстуально расположен левее (правее) других. Самый внутренний редекс – не содержит внутри себя других редексов. Самый внешний редекс – не содержится внутри никакого другого редекса. Аппликативный порядок редукций – редукция всегда применяется к самому левому из самых внутренних редексов Нормальный порядок редукций – редукция всегда применяется к самому левому из самых внешних редексов

6 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. Еще пример редукции выражения (λx.* x x)((λy.+ 1 y) 2) Аппликативный порядок редукций (λx.* x x)(+ 1 2) (λx.* x x) 3 * – нормальная форма Нормальный порядок редукций * ((λy.+ 1 y) 2) ((λy.+ 1 y) 2) * (+ 1 2) ((λy.+ 1 y) 2) * 3 ((λy.+ 1 y) 2) * 3 (+ 1 2) * – нормальная форма β-редукция δ-редукция β-редукция δ-редукция β-редукция δ-редукция β-редукция δ-редукция

7 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. Сравнение различных порядков редукций. Аппликативный порядок (АПР)Нормальный порядок (НПР) Не приводит к копированию одних и тех же выражений, если они не находятся в нормальной форме. Одни и те же выражения аргументов могут многократно копироваться при подстановке в тело лямбда-выражения. Выполняет редукцию даже тех выражений, которые в дальнейшем могут быть отброшены. Никогда не редуцирует выражение, если это может оказаться впоследствии ненужным. Может не приводить к нормальной форме, даже если она существует. Всегда приводит выражение к нормальной форме, если только она вообще существует. Преобразование выражения к нормальной форме в АПР соответствует энергичному порядку вычислений выражений в языках программирования. Преобразование выражения к нормальной форме в НПР соответствует вычислениям выражений с подстановкой аргументов «по наименованию».

8 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. Проблема конфликта имен. λx.((λy.λx.+ x y) x) Свободное вхождение переменной Связанное вхождение переменной λx.(λx.+ x x)λz.((λy.λx.+ x y) z) α-преобразование λx.(λz.+ x z)

9 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. Слабая заголовочная нормальная форма (СЗНФ) Выражение, не имеющее свободных переменных (замкнутое) находится в СЗНФ, если оно имеет один из следующих видов: Константа c Определение функции λx.E Частичное применение функции P E 1 E 2... E k Выражение λx.((λy.λx.+ x y) x) находится в СЗНФ. Вычисления, происходящие при исполнении программы в «ленивых» вычислениях, соответствуют редукции выражения в НПР до приведения к СЗНФ, дополненной эффектом «разделения» значений переменных при подстановке аргумента, еще не находящегося в СЗНФ. (λx.+ x x)(* 2 3) + (* 2 3) (* 2 3) + 6 (* 2 3) x x (* 2 3) + x x 6 12

10 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. Итоги: механизмы редукций в лямбда-исчислении 1. От способа применения редукций может зависеть окончательный вид выражения, но не его функциональный смысл. 2. Если выражение может быть приведено к нормальной форме, то это может быть сделано с помощью редукций в НПР, возможно, с переименованиями переменных. 3. Аппликативный порядок редукций, приводящий выражение к СЗНФ соответствует энергичной схеме вычислений, принятой в некоторых функциональных языках. 4. «Ленивая» схема вычислений может быть смоделирована приведением выражений к СЗНФ при применении НПР + разделение переменных.