Variable libre y variable ligada

En las matemáticas y en otras disciplinas que involucran lenguajes formales, incluidas la lógica matemática y la informática, una variable libre es una notación (un símbolo) que específica lugares en una expresión donde una sustitución puede producirse y no es un parámetro de esta o cualquier expresión contenedora. Algunos libros antiguos usan términos como variable real y variable aparente para referirse a variables libres y variables ligadas, respectivamente. La idea es relacionar a un marcador de posición (un símbolo que después será reemplazado por algún valor) o un carácter comodín que representa un símbolo no especificado.

En programación, el término variable libre hace referencia a variables usadas en una función que no son variables locales ni parámetros de esa función. El término variable no local es a menudo un sinónimo en este contexto.

Una variable ligada es una variable que anteriormente estaba libre, pero que ha sido ligada a un valor específico o conjunto de valores llamado dominio de discurso o universo. Por ejemplo, la variable x se convierte en una variable ligada cuando escribimos:

Para todo x, (x + 1)² = x² + 2x + 1.

o

Existe un x tal que x² = 2.

En cualquiera de estas proposiciones, no importa lógicamente si se usa x o cualquier otra letra. Sin embargo, puede ser confuso volver a usar la misma letra en otra parte de alguna proposición compuesta. Es decir, las variables libres se pueden convertir en ligadas y, en cierto sentido, dejan de estar disponibles como valores sustitutos para otros valores en la creación de fórmulas.

El término "variable ficticia" se utiliza también, a veces, para una variable ligada (más común en matemáticas generales que en informática), pero ese uso puede crear una ambigüedad con la definición de variables ficticias en el análisis de regresión.

Ejemplos

Antes de empezar a establecer una definición precisa de variable libre y variable ligada, aquí hay algunos ejemplos que quizás aclaren estos dos conceptos más de lo que lo haría la definición.

En la expresión:

${\displaystyle \sum _{k=1}^{10}f(k,n),}$ 

n es la variable libre y k es la variable ligada; consecuentemente el valor de esta expresión depende del valor de n, pero no hay nada llamado k de lo que pueda depender.

En la expresión:

${\displaystyle \int _{0}^{\infty }x^{y-1}e^{-x}\,dx,}$ 

y es la variable libre y x es la variable ligada; consecuentemente el valor de esta expresión depende del valor de y, pero no hay nada llamado x de lo que pueda depender.

En la expresión:

${\displaystyle \lim _{h\rightarrow 0}{\frac {f(x+h)-f(x)}{h}},}$ 

x es la variable libre y h es la variable ligada; consecuentemente el valor de esta expresión depende del valor de x, pero no hay nada llamado h de lo que pueda depender.

En la expresión:

${\displaystyle \forall x\ \exists y\ {\Big [}\varphi (x,y,z){\Big ]},}$ 

z es la variable libre y x e y son las variables ligadas, asociadas con cuantificadores lógicos; en consecuencia, el valor lógico de esta expresión depende del valor de z, pero no hay nada llamado x o y de lo que pueda depender.

Más ampliamente, en la mayoría de las demostraciones, usamos variables ligadas. En la siguiente demostración se prueba que cada cuadrado de un número entero par es divisible por ${\displaystyle 4}$ 

Sea ${\displaystyle n}$ un número entero par positivo. Entonces hay un número entero ${\displaystyle k}$  tal que ${\displaystyle n=2k}$ . Dado que ${\displaystyle n^{2}=4k^{2}}$ , tenemos ${\displaystyle n^{2}}$  divisible por ${\displaystyle 4}$ .

no solo k sino también n han sido usadas como variables ligadas durante toda la demostración.

Operadores de unión variable

Los siguientes

${\displaystyle \sum _{x\in S}\quad \quad \prod _{x\in S}\quad \quad \int _{0}^{\infty }\cdots \,dx\quad \quad \lim _{x\to 0}\quad \quad \forall x\quad \quad \exists x}$ 

son algunos operadores de variables comunes. Cada uno de ellos vincula la variable x para un conjunto S.

Tenga en cuenta que muchos de estos son operadores que actúan sobre funciones de variables ligadas. En contextos más complicados, estas notaciones pueden volverse incómodas y confusas. Puede ser útil cambiar a notaciones que hagan explícito el enlace, como

