Изменения

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

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

foo = foo ((\ a . bar)foo) bar = (\ a . y) y (\ b . y) main = (\ a . foo (a z) (y y)) y === Решение ===<font color=magenta> '''Осторожно! Магия''' </font> Расписывать формальный алгоритм довольно нудно и неприятно, поэтому здесь объяснение того, что происходит, а на примере должно быть понятно. Сначала по каждому терму из условия надо составить терм с таким же именем, только штрихованный. В нём мы будем использовать первые буквы остальных термов. Фиксируем порядок аргументов, например для 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.

== A2. Закодировать типы по Чёрчу (с взаимной рекурсией) через <tex> \mu </tex> - комбинатор ==

'''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 === Решение === <font color=magenta> '''Магия как в E2!''' </font> Опять делаем соотвествие между TypeName и TypeName'. Чтобы написать TypeName', необходимо преобразовать объявление дататипов по следующим правилам:* сначала идёт mu (это как fix, только для типов),* потом какая-нибудь уникальная буква для типа (например x для Return и y для Mice),* после точки абстракция, которая сначала принимает в качестве аргумента другую уникальную букву, а затем аргументами параметры типа,* T1 | T2 заменяется на T1 + T2,* T1 T2 заменяется на T1 <tex> \times </tex> T2,* параметры типа оставляем как есть,* если в конструкторе идёт наш тип, то пишем нашу уникальную букву, а затем уникальную букву другого типа, а если другой типа {{---}} наоборот; после чего параметры конструктора,* если тип не наш и не буковка параметр датайпа, и не принимает параметров (например Nothing), то пишем 1 вместо неё.  Return' = mu x . \ y . \ a b . (x y b a) <tex> \times </tex> (x y b a) <tex> \times </tex> b + (x y a a) <tex> \times </tex> (x y a a) <tex> \times </tex> (y x a) Mice' = mu y . \ x . \ a . (y x a) <tex> \times </tex> (x y a a) + (y x a) <tex> \times </tex> a После этого пишем ответ:  Return = Return' Mice' Mice = Mice' Return'

* [[АВЛ-дерево]]: [http://pastie.org/private/qbiu60aetjm9zrpqzrow ссылка на pastie]*: почему я не знал Haskell, когда это дерево было в лабе по дискретке на первом курсе? ;( просто списывается с конспекта один в один...* [[Квадродеревья | Квадродерево]]: [http://pastiepastebin.org/privatecom/sf1vdmrpe7ifvqgdongwq jV4DeRvv ссылка на pastiepastebin]

 ==Primitive=====Натуральные числаNat=== data Nat (+.) (-.) (*.)  divides :: Nat -> Nat -> Bool ===Rat=== data Rat (%+) (%-) (%*) (%/)  euler :: ? ==List== ===Угадайка===Дают тип, надо написать название функции из '''List.hs''' и реализовать её. ===Комбинаторика=== '''Тут можно использовать только набор заранее определённых функций листа( среди которых нет даже ''++'' )'''  subsequences :: [a] -> [ [ a ] ]  permutations :: [a] -> [ [ a ] ] ==Algebra== Zero 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 | Succ | 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 deriving ) 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 = (++) ==Categories==  class Category cat where id :: cat a a (.) :: cat b c -> cat a b -> cat a c class Functor f where fmap :: (a -> b) -> f a -> f b class Monad m where (>>=) :: m a -> (a -> m b) -> m b return :: a -> m a class (Functor f) => Applicative f where pure :: a -> f a (<*>) :: f (Showa -> b) -> f a -> f b class Functor m => MonadJoin m where returnJoin :: a -> m a join :: m (m a) -> m a data Identity a = Identity a runIdentity a = a instance Monad Identity where return x = Identity x (Identity x) >>= f = f x data Maybe a = Just a | Nothing instance Monad Maybe where Nothing >>= f = Nothing (Just x) >>= f = f x return x = Just x instance Monad [] where m >>= f = concat (map f m) return x = [x] class MonadFish m where returnFish :: a -> m a (>=>) :: (a -> m b) -> (b -> m c) -> (a -> m c) data State s r = State (s -> (r, s)) runState (State f) s = f s instance Monad (State s) where return r = State (\s -> (r,Reads)) (State x) <font color>>= f = State h where h s0 = let (r1, s1) = x s0 State g = f r1 (r2, s2) = g s1 in (r2, s2) newtype IdentityCPS a =greenIdentityCPS {runIdentityCPS :: forall r . (a -> r) ->r} caseIdentityCPS :: IdentityCPS a -> (a -> r) - Определение натуральных чисел</font>r natZero caseIdentityCPS = Zero <font color\x -> \f -> runIdentityCPS x f constrIdentityCPS :: a -> IdentityCPS a constrIdentityCPS =green\a ->IdentityCPS $ \f -> f a instance Functor IdentityCPS where fmap f ma = IdentityCPS $ \g -> caseIdentityCPS ma (\a - 0</font>g (f a)) natOne instance Applicative IdentityCPS where pure = Succ Zero constrIdentityCPS mf <font color*> ma = IdentityCPS $ \g -> caseIdentityCPS ma (\a -> caseIdentityCPS mf (\f -> g (f a ))) instance Monad IdentityCPS where return =greenconstrIdentityCPS ma >>= f = IdentityCPS $ \g -> caseIdentityCPS ma (\a - 1</font>runIdentityCPS (f a) g)

natCmp newtype MaybeCPS r a = MaybeCPS {runMaybeCPS :: Nat (a -> Nat r) -> Tri <font color=green>r -- Сравнивает два натуральных числа</font> natCmp Zero Zero = EQ natCmp Zero (Succ _) = LT natCmp (Succ _) Zero = GT natCmp (Succ n) (Succ m) = natCmp n mr}

natEq caseMaybeCPS :: Nat MaybeCPS r a -> Nat (a -> r) -> r -> Bool r <font colorcaseMaybeCPS =green\x ->\f -> \g - n совпадает с m</font> natEq Zero Zero = True natEq Zero (Succ _) = False natEq (Succ _) Zero = False natEq (Succ n) (Succ m) = natEq n mrunMaybeCPS x f g

natLt justCPS :: Nat a -> Nat -> Bool MaybeCPS r a <font colorjustCPS a =greenMaybeCPS $ \f ->\g -- n меньше m</font>f a natLt Zero Zero = Falsenothing :: MaybeCPS r a natLt Zero (Succ m) nothing = True natLt (Succ n) Zero = False natLt (Succ n) (Succ m) = natLt n mMaybeCPS $ \f -> \g -> g

infixl 6 +. <font colorinstance Functor (MaybeCPS r) where fmap f ma =greenMaybeCPS $ \g ->\h -- Сложение для натуральных чисел</font> caseMaybeCPS ma (+.) :: Nat -> Nat \a -> Nat Zero +. m = m g (Succ nf a) +. m = Succ (n +. m)h

infixl 6 -. instance Applicative (MaybeCPS r) where pure = justCPS mf <font color*> ma =greenMaybeCPS $ \g ->\h -- Вычитание для натуральных чисел</font> caseMaybeCPS ma (-.) :: Nat \a -> Nat caseMaybeCPS mf (\f -> Nat Zero -. _ = Zero n -. Zero = n (Succ ng $ f a) -. (Succ mh) = n -. mh

infixl 7 *instance Monad (MaybeCPS r) where return = justCPS ma >>= f = MaybeCPS $ \g -> \h -> caseMaybeCPS ma (\a -> runMaybeCPS (f a) g h) h newtype StateCPS s a = StateCPS {runStateCPS :: forall r . <font color=greens -> (s -> a -> r) -> r} caseStateCPS :: (StateCPS s a) -> ((s ->(s, a)) -> r) - Умножение для натуральных чисел</font>r caseStateCPS = \x -> \f -> f $ \s -> runStateCPS x s (\s -> \a -> (*.s, a)) state' :: Nat (s -> (s, a)) -> StateCPS s a state' st = StateCPS $ \s -> \f -> let (s', a) = st s in f s' a instance Functor (StateCPS s) where fmap f sa = StateCPS $ \s -> Nat \g -> NatcaseStateCPS sa (\st -> let (s', a) = st s in g s' (f a)) Zero instance Applicative (StateCPS s) where pure a = state' $ \s -> (s, a) sf <*. m > sa = StateCPS $ \s -> \g -> caseStateCPS sf (\stf -> let (s', f) = stf s in caseStateCPS sa (\sta -> let (s'', a) = Zerosta s' in g s'' (f a))) instance Monad (StateCPS s) where return a = state' $ \s -> (s, a) sa >>= f = StateCPS $ \s -> \g -> caseStateCPS sa (\sta -> let (s', a) = sta s in runStateCPS (f a) s' g) =Кр4=== deforestation ==Дана функция, необходимо её упростить, пользуясь техникой ''deforestation''. '''Мотивация:''' допустим, есть какая-то функция следующего вида: <code> foldl 0 (Succ n*) . filter (> 0) . map (\ x -> 3 *x - 10)</code> Первый map создаёт новый список, потом filter возвращает ещё список, и так далее. Если функций много (а их вполне может быть сколько угодно), то такой подход перестаёт быть эффективным. Идея в том, чтобы написать функцию, которая делает все необходимые действия "за раз": в данном примере можно рассматривать элемент списка, применять к нему функцию, потом проверять на условие в filter, а потом сразу считать произведение. Иногда можно посмотреть на композицию функций и придумать сразу оптимальный вариант. Это и требуется сделать во втором задании. Но можно и не думать, а применить стандартный алгоритм для преобразования, который даёт ответ. [http://www.sciencedirect.com/science/article/pii/030439759090147A По этой ссылке] описаны правила, по которым нужно преобразовывать функцию. Если коротко, то всё сводится к inline'у тел функций, причём мы хотим добиться отсутствия вызовов других функций на месте аргументов внешней функции (рекомендуется для начала почитать ссылку, посмотреть правила и пример оттуда). === Пример ===Будет разобран пример из [https://pp.vk.me/c622121/v622121192/ff98/NtvrRei7bR4. m jpg фото].  <code> <font color=green>-- дано</font> func = m foldr (+) 0 . map (n \x -> x *. m10)

natDivMod :: Nat -> Nat -> Pair Nat Nat <font color=green>-- Целое и остаток от деления n на mсначала перепишем композицию в обычную аппликацию для дальнейшей ясности</font> natDivMod n m func0 l = if foldr (n natLt m+) then Pair Zero n else Pair 0 (Succ div) mod where Pair div mod = map ((n \x -. m> x * 10) natDivMod ml)

natDiv n <font color=green>-- теперь инлайним foldr, то есть раскрываем его тело</font> func1 l = fst . natDivMod n '''case''' (map (\x -> x * 10) l) '''of''' [] -> 0 (x:xs) -> x + (foldr (+) 0 xs) <font color=green>-- а теперь инлайним map, заодно раскроем лямбду</font> func2 l = '''case''' ('''case''' l '''of''' [] -> [] (y:ys) -> y * 10 : map (*10) ys) '''of''' [] -> 0 (x:xs) -> x + (foldr (+) 0 xs) <font color=green>-- применяем преобразование case'a case'ов, то есть выносим внутренний case на первое место</font> 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)) <font color=green>-- Целоераскрываем внутренние case'ы: в них pattern-matching сразу срабатывает</font> natMod n func4 l = snd . natDivMod n '''case''' l '''of''' [] -> 0 (y:ys) -> 10 * y + (foldr (+) 0 (map (*10) ys)) <font color=green>-- Остатокзамечаем, что у нас получилось в конце выражение foldr (+) 0 (map (*10) ys), а это по сути наша функция func0, которую мы раскрывали изначально, поэтому тому куску можно дать другое имя</font> func5 l = '''case''' l '''of''' [] -> 0 (y:ys) -> 10 * y + func5 ys</code> == stream fusion == По сути это то же самое, только вводятся два дополнительных типа, а стандартные функции подстраиваются под них.* [http://code.haskell.org/~dons/papers/icfp088-coutts.pdf Статья]* [http://www2.tcs.ifi.lmu.de/~senjak/haskellbeatsc.pdf Презентация с красивым форматированием (мотивация)]* [http://www.mit.edu/~mtikekar/posts/stream-fusion.html Применение в реальной жизни]* [http://sprunge.us/ZONH Разбор задания с кр] == zippers and functions differentiation == Для каждой структуры данных (datatype'а) в Haskell можно составить соответствующий ей zipper: это другая структура данных, которая позволяет "гулять" по нашей структуре, взяв в фокус текущий элемент и запоминая при этом остальное состояние структуры данных (или контекст). Для списка легко придумывается zipper: мы находимся на какой-то позиции в списке, знаем значение элемента на этой позиции, знаем часть списка слева от текущего элемента и справа (для более глубокого понимания читай LearnYourHaskell). Поэтому zipper для списка имеет следующий вид: <code> '''data''' ZipperList a = ZList a [a] [a]</code> Но не для всех типов получается легко придумать zipper методом пристального взгляда. Чтобы составить zipper для произвольного типа без особых усилий, можно представить тип как функцию от параметра типа, а затем найти производную этого типа. Тогда если типу соответствует функция <tex> f(a) </tex>, то zipper выражается следующим образом: <tex> z(a) = a \cdot f'(a) </tex>. Рассмотрим внимательней типа List:<code> '''data''' List a = Nil | Cons a (List a)</code> Ему соотвествует следующее уравнение в функциях типов: <tex> f(a) = 1 + a \cdot f(a) </tex>. Если теперь продифференцировать обе части уравнения, то можно будет найти производную для списка. Обозначим список элементов типа <tex> x </tex> как <tex>L(x)</tex>. Из формулы для списка легко выражется, что <tex> L(x) = \dfrac{1}{1 - x} </tex>. Этим равенством будем пользоваться в дальнейшем. === Пример ===Найдём теперь zipper для какого-нибудь конкретного класса:<code> '''data''' Mice a = Haystack a (Mice a) a | Baboon (Mice a) | List' a a a</code> Запишем уравнение типа для него: <tex> f(a) = a \cdot f(a) \cdot a + f(a) + a \cdot a \cdot a \ (1)</tex>.  На самом деле порядок аргументов в типе не очень важен, мы сами его задаём, поэтому можно написать чуть более сокращенную запись:

<tex> f(a) ==Целые числа====Рациональные числа====GCD==a^2 \cdot f(a) + f(a) + a^3 </tex>

'''Тут я не уверенЗабудем на некоторое время, можем ли использовать ''natMod'' или надо дополнительно реализовывать еёчто мы работаем с типами.Продифференцируем обе части уравнение по переменной <tex> a <br/tex>Ещё мы вроде бы не можем использовать дополнительные функции!''', получим линейное уравнение относительно производной.

gcd :: Nat -<tex> Nat -> Nat gcd n Zero f'(a) = n gcd n m = gcd m 2a \cdot f(a) + a^2 \cdot f'(a) + f'(natMod n ma)+ 3a^2 </tex>

==Метод Ньютона====subsequences====permutations====А так же==* Дают тип какого-нибудь foldr Заметка: на этом надо остановиться и просят написать какой-нибудь foldr.* Написать определения каких-нибудь тайпклассов.* Написать какие-нибудь инстансы.* Доказать эквивалетность каких-нибудь двух определений монады.* CPS-преобразовать какие-нибудь типысоответствующий рекурсивный тип.* Написать монадные инстансы для CPS-преобразованных типовЗа дальнейшие действия будет сняты 0.5 баллов(ЯН: "слишком сложное решение")

<code> <font color=Кр4green>-- Итого ответ:</font> '''data''' DMice a =S a (Mice a) | H a (Mice a) | M a a (DMice a) | Y (DMice a) | A a a | K a a | Shmyak a a</code> Забавное, но бесполезное для сдачи ФП, продолжение: Выразим производную. <tex> f'(a) = \dfrac{2a \cdot f(a) + 3a^2}{1 - (a^2 + 1)} = (2a \cdot f(a) + 3a^2) \cdot \dfrac{1}{1 - (a^2 + 1)} \ (2)</tex> В итоге у нас производная является произведением двух функций, а для типа это значит, что он является произведением двух типов. При умножении на константу у нас будет просто несколько одинаковых конструкторов с разными именами.<code> <font color=green>--сначала распишем производную типа, полученного сразу после дифференцирования (1), если соблюдать исходный порядок аргументов в типах</font> '''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</code> Теперь распишем первую скобку в (2):<code> '''data''' DMice' = M1 a (Mice a) | M2 a (Mice a) | C1 a a | C2 a a | C3 a a</code> Дальше идёт дробь. Вспоминаем, что на самом деле ей отвечает тип <tex> L(a^2 + 1) </tex>.Поэтому получаем в итоге:<code> '''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)</code> * [http://learnyouahaskell.com/zippers LearnYourHaskell {{---}} Zippers]* [http://sprunge.us/HCDN Пример zipper'a из кр]