Редактирование: Haskell, 02 лекция (от 05 октября)

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

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

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

* '''Аудиозапись:''' http://esyr.org/lections/audio/haskell_2010_winter/haskell_10_10_05.ogg
* '''Видеозапись:''' http://esyr.org/video/haskell/haskell_10_10_05.raw.ogv

TRUE=&lambda;ab.a
 FALSE=&lambda;ab.b
 IF=&lambda;cab.cab

IF FALSE 1 0 &rarr; (&lambda;cab.cab) FALS 1 0 &rarr;&beta; (&lambda;ab.FALSE a b) 1 0 &rarr; (&lambda;ab.(&lambda;ab.b)ab) 1 0 &rarr;&alpha; (&lambda; ab(&lambda;xy.y)ab) 1 0 &rarr;&rarr;&beta; (&lambda;ab.b) 1 0 &rarr;&rarr;&beta;  0

AND=&lambda;ab.aba
OR=&lambda;ab.aab
NOT=&lambda;cab.cba

L=(&lambda;x.xx)(&lambda;x.xx)
Попробуем произвести подстановку:
L=(&lambda;x.xx)(&lambda;x.xx)

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

Попробуем записать следующее выражение:

TRUE 1 L

Каким образом мы можем его вычислить:

1-й вариатн: раскрываем TRUE

(&lambda;ab.a) 1 L &rarr;&beta; 1

2) TRUE 1 (&lambda;x.xx)(&lambda;x.xx) &rarr;&beta; и тут мы зациклились.

Получается, что в зависимости от порядка раскрытия, мы можем найти или не найти нормальную форму.

Нормальная редукционная стратегия - способ редукции &lambda;-терма, где на каждом шаге редукции выбирается наиболее левый и наиболее внешний &beta;-редакс.

что это значит:

MN &rArr; 1) M, 2) N

Вначале мы редуцируем M, потом N ("самый левый")

(&lambda;x.M)N &rArr; 1) (&lambda;x.M)N 2) M, N

Если мы здесь используем определение формальной системы, где есть эта конверсия (&eta;: &lambda;x.Mx &rArr; M), то все эти конверсии происх. после &beta;-редукции, в конце.

Определение 2. Аппликативная редукционная стратегия - способ редукции &lambda;-терма, где на каждом шаге выбирается &beta;-редакс, не содержащий других &beta;-редаксов.

В первом примере в первом случае была нормальная редукционная стратегия, в втором - аппликативная. Они моделирует следующие алгоритмы работы в ЯП: при вызове функции иы можем как вычислить аргументы до передачи функции, так и передать их внутрь. В случае С всегда используется аппликативная стратегия. При этом может быть такая ситуация: функция использует второй аргумент только если первый не равен нулю. При этом, если мы подадим такой вызов: f(0, 3/0), то оно рухнет, хотя второй аргумент даже не задействован. В первом случае такого не происходит, но оно работает медленно. Поэтому нормальная стратегия работает медленно, но всегда приводит к результатам. В современных функциональных языках используется модифицированная стратегия, называемая ленивой нормальной стратегией. Идея в том, что мы всё ещё не вычислили значение выражения, но вместо него мы используем дерево, и передаём не всё дерево, а ссылку на него. Это позволяет как ускорить процесс, так и всегда находить результат. Но в языке C существует пример использования нормальной стратегии: это встроенный оператор if.  Именно потому, что он встроенный (вы не можете написать свой такой же), он может её использовать. Мы вычислим каждую из ветвей только после вычисления условия.

В языке haskell if можно определить следующим образом:
 if :: Bool &rarr; a &rarr; a &rarr; a
 if true a b = a
 if false a b = b
В первой строчке задаются типы выражений. Тип Bool можно определить следующим образом:
 data Bool = True | False

Вернёмся к &lambda;-исчислению. Теперь понятно, каким образом происх вычисления.

Арифметика. Здесь используются нумералы Чёрча. Нумералы Чёрча это функция.

Определим 0 как FALSE для удобства.
 0 = FALSE = &lambda;x.x
 1 = &lambda;fx.fx
 2 = &lambda;fx.f(fx)
 ...
 n = &lambda;fx.f(...f(fx)...)

Теперь определим арифметику.
 add = &lambda;mnfx.mf(nfx)
 succ=&lambda;nfx.f(nfx)
 mlt=&lambda;mnfm(nf)
 exp=&lambda;mn.nm
легко проверить, что
 add 3 2
и
 5=&lambda;fx.f(f(f(f(fx)))))
эквивалентны.

Немного сложнее будет с вычитанием. Существует расширение, позволяющее добавлять отрицательные числа, но лектор не видит смысла его показывать, там всё ещё сложнее и запись ещё длиннее. Поэтому, функцию, которая производит вычитание, или хотя бы уменьшение на единицу... мы должны определить pred как функцию, возвращающую предыдущее число или если 0 то 0. Для этого мы должны уметь определять, является ли число нулём. Предикат для этого записывается следующим образом:
 iszero=&lambda;n.n(&lambda;x.FALSE)TRUE
Попробуем раскрыть его для нуля:
 iszero 0 &rarr; 0(&lambda;x.FALSE)TRUE &rarr; (&lambda;fx.x)(&lambda;x.FALSE)TRUE &rarr; TRUE
