Мне пришлось реализовать функцию map haskell для работы с церковными списками, которые определены следующим образом:
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
У меня нет идеи, как это решение работает, и я не знаю, как создать такую функцию. У меня уже есть опыт исчисления лямбды и церковных цифр, но это упражнение было большой головной болью для меня, и я должен уметь понимать и решать такие проблемы для своего экзамена на следующей неделе. Может кто-то, пожалуйста, дайте мне хороший источник, где я мог бы научиться решать такие проблемы или дать мне небольшое руководство о том, как это работает?