Variáveis livres e ligadas

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

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 para um espaço ou espaços em uma expressão, no(s) qual(is) uma certa substituição pode ocorrer, ou em relação ao(s) qual(is) uma operação de (soma ou quantificação, para dar dois exemplos) pode ocorrer. O conceito é semelhante ao de um apelido, uma palavra que identifica e até representa uma certa entidade.

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

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

ou

'Existe x tal que x2 = 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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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 x1, ..., xn e pode também conter outras variáveis. Neste caso dizemos que a definição da função liga as variáveis x1, ..., xn.

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[editar | editar código-fonte]

Bibliografia[editar | editar código-fonte]

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