Cálculo λ


Playlists

1 Cálculo λ

Computabilidade é uma área de estudo central da Ciência da Computação. Ela estuda a possibilidade de resolver um problema seguindo um algoritmo.

  • Modelo matemático de computação criado por Alan Turing em 1936. Consiste de uma Máquina de Estado Finita cuja entrada é provida por uma fita de execução de tamanho arbitrário.
  • A máquina permite ler, escrever, e andar por essa fita.

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

    • Apresentado em 1932 e refinado até 1940 quando apresentou a sua versão tipada.
    • Church foi o orientador de doutorado do Alan Turing, que publicou o paper descrevendo máquinas de Turing em 1936

Wikipedia

Figure 1: On Computable Numbers, With An Application To the Entscheidungsproblem. A. M. Turing

Figure 1: On Computable Numbers, With An Application To the Entscheidungsproblem. A. M. Turing

Figure 2: On Computable Numbers, With An Application To the Entscheidungsproblem. A. M. Turing

Figure 2: On Computable Numbers, With An Application To the Entscheidungsproblem. A. M. Turing

Figure 3: On Computable Numbers, With An Application To the Entscheidungsproblem. A. M. Turing

Figure 3: On Computable Numbers, With An Application To the Entscheidungsproblem. A. M. Turing

Problemas associados:

  • Decisão: verifica se um elemento \(s \in S\) também está contido em \(T\). Exemplo: testar se um número é primo, \(x \in \mathbb{N}, x \in P\).
  • Função: calcular o resultado da aplicação de uma função \(f : S \rightarrow T\). Exemplo: inverter uma string.
  • Busca: verificar se \(x R y\) em uma relação binária \(R\). Exemplo: buscar um clique em um grafo.
  • Otimização: encontrar a solução \(x^*\) entre todas as soluções do espaço de busca \(S\) de tal forma a maximizar ou minimizar uma função \(f(x)\). Exemplo: quanto devo colocar em cada possível investimento para maximizar meus lucros.

1.1 Qual a menor linguagem universal?

Nas linguagens que vocês aprenderam até agora, temos:

  • Atribuição (x = x + 1)
  • Booleanos, inteiros, floats, caracteres,…
  • Condicionais
  • Laços
  • Funções
  • Recursão
  • Ponteiros
  • Objetos, classes

Mas do que realmente precisamos para programar?

Cálculo \(\lambda\) Descreve computação apenas utilizando… funções !!

  • Atribuição (x = x + 1)
  • Booleanos, inteiros, float, caracteres,…
  • Condicionais
  • Laços
  • Funções
  • Recursão
  • Ponteiros
  • Objetos, classes

1.2 Linguagem do Cálculo \(\lambda\)

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.

Wikipedia

“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

1.3 Sintaxe do Cálculo \(\lambda\)

  • Composto de 3 elementos
    • Variáveis
    • Definição de funções
    • Aplicação de funções
  • Em sua sintaxe original a letra grega minúscula lambda (λ) é usada para definir funções. Por exemplo:
    • Função identidade: \(\lambda x.x\)
    • Função que devolve a função identidade: \(\lambda x.(\lambda y.y)\)
  • Nestes slides usamos a sintaxe de Haskell que troca
    • \(\lambda\) por \
    • . por ->
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:

  • Variável: x, y, z, um nome que assumirá um valor durante a computação.
  • Abstração: (ou função anônima ou função \(\lambda\))
    • \x -> e,
    • x é o parâmetro formal, e é o corpo da função
    • para qualquer valor x compute e
  • Aplicação: (ou chamada de função)
    • e1 e2, aplique o argumento e2 na função e1 (e1(e2)).
    • Todo e_i é uma expressão!

1.4 Exercício 1

  • 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

1.5 Resposta - Exercício 1

  • 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

1.6 Exemplos

\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

1.7 Funções de dois ou mais argumentos

\x -> (\y -> y) -- recebe dois args e retorna o segundo
\x -> (\y -> x) -- recebe dois args e retorna o primeiro

1.8 Syntatic Sugar

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

