Мне пришлось реализовать функцию haskell map для работы с церковными списками, которые определены следующим образом:
type Churchlist t u = (t->u->u)->u->u
В лямбда-исчислении списки кодируются следующим образом:
[] := λc. λn. n
[1,2,3] := λc. λn. c 1 (c 2 (c 3 n))
Пример решения этого упражнения:
mapChurch :: (t->s) -> (Churchlist t u) -> (Churchlist s u)
mapChurch f l = \c n -> l (c.f) n
Я понятия не имею, как работает это решение, и я не знаю, как создать такую функцию. У меня уже есть опыт работы с лямбда-исчислением и церковными числительными, но это упражнение стало для меня большой головной болью, и я должен быть в состоянии понять и решить такие задачи к экзамену на следующей неделе. Может ли кто-нибудь дать мне хороший источник, где я мог бы научиться решать такие проблемы, или дать мне небольшое руководство о том, как это работает?