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.”