❯ Введение

Реализация универсальной рекурсии в одну строку и объяснение ключевых конструкций лямбда‑исчисления на Python. Подойдёт даже тем, кто не очень знаком с Python. Если хотите понять, как из одних лишь функций строятся булевы, списки и числа и, быть может, попробовать до реализации некоторых алгоритмов самостоятельно — добро пожаловать под кат.

Начну с небольшой личной истории. Чисто из академического любопытства захотелось реализовать универсальную рекурсию в одну строку на Python, не прибегая к использованию именованных функций, на лямбдах. Мне было известно про то, что это возможно в лямбда исчислении, хоть мне и был неизвестен способ. После нескольких минут размышлений у меня получилось реализовать это, а процесс решения таких задач понравился, из этого вышли поиски другого в лямбда исчислении. Так и появилась идея о написании этой статьи. Моё решение оказалось аналогом Y-комбинатора для Python.

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

❯ Принципы работы лямбда исчисления

В лямбда исчислении есть всего несколько фундаментальных операций: аппликация и абстракция.

Абстракция или λ-абстракция, в свою очередь, строит функции по заданным выражениям. Можно задать функцию как (λx.expr), где x — имя переменной, а expr выражение, которое выйдет после применения функции. В expr можно использовать x. Если перевести это на Python, то будет (lambda x: expr).

Аппликация означает это вызов функции. Обычно обозначается как f a, где “f” это функция, а “a” — аргумент. Это соответствует математической записи f(a). Такая же запись используется и в Python. (lambda x: x)(y) будет как ((λx.x) y). Аргументами вполне могут служить и другие функции. А функции могут возвращать другие функции.

Функции от нескольких аргументов в лямбда исчислении записываются как (λx y.expr). Эта запись будет эквивалентна записи (λx.λy.expr). Если переводить на синтаксис Python, то будет (lambda x: lambda y: expr). Т.е. функции от множества аргументов задаются как функции, принимающие N-й аргумент, возвращающие функции, которые принимают (N + 1)-й элемент и лишь в конце выражение, которое может использовать эти аргументы.

Описанный процесс превращения функций многих переменных в функцию одной переменной называется карринг (также: каррирование).

В этом есть некоторое отличие лямбда исчисления от лямбд в Python. В Python записи (lambda x, y: x(y)) и (lambda x: lambda y: x(y)) не эквивалентны. (lambda x, y: x(y)) сразу требует несколько аргументов (вызов через (x, y) ), когда как (lambda x: lambda y: x(y)) требует цепочки вызовов (вызов через (x)(y) )

Запись f a b c эквивалентна записи (((f a) b) c)

Стратегии выполнения

Лямбда исчисление можно выполнять по разному. f задаётся как (λx.ax)((λy.by) c) или, если при переводе на синтаксис Python, (lambda x: a(x))((lambda y: b(y))(c)).

Можно различным образом раскрывать f: сначала раскрывать функцию (ленивый подход), или перед этим раскрывать её аргументы (энергичный подход).

Раскрытия с ленивым подходом: (λx.a x)((λy.b y) c) => a((λy.b y) c) => a(b c) (lambda x: a(x))((lambda y: b(y))(c)) => a((lambda y: b(y))(c)) => a(b(c))

Раскрытия с энергичным подходом: (λx.a x)((λy.b y) c) => (λx.a x)(b c) => a (b c) (lambda x: a(x))((lambda y: b(y))(c)) => (lambda x: a(x))(b(c)) => a(b(c))

Несложно заметить, что результат этих раскрытий получился одинаковый. Это доказывается теоремой Чёрча — Россера. Но стоит понимать, что теорема говорит лишь о том, что самая упрощенная форма будет одинаковой для любого порядка раскрытия, но это не означает достижимость этой формы при любом порядке раскрытия. К примеру, (lambda x, y: x)(42, (lambda x: x(x))(lambda x: x(x))) будет выполняться вечно при энергичном подходе, но достигнет конечного результата при ленивом.

Если рассматривать конкретно Python, то исполнение у него энергичное.

❯ Различные алгоритмы на лямбда исчислении

Сразу оговорюсь, что тут функции будут использовать функции от множества аргументов в стиле Python. И написано оно для языка Python, поэтому стоит учитывать энергичное выполнение. Но всё это можно переписать и в обычном лямбда исчислении.

Рекурсия

Многие вычисления могут требовать длительное (или даже бесконечное) вычисление, длительность которого зависит от аргументов.

Для этого в некоторых языках есть циклы, рекурсия. Рассмотрим рекурсивную реализацию факториала.

