Редактирование: Парадигмы программирования, 06 лекция (от 29 октября)

Материал из eSyr's wiki.

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

"На эту тему мне понравилась татуировка с Y-combinator"

лямбда-исчисления.

На самом деле, л-исчисл. имеют не совсем прямое. л-исчисл. было придумано Чёрчем задолго до программирования.

Похоже на то, что любую функцию, которая за конечное время даёт рез-т от конечного числа аргументов, записать можно. Также для неё можно сделать МТ, и т. д.

Л-вычисл это мат. абстр., некий формализм, прямого отн. к прогр. не имеющ.

Есть легенда, что еогда МакКарти писал лисп, он вдохновился л-исчисл, и лисп писался как реализ. л-исчисл. Это не так, хотя впоследствии лямбда туда была добавлена.

Как в л-исчисл запис. функция:

lambda x . и дальше выражение, задающее функцию. Как оно задётся, бывают разные способы. Обычно исп. польскую нотацию

lambda x . * 3 x

как это прочитать: 
* lambda — "функция от"
* . — которая возвращает

Большинство авторов рассм. ф-цию от одного параметра, но мощности это не уменьшает. Да, некоторые авторы пишут

lambda x y z . + x * y z

Но большинство всё же пишут

lambda x . lambda y . lambda z . + x * y z

Такая конструкция наз. лямбда-абстр, то, что после точки — телом. Как видно, в теле может содержаться произв. л-выр., в том числе лямбда.

Если мы видем два лямбда-выр., E_1 E_2, то это обычно значит, что первое выр. — функция, а второе, знач, к котторому его нужно применить.

Чисто синтаксически, функцию всегда применяют к самому левому арг., то есть, если есть такая запись:

(...((lambda x_1 . lambda x_2 . ... lambda x_n . E) a_1) a_2) ...) a_n

То есть соглащ., что такое выр. можно записать неск. короче:

(lambda x_1 . lamda x_2 . ... lambda x_n . E) a_1 a_2 ... a_n

Более формально можно записать в виде БНФ:

<exp> ::= lambda <id> . <exp> | <id> | <exp> <exp> | (<exp>) | <const>
 <id> ::= идентификатор (какие могут быть идент --- зависит от того, какой стиль приняли)
 <const> ::= константы

Константы заслуживают более внимательного рассмотрения. Конст. могут обозначать:
# Числа. Числа могут быть как целые, так и веществ. В больш. случае, когда рассм. л-выч., обычно до вещ. чисел не доходят.
# Булевы значения: Истина и Ложь. Как конкр. их обозначить, это тоже вопрос философский.
# [ Строки ]. Далеко не все авторы про них вспоминают
# Пустой список. Обычно его обозн. <>, хотя можно обозн. как угодно.
# Функции
## * . + - ....
## Знаки отношений: < > = != >= ...
## Функции работы со списками: CONS, HEAD, TAIL, NULL (предикат, проверка на пустой список)
## Иногда некоторые авторы, в частн., Филд, Харрисон, считают необх. ввод кортежей. TUPLE-n, INDEX
## COND
## '''...'''

Вообще, можно делать лямбда-выч. без констант, сконстр. из из первич. понятий, но это к прогр. мало отношения имеет. Без них тяжело. Сначала вводятся списки, потом числа как списки разной длины, а чтобы ввести умножение, нужно неск. страниц исписать.

Примеры лямбда-выражений. Самое простое — просто константа.

42
 (+ 6) ; функция, которая прибавляет 6
 lambda y . * 2 y ; лямбда-абстракция

В многоточие жироне входит в том числе cond. Он аналогичн лисповскому if. Похоже на сишную тернарную операцию.

(lambda f . lmbda a lambda b . f a b) (lambda x . (lambda y . x))

Вернёт a ((lambda x . (lambda y . x)) как ф-ция от двух. арг подст. в f, и сама по себе возвр. первый арг.).

lambda f . lambda x . COND (= x 1) x (* x (f (- x 1)))

Имеет отн. к вычислению факториала. Вообще, без имён функций тяжело, дальше мы посмотрим, как это решить.

Как л-выр. вычисл. Т. н. правила редукции.
* Константы редуц. в себя
* Функция и арг. Применяется дельта-правило. Например: + 1 2 ->_delta 3. Из этого выр. по дельта-правилу, или, применив дельта-редукцию, получаем 3. Понятно, что дельта-правила есть для каждой функции. Например, у нас есть выр.
 * (+ 1 2) (- 4 1) ->_delta * (+ 1 2) 3 ->_delta * 3 3 ->_delta 9
* Применение ф-ции, напис. через лямбда-абстракцию. Заменяем чисто текстуально, результат замены --- рез-т выражения:
 (lambda x . * x x) 2 ->_beta * 2 2  ->_delta 4
 (lambda x . + x x) (* (+ 2 3) 4) ->_beta + (* (+ 2 3) 4) (* (+ 2 3) 4)
