Если вы когда-нибудь задумывались о написании своего языка программирования, в особенности функционального, то должны быть в курсе, что лямбда исчисление - это основа всех функциональных языков. Я решил сделать цикл статей, где мы будем реализовывать интересные алгоритмы, используемые в компиляторах, а также различные исчисления. Лямбда-исчисление - это фундамент, с которого я и предлагаю начать погружение в эту нору.
Поскольку лямбда-исчисление не такая трудная тема, я предположу, что вы с ней уже знакомы, поэтому не буду тратить много времени на теорию. Если вы хотите углубится в этот вопрос, то рекомендую хорошую теоретическую статью.
Теория
Язык исчисления довольно простой и состоит всего из трёх элементов:
1) Переменные
2) Лямбда-функции
3) Применение
Вот, как это выглядит математически:
λx.M - функция, с аргументом x и телом MM 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 я рассматриваю.
Ну а закончить хотелось бы списком из чужих реализаций λ-исчисления, которые мне понравились:
Автор: k1ngmang