def fact(arg):
    return 1 if arg == 0 else arg * fact(arg - 1)

Внутри функции факториала используется вызов себя же через имя, так получается рекурсия. Но данный подход не получится сделать напрямую в лямбда исчислении, так как в лямбда исчислении у функций нет имён. Но это достижимо через некоторые функции, которые можно описать на лямбда исчислении. Они передают в функцию себя же в каком-то виде.

Предлагаю попробовать это реализовать своими силами в коде Python. Дам немного тестов

f = () # Ваша функция, задавайте через лямбды и не используйте прямую рекурсию через имена

assert(f(lambda s, y: y * s(y-1) if y != 0 else 1)(0) == 1)
assert(f(lambda s, y: y * s(y-1) if y != 0 else 1)(1) == 1)
assert(f(lambda s, y: y * s(y-1) if y != 0 else 1)(2) == 2)
assert(f(lambda s, y: y * s(y-1) if y != 0 else 1)(3) == 6)
assert(f(lambda s, y: y + s(y-1) if y != 0 else 0)(2) == 3)
assert(f(lambda s, y: y)(42) == 42)

Как видно из тестов, используется подход Python к определению функций нескольких аргументов. И, так как используется энергичный подход вычисления, следует это учитывать при написании кода.

fact = f(lambda s, y: y * s(y-1) if y != 0 else 1)

get_self = (lambda x: x(x))

f = lambda func: get_self(...)

f = lambda func: get_self(lambda s: ...)

f = lambda func: get_self(lambda s: lambda arg: ...)

f = lambda func: get_self(lambda s: lambda arg: func(s(s), arg))

f = (lambda g: (lambda x: x(x))(lambda s: lambda arg: g(s(s), arg)))

# Решение для любого кол-ва аргументов у функций через args и kwargs, более продвинутое из Python
# f = (lambda g: (lambda x: x(x))(lambda s: lambda *args, **kwargs: g(s(s), *args, **kwargs)))

Это решение будет аналогично Z-комбинатору, который является аналогом Y-комбинатора энергичного выполнения.

Именно такое решение у меня получилось из той личной истории, только потом оказалось, что оно уже изобретено в подобном виде и до меня :)

Y комбинатор

Y комбинатор был введён известным американским учёным Хаскеллом Карри. Он имеет следующий вид

Y = λf.(λx.f (x x)) (λx.f (x x))

Нетрудно заметить, что он уйдёт в бесконечную рекурсию при использовании энергичного выполнения. Для решения этой проблемы был придуман Z комбинатор. В нём следующий аргумент определён явно, что отложит вычисления.

Z = λf.(λx.f (λv.x x v)) (λx.f (λv.x x v))

Моё решение в прошлой части по поведению аналогично этому Z комбинатору.

Это всё комбинаторы неподвижной точки.

Boolean значения

В чистом лямбда‑исчислении нет отдельных типов — всё выражается функциями. Булевы значения удобно закодировать как функции‑матчеры: каждое значение — функция, которая принимает два аргумента (ветку истина и ветку ложь) и вызывает нужную.

true = lambda x, y: x
false = lambda x, y: y

Такая кодировка естественно служит для pattern matching, т.к. значение содержит логику выбора ветки.

Можно определить операции с такими булевыми значениями

# Негация
not_ = lambda b: b(false, true)

# И
and_ = lambda a, b: a(b, false)

# Или
or_  = lambda a, b: a(true, b)

# Эквивалентность
eq = lambda a, b: a(b, not_(b))

Кодировка Скотта

Cтруктура — это функция, которая принимает обработчики для каждого конструктора (например, on_empty и on_pair для списка) и вызывает нужный. Это фактически отложенный pattern‑matching.

nil = lambda on_empty, on_pair: on_empty
cons = lambda first, second: lambda on_empty, on_pair: on_pair(first, second)

Пример создания списка 0 -> 1 -> nil:

my_list = cons(0, cons(1, nil))
# my_list = lambda on_empty, on_pair: on_pair(0, lambda on_empty, on_pair: on_pair(1, lambda on_empty, on_pair: on_empty))

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

Разбор (pattern‑matching):

list_get_first = lambda l: l(None, lambda x, xs: x)
list_is_empty  = lambda l: l(True,  lambda _, __: False)

Эту кодировку можно использовать не только для списков, но и для других структур.

К примеру, так можно сделать числа:

fix = (lambda g: (lambda x: x(x))(lambda s: lambda arg: g(s(s), arg)))

# Ноль (Zero)
# Просто возвращает первый аргумент
zero = lambda on_zero, on_succ: on_zero