${\displaystyle \sum _{1,\ldots ,10}\left(k\mapsto f(k,n)\right)}$ 

para sumas o

${\displaystyle D\left(x\mapsto x^{2}+2x+1\right)}$ 

para diferenciaciones.

Explicación formal

 

Árbol que resume la sintaxis de la expresión ${\displaystyle \forall x\,((\exists y\,A(x))\vee B(z))}$ 

Los mecanismos de vinculación de variables ocurren en diferentes contextos en matemáticas, lógica e informática. En todos los casos, sin embargo, son propiedades puramente sintácticas de expresiones y variables en ellas. Para esta sección, podemos resumir la sintaxis identificando una expresión con un árbol cuyos nodos hojas son variables, constantes, funciones constantes o predicados constantes y, aquellos que no son nodos hoja, como operadores lógicos. Esta expresión puede entonces ser determinada haciendo un recorrido en el orden del árbol. Los operadores de vinculación de variables son operadores lógicos que se encuentran en casi todos los lenguajes formales. Un operador de vinculación Q toma dos argumentos: una variable v y una expresión P y, cuando se aplica a sus argumentos, se produce una nueva expresión Q(v, P). El significado de los operadores vinculantes es proporcionado por la semántica del lenguaje y no concierne aquí.

La vinculación de variable relaciona tres cosas: una variable "v", una ubicación "a" para esa variable en una expresión y un nodo "n" no hoja del árbol de la forma Q(v,P). Nota: definimos la ubicación en una expresión como el nodo hoja en un árbol sintáctico. La vinculación de la variable ocurre cuando esta ubicación esta por debajo del nodo n.

En el cálculo lambda, x es una variable ligada en el término M = λx. T es una variable libre en el término T. Decimos que x es una variable ligada en M y libre en T. Si T contiene un subtérmino λx. U entonces x es un religado en este término. Se dice que esta unión interna anidada de x "sombrea" la unión externa. Las apariciones dexenUson apariciones libres de la nuevax.^[1]​

Las variables ligadas al nivel superior de un programa son, técnicamente, variables libres dentro de los términos a los que están ligadas, pero a menudo se tratan especialmente porque pueden ser compiladas como direcciones fijas. De manera similar, un identificados vinculado a una función recursiva es una variable libre dentro de su propio cuerpo pero es tratada de manera especial

Un término cerrado es aquel que no contiene variables libres.

Expresiones de funciones

Para dar un ejemplo desde las matemáticas, considere una expresión que define una función

${\displaystyle f=\left[(x_{1},\ldots ,x_{n})\mapsto t\right]}$ 

donde t es una expresión. t puede contener alguna, todas o ninguna de las x₁, …, x_n y puede contener otras variables. En este caso decimos que la definición de la función liga las variables x₁, …, x_n.

De esta manera, la expresión de definición de funciones del tipo que se muestra arriba se puede considerar como el operador de vinculación de las variables, análoga a las expresiones lambda del cálculo lambda. Otros operadores vinculantes, como el signo de suma, pueden ser considerados como funciones de orden superior aplicados a una función. Así que, por ejemplo, la expresión

${\displaystyle \sum _{x\in S}{x^{2}}}$ 

puede ser tratada como una notación para

${\displaystyle \sum _{S}{(x\mapsto x^{2})}}$ 

donde${\displaystyle \sum _{S}{f}}$  es un operador con dos parámetros— una función de un parámetro, y un conjunto para evaluar esa función. Los otros operadores enumerados anteriormente pueden ser expresados de maneras similares; por ejemplo, el cuantificador universal ${\displaystyle \forall x\in S\ P(x)}$  se puede considerar como un operador que evalúa la conjunción lógica de la función P con valor booleano aplicado sobre el conjunto (posiblemente infinito) S.

Referencias

1. Thompson, 1991, p. 33.

Bibliografía

• Thompson, Simon (1991). Type theory and functional programming. Wokingham, England: Addison-Wesley. ISBN 0201416670. OCLC 23287456. 

Enlaces externos

• Esta obra contiene una traducción derivada de «Free variables and bound variables» de la Wikipedia en inglés, publicada por sus editores bajo la Licencia de documentación libre de GNU y la Licencia Creative Commons Atribución-CompartirIgual 3.0 Unported.

•   Datos: Q935944