Свободные и связанные переменные, подстановка и захват имён

В прошлой статье (https://courses.digitable.life/post/lambda-calculus/01-syntax/) мы научились читать лямбда-выражения: где абстракция, где аппликация, куда тянутся скобки. Теперь начинается самое интересное — и самое коварное.

Всё лямбда-исчисление держится на одной-единственной операции: взять функцию, взять аргумент, подставить аргумент вместо параметра. Ровно это делает ваш JavaScript, когда вы вызываете f(42). Казалось бы, что тут может пойти не так? Ответ: почти всё. Если подставлять «в лоб», заменяя одну букву на другое выражение, вы получите программу с другим смыслом. Не с ошибкой компиляции, не с исключением — просто с другим смыслом. Это и есть захват имён (variable capture), и это баг, на котором спотыкались авторы макросистем, шаблонизаторов и компиляторов на протяжении десятилетий.

Эта статья — про то, как переменные живут в лямбда-выражениях и как подставлять честно.

Зачем это программисту, а не логику

Прежде чем формализм — три ситуации, где вы уже сталкивались с этой темой, просто не называли её так.

1. Замыкания. Вы пишете:

const multiplier = 10;
const scale = (x) => x * multiplier;

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

2. Затенение (shadowing). Вы пишете const x = 1; внутри функции, где снаружи уже был x, и линтер ворчит no-shadow. Вопрос «какой именно x имеется в виду в этой строке» — это вопрос о том, какой λ связывает данное вхождение переменной.

3. Гигиена макросов. Если вы писали макросы на Rust, Scheme или Lisp, вам знакома проблема: макрос вставляет в код переменную tmp, а у пользователя в этом месте уже есть своя tmp — и всё ломается. Rust и Scheme решают это «гигиеническими» макросами, которые автоматически переименовывают внутренние имена. Это буквально capture-avoiding substitution из этой статьи, только в промышленном исполнении.

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

Свободные и связанные: интуиция

Возьмём выражение:

λx. x y

Читаем: «функция от x, которая применяет x к y».

• x объявлена прямо тут, как параметр. Её значение полностью определяется тем, что мы передадим в функцию. Она связана (bound).
• y не объявлена нигде внутри выражения. Чтобы понять, что это, нужен внешний контекст. Она свободна (free).

Ключевая интуиция, которую стоит запомнить на всю статью:

Имя связанной переменной не имеет значения. λx. x и λq. q — это одна и та же функция, просто параметр назван по-разному. Имя свободной переменной имеет значение. λx. x y и λx. x z — это разные функции: первая тянет из мира y, вторая — z.

Отсюда сразу следует практическое правило: переименовывать связанные переменные можно свободно (это называется альфа-конверсия, подробнее — в https://courses.digitable.life/post/lambda-calculus/03-reductions/), а свободные трогать нельзя никогда.

На картинке — выражение λx. λy. x y z. Каждое вхождение переменной «смотрит вверх» и ищет ближайший λ, который её связывает. x находит внешний λ, y — внутренний, а z не находит ничего и остаётся свободной. Ровно так же работает разрешение имён в вашем языке: интерпретатор идёт по цепочке лексических областей видимости наружу.

Одно имя, разные роли

Тонкость, которая сбивает новичков: свободное и связанное — свойство не переменной, а конкретного её вхождения. Одна и та же буква в одном выражении может быть и той, и другой:

(λx. x) x

• Первое x (после λ) — это объявление параметра, связывающее вхождение.
• Второе x (тело абстракции) — связанное вхождение, оно внутри области действия λx.
• Третье x (аргумент, справа от скобок) — свободное: оно снаружи, λx на него не распространяется.

В коде это выглядит абсолютно привычно:

// x снаружи и x внутри — разные переменные, случайно совпали имена
const x = 5;
const result = ((x) => x)(x);   // применяем identity к внешнему x

x = 5
result = (lambda x: x)(x)   # то же самое

Никто в здравом уме так не пишет, но компилятор с этим справляется без проблем — и мы должны научиться так же.

Строгое определение: множество свободных переменных

Теперь формально. Множество свободных переменных терма M обозначим FV(M). Определение — по структуре терма, три случая (ровно те три конструкции, из которых состоит синтаксис):

FV(x)      = {x}                        переменная свободна сама в себе
FV(M N)    = FV(M) ∪ FV(N)              аппликация: объединяем свободные обеих частей
FV(λx. M)  = FV(M) \ {x}                абстракция: связываем x, убираем его из множества

Три строчки — и всё. Единственная содержательная — третья: λ вычитает своё имя из множества свободных переменных тела.

Симметрично определяются связанные переменные:

BV(x)      = {}
BV(M N)    = BV(M) ∪ BV(N)
BV(λx. M)  = BV(M) ∪ {x}

Разберём FV(λx. λy. x y z) пошагово, снизу вверх — не «очевидно, получаем», а весь путь:

FV(z)                = {z}
FV(y)                = {y}
FV(x)                = {x}
FV(x y)              = FV(x) ∪ FV(y)      = {x, y}
FV((x y) z)          = {x, y} ∪ FV(z)     = {x, y, z}
FV(λy. x y z)        = {x, y, z} \ {y}    = {x, z}
FV(λx. λy. x y z)    = {x, z} \ {x}       = {z}

Итог: свободна только z. Что и было нарисовано на схеме выше.

Тот же обход в виде диаграммы — рекурсия идёт вниз по дереву, множества собираются на обратном пути:

Считаем FV кодом

Это ровно тот обход дерева, который вы напишете в любом интерпретаторе. Представим термы как простые объекты.

// Три конструктора термов
const V   = (name)       => ({ tag: "var", name });          // переменная
const Lam = (param, body) => ({ tag: "lam", param, body });   // абстракция
const App = (fn, arg)     => ({ tag: "app", fn, arg });       // аппликация

function freeVars(t) {
  switch (t.tag) {
    case "var": return new Set([t.name]);
    case "app": return new Set([...freeVars(t.fn), ...freeVars(t.arg)]);
    case "lam": {
      const s = freeVars(t.body);
      s.delete(t.param);          // λ вычитает своё имя
      return s;
    }
  }
}

// λx. λy. x y z
const term = Lam("x", Lam("y", App(App(V("x"), V("y")), V("z"))));
console.log([...freeVars(term)]);   // [ 'z' ]

from dataclasses import dataclass

@dataclass(frozen=True)
class Var:  name: str
@dataclass(frozen=True)
class Lam:  param: str; body: object
@dataclass(frozen=True)
class App:  fn: object; arg: object

def free_vars(t) -> set[str]:
    match t:
        case Var(name):        return {name}
        case App(fn, arg):     return free_vars(fn) | free_vars(arg)
        case Lam(param, body): return free_vars(body) - {param}   # λ вычитает своё имя

term = Lam("x", Lam("y", App(App(Var("x"), Var("y")), Var("z"))))
print(free_vars(term))   # {'z'}

Сложность: обход каждого узла ровно один раз, но объединение множеств стоит денег. Наивная реализация — O(n · k) по времени, где n — число узлов, k — размер множеств; по памяти O(n · k) в худшем случае из-за промежуточных множеств. На практике для учебных термов это неважно, а в настоящих компиляторах свободные переменные кэшируют прямо в узлах дерева.

Замкнутые термы и комбинаторы

Терм, у которого FV(M) = {}, называется замкнутым (closed term), или комбинатором. Такой терм самодостаточен: он не зависит ни от какого внешнего контекста, его значение полностью определено им самим.

Классика:

I = λx. x                     — тождество,           FV(I) = {}
K = λx. λy. x                 — константа,            FV(K) = {}
S = λf. λg. λx. f x (g x)     — «распределитель»,     FV(S) = {}
Ω = (λx. x x) (λx. x x)       — бесконечный цикл,     FV(Ω) = {}

Заметьте: Ω — замкнутый терм, который никогда не сойдётся. Замкнутость не означает «хороший», она означает «ни от чего снаружи не зависит».

Практический смысл: программа целиком — это всегда замкнутый терм. Если после компиляции в вашем терме остались свободные переменные, это в точности ошибка ReferenceError: foo is not defined / NameError: name 'foo' is not defined. Проверка на замкнутость — буквально то, что делает статический анализатор области видимости.

Подстановка

Теперь главное. Запись M[x := N] читается: «терм M, в котором все свободные вхождения x заменены на терм N».

Обратите внимание на слово «свободные» — оно тут не для красоты, оно и есть суть всей операции.

Определение по трём случаям плюс разбор случая абстракции на подслучаи:

1)  x[x := N]        = N                              нашли — заменяем
2)  y[x := N]        = y            если y ≠ x        другая переменная — не трогаем
3)  (P Q)[x := N]    = (P[x := N]) (Q[x := N])        аппликация — рекурсивно в обе части
4)  (λx. P)[x := N]  = λx. P                          параметр совпал — внутри x уже не свободна, стоп
5)  (λy. P)[x := N]  = λy. (P[x := N])                если y ≠ x и y ∉ FV(N)
6)  (λy. P)[x := N]  = λz. (P[y := z][x := N])        если y ≠ x и y ∈ FV(N):
                                                      сначала переименовать y в свежее z

