Содержание

1 Кр1
2 Кр2
3 Кр3
4 Кр4

Кр1

Убрать все сокращения и расставить все скобки

(λ a b . (λ c d e . e) a) (x y) y (λ f . x) y

Решение

Скобки ставятся по следующим правилам:

тело абстракции заключается в скобки: λ x . M [math] \Rightarrow [/math] λ x . (M)
аппликация левоассоциативна: a b c d [math] \Rightarrow [/math] ((a b) c) d
сокращения раскрываются во вложенные лямбды (сразу с расставлением скобок): λ a b c . M [math] \Rightarrow [/math] λ a . (λ b . (λ c . (M)))

Важно: тело абстракции забирает всё до конца той скобки, в которую заключена.

Итого: ((((λ a . (λ b . ((λ c . (λ d . (λ e . (e)))) a))) (x y)) y) (λ f . (x))) y

Привести в нормальную форму

λ a b . a (λ c . b c) a (λ d . d) a
λ a . (λ b . y) (λ c . y (y (λ d . a a a)) (x x) a)

Решение

В нормальной форме нет редукций. Если нормальная форма существует, то её можно достичь при помощи редукций нормальным порядком, а аппликативным можно и не достичь.

Уже в нормальное форме, как ни странно
λ a . y

Нормальный порядок редукции

(λ a . y (y (y (λ b . a))) y) (x (x (x (λ c d . d) y)) x)

Здесь про стратегии редуцирования с примерами и определениями.

Нормальный порядок редуцирования — сначала раскрывается самый левый самый внешний редекс. Пример не очень удачный, так в нём всего одна редукция, после которой получится: y (y (y (λ b . (x (x (x (λ c d . d) y)) x)))) y

Более показательные и содержательные примеры (во всех случаях одна редукция будет произведена):

(λ a . a) ((λ x . x) y) [math] \Rightarrow [/math] (λ x . x) y
x (λ a . ((λ x . x) y) ((λ z . z) y)) [math] \Rightarrow [/math] x (λ a . y ((λ z . z) y))

Аппликативный порядок редукции

Здесь ещё про стратегии редуцирования, но немного другим языком (может быть, кому-то более понятным).

Аппликативный порядок редуцирования — первым делом редуцируем самый левый самый глубокий терм. То есть сначала упрощаем "аргументы" аппликации.

Те же примеры (во всех случаях одна редукция будет произведена):

(λ a . a) ((λ x . x) y) [math] \Rightarrow [/math] (λ a . a) y
x (λ a . ((λ x . x) y) ((λ z . z) y)) [math] \Rightarrow [/math] x (λ a . ((λ x . x) y) y)

Ещё один для разнообразия: ((λ x . y) (λ z . t)) ((λ a b c . a b c ((λ s . t) y) (λ t . x) u) (λ x . x)) ((λ x . x x) z) [math] \Rightarrow [/math] ((λ x . y) (λ z . t)) ((λ a b c . a b c ((λ s . t) y) (λ t . x) u) (λ x . x)) (z z)

Ленивый порядок редукции

Ленивый порядок редуцирования — это когда мы якобы заворачиваем терм в коробку, и если делаем редукцию в одном из термов коробки, то она делается во всех. При этом сам порядок редуцирования нормальный.

То есть пример:

(λ f . f f) ((λ x . x) z)

Сначала делаем обычную редукцию нормальным порядком и получаем:

((λ x . x) z) ((λ x . x) z)

А потом после редукции нормальным порядком надо сделать изменения сразу в двух термах, потому что они якобы в коробках, и получим суммарно за 2 редукции:

z z

Выписать систему уравнений типизации

(λ a . a a) (λ b c . c)

Решение

Сначала надо дать типы всем термам и подтермам, раздавая каждый раз новые буквы новым переменным и термам. А потом связать эти буквы по следующим правилам:

если у нас абстракция (λ x . M) :: T0, x :: T1, M :: T2, то добавляем в систему T0 = T1 -> T2,
если имеем аппликацию (M N) :: T0, M :: T1, N :: T2, то добавляем T1 = T2 -> T0
если у нас переменная в теле абстракции встречается несколько раз и мы раздаём каждый раз ей новые буквы, то надо будет потом приравнять типы в аргументе абстракции и внутри её тела.

Итого:

(λ a . a a) (λ b c . c) :: A

(λ a . a a) :: B, (λ b c . c) :: C

a :: D, (a a) :: E

первая и вторая буквы "a" в E — a :: F, a :: G

Можем сразу расписать часть системы уравнений:

B = C -> A

