O cálculo lambda, nomeado comumente de lambda calculus, formalizado por Alonzo Church na década de 1930, é uma das fundações teóricas da ciência da computação e da lógica matemática.
Seguem os princípios básicos do cálculo lambda:
Abstração
A abstração é a principal característica do cálculo lambda e se refere à definição de funções anônimas. No cálculo lambda, uma função é definida pela notação λx.E, onde:
- λ é o símbolo lambda.
- x é o parâmetro da função.
- E é a expressão que define o corpo da função.
Por exemplo, a expressão λx.x + 1 representa uma função que adiciona 1 a seu argumento.
Aplicação
A aplicação é o processo de chamar uma função com um argumento. No cálculo lambda, a aplicação de uma função a um argumento é representada pela justaposição de duas expressões. Por exemplo, se temos a função: λx.x + 1 e queremos aplicá-la ao argumento 2, escrevemos (λx.x + 1)2
Redução
Redução é o processo de simplificação de expressões no cálculo lambda. Existem várias formas de redução, mas as mais comuns são:
Redução β (Beta): Substitui a variável vinculada na expressão da função pelo argumento fornecido, i.e, (λx.x + 1)2 se reduz a 2 + 1, que é 3.
Redução α (Alpha): Renomeia as variáveis vinculadas para evitar conflitos de nomes, i.e, λx.λx.x pode ser renomeado para λx.λy.y.
Variáveis Livres e Vinculadas
Uma variável é considerada vinculada se está definida dentro do escopo de uma abstração lambda. Caso contrário, é considerada uma variável livre. Por exemplo, na expressão λx.x+y, x é uma variável vinculada e y é uma variável livre.
Substituição
Substituição é o processo de substituir uma variável livre por uma expressão. Se temos uma expressão E e substituímos uma variável x por uma expressão N, representamos isso como E[x := N].
Funções Anônimas
No cálculo lambda, todas as funções são anônimas, o que significa que elas não têm um nome explícito. Isso contrasta com a programação tradicional, onde funções geralmente têm nomes.
Expressividade
O cálculo lambda é extremamente expressivo e pode representar qualquer função computável. Ele é Turing-completo, o que significa que qualquer coisa que pode ser computada por uma máquina de Turing também pode ser computada usando cálculo lambda.
Exemplo de Redução
Considere a função identidade λx.x. Aplicando essa função a um argumento a, temos:
(λx.x)a
Para reduzir isso, substituímos x por a no corpo da função:
a
Este é um exemplo simples de como a aplicação e a redução funcionam no cálculo lambda.
Notação e Como Usar:
Abstração
A notação λx.E define uma função anônima onde x é o parâmetro e E é o corpo da função. É importante notar que:
- O ponto (.) separa o parâmetro do corpo da função.
- As variáveis são case-sensitive.
Por exemplo, λx.x define uma função identidade que retorna o próprio argumento.
Aplicação
Para aplicar uma função a um argumento, simplesmente colocamos a função e o argumento lado a lado. Por exemplo, a aplicação da função identidade λx.x ao argumento a é escrita como (λx.x)a.
Redução β (Beta)
A redução β envolve substituir o parâmetro formal pelo argumento fornecido na aplicação. Considere a função λx.x + 1 aplicada a 2:
(λx.x + 1)2⇒ 2 + 1⇒ 3
Redução α
A redução α é usada para evitar conflitos de nomes, renomeando variáveis vinculadas. Por exemplo, λx.λx.x pode ser renomeado para λx.λy.y para evitar ambiguidades.
Variáveis Livres e Vinculadas
Na expressão λx.x + y, x é vinculado pelo λ enquanto y é livre. Isso significa que y não tem uma definição dentro da expressão e pode ser substituído por outro valor.
Substituição
Se temos uma expressão E e queremos substituir uma variável x por uma expressão N, representamos isso como E[x := N]. Por exemplo, se E = x + y e N = 2, então E[x := 2] resulta em 2 + y.
Exemplo Prático
Vamos considerar a função λx.λy.x + y e aplicá-la aos argumentos 3 e 4:
(λx.λy.x + y)3 ⇒ λy.3 + y
(λy.3 + y)4 ⇒ 3 + 4 ⇒ 7
Neste exemplo, primeiro aplicamos o 3 ao parâmetro x, resultando em uma nova função λy.3 + y. Depois aplicamos o 4 ao parâmetro y, resultando na expressão final 3 + 4, que se reduz a 7.
Fim.