λ-исчисление

Описание

λ-исчисление (лямбда-исчисление) лежит в основе большинства функциональных языков программирования: семейства Лиспа (Common Lisp, Scheme, Clojure и др.) и семейства ML (Standard ML, Haskell, Agda и пр.).

λ-исчисление состоит из языка λ-выражений и набора правил преобразования. Базовые правила построения λ-выражений:

  • переменная x является λ-выражением;
  • если e — λ-выражение, а x — переменная, то λ x . e также λ-выражение (лямбда-абстракция);
  • если e_1 и e_2 — λ-выражения, то e_1 e_2 также λ-выражение (аппликация).

Для удобства работы с λ-выражениями, при записи могут использоваться следующие упрощения:

  • внешние скобки могут быть опущены (λ x . e_1) e_2;
  • аппликация считается лево-ассоциативной e_1 e_2 e_3 ≡ ((e_1 e_2) e_3);
  • тело λ-выражения распространяется вправо насколько возможно λ x . e_1 e_2 ≡ λ x . (e_1 e_2);
  • последовательные λ-абстракции схлопываются в одну λ x . λ y . λ z . e ≡ λ x y z . e.

Оператор λ связывает переменную в выражении λ x . e. Переменные, подпадающие под какой-либо оператор λ-абстракции, называются связанными. Все прочие переменные называются свободными. Например, переменная y свободна в выражении λ x . y x. Переменная связывается ближайшим оператором λ. Например, единственное вхождение переменной x в выражении λ x . y (λ x . x) связано со вторым оператором λ.

Значение λ-выражения определяется правилами редукции:

  • α-конверсия: переименовывание связанных переменных
  • β-редукция: применение функции к аргументам
  • η-конверсия: выражает принцип две функции идентичны, если имеют одинаковый результат на всех входах

Применение функции к аргументам осуществляется за счёт подстановки выражения-аргумента вместо связанной переменной в теле λ-выражения:

     x[x -> e] ≡ e
     y[x -> e] ≡ y, если y ≠ x
     (e_1 e_2) [x -> e] ≡ (e_1 [x -> e]) (e_2 [x -> e])
     (λ x . e_1) [x -> e] ≡ λ x . e_1
     (λ y . e_1) [x -> e] ≡ λ y . (e_1 [x -> e]), если y ≠ x и y не входит свободно в e

Язык λ-выражений может быть расширен:

  • базовыми типами данных (например, числа, булевы значения, строки);
  • базовыми контейнерными типами (списки и кортежи);
  • встроенными операциями (например, +, -, sin, cos, and, or, ++)
  • специальными конструкциями (например, if e1 then e2 else e3 или let x1 = e1 in e2);
  • системой типов;
  • пользовательские структуры данных;
  • и т.д.

Минимальные требования (базовая часть)

Базовая реализация проекта, в которой должны разбираться все участники, должна:

  • определять структуру данных для синтаксического дерева;
  • содержать раздельно парсер и интерпретатор (с любой стратегией редукций);
  • предоставлять простую интерактивную среду программирования (REPL).

Расширенный парсер (индивидуальная часть)

Расширенный парсер должен добавлять хотя бы 2 различные возможности к базовому варианту. Ниже перечислены возможные варианты расширения парсера, однако этим списком они не ограничены:

  • разбор расширенного λ-исчисления;
  • восстановление после ошибок (например, если пользователь написал запятую (,) вместо точки (.), парсер может запомнить эту ошибку и продолжить разбор программы);
  • поддержка пользовательских инфиксных операций с возможностью задать приоритет и ассоциативность;
  • и т.д.

Система типов (индивидуальная часть)

Система типов помогает определить семантику λ-выражений, но также может быть использована для оптимизаций при интерпретации и генерации кода.

Система типов должна поддерживать хотя бы 2 различные возможности:

  • базовые типы (числа, булев тип, строки);
  • контейнерные типы (списки, кортежи, суммы);
  • параметрический полиморфизм;
  • пользовательские типы данных;
  • механизм автоматического вывода типа для терма;
  • и т.д.

Расширенная интерактивная среда (индивидуальная часть)

Расширенная интерактивная среда должна добавлять хотя бы 2 различные возможности к базовому интерфейсу. Ниже перечислены возможные варианты расширения интерактивной среды, однако этим списком они не ограничены:

  • команды интерпретатора:
    • показать все возможные варианты редукции терма (одного шага) и выбрать один;
    • показать тип выражения;
    • поменять порядок редукции;
    • перевести терм из/в кодировку Чёрча;
    • загрузить программу из файла;
  • интерпретация расширенного λ-исчисления;
  • дружелюбные сообщения об ошибках (например, для замкнутых термов при опечатке в имени переменной можно предложить имена переменных, отличающихся одной буквой, которые находятся в области видимости);
  • и т.д.