Haskell, 02 лекция (от 05 октября)

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

(Различия между версиями)
Перейти к: навигация, поиск
(Новая: TRUE=λab.a FALSE=λab.b IF=λcab.cab IF FALSE 1 0 → (λcab.cab) FALS 1 0 →β (λab.FALSE a b) 1 0 → (λab.(λab.b)ab) 1 0 &...)
 
(6 промежуточных версий не показаны.)
Строка 1: Строка 1:
-
TRUE=λab.a
+
* '''Презентация:''' [[Media:ТФП -- Лекция 2.pdf]]
-
FALSE=λab.b
+
* '''Аудиозапись:''' http://esyr.org/lections/audio/haskell_2010_winter/haskell_10_10_05.ogg
-
IF=λcab.cab
+
* '''Видеозапись:''' http://esyr.org/video/haskell/haskell_10_10_05.raw.ogv
 +
 
 +
TRUE=λab.a
 +
FALSE=λab.b
 +
IF=λcab.cab
IF FALSE 1 0 → (λcab.cab) FALS 1 0 →β (λab.FALSE a b) 1 0 → (λab.(λab.b)ab) 1 0 →α (λ ab(λxy.y)ab) 1 0 →→β (λab.b) 1 0 →→β 0
IF FALSE 1 0 → (λcab.cab) FALS 1 0 →β (λab.FALSE a b) 1 0 → (λab.(λab.b)ab) 1 0 →α (λ ab(λxy.y)ab) 1 0 →→β (λab.b) 1 0 →→β 0
Строка 27: Строка 31:
2) TRUE 1 (λx.xx)(λx.xx) →β и тут мы зациклились.
2) TRUE 1 (λx.xx)(λx.xx) →β и тут мы зациклились.
-
Получается, что в зависимости от порядка раскрытия, мы можем найти лии не найти норм. форму.
+
Получается, что в зависимости от порядка раскрытия, мы можем найти или не найти нормальную форму.
Строка 42: Строка 46:
Если мы здесь используем определение формальной системы, где есть эта конверсия (η: λx.Mx ⇒ M), то все эти конверсии происх. после β-редукции, в конце.
Если мы здесь используем определение формальной системы, где есть эта конверсия (η: λx.Mx ⇒ M), то все эти конверсии происх. после β-редукции, в конце.
-
Определение 2. Аппликативная редукционная стратегия - способ редукции λ-терма, где на каждом шагевыбирается β-редакс, не содержащий других β-редаксов.
+
Определение 2. Аппликативная редукционная стратегия - способ редукции λ-терма, где на каждом шаге выбирается β-редакс, не содержащий других β-редаксов.
-
В первом примере в первом случае была нормальная редукц. стратегия, в втором - аппликативная. Они моделир. следу алгоритмы работы в ЯП: при вызове функции иы иожем как вычисл. арг до передачи функции, так и передать их внутрь. В случае С всегда исп. аппликативная тсратегия. При этом может быть такая ситуация: функция исп. второй арг. только если первый не равен нулю. При этом, если мы подадим такой вызов: f(0, 3/0), то оно рухнет, хотя второй арг. даже не задействован. В первом сл. таокго не происх., но оно работает медленно. Поэтому норм. стратегия работает медленно, но всегда приводит к результатаы. В совр. функц. языках исп. модиф. стр., наз. ленивой норм. стратегйией. Идея в том, что мы всё ещё не вычисл. знач. выр., но вместо него мы исп. дерево, и передаём не всё дерево, а ссылку на него. Это позв. как ускорить процесс, так и всегда находить рез-т. Но в языке C существует пример исп. норм. стратегии: это встроенный оператор if. Именно опотму, что он встроенный (вы не можете написать свой такой же), он может её использовать. Мы вычисл. каждую из ветвей только после вычисл. условия.
+
В первом примере в первом случае была нормальная редукционная стратегия, в втором - аппликативная. Они моделирует следующие алгоритмы работы в ЯП: при вызове функции иы можем как вычислить аргументы до передачи функции, так и передать их внутрь. В случае С всегда используется аппликативная стратегия. При этом может быть такая ситуация: функция использует второй аргумент только если первый не равен нулю. При этом, если мы подадим такой вызов: f(0, 3/0), то оно рухнет, хотя второй аргумент даже не задействован. В первом случае такого не происходит, но оно работает медленно. Поэтому нормальная стратегия работает медленно, но всегда приводит к результатам. В современных функциональных языках используется модифицированная стратегия, называемая ленивой нормальной стратегией. Идея в том, что мы всё ещё не вычислили значение выражения, но вместо него мы используем дерево, и передаём не всё дерево, а ссылку на него. Это позволяет как ускорить процесс, так и всегда находить результат. Но в языке C существует пример использования нормальной стратегии: это встроенный оператор if. Именно потому, что он встроенный (вы не можете написать свой такой же), он может её использовать. Мы вычислим каждую из ветвей только после вычисления условия.
В языке haskell if можно определить следующим образом:
В языке haskell if можно определить следующим образом:
Строка 55: Строка 59:
Вернёмся к λ-исчислению. Теперь понятно, каким образом происх вычисления.
Вернёмся к λ-исчислению. Теперь понятно, каким образом происх вычисления.
-
Арифметика. Здесь исп. нумералы Чёрча. Нумералы Чёрча это функция.
+
Арифметика. Здесь используются нумералы Чёрча. Нумералы Чёрча это функция.
Определим 0 как FALSE для удобства.
Определим 0 как FALSE для удобства.
-
0 = FALSE = λx.x
+
0 = FALSE = λfx.x
1 = λfx.fx
1 = λfx.fx
2 = λfx.f(fx)
2 = λfx.f(fx)
Строка 67: Строка 71:
add = λmnfx.mf(nfx)
add = λmnfx.mf(nfx)
succ=λnfx.f(nfx)
succ=λnfx.f(nfx)
-
mlt=λmnfm(nf)
+
mlt=λmnf.m(nf)
exp=λmn.nm
exp=λmn.nm
легко проверить, что
легко проверить, что
Строка 75: Строка 79:
эквивалентны.
эквивалентны.
-
Немного сложнее будет с вычитанием. Существует расширение, позв. добавлять отр. числа, но лектор не видит смысла его показывать, там всё ещё сложнее и запись ещё длиннее. Поэтому, функция, которая произв. вычитание, или хотя бы уменьш. на единицу... мы должны опр. pred как функцию, возвр. пред. число или если 0 то 0. Для этого мы должны уметь опр., явл. ли число нулём. Предикат для этого запис. след. образом:
+
Немного сложнее будет с вычитанием. Существует расширение, позволяющее добавлять отрицательные числа, но лектор не видит смысла его показывать, там всё ещё сложнее и запись ещё длиннее. Поэтому, функцию, которая производит вычитание, или хотя бы уменьшение на единицу... мы должны определить pred как функцию, возвращающую предыдущее число или если 0 то 0. Для этого мы должны уметь определять, является ли число нулём. Предикат для этого записывается следующим образом:
iszero=λn.n(λx.FALSE)TRUE
iszero=λn.n(λx.FALSE)TRUE
Попробуем раскрыть его для нуля:
Попробуем раскрыть его для нуля:
iszero 0 → 0(λx.FALSE)TRUE → (λfx.x)(λx.FALSE)TRUE → TRUE
iszero 0 → 0(λx.FALSE)TRUE → (λfx.x)(λx.FALSE)TRUE → TRUE
-
Легко проверить, что если бы вместо x было бы хотя бы fx, то получилось бы FALSE. Обр. внимание, как произв. вычисления: вычилсения произв. через функцию, перед. в аргументе.
+
Легко проверить, что если бы вместо x было бы хотя бы fx, то получилось бы FALSE. Обратите внимание, как производятся вычисления: вычисления производятся через функцию, передаваему в аргументе.
В случае pred мы можем записать его как
В случае pred мы можем записать его как
Строка 87: Строка 91:
Это определение наиболее очевидно.
Это определение наиболее очевидно.
-
Таким обр., имея нумерала Чёрча, мы не тр. от языка налич. арифметики, тем не менее, обычно она есть, дабы вычисл. работали быстрее.
+
Таким образом, имея нумералы Чёрча, мы не требуем от языка наличия арифметики, тем не менее, обычно она есть, дабы вычисления работали быстрее.
-
Далее, списки. Мы говорили, что λ-исчисл это также способ моделир. структур данных. Попробуем смоделировать пару чисел.
+
Далее, списки. Мы говорили, что λ-исчисление это также способ моделирования структур данных. Попробуем смоделировать пару чисел.
Определим пару как:
Определим пару как:
PAIR=λxyf.fxy
PAIR=λxyf.fxy
-
Что даёт это определение: если мы определим пару из двух чисел, которую мы потом будем исп, то редуц. это след. образом:
+
Что даёт это определение: если мы определим пару из двух чисел, которую мы потом будем использовать, то редуцируется это следующим образом:
PAIR 4 2 →β λf.f 4 2
PAIR 4 2 →β λf.f 4 2
-
Это функция, которая, в зависимости от того, какой арг. вы подадите, выдаёт первый элемент или второй (в терминах лиспа - car/cdr)
+
Это функция, которая, в зависимости от того, какой аргумент вы подадите, выдаёт первый элемент или второй (в терминах лиспа - car/cdr)
CAR=FIRST=λp.p TRUE
CAR=FIRST=λp.p TRUE
CDR = SND = λp.p FALSE
CDR = SND = λp.p FALSE
Строка 101: Строка 105:
SND(PAIR 4 2) → (λp.p FALSE)(PAIR 4 2) → (PAIR 4 2)FALSE → (λf.f 4 2) FALSE → FALSE 4 2 → 2
SND(PAIR 4 2) → (λp.p FALSE)(PAIR 4 2) → (PAIR 4 2)FALSE → (λf.f 4 2) FALSE → FALSE 4 2 → 2
-
С исп. пары можем определить лисповский список. Что это такое? Это пара, где первый элемент это элемент, а второй — указатель на вторую пару такого же вида, где второй элемент тоже указатель на пару, где второй элемент — nil.
+
С использованием пары можем определить лисповский список. Что это такое? Это пара, где первый элемент это элемент, а второй — указатель на вторую пару такого же вида, где второй элемент тоже указатель на пару, где второй элемент — nil.
-
В лиспе конструктор списка — cons, первый элемент списка — car, получение хвоста списка — cdr. Также существует функция isnull, которая возвр. T, если список пуст.
+
В лиспе конструктор списка — cons, первый элемент списка — car, получение хвоста списка — cdr. Также существует функция isnull, которая возвращает T, если список пуст.
(3 4 5)
(3 4 5)
Строка 115: Строка 119:
car = λx.FIRST(SND x)
car = λx.FIRST(SND x)
cdr = &lamda;x.SND(SND x)
cdr = &lamda;x.SND(SND x)
-
Это уже можно исп. как список.
+
Это уже можно использовать как список.
-
Не хватает одного эл-та Тьюринг-полного языка — цикла. Наиболее рпостым методом, с т. з. лектора, явл. рекурсия. Как её организовать? Всё тот же Хаскел Карри решил исп. опр. неподвижной точки. Неподвижная точка — такая точка из обл. опр. функции, что значение функции в этой точке развно этой точке.
+
Не хватает одного элемента Тьюринг-полного языка — цикла. Наиболее простым методом, с т.з. лектора, является рекурсия. Как её организовать? Всё тот же Хаскел Карри решил использовать определение неподвижной точки. Неподвижная точка — такая точка из области определения функции, что значение функции в этой точке развно этой точке.
x — НТ f(x): x ∈ D(f), f(x) = x
x — НТ f(x): x ∈ D(f), f(x) = x
Строка 123: Строка 127:
λf(λx.f(xx))(λx.f(xx)) — Y-комбинатор
λf(λx.f(xx))(λx.f(xx)) — Y-комбинатор
-
Вообще говоря, комбинаторов неподв. точки чущ. очень много. Для примера лектор напишет только один, написанный Аланом Тьюрингом:
+
Вообще говоря, комбинаторов неподвижной точки существует очень много. Для примера лектор напишет только один, написанный Аланом Тьюрингом:
(λx.λy.(y(xxy)))(λx.λy.(y(xxy)))
(λx.λy.(y(xxy)))(λx.λy.(y(xxy)))
-
Общее св-во этих комбинаторов одно: у них есть некоторая часть, которая повт. Св-во на саомм деле, если мы попр. раск. комб. и подст. функцию, то его можно записать след. обазом:
+
Общее свойство этих комбинаторов одно: у них есть некоторая часть, которая повторяется. Свойство на самом деле, если мы попробуем раскодировать комбинацию и подставить функцию, то его можно записать следующим обазом:
Для некоторого ∀a∈Λ Ya=a(Ya)
Для некоторого ∀a∈Λ Ya=a(Ya)
-
Как это исп. для рекурсии? Попр. записать опр. факториала:
+
Как это использовать для рекурсии? Попробуем записать определение факториала:
n! = 1, если n=0; n(n-1)!
n! = 1, если n=0; n(n-1)!
-
Для опр. факт. требуется цикл. Опр. функцию итерация факториала:
+
Для определения факториала требуется цикл. Определим функцию итерация факториала:
IFACT=λf.λn.if(iszero n) 1 (mult n (f (pred n)))
IFACT=λf.λn.if(iszero n) 1 (mult n (f (pred n)))
после чего вычислим
после чего вычислим
(Y IFACT)5 = IFACT (Y IFACT) 5
(Y IFACT)5 = IFACT (Y IFACT) 5
-
Таким обр. мы можем видеть что аппара λ-исчисл. явл. Тьюринг-полным, несмотря на то, что мы не имеем переменных, не имеем ..., орг. всё мы можем.
+
Таким образом мы можем видеть что аппарат λ-исчисления является Тьюринг-полным, несмотря на то, что мы не имеем переменных, не имеем ..., организуем всё мы можем.
-
Так как ф. языки осн. на λ-исчисл, а в λ-исчисл. аппаратом для орг. итеративных выч. исп. рекурсия, то она же исп. и для ФЯП.
+
Так как функциональные языки основываются на λ-исчислении, а в λ-исчислении аппаратом для организации итеративных вычислений используется рекурсия, то она же используется и для ФЯП.
{{Haskell}}
{{Haskell}}
{{Lection-stub}}
{{Lection-stub}}