Случаи 1–3 очевидны. Случай 4 — важный: если λ уже связал то же имя, дальше идти незачем, внутри все вхождения x принадлежат этому λ, а не нашему. Случаи 5 и 6 — вот где всё веселье.

Схема принятия решения:

Шаг за шагом: безопасная подстановка

Посчитаем (λy. x y)[x := λa. a]. То есть в функции «применить x к y» заменяем x на тождество.

Шаг 0.  Терм:  λy. x y        Подставляем:  x := λa. a
Шаг 1.  Это абстракция λy. …  Параметр y ≠ x  →  случай 5 или 6
Шаг 2.  FV(λa. a) = {}        y ∉ {} → случай 5, всё безопасно
Шаг 3.  Уходим в тело:        (x y)[x := λa. a]
Шаг 4.  Это аппликация → случай 3:
            x[x := λa. a]  =  λa. a       (случай 1)
            y[x := λa. a]  =  y           (случай 2, y ≠ x)
Шаг 5.  Собираем тело:        (λa. a) y
Шаг 6.  Возвращаем λ:         λy. (λa. a) y

Результат: λy. (λa. a) y. Никто не пострадал.

Шаг за шагом: захват имени

А теперь то же самое, но подставляем терм, в котором есть свободная y. Возьмём классику — комбинатор K = λx. λy. x, применённый к свободной y.

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

