Variables libres et variables liées

En mathématiques et dans d'autres disciplines impliquant des langages formels , notamment la logique mathématique et l'informatique , une variable peut être dite libre ou liée. Certains ouvrages plus anciens utilisent les termes variable réelle et variable apparente pour désigner respectivement une variable libre et une variable liée . Une variable libre est une notation (un symbole) qui spécifie les endroits d'une expression où une substitution peut avoir lieu et n'est pas un paramètre de cette expression ou d'une expression conteneur. L'idée est liée à un espace réservé (un symbole qui sera ultérieurement remplacé par une valeur) ou à un caractère générique qui représente un symbole non spécifié.

En programmation informatique , le terme variable libre désigne les variables utilisées dans une fonction qui ne sont ni des variables locales ni des paramètres de cette fonction. Le terme variable non locale est souvent synonyme dans ce contexte.

Une instance d'un symbole de variable est liée , en revanche, si la valeur de ce symbole de variable a été liée à une valeur spécifique ou à une plage de valeurs dans le domaine du discours ou de l'univers . Cela peut être réalisé par l'utilisation de quantificateurs logiques, d'opérateurs de liaison de variable ou d'une déclaration explicite des valeurs autorisées pour la variable (comme, "...où est un entier positif".) Un symbole de variable est globalement lié si au moins une occurrence de celui-ci est liée. ^pp.142--143 Étant donné que le même symbole de variable peut apparaître à plusieurs endroits dans une expression, certaines occurrences du symbole de variable peuvent être libres tandis que d'autres sont liées, ^p.78 donc "libre" et "lié" sont d'abord définis pour les occurrences puis généralisés sur toutes les occurrences dudit symbole de variable dans l'expression. Quelle que soit la manière dont cela est fait, la variable cesse d'être une variable indépendante dont dépend la valeur de l'expression, que cette valeur soit une valeur de vérité ou le résultat numérique d'un calcul, ou, plus généralement, un élément d'un ensemble d'images d'une fonction.

Bien que le domaine du discours soit compris dans de nombreux contextes, lorsqu'une plage explicite de valeurs pour la variable liée n'a pas été donnée, il peut être nécessaire de spécifier le domaine afin d'évaluer correctement l'expression. Par exemple, considérons l'expression suivante dans laquelle les deux variables sont liées par des quantificateurs logiques :

Cette expression est évaluée à faux si le domaine de et est celui des nombres réels, mais à vrai si le domaine est celui des nombres complexes.

