В этой статье я попробую показать соотвествие между между математическими доказательствами и программами, а так же попытаюсь ненавязчиво ввести читателя в синтаксис Agda.
И да, эта статья тоже будет типо DRAFT и я ее буду дополнять.
Эта статья будет публичной, но в статусе DRAFT, скорее всего я буду ее дополнять и пересматривать, пока тут какие-то базовые определения и доказательство того, что у (λx.xx)(λx.xx) нет нормальной формы. Скорее всего тут есть некоторые неточности и даже ошибки, буду исправлять в процессе.
В этой статье решаю задачу основанную на меме от Max Howell(создатель Homebrew), которого на собеседовании в Google заставляли инвертировать бинарное дерево, но он почему-то не смог
Google: 90% of our engineers use the software you wrote (Homebrew), but you can’t invert a binary tree on a whiteboard so fuck off.
Max Howell не смог, но я верю, что вы сможете! Рекомендую решать самостоятельно.