Programação Funcional - Cálculo Lambda
Lambda calculus é uma estrutura desenvolvida por Alonzo Church em 1930 para estudar cálculos com funções.
Function creation - Church introduziu a notação λx.Epara denotar uma função em que 'x' é um argumento formal e 'E' é o corpo funcional. Essas funções podem ser sem nomes e argumentos únicos.
Function application - Church usou a notação E1.E2 para denotar a aplicação da função E1 para o argumento real E2. E todas as funções estão em um único argumento.
Sintaxe do cálculo lambda
O cálculo Lamdba inclui três tipos diferentes de expressões, ou seja,
E :: = x (variáveis)
| E 1 E 2 (aplicação de função)
| λx.E (criação de função)
Onde λx.E é chamada de abstração Lambda e E é conhecida como expressões λ.
Avaliando Cálculo Lambda
O cálculo lambda puro não possui funções integradas. Vamos avaliar a seguinte expressão -
(+ (* 5 6) (* 8 3))
Aqui, não podemos começar com '+' porque ele opera apenas em números. Existem duas expressões redutíveis: (* 5 6) e (* 8 3).
Podemos reduzir qualquer um primeiro. Por exemplo -
(+ (* 5 6) (* 8 3))
(+ 30 (* 8 3))
(+ 30 24)
= 54
Regra de redução β
Precisamos de uma regra de redução para lidar com λs
(λx . * 2 x) 4
(* 2 4)
= 8
Isso é chamado de redução β.
O parâmetro formal pode ser usado várias vezes -
(λx . + x x) 4
(+ 4 4)
= 8
Quando há vários termos, podemos tratá-los da seguinte maneira -
(λx . (λx . + (− x 1)) x 3) 9
O interior x pertence ao interior λ e o x externo pertence ao externo.
(λx . + (− x 1)) 9 3
+ (− 9 1) 3
+ 8 3
= 11
Variáveis livres e limitadas
Em uma expressão, cada aparência de uma variável é "livre" (para λ) ou "ligada" (para λ).
β-redução de (λx . E) y substitui todo x que ocorre gratuitamente em E com y. Por exemplo -
Redução Alfa
A redução alfa é muito simples e pode ser feita sem alterar o significado de uma expressão lambda.
λx . (λx . x) (+ 1 x) ↔ α λx . (λy . y) (+ 1 x)
Por exemplo -
(λx . (λx . + (− x 1)) x 3) 9
(λx . (λy . + (− y 1)) x 3) 9
(λy . + (− y 1)) 9 3
+ (− 9 1) 3
+ 8 3
11
Teorema de Church-Rosser
O Teorema de Church-Rosser afirma o seguinte -
Se E1 ↔ E2, então existe um E tal que E1 → E e E2 → E. “A redução de qualquer forma pode eventualmente produzir o mesmo resultado.”
Se E1 → E2 e E2 for a forma normal, haverá uma redução de ordem normal de E1 para E2. “A redução de ordem normal sempre produzirá uma forma normal, se houver.”