1.9 Escopo de uma variável

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 :( */
  • Na expressão \x -> e
    • x é uma variável
    • A expressão e é o escopo de x
    • Qualquer ocorrência de 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

1.10 Exercício 2

Na expressão abaixo, x é ligado ou livre?

(\x -> x) x

1.11 Resposta - Exercício 2

O primeiro é ligado e o segundo é livre.

1.12 Expressões fechadas

  • Se e não tem variáveis livres, então e é uma expressão fechada .
  • Expressões fechadas também são chamadas de combinadores ( combinators )

Qual é a menor expressão fechada possível?
\x -> x

1.13 Semântica

Podemos reescrever as expressões utilizando duas regras:

  • Passo α: renomeia um parâmetro formal.
  • Passo β: aplica uma expressão utilizando uma variável livre (ou, de maneira mais simples, chama uma função).

1.14 Redução \(\beta\)

(\x -> e1) e2 => e1[x := e2]
  • Onde e1[x := e2] significa, “e1 com todas as ocorrências livres de x substituídas por e2.”
  • Computação por substituição e busca
    • Se você vir uma abstração aplicada a um argumento, pegue o corpo da abstração e substitua todas as ocorrências livres do parâmetro formal pelo argumento
    • Dizemos que (\x -> e1) e2, β-reduz para e1[x := e2]
(\x -> x) 2 => 2

(\f -> f (\x -> x)) (somar 1) => (somar 1) (\x -> x)

1.15 Exercício 3

(\x -> (\y -> y)) 3 => ???

1.16 Resposta 3

(\x -> (\y -> y)) 3 => \y -> y

1.17 Equivalência \(\alpha\)

  • Renomeia as variáveis de uma função para evitar conflito:
\x -> x => \y -> y

1.18 Forma normal (Normal form)

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

1.19 Exercício 4

Quais dos termos abaixo não está na forma normal?

x
x y
(\x -> x) y
x (\y -> y)

1.20 Resposta - Exercício 4

(\x -> x) y

1.21 Avaliação

  • Um termo-\(\lambda\) e é avaliado para e' se existe uma sequência de passos:
e => e1 => ... => en => e'
  • … tal que 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)

1.22 Non-Terminating Evaluation

(\x -> x x) (\x -> x x)
  =β> (\x -> x x) (\x -> x x)
  • Ops… Conseguimos escrever programas que a cada redução nos leva a eles próprios.
  • É impossível chegar a uma forma normal.
  • Este é o combinador Ω ( Ω combinator )
  • O que ocorre se passarmos Ω como argumento para outra função?
let OMEGA = (\x -> x x) (\x -> x x)

(\x -> \y -> y) OMEGA

Essa expressão pode ser reduzida pra forma normal? Tente em casa. 😀

2 Programando com λ

  • Linguagens reais tem uma pancada de funcionalidades:
    • Booleanos
    • Registros (structs, tuplas, …)
    • Números
    • Funções
    • Recursão

Vamos ver como representar o resto dessas funcionalidades com cálculo λ! Comecemos com Booleanos.

  • Como expressamos o conceito de Verdadeiro e Falso utilizando funções?

Antes, é razoável nos perguntarmos:

  • Para que utilizamos Verdadeiro e Falso?

    • Decisões no formato: if b then e1 else e2.
  • Nós já implementamos as funções necessárias para essa definição em outros slides 😄

2.1 Booleanos

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

2.2 Exercício 5

Defina as seguintes funções:

NOT = \b -> ???
AND = \b1 b2 -> ???
OR  = \b1 b2 -> ???

2.3 Resposta 1 - Exercício 5

NOT = \b -> IF b Falso Verdadeiro
AND = \b1 b2 -> IF b1 b2 Falso
OR  = \b1 b2 -> IF b1 Verdadeiro b2
  • Dá pra melhorar?

2.4 Resposta 2 - Exercício 5

  • Sim! Lembre-se que 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

2.5 Checklist

  • Linguagens reais tem uma pancada de funcionalidades:

    • Booleanos
    • Registros (structs, tuplas, …)
    • Números
    • Funções
    • Recursão

    Vamos agora criar registros.

2.6 Registros

  • Vamos começar com registros com dois elementos (ou, pares )

  • Para que e como utilizamos pares?

    • Criamos um par dados dois itens
    • Pegamos o primeiro item de um par
    • Pegamos o segundo item de um par

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
  • Um par de x e y é apenas algo que permite você escolher entre x e y!
    • Ou seja, uma função que recebe um booleano e devolve ou x ou y
    • Onde você já viu isso antes? 😛
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

2.7 Exercício 6 - Trio/Terno/Tripla

  • Como implementar um registro com três valores?
TRIPLE = \x y z -> ???
FST3  = \t -> ???
SND3  = \t -> ???
TRD3  = \t -> ???

2.8 Solução - Exercício 6

