Лямбда как модель вычислений: числа Чёрча

Доказываем на практике: из трёх правил можно собрать арифметику. Запускаем 2 + 3 в чистом лямбда-исчислении.

Числа Чёрча — кодировка натуральных чисел как функций: число n — это функция, применяющая свой аргумент-функцию n раз.

Тьюринг-полнота без всего

Удивительный факт: лямбда-исчисление вычислительно эквивалентно машине Тьюринга. В нём нет чисел, булевых, пар, циклов — но всё это кодируется функциями. Это и значит «модель вычислений»: любой алгоритм выразим тремя правилами. Покажем это конструктивно — закодируем числа и сложим их работающим интерпретатором.

Идея кодировки Чёрча

Число n представляется функцией двух аргументов: бери функцию f и значение x, примени f к x ровно n раз.

0  =  \f. \x. x                 -- ноль применений
1  =  \f. \x. f x               -- одно
2  =  \f. \x. f (f x)           -- два
3  =  \f. \x. f (f (f x))       -- три

Сложение «n плюс m»: примени f сначала m раз, потом ещё n раз.

PLUS = \n. \m. \f. \x. n f (m f x)

Исполнимый интерпретатор: 2 + 3 = 5

Соберём редуктор из прошлого урока, закодируем числа Чёрча, сложим 2 и 3 и «декодируем» результат обратно в обычное целое, посчитав глубину применений.

_c = [0]
def fresh(b):
    _c[0] += 1; return b + str(_c[0])
def var(n):    return ("var", n)
def lam(p, b): return ("lam", p, b)
def app(f, a): return ("app", f, a)

def free_vars(t):
    if t[0]=="var": return {t[1]}
    if t[0]=="lam": return free_vars(t[2]) - {t[1]}
    return free_vars(t[1]) | free_vars(t[2])

def subst(t, x, s):
    if t[0]=="var": return s if t[1]==x else t
    if t[0]=="app": return app(subst(t[1],x,s), subst(t[2],x,s))
    p, b = t[1], t[2]
    if p == x: return t
    if p in free_vars(s):
        np = fresh(p); b = subst(b, p, var(np)); p = np
    return lam(p, subst(b, x, s))

def step(t):
    if t[0]=="app":
        if t[1][0]=="lam":
            return subst(t[1][2], t[1][1], t[2]), True
        nf,r = step(t[1])
        if r: return app(nf,t[2]), True
        na,r = step(t[2])
        if r: return app(t[1],na), True
        return t, False
    if t[0]=="lam":
        nb,r = step(t[2])
        if r: return lam(t[1],nb), True
        return t, False
    return t, False

def normalize(t, limit=10000):
    for _ in range(limit):
        t,r = step(t)
        if not r: return t
    return t

def church(n):
    body = var("x")
    for _ in range(n):
        body = app(var("f"), body)
    return lam("f", lam("x", body))

PLUS = lam("n", lam("m", lam("f", lam("x",
        app(app(var("n"), var("f")),
            app(app(var("m"), var("f")), var("x")))))))

def to_int(t):
    t = normalize(t)
    if t[0] != "lam": return None
    inner = t[2]
    if inner[0] != "lam": return None
    f, x = t[1], inner[1]
    body, cnt = inner[2], 0
    while body[0]=="app" and body[1]==("var", f):
        cnt += 1; body = body[2]
    return cnt

expr = app(app(PLUS, church(2)), church(3))
print("2 + 3 =", to_int(expr))
print("church(0) =", to_int(church(0)))
print("church(4) =", to_int(church(4)))

Вывод:

2 + 3 = 5
church(0) = 0
church(4) = 4

Никакой встроенной арифметики — только функции и бета-редукция. Число «существует» лишь как поведение: «примени аргумент n раз».

Булевы и не только

Тем же приёмом кодируются булевы значения и условие: TRUE = \a. \b. a (бери первое), FALSE = \a. \b. b (бери второе). Тогда IF c t e = c t e просто выбирает ветку. Пары, списки, рекурсия (через комбинатор неподвижной точки Y) — всё выражается. Так лямбда-исчисление становится полноценным языком программирования из трёх правил.

Как работает под капотом

Кодировка Чёрча — это представление данных через их сворачивание (fold). Число n — это «n-кратное применение», список — «правая свёртка по элементам». Эта идея напрямую отражается в современных языках: тип данных можно закодировать его элиминатором (как с ним работают), а не структурой. Отсюда — кодировки Чёрча/Скотта и связь с категорной семантикой (последний раздел).

Частые ошибки

• Искать «настоящие» числа в лямбда-исчислении. Их нет — есть только функции, ведущие себя как числа.
• Забывать про лимит шагов. Без типов терм может не завершиться; интерпретатор обязан иметь предохранитель (limit).
• Думать, что без типов плохо. Нетипизированное исчисление мощнее (Тьюринг-полно), но именно поэтому в нём есть «плохие» термы — отсюда мотивация типизировать в следующем разделе.

Итоги

• Лямбда-исчисление Тьюринг-полно: числа, булевы, пары — кодируются функциями.
• Число Чёрча n — функция, применяющая аргумент n раз; сложение — композиция применений.
• Работающий интерпретатор даёт 2 + 3 = 5 без встроенной арифметики.
• Кодировка данных через их использование — идея, которая вернётся в типах и категориях.