1 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления Рекурсия в лямбда-исчислении fac = λn.(if (= n 0) 1 (* n (fac (- n 1)))) FB = λf.λn.(if (= n 0) 1 (* n (f (- n 1)))) Найти fac такой, что fac = FB fac Существует ли функция Y такая, что fac = Y FB ? Y F = F (Y F) Y -комбинатор; комбинатор фиксированной точки. Лямбда-выражение для Y -комбинатора: Y = λh.(λx.h (x x))(λx.h (x x)) Y FY F (λx.F (x x))(λx.F (x x)) F ((λx.F (x x))(λx.F (x x))) F (Y F) Тогда функция fac может быть записана с помощью выражения Y FB (λh.(λx.h (x x))(λx.h (x x))) (λf.λn.(if (= n 0) 1 (* n (f (- n 1))))) Это выражение неприводимо к нормальной форме!

2 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. Пример работы рекурсии, выраженной с помощью Y-комбинатора fac 2 (Y FB) 2 FB ((Y FB)) 2FB = λf.λn.(if (= n 0) 1 (* n (f (- n 1)))) (λn.(if (= n 0) 1 (* n ((Y FB) (- n 1))))) 2 if (= 2 0) 1 (* 2 ((Y FB) (- 2 1))) * 2 ((Y FB) (- 2 1)) * 2 ((λn.(if (= n 0) 1 (* n ((Y FB) (- n 1))))) (- 2 1)) * 2 (if (= (- 2 1) 0) 1 (* (- 2 1) ((Y FB) (- (- 2 1) 1)))) * 2 (* 1 ((Y FB) (- (- 2 1) 1))) * 2 (* 1 ((λn.(if (= n 0) 1 (* n ((Y FB) (- n 1))))) (- (- 2 1) 1))) * 2 (* 1 (if (= 0 0) 1 (* (- (- 2 1) 1) ((Y FB) (- (- (- 2 1) 1) 1))))) * 2 (* 1 1) 2

3 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. Взаимно рекурсивные функции f1 = F1(f1,...,fn) f2 = F2(f1,...,fn) fn = Fn(f1,...,fn)... T = (f1,...,fn) TUPLE-n – набор функций кортежирования T = TUPLE-n f1... fn INDEX – функция индексации fi = INDEX i T T = TUPLE-n F1(INDEX 1 T,..., INDEX n T)... Fn(INDEX 1 T,..., INDEX n T) Это обычная функция с прямой рекурсией, которая может быть выражена с помощью Y-комбинатора: Y (λT.TUPLE-n F1... Fn) а каждая из функций fi получается применением к этому выражению функции индексации: fi = INDEX i (Y (λT.TUPLE-n F1... Fn))

4 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления Чистое лямбда-исчисление Чистое лямбда-исчисление – это исчисление без констант и встроенных функций. Соответственно, отсутствует и δ-редукция; есть только λ-выражения и β-редукция. Покажем, что выразительная сила чистого лямбда-исчисления не меньше, чем у традиционного функционального языка программирования. 1. Функция IF, логические значения и булевы функции. IF p e1 e2 p e1 e2 TRUE e1 e2 e1 FALSE e1 e2 e2 TRUE = λx.λy.x FALSE = λx.λy.y IF = λp.λx.λy.p x y AND = λp.λq.p q FALSE OR = λp.λq.p TRUE q NOT = λp.p FALSE TRUE