Наивно, без проверки на захват:

Шаг 0.  (λx. λy. x) y
Шаг 1.  Бета-редукция: тело (λy. x), подстановка x := y
Шаг 2.  Терм λy. x — абстракция, параметр y ≠ x → идём внутрь (наивно!)
Шаг 3.  x[x := y] = y
Шаг 4.  Собираем:  λy. y

Получили λy. y — тождественную функцию. Но мы ожидали константную! Внешняя, свободная y подлезла под λy и превратилась в связанную. Она сменила смысл: была «та самая y из внешнего мира», стала «параметр этой функции». Это и есть захват.

Правильно, с проверкой (случай 6):

Шаг 0.  (λx. λy. x) y
Шаг 1.  Бета-редукция: тело (λy. x), подстановка x := y
Шаг 2.  Терм λy. x, параметр y ≠ x. Проверяем: FV(y) = {y}, и y ∈ {y} → ОПАСНО
Шаг 3.  Переименовываем связанную y в свежее имя a:
            λy. x  ≡α  λa. x        (x — не y, так что тело не меняется)
Шаг 4.  Теперь параметр a, и a ∉ FV(y) = {y} → случай 5, безопасно
Шаг 5.  Идём внутрь: x[x := y] = y
Шаг 6.  Собираем: λa. y

Получили λa. y — константная функция, всегда возвращающая внешнюю y. Смысл сохранён.

Разница между двумя ответами колоссальна и при этом не видна невооружённым глазом: λy. y и λa. y отличаются одной буквой, но первая — тождество, вторая — константа. Это тот самый класс багов, который тихо портит результат вместо того, чтобы упасть.

Проверьте себя на знакомом коде — вот та же ловушка в JavaScript:

// K-комбинатор
const K = (x) => (y) => x;

const y = "внешний мир";
const f = K(y);
console.log(f("что угодно"));   // "внешний мир" — константа, всё верно

Движок JavaScript не подставляет текст программы, он кладёт значение в окружение (environment) — поэтому захват физически невозможен. Именно поэтому большинство реальных интерпретаторов используют модель окружений, а не текстовую подстановку. Но как только вы начинаете переписывать код — макросы, оптимизации компилятора, инлайнинг, шаблонизаторы — вы возвращаетесь ровно к этой проблеме.

«Свежее имя» — это какое?

В случае 6 нужно новое имя z, которое ни с чем не конфликтует. Формально:

z ∉ FV(P) ∪ FV(N) ∪ {x}

То есть свежее имя не должно встречаться свободно ни в теле, ни в подставляемом терме, ни совпадать с самим x. На практике имена генерируют счётчиком: a0, a1, a2… — это те самые tmp$3 и _v17, которые вы видели в сгенерированном коде и минифицированных бандлах.