Текущая версия

TRUE=λab.a
FALSE=λab.b
IF=λcab.cab

IF FALSE 1 0 → (λcab.cab) FALS 1 0 →β (λab.FALSE a b) 1 0 → (λab.(λab.b)ab) 1 0 →α (λ ab(λxy.y)ab) 1 0 →→β (λab.b) 1 0 →→β 0

AND=λab.aba OR=λab.aab NOT=λcab.cba

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

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

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

TRUE 1 L

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

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

(λab.a) 1 L →β 1

2) TRUE 1 (λx.xx)(λx.xx) →β и тут мы зациклились.

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


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

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

MN ⇒ 1) M, 2) N

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

(λx.M)N ⇒ 1) (λx.M)N 2) M, N

Если мы здесь используем определение формальной системы, где есть эта конверсия (η: λx.Mx ⇒ M), то все эти конверсии происх. после β-редукции, в конце.

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

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

В языке haskell if можно определить следующим образом:

if :: Bool → a → a → a
if true a b = a
if false a b = b

В первой строчке задаются типы выражений. Тип Bool можно определить следующим образом:

data Bool = True | False

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

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

Определим 0 как FALSE для удобства.

0 = FALSE = λfx.x
1 = λfx.fx
2 = λfx.f(fx)
...
n = λfx.f(...f(fx)...)

