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 2 = 1 : Преимущество функционального представления состоит в том, что основные арифметические.операции и операции сравнения удается записать без рекурсии.