Variables Libres

La noción de variable libre es fundamental para entender el significado de las expresiones en el cálculo lambda. Una variable es libre en una expresión si no está ligada por una abstracción.

$$\begin{aligned} \FV(x) &:= \{ x \}\\ \FV(\app{M}{N}) &:= \FV(M) \cup \FV(N)\\ \FV(\lam{x}{M}) &:= \FV(M) \setminus \{ x \} \end{aligned}$$

Veamos algunos ejemplos:

$\FV(\lam{x}{y}) = \ldots$

$\{x\}$ $x$ es el identificador ligado al $\lambda$. $\{y\}$ $\{x, y\}$ $x$ es el identificador ligado al $\lambda$. $\FV(\app{\lam{y}{y}}{x}) = \ldots$ $\{x\}$ $x$ es el identificador ligado al $\lambda$. $\{y\}$ $y$ es el identificador ligado al $\lambda$. $\{x, y\}$ $x$ es el identificador ligado al $\lambda$. $\FV(\app{(\lam{y}{y})}{(\lam{x}{x})}) = \ldots$ $\emptyset$ $\{x, y\}$ Ambos identificadores están ligados por sus respectivos $\lambda$. $\FV(\app{(\lam{y}{x})}{(\lam{x}{x})}) = \ldots$ $\emptyset$ Hay una abstracción con un identificador libre. $\{x\}$ Ambos identificadores están ligados por sus respectivos $\lambda$. $\{x, y\}$ La $x$ de la $\lam{y}{x}$ es libre.