Compartilhe esta página

Aprenda X em Y Minutos

Onde X=Lambda Calculus

Cálculo Lambda

Cálculo Lambda (cálculo-λ), originalmente criada por Alonzo Church, é a menor linguagem de programação do mundo. Composta apenas por funções, sem números, texto, booleans, ou qualquer outro tipo, apesar dessa limitação, cálculo lambda é capaz de representar qualquer Máquina de Turing!

Cálculo lambda é composto por 3 elementos: variáveis, funções e aplicações.

Nome Sintaxe Exemplo Explicação
Variável <nome> x uma variável chamada "x"
Função λ<parâmetro>.<corpo> λx.x uma função com parâmetro "x" e corpo "x"
Aplicação <função><variável ou função> (λx.x)a aplicando a função "λx.x" ao argumento "a"

A função mais simples é a função indentidade: λx.x equivalente a f(x) = x. O primeiro "x" é o argumento da função, e o segundo o corpo da função.

Variáveis Livres e Ligadas:

Avaliação:

Avaliação é realizada por Redução-β, que é essencialmente substituição léxica

Ao avaliar (λx.x)a, todo "x" no corpo da função é substituído por "a".

Você ainda pode criar funções de ordem superior

Tradicionalmente funções no cálculo lambda possuem um único parâmetro, porém usando a técnina de currying podes criar funções com múltiplos argumentos.

Às vezes λxy.<corpo> é usado como notação para: λx.λy.<corpo>


É importante ressaltar que cálculo lambda não tem números, carácteres, ou qualquer tipo que não seja uma função!

Lógica Booleana:

Cálculo lambda não tem booleans, valores lógicos de "verdade" e "falso".

No lugar temos:

T representado por: λx.λy.x

F representado por: λx.λy.y

Assim representamos os operadores lógicos:

Não a como: λa.a F T

a E b como: λa.λb.a b F

a OU b como: λa.λb.a T b

Números:

Apesar do cálculo lambda não ter números, podemos representa-los usando numerais Church.

Para todo número n: n = λf.fn assim:

0 = λf.λx.x

1 = λf.λx.f x

2 = λf.λx.f(f x)

3 = λf.λx.f(f(f x))

Para incrementar um numeral Church, usamos a função sucessora S(n) = n + 1 definida como:

S = λn.λf.λx.f((n f) x)

Usando-a definimos a função soma:

SOMA = λab.(a S)b

Desafio: defina sua própria função de multiplicação!

Ainda Menor: SKI, SK E Iota

Cálculo Combinador SKI

Seja, S, K, I as funções seguintes:

I x = x

k x y = x

S x y z = x z (y z)

Podemos converter uma expressão no cálculo lambda para uma no cálculo combinador SKI:

  1. λx.x = I
  2. λx.c = Kc desde que x não ocorra livre em c
  3. λx.(y z) = S (λx.y) (λx.z)

Exemplo com numeral church 2:

2 = λf.λx.f(f x)

Para a parte interna λx.f(f x):

  λx.f(f x)
= S (λx.f) (λx.(f x))          (caso 3)
= S (K f)  (S (λx.f) (λx.x))   (caso 2, 3)
= S (K f)  (S (K f) I)         (caso 2, 1)

Então:

  2
= λf.λx.f(f x)
= λf.(S (K f) (S (K f) I))
= λf.((S (K f)) (S (K f) I))
= S (λf.(S (K f))) (λf.(S (K f) I)) (caso 3)

Para o primeiro argumento λf.(S (K f)):

  λf.(S (K f))
= S (λf.S) (λf.(K f))       (caso 3)
= S (K S) (S (λf.K) (λf.f)) (caso 2, 3)
= S (K S) (S (K K) I)       (caso 2, 3)

Para o segundo argumento λf.(S (K f) I):

  λf.(S (K f) I)
= λf.((S (K f)) I)
= S (λf.(S (K f))) (λf.I)             (caso 3)
= S (S (λf.S) (λf.(K f))) (K I)       (caso 2, 3)
= S (S (K S) (S (λf.K) (λf.f))) (K I) (caso 1, 3)
= S (S (K S) (S (K K) I)) (K I)       (caso 1, 2)

Juntando-os:

  2
= S (λf.(S (K f))) (λf.(S (K f) I))
= S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))

Expandindo isso, finalizamos com a mesma expressão para o numeral Church 2.

Cálculo Combinador SK

O cálculo combinador SKI pode ser reduzido ainda mais. Ao notar que I = SKK, podemos remover o combinador I substituindo-o por SKK.

Combinador Iota

Cálculo combinador SK ainda não é mínimo. Definindo:

ι = λf.((f S) K)

Temos:

I = ιι
K = ι(ιI) = ι(ι(ιι))
S = ι(K) = ι(ι(ι(ιι)))

Para leituras mais avançadas:

  1. A Tutorial Introduction to the Lambda Calculus
  2. Cornell CS 312 Recitation 26: The Lambda Calculus
  3. Wikipedia - Lambda Calculus
  4. Wikipedia - SKI combinator calculus
  5. Wikipedia - Iota and Jot

Sugestões ou correções? Abra uma issue no repositório do GitHub, ou faça um pull request você mesmo!

Originalmente contribuído por Max Sun e atualizado por 1 colaborador.