3622
правки
Изменения
→Кр2: добавлен разбор кр2
* [https://pp.vk.me/c625826/v625826822/9174/QRhQIqwNX5Q.jpg]
Разбор будет по фоткам 3, 4 и , 5 (остальные задания аналогичны):
== N1. Порядок редуцирования ==
Лего проверить, что fst (pair a b) = a, подставив и сделав редукции.
== E1. Превратить let-биндинги в один большой лямбда-терм. ==
Конструкция
'''let''' x = z '''in''' y
превращается в
(\x . y) z
А пример просто превратится в
(\foo. [main]) [foo]
где [foo] {{---}} тело foo, [main] {{---}} тело main.
== E2. let-биндинги но с возможной взаимной рекурсией ==
):
== 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. Закодировать типы по Чёрчу (без взаимной рекурсии) ==
<code>
'''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)
</code>
=== Решение ===
У каждого типа есть <tex> N \geqslant 1</tex> конструктов, а у каждого конструктора есть <tex> K \geqslant 0 </tex> аргументов.
Фиксируем тип с <tex> N </tex> конструкторами. Каждый конструктор <tex> C_i </tex> этого типа превращается в абстракцию, в которой сначала идут <tex> K_i </tex> переменных {{---}} аргументы конструктора, а потом <tex> N </tex> переменных, отвечающих конструкторам. В теле просто выбирается нужный конструктор и применяется ко всем аргументам.
caseTypeName тоже является абстракцией, которая принимает сначала одну переменную, которая "выбирает" нужный конструктор, затем набор переменных в количестве числа конструкторов. В теле просто применяется первая переменная ко всем остальным.
<code>
<font color=green>-- сначала Doctor </font>
Minute = \ a . \ x y . x a
Maybe = \ a b c . \ x y . y a b c
caseDoctor = \ p . \ x y . p x y
<font color=green>-- теперь Hour </font>
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
</code>
Интересное наблюдение: переменная p в case является как раз нужным конструктором, в котором уже подставлены все аргументы этого конструктора.
== A2. Закодировать типы по Чёрчу (с взаимной рекурсией) ==
):
== H1. Написать Haskell-код какой-нибудь структуру данных ==
* [[АВЛ-дерево]]: [http://pastie.org/private/qbiu60aetjm9zrpqzrow ссылка на pastie]
*: почему я не знал Haskell, когда это дерево было в лабе по дискретке на первом курсе? ;( просто списывается с конспекта один в один...
* [[Квадродеревья | Квадродерево]]: [http://pastie.org/private/sf1vdmrpe7ifvqgdongwq ссылка на pastie]
*: не совсем то, что требует Ян, но я пока не распарсил то, что он требует; возможно, более правильная версия появится позже
=Кр3=
=Кр4=
