Variáveis livres e ligadas

Em programação de computadores, uma variável livre é uma variável referenciada em uma função, que não é nem uma variável local nem um argumento daquela função.

Em matemática, e em outras disciplinas envolvendo linguagens formais, incluindo a lógica matemática e a ciência da computação, uma variável livre é uma notação que especifica posições (lacunas) em uma expressão onde a substituição pode ocorrer. A ideia está relacionada a um marcador de posição (tal como a lacuna de um formulário) ou a um caractere curinga que representa um símbolo não especificado.

Exemplo: podemos convencionar que asterisco (*) em "Olá *!" é um símbolo-coringa, sendo substituído livremente por "mundo" (resultando em "Olá mundo!"); por "gente", (resultando em "Olá gente!") ou qualquer outra palavra.

A variável x passa a ser uma variável ligada (ou muda), quando escrevemos, por exemplo:

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

ou

'Existe x tal que x² = 2.'

Em ambas proposições, não importa logicamente se usamos x ou alguma outra letra. No entanto, ao optarmos por usar x estamos concordando em não mais usar esta letra para representar um valor específico, ao menos naquela parte da fómula em que ela é ligada. Em outras palavras, uma variável livre perde sua capacidade de indicar valores determinados ao tornar-se ligada.

Exemplos

Antes de começar uma definição precisa de variável livre e variável ligada, nós apresentaremos alguns exemplos que talvez tornem esses dois conceitos mais claros do que a definição tornaria:

Na expressão

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

n é uma variável livre e k é uma variável ligada; conseqüentemente o valor desta expressão depende do valor de n, mas não de k.

Na expressão

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

k aqui é uma variável livre e n é uma variável ligada; conseqüentemente o valor desta expressão depende do valor de k, mas não há coisa alguma chamada n do qual ele dependa.

Na expressão

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

y é uma variável livre e x é uma variável ligada; o valor desta expressão depende de y, mas não de x.

Na expressão

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

x é uma variável livre e h é uma variável ligada; o valor desta expressão depende do valor de x, mas não de algo chamado h.

Na expressão

$\forall x\ \exists y\ \varphi (x,y,z),$

z é uma variável livre, enquanto que x e y são variáveis ligadas; conseqüentemente, o valor lógico desta expressão depende do valor de z, mas não depende de x e nem de y.

Operadores ligadores de variáveis

O seguintes operadores...

$\sum _{x\in S}\,\qquad \qquad \prod _{x\in S}\,\qquad \qquad \int _{\alpha }^{\beta }\cdots \,dx\qquad \qquad \lim _{x\to 0}\,\qquad \qquad \forall x\,\qquad \qquad \exists x$

...são exemplos de operadores ligadores de variáveis. Nos casos acima, ligam variável $x$.

Explicação formal

Mecanismos ligadores de variáveis ocorrem em diferentes contextos na matemática, lógica e na ciência de computação, mas em todos os casos eles expressam propriedades puramente sintáticas das expressões e variáveis nelas contidas. Para esta seção podemos sintetizar a sintaxe identificando uma expressão com uma árvore cujos nós folhas são variáveis, constantes, constantes para função ou constantes para predicado, e cujos nós não-folhas são operadores lógicos. Os operadores ligadores de variáveis são operadores lógicos que ocorrem em quase toda linguagem formal. De fato, linguagens que não os têm costumam ser bem menos expressivas. Um operador ligador Q recebe dois argumentos: uma variável v e uma expressão P, e quando aplicado aos seus argumentos produz uma nova expressão Q(v, P). O significado dos operadores ligadores é dado pela semântica da linguagem e não nos interessa aqui.

Variáveis livres e ligadas em Lógica

Em lógica matemática, o conceito de variáveis livres e ligadas ganha sentido na lógica de primeira ordem e de ordens superiores. Os operadores ligadores de variáveis são os quantificadores $\forall$ e $\exists$.

O significado de uma variável ligada tem relação direta com sua posição na árvore da fórmula. O escopo de um quantificador é toda a árvore que tem esse quantificador por nó raiz. Uma instância de x em uma fórmula será ligada se e somente se estiver contida no escopo de um quantificador que é o nó pai de uma instância de x.

Considere, por exemplo, a árvore da fórmula

$(\forall x(P(x)\land Q(x)))\to (\lnot P(x)\lor Q(y))$

mostrada a seguir:

A árvore de uma fórmula da Lógica de Primeira Ordem

Os dois nós folhas x na sub-árvore que tem nó raiz $\forall$ são variáveis ligadas, pois estão no escopo de $\forall x$. No entanto, o nó folha x na sub-árvore direita de $\to$ é uma variável livre, pois não está no escopo de quantificador algum.

Outros casos

Para dar um exemplo de matemática, considere uma expressão que define a função

$(x_{1},\ldots ,x_{n})\mapsto \operatorname {t}$

onde t é uma expressão, que pode conter todos, alguns ou nenhum dos x₁, ..., x_n e pode também conter outras variáveis. Neste caso dizemos que a definição da função liga as variáveis x₁, ..., x_n.

No cálculo lambda, x é uma variável ligada no termo M = λ x . T, e uma variável livre de T. Dizemos que x é ligada em M e livre em T. Se T contém um subtermo λ x . U então x . Diz-se que esta ligação interna de x "encobre" a externa. Ocorrências de x em U são ocorrências livres de um novo x.

Variáveis ligadas no nível superior de um programa são tecnicamente variáveis livres nos termos para os quais elas são ligadas mas são normalmente tratadas de maneira especial, porque elas podem ser compiladas como endereços fixos. Semelhantemente, um identificador ligado a uma função recursiva é também tecnicamente uma variável livre em seu próprio corpo mas é tratada de maneira especial.

Um termo fechado é aquele que não contém variáveis livres.

Ver também

• Lógica de primeira ordem
• Atribuição (lógica)
• Constante
• Fórmula (lógica)
• Quantificação

Bibliografia

A maior parte deste artigo foi traduzida do artigo homônimo em inglês. Uma pequena parte foi traduzida e adaptada de:

• HUNT, Michael e RYAN, Mark - Logic in Computer Science, Cambridge University Press, 2004