B = D -> E

F = G -> E

D = F

D = G

Теперь расписываем терм с типом C (раскрыв сокращения для начала): (λ b . (λ c . c)) :: С

b :: H, (λ c . c) :: I

c :: J, c :: K

И добавляем уравнения:

C = H -> I

I = J -> K

J = K

Кодирование по Чёрчу

Выписать кайнды конструкторов типов, выписать типы конструкторов, закодировать по Чёрчу:

data Policeman a = Doctor a | Mice
data Tree a b c = Frog c | Pip (Tree a b c)

Этого задания не было в первой кр, поэтому оно будет расписано во второй. Вместо него была система уравнений типов чуть более адовая, чем в прошлом примере.

Кр2

Фотки

Разбор будет по фоткам 3, 4, 5 (остальные задания аналогичны):

N1. Порядок редуцирования

См. прошлую кр

E0. Определить примитивные конструкции

pair = \ x y p . p x y
fst  = \ r . r (\ x y . x)
snd  = \ r . r (\ x y . y)
fix  = \ f . (\ x . f (x x)) (\ x . f (x x))

Легко проверить, что fst (pair a b) = a, подставив и сделав редукции.

E1. Превратить let-биндинги в один большой лямбда-терм.

Конструкция

let x = z in y

превращается в

(\x . y) z

А пример просто превратится в

(\foo. [main]) [foo]

где [foo] — тело foo, [main] — тело main.

E2. let-биндинги, но с возможной взаимной рекурсией

foo = foo ((\ a . bar) foo)

bar = (\ a . y) y (\ b . y)

main = (\ a . foo (a z) (y y)) y

Решение

Осторожно! Магия

Расписывать формальный алгоритм довольно нудно и неприятно, поэтому здесь объяснение того, что происходит, а на примере должно быть понятно.

Сначала по каждому терму из условия надо составить терм с таким же именем, только штрихованный. В нём мы будем использовать первые буквы остальных термов. Фиксируем порядок аргументов, например для foo' это будет f b m. Тогда у всех остальных термов будет циклический порядок. То есть для bar' будет b m f, а для main' — m f b.

Теперь пишем foo'. Сначала используем fix. Потом абстракцию, аргументами которой является нужный набор из циклических перестановок (см. соответствие выше), а телом абстракции является тело foo с изменениями. Если встречается имя терма из задания, то надо его заменить на нужный циклический порядок. И если имена первых букв по каким-то причинам не подходят (коллизятся со связанными переменными), то надо более удачные имена этим переменным придумать.

Итого, после преобразований:

foo'  = fix (\ f b m . f b m ((\ a . b m f) (f b m)))
bar'  = fix (\ b m f . (\ a . y) y (\ b . y))
main' = fix (\ m f b . (\ a . f b m (a z) (y y)) y)

Результирующий терм выглядит как вызов штрихованной функции в нужной циклической перестановке:

main = main' foo' bar'

Но так как в этом задании дополнительные термы использовать нельзя, то main', foo', bar' надо проинлайнить в main.

N2. Раскрыть, как в E1 и нормализовать

В общем, в задании всё сказано. Надо превратить в один большой терм как в E1, а затем нормализовать, как в задании из первой кр.

S1. Расписать систему уравнений типов

Как в первой кр.

TP1. Убрать сокращения и расставить скобки

Именно это и требуется сделать. Разве что там вместо тела абстракции расписан её тип. А (->) в типе в отличие от аппликации правоассоциативна, то есть в

a -> b -> c

скобки ставятся следующим образом:

a -> (b -> c)

Итого:

дано: (\ a b . b -> b -> a) x
получается: (\ a . (\ b . b -> (b -> a))) x // вроде бы тут как раз весь тип внутри не надо заключать в скобки

TF1. Составить терм по типу

Тут надо пользоваться логикой. Вроде бы во всех примерах можно решить методом пристального взгляда. Мотивация: чтобы решение системы уравнений типов совпадало с полученным типом. Но в некоторых случаях довольно трудно (или даже невозможно) придумать терм по типу, например здесь не придумывается:

(a -> b) -> b -> a

Решение

Дано: forall a b c . (b -> c -> a) -> (c -> b) -> c -> a

Ответ: \f g c . f (g c) c

A1. Закодировать типы по Чёрчу (без взаимной рекурсии)


 data Doctor a = Minute a | Maybe a a a
 data Hour a b = Hour (Hour b b) (Doctor a) (Doctor b) | Roll b (Doctor a)

Решение

