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

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

Версия от 22:38, 5 октября 2010; ESyr01 (Обсуждение | вклад)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)

ПРЕДУПРЕЖДЕНИЕ: Вы редактируете устаревшую версию данной страницы. После сохранения страницы будут потеряны изменения, сделанные в последующих версиях.

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

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.org/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