Теперь определим арифметику.

add = λmnfx.mf(nfx)
succ=λnfx.f(nfx)
mlt=λmnf.m(nf)
exp=λmn.nm

легко проверить, что

add 3 2

и

5=λfx.f(f(f(f(fx)))))

эквивалентны.

Немного сложнее будет с вычитанием. Существует расширение, позволяющее добавлять отрицательные числа, но лектор не видит смысла его показывать, там всё ещё сложнее и запись ещё длиннее. Поэтому, функцию, которая производит вычитание, или хотя бы уменьшение на единицу... мы должны определить pred как функцию, возвращающую предыдущее число или если 0 то 0. Для этого мы должны уметь определять, является ли число нулём. Предикат для этого записывается следующим образом:

iszero=λn.n(λx.FALSE)TRUE

Попробуем раскрыть его для нуля:

iszero 0 → 0(λx.FALSE)TRUE → (λfx.x)(λx.FALSE)TRUE → TRUE

Легко проверить, что если бы вместо x было бы хотя бы fx, то получилось бы FALSE. Обратите внимание, как производятся вычисления: вычисления производятся через функцию, передаваему в аргументе.

В случае pred мы можем записать его как

pred=λn.n(λgk. iszero(g 1) k (add (gk) 1)) (λv.0)0

