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

Ver resposta

1.5 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

Se desejarmos escrever funções que recebem mais de um argumento podemos escrever:

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

Contudo essa sintaxe pode se tornar inconveniente muito rapidamente. Por isto, utilizaremos a seguinte notação simplificada (açúcares sintáticos) para simplificar a redação dessas expressões:

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

1.6 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.7 Exercício 2

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

(\x -> x) x
Ver resposta

1.8 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

Adaptado de [SK​].

  1. As funções lambda são anônimas, então elas SEMPRE são denotadas pela sua própria expressão escrita de forma completa. Contudo, como convenção de notação (e por conveniência) nesse texto utilizamos sinônimos escritos com todas as letras em maiúsculas para expressões que são utilizadas repetidamente. Exemplo: ZERO, INC, SOMA, Y.

  2. Sempre escritos em letras maiúsculas, os sinônimos como por exemplo \(\text{TESTE} = e_1e_2\) devem ser entendidos como uma expressão completa e fechada. Assim, \(e_0\text{TESTE}\) é o mesmo que \(e_0~(\text{TESTE})\) que é o mesmo que \(e_o~(e_1~e_2)\).

  3. Aplicação de funções é associativa à esquerda. Isso significa que \(e_1e_2e_3\) equivale a \(((e_1~e_2)~e_3)\).

  4. O escopo de uma variável \(x\), como em \(\lambda x\) sempre se estende o máximo possível para a direita. Logo:

    \(\lambda x~.e_1e_2e_3\) é equivalente a \((\lambda x.(e_1e_2e_3))\) e NÃO a \(((\lambda x.e_1e_2)~e_3)\).

    Isso significa que a aplicação de funções tem maior precedência do que definição de funções e que parênteses são necessários para escrever \((\lambda x~.e_1e_2)e_3\), nos casos que \(e_3\) deve ser usado como um argumento para a função \(\lambda x.e_1e_2\) e não parte desta função propriamente dita.

  5. \(\lambda xyz~.e\) é um açúcar sintático para \((\lambda x.(\lambda y.(\lambda z.~e)))\)

Exemplo:

Como a sintaxe do cálculo lambda é realmente minimalista, às vezes pode ser complicado definir exatamente como uma expressão deve ser interpretada. O exemplo abaixo, retirado de [SK]​, ilustra como colocar os parêntes em uma expressão lambda de modo a evidenciar a organização dos termos na seguinte expressão:

\((\lambda n~.\lambda f.\lambda x.f(nfx))(\lambda g.\lambda y.gy)\)

Utilizando a regra 4, primeiramente identificamos as abstrações. Observe que as abstrações do primeiro termo são limitadas pelo conjunto de parênteses:

\((\lambda x~.f(nfx)) \quad (\lambda y~.gy)\)
\((\lambda f~.(\lambda x.f(nfx))) \quad (\lambda g~.(\lambda y.gy))\)
\((\lambda n~.(\lambda f.(\lambda x.f(nfx))))\)

Em seguida, agrupamos as combinações pela associatividade à esquerda (Regra 3) e chegamos à expressão final:

\(((\lambda n~.(\lambda f.(\lambda x.(f((nf)x)))))(\lambda g.(\lambda y.(gy))))\)

1.9 Semântica

Para simplificar ou avaliar uma expressão lambda, efetuamos uma sequência de reduções até que nenhuma redução possa ser mais aplicada. A regra principal para fazer a avaliação/redução de uma expressão lambda é a redução β , que representa a aplicação da função.

Contudo, como a substituição de variáveis livres em uma expressão pode causar capturas, é necessário também que tenhamos um mecanismo para renomear uma variável ligada. A tal operação damos o nome de redução α .

  • 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.10 Redução \(\alpha\)

Redução α Sejam v e w variáveis e e uma expressão lambda. Então uma redução α é definida como:

\v -> e  α=> \w -> e[v := w]
  • Onde e[v := w] significa: “e com todas as ocorrências livres de v substituídas por w”.

Ou de maneira mais simplificada: Reduções α renomeiam as variáveis de uma função para evitar conflitos.

-- Exemplo 1
    \x -> x
α=> \y -> y

-- Exemplo 2
    \y -> (\f -> f x) y
α=> \z -> (\f -> f x) z
α=> \z -> (\g -> g x) z

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

Note que no exemplo 3 acima, apenas as ocorrências livres de x no corpo da função foram substituídas.

1.11 Redução \(\beta\)

Redução β Seja x uma variável, e e1 e e2 expressões lambdas. Então uma redução β é definida como:

