ТМВ-2020-Лекция-07.04.2020

Материал из Кафедра Прикладной Математики
Перейти к навигации Перейти к поиску

Тема лекции - λ - моделирование.

λ - моделирование

1) \(<=>\) отношение конверсии. Это симметрично относительно \(=>\)

\((\lambda m.m)f <=> f\)

  • \(\alpha\) - конверсия
  • \(\beta\) - редукция
  • обращение операций к \(\beta\) - редукции

\(\lambda x.xy <=> (\lambda zx.xz)y\)

2) Комбинатор - замкнутый \(\lambda\) - терм (без свободных переменных).

Логические значения

boolean

\(true = \lambda x_1 x_2.x_1\)

\(false = \lambda x_1 x_2.x_2\)

Если есть комбинатор \(B \in {true, flase}\), тогда для любых \(\forall \lambda\) - термов \(M,N\)

\( BMN = \begin{cases} M \mbox{, если B - true } \\ N \mbox{, иначе } \end{cases} \)

Эти конструкции очень похожи на \(if ... then ... else\).

Примеры

\(true\ x\ y = (\lambda x_1 x_2.x_1)xy = (((\lambda x_1 x_2.x_1)x)y) = ((\lambda x_2.x)y) = x\)

То есть сама по себе булева переменная является функцией логического вывода.

Логические функции (примеры)

Оператор \(And\)

\(And\ True\ True = True\), иначе \(False\)

Если первая переменная \(False\), то мы, не проверяя вторую переменную, возвращаем \(Fasle\).

\(And = \lambda x_1 x_2.x_1 x_2\ False = \lambda x_1 x_2. x_1 x_2 x_1\)

Оператор \(Or\)

\(Or\ False\ False = False\), иначе \(True\)

\(Or = \lambda x_1 x_2.x_1\ true\ x_2 = \lambda x_1 x_2.x_1 x_1 x_2\)

\(Or\ False\ False = False\ False\ False = (\lambda x_1 x_2.x_2) False\ False = False\)

\(Or\ True\ False = True\ True\ False = (\lambda x_1 x_2.x_1)\ True\ False = True\)

Оператор \(Not\)

\(Not\ False = True, Not\ True = False\)

\(Not = \lambda x.x\ False\ True\)

\(Not = \lambda x.x\ True\ False\)

Как конструировать типы

\(True = \lambda x_1 x_2.x_1\) правая часть - \(\lambda\) проекция

Алгоритм конструирования:

1) Определяем базовые \(\lambda\) - проекции

2) Построить другие комбинаторы а их основе

Пары

\(pair\ x\ y = \)"\(<x, y>\)"

\(fst (pair\ x\ y) = x\) - взятие первого компонента

\(snd (pair\ x\ y) = y\) - взятие второго компонента

Комбинатор \(pair\):

\(pair = \lambda x_1x_2f.fx_1x_2\)

\(pair\ x \ y = (\lambda x_1 x_2 f.f x_1 x_2)xy = \lambda f.fxy\)

\(fst(pair\ x\ y) = (\lambda p.p\ true)(\lambda fxy) = (\lambda f.fxy)true = true\ x\ y = x\)

\(snd = \lambda p.p\ false\)

\(pair\ x\ y = \lambda f.fxy\) и \(pair = \lambda xyf.fxy\) - эквивалентны

Натуральные числа (нумералы)

Определим 0:

\(0 = \lambda fx.x\)

Определим 1:

\(1 = \lambda fx.fx\)

Определим n:

\(n = \lambda fx.f(...(fx))\), где \(f\) ровно \(n\) штук

Операции над числами

succ

Прибавление к числу единицы: \(succ\ n = n + 1\)

\(succ = \lambda nfx.f(nfx)\)

Пояснение:

\(nf = f^n\)

\(3f = (\lambda fx. f(f(fx))) = f^3\)

Таким образом,

\(succ \ n =(\lambda nfx.f(nfx))n = \lambda fx.f(nf)x = \lambda fx.f(\lambda x.(f(f...(fx)))1) = \lambda fx.f(f(f...(fx)))\)

add

Сложение двух чисел: \(add\ n\ m = n + m\)

\(add = \lambda nm.(m succ) n = \lambda nmfx.mf(nfx)\)

mult

Произведение двух чисел: \(mult\ m\ n = m*n\)

\(mult = \lambda nmfx.m(nf)x\)

exp

Возведение в степень: \(exp\ n\ m = n^m\)

