Haskell, 03 лекция (от 12 октября)

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

(Различия между версиями)
Перейти к: навигация, поиск
(Новая: <!--* '''Презентация:''' http://haskell.secsem.ru/2010/Lectures?action=AttachFile&do=view&target=ТФП+--+Лекция+2.pdf--> * '''Аудиозапись:''' http://esyr.or...)
 
(1 промежуточная версия не показана)
Строка 1: Строка 1:
-
<!--* '''Презентация:''' http://haskell.secsem.ru/2010/Lectures?action=AttachFile&do=view&target=ТФП+--+Лекция+2.pdf-->
+
* '''Презентация:''' [[Media:ТФП -- Лекция 3.pdf]]
* '''Аудиозапись:''' http://esyr.org/lections/audio/haskell_2010_winter/haskell_10_10_12.ogg
* '''Аудиозапись:''' http://esyr.org/lections/audio/haskell_2010_winter/haskell_10_10_12.ogg
* '''Видеозапись:''' http://esyr.org/video/haskell/haskell_10_10_12.raw.ogv
* '''Видеозапись:''' http://esyr.org/video/haskell/haskell_10_10_12.raw.ogv
-
Базовый комбинатор - базовый заранее опред. объект, не содерж. ююю переменных, деклар. правила комбинирования объектов друг с другом и придст. как правило вида: Px_1..x_n = E
+
Базовый комбинатор - базовый заранее определённый объект, не содержащий ююю переменных, декларирующий правила комбинирования объектов друг с другом и представляемый как правило вида: Px_1..x_n = E
Формальная система - четвёрка (S, F, A, R)
Формальная система - четвёрка (S, F, A, R)
Строка 20: Строка 20:
# a=b &rArr; ac=bc
# a=b &rArr; ac=bc
-
Набор аксиом — набор базисных комбинаторов. Базисов сущ. беск. множество, это доказывается
+
Набор аксиом — набор базисных комбинаторов. Базисов существует бесконечное множество, это доказывается
K= &lambda;xy.x Kxy=x
K= &lambda;xy.x Kxy=x
Строка 33: Строка 33:
* Дубликатор: Wxy = xyy
* Дубликатор: Wxy = xyy
-
Возьмём базис KS. Покажем, что комбинация трёх комбинаторов SKK из этого бахиса предст. собой тождество.
+
Возьмём базис KS. Покажем, что комбинация трёх комбинаторов SKK из этого базиса представляет собой тождество.
SKK = I
SKK = I
(SKK)x = SKKx =S KxKx = KxKx = Kx = x = Ix
(SKK)x = SKKx =S KxKx = KxKx = Kx = x = Ix
-
Для того, чтобы выр. &lambda;-выражения через комб., сущ. 6 простых правил:
+
Для того, чтобы выражать &lambda;-выражения через комбинаторы, сущ. 6 простых правил:
-
# Переменная: T[x] = x (для того, чтобы показать, что мы не закончили трансформ., исп. обозначение T[])
+
# Переменная: T[x] = x (для того, чтобы показать, что мы не закончили трансформацию, используется обозначение T[])
# Аппликация: T[(MN)] = T[M]T[N]
# Аппликация: T[(MN)] = T[M]T[N]
-
# Абстракция: T[&lambda;xM]. Тут есть неск. вариантов:
+
# Абстракция: T[&lambda;xM]. Тут есть несколько вариантов:
-
#* &lambda;x.M: x&notin; FV(M), тогда (&lambda;x.M)a = M, то есть, мы отм. аргумент. Это то, что делает канцеллятор: (KT[M])a = T[M]
+
#* &lambda;x.M: x&notin; FV(M), тогда (&lambda;x.M)a = M, то есть, мы отменим аргумент. Это то, что делает канцеллятор: (KT[M])a = T[M]
#: T[&lambda;x.M] = (KT[M]), X&notin; FV(M)
#: T[&lambda;x.M] = (KT[M]), X&notin; FV(M)
# &lambda;x.x = I = SKK
# &lambda;x.x = I = SKK
Строка 50: Строка 50:
#: T[&lambda;x.(MN)] = (ST[&lambda;x.M]T[&lambda;x.N])
#: T[&lambda;x.(MN)] = (ST[&lambda;x.M]T[&lambda;x.N])
-
Этих правил дост., чтобы привести в комб. логику любой &lambda;-терм.
+
Этих правил достаточно, чтобы привести в комбинаторную логику любой &lambda;-терм.
-
Экв в одну сторону показали, в другую сторону тривиально.
+
Эквивалентность в одну сторону показали, в другую сторону тривиально.
-
Базис из двух комб. Не явл. мин. возм., но он явл. дост. удобным. Можно привести пример базиса из одного комбинатора, через который выраж. всё остальное:
+
Базис из двух комбинаторов. Не является минимально возможным, но он является достаточно удобным. Можно привести пример базиса из одного комбинатора, через который выражается всё остальное:
X=&lambda;x(xKSK)
X=&lambda;x(xKSK)
Строка 63: Строка 63:
S=X(XX)
S=X(XX)
-
Другим важным св-вом явл. возм. выполн. итеративные выч.
+
Другим важным свойством является возможность выполнения итеративных вычислений.
-
В прошлый раз мы гвоорили про функ. неподв. точки. Она пришла из комб. и была предложена Карри.
+
В прошлый раз мы говорили про неподвижные точки. Они пришли из комбинаторики и были предложены Карри.
-
Что такое неподв. точка? Это x&isin;D(f) такое, что f(x)=x
+
Что такое неподвижная точка? Это x&isin;D(f) такое, что f(x)=x
-
В комб. логике это немного другое, это такой терм, что M: &forall;F: MF=F(MF)
+
В комбинаторной логике это немного другое, это такой терм, что M: &forall;F: MF=F(MF)
-
Такая точка сущ., сущ. теорема, что неподв. точка сущ. для люього терма.
+
'''Теорема'''. Неподвижная точка существует для любого терма.
-
Док-ва. Построим комб. вида W = &lambda;x.F(xx) и выберем комб. вида V=WW, преобр. его, получим V=WW=(&lambda;x.F(xx))W = F(WW) = F(V)
+
'''Доказательство'''. Построим комбинатор вида W = &lambda;x.F(xx) и выберем комбинатор вида V=WW, преобразуем его, получим V=WW=(&lambda;x.F(xx))W = F(WW) = F(V)
-
Эту теорему удал. докащать раньше, чем выр. первый пардокс. комб. Карри .это комб. вида Y=S(BWB)(BWB), который явл. неподв. для любой комб. функции.
+
Эту теорему удалось доказать раньше, чем выразить первый парадокс комбинаторов Карри — это комбинатор вида Y=S(BWB)(BWB), который является неподвижной точкой для любой комбинаторной функции.
-
Если нам для чего-либоы было бы удобно исп. комб. логику, то постр. язык на &lambda;-исчисл., мы могли бы легко произв. конверт. из одного в другое Такое преобр. имеет хотя бы одно практ. применение: реализация ленивой редукции.
+
Если нам для чего-либо было бы удобно использовать комбинаторную логику, то построенный язык на &lambda;-исчислении, мы могли бы легко производить конвертацию из одного в другое. Такое преобразование имеет хотя бы одно практическое применение: реализация ленивой редукции.
-
Что такое ленивой редукция? Ленивая ред. стр. — ред. стр., вбирающая в себя положительные черты обеих.
+
Что такое ленивой редукция? Ленивая редукция стр. — редукция стр., вбирающая в себя положительные черты обеих.
-
Для начала, усл. правила перевода, добавим неск. правил:
+
Для начала, усл. правила перевода, добавим несколько правил:
-
# Для начала скажем, что последнее, 6-е правило, которое выгл. след. образом: T[&lambda;x.(MN)] = (ST[&lambda;x.M]T[&lambda;x.N]), действ. только в одном случае: оно дейст. только в случае, когда x входит свободно как в M, так и в N: x &isin; FV(M) &cap; FV(N). Для других случаев мы будем более специфичны.
+
# Для начала скажем, что последнее, 6-е правило, которое выглядит следующим образом: T[&lambda;x.(MN)] = (ST[&lambda;x.M]T[&lambda;x.N]), действительно только в одном случае: оно действительно только в случае, когда x входит свободно как в M, так и в N: x &isin; FV(M) &cap; FV(N). Для других случаев мы будем более специфичны.
## x &isin; FV(M), x &notin; FV(N): (CT[&lambda;x.M]T[N])
## x &isin; FV(M), x &notin; FV(N): (CT[&lambda;x.M]T[N])
## x &isin; FV(N), x &notin; FV(M): (BT[M]T[&lambda;x.N])
## x &isin; FV(N), x &notin; FV(M): (BT[M]T[&lambda;x.N])
-
Т. о. мы получаем выр. &lambda;-исчисл. в немнгого более широком базисе. Этот базис сост. не только из SK, но и из B и C.
+
Таким образом, мы получаем выражение &lambda;-исчисления в немного более широком базисе. Этот базис состоит не только из SK, но и из B и C.
-
Как мы это исп.? Попробуем применить:
+
Как мы это используем? Попробуем применить:
(&lambda;f.f2)(&lambda;n(add nn))
(&lambda;f.f2)(&lambda;n(add nn))
(&lambda;n(add nn))2 &rArr; add 2 2
(&lambda;n(add nn))2 &rArr; add 2 2
-
При этом если у нас будет не 2, а более сложное выр., ты мы его будем выч. два раза. Попробуем перевесмти выр. в базис KSBC:
+
При этом если у нас будет не 2, а более сложное выражение, ты мы его будем вычислять два раза. Попробуем перевести выражение в базис KSBC:
T[(&lambda;f.f2)(&lambda;n(add nn))] &rArr;(6.2) CT[&lambda;ff]2 T[&lambda;n(add n n)] &rArr;(4) C I 2T[&lambda;n((add n) n)] &rArr;(6.1) C I 2 (S T[&lambda;n add n]T[&lambda;n.n]) &rArr; C I 2 (S T[&lambda;n.add n] I
T[(&lambda;f.f2)(&lambda;n(add nn))] &rArr;(6.2) CT[&lambda;ff]2 T[&lambda;n(add n n)] &rArr;(4) C I 2T[&lambda;n((add n) n)] &rArr;(6.1) C I 2 (S T[&lambda;n add n]T[&lambda;n.n]) &rArr; C I 2 (S T[&lambda;n.add n] I
Строка 99: Строка 99:
&eta;: &lambda;x.Mx = M
&eta;: &lambda;x.Mx = M
-
Тот же человек, который спрашивал про альт. запись T/F, спрашивал, можно ли записать NOT = &lambda;x. IF x FALSE TRUE, и тогда можно избавиться от IF, но почме это можно сделать?
+
Тот же человек, который спрашивал про альтернативную запись T/F, спрашивал, можно ли записать NOT = &lambda;x. IF x FALSE TRUE, и тогда можно избавиться от IF, но почему это можно сделать?
: IF = &lambda;cab.cab &rArr; (&lambda;c(&lambda;a(b(ca)b)))
: IF = &lambda;cab.cab &rArr; (&lambda;c(&lambda;a(b(ca)b)))
&eta;&rArr; (&lambda;c(&lambda;a ca)) = &lambda;cc
&eta;&rArr; (&lambda;c(&lambda;a ca)) = &lambda;cc
Строка 107: Строка 107:
Естественно, при реализации логику и арифметику делают аппаратными.
Естественно, при реализации логику и арифметику делают аппаратными.
-
Как устроен вызов функции в C: (rfhnbyrf)
+
Как устроен вызов функции в C: (картинка)
int f(char c)
int f(char c)
Строка 117: Строка 117:
}
}
-
При этом можно исп хвостовую рекурсию, не кладя всё на стек, а просто переписав возр. зн.
+
При этом можно использовать хвостовую рекурсию, не кладя всё на стек, а просто переписав возвращаемое значение.
При этом, если есть побочные эффекты, то сделать это не удастся.
При этом, если есть побочные эффекты, то сделать это не удастся.

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

Базовый комбинатор - базовый заранее определённый объект, не содержащий ююю переменных, декларирующий правила комбинирования объектов друг с другом и представляемый как правило вида: Px_1..x_n = E

Формальная система - четвёрка (S, F, A, R)

  • S - алфавит, S={A-Z,a-z,(,)}

Множество термов: T_c=

  1. a-z - переменные
  2. A-Z - базовые комбинаторы
  3. M∈T_c, N∈T_c *rArr; (MN)∈T_c - комбинации комбинаторов

Св-ва комбинаторов:

  1. a=a
  2. a=b ⇒ b=a
  3. a=b, b=c ⇒ a=c
  4. a=b ⇒ ca=cb
  5. a=b ⇒ ac=bc

Набор аксиом — набор базисных комбинаторов. Базисов существует бесконечное множество, это доказывается

K= λxy.x Kxy=x
S=λxyz.xz(yz) Sxyz = xz(yz)

Комбинатор тождества: Ix=x

  • K — канцеллятор, он отменяет второй аргумент.
  • S — коннектор.
  • Композитор: Bxyz=x(yz)
  • Пермутатор: Сxyz = Cxzy
  • Дубликатор: Wxy = xyy

Возьмём базис KS. Покажем, что комбинация трёх комбинаторов SKK из этого базиса представляет собой тождество.

SKK = I
(SKK)x = SKKx =S KxKx = KxKx = Kx = x = Ix

Для того, чтобы выражать λ-выражения через комбинаторы, сущ. 6 простых правил:

  1. Переменная: T[x] = x (для того, чтобы показать, что мы не закончили трансформацию, используется обозначение T[])
  2. Аппликация: T[(MN)] = T[M]T[N]
  3. Абстракция: T[λxM]. Тут есть несколько вариантов:
    • λx.M: x∉ FV(M), тогда (λx.M)a = M, то есть, мы отменим аргумент. Это то, что делает канцеллятор: (KT[M])a = T[M]
    T[λx.M] = (KT[M]), X∉ FV(M)
  4. λx.x = I = SKK
  5. T[λx.λy.M] = T[λx.T[λy.M]], x∈FV(M)
  6. T[λx(MN)]
    • (λx.(MN))a = (λx.M)a((λx.N)a) = S (λx.M)(λx.N)a
    T[λx.(MN)] = (ST[λx.M]T[λx.N])

Этих правил достаточно, чтобы привести в комбинаторную логику любой λ-терм.

Эквивалентность в одну сторону показали, в другую сторону тривиально.

Базис из двух комбинаторов. Не является минимально возможным, но он является достаточно удобным. Можно привести пример базиса из одного комбинатора, через который выражается всё остальное:

X=λx(xKSK)

Для того, чтобы это показать, выразим любой другой базис, например, SK, через него:

K=(XX)X
S=X(XX)

Другим важным свойством является возможность выполнения итеративных вычислений.

В прошлый раз мы говорили про неподвижные точки. Они пришли из комбинаторики и были предложены Карри.

Что такое неподвижная точка? Это x∈D(f) такое, что f(x)=x

В комбинаторной логике это немного другое, это такой терм, что M: ∀F: MF=F(MF)

Теорема. Неподвижная точка существует для любого терма.

Доказательство. Построим комбинатор вида W = λx.F(xx) и выберем комбинатор вида V=WW, преобразуем его, получим V=WW=(λx.F(xx))W = F(WW) = F(V)

Эту теорему удалось доказать раньше, чем выразить первый парадокс комбинаторов Карри — это комбинатор вида Y=S(BWB)(BWB), который является неподвижной точкой для любой комбинаторной функции.

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

Что такое ленивой редукция? Ленивая редукция стр. — редукция стр., вбирающая в себя положительные черты обеих.

Для начала, усл. правила перевода, добавим несколько правил:

  1. Для начала скажем, что последнее, 6-е правило, которое выглядит следующим образом: T[λx.(MN)] = (ST[λx.M]T[λx.N]), действительно только в одном случае: оно действительно только в случае, когда x входит свободно как в M, так и в N: x ∈ FV(M) ∩ FV(N). Для других случаев мы будем более специфичны.
    1. x ∈ FV(M), x ∉ FV(N): (CT[λx.M]T[N])
    2. x ∈ FV(N), x ∉ FV(M): (BT[M]T[λx.N])

Таким образом, мы получаем выражение λ-исчисления в немного более широком базисе. Этот базис состоит не только из SK, но и из B и C.

Как мы это используем? Попробуем применить:

(λf.f2)(λn(add nn))
(λn(add nn))2 ⇒ add 2 2

При этом если у нас будет не 2, а более сложное выражение, ты мы его будем вычислять два раза. Попробуем перевести выражение в базис KSBC:

T[(λf.f2)(λn(add nn))] ⇒(6.2) CT[λff]2 T[λn(add n n)] ⇒(4) C I 2T[λn((add n) n)] ⇒(6.1) C I 2 (S T[λn add n]T[λn.n]) ⇒ C I 2 (S T[λn.add n] I

η: λx.Mx = M

Тот же человек, который спрашивал про альтернативную запись T/F, спрашивал, можно ли записать NOT = λx. IF x FALSE TRUE, и тогда можно избавиться от IF, но почему это можно сделать?

IF = λcab.cab ⇒ (λc(λa(b(ca)b)))
η⇒ (λc(λa ca)) = λcc

C I 2 (S T[λn.add n] I ⇒η C I 2(S add I)

Естественно, при реализации логику и арифметику делают аппаратными.

Как устроен вызов функции в C: (картинка)

int f(char c)
{
  if (c == 0)
    return 0;
  else
    return f(c - 1);
}

При этом можно использовать хвостовую рекурсию, не кладя всё на стек, а просто переписав возвращаемое значение.

При этом, если есть побочные эффекты, то сделать это не удастся.


Теория функционального программирования. Язык 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


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

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