Редактирование: Парадигмы программирования, 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»]]]
* '''Аудиозапись:''' http://esyr.org/lections/audio/paradigms_2009_winter/paradigms_09_10_29.ogg

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

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

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

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

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

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

&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://www.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 семестр

Поиск

Инструменты

@@ Строка 147: / Строка 147: @@
  (&lambda; x . &lambda; y . y) ((&lambda; z . z z) (&lambda; z . z. z))
-Вопрос, какой же редекс тогда надо выбирать и зачем? Введём несколько определений.
+Вопрос, какой же редекс тогда надо выбирать и зачем? Введём неск. определений.
  * Самый левый редекс --- его лямбда или имя примитивной функции находятся текстуально левее всех остальных.
  * Самый внешний редекс --- тот, который текстуально не содержится ни в каком другом.
- * Самый внутренний --- тот, в котором не содержится никакой другой.
+ * Самый внутренний --- тот, в котором не содерж. никакой другой.
 Есть два порядка?
@@ Строка 158: / Строка 158: @@
 Здесь мы сначала применили сначала нормальный, потом аппликативный. Теперь можно уточнить:
-Следствие из теор. Чёрча-Россера. нормальный порядок редукции приводит к нормальной
+Следствие из теор. Чёрча-Россера. нормальный порядок редукции приводит к норм. форме за конеч. число шагов, если она вообще есть.
-форме за конечное число шагов, если она вообще есть.
-Теперь самое интересное. Если отвлечься от л-выражений и вернуться к программированию, то можно вспомнить, что есть энергичная и ленивая стратегия вычислений При энергичной мы вычисляем всё, что только можем. При ленивых вычислениях увидев выражение мы запоминаем его и не вычисляем до тех пор, пока не припрёт. Например:
+Теперь самое интересное. Если отвлечься от л-выр. и вернуться к прогр., то можно вспомнить, что есть энергинча и ленивая стратегия вычисл. При энерг. мы выч. всё, что только можем. При ленивых выч. мы при виде выр. мы запоминаем его и не вычисляем, пока можно, до тех пор, пока не припрёт. Например:
  (   ) > 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: / Строка 192: @@
  (&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. Хочется нам, к примеру, сделать рек. функцию, но как, здесь же нет имён? Мы эту фнкцию получим в кач. второго аргумента. То есть функция получает на фход аргмент и самого себя, и исхитримся и подадим её на вход.