Связанная переменная

Связанная переменная (связанный идентификатор) — в λ-исчислении переменная $v$, входящая в некоторый λ-терм $M$ и удовлетворяющая одному из следующих условий:

1. $M = \lambda v'.M'$, и $v = v'$;
2. $M = (M_1 M_2)$, и $v$ связана в $M_1$ или $M_2$ (то есть один и тот же идентификатор может быть как свободен, так и связан в λ-терме);
3. $M = (M')$, и $v$ связана в $M'$.

Множество переменных $v$, связанных в терме $M$, обозначается как $BV(M)$ (от англ. bounded variable — связанная переменная).

См. также

• Свободная переменная