\(exp = \lambda nmfx.mnfx = \lambda nmfx.((mn)f)x\)

sub и pre

Вычитание двух чисел: \(sub \ m \ n = max\{n - m, 0\}\) (так как у нас есть только натуральные числа)

Вычитание единицы: \(pre\ n = max\{n - 1, 0\}\)

Мы хотим построить такую функцию, что \(g: (x,y) \rightarrow (f(x),x)\), где \(f\) - фиксированная функция.

\(g = \lambda p.pair(f(fst\ p))(fst\ p)\)

\(gf = \lambda fp.pair(f(fst\ p))(fst\ p)\)

Пример: \(2gxy = g(f(x),x) = (f(f(x)),f(x))\)

В общем виде: \(ngxy = (f^n(x), f^{n-1}(x))\)

\(pre = \lambda nfx.snd(ngf(pair\ x x))\)

Подставим аргументы и посмотрим, как это работает:

\(pre\ 0 = \lambda fx.snd(0 gf(pair\ x x)) = \lambda fx.snd(pair(x x)) = \lambda fx.x = 0\)

\(pre\ 1 = \lambda fx.snd(1 gf(pair\ x x)) = \lambda fx.snd((\lambda fx.fx)gf(pair x x)) = \lambda fx.(snd((\lambda x.(\lambda fp.pair(f(fst p))(fst p)) 2)(pair x x)) = \)

\(\lambda fx.snd((\lambda fp.pair(f(fst p))(fst p))(pair x x))\)

Рекурсивное программирование

\( n! = \begin{cases} 1 \mbox{, n = 0 } \\ n * (n - 1) \mbox{, иначе } \end{cases} \)

Проверка на нуль:

\(iszero = \lambda n.n(\lambda z.false) true\)

Примеры:

\(iszero\ 0 = (\lambda fx.x)(\lambda z.false) true = true\)

\(iszero\ 1 = (\lambda fx.fx)(\lambda z.false) true = (\lambda z.false) true = false\)

\(fact = \lambda n.(iszero\ n) 1 (mult\ n(fact (pre\ n)))\)

В общем случае у нас есть уравнение: \(F = \lambda m.mF\)

В \(\lambda\) - исчислении есть универсальный способ решения рекурсивных уравнений.

Теорема 1 (о неподвижной точке)

\(\forall \ \lambda\) - терма \(F\) существует неподвижная точка.

Неподвижная точка: \(X: FX = X\)

Доказательство:

Конструктивное.

Рассмотрим терм \(F(x\ x)\).

\(\lambda x.F(x\ x) = W\)

\(X = WW\) (неподвижная точка)

\(X = WW = (\lambda x.F(x\ x))W = F(W\ W) = F(X) = FX\)

Таким образом, с помощью \(\beta\) - редукции мы доказали, что терм является неподвижной точкой.

Теорема 2

Существует комбинатор неподвижной точки \(Y\)

\(\forall F: F(YF) = YF\)

Доказательство:

\(Y = \lambda f(\lambda x.f(x\ x) \lambda x.f(x\ x))\)

\(YF = \lambda x.F(x\ x) \lambda x.F(x\ x) = F(\lambda x.F(x\ x)\lambda x.F(x\ x)) = F(YF)\)

\(Y\) также называется парадоксальным комбинатором Карри.

Пример:

\(fact = \lambda n.(iszero\ n) 1 (mult\ n(fact (pre\ n)))\)
Перепишем в другом виде. Мы на самом деле можем применить обратную операцию операции \(\beta\) - редукции и вынести наш \(fact\) из терма:

\(fact = (\lambda fn.(iszero\ n) 1 (mult\ n (f(pre\ n)))) fact\)

Пусть \(fact' = ((\lambda fn.(iszero\ n) 1 (mult\ n (f(pre\ n))))\)

Соответственно \(fact\) - неподвижная точка для \(fact'\). Про неподвижную точку мы знаем то, что она получается с помощью комбинатора Карри: \(fact = Y\ fact'\)

Разложим факториал на примере:

\(fact\ 3 = (Y\ fact') 3 = fact' (Y\ fact') 3 = iszero(3) 1 (mult\ 3 ((Y fact')(pre\ 3))) = \)

\(mult\ 3 ((Y\ fact') 2) = mult\ 2 ((Y\ fact') 1)) = mult\ 3(mult\ 2(mult\ 1\ 1)) = 6\)