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

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

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

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

[[Image:paradigm_091029_01.jpg|thumb|right|300px|«На эту тему мне понравилась [http://theartoftattoo.files.wordpress.com/2009/04/y-combinator.jpg татуировка с 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 &rarr;&delta; 3. Из этого выр. по дельта-правилу, или, применив дельта-редукцию, получаем 3. Понятно, что дельта-правила есть для каждой функции. Например, у нас есть выр.
 * (+ 1 2) (- 4 1) &rarr;&delta; * (+ 1 2) 3 &rarr;&delta; * 3 3 &rarr;&delta; 9
* Применение ф-ции, напис. через лямбда-абстракцию. Заменяем чисто текстуально, результат замены --- рез-т выражения:
 (&lambda; x . * x x) 2 &rarr;&beta; * 2 2 &rarr;&delta; 4
 (&lambda; x . + x x) (* (+ 2 3) 4) &rarr;&beta; + (* (+ 2 3) 4) (* (+ 2 3) 4)
: Текстуально оно становится длиннее, но мы избавляемся от символа лямбда.
 (&lambda; x . &lambda; y . + x y) 7 8 &rarr;&beta; (&lambda; y . + 7 y) 8 &rarr;&beta; + 7 8 &rarr;&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 &rarr;&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), то можно вести речь об &eta;-преобразовании.

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

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

E &rarr;&eta; &lambda; x. E x

Что оно позв. делать? Например, част. применение встроенных функций. Например, если есть * x y. Является ли * 3 л-выр? Да. А как же с ним работать. Применим &eta;-преобр, получим &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.

<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>

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

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

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

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

Получено с http://esyr.name/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»]]]
-* '''Аудиозапись:''' http://esyr.org/lections/audio/paradigms_2009_winter/paradigms_09_10_29.ogg
 = лямбда-исчисления =
-Лямбда-исчисление было придумано Чёрчем задолго до программирования.
+На самом деле, л-исчисл. имеют не совсем прямое. л-исчисл. было придумано Чёрчем задолго до программирования.
-Похоже на то, что любую функцию, которая за конечное время даёт результат от конечного числа аргументов, записать можно. Также для неё можно сделать МТ, и т. д.
+Похоже на то, что любую функцию, которая за конечное время даёт рез-т от конечного числа аргументов, записать можно. Также для неё можно сделать МТ, и т. д.
-Лямбда-вычисления это математическая абстракция, некий формализм, прямого отношения к программированию не имеющая
+Л-вычисл это мат. абстр., некий формализм, прямого отн. к прогр. не имеющ.
-Есть легенда, что когда МакКарти писал лисп, он вдохновился л-исчислением, и лисп писался как его реализация. Это не так, хотя впоследствии лямбда туда была добавлена.
+Есть легенда, что еогда МакКарти писал лисп, он вдохновился л-исчисл, и лисп писался как реализ. л-исчисл. Это не так, хотя впоследствии лямбда туда была добавлена.
-Как в л-исчислислении записывается функция:
+Как в л-исчисл запис. функция:
-&lambda; x . и дальше выражение, задающее функцию. Есть разные способы, обычно используют польскую нотацию
+&lambda; x . и дальше выражение, задающее функцию. Как оно задётся, бывают разные способы. Обычно исп. польскую нотацию
  &lambda; x . * 3 x
@@ Строка 22: / Строка 21: @@
 * . — которая возвращает
-Большинство авторов рассматривают ф-цию от одного параметра, но мощности это не уменьшает. Да, некоторые авторы пишут
+Большинство авторов рассм. ф-цию от одного параметра, но мощности это не уменьшает. Да, некоторые авторы пишут
  &lambda; x y z . + x * y z
@@ Строка 30: / Строка 29: @@
  &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 . lamda x_2 . ... &lambda; x_n . E) a_1 a_2 ... a_n
@@ Строка 46: / Строка 44: @@
  <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
 ## '''...'''
-Вообще, можно делать лямбда-вычисления без констант, сконстр. их из первич. понятий, но это к прогр. мало отношения имеет. Без них тяжело. Сначала вводятся списки, потом числа как списки разной длины, а чтобы ввести умножение, нужно несколько страниц исписать.
+Вообще, можно делать лямбда-выч. без констант, сконстр. из из первич. понятий, но это к прогр. мало отношения имеет. Без них тяжело. Сначала вводятся списки, потом числа как списки разной длины, а чтобы ввести умножение, нужно неск. страниц исписать.
 Примеры лямбда-выражений. Самое простое — просто константа.
@@ Строка 70: / Строка 68: @@
  &lambda; y . * 2 y ; лямбда-абстракция
-В многоточие входит в том числе cond. Он аналогичен лисповскому if. Похоже на сишную тернарную операцию.
+В многоточие жироне входит в том числе cond. Он аналогичн лисповскому if. Похоже на сишную тернарную операцию.
  (&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)))