Полная реализация подстановки

Соберём всё вместе. Это буквально ядро интерпретатора лямбда-исчисления — и оно короткое.

from itertools import count

_counter = count()

def fresh(base: str) -> str:
    """Генерируем гарантированно новое имя: x -> x#0, x#1, ..."""
    return f"{base}#{next(_counter)}"

def rename(t, old: str, new: str):
    """Переименование связанной переменной (частный случай подстановки на переменную)."""
    return subst(t, old, Var(new))

def subst(t, x: str, n):
    """t[x := n] — подстановка, избегающая захвата."""
    match t:
        # 1) и 2): переменная
        case Var(name):
            return n if name == x else t

        # 3) аппликация — рекурсивно в обе части
        case App(fn, arg):
            return App(subst(fn, x, n), subst(arg, x, n))

        case Lam(param, body):
            # 4) параметр совпал — внутри x уже связана, дальше не идём
            if param == x:
                return t
            # 6) параметр свободен в n — будет захват, переименовываем
            if param in free_vars(n):
                z = fresh(param)
                body = subst(body, param, Var(z))   # α-переименование
                return Lam(z, subst(body, x, n))
            # 5) безопасно
            return Lam(param, subst(body, x, n))

def show(t) -> str:
    match t:
        case Var(name):        return name
        case Lam(param, body): return f"(\\{param}. {show(body)})"
        case App(fn, arg):     return f"({show(fn)} {show(arg)})"

# Тот самый опасный случай: (λy. x)[x := y]
danger = Lam("y", Var("x"))
print(show(subst(danger, "x", Var("y"))))   # (\y#0. y) — захвата не произошло

То же самое на JavaScript:

let counter = 0;
const fresh = (base) => `${base}#${counter++}`;

function subst(t, x, n) {          // t[x := n]
  switch (t.tag) {
    case "var":
      return t.name === x ? n : t;

    case "app":
      return App(subst(t.fn, x, n), subst(t.arg, x, n));

    case "lam": {
      if (t.param === x) return t;                    // случай 4: стоп

      if (freeVars(n).has(t.param)) {                 // случай 6: опасность захвата
        const z = fresh(t.param);
        const renamed = subst(t.body, t.param, V(z)); // α-переименование
        return Lam(z, subst(renamed, x, n));
      }

      return Lam(t.param, subst(t.body, x, n));       // случай 5: безопасно
    }
  }
}

const show = (t) =>
  t.tag === "var" ? t.name
  : t.tag === "lam" ? `(\\${t.param}. ${show(t.body)})`
  : `(${show(t.fn)} ${show(t.arg)})`;

console.log(show(subst(Lam("y", V("x")), "x", V("y"))));  // (\y#0. y)

Сложность: в худшем случае O(n · m), где n — размер терма-приёмника, m — размер подставляемого терма (он может копироваться в каждое вхождение x). Плюс на каждом λ считаются FV(n) — если не кэшировать, это ещё множитель. Отсюда и берётся печально известная «экспоненциальная раздутость» наивных редукторов: подставляем большой терм в несколько мест, потом ещё раз, и терм растёт как снежный ком.

Конвенция Барендрегта: как перестать думать о захвате

В математической литературе (в первую очередь — в каноническом Barendregt, «The Lambda Calculus: Its Syntax and Semantics») принято соглашение:

Все связанные переменные в рассматриваемом терме считаются попарно различными и отличными от всех свободных переменных.

Если это соблюдено, случай 6 никогда не сработает — и подстановка становится тупой заменой букв. Удобно на бумаге; в коде так делать нельзя, потому что после каждой редукции инвариант приходится восстанавливать заново.

Как эту проблему решают в проде: индексы де Брёйна

Радикальное решение: избавиться от имён вообще. Николас де Брёйн предложил представлять переменную числом — сколько λ нужно пройти наружу, чтобы дойти до её связывающего.

Что мы получаем:

• Альфа-эквивалентность становится равенством строк. λx. x и λq. q — оба λ. 0. Сравнение термов на равенство — это ==, без всякого обхода с картой переименований.
• Захват имён невозможен по построению. Имён нет — захватывать нечего.
• Цена: при подставке нужно «сдвигать» (shift) индексы свободных переменных, когда терм переезжает под новый λ. Это отдельная операция, и в ней тоже легко ошибиться, просто ошибки другого рода.

