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

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

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

Базовый комбинатор - базовый заранее определённый объект, не содержащий ююю переменных, декларирующий правила комбинирования объектов друг с другом и представляемый как правило вида: 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);
}

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

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