5 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. 2. Списки и основные функции обработки списков Чистое лямбда-исчисление (продолжение) NULL (CONS A B) FALSE NULL = λt.t (λx.λy.FALSE) NULL NIL TRUE NIL = λx.TRUE проверка: NULL NIL (λt.t (λx.λy.FALSE))(λx.TRUE) (λx.TRUE)(λx.λy.FALSE) TRUE CONS A B λs.s A B CONS = λx.λy.λs.s x y CAR (λs.s A B) A CDR (λs.s A B) B CAR = λt.t TRUE CDR = λt.t FALSE проверка: CAR (CONS A B) CAR ((λx.λy.λs.s x y) A B) CAR (λs.s A B) (λt.t TRUE)(λs.s A B) (λs.s A B) TRUE TRUE A B A Дополнительные функции обработки списков JOIN = λp.λq.IF (NULL p) q (CONS (CAR p) (JOIN (CDR p) q)) избавляемся от явной рекурсии с помощью Y-комбинатора JOIN = Y (λf.λp.λq.IF (NULL p) q (CONS (CAR p) (f (CDR p) q)))

6 Кубенский А.А. Функциональное программирование. Глава 4. Основы лямбда-исчисления. 3. Целые числа и арифметика. 3 а. Представление в виде списков (подсчет элементов списка) Чистое лямбда-исчисление (продолжение) 0 = NIL SUCC = λn.CONS NIL n PRED = CDR n = (CONS NIL (CONS NIL (... NIL))) n раз EQ0 = NULL На базе этих основных функций можно построить всю арифметику. 3 б. Функциональное представление (подсчет применений функции). 0 = λf.λx.xn = λf.λx.(f (f (... x))) n раз SUCC = λn.λf.λx.(f (n f x)) PLUS = λm.λn.(m SUCC n) MULT = λm.λn.(m (PLUS n) 0) EQ0 = λn.(n (λx.FALSE) TRUE) PRED = λn.λf.λx.(n (λg.λh.(h (g f))) (λu.x) (λu.u)) проверка: PRED 0 λf.λx.(0 (λg.λh.(h (g f))) (λu.x) (λu.u)) λf.λx.((λu.x) (λu.u)) λf.λx.x 0 Проверим, что PRED 1 = 0 :

7 PRED = λn.λf.λx.(n (λg.λh.(h (g f))) (λu.x) (λu.u)) 1 = λf.λx.(f x) Вычитание PRED 1 = λf.λx.((λf.λx.(f x)) (λg.λh.(h (g f))) (λu.x) (λu.u)) PRED 1 = λf.λx.(((λg.λh.(h (g f))) (λu.x)) (λu.u)) PRED 1 = λf.λx.((λh.(h ((λu.x) f))) (λu.u)) PRED 1 = λf.λx.((λh.(h x)) (λu.u)) PRED 1 = λf.λx.((λu.u) x) PRED 1 = λf.λx.x = 0 Преимущество функционального представления состоит в том, что основные арифметические.операции и операции сравнения удается записать без рекурсии.

8 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ. Глава 5. Системы исполнения функциональных программ 5.1. Интерпретаторы и компиляторы. Программа (функция) Аргументы Результат применения функции Интерпретатор Схема интерпретации Исходная программа (функция) Компилятор Результирующая (эквивалентная) программа Схема компиляции В обоих случаях исходная функция служит в качестве входных данных; в случае компиляции результатом также является функция. Для получения результата необходима интерпретация аппаратным или программным интерпретатором.

9 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ Представление функциональных программ. Вводим простой функциональный язык – расширенное лямбда-исчисление; покажем, что все основные конструкции языка типа Haskell могут быть легко скомпилированы в это расширенное лямбда-исчисление. 1. Константы – целые числа, логические значения. c : 0 25 TRUE 2. Константы – примитивные функции. f : + = IF TUPLE-n INDEX 3. Лямбда-выражения. (λx.e) : λx.+ x x 4. Применение примитивной функции или лямбда-выражения к аргументу. (e1 e2) : (λx.+ x x) 2 5. Простой блок. (let x = e1 in e2) : let f = (λx.+ x x) in (f 2) 6. Рекурсивный блок. (letrec x1 = e1; x2 = e2;... xn = en in e) : letrec f = λn.IF (= n 0) 1 (* n (f (- n 1))) in (f 5) Таким образом, в чистое лямбда-исчисление введены константы, функции, связывание имен со значениями и рекурсия.