Наконец, вычитание

sub=λmn.n PRED m

Это определение наиболее очевидно.

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

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

Определим пару как:

PAIR=λxyf.fxy

Что даёт это определение: если мы определим пару из двух чисел, которую мы потом будем использовать, то редуцируется это следующим образом:

PAIR 4 2 →β λf.f 4 2

Это функция, которая, в зависимости от того, какой аргумент вы подадите, выдаёт первый элемент или второй (в терминах лиспа - car/cdr)

CAR=FIRST=λp.p TRUE
CDR = SND = λp.p FALSE
SND(PAIR 4 2) → (λp.p FALSE)(PAIR 4 2) → (PAIR 4 2)FALSE → (λf.f 4 2) FALSE → FALSE 4 2 → 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 = λx.x
cons = λxy.PAIR FALSE (PAIR xy)
isnull = FIRST
car = λx.FIRST(SND x)
cdr = &lamda;x.SND(SND x)

Это уже можно использовать как список.

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

x — НТ f(x): x ∈ D(f), f(x) = x

Комбинатор:

λf(λx.f(xx))(λx.f(xx)) — Y-комбинатор

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

(λx.λy.(y(xxy)))(λx.λy.(y(xxy)))

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

Для некоторого ∀a∈Λ Ya=a(Ya)

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

Для определения факториала требуется цикл. Определим функцию итерация факториала:

IFACT=λf.λn.if(iszero n) 1 (mult n (f (pred n)))

после чего вычислим

(Y IFACT)5 = IFACT (Y IFACT) 5

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

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


Теория функционального программирования. Язык Haskell


00 01 02 03 04 05 06 07 08 09 10 11 12


Календарь

Сентябрь
23 28
Октябрь
05 12 19 26
Ноябрь
02 09 16 23 30
Декабрь
07 14


Эта статья является конспектом лекции.

Эта статья ещё не вычитана. Пожалуйста, вычитайте её и исправьте ошибки, если они есть.
Личные инструменты
Разделы