: Текстуально оно становится длиннее, но мы избавляемся от символа лямбда.
 (lambda x . lambda y . + x y) 7 8 ->_beta (lambda y . + 7 y) 8 ->_beta + 7 8 ->_delta 15

Редуцируемая часть. выр наз. редексом (redex, reducible expression)

Если редаксов в выр. нет, тогда говорят, что выр. имеет норм. форму.

Имеется некий подводный камень, связанный с одноим. символами. Рассмотрим выражение:

lambda x . (lambda x . x) (+ 1 x)

В чём здесь неприятность? Очевидно, что

lambda x_2 . (lambda lambda x_1 . x_1) (+ 1 x_1)

Если взять это в скобки и где-то применить, то понятно, что получится не то, что хотели. Получается конфликт имён. Как это разрешить? Например, постановить, что если мы подобные вещи применяем к чему-то, то внутри ничего не трогать.

Есть второй вариант, т. н. альфа-преобразовнаие. Оно не наз. редукцие, поск. оно ничего не упрощ., оно переименовывает пременную.

Если не учитывать контекст имён, то что получится:

(lambda x . (lambda x . x) (+ 1 x)) 3 -> (lambda x . 3) (+ 1 3) -> 7
 (lambda x . (lambda y . y) (+ 1 x)) 3 -> (lambda y . y) (+ 1 3) -> ... -> 8

То есть вот, конфликты имён бывают, конфликты имён ращреш. альфа-преобр, это не совсем ред., хотя записывается также:

lambda x. x ->_alpha lambda y . y

Порядок выбор редексов для редукции. В л-выр может быть неск. редексов, и вопрос, с какого начать? Вопрос интересный и весьма принципиальный. Рассмотрим пример:

(lambda f . lambda x . f 4 x) (lambda y . lambda x . + x y) 3 ->
  --------                      ---------------------------
  ----------------------------------------------------------
 (lambda x . (lambda y . lambda x + x y) 4 x) 3 ->
                                      ---- ---- 
на самом деле, тут в обоих случаях получится одно и то же
 1. (lambda y . lambda x + x y) 4 3 -> (lambda x . + x 4) 3 -> + 3 4 -> 7
 2. (lambda x . (lambda x . + x 4) x) 3 -> (lambda x . + x 4) 3 -> + 3 4 -> 7

В принципе, до какой-то степени так и должно быть, но есть теорема Чёрча-Россера, которая гласит, что если у лямбда-выр. есть норм. форма, то она только одна (если неск., то они эквив. с точностью до алф. преобр.). Из этого следует, что она аже достигается. Но выбрав нехороший порядок редукции, то можно не прийти к норм. форме вообще. Есть классич. пример, когда один порядок не приводит к норм. форме вооббще никогда, другой же за один шаг.

(lambda x . lambda y . y) ((lambda z . z z) (lambda z . z. z))

Здесь есть два варианта:

(lambda x . lambda y . y) ((lambda z . z z) (lambda z . z. z))
         -                 ------------------------------------
тогда мы достигаем результат за один шаг:
 lambda y . y

но есть и второй редекс:

(lambda x . lambda y . y) ((lambda z . z z) (lambda z . z. z))
                            ----------------------------------
но он при применении даст сам себя:
 (lambda x . lambda y . y) ((lambda z . z z) (lambda z . z. z))

Вопрос, какой же редекс тогда надо выбирать и зачем? Введём неск. определений.
 * Самый левый редекс --- его лямбда или имя примитивной функции находятся текстуально левее всех остальных.
 * Самый внешний редекс --- тот, который текстуально не содерж. ни в каком другом.
 * Самый внутренний --- тот, который в котором не содерж. никакой другой.

Есть два порядка?
 * Аппликативный --- выбирается самый левый внутренний.
 * Нормальный --- берём все самые внешние, выбираем из них самый левый, и его используем.

Здесь мы сначла применили сначала нормальный, потом аппликативный. Теперь можно уточнить:

Следствие из теор. Чёрча-Россера. нормальный порядок редукции приводит к норм. форме за конеч. число шагов, если она вообще есть.

Теперь самое интересное. Если отвлечься от л-выр. и вернуться к прогр., то можно вспомнить, что есть энергинча и ленивая стратегия вычисл. При энерг. мы выч. всё, что только можем. При ленивых выч. мы при виде выр. мы запоминаем его и не вычисляем, пока можно, до тех пор, пока не припрёт. Например:
 (   ) > 3
Вот тут нам надо вычислить знач. выр., не раньше. Бывает ли такое в языках прогр.? Бывает, но очень редко и по-немногу. Ленивая семантика из компилир. языков --- только хаскель, но все привычные, императивные --- энергичные.

Где можно встретить ленивую модель вычислений? Например, при подст. макросов. Макропроцессору это просто, поск. он работает на уровне текстовых строк. В некоторых командно-скриптовых языках ленивая семантика имеется.