Так устроено внутри реальных систем: ядро Coq, тайпчекер Haskell (GHC использует гибрид — уникальные имена Unique вместо переиспользуемых), и большинство учебных реализаций из книги «Types and Programming Languages» Бенджамина Пирса — там глава 6 целиком посвящена безымянному представлению.

Третий подход, который вы уже видели, — окружения и замыкания. Не подставлять ничего в терм, а нести рядом словарь «имя → значение». Именно так работают интерпретаторы Python, JavaScript, Lisp: f(42) не переписывает тело f, а создаёт новый фрейм. Захвата не бывает, потому что подстановки не бывает. Подробнее — в https://courses.digitable.life/post/lambda-calculus/08-evaluation-strategies/.

Сравнение трёх подходов:

Типичные ошибки

1. Забыть слово «свободные» в определении подстановки. Самая частая. Подстановка заменяет только свободные вхождения. В (λx. x)[x := N] заменять нечего — внутри x связана своим λ.

2. Проверять на захват не тот терм. Смотреть надо на FV(N) — свободные переменные того, что подставляем, — и сверять с параметром абстракции. Не наоборот.

3. Переименовывать свободные переменные. Свободная переменная — это внешняя зависимость. Переименовать её — всё равно что в JavaScript заменить fetch на fetch2: программа станет другой.

4. Генерировать «свежее» имя, не проверив его свежесть. Если брать x', x'', а в терме уже есть x', конфликт вернётся. Либо счётчик, гарантированно уникальный на всю программу, либо честная проверка на вхождение.

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

Упражнения

Решайте с карандашом, ответы ниже. Каждый ответ разобран пошагово.

1. Найдите FV(λx. y (λy. y x)).

2. Вычислите (λy. x)[x := λz. z y].

3. Вычислите ((λx. y x) x)[x := λa. a].

4. Приведите (λx. λy. x y) y к нормальной форме.

5. Приведите (λx. λy. x) ((λz. z) w) к нормальной форме.

6. Замкнут ли терм λf. (λx. f (x x)) (λx. f (x x))?

Ответы

1. FV(λx. y (λy. y x))

FV(x)             = {x}
FV(y)             = {y}
FV(y x)           = {y} ∪ {x}      = {x, y}
FV(λy. y x)       = {x, y} \ {y}   = {x}
FV(y (λy. y x))   = {y} ∪ {x}      = {x, y}
FV(λx. …)         = {x, y} \ {x}   = {y}

Ответ: {y}. Внешнее y свободно; внутреннее y в λy. y x — связанное, это другая переменная с тем же именем.

2. (λy. x)[x := λz. z y]

Шаг 1.  Абстракция λy. …, параметр y, подставляем вместо x. y ≠ x.
Шаг 2.  FV(λz. z y) = ({z} ∪ {y}) \ {z} = {y}. Параметр y ∈ {y} → захват!
Шаг 3.  Переименовываем: λy. x  ≡α  λb. x
Шаг 4.  Теперь b ∉ {y}, безопасно. Идём в тело: x[x := λz. z y] = λz. z y
Шаг 5.  Ответ: λb. (λz. z y)

Наивный (неверный) ответ был бы λy. λz. z y — внешняя y захвачена, смысл потерян.

3. ((λx. y x) x)[x := λa. a]

Шаг 1.  Аппликация → случай 3, работаем отдельно с левой и правой частью.
Шаг 2.  Левая: (λx. y x)[x := λa. a]. Параметр совпал с x → случай 4, стоп.
        Результат: λx. y x (без изменений!)
Шаг 3.  Правая: x[x := λa. a] = λa. a   (случай 1)
Шаг 4.  Ответ: (λx. y x) (λa. a)

Суть: x внутри абстракции связана и подстановке не подлежит, а x снаружи — свободна и заменяется.

4. (λx. λy. x y) y

Шаг 1.  Редекс: (λx. λy. x y) применяется к y. Подстановка: (λy. x y)[x := y]
Шаг 2.  Абстракция λy. …, параметр y ≠ x. FV(y) = {y}. Параметр y ∈ {y} → захват!
Шаг 3.  α-переименование: λy. x y  ≡α  λc. x c
Шаг 4.  Теперь безопасно: (x c)[x := y] = (x[x := y]) (c[x := y]) = y c
Шаг 5.  Собираем: λc. y c
Шаг 6.  Редексов больше нет → нормальная форма.

