http://neerc.ifmo.ru/wiki/api.php?action=feedcontributions&user=109.167.205.10&feedformat=atomВикиконспекты - Вклад участника [ru]2024-03-28T09:16:15ZВклад участникаMediaWiki 1.30.0http://neerc.ifmo.ru/wiki/index.php?title=%D0%A4%D1%83%D0%BD%D0%BA%D1%86%D0%B8%D0%BE%D0%BD%D0%B0%D0%BB%D1%8C%D0%BD%D0%BE%D0%B5_%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D0%B5&diff=45798Функциональное программирование2015-04-26T20:18:21Z<p>109.167.205.10: /* Целые числа */</p>
<hr />
<div>=Кр1=<br />
==Убрать все сокращения и расставить все скобки==<br />
(λ a b . (λ c d e . e) a) (x y) y (λ f . x) y<br />
<br />
=== Решение ===<br />
Скобки ставятся по следующим правилам:<br />
* тело абстракции заключается в скобки: λ x . M <tex> \Rightarrow </tex> λ x . (M)<br />
* аппликация левоассоциативна: a b c d <tex> \Rightarrow </tex> ((a b) c) d<br />
* сокращения раскрываются во вложенные лямбды (сразу с расставлением скобок): λ a b c . M <tex> \Rightarrow </tex> λ a . (λ b . (λ c . (M)))<br />
Важно: тело абстракции забирает всё до конца той скобки, в которую заключена.<br />
<br />
Итого: ((((λ a . (λ b . ((λ c . (λ d . (λ e . (e)))) a))) (x y)) y) (λ f . (x))) y<br />
<br />
==Привести в нормальную форму==<br />
<br />
λ a b . a (λ c . b c) a (λ d . d) a<br />
<br/><br />
λ a . (λ b . y) (λ c . y (y (λ d . a a a)) (x x) a)<br />
<br />
=== Решение ===<br />
В нормальной форме нет редукций. Если нормальная форма существует, то её можно достичь при помощи редукций нормальным порядком, а аппликативным можно и не достичь.<br />
<br />
# Уже в нормальное форме, как ни странно<br />
# λ a . y<br />
<br />
==Нормальный порядок редукции==<br />
(λ a . y (y (y (λ b . a))) y) (x (x (x (λ c d . d) y)) x)<br />
<br />
[http://softoption.us/content/node/46 Здесь] про стратегии редуцирования с примерами и определениями.<br />
<br />
'''Нормальный порядок редуцирования''' {{---}} сначала раскрывается самый левый самый внешний редекс.<br />
Пример не очень удачный, так в нём всего одна редукция, после которой получится: y (y (y (λ b . (x (x (x (λ c d . d) y)) x)))) y<br />
<br />
Более показательные и содержательные примеры (во всех случаях одна редукция будет произведена):<br />
* (λ a . a) ((λ x . x) y) <tex> \Rightarrow </tex> (λ x . x) y<br />
* x (λ a . ((λ x . x) y) ((λ z . z) y)) <tex> \Rightarrow </tex> x (λ a . y ((λ z . z) y))<br />
<br />
==Аппликативный порядок редукции==<br />
[http://pv.bstu.ru/flp/fpLectures.pdf Здесь] ещё про стратегии редуцирования, но немного другим языком (может быть, кому-то более понятным).<br />
<br />
'''Аппликативный порядок редуцирования''' {{---}} первым делом редуцируем самый левый самый глубокий терм. То есть сначала упрощаем "аргументы" аппликации.<br />
<br />
Те же примеры (во всех случаях одна редукция будет произведена):<br />
* (λ a . a) ((λ x . x) y) <tex> \Rightarrow </tex> (λ a . a) y<br />
* x (λ a . ((λ x . x) y) ((λ z . z) y)) <tex> \Rightarrow </tex> x (λ a . ((λ x . x) y) y)<br />
Ещё один для разнообразия:<br />
((λ x . y) (λ z . t)) ((λ a b c . a b c ((λ s . t) y) (λ t . x) u) (λ x . x)) ((λ x . x x) z) <tex> \Rightarrow </tex><br />
((λ x . y) (λ z . t)) ((λ a b c . a b c ((λ s . t) y) (λ t . x) u) (λ x . x)) (z z)<br />
<br />
==Выписать систему уравнений типизации==<br />
(λ a . a a) (λ b c . c)<br />
<br />
=== Решение ===<br />
Сначала надо дать типы всем термам и подтермам, раздавая каждый раз новые буквы новым переменным и термам. А потом связать эти буквы по следующим правилам:<br />
* если у нас абстракция (λ x . M) :: T0, x :: T1, M :: T2, то добавляем в систему T0 = T1 -> T2,<br />
* если имеем аппликацию (M N) :: T0, M :: T1, N :: T2, то добавляем T1 = T2 -> T0<br />
* если у нас переменная в теле абстракции встречается несколько раз и мы раздаём каждый раз ей новые буквы, то надо будет потом приравнять типы в аргументе абстракции и внутри её тела.<br />
<br />
Итого:<br />
<br />
(λ a . a a) (λ b c . c) :: A<br />
<br />
(λ a . a a) :: B, (λ b c . c) :: C<br />
<br />
a :: D, (a a) :: E<br />
<br />
первая и вторая буквы "a" в E {{---}} a :: F, a :: G<br />
<br />
Можем сразу расписать часть системы уравнений:<br />
<br />
B = C -> A<br />
<br />
B = D -> E<br />
<br />
F = G -> E<br />
<br />
D = F<br />
<br />
D = G<br />
<br />
Теперь расписываем терм с типом C (раскрыв сокращения для начала): (λ b . (λ c . c)) :: С<br />
<br />
b :: H, (λ c . c) :: I<br />
<br />
c :: J, c :: K<br />
<br />
И добавляем уравнения:<br />
<br />
C = H -> I<br />
<br />
I = J -> K<br />
<br />
J = K<br />
<br />
==Кодирование по Чёрчу==<br />
Выписать кайнды конструкторов типов, выписать типы конструкторов, закодировать по Чёрчу:<br />
<br />
data Policeman a = Doctor a | Mice<br />
<br/><br />
data Tree a b c = Frog c | Pip (Tree a b c)<br />
<br />
Этого задания не было в первой кр, поэтому оно будет расписано во второй. Вместо него была система уравнений типов чуть более адовая, чем в прошлом примере.<br />
<br />
=Кр2=<br />
==Фотки==<br />
* [https://pp.vk.me/c625522/v625522095/bb5e/DJapJCj1SGE.jpg]<br />
* [https://pp.vk.me/c625522/v625522095/bb68/OwKD9uzHoA8.jpg]<br />
* [https://pp.vk.me/c622826/v622826349/bfc5/atAYCtU1zZI.jpg]<br />
* [https://pp.vk.me/c622826/v622826349/bfcf/FvqIHdp-Dmw.jpg]<br />
* [https://pp.vk.me/c622826/v622826349/bfd9/uMwr0U0rfrI.jpg]<br />
* [https://pp.vk.me/c622820/v622820834/92be/d-3b04La1JQ.jpg]<br />
* [https://pp.vk.me/c622820/v622820834/92c8/UUa3Pn9hASM.jpg]<br />
* [https://pp.vk.me/c625826/v625826822/9142/uc_MHBKBJv4.jpg]<br />
* [https://pp.vk.me/c625826/v625826822/914c/-bzSn1_q6YI.jpg]<br />
* [https://pp.vk.me/c625826/v625826822/9156/gULmjYE46fY.jpg]<br />
* [https://pp.vk.me/c625826/v625826822/9160/8s4as7q7uKA.jpg]<br />
* [https://pp.vk.me/c625826/v625826822/916a/2US214bNwv0.jpg]<br />
* [https://pp.vk.me/c625826/v625826822/9174/QRhQIqwNX5Q.jpg]<br />
<br />
Разбор будет по фоткам 3, 4, 5 (остальные задания аналогичны):<br />
<br />
== N1. Порядок редуцирования ==<br />
См. прошлую кр<br />
<br />
== E0. Определить примитивные конструкции == <br />
<br />
pair = \ x y p . p x y<br />
fst = \ r . r (\ x y . x)<br />
snd = \ r . r (\ x y . y)<br />
fix = \ f . (\ x . f (x x)) (\ x . f (x x))<br />
<br />
Легко проверить, что fst (pair a b) = a, подставив и сделав редукции.<br />
<br />
== E1. Превратить let-биндинги в один большой лямбда-терм. ==<br />
<br />
Конструкция <br />
<br />
'''let''' x = z '''in''' y<br />
<br />
превращается в <br />
<br />
(\x . y) z <br />
<br />
А пример просто превратится в <br />
<br />
(\foo. [main]) [foo]<br />
<br />
где [foo] {{---}} тело foo, [main] {{---}} тело main.<br />
<br />
== E2. let-биндинги, но с возможной взаимной рекурсией ==<br />
<br />
foo = foo ((\ a . bar) foo)<br />
<br />
bar = (\ a . y) y (\ b . y)<br />
<br />
main = (\ a . foo (a z) (y y)) y<br />
<br />
=== Решение ===<br />
<font color=magenta> '''Осторожно! Магия''' </font><br />
<br />
Расписывать формальный алгоритм довольно нудно и неприятно, поэтому здесь объяснение того, что происходит, а на примере должно быть понятно.<br />
<br />
Сначала по каждому терму из условия надо составить терм с таким же именем, только штрихованный. В нём мы будем использовать первые буквы остальных термов. Фиксируем порядок аргументов, например для foo' это будет f b m. Тогда у всех остальных термов будет циклический порядок. То есть для bar' будет b m f, а для main' {{---}} m f b.<br />
<br />
Теперь пишем foo'. Сначала используем fix. Потом абстракцию, аргументами которой является нужный набор из циклических перестановок (см. соответствие выше), а телом абстракции является тело foo с изменениями. Если встречается имя терма из задания, то надо его заменить на нужный циклический порядок. И если имена первых букв по каким-то причинам не подходят (коллизятся со связанными переменными), то надо более удачные имена этим переменным придумать.<br />
<br />
Итого, после преобразований:<br />
<br />
foo' = fix (\ f b m . f b m ((\ a . b m f) (f b m)))<br />
bar' = fix (\ b m f . (\ a . y) y (\ b . y))<br />
main' = fix (\ m f b . (\ a . f b m (a z) (y y)) y)<br />
<br />
Результирующий терм выглядит как вызов штрихованной функции в нужной циклической перестановке:<br />
<br />
main = main' foo' bar'<br />
<br />
Но так как в этом задании дополнительные термы использовать нельзя, то main', foo', bar' надо проинлайнить в main.<br />
<br />
== N2. Раскрыть, как в E1 и нормализовать ==<br />
<br />
В общем, в задании всё сказано. Надо превратить в один большой терм как в E1, а затем нормализовать, как в задании из первой кр.<br />
<br />
== S1. Расписать систему уравнений типов ==<br />
<br />
Как в первой кр.<br />
<br />
== TP1. Убрать сокращения и расставить скобки ==<br />
<br />
Именно это и требуется сделать. Разве что там вместо тела абстракции расписан её тип. А (->) в типе в отличие от аппликации правоассоциативна, то есть в <br />
<br />
a -> b -> c<br />
<br />
скобки ставятся следующим образом:<br />
<br />
a -> (b -> c)<br />
<br />
Итого:<br />
* дано: (\ a b . b -> b -> a) x<br />
* получается: (\ a . (\ b . b -> (b -> a))) x // вроде бы тут как раз весь тип внутри не надо заключать в скобки<br />
<br />
== TF1. Составить терм по типу ==<br />
<br />
Тут надо пользоваться логикой. Вроде бы во всех примерах можно решить методом пристального взгляда. Мотивация: чтобы решение системы уравнений типов совпадало с полученным типом. Но в некоторых случаях довольно трудно (или даже невозможно) придумать терм по типу, например здесь не придумывается:<br />
<br />
(a -> b) -> b -> a<br />
<br />
=== Решение ===<br />
<br />
Дано: forall a b c . (b -> c -> a) -> (c -> b) -> c -> a<br />
<br />
Ответ: \f g c . f (g c) c<br />
<br />
== A1. Закодировать типы по Чёрчу (без взаимной рекурсии) ==<br />
<br />
<code><br />
'''data''' Doctor a = Minute a | Maybe a a a<br />
'''data''' Hour a b = Hour (Hour b b) (Doctor a) (Doctor b) | Roll b (Doctor a)<br />
</code><br />
<br />
=== Решение ===<br />
У каждого типа есть <tex> N \geqslant 1</tex> конструктов, а у каждого конструктора есть <tex> K \geqslant 0 </tex> аргументов. <br />
<br />
Фиксируем тип с <tex> N </tex> конструкторами. Каждый конструктор <tex> C_i </tex> этого типа превращается в абстракцию, в которой сначала идут <tex> K_i </tex> переменных {{---}} аргументы конструктора, а потом <tex> N </tex> переменных, отвечающих конструкторам. В теле просто выбирается нужный конструктор и применяется ко всем аргументам.<br />
<br />
caseTypeName тоже является абстракцией, которая принимает сначала одну переменную, которая "выбирает" нужный конструктор, затем набор переменных в количестве числа конструкторов. В теле просто применяется первая переменная ко всем остальным.<br />
<br />
<code><br />
<font color=green>-- сначала Doctor </font><br />
Minute = \ a . \ x y . x a<br />
Maybe = \ a b c . \ x y . y a b c<br />
caseDoctor = \ p . \ x y . p x y<br />
<font color=green>-- теперь Hour </font><br />
Hour = \ a b c . \ x y . x a b c<br />
Roll = \ a b . \ x y . y a b<br />
caseHour = \ p . \ x y . p x y<br />
</code><br />
<br />
Интересное наблюдение: переменная p в case является как раз нужным конструктором, в котором уже подставлены все аргументы этого конструктора.<br />
<br />
== A2. Закодировать типы по Чёрчу (с взаимной рекурсией) ==<br />
<br />
'''data''' Return a b = List (Return b a) (Return b a) b | Roll (Return a a) (Return a a) (Mice a)<br />
'''data''' Mice a = Bucket (Mice a) (Return a a) | Haystack (Mice a) a<br />
<br />
=== Решение ===<br />
<br />
<font color=magenta> '''Магия как в E2!''' </font><br />
<br />
Опять делаем соотвествие между TypeName и TypeName'. Чтобы написать TypeName', необходимо преобразовать объявление дататипов по следующим правилам:<br />
* сначала идёт mu (это как fix, только для типов),<br />
* потом какая-нибудь уникальная буква для типа (например x для Return и y для Mice),<br />
* после точки абстракция, которая сначала принимает в качестве аргумента другую уникальную букву, а затем аргументами параметры типа,<br />
* T1 | T2 заменяется на T1 + T2,<br />
* T1 T2 заменяется на T1 <tex> \times </tex> T2,<br />
* параметры типа оставляем как есть,<br />
* если в конструкторе идёт наш тип, то пишем нашу уникальную букву, а затем уникальную букву другого типа, а если другой типа {{---}} наоборот; после чего параметры конструктора,<br />
* если тип не наш и не буковка параметр датайпа, и не принимает параметров (например Nothing), то пишем 1 вместо неё.<br />
<br />
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)<br />
Mice' = mu y . \ x . \ a . (y x a) <tex> \times </tex> (x y a a) | (y x a) <tex> \times </tex> a<br />
<br />
После этого пишем ответ:<br />
<br />
Return = Return' Mice'<br />
Mice = Mice' Return'<br />
<br />
== H1. Написать Haskell-код какой-нибудь структуру данных ==<br />
<br />
* [[АВЛ-дерево]]: [http://pastie.org/private/qbiu60aetjm9zrpqzrow ссылка на pastie]<br />
*: почему я не знал Haskell, когда это дерево было в лабе по дискретке на первом курсе? ;( просто списывается с конспекта один в один...<br />
* [[Квадродеревья | Квадродерево]]: [http://pastie.org/private/sf1vdmrpe7ifvqgdongwq ссылка на pastie]<br />
*: не совсем то, что требует Ян, но я пока не распарсил то, что он требует; возможно, более правильная версия появится позже<br />
<br />
=Кр3=<br />
===ITMOPrelude===<br />
#gromakovsky<br />
#* [https://github.com/gromakovsky/haskell-course-ru/blob/master/ITMOPrelude/Primitive.hs Primitive.hs]<br />
#* [https://github.com/gromakovsky/haskell-course-ru/blob/master/ITMOPrelude/List.hs List.hs]<br />
# yakupov<br />
#* [https://github.com/yakupov/Haskell_lab/blob/master/ITMOPrelude/Primitive.hs Primitive.hs]<br />
#* [https://github.com/yakupov/Haskell_lab/blob/master/ITMOPrelude/List.hs List.hs]<br />
# itanf<br />
#* [https://github.com/itanf/ITMO-Training-FunctionalProgramming/blob/master/ITMOPrelude/Primitive.hs Primitive.hs]<br />
#* [https://github.com/itanf/ITMO-Training-FunctionalProgramming/blob/master/ITMOPrelude/List.hs List.hs]<br />
==Натуральные числа==<br />
data Nat = Zero | Succ Nat deriving (Show,Read) <font color=green>-- Определение натуральных чисел</font><br />
natZero = Zero <font color=green>-- 0</font><br />
natOne = Succ Zero <font color=green>-- 1</font><br />
<br />
natCmp :: Nat -> Nat -> Tri <font color=green>-- Сравнивает два натуральных числа</font><br />
natCmp Zero Zero = EQ<br />
natCmp Zero (Succ _) = LT<br />
natCmp (Succ _) Zero = GT<br />
natCmp (Succ n) (Succ m) = natCmp n m<br />
<br />
natEq :: Nat -> Nat -> Bool <font color=green>-- n совпадает с m</font><br />
natEq Zero Zero = True<br />
natEq Zero (Succ _) = False<br />
natEq (Succ _) Zero = False<br />
natEq (Succ n) (Succ m) = natEq n m<br />
<br />
natLt :: Nat -> Nat -> Bool <font color=green>-- n меньше m</font><br />
natLt Zero Zero = False<br />
natLt Zero (Succ m) = True<br />
natLt (Succ n) Zero = False<br />
natLt (Succ n) (Succ m) = natLt n m<br />
<br />
infixl 6 +. <font color=green>-- Сложение для натуральных чисел</font><br />
(+.) :: Nat -> Nat -> Nat<br />
Zero +. m = m<br />
(Succ n) +. m = Succ (n +. m)<br />
<br />
infixl 6 -. <font color=green>-- Вычитание для натуральных чисел</font><br />
(-.) :: Nat -> Nat -> Nat<br />
Zero -. _ = Zero<br />
n -. Zero = n<br />
(Succ n) -. (Succ m) = n -. m<br />
<br />
infixl 7 *. <font color=green>-- Умножение для натуральных чисел</font><br />
(*.) :: Nat -> Nat -> Nat<br />
Zero *. m = Zero<br />
(Succ n) *. m = m +. (n *. m)<br />
<br />
natDivMod :: Nat -> Nat -> Pair Nat Nat <font color=green>-- Целое и остаток от деления n на m</font><br />
natDivMod n m =<br />
if (n natLt m)<br />
then Pair Zero n<br />
else Pair (Succ div) mod where Pair div mod = ((n -. m) natDivMod m)<br />
<br />
natDiv n = fst . natDivMod n <font color=green>-- Целое</font><br />
natMod n = snd . natDivMod n <font color=green>-- Остаток</font><br />
<br />
==Целые числа==<br />
data Int = Plus Nat | Minus Nat deriving (Show,Read)<br />
<br />
intZero = Plus Zero<br />
intOne = Plus (Succ Zero)<br />
intNegOne = Minus (Succ Zero)<br />
<br />
intNeg :: Int -> Int<br />
intNeg (Plus x) = Minus x<br />
intNeg (Minus x) = Plus x<br />
<br />
intCmp :: Int -> Int -> Tri<br />
intCmp (Plus Zero) (Minus Zero) = EQ<br />
intCmp (Minus Zero) (Plus Zero) = EQ<br />
intCmp (Plus Zero) (Minus (Succ x)) = GT<br />
intCmp (Minus Zero) (Plus (Succ x)) = LT<br />
intCmp (Plus (Succ x)) (Minus Zero) = GT<br />
intCmp (Minus (Succ x)) (Plus Zero) = LT<br />
intCmp (Plus x) (Plus y) = natCmp x y<br />
intCmp (Minus x) (Minus y) = natCmp y x<br />
<br />
intEq :: Int -> Int -> Bool<br />
intEq (Plus Zero) (Minus Zero) = True<br />
intEq (Minus Zero) (Plus Zero) = True<br />
intEq (Plus Zero) (Minus (Succ x)) = False<br />
intEq (Minus Zero) (Plus (Succ x)) = False<br />
intEq (Plus (Succ x)) (Minus Zero) = False<br />
intEq (Minus (Succ x)) (Plus Zero) = False<br />
intEq (Plus x) (Plus y) = natEq x y<br />
intEq (Minus x) (Minus y) = natEq x y<br />
<br />
intLt :: Int -> Int -> Bool<br />
intLt (Plus Zero) (Minus Zero) = False<br />
intLt (Minus Zero) (Plus Zero) = False<br />
intLt (Plus Zero) (Minus (Succ x)) = False<br />
intLt (Minus Zero) (Plus (Succ x)) = True<br />
intLt (Plus (Succ x)) (Minus Zero) = False<br />
intLt (Minus (Succ x)) (Plus Zero) = True<br />
intLt (Plus x) (Plus y) = natLt x y<br />
intLt (Minus x) (Minus y) = natLt y x<br />
<br />
infixl 6 .+., .-.<br />
(.+.) :: Int -> Int -> Int<br />
(Plus m) .+. (Plus n) = Plus (m +. n)<br />
(Minus m) .+. (Minus n) = Minus (m +. n)<br />
(Plus (Succ m)) .+. (Minus (Succ n)) = (Plus m) .+. (Minus n)<br />
(Minus (Succ m)) .+. (Plus (Succ n)) = (Plus n) .+. (Minus m)<br />
x .+. (Plus Zero) = x<br />
x .+. (Minus Zero) = x<br />
(Plus Zero) .+. y = y<br />
(Minus Zero) .+. y = y<br />
<br />
(.-.) :: Int -> Int -> Int<br />
n .-. m = n .+. (intNeg m)<br />
<br />
infixl 7 .*.<br />
(.*.) :: Int -> Int -> Int<br />
(Plus m) .*. (Plus n) = Plus (m *. n)<br />
(Minus m) .*. (Minus n) = Plus (m *. n)<br />
(Plus m) .*. (Minus n) = Minus (m *. n)<br />
(Minus m) .*. (Plus n) = Minus (m *. n)<br />
<br />
==Рациональные числа==<br />
data Rat = Rat Int Nat<br />
<br />
ratNeg :: Rat -> Rat<br />
ratNeg (Rat x y) = Rat (intNeg x) y<br />
<br />
ratInv :: Rat -> Rat<br />
ratInv (Rat (Plus x) y) = Rat (Plus y) x<br />
ratInv (Rat (Minus x) y) = Rat (Minus y) x<br />
<br />
ratCmp :: Rat -> Rat -> Tri<br />
ratCmp (Rat a b) (Rat c d) = intCmp (a .*. (Plus d)) (c .*. (Plus b))<br />
<br />
ratEq :: Rat -> Rat -> Bool<br />
ratEq (Rat a b) (Rat c d) = intEq (a .*. (Plus d)) (c .*. (Plus b))<br />
<br />
ratLt :: Rat -> Rat -> Bool<br />
ratLt (Rat a b) (Rat c d) = intEq (a .*. (Plus d)) (c .*. (Plus b))<br />
<br />
internalRatPlus :: Rat -> Rat -> Rat<br />
internalRatPlus (Rat a b) (Rat c d) = Rat ((a .*. (Plus d)) .+. (c .*. (Plus b))) (b *. d)<br />
<br />
internalRatShorten :: Rat -> Rat<br />
internalRatShorten (Rat (Plus a) b) = Rat (Plus (a /. (gcd a b))) (b /. (gcd a b))<br />
internalRatShorten (Rat (Minus a) b) = Rat (Minus (a /. (gcd a b))) (b /. (gcd a b))<br />
<br />
infixl 7 %+, %-<br />
(%+) :: Rat -> Rat -> Rat<br />
n %+ m = internalRatShorten (internalRatPlus n m)<br />
<br />
(%-) :: Rat -> Rat -> Rat<br />
n %- m = n %+ (ratNeg m)<br />
<br />
infixl 7 %*, %/<br />
(%*) :: Rat -> Rat -> Rat<br />
(Rat a b) %* (Rat c d) = Rat (a .*. c) (b *. d)<br />
<br />
(%/) :: Rat -> Rat -> Rat<br />
n %/ m = n %* (ratInv m)<br />
<br />
==GCD==<br />
<br />
'''Тут я не уверен, можем ли использовать ''natMod'' или надо дополнительно реализовывать её.<br/>Ещё мы вроде бы не можем использовать дополнительные функции!'''<br />
<br />
gcd :: Nat -> Nat -> Nat<br />
gcd n Zero = n<br />
gcd n m = gcd m (natMod n m)<br />
<br />
==Метод Ньютона==<br />
==subsequences==<br />
subsequences :: List a -> List (List a)<br />
subsequences Nil = Cons Nil Nil<br />
subsequences xs = (subseqtoend xs) ++ (subseqtoend (init xs))<br />
where<br />
subseqtoend :: List a -> List (List a)<br />
subseqtoend Nil = Nil<br />
subseqtoend (Cons x xs) = (Cons (Cons x xs) (subseqtoend(xs)))<br />
<br />
==permutations==<br />
permutations :: List a -> List (List a)<br />
permutations Nil = Nil<br />
permutations (Cons x Nil) = (Cons (Cons x Nil) Nil)<br />
permutations (Cons x xs) = insertAtEveryPosForList (permutations xs) x<br />
where<br />
insertAtEveryPos :: List a -> a -> Nat -> List (List a)<br />
insertAtEveryPos str elem Zero = Cons (insert Zero elem Nil str) Nil<br />
insertAtEveryPos str elem pos = (insertAtEveryPos str elem (pos -. natOne)) ++ (Cons (insert pos elem Nil str) Nil)<br />
<br />
insertAtEveryPosForList :: List (List a) -> a -> List (List a)<br />
insertAtEveryPosForList (Cons x Nil) elem = insertAtEveryPos x elem (length x)<br />
insertAtEveryPosForList (Cons x xs) elem = (insertAtEveryPosForList xs elem) ++ (insertAtEveryPos x elem (length x))<br />
<br />
==А так же==<br />
* Дают тип какого-нибудь foldr и просят написать какой-нибудь foldr.<br />
* Написать определения каких-нибудь тайпклассов.<br />
* Написать какие-нибудь инстансы.<br />
* Доказать эквивалетность каких-нибудь двух определений монады.<br />
* CPS-преобразовать какие-нибудь типы.<br />
* Написать монадные инстансы для CPS-преобразованных типов.<br />
<br />
=Кр4=</div>109.167.205.10