Le terme « variable fictive » est également parfois utilisé pour une variable liée (plus souvent en mathématiques générales qu'en informatique), mais il ne faut pas le confondre avec le concept de variable fictive, du même nom mais sans rapport, utilisé en statistique, le plus souvent dans l'analyse de régression. ^p.17

Avant d’énoncer une définition précise de la variable libre et de la variable liée, voici quelques exemples qui rendent peut-être ces deux concepts plus clairs que ne le ferait la définition :

Dans l'expression

n est une variable libre et k est une variable liée ; par conséquent, la valeur de cette expression dépend de la valeur de n , mais il n'y a rien appelé k dont elle pourrait dépendre.

Dans l'expression

y est une variable libre et x est une variable liée ; par conséquent, la valeur de cette expression dépend de la valeur de y , mais il n'y a rien appelé x dont elle pourrait dépendre.

Dans l'expression

x est une variable libre et h est une variable liée ; par conséquent, la valeur de cette expression dépend de la valeur de x , mais il n'y a rien appelé h dont elle pourrait dépendre.

Dans l'expression

z est une variable libre et x et y sont des variables liées, associées à des quantificateurs logiques ; par conséquent la valeur logique de cette expression dépend de la valeur de z , mais il n'y a rien appelé x ou y dont elle pourrait dépendre.

Plus généralement, dans la plupart des preuves, des variables liées sont utilisées. Par exemple, la preuve suivante montre que tous les carrés d'entiers pairs positifs sont divisibles par

Soit un entier positif pair. Alors il existe un entier tel que . Puisque , on a divisible par

non seulement k mais aussi n ont été utilisés comme variables liées dans leur ensemble dans la preuve.

Ce qui suit

sont quelques opérateurs de liaison de variables courants. Chacun d'eux lie la variable x à un ensemble S.

La plupart d'entre eux sont des opérateurs qui agissent sur les fonctions de la variable liée. Dans des contextes plus complexes, de telles notations peuvent devenir maladroites et déroutantes. Il peut être utile de passer à des notations qui rendent la liaison explicite, comme

pour des sommes ou

pour la différenciation.

Les mécanismes de liaison de variables se produisent dans différents contextes en mathématiques, en logique et en informatique. Dans tous les cas, cependant, il s'agit de propriétés purement syntaxiques des expressions et des variables qu'elles contiennent. Pour cette section, nous pouvons résumer la syntaxe en identifiant une expression avec un arbre dont les nœuds feuilles sont des variables, des constantes, des constantes de fonction ou des constantes de prédicat et dont les nœuds non feuilles sont des opérateurs logiques. Cette expression peut ensuite être déterminée en effectuant un parcours ordonné de l'arbre. Les opérateurs de liaison de variables sont des opérateurs logiques qui apparaissent dans presque tous les langages formels. Un opérateur de liaison Q prend deux arguments : une variable v et une expression P , et lorsqu'il est appliqué à ses arguments produit une nouvelle expression Q( v , P ). La signification des opérateurs de liaison est fournie par la sémantique du langage et ne nous concerne pas ici.

La liaison de variable concerne trois éléments : une variable v , un emplacement a pour cette variable dans une expression et un nœud non-feuille n de la forme Q( v , P ). Remarque : nous définissons un emplacement dans une expression comme un nœud feuille dans l'arbre syntaxique. La liaison de variable se produit lorsque cet emplacement se trouve sous le nœud n .

Dans le calcul lambda , xest une variable liée dans le terme M = λx. Tet une variable libre dans le terme T. On dit que xest lié dans Met libre dans T. Si Tcontient un sous-terme λx. Ualors xest rebondi dans ce terme. Cette liaison interne imbriquée de xest dite « masquer » la liaison externe. Les occurrences de xdans Usont des occurrences libres du nouveau x.

Les variables liées au niveau supérieur d'un programme sont techniquement des variables libres dans les termes auxquels elles sont liées, mais sont souvent traitées de manière spéciale car elles peuvent être compilées sous forme d'adresses fixes. De même, un identifiant lié à une fonction récursive est également techniquement une variable libre dans son propre corps, mais est traité de manière spéciale.

Un terme fermé est un terme ne contenant aucune variable libre.

Pour donner un exemple mathématique, considérons une expression qui définit une fonction

où t est une expression. t peut contenir tout ou partie des x ₁ , …, x _n ou aucun d' entre eux et peut contenir d'autres variables. Dans ce cas, nous disons que la définition de fonction lie les variables x ₁ , …, x _n .

De cette manière, les expressions de définition de fonction du type présenté ci-dessus peuvent être considérées comme l' opérateur de liaison de variable, analogue aux expressions lambda du calcul lambda . D'autres opérateurs de liaison, comme le signe de sommation , peuvent être considérés comme des fonctions d'ordre supérieur s'appliquant à une fonction. Ainsi, par exemple, l'expression

pourrait être traité comme une notation pour

où est un opérateur à deux paramètres : une fonction à un paramètre et un ensemble sur lequel évaluer cette fonction. Les autres opérateurs listés ci-dessus peuvent être exprimés de manière similaire ; par exemple, le quantificateur universel peut être considéré comme un opérateur qui évalue la conjonction logique de la fonction à valeur booléenne P appliquée sur l'ensemble (éventuellement infini) S .