-Имеет отношение к вычислению факториала. Вообще, без имён функций тяжело, дальше мы посмотрим, как это решить.
+Имеет отн. к вычислению факториала. Вообще, без имён функций тяжело, дальше мы посмотрим, как это решить.
-Как л-выр. вычисл. Т.н. правила редукции.
+Как л-выр. вычисл. Т. н. правила редукции.
-* Константы редуцуются в себя
+* Константы редуц. в себя
 * Функция и арг. Применяется дельта-правило. Например: + 1 2 &rarr;<sub>&delta;</sub> 3. Из этого выр. по дельта-правилу, или, применив дельта-редукцию, получаем 3. Понятно, что дельта-правила есть для каждой функции. Например, у нас есть выр.
  * (+ 1 2) (- 4 1) &rarr;<sub>&delta;</sub> * (+ 1 2) 3 &rarr;<sub>&delta;</sub> * 3 3 &rarr;<sub>&delta;</sub> 9
-* Применение ф-ции, написанной через лямбда-абстракцию. Заменяем чисто текстуально, результат замены --- результат выражения:
+* Применение ф-ции, напис. через лямбда-абстракцию. Заменяем чисто текстуально, результат замены --- рез-т выражения:
  (&lambda; x . * x x) 2 &rarr;<sub>&beta;</sub> * 2 2  &rarr;<sub>&delta;</sub> 4
  (&lambda; x . + x x) (* (+ 2 3) 4) &rarr;<sub>&beta;</sub> + (* (+ 2 3) 4) (* (+ 2 3) 4)
@@ Строка 90: / Строка 88: @@
  (&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
-Редуцируемая часть выражения  называется редексом (redex, reducible expression)
+Редуцируемая часть. выр наз. редексом (redex, reducible expression)
-Если редексов в выражении нет, тогда говорят, что выражение имеет норм. форму.
+Если редаксов в выр. нет, тогда говорят, что выр. имеет норм. форму.
-Имеется некий подводный камень, связанный с одноименными символами. Рассмотрим выражение:
+Имеется некий подводный камень, связанный с одноим. символами. Рассмотрим выражение:
  &lambda; x . (&lambda; x . x) (+ 1 x)
@@ Строка 104: / Строка 102: @@
 Если взять это в скобки и где-то применить, то понятно, что получится не то, что хотели. Получается конфликт имён. Как это разрешить? Например, постановить, что если мы подобные вещи применяем к чему-то, то внутри ничего не трогать.
-Есть второй вариант, т.н. альфа-преобразование. Оно не называется редукцией, поскольку ничего не упрощает, оно переименовывает перемененную.
+Есть второй вариант, т. н. альфа-преобразовнаие. Оно не наз. редукцие, поск. оно ничего не упрощ., оно переименовывает пременную.
 Если не учитывать контекст имён, то что получится:
@@ Строка 111: / Строка 109: @@
  (&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; f . &lambda; x . f 4 x) (&lambda; y . &lambda; x . + x y) 3 ->
@@ Строка 126: / Строка 124: @@
 . (&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))
@@ Строка 147: / Строка 142: @@
  (&lambda; x . &lambda; y . y) ((&lambda; z . z z) (&lambda; z . z. z))
-Вопрос, какой же редекс тогда надо выбирать и зачем? Введём несколько определений.
+Вопрос, какой же редекс тогда надо выбирать и зачем? Введём неск. определений.
  * Самый левый редекс --- его лямбда или имя примитивной функции находятся текстуально левее всех остальных.
- * Самый внешний редекс --- тот, который текстуально не содержится ни в каком другом.
+ * Самый внешний редекс --- тот, который текстуально не содерж. ни в каком другом.
- * Самый внутренний --- тот, в котором не содержится никакой другой.
+ * Самый внутренний --- тот, который в котором не содерж. никакой другой.
 Есть два порядка?
  * Аппликативный --- выбирается самый левый внутренний.
