Бета-редукция: вычисление как переписывание

Как «работает» лямбда-исчисление: всё вычисление — это повторная подстановка аргумента в тело.

Бета-редукция — правило вычисления: применение функции к аргументу (\x. e) a переписывается в тело e, где x заменён на a.

Единственное правило

У лямбда-исчисления один-единственный вычислительный шаг — бета-редукция:

(\x. e) a   --beta->   e[x := a]

Читается: «применили функцию \x. e к аргументу a — заменили в теле e все вхождения x на a». Запись e[x := a] — это подстановка. Вычислить программу значит повторять этот шаг, пока есть что редуцировать. Результат без редексов называется нормальной формой.

(\x. x) y                  --beta->  y
(\x. \y. x) a b            --beta->  (\y. a) b  --beta->  a
(\f. f (f z)) (\x. x)      --beta->  (\x.x)((\x.x) z) --*->  z

Подстановка с защитой от захвата

Сердце редукции — корректная подстановка. Опасность из прошлого урока: при входе под лямбду \y. ..., если подставляемое выражение содержит свободную y, мы обязаны переименовать y в свежее имя, иначе захватим. Реализуем это честно.

_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))
    # lam
    p, b = t[1], t[2]
    if p == x:
        return t                          # x перекрыт — не трогаем
    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 show(t):
    if t[0]=="var": return t[1]
    if t[0]=="lam": return "(\\"+t[1]+". "+show(t[2])+")"
    return "("+show(t[1])+" "+show(t[2])+")"

# проверим защиту от захвата: (\x. \y. x) y
term = app(lam("x", lam("y", var("x"))), var("y"))
print("подставляем y вместо x в \\y.x:")
print(show(subst(lam("y", var("x")), "x", var("y"))))

Вывод:

подставляем y вместо x в \y.x:
(\y1. y)

Связанная y переименована в y1, поэтому подставленная свободная y не захватилась. Именно так интерпретатор остаётся корректным.

Нормализация: повторяем шаг до упора

Соберём полный редуктор: ищем редекс (применение лямбды), делаем шаг, повторяем. Применим нормальную стратегию — редуцируем самый левый внешний редекс (узлы и подстановка — те же, что выше).

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])
_c = [0]
def fresh(b):
    _c[0] += 1; return b + str(_c[0])
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 show(t):
    if t[0]=="var": return t[1]
    if t[0]=="lam": return "(\\"+t[1]+". "+show(t[2])+")"
    return "("+show(t[1])+" "+show(t[2])+")"

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=1000):
    for _ in range(limit):
        t, r = step(t)
        if not r:
            return t
    return t

# (\f. \x. f (f x)) (\n. n) z   -- применяем "дважды" тождество к z
twice = lam("f", lam("x", app(var("f"), app(var("f"), var("x")))))
expr  = app(app(twice, lam("n", var("n"))), var("z"))
print("результат:", show(normalize(expr)))

Вывод:

результат: z

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

Существуют разные стратегии выбора редекса. «Нормальный порядок» (самый левый внешний) гарантированно находит нормальную форму, если она есть. «Аппликативный порядок» (сначала аргумент) соответствует энергичной семантике большинства языков, но может зациклиться там, где нормальный порядок завершился бы. Ленивые языки (Haskell) близки к нормальному порядку с разделением вычислений.

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

Подстановка без защиты от захвата. Самый частый баг интерпретатора; всегда переименовывайте связанное имя при риске коллизии.
Считать, что нормальная форма всегда существует. Терм (\x. x x)(\x. x x) редуцируется сам в себя бесконечно — нормальной формы нет.
Игнорировать стратегию. Один и тот же терм при аппликативном порядке может зациклиться, при нормальном — завершиться.

Итоги

Бета-редукция — единственное правило: (\x.e) a переписывается в e[x:=a].
Подстановка обязана защищаться от захвата переименованием связанных имён.
Нормализация — повторение шага до нормальной формы (которой может и не быть).
Стратегия редукции влияет на завершаемость (нормальный vs аппликативный порядок).