В порядке самообразования решил поподробнее изучить λ-исчисление. Нашел несколько книжек и пр. Забавной показалась теорема о существовании неподвижной точки у любой функции. Решил "проверить", переписал Y-комбинатор из книжки на знакомом мне Haskell... Угу, фиг - его невозможно типизировать. Хотел было попробовать на Scheme, но сообразил, что типизация она и в scheme типизация. Тогда стал искать какой-нибудь язык, реализующий нетипизированное λ-исчисление, чтобы на нем можно было "поиграться" с примерами из книжек. Нашел только unlambda, который, как оказалось, реализует вовсе даже не лямбду, а комбинаторную логику, а синтаксис у него похож более всего на brainfuck. Вздохнул и решил писать что-то такое сам...
Вроде написал, и примеры из книжек на нем работают, но в сложных выражениях пока что вылезают баги при α-конверсии (переменные то переименуются, когда не надо, то наоборот). Надеюсь всё-таки допилить...
Подробности про язык тут, само поделие тут (Depends: python, python-ply; запускать ./pylambda.py в терминале).
Подписаться на:
Комментарии к сообщению (Atom)
Кстати можно сюда посмотреть
ОтветитьУдалитьhttp://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html,
тут реализация интерпретатора нескольких видов лямбда-исчисления
> Нашел несколько книжек и пр.
ОтветитьУдалитьможно поинтересоваться какие? тоже хочу изучить, но ничего путного не нашел :(
Например, могу рекомендовать: Х.Барендрет. λ-исчисление: его синтаксис и семантика. М.:Мир, 1985. Есть в электронном виде (скан).
ОтветитьУдалить