Skip to content

Latest commit

 

History

History
208 lines (163 loc) · 6.29 KB

lambda.org

File metadata and controls

208 lines (163 loc) · 6.29 KB

Cálculo Lambda

1 Introdução para o Cálculo Lambda ($λ$)

Sistema formal proposto por Church e Kleene

  • Base da programação funcional
  • Divide a definição de uma função do seu nome

Visão Rápida

  • Sintaxe: ${λ}x{⋅}x*x$
  • Aplicação a um valor: $(({λ}x{⋅}x*x)2)$ → $2*2$

Cálculo Lambda Puro (não-interpretado)

  • Qualquer identificador é uma expressão lambda
  • Se M e N são expressões lambda, a aplicação de M a N, representada por (M N), também é uma expressão lambda
  • Uma abstração, escrita como $({λ}x{⋅}M)$, onde x é um identificador e M é uma expressão lambda, é também uma expressão lambda

2 Regras Gramaticais

Sintaxe em Formato BNF para expressões Lambda

Exemplos

  • $x$
  • $({λ}x{⋅}x)$
  • $(({λ}x{⋅}x)({λ}y{⋅}y))$
  • $(x{λ}x{⋅}x*y)$

3 Variáveis ligadas são marcadores de lugar

Considerando $({λ}x{⋅}M)$, a variável x é ligada se ela está presente em M

  • $({λ}x{⋅}x)$ e $({λ}x{⋅}x*x)$, onde x é ligada

Se x não está presente em M, ela é uma Variável Livre

  • $({λ}x{⋅}x*y*z)$, onde y e z são livres

Definindo formalmente

  • $livre(x) = x$
  • $livre(M N) = livre(M) \bigcup livre(N)$
  • $livre({λ}x{⋅}M) = livre(M) - \{x\}$

4 Processo de substituição (aplicação)

Considerando $({λ}x{⋅}M)[x ← N]$ Substituir x pela expressão N em M

  • Se as variáveis livres de N não são ligadas em M
  • Caso contrário
    1. Assumir que uma variável y é livre em N e ligada em M
    2. Substitua as ocorrências de y em M por uma nova variável
    3. Repita até que a condição principal se aplique

Exemplos

  • $x[x ← y ] = y$
  • $(xx)[x ← y ] = (yy)$
  • $({λ}x{⋅}(zx))[x ← y ] = (zy)$

Formalização da Substituição: Regras de Redução

  • Redução-$β$ (beta) e Redução-$α$ (alfa)

5 Redução-$β$

Uma aplicação singular de função.

As variáveis livres de N não podem estar ligadas em M

  • Exemplo de Redução-$β$
    • $(({λ}x{⋅}x*x)2) ⇒β [x ← 2] 2*2$
  • Exemplo onde não podemos aplicar a Redução-$β$
    • $(({λ}g.{λ}h.g\ h\ h)h)$

A redução-$α$ resolve esta limitação

6 Redução-$α$

Renomear as variáveis ligadas de uma expressão.

Renomeia x por y em M, se y não aparece em M

  • Aplicando Redução-$α$ ao exemplo anterior
    • $(({λ}g.\underline{{λ}h.g\ h\ h})h) ⇒α [h ← k] (({λ}g.{λ}k.g\ k\ k)h)$
  • Terminando o exemplo com Redução-$β$
    • $((\underline{{λ}g}.{λ}k.g\ k\ k)\underline{h})$
    • $({λ}k.h\ k\ k)$
    • $h$

7 Cálculo Lambda em LPs

  • \alert{LISP/Scheme}
    (testar com sbcl) 
    ((LAMBDA (L) (CAR (CDR L))) '(A B C))      
((LAMBDA (x) (* x x)) 2)
  • \alert{Haskell}
    (testar com ghci) 
    (\l -> head (tail l)) [1, 2, 3]
(\x -> x*x)2
  • \alert{Python} (com recursos funcionais)
    (testar com python) 
    (lambda l: l[1:][0]) ([1, 2, 3])
(lambda x: x*x)(2)

8 Exercícios

Realize reduções-$β$ ao máximo

  • ((\y.((\x.xyz)a))b)
  • ((\x. * x x)5)
  • ((\x. x * x)5)
  • ((\y. ((\x. x + y + z)3))2)
  • ((\v. (\w.w))((\x.x)(y(\z.z))))