Функциональное программирование — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Кодирование по Чёрчу)
(Кр2)
Строка 117: Строка 117:
 
* [https://pp.vk.me/c625826/v625826822/916a/2US214bNwv0.jpg]
 
* [https://pp.vk.me/c625826/v625826822/916a/2US214bNwv0.jpg]
 
* [https://pp.vk.me/c625826/v625826822/9174/QRhQIqwNX5Q.jpg]
 
* [https://pp.vk.me/c625826/v625826822/9174/QRhQIqwNX5Q.jpg]
 +
 +
Разбор будет по фоткам 3 и 4 (остальные задания аналогичны):
 +
 +
== N1. Порядок редуцирования ==
 +
См. прошлую кр
 +
 +
== E0. Определить примитивные конструкции ==
 +
 +
* pair = \ x y p . p x y
 +
 
=Кр3=
 
=Кр3=
 
=Кр4=
 
=Кр4=

Версия 11:27, 26 апреля 2015

Кр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)

Решение

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

  1. Уже в нормальное форме, как ни странно
  2. λ b . 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)

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

(λ 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 (остальные задания аналогичны):

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

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

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

  • pair = \ x y p . p x y

Кр3

Кр4