- * Нормальный --- из всех самых внешних, выбираем самый левый.
+ * Нормальный --- берём все самые внешние, выбираем из них самый левый, и его используем.
-Здесь мы сначала применили сначала нормальный, потом аппликативный. Теперь можно уточнить:
+Здесь мы сначла применили сначала нормальный, потом аппликативный. Теперь можно уточнить:
-Следствие из теор. Чёрча-Россера. нормальный порядок редукции приводит к нормальной
+Следствие из теор. Чёрча-Россера. нормальный порядок редукции приводит к норм. форме за конеч. число шагов, если она вообще есть.
-форме за конечное число шагов, если она вообще есть.
-Теперь самое интересное. Если отвлечься от л-выражений и вернуться к программированию, то можно вспомнить, что есть энергичная и ленивая стратегия вычислений При энергичной мы вычисляем всё, что только можем. При ленивых вычислениях увидев выражение мы запоминаем его и не вычисляем до тех пор, пока не припрёт. Например:
+Теперь самое интересное. Если отвлечься от л-выр. и вернуться к прогр., то можно вспомнить, что есть энергинча и ленивая стратегия вычисл. При энерг. мы выч. всё, что только можем. При ленивых выч. мы при виде выр. мы запоминаем его и не вычисляем, пока можно, до тех пор, пока не припрёт. Например:
  (   ) > 3
-Вот тут нам действительно надо вычислить значение выражение, не раньше. Бывает ли такое в языках программирования? Бывает, но очень редко. Ленивая семантика из компилир. языков --- только haskell, но все привычные, императивные --- энергичные.
+Вот тут нам надо вычислить знач. выр., не раньше. Бывает ли такое в языках прогр.? Бывает, но очень редко и по-немногу. Ленивая семантика из компилир. языков --- только хаскель, но все привычные, императивные --- энергичные.
-Где можно встретить ленивую модель вычислений? Например, при подстановке макросов. Макропроцессору это просто, поскольку он работает на уровне текстовых строк. В некоторых командно-скриптовых языках ленивая семантика имеется.
+Где можно встретить ленивую модель вычислений? Например, при подст. макросов. Макропроцессору это просто, поск. он работает на уровне текстовых строк. В некоторых командно-скриптовых языках ленивая семантика имеется.
 Но сейчас, когда мы смотрим на л-выч., мы видим, что ленивый порядок вычисл. оказался в каком-то виде мощнее.
-Введём такую вещь, как понятие связанных и свободных переменных
+Введём такую вещб, как понятие связанных и свободных переменных
  &lambda; x . x y
-Понятно, что x связанная, а y --- свободная. Если чуть строже, то построим мн-во FV(E) (free variables(expression)). Как оно вводится:
+Понятно, что x связ., а y --- вободная. Если чуть строже, то построим мн-во FV(E) (free variables(expression)). Как оно вводится:
 * FV(x) = {x}
 * FV(c) = &empty;
@@ Строка 193: / Строка 187: @@
  (&lambda; x . E x) a &rarr;<sub>&beta;</sub> E a
-Главное, чтобы в E не было свободной переменной x, иначе ничего не выйдет. Соответственно, делаем это преобразование:
+Главное, чтобы в E не было свободной переменной x, иначе ничего не выйдет. Соотв, делаем это преобр.:
  E &rarr;<sub>&eta;</sub> &lambda; x. E x
-Что оно позволяет делать? Например, частичное применение встроенных функций. Например, если есть * x y. Является ли * 3 л-выр? Да. А как же с ним работать? Применим &eta;-преобр, получим &lambda; x . * 3 x. Благодаря этому мы можем делать частичное применение функций.
+Что оно позв. делать? Например, част. применение встроенных функций. Например, если есть * x y. Является ли * 3 л-выр? Да. А как же с ним работать. Применим &eta;-преобр, получим &lambda; x . * 3 x. Благодаря этому мы можем делать частичное применение функций.
-... это называется карринг, по имени учёного Карри Хаскелла (Curry).
+... это называется карринг, по имени учёного Карри (Curry).
 Наконец, последнее на сегодня, что же такое Y-combinator. Хочется нам, к примеру, сделать рек. функцию, но как, здесь же нет имён? Мы эту фнкцию получим в кач. второго аргумента. То есть функция получает на фход аргмент и самого себя, и исхитримся и подадим её на вход.
@@ Строка 255: / Строка 249: @@
 Изображение:Paradigm 091029 19.jpg|Currying.
 Изображение:Paradigm 091029 20.jpg|Y-combinator.
-</gallery>
+<gallery>
 {{Парадигмы программирования}}
 {{Lection-stub}}