# Следующее число (Successor)
# Принимает число 'n' и возвращает функцию, 
# которая при вызове отдаст этот 'n' во второй аргумент. 
# Это позволяет увеличить уровень вложенности на 1, что и означает увелечение числа на 1
succ = lambda n: lambda on_zero, on_succ: on_succ(n)

# Примеры чисел
one = succ(zero)
two = succ(one)
three = succ(two)

# Получает обычное число в Python из такого
to_python_int = fix(lambda s, num: num(0, lambda x: 1 + s(x) ))

Прибавление на единицу задаётся как succ(x), где x - число, к которому прибавляют.

Реализацию вычитания я предлагаю попробовать реализовать читателю. Вот тесты

assert(to_python_int(pred(one)) == 0)
assert(to_python_int(pred(two)) == 1)
assert(to_python_int(pred(three)) == 2)

pred = lambda num: num(0, lambda x: x)

Кодировка Чёрча

Эта кодировка была придумана Алонзо Чёрчем. Вместо того, чтобы создавать вложенную структуру, которая принимает функции на каждом шаге, он задал структуры как свёртку.

my_list = lambda f, x: f(0, f(1, x))

Стоит заметить, что функция используется одна и та же. Это задаёт некие ограничения с точки зрения гибкости использования.

Получение первого элемента списка выглядит так:

list_get_first = lambda l: l((lambda x, xs: x), None)

В этой же кодировке можно задавать и числа.

Эти числа — это просто применение функции N раз: 0 это x, 1 это f(x), 2 это f(f(x)) и так далее.

zero  = lambda f, x: x
one   = lambda f, x: f(x)
two   = lambda f, x: f(f(x))
three = lambda f, x: f(f(f(x)))

# Как можно заметить, в такой реализации не потребовался комбинатор неподвижной точки, тогда как с числами Скотта он был необходим.
to_python_int = lambda n: n(lambda x: x + 1, 0)

succ = lambda num: lambda f, x: f(num(f, x))

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

Тесты

assert(to_python_int(pred(one)) == 0)
assert(to_python_int(pred(two)) == 1)
assert(to_python_int(pred(three)) == 2)

Метод Стивена Клини

pair = lambda first, second: lambda f: f(first, second)
pair_first = lambda pair: pair(lambda first, _: first)
pair_second = lambda pair: pair(lambda _, second: second)

pair = lambda first, second: lambda f: f(first, second)
pair_first = lambda pair: pair(lambda first, _: first)
pair_second = lambda pair: pair(lambda _, second: second)

# (x, y) => (y, y + 1)
shift_and_add = lambda pair: lambda f: f(pair_second(pair), succ(pair_second(pair)))

pred = lambda n: pair_first(n(shift_and_add, pair(zero, zero)))

Метод Барендрегта

pred_iter = lambda f: lambda g: lambda h: h(g(f))

# pred_iter(f)(x)
#   => (lambda g: lambda h: h(g(f)))(x)
#   => lambda h: h(x(f))

# pred_iter(f)(lambda h: h(x(f)))
#   => (lambda g: lambda h: h(g(f)))(lambda h: h(x(f)))
#   => lambda h: h((lambda h: h(x(f)))(f)) 
#   => lambda h: h(f(x(f))) 

pred = lambda n: lambda f, x: n(pred_iter(f), lambda _: x)(lambda v: v)

Моё решение 1

fix = (lambda g: (lambda x: x(x))(lambda s: lambda arg: g(s(s), arg)))

scott_zero = lambda on_zero, _: on_zero

scott_pred = lambda num: num(0, lambda x: x)

c_to_scott = lambda num: num(lambda p: lambda _, on_succ: on_succ(p), scott_zero)
scott_to_c = fix(lambda s, num: lambda f, x: num(x, lambda p: f(s(p)(f, x)) ))

pred = lambda num: scott_to_c(scott_pred(c_to_scott(num)))

Моё решение 2

Его у меня получилось придумать в ходе написания этой статьи. Оно получилось достаточно элегантным и его можно обобщить на другие алгоритмы (вычитание, деление и т.д.) и другие типы данных в кодировке Чёрча.

Его можно найти тут.

Хочу написать научную статью с этим алгоритмом, но опыта научных публикаций не имею. Ищу опытных соавторов.

❯ Заключение

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

В статье мы прошли путь от базовых понятий (абстракция и аппликация) через различие стратегий редукции до практических кодировок — Чёрча и Скотта — и показали, как это всё реализуется на Python, который является энергичным языком.

Новости, обзоры продуктов и конкурсы от команды Timeweb.Cloud — в нашем Telegram-канале ↩