Variable libre

Vérifier si une variable (mathématique) dans un terme est libre ou bien est muette revient à tenter de satisfaire l'un des trois critères suivants[1] :

1. Remplacer la variable étudiée par une autre « lettre » vierge (qui n'apparaît pas initialement dans l'expression). Si l'on obtient une expression synonyme alors la variable initiale était liée (α-conversion) ;
2. S'il est possible de trouver une expression synonyme d'où la variable a complètement disparu, alors la variable est muette ;${\displaystyle {\begin{aligned}\int _{0}^{1}x{\rm {d}}x&={\frac {1}{2}}\\\sum _{k=0}^{5}{2^{k}}&=2^{0}+2^{1}+2^{2}+2^{3}+2^{4}+2^{5}=63\end{aligned}}}$
3. Repérer un signe qui rend la variable muette, on parle alors de signes mutificateurs.

${\displaystyle \sum _{x\in S}\quad \quad \prod _{x\in S}\quad \quad \int _{0}^{\infty }\cdots {\rm {d}}x\quad \quad \lim _{x\to 0}\quad \quad \forall x\quad \quad \exists x\quad \quad \lambda x\quad \quad \psi x}$

L'ensemble des variables libres en lambda-calcul, noté ${\displaystyle FV(t)}$, est défini par induction sur les λ-termes :

${\displaystyle FV(x)=\{x\}}$

${\displaystyle FV(tu)=FV(t)\cup FV(u)}$

${\displaystyle FV(\lambda x.t)=FV(t)\setminus \{x\}.}$

Dans l'expression

${\displaystyle \forall x,f(x)=f(y)}$

la variable ${\displaystyle x}$ n'est pas libre (on dit qu'elle est liée), tandis que la variable ${\displaystyle y}$ est libre. Dans l'expression

${\displaystyle \int _{0}^{1}z^{2}xdz}$

la variable ${\displaystyle z}$ est liée, tandis que la variable ${\displaystyle x}$ est libre. Dans l'expression qui suit x est une variable muette mais y est une variable libre car on « parle » de y.

${\displaystyle \int _{0}^{\infty }x^{y-1}{\rm {e}}^{-x}{\rm {d}}x.}$

Dans la fonction ${\displaystyle \lambda u.\lambda t.(uvt)}$, les variables ${\displaystyle u}$ et ${\displaystyle t}$ sont liées, tandis que la variable ${\displaystyle v}$ est libre. En effet,

${\displaystyle FV(uvt)=FV(u)\cup FV(v)\cup FV(t)=\{u,v,t\}}$

et donc

${\displaystyle FV(\lambda u.\lambda t.(uvt))=FV(\lambda t.(uvt))\setminus \{u\}=FV(uvt)\setminus \{u\}\setminus \{t\}}$

${\displaystyle \qquad \qquad \qquad \quad =\{u,v,t\}\setminus \{u\}\setminus \{t\}=\{v\}.}$