Teoria da Computação

...

Na lógica matemática e na ciência da computação, lambda cálculo, também escrito como cálculo-λ é um sistema formal que estuda funções recursivas computáveis, no que se refere a teoria da computabilidade, e fenômenos relacionados, como variáveis ligadas e substituição. Sua principal característica são as entidades que podem ser utilizadas como argumentos e retornadas como valores de outras funções.

A parte relevante de lambda cálculo para computação ficou conhecida como lambda cálculo não-tipado. O lambda cálculo tipado e o não-tipado tem suas ideias aplicadas nos campos da lógica, teoria da recursão (computabilidade) e linguística, e tem tido um grande papel no desenvolvimento da teoria de linguagens de programação (com a versão não-tipada sendo a inspiração original para programação funcional, em particular LISP, e a versão tipada contribuindo para fundamentar modernos sistemas de tipos e linguagens de programação)

O cálculo lambda é uma coleção de diversos sistemas formais baseados em uma notação para funções inventada por Alonzo Chochem 1936 com o intuito de capturar os aspectos mais básicos da maneira pela qual operadores ou funções podem ser combinados para formar outros operadores.

O cálculo lambda serve como uma ponte entre linguagens funcionais de alto nível e suas implementáveis de baixo nível. Raízes para a apresentação do cálculo lambda como uma linguagem intermediária: uma linguagem extremamente simples, consistindo de somente algumas poucas construções sintáticas e de uma semântica simples.

Uma implementação do cálculo lambda necessita somente suportar algumas construções simples.

A sua semântica simples nos permite analisar facilmente a correção de sua implementação.

Trata-se de uma linguagem expressiva, a qual é suficientemente poderosa para expressar todos os programas funcionais e, por conseguinte, todas as funções computáveis. Isto significa que, se uma boa implementação do cálculo lambda é disponível, pode-se implementar qualquer linguagem funcional através da implementação de um compilador desta para o cálculo lambda.

Termos lambda

A sintaxe de termos lambda é particularmente simples. Existem três maneiras de obtê-las:

- Um termo lambda pode ser uma variável, x;

- Se t é um termo lambda, e x é uma variável, então λx.t é um termo lambda (chamado abstração lambda);

- Se t e s são termos lambda, então ts é um termo lambda (chamado aplicação).

Nada mais é termo lambda, apesar de que parênteses podem ser usados para tirar ambiguidades entre termos.

Uma abstração lambda é uma definição de uma função não nomeada que é capaz e receber uma entrada e substitui-la em sua expressão. Define, assim, uma função anônima que recebe e retorna. Por exemplo, é uma abstração lambda para a função usando o termo para. A definição de uma função com a abstração lambda meramente "configura" a função, mas não a invoca. A abstração binds (liga) a variável no termo.

Uma aplicação representa a aplicação de uma função com um argumento, ou seja, ela representa o ato de chamar a função com entrada para produzir.

Em lambda cálculo não existe o conceito de declaração de variáveis. Em uma definição tal qual lambda cálculo trata como uma variável que ainda não foi definida. A abstração lambda é sintaticamente valida, e representa uma função que soma a entrada com o valor ainda não conhecido.

Parênteses podem ser usados para distinguir termos. Por exemplo, e representam diferentes termos (embora eles coincidentemente possam ser reduzidos para o mesmo termo normal). Aqui o primeiro exemplo define uma função que define outra função e retorna o resultado de aplicar x para a função-filha (aplicar a função e então retornar), enquanto o segundo exemplo define uma função que retorna uma função para qualquer entrada e então retorna à aplicação dela a x (retorna uma função e então aplica).

Funções que operam em funções

Em lambda cálculo, funções são consideradas como valores, então elas podem servir de entrada para outras funções, e funções podem retornar funções como saída.

Por exemplo, λx.x representa a função identidade, x ↦ x, e (λx.x)y representa a função identidade aplicada a y. E assim, (λx.y) representa a função constante x ↦ y, uma função que sempre retorna, independentemente da entrada. É importante ressaltar que a aplicação de funções é associativa à esquerda, então (λx.x)y z = ((λx.x)y)z.

O que torna os termos ainda mais interessantes são as várias noções de equivalência e redução que podem ser definidas sobre eles.

Alfa-equivalência

Uma forma básica de equivalência, definida para termos lambda, é chamada de alfa-equivalência.

Ela determina que a escolha da variável ligada, na abstração lambda, não importa (normalmente).

Por exemplo, λx.x e λy.y são termos lambda alfa-equivalentes, representando a mesma função identidade.

Perceba que os termos x e y não são alfa-equivalentes, porque eles não estão ligados por uma abstração lambda.

Em muitos casos, é fácil de identificar termos lambda equivalentes.

As próximas definições serão necessárias para que a definição de beta-redução seja possível.

Variáveis livres

As variáveis livres de um termo são aquelas variáveis que não são ligadas por uma abstração lambda.

Isto é, as variáveis livres de x são apenas x; as variáveis livres de λx.t são as variáveis livres de t, com x removido, e as variáveis livres de ts são a união das variáveis livres de t e s.

Por exemplo, o termo lambda representando a função identidade λx.x não tem variáveis livres, mas a função constante λx.y tem uma única variável livre, y.

Funções recursivas

As funções recursivas (ou funções recursivas