Calculo Lambda

Cálculo Lambda

Introdução Na lógica matemática e na ciência da computação, lambda calculus ou cálculo lambda, também escrito como cálculo­λ é um sistema formal que aborda funções recursivas computáveis, em relação a teoria da computação, e fenômenos relacionados, como variáveis ligadas e substituição. A principal característica do cálculo lambda é tratar funções como
“cidadãos de primeira classe”, isto é, entidades que podem ser, como um dado qualquer, utilizadas como argumentos e retornadas como valores de outras funções. O cálculo lambda é uma união de diversos sistemas formais que se baseiam numa notação para funções criada por Alonzo Church, em 1936, com a finalidade de capturar os aspectos básicos das combinações de operadores ou funções para formar outros operadores. O cálculo lambda atua como um elo entre linguagens funcionais de alto nível e suas implementações de baixo nível. É uma linguagem muito simples, consistindo apenas de algumas poucas construções sintáticas e de uma semântica simples, por isso sua implementação necessita suportar algumas poucas construções simples. Pela simplicidade de sua semântica é possível analisar facilmente a corretude de sua implementação. É uma linguagem expressiva, que é suficientemente poderosa para expressar todos os programas funcionais e, consequentemente, todas as funções computáveis. Isso significa que se uma boa implementação do cálculo lambda é disponível, é possível implementar qualquer linguagem funcional através da implementação de um compilador dela para o cálculo lambda.

Definição Formal
A linguagem do cálculo lambda usa um alfabeto S constituído de: ●

um conjunto de variáveis: v
, v
, v
,....v
....
0
1
2
n

●

abstrator λ (lambda)

●

agrupadores (.)

Ao conjunto de cadeias finitas