Легко проверить, что если бы вместо x было бы хотя бы fx, то получилось бы FALSE. Обратите внимание, как производятся вычисления: вычисления производятся через функцию, передаваему в аргументе.

В случае pred мы можем записать его как
 pred=&lambda;n.n(&lambda;gk. iszero(g 1) k (add (gk) 1)) (&lambda;v.0)0
Наконец, вычитание
 sub=&lambda;mn.n PRED m
Это определение наиболее очевидно.

Таким образом, имея нумералы Чёрча, мы не требуем от языка наличия арифметики, тем не менее, обычно она есть, дабы вычисления работали быстрее.

Далее, списки. Мы говорили, что &lambda;-исчисление это также способ моделирования структур данных. Попробуем смоделировать пару чисел.

Определим пару как:
 PAIR=&lambda;xyf.fxy
Что даёт это определение: если мы определим пару из двух чисел, которую мы потом будем использовать, то редуцируется это следующим образом:
 PAIR 4 2 &rarr;&beta; &lambda;f.f 4 2
Это функция, которая, в зависимости от того, какой аргумент вы подадите, выдаёт первый элемент или второй (в терминах лиспа - car/cdr)
 CAR=FIRST=&lambda;p.p TRUE
 CDR = SND = &lambda;p.p FALSE

SND(PAIR 4 2) &rarr; (&lambda;p.p FALSE)(PAIR 4 2) &rarr; (PAIR 4 2)FALSE &rarr; (&lambda;f.f 4 2) FALSE &rarr; FALSE 4 2 &rarr; 2

С использованием пары можем определить лисповский список. Что это такое? Это пара, где первый элемент это элемент, а второй — указатель на вторую пару такого же вида, где второй элемент тоже указатель на пару, где второй элемент — nil.

В лиспе конструктор списка — cons, первый элемент списка — car, получение хвоста списка — cdr. Также существует функция isnull, которая возвращает T, если список пуст.

(3 4 5)
 (car '(3 4 5)) = 3
 (cdr '(3 4 5)) = '(4 5)
 (isnull (cdr (cdr (cdr '(3 4 5))))) = T

nil = &lambda;x.x
 cons = &lambda;xy.PAIR FALSE (PAIR xy)
 isnull = FIRST
 car = &lambda;x.FIRST(SND x)
 cdr = &lamda;x.SND(SND x)
Это уже можно использовать как список.

Не хватает одного элемента Тьюринг-полного языка — цикла. Наиболее простым методом, с т.з. лектора, является рекурсия. Как её организовать? Всё тот же Хаскел Карри решил использовать определение неподвижной точки. Неподвижная точка — такая точка из области определения функции, что значение функции в этой точке развно этой точке.
 x — НТ f(x): x &isin; D(f), f(x) = x

Комбинатор:
 &lambda;f(&lambda;x.f(xx))(&lambda;x.f(xx)) — Y-комбинатор

Вообще говоря, комбинаторов неподвижной точки существует очень много. Для примера лектор напишет только один, написанный Аланом Тьюрингом:
 (&lambda;x.&lambda;y.(y(xxy)))(&lambda;x.&lambda;y.(y(xxy)))

Общее свойство этих комбинаторов одно: у них есть некоторая часть, которая повторяется. Свойство на самом деле, если мы попробуем раскодировать комбинацию и подставить функцию, то его можно записать следующим обазом:

Для некоторого &forall;a&isin;&Lambda; Ya=a(Ya)

Как это использовать для рекурсии? Попробуем записать определение факториала:
n! = 1, если n=0; n(n-1)!

Для определения факториала требуется цикл. Определим функцию итерация факториала:
 IFACT=&lambda;f.&lambda;n.if(iszero n) 1 (mult n (f (pred n)))
после чего вычислим
 (Y IFACT)5 = IFACT (Y IFACT) 5
Таким образом мы можем видеть что аппарат &lambda;-исчисления является Тьюринг-полным, несмотря на то, что мы не имеем переменных, не имеем ..., организуем всё мы можем.

Так как функциональные языки основываются на &lambda;-исчислении, а в &lambda;-исчислении аппаратом для организации итеративных вычислений используется рекурсия, то она же используется и для ФЯП.

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

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

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

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

Получено с http://esyr.us/wiki/Haskell%2C_02_%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F_%28%D0%BE%D1%82_05_%D0%BE%D0%BA%D1%82%D1%8F%D0%B1%D1%80%D1%8F%29

Редактирование: Haskell, 02 лекция (от 05 октября)

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

Просмотры

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

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 1: / Строка 1: @@
-* '''Презентация:''' [[Media:ТФП -- Лекция 2.pdf]]
 * '''Аудиозапись:''' http://esyr.org/lections/audio/haskell_2010_winter/haskell_10_10_05.ogg
 * '''Видеозапись:''' http://esyr.org/video/haskell/haskell_10_10_05.raw.ogv
@@ Строка 62: / Строка 61: @@
 Определим 0 как FALSE для удобства.
-= FALSE = &lambda;fx.x
+= FALSE = &lambda;x.x
 = &lambda;fx.fx
 = &lambda;fx.f(fx)
@@ Строка 71: / Строка 70: @@
  add = &lambda;mnfx.mf(nfx)
  succ=&lambda;nfx.f(nfx)
- mlt=&lambda;mnf.m(nf)
+ mlt=&lambda;mnfm(nf)
  exp=&lambda;mn.nm
 легко проверить, что