Связанные и свободные переменные, альфа-эквивалентность

Почему \x.x и \y.y — это одна и та же функция, и где прячется ловушка захвата имён.

Связанная переменная введена своей абстракцией и локальна для неё; свободная — не связана ни одной охватывающей абстракцией и зависит от контекста.

Кто кого связывает

В выражении \x. x y переменная x связана ближайшей лямбдой \x — это её «локальная переменная». Переменная y ничем не связана внутри выражения, она свободна: её смысл приходит снаружи. Аналогия с обычным кодом: связанная — это параметр функции, свободная — глобальная переменная или замыкание.

\x. x y          -- x связана, y свободна
\x. \y. x y      -- x и y связаны
x (\x. x)        -- первый x свободен, второй (внутри \x) связан

Альфа-эквивалентность

Имя связанной переменной — чистая условность. Функция \x. x и \y. y — это одна и та же функция тождества; различие лишь в выборе буквы. Переименование связанной переменной (согласованно во всём её теле) называется альфа-преобразованием, а равенство выражений с точностью до таких переименований — альфа-эквивалентностью. Менять можно только связанные имена и только так, чтобы не столкнуться с уже занятым именем.

\x. x        =α  \y. y          -- да, одна функция
\x. \y. x    =α  \a. \b. a      -- да
\x. \y. x    =α  \y. \y. y      -- НЕТ: переименование захватило бы внешнюю x

Демонстрация: вычисляем множества свободных переменных

Свободные переменные находятся структурно: у переменной — она сама, у аппликации — объединение, у абстракции — свободные тела минус связанное имя.

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]}     # связали t[1] — убрали
    return free_vars(t[1]) | free_vars(t[2])

e1 = lam("x", app(var("x"), var("y")))      # \x. x y
e2 = app(var("x"), lam("x", var("x")))      # x (\x. x)
print("free(\\x. x y) :", sorted(free_vars(e1)))
print("free(x (\\x.x)):", sorted(free_vars(e2)))

Вывод:

free(\x. x y) : ['y']
free(x (\x.x)): ['x']

Захват переменной — главная ловушка

Зачем нам всё это? Потому что при вычислении мы подставляем выражения внутрь функций, и наивная подстановка может захватить свободную переменную. Если в \x. y подставить вместо y выражение, содержащее x, то этот x ошибочно «прилипнет» к локальному \x. Лекарство — перед подстановкой переименовать связанную переменную (альфа), чтобы имена не столкнулись. Этот аккуратный механизм мы реализуем в следующем уроке про бета-редукцию.

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

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

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

• Переименовать свободную переменную. Альфа меняет только связанные имена; трогать свободные нельзя — изменится смысл.
• Игнорировать захват при подстановке. Без переименования подстановка может «приклеить» свободную переменную к чужой лямбде — классический баг наивных интерпретаторов.
• Считать, что имя что-то значит. Для связанной переменной важна только структура связывания, а не буква.

Итоги

• Связанная переменная локальна для своей лямбды, свободная зависит от контекста.
• Альфа-эквивалентность: переименование связанных имён не меняет функцию.
• Свободные переменные вычисляются структурно (тело минус связанное имя).
• Захват переменной — главная опасность подстановки; лечится альфа-переименованием или индексами де Брёйна.