TRIPLE = \x y z -> PAIR x (PAIR y z)
FST3  = \t -> FST t
SND3  = \t -> FST (SND t)
TRD3  = \t -> SND (SND t)

2.9 Checklist

  • Linguagens reais tem uma pancada de funcionalidades:

    • Booleanos
    • Registros (structs, tuplas, …)
    • Números
    • Funções
    • Recursão

    Vamos agora representar os números.

2.10 Números Naturais

  • Considere os números naturais \(0, 1, 2,\ldots\)

  • Para que (e como) os utilizamos?

    • Contagem: \(0\), inc, dec
    • Aritmética: +, -, *
    • Comparações: ==, <, …
  • Vamos começar definindo os números:
ZERO = ???
UM   = ???
DOIS = ???
...
  • Números de Church: um número 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

  • Função INC deve adicionar \(1\) ao número n:
INC = \n -> ???

Função INC deve adicionar \(1\) ao número n:

  • Vamos começar olhando o caso mais simples: \(0 + 1\)
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

2.11 Exercício 7

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)))

2.12 Solução - Exercício 7

ADD = \n m -> ???
ADD DOIS UM = TRES
ADD (\f x -> f (f x)) (\f x -> f x) = (\f x -> f (f (f x)))
  • Há uma “transferência”, uma junção da aplicação dos f s das parcelas
  • Nós já temos uma operação que adiciona um f 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

2.13 Checklist

  • Linguagens reais tem uma pancada de funcionalidades:
    • Booleanos
    • Registros (structs, tuplas, …)
    • Números
    • Funções
    • Recursão

E finalmente vamos terminar vendo como fazer chamadas recursivas.

3 O combinador Y

  • Já fizemos algo nessa linha quando falamos do combinador Ω
  • Basta misturarmos a ideia do Ω com uma função que queremos que seja “carregada” junto
  • Haskell Brooks Curry 😄 foi o primeiro a fazê-lo!
    • Haskell foi orientado de doutorado do David Hilbert

Wikipedia/Gleb.svechnikov CC BY-SA 4.0

É tão importante que alguns chegam até a tatuá-lo!

Figure 4: https://www.youtube.com/watch?v=BC8ZAMwfwi4

Figure 4: https://www.youtube.com/watch?v=BC8ZAMwfwi4

Um vídeo um pouco mais “sério”:

Figure 5: Essentials: Functional Programming&rsquo;s Y Combinator - Computerphile - https://www.youtube.com/watch?v=9T8A89jgeTI

Figure 5: Essentials: Functional Programming’s Y Combinator - Computerphile - https://www.youtube.com/watch?v=9T8A89jgeTI

3.1 Recursão - O exemplo do fatorial

  • Queremos escrever uma função fatorial recursiva

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)
  • Contudo, em cálculo \(\lambda\) isso não é possível!
  • Funções são anônimas! 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

  • pfat p, ou em outras palavras, p nfat p n
    • Exemplo: \(3!\) ≡ p 3fat p 3 ≡ \(6\)
  • Ou seja, queremos que p seja ponto fixo 1 da função fat.

3.2 Ponto fixo de funções \(\lambda\)

Considere a expressão

A = (\x -> f (x x)) (\x -> f (x x))
  • Qualquer semelhança com o combinador Ω ((\x -> x x) (\x -> x x)) não é mera coincidência

Logo:

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 é? 🤔 **

3.3 O combinador Y

  • O combinador Y nos permite escrever uma expressão \(\lambda\) cuja avaliação se repete indefinidamente, tal qual o combinador Ω, mas que diferentemente deste faz algo útil durante cada redução: a avaliação da função f
  • O “pulo do gato” está no uso do ponto fixo de funções \(\lambda\) (que pode ser obtido pela simples aplicação de Y a qualquer termo λ) já que podemos trocar 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
  • Linguagens reais tem uma pancada de funcionalidades:
    • Booleanos
    • Registros (structs, tuplas, …)
    • Números
    • Funções
    • Recursão

Checklist completo!

4 Combinador Y em Haskell

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)
  • O problema ocorre pois o sistema de tipos do Haskell não permite tipos infinitos (que é justamente o que o combinador Y é!)
  • Considere a expressão (x x)
    • x é uma função que recebe um parâmetro
    • Sejam a 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
>

4.1 Combinador Y em outras linguagens

Veja https://rosettacode.org/wiki/Y_combinator para uma lista da implementação do combinador Y em diferentes linguagens de programação.

5 Para saber mais

6 Disclaimer

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.


  1. 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\). ↩︎