Но сейчас, когда мы смотрим на л-выч., мы видим, что ленивый порядок вычисл. оказался в каком-то виде мощнее.

Введём такую вещб, как понятие связанных и свободных переменных

lambda x . x y

Понятно, что x связ., а y --- вободная. Если чуть строже, то построим мн-во FV(E) (free variables(expression)). Как оно вводится:
* FV(x) = {x}
* FV(c) = &empty;
* FV(E_1, E_2) = FV(E_1) &cup; FV(e_2)
* FV(lambda x  . E_1) = FV(E_1) \ {x}

Аналогично можно ввести мн-во Bound variables, BV(E):
* BV(x) = &empty;
* BV(c) = &empty;
* BV(E_1, E_2) = BV(E_1) &cup; BV(e_2) ; отсюда следует, что прееменная может быт ьи свободная, и связана, но свободна в одной части, а связана в другой
* BV(lambda x  . E_1) = BV(E_1) &cup; {x}

Выражение, в котором нет связ. переменных, наз. замкнутым. Замкнутыми выр. ещё наз. комбинаторами.

Если x &notin; FV(E), то можно вести речь об &etta;-преобразовании.

Можно заметить, что lambda x . E x есть то же самое, что E. Попробуем и то, и другое к a:
 E a
 (lambda x . E x) a ->_beta E a

Главное, чтобы в E не было свободной переменной x, иначе ничего не выйдет. Соотв, делаем это преобр.:

E ->_etta lambda x. E x

Что оно позв. делать? Например, част. применение встроенных функций. Например, если есть * x y. Является ли * 3 л-выр? Да. А как же с ним работать. Применим &etta;-преобр, получим lambda x . * 3 x. Благодаря этому мы можем делать частичное применение функций.

... это называется карринг, по имени учёного Карри (Curry).

Наконец, последнее на сегодня, что же такое Y-combinator. Хочется нам, к примеру, сделать рек. функцию, но как, здесь же нет имён? Мы эту фнкцию получим в кач. второго аргумента. То есть функция получает на фход аргмент и самого себя, и исхитримся и подадим её на вход.

Рассмотрим более идиотический пример --- сумма от 1 до n.

Лектор напишет её сначала на лиспе:

(setq f #'(lambda (s x) (if (= x 0) 0 (+ x (funcall s s (- x 1))))))

Что теперь сделать? Нао её вызвать, подав ей на вход число и её саму. Как это сделать?

(funcall f f 5) => 15

можно то же самое сделать и на лямбда-абстракциях

lambda s . lambda x . COND (= x 0) 0 (+ x (s (- x 1)))

Сущ. неподв. точка, т. е. f(x) = x, и она есть для кажого лямбда-выр.

Есть Y-combinator, который делает:

Y f = f(Y f)

Как выглядит Y-combinator:

Y = lambda h . (lambda x . h (x x)) (lambda x . h (x x))

теперь осталось что?

Y lambda s . lambda x . COND (= x 0) 0 (+ x (s (- x 1)))

И отредуцировать. Результатом будет функция, от одного арг., выч. сумму.

y-comb. используется в haskell.

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.us/wiki/%D0%9F%D0%B0%D1%80%D0%B0%D0%B4%D0%B8%D0%B3%D0%BC%D1%8B_%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D1%8F%2C_06_%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F_%28%D0%BE%D1%82_29_%D0%BE%D0%BA%D1%82%D1%8F%D0%B1%D1%80%D1%8F%29

Редактирование: Парадигмы программирования, 06 лекция (от 29 октября)

Материал из eSyr's wiki.

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 1: / Строка 1: @@
-[[Image:paradigm_091029_01.jpg|thumb|right|300px|«На эту тему мне понравилась [http://theartoftattoo.files.wordpress.com/2009/04/y-combinator.jpg татуировка с Y-combinator»]]]
+"На эту тему мне понравилась татуировка с Y-combinator"
-* '''Аудиозапись:''' http://esyr.org/lections/audio/paradigms_2009_winter/paradigms_09_10_29.ogg
-= лямбда-исчисления =
+лямбда-исчисления.
-Лямбда-исчисление было придумано Чёрчем задолго до программирования.
+На самом деле, л-исчисл. имеют не совсем прямое. л-исчисл. было придумано Чёрчем задолго до программирования.
-Похоже на то, что любую функцию, которая за конечное время даёт результат от конечного числа аргументов, записать можно. Также для неё можно сделать МТ, и т. д.
+Похоже на то, что любую функцию, которая за конечное время даёт рез-т от конечного числа аргументов, записать можно. Также для неё можно сделать МТ, и т. д.
-Лямбда-вычисления это математическая абстракция, некий формализм, прямого отношения к программированию не имеющая
+Л-вычисл это мат. абстр., некий формализм, прямого отн. к прогр. не имеющ.
-Есть легенда, что когда МакКарти писал лисп, он вдохновился л-исчислением, и лисп писался как его реализация. Это не так, хотя впоследствии лямбда туда была добавлена.
+Есть легенда, что еогда МакКарти писал лисп, он вдохновился л-исчисл, и лисп писался как реализ. л-исчисл. Это не так, хотя впоследствии лямбда туда была добавлена.
-Как в л-исчислислении записывается функция:
+Как в л-исчисл запис. функция:
-&lambda; x . и дальше выражение, задающее функцию. Есть разные способы, обычно используют польскую нотацию
+lambda x . и дальше выражение, задающее функцию. Как оно задётся, бывают разные способы. Обычно исп. польскую нотацию
- &lambda; x . * 3 x
+ lambda x . * 3 x
 как это прочитать:
-* &lambda; — "функция от"
+* lambda — "функция от"
 * . — которая возвращает
-Большинство авторов рассматривают ф-цию от одного параметра, но мощности это не уменьшает. Да, некоторые авторы пишут
+Большинство авторов рассм. ф-цию от одного параметра, но мощности это не уменьшает. Да, некоторые авторы пишут
- &lambda; x y z . + x * y z
+ lambda x y z . + x * y z
 Но большинство всё же пишут
- &lambda; x . &lambda; y . &lambda; z . + x * y z
+ lambda x . lambda y . lambda z . + x * y z
-Такая конструкция называется лямбда-абстракцией, то, что после точки — телом. Как видно, в теле может содержаться произвольное л-выражение, в том числе лямбда.
+Такая конструкция наз. лямбда-абстр, то, что после точки — телом. Как видно, в теле может содержаться произв. л-выр., в том числе лямбда.
-Если мы видим два лямбда-выражения, E_1 E_2, то это обычно значит, что первое выр. — функция,второе -
+Если мы видем два лямбда-выр., E_1 E_2, то это обычно значит, что первое выр. — функция, а второе, знач, к котторому его нужно применить.
-знач, к которому ее нужно применить.
-Чисто синтаксически, функцию всегда применяют к самому левому аргументу. Если есть такая запись:
+Чисто синтаксически, функцию всегда применяют к самому левому арг., то есть, если есть такая запись:
- (...((&lambda; x_1 . &lambda; x_2 . ... &lambda; x_n . E) a_1) a_2) ...) a_n
+ (...((lambda x_1 . lambda x_2 . ... lambda x_n . E) a_1) a_2) ...) a_n
-...то есть соглашение, что такое выражение можно записать несколько короче:
+То есть соглащ., что такое выр. можно записать неск. короче:
- (&lambda; x_1 . lamda x_2 . ... &lambda; x_n . E) a_1 a_2 ... a_n
+ (lambda x_1 . lamda x_2 . ... lambda x_n . E) a_1 a_2 ... a_n
 Более формально можно записать в виде БНФ:
- <exp> ::= &lambda; <id> . <exp> | <id> | <exp> <exp> | (<exp>) | <const>
+ <exp> ::= lambda <id> . <exp> | <id> | <exp> <exp> | (<exp>) | <const>
- <id> ::= идентификатор (какие могут быть идентификаторы --- зависит от того, какой стиль приняли)
+ <id> ::= идентификатор (какие могут быть идент --- зависит от того, какой стиль приняли)
  <const> ::= константы
-Константы заслуживают более внимательного рассмотрения. Они могут обозначать:
+Константы заслуживают более внимательного рассмотрения. Конст. могут обозначать:
-# Числа. Числа могут быть как целые, так и веществ. Когда рассматривают л-вычисления, обычно до веществ. чисел не доходят.
+# Числа. Числа могут быть как целые, так и веществ. В больш. случае, когда рассм. л-выч., обычно до вещ. чисел не доходят.
-# Булевы значения: Истина и Ложь. Как конкретно их обозначить, это тоже вопрос философский.
+# Булевы значения: Истина и Ложь. Как конкр. их обозначить, это тоже вопрос философский.
 # [ Строки ]. Далеко не все авторы про них вспоминают
 # Пустой список. Обычно его обозн. <>, хотя можно обозн. как угодно.
@@ Строка 58: / Строка 56: @@
 ## Знаки отношений: < > = != >= ...
 ## Функции работы со списками: CONS, HEAD, TAIL, NULL (предикат, проверка на пустой список)
-## Иногда некоторые авторы, в частности, Филд и Харрисон, считают необходимым ввод кортежей. TUPLE-n, INDEX
+## Иногда некоторые авторы, в частн., Филд, Харрисон, считают необх. ввод кортежей. TUPLE-n, INDEX
 ## COND
 ## '''...'''
-Вообще, можно делать лямбда-вычисления без констант, сконстр. их из первич. понятий, но это к прогр. мало отношения имеет. Без них тяжело. Сначала вводятся списки, потом числа как списки разной длины, а чтобы ввести умножение, нужно несколько страниц исписать.
+Вообще, можно делать лямбда-выч. без констант, сконстр. из из первич. понятий, но это к прогр. мало отношения имеет. Без них тяжело. Сначала вводятся списки, потом числа как списки разной длины, а чтобы ввести умножение, нужно неск. страниц исписать.
 Примеры лямбда-выражений. Самое простое — просто константа.
@@ Строка 68: / Строка 66: @@
  (+ 6) ; функция, которая прибавляет 6
- &lambda; y . * 2 y ; лямбда-абстракция
+ lambda y . * 2 y ; лямбда-абстракция
-В многоточие входит в том числе cond. Он аналогичен лисповскому if. Похоже на сишную тернарную операцию.
+В многоточие жироне входит в том числе cond. Он аналогичн лисповскому if. Похоже на сишную тернарную операцию.
- (&lambda; f . lmbda a &lambda; b . f a b) (&lambda; x . (&lambda; y . x))
+ (lambda f . lmbda a lambda b . f a b) (lambda x . (lambda y . x))
-Вернёт a ((&lambda; x . (&lambda; y . x)) как ф-ция от двух. арг подст. в f, и сама по себе возвращает первый арг.).
+Вернёт a ((lambda x . (lambda y . x)) как ф-ция от двух. арг подст. в f, и сама по себе возвр. первый арг.).
- &lambda; f . &lambda; x . COND (= x 1) x (* x (f (- x 1)))
+ lambda f . lambda x . COND (= x 1) x (* x (f (- x 1)))
-Имеет отношение к вычислению факториала. Вообще, без имён функций тяжело, дальше мы посмотрим, как это решить.
+Имеет отн. к вычислению факториала. Вообще, без имён функций тяжело, дальше мы посмотрим, как это решить.
-Как л-выр. вычисл. Т.н. правила редукции.
+Как л-выр. вычисл. Т. н. правила редукции.
-* Константы редуцуются в себя
+* Константы редуц. в себя
-* Функция и арг. Применяется дельта-правило. Например: + 1 2 &rarr;<sub>&delta;</sub> 3. Из этого выр. по дельта-правилу, или, применив дельта-редукцию, получаем 3. Понятно, что дельта-правила есть для каждой функции. Например, у нас есть выр.
+* Функция и арг. Применяется дельта-правило. Например: + 1 2 ->_delta 3. Из этого выр. по дельта-правилу, или, применив дельта-редукцию, получаем 3. Понятно, что дельта-правила есть для каждой функции. Например, у нас есть выр.
- * (+ 1 2) (- 4 1) &rarr;<sub>&delta;</sub> * (+ 1 2) 3 &rarr;<sub>&delta;</sub> * 3 3 &rarr;<sub>&delta;</sub> 9
+ * (+ 1 2) (- 4 1) ->_delta * (+ 1 2) 3 ->_delta * 3 3 ->_delta 9
-* Применение ф-ции, написанной через лямбда-абстракцию. Заменяем чисто текстуально, результат замены --- результат выражения:
+* Применение ф-ции, напис. через лямбда-абстракцию. Заменяем чисто текстуально, результат замены --- рез-т выражения:
- (&lambda; x . * x x) 2 &rarr;<sub>&beta;</sub> * 2 2  &rarr;<sub>&delta;</sub> 4
+ (lambda x . * x x) 2 ->_beta * 2 2  ->_delta 4
- (&lambda; x . + x x) (* (+ 2 3) 4) &rarr;<sub>&beta;</sub> + (* (+ 2 3) 4) (* (+ 2 3) 4)
+ (lambda x . + x x) (* (+ 2 3) 4) ->_beta + (* (+ 2 3) 4) (* (+ 2 3) 4)
 : Текстуально оно становится длиннее, но мы избавляемся от символа лямбда.
- (&lambda; x . &lambda; y . + x y) 7 8 &rarr;<sub>&beta;</sub> (&lambda; y . + 7 y) 8 &rarr;<sub>&beta;</sub> + 7 8 &rarr;<sub>&delta;</sub> 15
+ (lambda x . lambda y . + x y) 7 8 ->_beta (lambda y . + 7 y) 8 ->_beta + 7 8 ->_delta 15
-Редуцируемая часть выражения  называется редексом (redex, reducible expression)
+Редуцируемая часть. выр наз. редексом (redex, reducible expression)
-Если редексов в выражении нет, тогда говорят, что выражение имеет норм. форму.
+Если редаксов в выр. нет, тогда говорят, что выр. имеет норм. форму.
-Имеется некий подводный камень, связанный с одноименными символами. Рассмотрим выражение:
+Имеется некий подводный камень, связанный с одноим. символами. Рассмотрим выражение:
- &lambda; x . (&lambda; x . x) (+ 1 x)
+ lambda x . (lambda x . x) (+ 1 x)
 В чём здесь неприятность? Очевидно, что
- &lambda; x_2 . (&lambda; &lambda; x_1 . x_1) (+ 1 x_1)
+ lambda x_2 . (lambda lambda x_1 . x_1) (+ 1 x_1)
 Если взять это в скобки и где-то применить, то понятно, что получится не то, что хотели. Получается конфликт имён. Как это разрешить? Например, постановить, что если мы подобные вещи применяем к чему-то, то внутри ничего не трогать.
-Есть второй вариант, т.н. альфа-преобразование. Оно не называется редукцией, поскольку ничего не упрощает, оно переименовывает перемененную.
+Есть второй вариант, т. н. альфа-преобразовнаие. Оно не наз. редукцие, поск. оно ничего не упрощ., оно переименовывает пременную.
 Если не учитывать контекст имён, то что получится:
- (&lambda; x . (&lambda; x . x) (+ 1 x)) 3 -> (&lambda; x . 3) (+ 1 3) -> 7
+ (lambda x . (lambda x . x) (+ 1 x)) 3 -> (lambda x . 3) (+ 1 3) -> 7
- (&lambda; x . (&lambda; y . y) (+ 1 x)) 3 -> (&lambda; y . y) (+ 1 3) -> ... -> 8
+ (lambda x . (lambda y . y) (+ 1 x)) 3 -> (lambda y . y) (+ 1 3) -> ... -> 8
-То есть вот, конфликты имён бывают, конфликты имён разрешает альфа-преобразование, это не совсем редекс, хотя записывается также:
+То есть вот, конфликты имён бывают, конфликты имён ращреш. альфа-преобр, это не совсем ред., хотя записывается также:
- &lambda; x. x &rarr;<sub>&alpha;</sub> &lambda; y . y
+ lambda x. x ->_alpha lambda y . y
-Порядок выбора редексов для редукции. В л-выр может быть несколько редексов, и вопрос, с какого начать? Вопрос интересный и весьма принципиальный. Рассмотрим пример:
+Порядок выбор редексов для редукции. В л-выр может быть неск. редексов, и вопрос, с какого начать? Вопрос интересный и весьма принципиальный. Рассмотрим пример:
- (&lambda; f . &lambda; x . f 4 x) (&lambda; y . &lambda; x . + x y) 3 ->
+ (lambda f . lambda x . f 4 x) (lambda y . lambda x . + x y) 3 ->
   --------                      ---------------------------
   ----------------------------------------------------------
- (&lambda; x . (&lambda; y . &lambda; x + x y) 4 x) 3 ->
+ (lambda x . (lambda y . lambda x + x y) 4 x) 3 ->
                                       ---- ----
 на самом деле, тут в обоих случаях получится одно и то же
-. (&lambda; y . &lambda; x + x y) 4 3 -> (&lambda; x . + x 4) 3 -> + 3 4 -> 7
+. (lambda y . lambda x + x y) 4 3 -> (lambda x . + x 4) 3 -> + 3 4 -> 7
-. (&lambda; x . (&lambda; x . + x 4) x) 3 -> (&lambda; x . + x 4) 3 -> + 3 4 -> 7
+. (lambda x . (lambda x . + x 4) x) 3 -> (lambda x . + x 4) 3 -> + 3 4 -> 7
-Теорема Чёрча-Россера: если у лямбда-выражения есть нормальная форма, то она единственна (если несколько, то они эквивалентны с точностью до альфа-преобразования).
+В принципе, до какой-то степени так и должно быть, но есть теорема Чёрча-Россера, которая гласит, что если у лямбда-выр. есть норм. форма, то она только одна (если неск., то они эквив. с точностью до алф. преобр.). Из этого следует, что она аже достигается. Но выбрав нехороший порядок редукции, то можно не прийти к норм. форме вообще. Есть классич. пример, когда один порядок не приводит к норм. форме вооббще никогда, другой же за один шаг.
-Из этого следует, что она даже достигается. Но выбрав нехороший порядок редукции, можно не прийти к норм. форме вообще. Есть классический пример, когда один порядок не приводит к норм. форме вообще никогда,
+ (lambda x . lambda y . y) ((lambda z . z z) (lambda z . z. z))
-другой же за один шаг.
- (&lambda; x . &lambda; y . y) ((&lambda; z . z z) (&lambda; z . z. z))
 Здесь есть два варианта:
- (&lambda; x . &lambda; y . y) ((&lambda; z . z z) (&lambda; z . z. z))
+ (lambda x . lambda y . y) ((lambda z . z z) (lambda z . z. z))
          -                 ------------------------------------
 тогда мы достигаем результат за один шаг:
- &lambda; y . y
+ lambda y . y
 но есть и второй редекс:
- (&lambda; x . &lambda; y . y) ((&lambda; z . z z) (&lambda; z . z. z))
+ (lambda x . lambda y . y) ((lambda z . z z) (lambda z . z. z))
                             ----------------------------------
 но он при применении даст сам себя:
- (&lambda; x . &lambda; y . y) ((&lambda; z . z z) (&lambda; z . z. z))
+ (lambda x . lambda y . y) ((lambda z . z z) (lambda z . z. z))
-Вопрос, какой же редекс тогда надо выбирать и зачем? Введём несколько определений.
+Вопрос, какой же редекс тогда надо выбирать и зачем? Введём неск. определений.
  * Самый левый редекс --- его лямбда или имя примитивной функции находятся текстуально левее всех остальных.
- * Самый внешний редекс --- тот, который текстуально не содержится ни в каком другом.
+ * Самый внешний редекс --- тот, который текстуально не содерж. ни в каком другом.
- * Самый внутренний --- тот, в котором не содержится никакой другой.
+ * Самый внутренний --- тот, который в котором не содерж. никакой другой.
 Есть два порядка?
  * Аппликативный --- выбирается самый левый внутренний.
- * Нормальный --- из всех самых внешних, выбираем самый левый.
+ * Нормальный --- берём все самые внешние, выбираем из них самый левый, и его используем.
-Здесь мы сначала применили сначала нормальный, потом аппликативный. Теперь можно уточнить:
+Здесь мы сначла применили сначала нормальный, потом аппликативный. Теперь можно уточнить:
-Следствие из теор. Чёрча-Россера. нормальный порядок редукции приводит к нормальной
+Следствие из теор. Чёрча-Россера. нормальный порядок редукции приводит к норм. форме за конеч. число шагов, если она вообще есть.
-форме за конечное число шагов, если она вообще есть.
-Теперь самое интересное. Если отвлечься от л-выражений и вернуться к программированию, то можно вспомнить, что есть энергичная и ленивая стратегия вычислений При энергичной мы вычисляем всё, что только можем. При ленивых вычислениях увидев выражение мы запоминаем его и не вычисляем до тех пор, пока не припрёт. Например:
+Теперь самое интересное. Если отвлечься от л-выр. и вернуться к прогр., то можно вспомнить, что есть энергинча и ленивая стратегия вычисл. При энерг. мы выч. всё, что только можем. При ленивых выч. мы при виде выр. мы запоминаем его и не вычисляем, пока можно, до тех пор, пока не припрёт. Например:
  (   ) > 3
-Вот тут нам действительно надо вычислить значение выражение, не раньше. Бывает ли такое в языках программирования? Бывает, но очень редко. Ленивая семантика из компилир. языков --- только haskell, но все привычные, императивные --- энергичные.
+Вот тут нам надо вычислить знач. выр., не раньше. Бывает ли такое в языках прогр.? Бывает, но очень редко и по-немногу. Ленивая семантика из компилир. языков --- только хаскель, но все привычные, императивные --- энергичные.
-Где можно встретить ленивую модель вычислений? Например, при подстановке макросов. Макропроцессору это просто, поскольку он работает на уровне текстовых строк. В некоторых командно-скриптовых языках ленивая семантика имеется.
+Где можно встретить ленивую модель вычислений? Например, при подст. макросов. Макропроцессору это просто, поск. он работает на уровне текстовых строк. В некоторых командно-скриптовых языках ленивая семантика имеется.
 Но сейчас, когда мы смотрим на л-выч., мы видим, что ленивый порядок вычисл. оказался в каком-то виде мощнее.
-Введём такую вещь, как понятие связанных и свободных переменных
+Введём такую вещб, как понятие связанных и свободных переменных
- &lambda; x . x y
+ lambda x . x y
-Понятно, что x связанная, а y --- свободная. Если чуть строже, то построим мн-во FV(E) (free variables(expression)). Как оно вводится:
+Понятно, что x связ., а y --- вободная. Если чуть строже, то построим мн-во FV(E) (free variables(expression)). Как оно вводится:
 * FV(x) = {x}
 * FV(c) = &empty;
 * FV(E_1, E_2) = FV(E_1) &cup; FV(e_2)
-* FV(&lambda; x  . E_1) = FV(E_1) \ {x}
+* FV(lambda x  . E_1) = FV(E_1) \ {x}
 Аналогично можно ввести мн-во Bound variables, BV(E):
@@ Строка 183: / Строка 177: @@
 * BV(c) = &empty;
 * BV(E_1, E_2) = BV(E_1) &cup; BV(e_2) ; отсюда следует, что прееменная может быт ьи свободная, и связана, но свободна в одной части, а связана в другой
-* BV(&lambda; x  . E_1) = BV(E_1) &cup; {x}
+* BV(lambda x  . E_1) = BV(E_1) &cup; {x}
 Выражение, в котором нет связ. переменных, наз. замкнутым. Замкнутыми выр. ещё наз. комбинаторами.
-Если x &notin; FV(E), то можно вести речь об &eta;-преобразовании.
+Если x &notin; FV(E), то можно вести речь об &etta;-преобразовании.
-Можно заметить, что &lambda; x . E x есть то же самое, что E. Попробуем и то, и другое к a:
+Можно заметить, что lambda x . E x есть то же самое, что E. Попробуем и то, и другое к a:
  E a
- (&lambda; x . E x) a &rarr;<sub>&beta;</sub> E a
+ (lambda x . E x) a ->_beta E a
-Главное, чтобы в E не было свободной переменной x, иначе ничего не выйдет. Соответственно, делаем это преобразование:
+Главное, чтобы в E не было свободной переменной x, иначе ничего не выйдет. Соотв, делаем это преобр.:
- E &rarr;<sub>&eta;</sub> &lambda; x. E x
+ E ->_etta lambda x. E x
-Что оно позволяет делать? Например, частичное применение встроенных функций. Например, если есть * x y. Является ли * 3 л-выр? Да. А как же с ним работать? Применим &eta;-преобр, получим &lambda; x . * 3 x. Благодаря этому мы можем делать частичное применение функций.
+Что оно позв. делать? Например, част. применение встроенных функций. Например, если есть * x y. Является ли * 3 л-выр? Да. А как же с ним работать. Применим &etta;-преобр, получим lambda x . * 3 x. Благодаря этому мы можем делать частичное применение функций.
-... это называется карринг, по имени учёного Карри Хаскелла (Curry).
+... это называется карринг, по имени учёного Карри (Curry).
 Наконец, последнее на сегодня, что же такое Y-combinator. Хочется нам, к примеру, сделать рек. функцию, но как, здесь же нет имён? Мы эту фнкцию получим в кач. второго аргумента. То есть функция получает на фход аргмент и самого себя, и исхитримся и подадим её на вход.
@@ Строка 207: / Строка 201: @@
 Лектор напишет её сначала на лиспе:
- (setq f #'(&lambda; (s x) (if (= x 0) 0 (+ x (funcall s s (- x 1))))))
+ (setq f #'(lambda (s x) (if (= x 0) 0 (+ x (funcall s s (- x 1))))))
 Что теперь сделать? Нао её вызвать, подав ей на вход число и её саму. Как это сделать?
@@ Строка 215: / Строка 209: @@
 можно то же самое сделать и на лямбда-абстракциях
-&lambda; s . &lambda; x . COND (= x 0) 0 (+ x (s (- x 1)))
+lambda s . lambda x . COND (= x 0) 0 (+ x (s (- x 1)))
 Сущ. неподв. точка, т. е. f(x) = x, и она есть для кажого лямбда-выр.
@@ Строка 225: / Строка 219: @@
 Как выглядит Y-combinator:
- Y = &lambda; h . (&lambda; x . h (x x)) (&lambda; x . h (x x))
+ Y = lambda h . (lambda x . h (x x)) (lambda x . h (x x))
 теперь осталось что?
- Y &lambda; s . &lambda; x . COND (= x 0) 0 (+ x (s (- x 1)))
+ Y lambda s . lambda x . COND (= x 0) 0 (+ x (s (- x 1)))
 И отредуцировать. Результатом будет функция, от одного арг., выч. сумму.
 y-comb. используется в haskell.
-<gallery perrow="5" widths="200">
-Изображение:Paradigm 091029 02.jpg|&lambda;-исчисление.
-Изображение:Paradigm 091029 03.jpg|Сокращённая форма для нескольких функций.
-Изображение:Paradigm 091029 04.jpg|БНФ для &lambda;-выражений.
-Изображение:Paradigm 091029 05.jpg|БНФ для &lambda;-выражений.
-Изображение:Paradigm 091029 06.jpg|&beta;-редукция, &delta;-редукция.
-Изображение:Paradigm 091029 07.jpg|Пример с увеличением текстуальной длины выражения при применении &beta;-редукции.
-Изображение:Paradigm 091029 08.jpg|Пример с увеличением текстуальной длины выражения при применении &beta;-редукции. Исправленный вариант.
-Изображение:Paradigm 091029 09.jpg|Пример на использование &beta;-редукции.
-Изображение:Paradigm 091029 10.jpg|Конфликт имён.
-Изображение:Paradigm 091029 11.jpg|&alpha;-преобразование.
-Изображение:Paradigm 091029 12.jpg|Разный порядок выбора редексов для редукции.
-Изображение:Paradigm 091029 13.jpg|Пример с бесконечной ветвью редуцирования редексов.
-Изображение:Paradigm 091029 14.jpg|Почему ленивое вычисление логических выражение не есть ленивые вычисления.
-Изображение:Paradigm 091029 15.jpg|Построение множеств free variables и bounded variables.
-Изображение:Paradigm 091029 16.jpg|&eta;-преобразование.
-Изображение:Paradigm 091029 17.jpg|&eta;-преобразование.
-Изображение:Paradigm 091029 18.jpg|Пример использования &eta;-преобразования.
-Изображение:Paradigm 091029 19.jpg|Currying.
-Изображение:Paradigm 091029 20.jpg|Y-combinator.
-</gallery>
 {{Парадигмы программирования}}
 {{Lection-stub}}