Редактирование: Парадигмы программирования, 06 лекция (от 29 октября)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 1: | Строка 1: | ||
[[Image:paradigm_091029_01.jpg|thumb|right|300px|«На эту тему мне понравилась [http://theartoftattoo.files.wordpress.com/2009/04/y-combinator.jpg татуировка с Y-combinator»]]] | [[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 | ||
= лямбда-исчисления = | = лямбда-исчисления = | ||
- | + | На самом деле, л-исчисл. имеют не совсем прямое. л-исчисл. было придумано Чёрчем задолго до программирования. | |
- | Похоже на то, что любую функцию, которая за конечное время даёт | + | Похоже на то, что любую функцию, которая за конечное время даёт рез-т от конечного числа аргументов, записать можно. Также для неё можно сделать МТ, и т. д. |
- | + | Л-вычисл это мат. абстр., некий формализм, прямого отн. к прогр. не имеющ. | |
- | Есть легенда, что | + | Есть легенда, что еогда МакКарти писал лисп, он вдохновился л-исчисл, и лисп писался как реализ. л-исчисл. Это не так, хотя впоследствии лямбда туда была добавлена. |
- | Как в л- | + | Как в л-исчисл запис. функция: |
- | λ x . и дальше выражение, задающее функцию. | + | λ x . и дальше выражение, задающее функцию. Как оно задётся, бывают разные способы. Обычно исп. польскую нотацию |
λ x . * 3 x | λ x . * 3 x | ||
Строка 22: | Строка 21: | ||
* . — которая возвращает | * . — которая возвращает | ||
- | Большинство авторов | + | Большинство авторов рассм. ф-цию от одного параметра, но мощности это не уменьшает. Да, некоторые авторы пишут |
λ x y z . + x * y z | λ x y z . + x * y z | ||
Строка 30: | Строка 29: | ||
λ x . λ y . λ z . + x * y z | λ x . λ y . λ z . + x * y z | ||
- | Такая конструкция | + | Такая конструкция наз. лямбда-абстр, то, что после точки — телом. Как видно, в теле может содержаться произв. л-выр., в том числе лямбда. |
- | Если мы | + | Если мы видем два лямбда-выр., E_1 E_2, то это обычно значит, что первое выр. — функция, а второе, знач, к котторому его нужно применить. |
- | знач, к | + | |
- | Чисто синтаксически, функцию всегда применяют к самому левому | + | Чисто синтаксически, функцию всегда применяют к самому левому арг., то есть, если есть такая запись: |
(...((λ x_1 . λ x_2 . ... λ x_n . E) a_1) a_2) ...) a_n | (...((λ x_1 . λ x_2 . ... λ x_n . E) a_1) a_2) ...) a_n | ||
- | + | То есть соглащ., что такое выр. можно записать неск. короче: | |
(λ x_1 . lamda x_2 . ... λ x_n . E) a_1 a_2 ... a_n | (λ x_1 . lamda x_2 . ... λ x_n . E) a_1 a_2 ... a_n | ||
Строка 46: | Строка 44: | ||
<exp> ::= λ <id> . <exp> | <id> | <exp> <exp> | (<exp>) | <const> | <exp> ::= λ <id> . <exp> | <id> | <exp> <exp> | (<exp>) | <const> | ||
- | <id> ::= идентификатор (какие могут быть | + | <id> ::= идентификатор (какие могут быть идент --- зависит от того, какой стиль приняли) |
<const> ::= константы | <const> ::= константы | ||
- | Константы заслуживают более внимательного рассмотрения. | + | Константы заслуживают более внимательного рассмотрения. Конст. могут обозначать: |
- | # Числа. Числа могут быть как целые, так и веществ. | + | # Числа. Числа могут быть как целые, так и веществ. В больш. случае, когда рассм. л-выч., обычно до вещ. чисел не доходят. |
- | # Булевы значения: Истина и Ложь. Как | + | # Булевы значения: Истина и Ложь. Как конкр. их обозначить, это тоже вопрос философский. |
# [ Строки ]. Далеко не все авторы про них вспоминают | # [ Строки ]. Далеко не все авторы про них вспоминают | ||
# Пустой список. Обычно его обозн. <>, хотя можно обозн. как угодно. | # Пустой список. Обычно его обозн. <>, хотя можно обозн. как угодно. | ||
Строка 58: | Строка 56: | ||
## Знаки отношений: < > = != >= ... | ## Знаки отношений: < > = != >= ... | ||
## Функции работы со списками: CONS, HEAD, TAIL, NULL (предикат, проверка на пустой список) | ## Функции работы со списками: CONS, HEAD, TAIL, NULL (предикат, проверка на пустой список) | ||
- | ## Иногда некоторые авторы, в | + | ## Иногда некоторые авторы, в частн., Филд, Харрисон, считают необх. ввод кортежей. TUPLE-n, INDEX |
## COND | ## COND | ||
## '''...''' | ## '''...''' | ||
- | Вообще, можно делать лямбда- | + | Вообще, можно делать лямбда-выч. без констант, сконстр. из из первич. понятий, но это к прогр. мало отношения имеет. Без них тяжело. Сначала вводятся списки, потом числа как списки разной длины, а чтобы ввести умножение, нужно неск. страниц исписать. |
Примеры лямбда-выражений. Самое простое — просто константа. | Примеры лямбда-выражений. Самое простое — просто константа. | ||
Строка 70: | Строка 68: | ||
λ y . * 2 y ; лямбда-абстракция | λ y . * 2 y ; лямбда-абстракция | ||
- | В многоточие входит в том числе cond. Он | + | В многоточие жироне входит в том числе cond. Он аналогичн лисповскому if. Похоже на сишную тернарную операцию. |
(λ f . lmbda a λ b . f a b) (λ x . (λ y . x)) | (λ f . lmbda a λ b . f a b) (λ x . (λ y . x)) | ||
- | Вернёт a ((λ x . (λ y . x)) как ф-ция от двух. арг подст. в f, и сама по себе | + | Вернёт a ((λ x . (λ y . x)) как ф-ция от двух. арг подст. в f, и сама по себе возвр. первый арг.). |
λ f . λ x . COND (= x 1) x (* x (f (- x 1))) | λ f . λ x . COND (= x 1) x (* x (f (- x 1))) | ||
- | Имеет | + | Имеет отн. к вычислению факториала. Вообще, без имён функций тяжело, дальше мы посмотрим, как это решить. |
- | Как л-выр. вычисл. Т.н. правила редукции. | + | Как л-выр. вычисл. Т. н. правила редукции. |
- | * Константы | + | * Константы редуц. в себя |
* Функция и арг. Применяется дельта-правило. Например: + 1 2 →<sub>δ</sub> 3. Из этого выр. по дельта-правилу, или, применив дельта-редукцию, получаем 3. Понятно, что дельта-правила есть для каждой функции. Например, у нас есть выр. | * Функция и арг. Применяется дельта-правило. Например: + 1 2 →<sub>δ</sub> 3. Из этого выр. по дельта-правилу, или, применив дельта-редукцию, получаем 3. Понятно, что дельта-правила есть для каждой функции. Например, у нас есть выр. | ||
* (+ 1 2) (- 4 1) →<sub>δ</sub> * (+ 1 2) 3 →<sub>δ</sub> * 3 3 →<sub>δ</sub> 9 | * (+ 1 2) (- 4 1) →<sub>δ</sub> * (+ 1 2) 3 →<sub>δ</sub> * 3 3 →<sub>δ</sub> 9 | ||
- | * Применение ф-ции, | + | * Применение ф-ции, напис. через лямбда-абстракцию. Заменяем чисто текстуально, результат замены --- рез-т выражения: |
(λ x . * x x) 2 →<sub>β</sub> * 2 2 →<sub>δ</sub> 4 | (λ x . * x x) 2 →<sub>β</sub> * 2 2 →<sub>δ</sub> 4 | ||
(λ x . + x x) (* (+ 2 3) 4) →<sub>β</sub> + (* (+ 2 3) 4) (* (+ 2 3) 4) | (λ x . + x x) (* (+ 2 3) 4) →<sub>β</sub> + (* (+ 2 3) 4) (* (+ 2 3) 4) | ||
Строка 90: | Строка 88: | ||
(λ x . λ y . + x y) 7 8 →<sub>β</sub> (λ y . + 7 y) 8 →<sub>β</sub> + 7 8 →<sub>δ</sub> 15 | (λ x . λ y . + x y) 7 8 →<sub>β</sub> (λ y . + 7 y) 8 →<sub>β</sub> + 7 8 →<sub>δ</sub> 15 | ||
- | Редуцируемая часть | + | Редуцируемая часть. выр наз. редексом (redex, reducible expression) |
- | Если | + | Если редаксов в выр. нет, тогда говорят, что выр. имеет норм. форму. |
- | Имеется некий подводный камень, связанный с | + | Имеется некий подводный камень, связанный с одноим. символами. Рассмотрим выражение: |
λ x . (λ x . x) (+ 1 x) | λ x . (λ x . x) (+ 1 x) | ||
Строка 104: | Строка 102: | ||
Если взять это в скобки и где-то применить, то понятно, что получится не то, что хотели. Получается конфликт имён. Как это разрешить? Например, постановить, что если мы подобные вещи применяем к чему-то, то внутри ничего не трогать. | Если взять это в скобки и где-то применить, то понятно, что получится не то, что хотели. Получается конфликт имён. Как это разрешить? Например, постановить, что если мы подобные вещи применяем к чему-то, то внутри ничего не трогать. | ||
- | Есть второй вариант, т.н. альфа- | + | Есть второй вариант, т. н. альфа-преобразовнаие. Оно не наз. редукцие, поск. оно ничего не упрощ., оно переименовывает пременную. |
Если не учитывать контекст имён, то что получится: | Если не учитывать контекст имён, то что получится: | ||
Строка 111: | Строка 109: | ||
(λ x . (λ y . y) (+ 1 x)) 3 -> (λ y . y) (+ 1 3) -> ... -> 8 | (λ x . (λ y . y) (+ 1 x)) 3 -> (λ y . y) (+ 1 3) -> ... -> 8 | ||
- | То есть вот, конфликты имён бывают, конфликты имён | + | То есть вот, конфликты имён бывают, конфликты имён ращреш. альфа-преобр, это не совсем ред., хотя записывается также: |
λ x. x →<sub>α</sub> λ y . y | λ x. x →<sub>α</sub> λ y . y | ||
- | Порядок | + | Порядок выбор редексов для редукции. В л-выр может быть неск. редексов, и вопрос, с какого начать? Вопрос интересный и весьма принципиальный. Рассмотрим пример: |
(λ f . λ x . f 4 x) (λ y . λ x . + x y) 3 -> | (λ f . λ x . f 4 x) (λ y . λ x . + x y) 3 -> | ||
Строка 126: | Строка 124: | ||
2. (λ x . (λ x . + x 4) x) 3 -> (λ x . + x 4) 3 -> + 3 4 -> 7 | 2. (λ x . (λ x . + x 4) x) 3 -> (λ x . + x 4) 3 -> + 3 4 -> 7 | ||
- | + | В принципе, до какой-то степени так и должно быть, но есть теорема Чёрча-Россера, которая гласит, что если у лямбда-выр. есть норм. форма, то она только одна (если неск., то они эквив. с точностью до алф. преобр.). Из этого следует, что она аже достигается. Но выбрав нехороший порядок редукции, то можно не прийти к норм. форме вообще. Есть классич. пример, когда один порядок не приводит к норм. форме вооббще никогда, другой же за один шаг. | |
- | + | ||
- | Из этого следует, что она | + | |
- | другой же за один шаг. | + | |
(λ x . λ y . y) ((λ z . z z) (λ z . z. z)) | (λ x . λ y . y) ((λ z . z z) (λ z . z. z)) | ||
Строка 147: | Строка 142: | ||
(λ x . λ y . y) ((λ z . z z) (λ z . z. z)) | (λ x . λ y . y) ((λ z . z z) (λ z . z. z)) | ||
- | Вопрос, какой же редекс тогда надо выбирать и зачем? Введём | + | Вопрос, какой же редекс тогда надо выбирать и зачем? Введём неск. определений. |
* Самый левый редекс --- его лямбда или имя примитивной функции находятся текстуально левее всех остальных. | * Самый левый редекс --- его лямбда или имя примитивной функции находятся текстуально левее всех остальных. | ||
- | * Самый внешний редекс --- тот, который текстуально не | + | * Самый внешний редекс --- тот, который текстуально не содерж. ни в каком другом. |
- | * Самый внутренний --- тот, в котором не | + | * Самый внутренний --- тот, который в котором не содерж. никакой другой. |
Есть два порядка? | Есть два порядка? | ||
* Аппликативный --- выбирается самый левый внутренний. | * Аппликативный --- выбирается самый левый внутренний. | ||
- | * Нормальный --- | + | * Нормальный --- берём все самые внешние, выбираем из них самый левый, и его используем. |
- | Здесь мы | + | Здесь мы сначла применили сначала нормальный, потом аппликативный. Теперь можно уточнить: |
- | Следствие из теор. Чёрча-Россера. нормальный порядок редукции приводит к | + | Следствие из теор. Чёрча-Россера. нормальный порядок редукции приводит к норм. форме за конеч. число шагов, если она вообще есть. |
- | форме за | + | |
- | Теперь самое интересное. Если отвлечься от л- | + | Теперь самое интересное. Если отвлечься от л-выр. и вернуться к прогр., то можно вспомнить, что есть энергинча и ленивая стратегия вычисл. При энерг. мы выч. всё, что только можем. При ленивых выч. мы при виде выр. мы запоминаем его и не вычисляем, пока можно, до тех пор, пока не припрёт. Например: |
( ) > 3 | ( ) > 3 | ||
- | Вот тут нам | + | Вот тут нам надо вычислить знач. выр., не раньше. Бывает ли такое в языках прогр.? Бывает, но очень редко и по-немногу. Ленивая семантика из компилир. языков --- только хаскель, но все привычные, императивные --- энергичные. |
- | Где можно встретить ленивую модель вычислений? Например, при | + | Где можно встретить ленивую модель вычислений? Например, при подст. макросов. Макропроцессору это просто, поск. он работает на уровне текстовых строк. В некоторых командно-скриптовых языках ленивая семантика имеется. |
Но сейчас, когда мы смотрим на л-выч., мы видим, что ленивый порядок вычисл. оказался в каком-то виде мощнее. | Но сейчас, когда мы смотрим на л-выч., мы видим, что ленивый порядок вычисл. оказался в каком-то виде мощнее. | ||
- | Введём такую | + | Введём такую вещб, как понятие связанных и свободных переменных |
λ x . x y | λ x . x y | ||
- | Понятно, что x | + | Понятно, что x связ., а y --- вободная. Если чуть строже, то построим мн-во FV(E) (free variables(expression)). Как оно вводится: |
* FV(x) = {x} | * FV(x) = {x} | ||
* FV(c) = ∅ | * FV(c) = ∅ | ||
Строка 193: | Строка 187: | ||
(λ x . E x) a →<sub>β</sub> E a | (λ x . E x) a →<sub>β</sub> E a | ||
- | Главное, чтобы в E не было свободной переменной x, иначе ничего не выйдет. | + | Главное, чтобы в E не было свободной переменной x, иначе ничего не выйдет. Соотв, делаем это преобр.: |
E →<sub>η</sub> λ x. E x | E →<sub>η</sub> λ x. E x | ||
- | Что оно | + | Что оно позв. делать? Например, част. применение встроенных функций. Например, если есть * x y. Является ли * 3 л-выр? Да. А как же с ним работать. Применим η-преобр, получим λ x . * 3 x. Благодаря этому мы можем делать частичное применение функций. |
- | ... это называется карринг, по имени учёного Карри | + | ... это называется карринг, по имени учёного Карри (Curry). |
Наконец, последнее на сегодня, что же такое Y-combinator. Хочется нам, к примеру, сделать рек. функцию, но как, здесь же нет имён? Мы эту фнкцию получим в кач. второго аргумента. То есть функция получает на фход аргмент и самого себя, и исхитримся и подадим её на вход. | Наконец, последнее на сегодня, что же такое Y-combinator. Хочется нам, к примеру, сделать рек. функцию, но как, здесь же нет имён? Мы эту фнкцию получим в кач. второго аргумента. То есть функция получает на фход аргмент и самого себя, и исхитримся и подадим её на вход. |