mirror of
https://github.com/adambard/learnxinyminutes-docs.git
synced 2024-12-23 17:41:41 +00:00
208 lines
5.6 KiB
Markdown
208 lines
5.6 KiB
Markdown
|
---
|
|||
|
contributors:
|
|||
|
- ["Max Sun", "http://github.com/maxsun"]
|
|||
|
- ["Yan Hui Hang", "http://github.com/yanhh0"]
|
|||
|
translators:
|
|||
|
- ["Gustavo Tramontin", "https://github.com/gustatramontin"]
|
|||
|
---
|
|||
|
|
|||
|
# Cálculo Lambda
|
|||
|
|
|||
|
Cálculo Lambda (cálculo-λ), originalmente criada por
|
|||
|
[Alonzo Church](https://en.wikipedia.org/wiki/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:
|
|||
|
|
|||
|
- Na função `λx.x`, "x" é uma variável ligada porque ela está
|
|||
|
no corpo e em um dos parâmetros da função.
|
|||
|
- Na função `λx.y`, "y" é uma variável livre porque ela não foi definida anteriormente.
|
|||
|
|
|||
|
## Avaliação:
|
|||
|
|
|||
|
Avaliação é realizada por
|
|||
|
[Redução-β](https://en.wikipedia.org/wiki/Lambda_calculus#Beta_reduction),
|
|||
|
que é essencialmente substituição léxica
|
|||
|
|
|||
|
Ao avaliar `(λx.x)a`, todo "x" no corpo da função é substituído por "a".
|
|||
|
|
|||
|
- `(λx.x)a` avalia para: `a`
|
|||
|
- `(λx.y)a` avalia para: `y`
|
|||
|
|
|||
|
Você ainda pode criar funções de ordem superior
|
|||
|
|
|||
|
- `(λx.(λy.x))a` avalia para: `λy.a`
|
|||
|
|
|||
|
Tradicionalmente funções no cálculo lambda possuem um único parâmetro,
|
|||
|
porém usando a técnina de [currying](https://en.wikipedia.org/wiki/Currying)
|
|||
|
podes criar funções com múltiplos argumentos.
|
|||
|
|
|||
|
- `(λx.λy.λz.xyz)` equivale a `f(x, y, z) = ((x y) z)`
|
|||
|
|
|||
|
À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`
|
|||
|
|
|||
|
* `T` e `F` para Verdade e Falso respectivamente.
|
|||
|
|
|||
|
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](https://en.wikipedia.org/wiki/Church_encoding).
|
|||
|
|
|||
|
Para todo número n: <code>n = λf.f<sup>n</sup></code> 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](http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf)
|
|||
|
2. [Cornell CS 312 Recitation 26: The Lambda Calculus](http://www.cs.cornell.edu/courses/cs3110/2008fa/recitations/rec26.html)
|
|||
|
3. [Wikipedia - Lambda Calculus](https://en.wikipedia.org/wiki/Lambda_calculus)
|
|||
|
4. [Wikipedia - SKI combinator calculus](https://en.wikipedia.org/wiki/SKI_combinator_calculus)
|
|||
|
5. [Wikipedia - Iota and Jot](https://en.wikipedia.org/wiki/Iota_and_Jot)
|