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

Поскольку лямбда-исчисление не такая трудная тема, я предположу, что вы с ней уже знакомы, поэтому не буду тратить много времени на теорию. Если вы хотите углубится в этот вопрос, то рекомендую хорошую теоретическую статью.

Теория

Язык исчисления довольно простой и состоит всего из трёх элементов:

1) Переменные

2) Лямбда-функции

3) Применение

Вот, как это выглядит математически:

λx.M - функция, с аргументом x и телом M
M N - применение функции M к аргументу N

Теперь затронем β-редукцию.
β-редукция — это единственное правило вычислений в лямбда-исчислении. Оно описывает, что происходит, когда функция применяется к аргументу. Как бы (страшно?) это не звучало, суть в том, чтобы заменить все вхождения параметра в теле функции на переданный аргумент (фактически вызов функции).

Рассмотрим на следующем примере: (λx.M) N

Как мы помним - это применение функции M к аргументу N. Результатом β-редукции будет новое выражение, которое мы получаем, взяв тело функции M и заменив в нём каждое свободное вхождение переменной x на аргумент N. Результат: M[x := N].

Это теоретический минимум, который я хотел вам предоставить. Теперь можно приступить ко второй части этой статьи - реализации.

Реализация

Я долго думал, на каком языке писать реализацию. Хотелось взять что-то функциональное, но при этом понятное. Остановился я на языке gleam. Сейчас он становится все более модным, а самое главное: он функциональный и простой для освоения человеком, который видит его в первый раз. Его плюсом также является отсутствие циклов и иммутабельность данных, так что конечное решение должно получится вполне красивым и лаконичным.
Начнем с определения термов (выражений). Как мы помним, их всего 3: переменная, функция, применение. Давайте так и запишем:

pub type Term {
  Variable(Int) // Переменная
  Lambda(fn(Term) -> Term) // Лямбда-функция
  Apply(Term, Term) // Применение
}

Обратите внимание, что в конструкторе переменной указан тип Int. Поскольку наша цель построить математически точную модель, мы будем использовать индексы де Брейна. Идея в том, чтобы представить переменную числом, которое показывает "на сколько лямбд назад она была объявлена". Это позволяет решить проблему с α-конверсией (переименованием переменных):

// Одинаковые ли эти функции?
λx.x    и    λy.y    // Да! Но имена разные - это α-эквивалентность

// Из этого следует:

// Тут нужно переименовывать:
(λx.x) и (λy.y)

// А тут и так всё одинаково :)
(λ.0) и (λ.0)

Теперь реализуем функцию reduce, где мы при помощи конструкции case обработаем случай, когда наш Term - Apply (применение). Лямбда-функции и переменные не вычисляются.

pub fn reduce(term: Term) -> Term {
  case term {
    Apply(m, n) -> {
      let n = reduce(n)   // Вычисляем аргумент
      case reduce(m) {    // Вычисляем функцию
        Lambda(f) -> reduce(f(n))    // Бета-редукция
        m -> Apply(m, n)    // Не функция, поэтому оставляем как есть
      }
    }
    term -> term
  }
}

Как я и обещал, из-за отсутствия циклов мы вынуждены использовать рекурсию, что помогает нам сделать решение довольно элегантным.

И на этом можно было бы закончить, но как нам проверить работу? Функция print в gleam принимает только строку, а значит нам нужно сделать ещё одну функцию, которая преобразует Term в строку. Сделать это можно как-то так:

pub fn to_string(lvl: Int, term: Term) -> String {
  case term {
    Lambda(f) -> "(" <> "λ." <> to_string(lvl + 1, f(Variable(lvl))) <> ")"
    Apply(m, n) -> to_string(lvl, m) <> " " <> to_string(lvl, n)
    Variable(i) -> int.to_string(i)
  }
}

А теперь давайте напишем что-нибудь интересное, например Z-комбинатор. Он является вариантом Y-комбинатора, а он в свою очередь позволяет реализовать рекурсию в языках, где ее нет. Вот так определяется Z-комбинатор:
Z = λf.(λx.f (λv.x x v)) (λx.f (λv.x x v))

Он «оборачивает» рекурсивный вызов в лямбду, которая вычисляется только когда нужен ее аргумент v.

pub fn main() {
  let z =
    Lambda(fn(f) {
      let inner =
        Lambda(fn(x) { Apply(f, Lambda(fn(v) { Apply(Apply(x, x), v) })) })
      Apply(inner, inner)
    })

  io.println(to_string(0, z))
}

На этом я предлагаю закончить. Более интересные примеры я выложу в репозиторий проекта, там же вы сможете найти полный код, представленный в этой статье. Кто захочет - может добавить свои примеры, или указать на возможные неточности в коде. Все issue и pr я рассматриваю.

Ну а закончить хотелось бы списком из чужих реализаций λ-исчисления, которые мне понравились:

Python
Elixir
Rust
Go
Ocaml