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

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

Перейти к: навигация, поиск

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


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

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