(\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.12 Exercício 3

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

1.13 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.14 Exercício 4

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

x
x y
(\x -> x) y
x (\y -> y)
Ver resposta

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

Além das reduções \(\alpha\) e \(\beta\) que são as principais, existem algumas outras (e.g., \(\delta\)) que não entraremos em detalhes neste texto. Abaixo descrevemos brevemente a redução \(\eta\) que para os nossos propósitos de simplificação de expressões pode ser muito útil.

  • Redução η Seja v uma variável, e e uma expressão lambda (denotando uma função). Se v não tem ocorrências livres em e, então:
    \v -> e v
η=> e

Leitura: η=> → “eta-reduz para”.

Esta redução é, na verdade, trivial (e fácil de se enxergar) quando pensamos em funções comuns. Por exemplo: \(f(x, y) = g (x, y), \forall x, y \implies f = g\).

1.16 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?
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 -> ???
Ver resposta

Ainda dá pra melhorar?

Ver resposta

2.3 Checklist

  • Linguagens reais tem uma pancada de funcionalidades:

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

    Vamos agora criar registros.

2.4 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.5 Exercício 6 - Trio/Terno/Tripla

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

2.6 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.7 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.8 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)))
  • 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?

Ver resposta

2.9 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’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

  • p ≡ fat p, ou em outras palavras, p n ≡ fat p n
    • Exemplo: \(3!\) ≡ p 3 ≡ fat 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, como A = f A para todo f , então 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 Exercícios2

  1. Adicione parênteses às expressões abaixo para evidenciar a ordem de avaliação:

    1. \(\lambda x~.~ x~ \lambda y~.yx\)
    2. \((\lambda x~.x)(\lambda y~.~ y)~ \lambda x~.~ x~ (\lambda y~.~ y)~ z\)
    3. \((\lambda f~.\lambda y.~ \lambda z~.~ f~ z~ y~ z)~ p x\)
    4. \(\lambda x~.~ x~ \lambda y~.~ y~ \lambda z~.~ z \lambda w~.~ w~ z~ y~ x\)

  2. Reescreva as expressões do Exercício 1 utilizando a sintaxe de Haskell.

  3. Considere a função DUAS_VEZES = \f x -> f (f x) e a função INC dada. Utilizando-as, defina as funções:

    1. SOMA_QUATRO que devolve o número passado como argumento somado a 4

    2. SOMA_DEZESSEIS que devolve o número passado como argumento somado a 16

    3. SOMA_SESSENTA_E_QUATRO que devolve o número passado como argumento somado a 64

  4. Utilize reduções \(\beta\) (e \(\alpha\) caso ache conveniente) para reduzir as expressões abaixo para a sua forma normal (caso ela exista).

    1. (\ g -> g 5) (\ x -> add x 3)
    2. (\x -> (\ y z -> z y) x) p (\x -> x)
    3. (\x -> x x x) (\x -> x x x)
    4. (\x -> \y -> (add x ((\x -> sub x 3) y))) 5 6
    5. (\c -> c (\a -> \b -> b)) ((\a -> \b -> \f -> f a b) p q)
    6. DUAS_VEZES (\n -> (mul 2 (add n 1))) 5
    7. DUAS_VEZES (DUAS_VEZES (\n -> (mul 2 (add n 1)))) 5
    8. DUAS_VEZES DUAS_VEZES sqr 2
    9. (\x -> ((\z -> (add x x)) ((\x -> \z -> (z 13 x)) 0 div))) ((\x -> (x 5)) sqr)

  5. Utilizandos as funções TRIPLE e TRD3, mostre passo-a-passo que TRD3 (TRIPLE p q r) = r.

  6. O cálculo \(\lambda\) admite funções com apenas um único parâmetro formal. Contudo muitas funções necessitam de um ou mais parâmetros (ex. soma, divisão, …). Para lidar com esses casos temos duas abordagens possíveis: (i) utilizar pares (ou no caso geral, tuplas de tamanho apropriado) de elementos como argumentos; (ii) utilizar a versão curried da função que tem a propriedade de que seus argumentos são fornecidos um por vez. Por exemplo, a expressão 3 + 5 poderia ser escrita como ((ADD 3) 5). Considerando as funções PAIR, FST e SND e as funções abaixo:

    • CURRY = \f x y -> f (PAIR x y)
    • UNCURRY = \f p -> f (FST p) (SND p)

    Mostre que:

    1. CURRY (UNCURRY h) = h
    2. UNCURRY (CURRY h) (PAIR r s) = h (PAIR r s)

  7. Diversas linguagens de programação, em particular as funcionais, fornecem a construção let para criar e inicializar uma variável com um valor. Converta as expressões que usam let abaixo para expressões que usam apenas lambdas.

    1. let x = 5 in let y = (add x 3) in (mul x y)
    2. let a = 7 in let g = λx . (mul a x) in let a = 2 in (g 10)

  8. Forneça a forma normal das expressões do exercício 7.

  9. Baseando-se na implementação de INC e na definição dos números de Church, forneça a implementação da operação MULT = \a b -> ... que recebe dois números inteiros a e b e devolve o valor de a multiplicado por b.

  10. Utilizando o combinador Y, implemente a função recursiva FIB que dado n devolve o n-ésimo número da sequência de Fibonacci. Exemplos:

    • Y FIB ZERO resulta em ZERO
    • Y FIB DOIS resulta em UM
    • Y FIB SEIS resulta em OITO

  11. Utilizando cálculo \(\lambda\) e as funções desenvolvidas nos exercícios anteriores, implemente uma função POT que recebe 2 números inteiros, b e p e que devolva o valor \(b^p\).

6 Para saber mais

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

  2. Adaptados de [SK]​ ↩︎