Cálculo lambda

Origem: Wikipédia, a enciclopédia livre.
(Redirecionado de Cálculo Lambda)
Ir para: navegação, pesquisa

Na lógica matemática e na ciência da computação, cálculo lambda, 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 cálculo lambda para computação ficou conhecida como cálculo lambda não-tipado. O cálculo lambda tipado e o não-tipado tem suas idéias 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). Neste artigo, a versão não-tipada será discutida largamente.

História[editar | editar código-fonte]

Cálculo lambda foi apresentada por Alonzo Church na década de 1930 como parte da investigação dos fundamentos da matemática[1] [2] . O sistema original foi demonstrado ser logicamente inconsistente em 1935 quando Stephen Kleene e J. Barkley Rosser desenvolveram o paradoxo Kleene-Rosser.

Em seguida, em 1936, Church isolou e publicou apenas a parte que era relevante para a computação e que depois ficou conhecida como cálculo lambda não-tipado.[3] Em 1940, ele também apresentou uma versão computacionalmente mais fraca, mas com um sistema lógico consistente, conhecido como cálculo lambda simplesmente tipado.[4]

Descrição informal[editar | editar código-fonte]

Motivação[editar | editar código-fonte]

Funções recursivas são um conceito fundamental dentro da ciência da computação e da matemática. O cálculo-λ provê uma semântica simples para computações, permitindo que propriedades da computação fossem estudadas formalmente.

Considere os dois exemplos a seguir. A função identidade

I(x) = x

recebe uma única entrada, x, e imediatamente retorna x (ou seja, a identidade não faz nada com sua entrada), enquanto a função

sqsum(x, y) = x*x + y*y

recebe um par de entradas, x e y e retorna a soma de seus quadrados, x*x + y*y. Usando estes dois exemplos, podemos fazer algumas observações úteis que motivam as principais idéias em cálculo-λ.

A primeira observação é que funções não precisam ser nomeadas explicitamente. Isto é, a função

sqsum(x, y) = x*x + y*y

pode ser reescrita na forma anônima como

(x, y) ↦ x*x + y*y

(leia-se “a tupla x e y é mapeada em x*x + y*y”). Similarmente,

I(x) = x

pode ser reescrita em sua forma anônima para x ↦ x, onde a entrada é simplesmente mapeada para si mesma.

A segunda observação é que a escolha do nome para os argumentos de uma função é totalmente irrelevante. Isto é,

x ↦ x e
y ↦ y

expressam a mesma função: a identidade. De forma similar,

(x, y) ↦ x*x + y*y e
(u, v) ↦ u*u + v*v

também expressam a mesma função.

Finalmente, qualquer função que recebe duas entradas, como a função sqsum do exemplo, pode ser reelaborada numa função equivalente que recebe uma única entrada e tem, como saída, uma outra função, que por sua vez também aceita uma única entrada. Por exemplo,

(x, y) ↦ x*x + y*y

pode ser reelaborada para

x ↦ (y ↦ x*x + y*y)

Esta transformação é chamada currying, e pode ser generalizada para funções que aceitam um número arbitrário de argumentos.

Currying pode ser entendido de forma mais clara através de um exemplo. Compare a função

(x, y) ↦ x*x + y*y

com sua forma "curryficada",

x ↦ (y ↦ x*x + y*y)

Dado dois argumentos, temos:

((x, y) ↦ x*x + y*y)(5, 2)
= 5*5 + 2*2 = 29

No entanto, usando currying, temos:

((x ↦ (y ↦ x*x + y*y))(5))(2)
= (y ↦ 5*5 + y*y)(2)
= 5*5 + 2*2 = 29

e assim vemos que as versões com ou sem currying computam o mesmo resultado. Perceba que x*x se transformou numa constante.

O cálculo lambda[editar | editar código-fonte]

O cálculo lambda consiste de uma linguagem de termos lambda junto com uma teoria equacional (que pode também ser entendida operacionalmente).

Como os nomes de funções são uma mera conveniência, o cálculo lambda não tem interesse em nomear uma função. Já que todas as funções esperando mais de um argumento podem ser transformadas em funções equivalentes recebendo uma única entrada (via Currying), o cálculo lambda não tem interesse em criar funções que aceitam mais de um argumento. E como os nomes dos argumentos são irrelevantes, a noção nativa de igualdade entre termos lambda se chama equivalência-alpha e que demonstra este princípio.

Termos lambda[editar | editar código-fonte]

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 parenteses podem ser usados para tirar ambiguidades entre termos.

Intuitivamente, uma abstração lambda λx.t representa uma função anônima que recebe uma única entrada, e o λ é dito ligar x em t, e uma aplicação ts representa a aplicação da entrada s a uma função t. Em cálculo lambda, 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 y, independentemente da entrada. É importante ressaltar que a aplicação de funções é associativa à esquerda, então (λx.x)y z = ((λx.x)y)z.

Termos lambda por si só não são particularmente interessantes. O que os fazem interessantes são as várias noções de equivalência e redução que podem ser definidas sobre eles.

Alfa-equivalência[editar | editar código-fonte]

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

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.

Definição formal[editar | editar código-fonte]

Expressões lambda são compostas por

variáveis v1, v2, …, vn
símbolos abstratos λ (lambda) e . (ponto)
parênteses ( )

Considerando um número infinito de identificadores: {a, b, c, …, x, y, z, x1, x2, …}, o conjunto de todas as expressões do lambda pode então ser descrito pela seguinte gramática livre de contexto na forma normal de Backus:

<expressão> ::= <identificador>
<expressão> ::= (λ<identificador>. <expressão>)
<expressão> ::= (<expressão> <expressão>)

Os ajustes de lambda, Λ, podem ser definidas recursivamente:

  1. se x é uma variável, então x ∈ Λ
  2. se x é uma variável e M ∈ Λ, então (λx.M) ∈ Λ
  3. se M, N ∈ Λ, então (M N) ∈ Λ

Instâncias da regra 2 são conhecidas como abstrações e instâncias de regra 3 são conhecidas como aplicações.

Outras linguagens puras[editar | editar código-fonte]

Ver também[editar | editar código-fonte]

Referências[editar | editar código-fonte]

  1. A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).
  2. Para saber a história completa, veja "History of Lambda-calculus and Combinatory Logic" (2006), de Cardone e Hindley.
  3. A. Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, Volume 58, No. 2. (Apr., 1936), pp. 345-363.
  4. A. Church, "A Formulation of the Simple Theory of Types", Journal of Symbolic Logic, Volume 5 (1940).
Ícone de esboço Este artigo sobre programação de computadores é um esboço. Você pode ajudar a Wikipédia expandindo-o.