Связанные и свободные переменные

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

\mathrm{FV}(x) = \{x\}, \qquad \mathrm{FV}(\lambda x.\,M) = \mathrm{FV}(M)\setminus\{x\}, \qquad \mathrm{FV}(M\,N) = \mathrm{FV}(M)\cup\mathrm{FV}(N)

(1.2)

У одиночной переменной $x$ свободна сама $x$ . В абстракции $\lambda x.\,M$ переменная $x$ связывается ближайшей лямбдой, поэтому из свободных переменных тела $M$ её надо убрать. В применении $M\,N$ свободные переменные берутся из обеих частей: всё свободное в $M$ плюс всё свободное в $N$ . Терм без свободных переменных называется замкнутым, или комбинатором; при этом одна и та же буква может встретиться и свободно, и связанно, например, в $x\,(\lambda x.\,x)$ .

Напомню, что терм представляет собой дерево, а переменные — листья. Так вот, в листья можно подставлять, в свою очередь, поддеревья, то есть термы. Такая операция называется подстановкой. Вот несколько примеров таких подстановок:

x[x{:=}N] = N, \qquad y[x{:=}N] = y \;\; (y \neq x)

(1.3)

(M_1\,M_2)[x{:=}N] = M_1[x{:=}N]\;M_2[x{:=}N]

(1.4)

(\lambda y.\,M)[x{:=}N] = \lambda y.\,M[x{:=}N], \qquad y \neq x,\; y \notin \mathrm{FV}(N)

(1.5)

Вот видите, появились уже какие-то ограничения. А почему? Тут есть важная тонкость. Например, если условие $y \notin \mathrm{FV}(N)$ нарушено, свободная переменная «захватывается» чужой абстракцией:

(\lambda y.\,x)[x{:=}y] \neq \lambda y.\,y \quad\text{— смысл изменился!}

Лекарство — α-конверсия, но об этом чуть позже.