Уходим в даун

В порядке самообразования решил поподробнее изучить λ-исчисление. Нашел несколько книжек и пр. Забавной показалась теорема о существовании неподвижной точки у любой функции. Решил "проверить", переписал Y-комбинатор из книжки на знакомом мне Haskell... Угу, фиг - его невозможно типизировать. Хотел было попробовать на Scheme, но сообразил, что типизация она и в scheme типизация. Тогда стал искать какой-нибудь язык, реализующий нетипизированное λ-исчисление, чтобы на нем можно было "поиграться" с примерами из книжек. Нашел только unlambda, который, как оказалось, реализует вовсе даже не лямбду, а комбинаторную логику, а синтаксис у него похож более всего на brainfuck. Вздохнул и решил писать что-то такое сам...

Вроде написал, и примеры из книжек на нем работают, но в сложных выражениях пока что вылезают баги при α-конверсии (переменные то переименуются, когда не надо, то наоборот). Надеюсь всё-таки допилить...

Подробности про язык тут, само поделие тут (Depends: python, python-ply; запускать ./pylambda.py в терминале).