У каждого типа есть [math] N \geqslant 1[/math] конструктов, а у каждого конструктора есть [math] K \geqslant 0 [/math] аргументов.

Фиксируем тип с [math] N [/math] конструкторами. Каждый конструктор [math] C_i [/math] этого типа превращается в абстракцию, в которой сначала идут [math] K_i [/math] переменных — аргументы конструктора, а потом [math] N [/math] переменных, отвечающих конструкторам. В теле просто выбирается нужный конструктор и применяется ко всем аргументам.

caseTypeName тоже является абстракцией, которая принимает сначала одну переменную, которая "выбирает" нужный конструктор, затем набор переменных в количестве числа конструкторов. В теле просто применяется первая переменная ко всем остальным.


 -- сначала Doctor 
 Minute = \ a . \ x y . x a
 Maybe  = \ a b c . \ x y . y a b c
 caseDoctor = \ p . \ x y . p x y
 -- теперь Hour 
 Hour = \ a b c . \ x y . x a b c
 Roll = \ a b . \ x y . y a b
 caseHour = \ p . \ x y . p x y

Интересное наблюдение: переменная p в case является как раз нужным конструктором, в котором уже подставлены все аргументы этого конструктора.

A2. Закодировать типы через [math] \mu [/math] - комбинатор

data Return a b = List (Return b a) (Return b a) b | Roll (Return a a) (Return a a) (Mice a)
data Mice a = Bucket (Mice a) (Return a a) | Haystack (Mice a) a

Решение

Магия как в E2!

Опять делаем соотвествие между TypeName и TypeName'. Чтобы написать TypeName', необходимо преобразовать объявление дататипов по следующим правилам:

сначала идёт mu (это как fix, только для типов),
потом какая-нибудь уникальная буква для типа (например x для Return и y для Mice),
после точки абстракция, которая сначала принимает в качестве аргумента другую уникальную букву, а затем аргументами параметры типа,
T1 | T2 заменяется на T1 + T2,
T1 T2 заменяется на T1 [math] \times [/math] T2,
параметры типа оставляем как есть,
если в конструкторе идёт наш тип, то пишем нашу уникальную букву, а затем уникальную букву другого типа, а если другой типа — наоборот; после чего параметры конструктора,
если тип не наш и не буковка параметр датайпа, и не принимает параметров (например Nothing), то пишем 1 вместо неё.

Return' = mu x . \ y . \ a b . (x y b a) [math] \times [/math] (x y b a) [math] \times [/math] b + (x y a a) [math] \times [/math] (x y a a) [math] \times [/math] (y x a)
Mice'   = mu y . \ x . \ a . (y x a) [math] \times [/math] (x y a a) + (y x a) [math] \times [/math] a

После этого пишем ответ:

Return = Return' Mice'
Mice   = Mice' Return'

H1. Написать Haskell-код какой-нибудь структуру данных

