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

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

Тема лекции - \(\lambda\) - исчисление.

\(\lambda\) - нотация

\(\lambda\) - нотация - способ записи функции.

Примеры записи функции:

1) \(F(x,y) = x^2 + y\) - классическая нотация

2) \(F(x,y) = +*xxy\) - польская нотация

Алонзо Чёрч предложил следующую нотацию:

\(F \cong \lambda xy.x^2+y;\)

\(F \cong \lambda xy.+*xxy\)

\(\lambda\) - исчисление

\(\lambda\) - исчисление - формальная логическая система. То есть в \(\lambda\) - исчислении есть некоторый синтаксис, который позволяет описывать некоторые объекты. \(\lambda\) - исчисление лежит в основе функциональных языков программирования.

Синтаксис

1) Переменные: \(x_1 x_2 ...\)

2) Служебные символы: ( ) .

3) Лямбда - квантор: \(\lambda\)

С помощью этих символов мы можем определять \(\lambda\) - термы.

\(\lambda\) - термы

1) Переменная \(x_i\)

2) \(A, B\) - термы, тогда \((AB)\) - \(\lambda\)-терм

3) \(x\) - переменная, \(A\) - \(\lambda\) - терм \(\Rightarrow\) \(\lambda x.A - \lambda\) - терм

Семантика

\(\lambda x.A - A\), как функция от \(x (F(x) = A\))

\((AB)\) - функциональный терм, который обозначает подстановку в \(A B\) в качестве аргумента.

Пример

\(((\lambda x_1.x_1) x_2) \Rightarrow x_2\)

Соглашение

1) \(x_1 x_2 x_3\) = \((x_1 x_2)x_3\)

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

3) вместо \(x_i\) может быть любое слово (переменные можем называть так, как хотим)

Связные и свободные переменные

Существуют связные и свободные переменные. Переменные, которые следуют после \(\lambda\) - квантора - связные.

Пример

\(\lambda x.(x \lambda z.yz)\)

В данном случае связные переменные : \(x, z\), а свободный : \(y\)

Некорректно говорить, что \((\lambda x. \lambda x. x) y = y\)

На самом деле \((\lambda x. \lambda x. x) y = \lambda x.x\)

Нумералы Чёрча

\(N : \rightarrow nat\) (из пустого множества аргументов даёт нам натуральное число) - конструктор нуля

\(S : nat \rightarrow nat \) - конструктор + 1

Пример

\(3 = S(S(S(N)))\)

То же самое мы можем сказать для термов

Конструкторы термов

\(X : nat \rightarrow term | (x_i, i \in N_0)\)

\(A : term * term \rightarrow term | (AB)\)

\(L : nat * term \rightarrow term | (\lambda x.A)\)

Эти конструкторы нужны для того, чтобы формально определить множество свободных переменных.

Свободные переменные

Будем использовать функцию \(FV\) - free variable.

\(FV(x_n) \cong {X_n}\)

\(FV((t_1,t_2)) \cong FV(t_1) \cup FV(t_2) \)

\(FV(\lambda x_n t) \cong FV(t) / {x_n}\)

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

Подстановка

\(x/y \lambda z.xy = \lambda z.xx\)

Рекурсивное определение:

\([t/x_n]x_n \cong t\)

\([t/x_n]x_m \cong x_m (m \neq n)\)

\([t/x_n](t_1t_2) \cong ([t/x_n]t_1 [t/x_n]t_2)\)

\([t/x_n](\lambda x_n.t_1) = \lambda x_n.t_1\)

\([t/x_n](\lambda x_m.t_1) = \lambda x_m.[t/x_n]t_1 (m \neq n)\)

Над термами существуют 2 синтаксически важные операции - \(\alpha\) - конверсия и \(\beta\) - редукция

\(\alpha\) - конверсия

\(\alpha\) - конверсия - переименование связанной переменной, причем корректное.

\(\lambda x_n.t \rightarrow^\alpha \lambda x_m.[x_m/x_n]t\) \(x_m \notin FV(t)\)

Важно заметить, что

\(\lambda x_m.[x_m/x_n]t \rightarrow^\alpha \lambda x_n.[x_n/x_m][x_m/x_n]t\)

Таким образом, \(\alpha\) - конверсия - симметричная операция.

Примеры

1) \(\lambda x.xy \rightarrow^\alpha \lambda z.zy\)

2) \(\lambda x.xy \rightarrow^\alpha \lambda y.yy\) - так переименовать нельзя, так как \(y\) - свободная переменная

\(\beta\) - редукция

\(\beta\) - редукция описывает как мы наши функциональные термы используем.

