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: (rfhnbyrf)

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

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

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