АВЛ-дерево: ссылка на pastebin
почему я не знал Haskell, когда это дерево было в лабе по дискретке на первом курсе? ;( просто списывается с конспекта один в один...
Квадродерево: ссылка на pastebin
не совсем то, что требует Ян, но я пока не распарсил то, что он требует; возможно, более правильная версия появится позже

Кр3

ITMOPrelude

Primitive

Nat

data Nat
(+.)
(-.)
(*.)

divides :: Nat -> Nat -> Bool

Rat

data Rat
(%+)
(%-)
(%*)
(%/)

euler :: ?

List

Угадайка

Дают тип, надо написать название функции из List.hs и реализовать её.

Комбинаторика

Тут можно использовать только набор заранее определённых функций листа( среди которых нет даже ++ )

subsequences :: [a] -> [ [ a ] ]

permutations :: [a] -> [ [ a ] ]

Algebra

class Monoid a where
	mempty :: a
	mappend :: a -> a -> a

class Monoid a => Group a where
	ginv :: a -> a

mconcat :: (Monoid a) => List a -> a
mconcat = foldr mappend mempty

instance Monoid Unit where
	mempty	  = Unit
	mappend _ _ = Unit

instance Group Unit where
	ginv _ = Unit

instance (Monoid a, Monoid b) => Monoid (Pair a b) where
	mempty	  = Pair mempty mempty
	mappend a b = Pair {fst = fst a `mappend` fst b,
						snd = snd b `mappend` snd b}

instance (Monoid a) => Monoid (Maybe a) where
	mempty					= Just mempty
	mappend (Just a) (Just b) = Just $ mappend a b
	mappend _ _			   = Nothing

newtype First a = First { getFirst :: Maybe a}

instance Monoid (First a) where
	mempty					= First Nothing
	mappend (First Nothing) x = x
	mappend x _			   = x

newtype Last a = Last { getLast :: Maybe a}

instance Monoid (Last a) where
	mempty				   = Last Nothing
	mappend x (Last Nothing) = x
	mappend _ x			  = x

newtype Any = Any { getAny :: Bool }

instance Monoid Any where
	mempty				  = Any False
	mappend (Any a) (Any b) = Any $ a || b

newtype All = All { getAll :: Bool }

instance Monoid All where
	mempty				  = All True
	mappend (All a) (All b) = All $ a && b

-- Лексикографическое сравнение
instance Monoid Tri where
	mempty	   = EQ
	mappend LT _ = LT
	mappend EQ a = a
	mappend GT _ = GT

newtype Sum a = Sum { getSum :: a }

instance Monoid (Sum Nat) where
	mempty				  = Sum natZero
	mappend (Sum a) (Sum b) = Sum $ a +. b

newtype Product a = Product { getProduct :: a }

instance Monoid (Product Nat) where
	mempty						  = Product natOne
	mappend (Product a) (Product b) = Product $ a *. b

instance Monoid (Sum Int) where
	mempty				  = Sum intZero
	mappend (Sum a) (Sum b) = Sum $ a .+. b

instance Group (Sum Int) where
	ginv = Sum . intNeg . getSum

instance Monoid (Product Int) where
	mempty						  = Product intOne
	mappend (Product a) (Product b) = Product $ a .*. b

instance Monoid (Sum Rat) where
	mempty				  = Sum ratZero
	mappend (Sum a) (Sum b) = Sum $ a %+ b

instance Group (Sum Rat) where
	ginv = Sum . ratNeg . getSum

instance Monoid (Product Rat) where
	mempty						  = Product ratOne
	mappend (Product a) (Product b) = Product $ a %* b

instance Group (Product Rat) where
	ginv = Product . ratInv . getProduct

instance Monoid (List a) where
	mempty = Nil
	mappend = (++)

Кр4

deforestation

Дана функция, необходимо её упростить, пользуясь техникой deforestation.

Мотивация: допустим, есть какая-то функция следующего вида:


 foldl 0 (*) . filter (> 0) . map (\ x -> 3 * x - 10)

Первый map создаёт новый список, потом filter возвращает ещё список, и так далее. Если функций много (а их вполне может быть сколько угодно), то такой подход перестаёт быть эффективным. Идея в том, чтобы написать функцию, которая делает все необходимые действия "за раз": в данном примере можно рассматривать элемент списка, применять к нему функцию, потом проверять на условие в filter, а потом сразу считать произведение. Иногда можно посмотреть на композицию функций и придумать сразу оптимальный вариант. Это и требуется сделать во втором задании. Но можно и не думать, а применить стандартный алгоритм для преобразования, который даёт ответ.

По этой ссылке описаны правила, по которым нужно преобразовывать функцию. Если коротко, то всё сводится к inline'у тел функций, причём мы хотим добиться отсутствия вызовов других функций на месте аргументов внешней функции (рекомендуется для начала почитать ссылку, посмотреть правила и пример оттуда).

Пример

Будет разобран пример из фото.


-- дано
func = foldr (+) 0 . map (\x -> x * 10)

-- сначала перепишем композицию в обычную аппликацию для дальнейшей ясности
func0 l = foldr (+) 0 (map (\x -> x * 10) l)




-- теперь инлайним foldr, то есть раскрываем его тело
func1 l = case (map (\x -> x * 10) l) of
               [] -> 0
               (x:xs) -> x + (foldr (+) 0 xs)               
         
-- а теперь инлайним map, заодно раскроем лямбду
func2 l = case (case l of
                     [] -> []
                     (y:ys) -> y * 10 : map (*10) ys) of
               [] -> 0
               (x:xs) -> x + (foldr (+) 0 xs)
               
-- применяем преобразование case'a case'ов, то есть выносим внутренний case на первое место
func3 l = case l of
               [] -> (case [] of
                           [] -> 0
                           (x:xs) -> x + (foldr (+) 0 xs))
               (y:ys) -> (case (y * 10 : map (*10) ys) of
                               [] -> 0
                               (x:xs) -> x + (foldr (+) 0 xs))
                                
-- раскрываем внутренние case'ы: в них pattern-matching сразу срабатывает
func4 l = case l of
               [] -> 0
               (y:ys) -> 10 * y + (foldr (+) 0 (map (*10) ys))
                
-- замечаем, что у нас получилось в конце выражение foldr (+) 0 (map (*10) ys), а это по сути наша функция func0, 
которую мы раскрывали изначально, поэтому тому куску можно дать имя другое имя
func5 l = case l of
               [] -> 0
               (y:ys) -> 10 * y + func5 ys

stream fusion

По сути это то же самое, только вводятся два дополнительных типа, а стандартные функции подстраиваются под них.

zippers and functions differentiation

Для каждой структуры данных (datatype'а) в Haskell можно составить соответствующий ей zipper: это другая структура данных, которая позволяет "гулять" по нашей структуре, беря в фокус текущий элемент, запоминая при этом остальное состание структуры данных (или контекст). Для списка легко придумывается zipper: мы находимся на какой-то позиции в списке, знаем значение элемента на этой позиции, знаем часть списка слева от текущего элемента и справа (для более глубокого понимания читай LearnYourHaskell). Поэтому zipper для листа имеет следующий вид:


data ZipperList a = ZList a [a] [a]

Но не для всех типов получается легко придумать zipper методом пристального взгляда. Чтобы уметь составить zipper для произвольного типа, можно представить тип как функцию от параметра типа, а затем найти производную этого типа. Тогда если типу соответствует функция [math] f(a) [/math], то zipper выражается следующим образом: [math] z(a) = a \cdot f'(a) [/math].

Рассмотрим внимательней типа List:


data List a = Nil | Cons a (List a)

Ему соотвествует следующее уравнение в функциях типов: [math] f(a) = 1 + a \cdot f(a) [/math]. Если теперь продифференцировать обе части уравнения, то можно будет найти производную для списка. Обозначим список элементов типа [math] x [/math] как [math]L(x)[/math]. Из формулы для списка легко выражется, что [math] L(x) = \dfrac{1}{1 - x} [/math]. Этим равенством будем пользоваться в дальнейшем.

Пример

Найдём теперь zipper для какого-нибудь конкретного класса:


data Mice a = Haystack a (Mice a) a | Baboon (Mice a) | List' a a a

Запишем уравнение типа для него: .

На самом деле порядок аргументов в типе не очень важен, мы сами его задаём, поэтому можно написать чуть более сокращенную запись:

Забудем на некоторое время, что мы работаем с типами. Продифференцируем обе части уравнение по переменной [math] a [/math], получим линейное уравнение относительно производной, а затем выразим её.

В итоге у нас производная является произведением двух функций, а для типа это значит, что он является произведением двух типов. При умножении на константу у нас будет просто несколько одинаковых конструкторов с разными именами, поэтому распишем типа для первой скобки:


--сначала распишем производную типа, полученного сразу после дифференцирования (1), если всё аккуратно раскрыть
data DMice a = S (Mice a) a | H a (DMice a) a | M a (Mice a) | Y (DMice a) | A a a | K a a | Shmyak a a

Теперь распишем первую скобку в (2):


 data DMice' = M1 a (Mice a) | M2 a (Mice a) | C1 a a | C2 a a | C3 a a

Дальше идёт дробь. Вспоминаем, что на самом деле ей отвечает тип [math] L(a^2 + 1) [/math]. Поэтому получаем в итоге:


data DMiceListElem a = DM1 a a | DM0
data DMiceList a = MNil | MCons (DMiceListElem a) (DMiceList a)
data ZMice a = ZMice a (DMice' a) (DMiceList a)

Функциональное программирование

Содержание

Кр1

Убрать все сокращения и расставить все скобки

Решение

Привести в нормальную форму

Решение

Нормальный порядок редукции

Аппликативный порядок редукции

Ленивый порядок редукции

Выписать систему уравнений типизации

Решение

Кодирование по Чёрчу

Кр2

Фотки

N1. Порядок редуцирования

E0. Определить примитивные конструкции

E1. Превратить let-биндинги в один большой лямбда-терм.

E2. let-биндинги, но с возможной взаимной рекурсией

Решение

N2. Раскрыть, как в E1 и нормализовать

S1. Расписать систему уравнений типов

TP1. Убрать сокращения и расставить скобки

TF1. Составить терм по типу

Решение

A1. Закодировать типы по Чёрчу (без взаимной рекурсии)

Решение

A2. Закодировать типы через [math] \mu [/math] - комбинатор

Решение

H1. Написать Haskell-код какой-нибудь структуру данных

Кр3

ITMOPrelude

Primitive

Nat

Rat

List

Угадайка

Комбинаторика

Algebra

Categories

Кр4

deforestation

Пример

stream fusion

zippers and functions differentiation

Пример

Навигация

Поиск