Playlists
Computabilidade é uma área de estudo central da Ciência da Computação. Ela estuda a possibilidade de resolver um problema seguindo um algoritmo.
Wikipedia - Domínio Público
Cálculo λ
Sistema formal para expressar computação baseado em abstração de funções e aplicação usando apenas atribuições de nomes e substituições .
Criado por Alonzo Church na década de 1930
Problemas associados:
Nas linguagens que vocês aprenderam até agora, temos:
x = x + 1
)Mas do que realmente precisamos para programar?
Cálculo \(\lambda\) Descreve computação apenas utilizando… funções !!
x = x + 1
)Uma linguagem deve ser descrita em função de sua sintaxe e semântica (vocês estudarão isso em compiladores), ou de maneira menos formal, como você escreve e o que significa.
“Whatever the next 700 languages turn out to be, they will surely be variants of lambda calculus.”
Peter Landin, 1966
“The next 700 programming languages”. Communications of the ACM. Association for Computing Machinery. 9 (3): 157–166. https://doi.org/10.1145%2F365230.365257
\
->
e ::= x
| \x -> e
| e1 e2
Um programa é definido por uma expressão e
, ou
termos -\(\lambda\) que podem assumir uma de três formas:
x, y, z
, um nome que assumirá um valor
durante a computação.\x -> e
,x
é o parâmetro formal, e
é o corpo da funçãox
compute e
e1 e2
, aplique o argumento e2
na função e1
(e1(e2)
).e_i
é uma expressão!Qual dos seguintes termos está sintaticamente incorreto?
(a) \(\x -> x) -> y
(b) \x -> x x
(c) \x -> x (y x)
(d) Alternativas a e c
(e) Todas acima
Qual dos seguintes termos está sintaticamente incorreto?
(a) \(\x -> x) -> y
(b) \x -> x x
(c) \x -> x (y x)
(d) Alternativas a e c
(e) Todas acima
Alternativa A
\x -> x -- função identidade
\x -> (\y -> y) -- retorna a função identidade
\f -> f (\x -> x) -- função que aplica seu argumento
-- (que é uma função)
-- na função identidade
\x -> (\y -> y) -- recebe dois args e retorna o segundo
\x -> (\y -> x) -- recebe dois args e retorna o primeiro
original | syntatic sugar |
---|---|
(((e1 e2) e3) e4) |
e1 e2 e3 e4 |
\x -> (\y -> (\z -> e)) |
\x -> \y -> \z -> e |
\x -> \y -> \z -> e |
\x y z -> e |
\x y -> y
Escopo indica a visibilidade de uma variável. Em C, Java:
int x; /* x está visível aqui, mas y não */
{
int y; /* x e y estão visíveis */
}
/* y deixou de existir :( */
\x -> e
x
é uma variávele
é o escopo de x
x
em e
está ligada
(_ bound _) por \x
:\x -> x
\x -> \y -> x
Por outro lado x
está livre (_ free _) se não
está dentro de uma abstração:
x y -- não tem \
\y -> x y -- x vem de outro lugar
(\x -> \y -> x) x -- o segundo x é diferente do primeiro
Na expressão abaixo, x
é ligado ou livre?
(\x -> x) x
O primeiro é ligado e o segundo é livre.
e
não tem variáveis livres, então e
é uma expressão fechada .Qual é a menor expressão fechada possível?
\x -> x
Podemos reescrever as expressões utilizando duas regras:
(\x -> e1) e2 => e1[x := e2]
e1[x := e2]
significa, “e1 com todas as ocorrências livres
de x
substituídas por e2
.”(\x -> e1) e2
, β-reduz para e1[x := e2]
(\x -> x) 2 => 2
(\f -> f (\x -> x)) (somar 1) => (somar 1) (\x -> x)
(\x -> (\y -> y)) 3 => ???
(\x -> (\y -> y)) 3 => \y -> y
\x -> x => \y -> y
Um termo-\(\lambda\) na forma (\x -> e1) e2
é chamado de expressão redutível ( reducible expression ) ou redex
O termo está em sua forma normal se não contém nenhum redex .
Quais dos termos abaixo não está na forma normal?
x
x y
(\x -> x) y
x (\y -> y)
(\x -> x) y
e
é avaliado para e'
se existe uma
sequência de passos:e => e1 => ... => en => e'
e'
seja uma forma normal.-- Exemplo 1
(\x -> x) 3 => 3
--Exemplo 2
(\f -> f (\x -> x)) (\x -> x)
=> (\x -> x) (\x -> x)
=> (\x -> x)
(\x -> x x) (\x -> x x)
=β> (\x -> x x) (\x -> x x)
let OMEGA = (\x -> x x) (\x -> x x)
(\x -> \y -> y) OMEGA
Essa expressão pode ser reduzida pra forma normal? Tente em casa. 😀
Vamos ver como representar o resto dessas funcionalidades com cálculo λ! Comecemos com Booleanos.
Antes, é razoável nos perguntarmos:
Para que utilizamos Verdadeiro e Falso?
if b then e1 else e2
.Nós já implementamos as funções necessárias para essa definição em outros slides 😄
Verdadeiro = \x y -> x
Falso = \x y -> y
IF = \b x y -> b x y
IF Verdadeiro 2 3
=> (\b x y -> b x y) Verdadeiro 2 3
=> (\x y -> Verdadeiro x y) 2 3
=> (\y -> Verdadeiro 2 y) 3
=> Verdadeiro 2 3
=> (\x y -> x) 2 3
=> (\y -> 2) 3
=> 2
Defina as seguintes funções:
NOT = \b -> ???
AND = \b1 b2 -> ???
OR = \b1 b2 -> ???
NOT = \b -> IF b Falso Verdadeiro
AND = \b1 b2 -> IF b1 b2 Falso
OR = \b1 b2 -> IF b1 Verdadeiro b2
IF = \b x y -> b x y
, então:NOT = \b -> IF b Falso Verdadeiro
=> \b -> b Falso Verdadeiro
AND = \b1 b2 -> IF b1 b2 Falso
=> \b1 b2 -> b1 b2 Falso
OR = \b1 b2 -> IF b1 Verdadeiro b2
=> \b1 b2 -> b1 Verdadeiro b2
Linguagens reais tem uma pancada de funcionalidades:
Vamos agora criar registros.
Vamos começar com registros com dois elementos (ou, pares )
Para que e como utilizamos pares?
A API de Pares
Precisamos definir três funções:
PAIR = \x y -> ??? -- Cria um par com elementos x e y
-- { fst : x, snd : y }
FST = \p -> ??? -- Devolve o primeiro elemento
-- p.fst
SND = \p -> ??? -- Devolve o segundo elemento
-- p.snd
Tal que
FST (PAIR abacate banana)
=> abacate
SND (PAIR abacate banana)
=> banana
x
e y
é apenas algo que permite você escolher entre
x
e y
!
x
ou y
PAIR = \x y -> (\b -> IF b x y)
FST = \p -> p Verdadeiro -- Chamando com Verdadeiro, pega o primeiro elemento
SND = \p -> p Falso -- Chamando com Falso, pega o segundo elemento
TRIPLE = \x y z -> ???
FST3 = \t -> ???
SND3 = \t -> ???
TRD3 = \t -> ???
TRIPLE = \x y z -> PAIR x (PAIR y z)
FST3 = \t -> FST t
SND3 = \t -> FST (SND t)
TRD3 = \t -> SND (SND t)
Linguagens reais tem uma pancada de funcionalidades:
Vamos agora representar os números.
Considere os números naturais \(0, 1, 2,\ldots\)
Para que (e como) os utilizamos?
inc
, dec
+, -, *
==
, <
, …ZERO = ???
UM = ???
DOIS = ???
...
N
é codificado como a
chamada de uma função N
vezes:ZERO = ???
UM = \f x -> f x
DOIS = \f x -> f (f x)
TRES = \f x -> f (f (f x))
...
E o ZERO
?
ZERO = ???
UM = \f x -> f x
DOIS = \f x -> f (f x)
TRES = \f x -> f (f (f x))
...
Com que essa definição parece?
ZERO = \f x -> x
UM = \f x -> f x
DOIS = \f x -> f (f x)
TRES = \f x -> f (f (f x))
...
ZERO = \f x -> x
Falso = \x y -> y
Vamos fazer uma função que determina se um número é 0, chamada
isZero
. Para isto, vamos começar pela representação de 0. Usando
nossa representação com ADTs:
zero = \f -> \x -> x
Que é a mesma coisa que \(\text{zero} = \lambda f.\lambda x.x\) usando notaçao matemática.
Em outras palavras, zero
é uma função constante que devolve a
identidade. Se, então aplicarmos zero
a qualquer coisa, vamos
ter como resposta, identidade.
Vamos agora olhar a representação de 1:
um = \ f -> \x -> f x
e de 2:
dois = \ f -> x -> f (f x)
Ou seja, o número n é na verdade quantas vezes aplicamos f
repetidamente em x
. O caso base é o 0 que aplica f
0 vez, ou
seja a identidade.
Agora que sabemos disso, o que acontece se aplicarmos zero (que é uma função lambda) em algo?
zero algo
= (\f -> \x -> x) algo
β=> = \x -> x
Vamos analisar uma função mais elaborada agora.
isZero = \n -> (n (\x -> false)) true
Ou em notação matemática:
\(\text{isZero} = \lambda n. (n (\lambda x. \text{false})) \text{true}\)
Vamos ver o que ocorre quando passamos 0 como parâmetro:
isZero zero
= (\n -> (n (\x -> false)) true) zero
β=> = (zero (\x -> false)) true
= ((\f -> \x -> x) (\x -> false)) true
β=> = (\x -> x) true
β=> = true
E se aplicarmos com 1?
isZero um
= (\n -> (n (\x -> false)) true) um
β=> = (um (\x -> false)) true
= ((\ f -> \x -> f x) (\x -> false)) true
β=> = (\x -> (\x -> false) x) true
β=> = (\x -> false) true
β=> = false
Ou seja, a função isZero
nada mais é que uma função que identifica
se a função recebida como parâmetro é a função identidade (ou seja
0). Como que ela “identifica” isso?
Aplicando n
sobre true
e passando como f
uma função constante que
devolve false
temos que se n
for 0, ele é a identidade que
quando aplicada sobre true
, vai devolver true
, independentemente
de f
. Se por outro lado n
não for a identidade (e portando
diferente de 0) a aplicação de f
vai sempre devolver false
(pq é
constante false
) identificando, portanto, se o número é 0 ou não.
Outra maneira de ver como isso funciona, é revermos o conceito de
booleanos e a razão pela qual um if
desnecessário (você pode usar o
booleano direto como se fosse um if
!). Reveja a seção acima sobre
booleanos caso isso ainda não esteja claro para você. Lembre-se também
que definição de false
é a mesma que zero
! Com isso você consegue
explicar o funcionamento da função isZero
?
Um pouco de aritmética com números de Church
INC
deve adicionar \(1\) ao número n
:INC = \n -> ???
Função INC
deve adicionar \(1\) ao número n
:
INC = \n -> ???
-- Caso mais simples
INC ZERO = UM
Substituindo pelas definições:
INC = \n -> ???
-- Caso mais simples
INC ZERO = UM
INC (\f x -> x) = \f x -> f x
A operação que deve ser feita para encontrar o novo x
é em função do
ZERO
:
INC = \n -> ???
-- Caso mais simples
INC ZERO = UM
INC (\f x -> x) = \f x -> f x
INC (\f x -> x) = \f x -> f ((\f x -> x) ???)
Se eu passar como argumento de ZERO
o f
e o x
, obtemos:
INC = \n -> ???
-- Caso mais simples
INC ZERO = UM
INC (\f x -> x) = \f x -> f x
INC (\f x -> x) = \f x -> f ((\f x -> x) ???)
INC (\f x -> x) = \f x -> f ((\f x -> x) f x)
β=> \f x -> f x = UM
-- Mas se você reparar
INC ZERO = \f x -> f (ZERO f x)
-- Assim, podemos fazer
INC = \n -> \f x -> f (n f x)
Vamos testar!
INC = \n -> \f x -> f (n f x)
INC UM -- Substituindo
(\n -> \f x -> f (n f x)) (\f x -> f x)
β=> \f x -> f ((\f x -> f x) f x)
β=> \f x -> f ((\x -> f x) x)
β=> \f x -> f (f x)
= DOIS
INC DOIS -- Substituindo
(\n -> \f x -> f (n f x)) (\f x -> f (f x))
β=> \f x -> f ((\f x -> f (f x)) f x)
β=> \f x -> f ((\x -> f (f x)) x)
β=> \f x -> f (f (f x))
= TRES
Como implementar a função ADD
?
ADD = \n m -> ???
ADD DOIS UM = TRES
ADD (\f x -> f (f x)) (\f x -> f x) = (\f x -> f (f (f x)))
ADD = \n m -> ???
ADD DOIS UM = TRES
ADD (\f x -> f (f x)) (\f x -> f x) = (\f x -> f (f (f x)))
f
s das parcelasf
a um número já existente: INC
O pulo do gato!
DOIS INC -- Substituindo
= (\f x -> f (f x)) INC
β=> (\x -> INC (INC x)) = SOMA_DOIS
Que é uma função que soma 2
a qualquer número x
!
Será que isso funciona para qualquer caso?
QUATRO INC -- Substituindo
= (\f x -> f (f (f (f x))) INC
β=> (\x -> INC (INC (INC (INC x))) = SOMA_QUATRO
Dado qualquer número x
incrementa x
, 4
vezes.
Agora estamos prontos para fazer a função ADD
!
Como implementar a função ADD
?
ADD = \n m -> n INC m
-- 'n INC' é função que incrementa x recebido como parâmetro n vezes
-- quando aplicada em m incrementa m, n vezes. Ou seja, resulta em m + n
E finalmente vamos terminar vendo como fazer chamadas recursivas.
Wikipedia/Gleb.svechnikov CC BY-SA 4.0
É tão importante que alguns chegam até a tatuá-lo!
Um vídeo um pouco mais “sério”:
Em Haskell, poderíamos escrevê-la da seguinte maneira:
fat x = if x == 0 then 1 else x * fat (x - 1)
-- Ou usando lambda
fat = \x -> if x == 0 then 1 else x * fat (x - 1)
fat
faz referência a si própria por nome!Podemos contornar o problema criando uma nova versão de fat
que
não referencie nomes não definidos pela própria expressão
fat = \f -> \x -> if x == 0 then 1 else x * f (x - 1)
-- Ou usando açúcar sintático
fat = \f x -> if x == 0 then 1 else x * f (x - 1)
Pergunta
Quero calcular fatorial de 3. O que passar como f
na expressão abaixo?
fat ??? 3
fat = \f x -> if x == 0 then 1 else x * f (x - 1)
O mais conveniente seria usar um valor para f
, digamos p
, tal
que
p
≡ fat p
, ou em outras palavras, p n
≡ fat p n
p 3
≡ fat p 3
≡ \(6\)p
seja ponto fixo 1 da
função fat
.Considere a expressão
A = (\x -> f (x x)) (\x -> f (x x))
(\x -> x x) (\x -> x x)
) não é mera coincidênciaLogo:
A = (\x -> f (x x)) (\x -> f (x x))
= f ((\x -> f (x x)) (\x -> f (x x))) -- por redução β
= f A
Ou seja, para todo f , A é ponto fixo de f
!
Podemos, então, finalmente construir o combinador Y (_ Y-combinator _)
O combinador Y nada mais é do que uma expressão \(\lambda\) que devolve um ponto fixo para qualquer função \(\lambda\)
A = (\x -> f (x x)) (\x -> f (x x)) -- Definida acima
Y = \f -> A -- liga a variável f em A
Y = \f -> (\x -> f (x x)) (\x -> f (x x)) -- Combinador Y
Ou, em notação matemática:
\(\lambda f.\,(\lambda x.\, f\enspace (x\enspace x)) \enspace(\lambda x.\, f\enspace (x\enspace x))\)
** Como que é? 🤔 **
f
A
por f A
, ou seja, trocamos uma
expressão que contém apenas A
por outra que avalia f
e que
ainda contém A
Vamos aplicar o combinador Y ao fatorial.
fat = \f x -> if x == 0 then 1 else x * f (x - 1)
Y = \f -> (\x -> f (x x)) (\x -> f (x x))
-- Quero calcular 3!
Y fat 3
= fat (Y fat) 3 -- Pois (Y fat) é ponto fixo de fat!
= (\f x -> if x == 0 then 1 else x * f (x - 1)) (Y fat) 3
= (\x -> if x == 0 then 1 else x * (Y fat) (x - 1)) 3
= if 3 == 0 then 1 else 3 * (Y fat) (3 - 1)
= 3 * (Y fat 2)
= 3 * (fat (Y fat) 2)
= 3 * ((\f x -> if x == 0 then 1 else x * f (x - 1)) (Y fat) 2)
= 3 * ((\x -> if x == 0 then 1 else x * (Y fat) (x - 1)) 2)
= 3 * (if 2 == 0 then 1 else 2 * (Y fat) (2 - 1))
= 3 * (2 * (Y fat) 1)
= 3 * (2 * (Y fat) 1)
= 3 * 2 * ((Y fat) 1)
= 6 * (fat (Y fat) 1)
= 6 * ((\f x -> if x == 0 then 1 else x * f (x - 1)) (Y fat) 1)
= 6 * ((\x -> if x == 0 then 1 else x * (Y fat) (x - 1)) 1)
= 6 * (if 1 == 0 then 1 else 1 * (Y fat) (1 - 1))
= 6 * 1 * ((Y fat) 0)
= 6 * (fat (Y fat) 0)
= 6 * ((\f x -> if x == 0 then 1 else x * f (x - 1)) (Y fat) 0)
= 6 * ((\x -> if x == 0 then 1 else x * (Y fat) (x - 1)) 0)
= 6 * (if 0 == 0 then 1 else 0 * (Y fat) (0 - 1))
= 6 * 1
= 6
Checklist completo!
y = \f -> (\x -> f (x x)) (\x -> f (x x))
Se você tentar criar o combinador Y em Haskell usando a expressão acima você receberá o seguinte erro:
• Occurs check: cannot construct the infinite type: t0 ~ t0 -> t
• In the first argument of ‘x’, namely ‘x’
In the first argument of ‘f’, namely ‘(x x)’
In the expression: f (x x)
• Relevant bindings include
x :: t0 -> t (bound at <interactive>:3:29)
f :: t -> t (bound at <interactive>:3:6)
y :: (t -> t) -> t (bound at <interactive>:3:1)
(x x)
x
é uma função que recebe um parâmetroa
e b
os tipos do seu parâmetro e resultado
respectivamente. Logo:x :: a -> b
-- Como na expressão x é aplicada a x, então:
x :: a
-- Logo a = (a -> b) que é um tipo infinito
Haskell não aceita tipos infinitos pois isso poderia causar problemas (laços infinitos) no verificador de tipos do compilador
Há duas soluções possíveis
Criar um operador de ponto fixo sem usar lambdas
y :: (a -> a) -> a
y f = f (y f)
Forçar o sistema de tipos do Haskell a engolir os tipos na
marra via unsafeCoerce
import Unsafe.Coerce
y :: (a -> a) -> a
y = \f -> (\x -> f (unsafeCoerce x x)) (\x -> f (unsafeCoerce x x))
Os tipos de y
de ambas as soluções são exatamente os mesmos!
Saída do ghci
> fat = \f x -> if x == 0 then 1 else x * f (x - 1)
> import Unsafe.Coerce
> y = \f -> (\x -> f (unsafeCoerce x x)) (\x -> f (unsafeCoerce x x))
> y fat 3
6
> y fat 10
3628800
>
Veja https://rosettacode.org/wiki/Y_combinator para uma lista da implementação do combinador Y em diferentes linguagens de programação.
Estes slides foram preparados para os cursos de Paradigmas de Programação e Desenvolvimento Orientado a Tipos na UFABC.
Este material pode ser usado livremente desde que sejam mantidos, além deste aviso, os créditos aos autores e instituições.
Um \textbf{ponto fixo} de uma função \(f\) é um elemento do domínio de uma função que é mapeado para si mesmo pela função. Por exemplo, \(0,1 \text{ e } -1\) são pontos fixos de \(f(x) = x^3\) pois \(f(0) = 0^3 = 0\), \(f(1) = 1^3 = 1\) e \(f(-1) = -1^3 = -1\). ↩︎