10 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ Представление функциональных программ. Компиляция с языка Haskell в расширенное лямбда-исчисление. 1. Исключаем все конструкции, связанные с определением и контролем типов: type, data, ::, class, instance 2. Многие конструкции переводятся (почти) без изменения: константа: c c примитивная функция: f f лямбда-выражение: (\x->e) (λx.e'), где e' – результат компиляции e переменная: x x применение функции: (e1 e2) (e1' e2'); e1+e2 (+ e1' e2') блоки: (e where f = e1) (let f = e1' in e') 3. Кортежи переводятся в применения примитивной функции TUPLE-n : кортеж: (e1, e2, e3) (TUPLE-3 e1' e2' e3') 4. Применение конструкторов переводится в применение примитивной функции TUPLE-n, первым аргументом которого служит номер конструктора в определении типа: например: [3] 3 : [] (TUPLE (TUPLE-1 0)) 5. Многие конструкции, такие как фильтры, арифметические прогрессии и т.п. переводятся в вызовы соответствующих примитивных функций.

11 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ. Компиляция с языка Haskell в расширенное лямбда-исчисление. 6. Определения функций, включающие образцы и условия, сначала переводятся в лямбда-выражения, содержащие конструкцию case в определяющем выражении. например: assoc x ((y,e):lst) | x == y = e | otherwise = assoc x lst assoc x [] = [] переходит в: assoc = \a1 -> \a2 -> case (a1, a2) of (x, ((y,e):lst)) | x == y -> e | otherwise -> assoc x lst (_, []) -> [] Конструкция case затем транслируется в расширенное лямбда-исчисление (далее). 7. Программный модуль (серия определений) транслируется в заголовок блока letrec. name_1 = expr_1 name_2 = expr_2... name_k = expr_k letrec name_1 = expr_1'; name_2 = expr_2';... name_k = expr_k' in Перед исполнением программы вычисляемое выражение компилируется и помещается в блок letrec после in.

12 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ. Компиляция case -выражения case param of pattern_1 | cond_11 -> expr_11 | cond_12 -> expr_12... pattern_2 | cond_21 -> expr_ pattern_k | cond_k1 -> expr_k1... letrec f1 = λa.IF (образец_1) let (связывание_1) in IF cond_11' expr_11' IF cond_12' expr_12'... (f2 a) (f2 a) f2 = λa.IF (образец_2) let (связывание_2) in IF cond_21' expr_21' IF cond_22' expr_22'... (f3 a) (f3 a)... fk = λa.IF (образец_k)... error error in f1 param'

13 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ. Компиляция сопоставления с образцом и связывания case y) of ([], (e:_)) -> expr Аргумент arg, удовлетворяющий образцу, должен иметь вид: ( [], ( (:) e _ )) (TUPLE-2 (TUPLE-1 0) (TUPLE-3 1 e foo)) (AND (EQ (INDEX 1 (INDEX 1 arg)) 0) (EQ (INDEX 1 (INDEX 2 arg)) 1)) arg[1,1] == 0 && arg[2,1] == 1 Возможно также сопоставление с константой: case arg of [25] -> expr ((:) 25 []) arg[1] == 1 && arg[2] == 25 && arg[3,1] == 0 Связывание: x = arg[1]; y = arg[2]; e = arg[2,2]

14 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ. Представление программ расширенного лямбда-исчисления data Expr = Integral Integer | Logical Bool -- константы | Function String -- примитивные функции | Variable String -- переменные | Lambda String Expr -- лямбда-выражение | Application Expr Expr -- применение функции | Let String Expr Expr -- простой блок | Letrec [(String, Expr)] Expr -- рекурсивный блок например: let plus = (λx.λy.x+y) in (plus 1 2) будет представлено в виде: (Let "plus" (Lambda "x" (Lambda "y" (Application (Application (Function "+") (Variable "x")) (Variable "y")))) (Application (Application (Variable "plus") (Integral 1)) (Integral 2)) )