понедельник, февраля 11, 2008

Интерпретатор lambda-исчисления

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

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

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

3 комментария:

  1. Кстати можно сюда посмотреть
    http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html,
    тут реализация интерпретатора нескольких видов лямбда-исчисления

    ОтветитьУдалить
  2. Анонимный11/30/2008 11:52 PM

    > Нашел несколько книжек и пр.
    можно поинтересоваться какие? тоже хочу изучить, но ничего путного не нашел :(

    ОтветитьУдалить
  3. Например, могу рекомендовать: Х.Барендрет. λ-исчисление: его синтаксис и семантика. М.:Мир, 1985. Есть в электронном виде (скан).

    ОтветитьУдалить