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

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

\displaystyle \mathrm{FV}(x)

\displaystyle = \{x\}, \qquad \mathrm{FV}(\lambda x.\,M)

\displaystyle = \mathrm{FV}(M)\setminus\{x\}, \qquad \mathrm{FV}(M\,N)

\displaystyle = \mathrm{FV}(M)\cup\mathrm{FV}(N)

(1.2)

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

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

\displaystyle x[x{:=}N]

\displaystyle = N, \qquad y[x{:=}N]

\displaystyle = y \;\; (y \neq x)

(1.3)

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

\displaystyle = M_1[x{:=}N]\;M_2[x{:=}N]

(1.4)

\displaystyle (\lambda y.\,M)[x{:=}N]

\displaystyle = \lambda y.\,M[x{:=}N], \qquad y

\displaystyle \neq x,\; y

\displaystyle \notin \mathrm{FV}(N)

(1.5)

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

\displaystyle (\lambda y.\,x)[x{:=}y]

\displaystyle \neq \lambda y.\,y \quad\text{— смысл изменился!}

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