\(\lambda x_n.t't \rightarrow ^\beta [t/x_n]t'\) (левая часть именуется как (\(\beta\) - редекс, правая - \(\beta\) - контракт)).

Пример

\((\lambda x.xx)(\lambda z.z) \rightarrow ^\beta [\lambda z.z/x]\lambda x.xx = (\lambda z.z)(\lambda z.z)\) (то есть теперь наша связная переменная приобрела некоторое значение, мы в функцию подставили аргумент, аргумент - второй терм в нашей конкатенации(функциональном терме))

\(\beta\) - нормальная форма

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

Пример

\((\lambda xy.(x+y)z)z \rightarrow ^\beta (\lambda y.(z+y))z \rightarrow ^\beta z+z\) (таким образом, мы нашли \(\beta\) - нормальную форму, выполнив все \(\beta\) - редукции, которые возможны)

Термы без нормальной формы:

\((\lambda x.xx)(\lambda x.xx) \rightarrow ^\beta [\lambda x.xx/x]\lambda x.xx = (\lambda x.xx)(\lambda x.xx)\)

Некорректное применение:

\((\lambda xy.xyz)y \rightarrow ^ \beta (\lambda y.yyz)\) (так делать нельзя!!!)

Но выход есть:

\((\lambda xy.xyz)y \rightarrow ^\alpha (\lambda xk.xkz)y \rightarrow ^\beta \lambda k.ykz\)

\(\lambda\) - контекст

◻ - "дырка"

\(\lambda x.◻\)

1) ◻

2) t◻ ,◻t

3) \(\lambda x.◻\)

Конструкторы:

\(H : \rightarrow context\) | ◻

\(A' : context * term \rightarrow context\)

\(A\)''\( : term * context \rightarrow context\)

\(L : nat * context \rightarrow context\) (таким образом мы получаем связывание переменной)

Примеры

\(L(1, ◻) = \lambda x_1.◻\)

\(\lambda x_1. \lambda x_2. (x_1 + x_2)*◻\)

Деструкторы

\(k\) - контекст, \(t\) - терм, то \(k[t] = [t/◻]k\)

\(k'\) - контекст, \(t\) - терм, то \(k[t] = [k'/◻]k\)

Вхождение

Вхождение терма \(t_1\) в \(t\) - это пара \(<t_1,k> : k[t_1] = t\)

Отношение редукции

Обозначение : =>

Отношение редукции - это минимальное отношение, которое удовлетворяет следующим условиям:

  1. t => t
  2. \(t_1 \rightarrow ^ \alpha t_2 \supset t_1 => t_2\)
  3. \(t_1 \rightarrow ^ \beta t_2 \supset t_1 => t_2\)
  4. \(t_1 => t_2 \cap t_2 => t_3 \supset t_1 => t_3\)
  5. \(t_1 => t_2 \supset k[t_1] => k[t_2]\)

Процесс редукции t' к t''

Процесс редукции - последовательность термов \(t_1, ..., t_l, l \geq 1\)

  1. \(t' = t_1\)
  2. \(t\)''\( = t_l\)
  3. \(\forall i \in 1 .. l-1 \exists \tau_{i}'\) и \(\tau_{i}\)'' - термы и \(\exists k_i\) - контекст или \(\tau_{i}' \rightarrow ^ \alpha \tau_{i}\)'' или \(\tau_{i}' \rightarrow ^ \beta \tau_{i}\)'' и \(k[\tau_{i}'] = t_i\), и \(k[\tau_{i}\)''\(] = t_{i+1}\)

Пример

\(\lambda x.xy \rightarrow ^ \beta y\)

\(\tau_{1}' = \lambda x.xy\)

\(\tau_{1}\)''\( = y\)

\(k = ◻\)

\(k[\tau_{i}'] = \lambda x.xy\)

\(k[\tau_{i}\)''\(] = y\)

Если терм имеет \(\beta\) - нормальную форму, то он получается в процессе стандартной редукции.

Конфлюэнтность отношения

\(\forall t', t_1, t_2 \in T\), если \([t' \rightarrow t_1 \cap t' \rightarrow t_2 \supset (\exists t\)''\(\in T)\) \(t_1 \rightarrow t\)''\(\cap t_2 \rightarrow t\)''\()]\)

Теорема Чёрча - Россера

Отношение редукции (=>) конфлюэнтно.

Следствие 1

Если \(M,N,K,P\) - термы и \(M => N, N => P\), а \(P\) - в нормальной форме, тогда \(K => P\)

Следствие 2

Нормальная форма - единственная.