Variable libre

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

En mathématiques, et dans d'autres disciplines comprenant des langages formels dont la logique mathématique, une variable libre ou variable parlante[réf. nécessaire] est une notation qui spécifie à quelles places dans une expression mathématique (en) une substitution peut avoir lieu. Cette idée est liée à celle de marque substitutive (un symbole qui sera plus tard remplacé par une chaîne de caractères), ou de caractère joker qui tient lieu de symbole non spécifié, qui s'oppose à la notion de variable muette ou variable liée.

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

Définition[modifier | modifier le code]

Général[modifier | modifier le code]

Décider si une variable (mathématique) dans un terme est libre ou bien muette revient à satisfaire trois critères[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\begin{align}\int_0^1x{\rm d}x&=\frac12\\\sum_{k=0}^5{2^k}&= 2^0 + 2^1 + 2^2 + 2^3 + 2^4 + 2^5 = 63\end{align}
  3. 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

Exemple du cas ci-dessous, 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[modifier | modifier le code]

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

FV (x)   = \{ x \}

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

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

Variables libres efficaces[modifier | modifier le code]

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.

Note et références[modifier | modifier le code]

(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)

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

Voir aussi[modifier | modifier le code]