Редактирование: Haskell, 03 лекция (от 12 октября)

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

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

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

Текущая версия Ваш текст
Строка 3: Строка 3:
* '''Видеозапись:''' 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 ⇒ ac=bc
# a=b ⇒ ac=bc
-
Набор аксиом — набор базисных комбинаторов. Базисов существует бесконечное множество, это доказывается
+
Набор аксиом — набор базисных комбинаторов. Базисов сущ. беск. множество, это доказывается
K= λxy.x Kxy=x
K= λ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
-
Для того, чтобы выражать λ-выражения через комбинаторы, сущ. 6 простых правил:
+
Для того, чтобы выр. λ-выражения через комб., сущ. 6 простых правил:
-
# Переменная: T[x] = x (для того, чтобы показать, что мы не закончили трансформацию, используется обозначение T[])
+
# Переменная: T[x] = x (для того, чтобы показать, что мы не закончили трансформ., исп. обозначение T[])
# Аппликация: T[(MN)] = T[M]T[N]
# Аппликация: T[(MN)] = T[M]T[N]
-
# Абстракция: T[λxM]. Тут есть несколько вариантов:
+
# Абстракция: T[λxM]. Тут есть неск. вариантов:
-
#* λx.M: x∉ FV(M), тогда (λx.M)a = M, то есть, мы отменим аргумент. Это то, что делает канцеллятор: (KT[M])a = T[M]
+
#* λx.M: x∉ FV(M), тогда (λx.M)a = M, то есть, мы отм. аргумент. Это то, что делает канцеллятор: (KT[M])a = T[M]
#: T[λx.M] = (KT[M]), X∉ FV(M)
#: T[λx.M] = (KT[M]), X∉ FV(M)
# λx.x = I = SKK
# λx.x = I = SKK
Строка 50: Строка 50:
#: T[λx.(MN)] = (ST[λx.M]T[λx.N])
#: T[λx.(MN)] = (ST[λx.M]T[λx.N])
-
Этих правил достаточно, чтобы привести в комбинаторную логику любой λ-терм.
+
Этих правил дост., чтобы привести в комб. логику любой λ-терм.
-
Эквивалентность в одну сторону показали, в другую сторону тривиально.
+
Экв в одну сторону показали, в другую сторону тривиально.
-
Базис из двух комбинаторов. Не является минимально возможным, но он является достаточно удобным. Можно привести пример базиса из одного комбинатора, через который выражается всё остальное:
+
Базис из двух комб. Не явл. мин. возм., но он явл. дост. удобным. Можно привести пример базиса из одного комбинатора, через который выраж. всё остальное:
X=λx(xKSK)
X=λx(xKSK)
Строка 63: Строка 63:
S=X(XX)
S=X(XX)
-
Другим важным свойством является возможность выполнения итеративных вычислений.
+
Другим важным св-вом явл. возм. выполн. итеративные выч.
-
В прошлый раз мы говорили про неподвижные точки. Они пришли из комбинаторики и были предложены Карри.
+
В прошлый раз мы гвоорили про функ. неподв. точки. Она пришла из комб. и была предложена Карри.
-
Что такое неподвижная точка? Это x∈D(f) такое, что f(x)=x
+
Что такое неподв. точка? Это x∈D(f) такое, что f(x)=x
-
В комбинаторной логике это немного другое, это такой терм, что M: ∀F: MF=F(MF)
+
В комб. логике это немного другое, это такой терм, что M: ∀F: MF=F(MF)
-
'''Теорема'''. Неподвижная точка существует для любого терма.
+
Такая точка сущ., сущ. теорема, что неподв. точка сущ. для люього терма.
-
'''Доказательство'''. Построим комбинатор вида W = λx.F(xx) и выберем комбинатор вида V=WW, преобразуем его, получим V=WW=(λx.F(xx))W = F(WW) = F(V)
+
Док-ва. Построим комб. вида W = λx.F(xx) и выберем комб. вида V=WW, преобр. его, получим V=WW=(λx.F(xx))W = F(WW) = F(V)
-
Эту теорему удалось доказать раньше, чем выразить первый парадокс комбинаторов Карри — это комбинатор вида Y=S(BWB)(BWB), который является неподвижной точкой для любой комбинаторной функции.
+
Эту теорему удал. докащать раньше, чем выр. первый пардокс. комб. Карри .это комб. вида Y=S(BWB)(BWB), который явл. неподв. для любой комб. функции.
-
Если нам для чего-либо было бы удобно использовать комбинаторную логику, то построенный язык на λ-исчислении, мы могли бы легко производить конвертацию из одного в другое. Такое преобразование имеет хотя бы одно практическое применение: реализация ленивой редукции.
+
Если нам для чего-либоы было бы удобно исп. комб. логику, то постр. язык на λ-исчисл., мы могли бы легко произв. конверт. из одного в другое Такое преобр. имеет хотя бы одно практ. применение: реализация ленивой редукции.
-
Что такое ленивой редукция? Ленивая редукция стр. — редукция стр., вбирающая в себя положительные черты обеих.
+
Что такое ленивой редукция? Ленивая ред. стр. — ред. стр., вбирающая в себя положительные черты обеих.
-
Для начала, усл. правила перевода, добавим несколько правил:
+
Для начала, усл. правила перевода, добавим неск. правил:
-
# Для начала скажем, что последнее, 6-е правило, которое выглядит следующим образом: T[λx.(MN)] = (ST[λx.M]T[λx.N]), действительно только в одном случае: оно действительно только в случае, когда x входит свободно как в M, так и в N: x ∈ FV(M) ∩ FV(N). Для других случаев мы будем более специфичны.
+
# Для начала скажем, что последнее, 6-е правило, которое выгл. след. образом: T[λx.(MN)] = (ST[λx.M]T[λx.N]), действ. только в одном случае: оно дейст. только в случае, когда x входит свободно как в M, так и в N: x ∈ FV(M) ∩ FV(N). Для других случаев мы будем более специфичны.
## x ∈ FV(M), x ∉ FV(N): (CT[λx.M]T[N])
## x ∈ FV(M), x ∉ FV(N): (CT[λx.M]T[N])
## x ∈ FV(N), x ∉ FV(M): (BT[M]T[λx.N])
## x ∈ FV(N), x ∉ FV(M): (BT[M]T[λx.N])
-
Таким образом, мы получаем выражение λ-исчисления в немного более широком базисе. Этот базис состоит не только из SK, но и из B и C.
+
Т. о. мы получаем выр. λ-исчисл. в немнгого более широком базисе. Этот базис сост. не только из SK, но и из B и C.
-
Как мы это используем? Попробуем применить:
+
Как мы это исп.? Попробуем применить:
(λf.f2)(λn(add nn))
(λf.f2)(λn(add nn))
(λn(add nn))2 ⇒ add 2 2
(λn(add nn))2 ⇒ add 2 2
-
При этом если у нас будет не 2, а более сложное выражение, ты мы его будем вычислять два раза. Попробуем перевести выражение в базис KSBC:
+
При этом если у нас будет не 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
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
Строка 99: Строка 99:
η: λx.Mx = M
η: λx.Mx = M
-
Тот же человек, который спрашивал про альтернативную запись T/F, спрашивал, можно ли записать NOT = λx. IF x FALSE TRUE, и тогда можно избавиться от IF, но почему это можно сделать?
+
Тот же человек, который спрашивал про альт. запись T/F, спрашивал, можно ли записать NOT = λx. IF x FALSE TRUE, и тогда можно избавиться от IF, но почме это можно сделать?
: IF = λcab.cab ⇒ (λc(λa(b(ca)b)))
: IF = λcab.cab ⇒ (λc(λa(b(ca)b)))
η⇒ (λc(λa ca)) = λcc
η⇒ (λc(λa ca)) = λcc
Строка 107: Строка 107:
Естественно, при реализации логику и арифметику делают аппаратными.
Естественно, при реализации логику и арифметику делают аппаратными.
-
Как устроен вызов функции в C: (картинка)
+
Как устроен вызов функции в C: (rfhnbyrf)
int f(char c)
int f(char c)
Строка 117: Строка 117:
}
}
-
При этом можно использовать хвостовую рекурсию, не кладя всё на стек, а просто переписав возвращаемое значение.
+
При этом можно исп хвостовую рекурсию, не кладя всё на стек, а просто переписав возр. зн.
При этом, если есть побочные эффекты, то сделать это не удастся.
При этом, если есть побочные эффекты, то сделать это не удастся.

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!


Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.us/wiki/Haskell%2C_03_%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F_%28%D0%BE%D1%82_12_%D0%BE%D0%BA%D1%82%D1%8F%D0%B1%D1%80%D1%8F%29
Личные инструменты
Разделы