Variable libre

En mathématiques, et dans d'autres disciplines comprenant des langages formels dont la logique mathématique, une variable libre est une notation qui spécifie à quelles places dans une expression une substitution peut avoir lieu. Elle s'oppose à la notion de variable muette (encore appelée variable liée).

En programmation informatique une variable libre est une variable référencée dans une fonction, qui n'est ni une variable locale, ni un paramètre de cette fonction.

Présentation

En mathématiques

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] :

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) ;
S'il est possible de trouver une expression synonyme d'où la variable a complètement disparu, alors la variable est muette ; ${\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}}$
Repérer un signe qui rend la variable muette, on parle alors de signes mutificateurs.

\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

En lambda-calcul

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

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

$FV(tu)=FV(t)\cup FV(u)$

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

Variables libres efficaces

La notion mathématique de variable efficace raffine celle de variable libre. Une variable libre est « inefficace »^{[réf. nécessaire]} lorsque la signification de l'expression dans laquelle elle intervient ne dépend pas de celle de l'objet qui instancie cette variable.

La variable x de l'expression x = x est « inefficace » car x est une variable libre (comme il n'existe aucun signe mutificateur) mais l'énoncé reste vrai quel que soit l'objet désigné par x.

L'expression suivante a en effet pour x, une variable libre efficace : x + 1 = 0.

Exemples

En mathématiques

Dans l'expression

\forall x,f(x)=f(y)

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

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

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

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

En lambda calcul

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

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

et donc

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

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

Notes et références

(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Free variables and bound variables » (voir la liste des auteurs).

« Stage de logique - Notes prises lors du stage de logique animé par René Cori » [PDF], sur Académie de La Réunion, décembre 2009.

Voir aussi

Portail des mathématiques
Portail de l’informatique

Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.

[1] « Stage de logique - Notes prises lors du stage de logique animé par René Cori » [PDF], sur Académie de La Réunion, décembre 2009.