Variable lliure i variable lligada

En les matemàtiques i en atres disciplines que involucren llenguages formals, incloses la llògica matemàtica i l'informàtica, una variable lliure és una notació (un símbol) que específica llocs en una expressió a on una substitució pot produir-se i no és un paràmetro d'esta o qualsevol expressió contenidor. Alguns llibres antics usen térmens com a variable real i variable aparent per a referir-se a variables lliures i variables lligades, respectivament. L'idea és relacionar a un marcador de posició (un símbol que despuix serà reemplaçat per algun valor) o un caràcter comodí que representa un símbol no especificat.

En programació, el terme variable lliure fa referència a variables usades en una funció que no són variables locals ni paràmetros d'eixa funció. El terme variable no local és a sovint un sinònim en este context.

Una variable lligada és una variable que anteriorment estava lliure, pero que ha segut lligada a un valor específic o conjunt de valors cridat domini de discurs o univers. Per eixemple, la variable x es convertix en una variable lligada quan escrivim:

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

o

Existix un x tal que x² = 2.

En qualsevol d'estes proposicions, no importa llògicament si s'usa x o qualsevol atra lletra. No obstant, pot ser confús tornar a usar la mateixa lletra en una atra part d'alguna proposició composta. És dir, les variables lliures es poden convertir en lligades i, en cert sentit, deixen d'estar disponibles com valores substituts per a atres valors en la creació de fòrmules.

El terme "variable fictícia" s'utilisa també, a voltes, per a una variable lligada (més comuna en matemàtiques generals que en informàtica), pero eixe us pot crear una ambigüitat en la definició de variables fictícies en l'anàlisis de regressió.

Eixemples

Abans d'escomençar a establir una definició precisa de variable lliure i variable lligada, ací hi ha alguns eixemples que potser aclarixquen estos dos conceptes més de lo que ho faria la definició.

En l'expressió:

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

n és la variable lliure i k és la variable lligada; conseqüentment el valor d'esta expressió depén del valor de n, pero no hi ha res cridat k de lo que puga dependre.

En l'expressió:

$\underset{0}{\overset{\mathrm{\infty }}{\int }}{x}^{y-1}{e}^{-x}dx,$

i és la variable lliure i x és la variable lligada; conseqüentment el valor d'esta expressió depén del valor de i, pero no hi ha res cridat x de lo que puga dependre.

En l'expressió:

$\underset{h\to 0}{\lim }\frac{f(x+h)-f(x)}{h},$

x és la variable lliure i h és la variable lligada; conseqüentment el valor d'esta expressió depén del valor de x, pero no hi ha res cridat h de lo que puga dependre.

En l'expressió:

$\mathrm{\forall }x\mathrm{\exists }y[\phi (x,y,z)],$

z és la variable lliure i x i i són les variables lligades, associades en quantificadors llògics; en conseqüència, el valor llògic d'esta expressió depén del valor de z, pero no hi ha res cridat x o i de lo que puga dependre.

Més àmpliament, en la majoria de les demostracions, usem variables lligades. En la següent demostració es prova que cada quadrat d'un número entero parell és divisible per $4$

Siga $n$un número entero parell positiu. Llavors hi ha un número entero $k$ tal que $n=2k$. Ya que $n^2=4k^2$, tenim $n^2$ divisible per $4$.

no solament k sino també n han segut usades com a variables lligades durant tota la demostració.

Operadors d'unió variable

Els següents

$\sum _{x\in S}\prod _{x\in S}\underset{0}{\overset{\mathrm{\infty }}{\int }}\cdots dx\underset{x\to 0}{\lim }\mathrm{\forall }x\mathrm{\exists }x$

són alguns operadors de variables comunes. Cada u d'ells vincula la variable x per a un conjunt S.

Tinga en conte que molts d'estos són operadors que actuen sobre funcions de variables lligades. En contexts més complicats, estes notacions poden tornar-se incómodes i confuses. Pot ser útil canviar a notacions que facen explícit l'enllaç, com

$\sum _{1,\dots ,10}(k\mapsto f(k,n))$

per a sumes o

$D(x\mapsto x^2+2x+1)$

per a diferenciació.

Explicació formal

Arbre que resumix la sintaxis de l'expressió $\mathrm{\forall }x((\mathrm{\exists }yA(x))\vee B(z))$

Els mecanismes de vinculació de variables ocorren en diferents contexts en matemàtiques, llògica i informàtica. En tots els casos, no obstant, són propietats purament sintàctiques d'expressions i variables en elles. Per a esta secció, podem resumir la sintaxis identificant una expressió en un arbre els nodos del qual fulls són variables, constants, funcions constants o predicats constants i, aquells que no són nodos full, com a operadors llògics. Esta expressió pot llavors ser determinada fent un recorregut en l'orde de l'arbre. Els operadors de vinculació de variables són operadors llògics que es troben en casi tots els llenguages formals. Un operador de vinculació Q pren dos arguments: una variable v i una expressió P i, quan s'aplica als seus arguments, es produïx una nova expressió Q(v, P). El significat dels operadors vinculants és proporcionat per la semàntica del llenguage i no concernix ací.

La vinculació de variable relaciona tres coses: una variable "v", una ubicació "a" per a eixa variable en una expressió i un nodo "n" no full de l'arbre de la forma Q(v,P). Nota: definim l'ubicació en una expressió com el nodo full en un arbre sintàctic. La vinculació de la variable ocorre quan esta ubicació està per baix del nodo n.

En el càlcul lambda, x és una variable lligada en el terme M = λx. T és una variable lliure en el terme T. Diem que x és una variable lligada en M i lliure en T. Si T conté un subtérmino λx. O llavors x és un religado en este terme. Es diu que esta unió interna anidada de x "sombrea" l'unió externa. Les aparicions dexenOsón aparicions lliures de la novax.

Les variables lligades al nivell superior d'un programa són, tècnicament, variables lliures dins dels térmens als que estan lligades, pero a sovint es tracten especialment perque poden ser compiladas com a direccions fixes. De manera similar, un identificats vinculat a una funció recursiva és una variable lliure dins del seu propi cos pero és tractada de manera especial

Un terme tancat és aquell que no conté variables lliures.

Expressions de funcions

Per a donar un eixemple des de les matemàtiques, considere una expressió que definix una funció

$f=[(x_1,\dots ,x_n)\mapsto t]$

a on t és una expressió. t pot contindre alguna, totes o cap de les x₁, …, x_n i pot contindre atres variables. En este cas diem que la definició de la funció lliga les variables x₁, …, x_n.

D'esta manera, l'expressió de definició de funcions del tipo que es mostra dalt es pot considerar com l'operador de vinculació de les variables, anàloga a les expressions lambda del càlcul lambda. Atres operadors vinculants, com el signe de suma, poden ser considerats com funcions d'orde superior aplicats a una funció. Aixina que, per eixemple, l'expressió

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

pot ser tractada com una notació para

$\sum _S(x\mapsto x^2)$

a on$\sum _{S}f$ és un operador en dos paràmetros— una funció d'un paràmetro, i un conjunt per a evaluar eixa funció. Els atres operadors enumerats anteriorment poden ser expressats de maneres similars; per eixemple, el quantificador universal $\mathrm{\forall }x\in SP(x)$ es pot considerar com un operador que evalua la conjunció llògica de la funció P en valor booleano aplicat sobre el conjunt (possiblement infinit) S.

Bibliografia

• (1991) Type theory and functional programming, Addison-Wesley. OCLC 23287456. ISBN 0201416670.