Ответ: λc. y c. (По эта-правилу это эквивалентно просто y — но это уже тема https://courses.digitable.life/post/lambda-calculus/03-reductions/.) Наивный ответ λy. y y был бы грубо неверным.

5. (λx. λy. x) ((λz. z) w)

Возьмём нормальный порядок — редуцируем самый левый внешний редекс первым.

Шаг 1.  Внешний редекс: (λx. λy. x) применяется к ((λz. z) w).
Шаг 2.  Подстановка: (λy. x)[x := (λz. z) w]
Шаг 3.  FV((λz. z) w) = {} ∪ {w} = {w}. Параметр y ∉ {w} → безопасно, случай 5.
Шаг 4.  Идём в тело: x[x := (λz. z) w] = (λz. z) w
Шаг 5.  Собираем: λy. ((λz. z) w)
Шаг 6.  Внутри остался редекс: (λz. z) w → z[z := w] = w
Шаг 7.  Итог: λy. w

Ответ: λy. w. Обратите внимание: аргумент был вычислен после подстановки — это ленивость нормального порядка. При аппликативном порядке мы бы сначала свернули (λz. z) w → w, а потом подставили — результат тот же, но путь другой. Почему пути иногда дают разные результаты, разбирается в https://courses.digitable.life/post/lambda-calculus/08-evaluation-strategies/.

6. λf. (λx. f (x x)) (λx. f (x x))

FV(x)                       = {x}
FV(x x)                     = {x}
FV(f (x x))                 = {f} ∪ {x}   = {f, x}
FV(λx. f (x x))             = {f, x} \ {x} = {f}
FV(обе половины вместе)     = {f} ∪ {f}   = {f}
FV(λf. …)                   = {f} \ {f}   = {}

Ответ: да, замкнут. Это Y-комбинатор — механизм рекурсии без имён, и мы разберём его целиком в https://courses.digitable.life/post/lambda-calculus/07-recursion-and-y/. Обратите внимание: он замкнут, но нормальной формы не имеет — редуцируется бесконечно.

Мини-итог

• Связанная переменная — параметр, объявленный ближайшим охватывающим λ. Её имя не важно и может быть изменено.
• Свободная переменная — внешняя зависимость терма. Её имя важно и трогать его нельзя.
• Свободное/связанное — свойство вхождения, а не буквы: одна и та же x в разных местах может быть и той, и другой.
• FV(λx. M) = FV(M) \ {x} — вся суть связывания в одной строке.
• Терм без свободных переменных — замкнутый терм, он же комбинатор. Ваша скомпилированная программа обязана быть замкнутой.
• M[x := N] заменяет только свободные вхождения x.
• Если параметр абстракции входит в FV(N), наивная подстановка захватит свободную переменную и молча изменит смысл терма. Лекарство — переименовать связанную переменную свежим именем перед спуском внутрь.
• В настоящих системах проблему обходят тремя способами: свежие имена, индексы де Брёйна, окружения и замыкания.

Источники и что почитать

• Benjamin C. Pierce, Types and Programming Languages, главы 5–6 — самое аккуратное изложение подстановки и безымянного представления: https://www.cis.upenn.edu/~bcpierce/tapl/
• Henk Barendregt, The Lambda Calculus: Its Syntax and Semantics — канон, глава 2 про подстановку и конвенцию о переменных.
• Стэнфордская философская энциклопедия, статья The Lambda Calculus: https://plato.stanford.edu/entries/lambda-calculus/
• Peter Sestoft, Demonstrating Lambda Calculus Reduction — с онлайн-редуктором, где можно пошагово прогонять свои термы: https://www.itu.dk/people/sestoft/lamreduce/
• Про гигиену макросов как прикладную версию этой задачи — Rust Reference, Macros By Example / Hygiene.

Если хочется закрепить со стороны практики — посмотрите, как замыкания и свободные переменные устроены в курсе https://courses.digitable.life/post/functional-programming/00-overview/; формальная сторона (индукция по структуре, множества, отношения эквивалентности) разобрана в курсе https://courses.digitable.life/post/mathematics/00-overview/.

Что дальше

Мы разобрали, как подставлять корректно. Осталось назвать вещи своими именами: переименование связанной переменной — это альфа, подстановка аргумента в тело — это бета, а есть ещё эта, которая объясняет, почему λx. f x и f — это одно и то же. Три преобразования, из которых состоит абсолютно всё лямбда-исчисление.

Альфа, бета и эта: три преобразования, из которых всё состоит