Uma Introdução a Cálculo Lambda

Este artigo serve como uma uma introdução simples de cálculo lambda.

Definição

Cálculo lambda ou Cálculo λ pode ser chamado a linguagem de programação universal mais pequena do mundo. Foi originalmente desenvolvido pelo Alonzo Church provavelmente entre 1930 e 1940 para uso no estudo de propriedades de funções efectivamente computáveis. Também é uma área de estudo da teoria da computação que faz parte da ciência da computação. Foi introduzido como mecanismo para formalizar o conceito de computação efetiva.

O que é uma função efetivamente computável?

De acordo com a tese de Church-Turing, funções computáveis são exatamente as funções que podem ser calculadas usando um dispositivo mecânico de cálculo dado uma quantidade ilimitada de espaço de armazenamento e de tempo de execução. De maneira equivalente, a mesma tese define que qualquer função que possui um algoritmo é computável. Observe que um algoritmo, neste sentido, é interpretado como sendo uma sequência de passos que uma pessoa, com tempo ilimitado e caneta e papéis infinitos, pode seguir.

Como pode ser definida como linguagem de programação universal?

Cálculo λ é universal no sentido de que qualquer função computável pode ser expressado e avaliado com seu formalismo e é o equivalente da máquina do Turning. Contudo cálculo λ enfatiza o uso de regras de transformações e não se importa com a máquina que implementa as suas funções.

Conceito central de λ Cálculo

O conceito central em cálculo λ é a expressão ou termo lambda. Um “nome” também chamado “variável” é um identificador e, neste caso, pode ser qualquer um das letras a,b,c… Um termo lambda ou expresssão lambda pode ser definida recursivamente das seguintes maneiras:

<expressão> := <nome> | <função> | <aplicação>

<função> := λ<nome>.<expressão>

<aplicação> := <expressão><expressão>

Uma expressão lambda pode estar envolto de parênteses para dar mais clareza. Por exemplo T é um termo lambda, (T) é equivalente á T. As únicas palavras chaves usadas na linguagem são λ e o ponto final (.).

Para evitar desordem com parênteses, adotamos a
A convenção que a aplicação é associada a partir da esquerda, isso é, o termo lambda:

é expressado da seguinte maneira:

Com essa definição um único identificador é um termo λ. Um exemplo simples de uma função:

função lambda

Esta expressão identifica a função identidade. O nome após o λ é o identificador do argumento da função. A expressão após o ponto é (Neste caso o x) é chamado o corpo da definição da função.

Podemos aplicar uma função a um termo lambda. Um exemplo de aplicação:

Este é a função identidade aplicado ao y. Parênteses são usadas para evitar ambiguidade. Aplicações são avaliadas por substituir o argumento x (neste caso o y) no corpo da definição da função:

Nesta transformação a notação:

é usado para indicar que todas ocorrências de x serão substituidas com y no lado direto. Os nomes das funções não carregam nenhum significado. São apenas “place holders”, isso é eles identificam como organizar uma função quando é avaliada. Portanto,

e consequentemente. Usamos:

para indicar que quando A é equivalente a B, A é o um sinonimo de B.

No próximo artigo irei abordar sobre variáveis livres e atadas e outros assuntos relacionados com a teoria da computação.

Muito obrigado por ter lido este artigo. Não esqueça de partilhar este artigo com teus amigos no mundo da computação! 😄