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

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

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

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

См. также

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