
Introdução ao -calculus
Prof. Gustavo Motta
Departamento de Informática/UFPB
04
(c) 2007 Gustavo Motta
1
-calculus
Sumário
 Definições recursivas e o combinador Y
04
(c) 2007 Gustavo Motta
2
-calculus
Definições recursivas e o
combinador Y
 Definições recursivas


Definição fácil em linguagens de alto nível
Devem ser definíveis no -calculus


Solução formal para equações recursivas
Combinador Y
(Y)E  (E)(Y)E
 para toda expressão- E. Isso implica que
(Y)E  (E)(E)...(E)(Y)E
 para um número qualquer de iterações em E

Questão
 Existe uma expressão- fechada com essa propriedade?
04
(c) 2007 Gustavo Motta
3
-calculus
Definições recursivas e o
combinador Y
 Resposta



04
Sim. A partir da expressão-
(x.(x)x)x.(x)x
que se reduz para ela mesma, ad infinitum,
acrescentamos um prefixo da forma (E)
y.(x.(y)(x)x)x.(y)(x)x
e então
(y.(x.(y)(x)x)x.(y)(x)x)E  (x.(E)(x)x)x.(E)(x)x
que se reduz para
(E)(x.(E)(x)x)x.(E)(x)x
(c) 2007 Gustavo Motta
4
-calculus
Definições recursivas e o
combinador Y
 Logo

O combinador Y é definidor por
Y  y.(x.(y)(x)x)x.(y)(x)x

É uma função de alta ordem que computa o
ponto fixo de outras funções

Usado para encontrar solução para definições
recursivas da forma
f = (E)f

04
com f não ocorrendo livre em E
(c) 2007 Gustavo Motta
5
-calculus
Definições recursivas e o
combinador Y

A solução desta equação
f = (E)f
é o ponto fixo da função de alta ordem E e pode
ser obtida substituindo-se f por (Y)E, obtendo
(Y)E = (E)(Y)E
e essa equação é verdadeira para todo E pela
definição de Y

04
Y passa a ser um achador universal de pontos
fixos, denominado de combinador de ponto fixo
(c) 2007 Gustavo Motta
6
-calculus
Definições recursivas e o
combinador Y
 Exemplo – solução para função fatorial
(fact)n = if n = 0 then 1 else ((*)n)(fact)(pred)n
em notação-
(fact)n = (((zero)n)1)((*)n)(fact)(pred)n
que é equivalente a
fact = n.(((zero)n)1)((*)n)(fact)(pred)n
Agora, abstraindo a ocorrência livre de ‘fact’
fact = (f.n.(((zero)n)1)((*)n)(f)(pred)n)fact
Temos que fact é o ponto fixo da expressão
f.n.(((zero)n)1)((*)n)(f)(pred)n
04
(c) 2007 Gustavo Motta
7
-calculus
Definições recursivas e o
combinador Y
 Exemplo – solução para função fatorial
Logo, a função fatorial é definida pelo combinador
fact = (Y)f.n.(((zero)n)1)((*)n)(f)(pred)n
 Técnica aplicável a toda definição recursiva
 Independe da forma da expressão do lado direito
 O -cálculo possui uma técnica universal de
remoção de recursividade

Aplicável até quando não há solução realística
x=x+1
aplicando-se a técnica, tem-se
x = (Y)x.((+)x)1, que redunda num número infinito de
04
reduções, por não
forma
(c) 2007ter
Gustavo
Motta normal
8
-calculus
Definições recursivas e o
combinador Y
Exemplo – aplicação da função fatorial
((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)5
((f.n.(((zero)n)1)((*)n)(f)(pred)n)(Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)5
(n.(((zero)n)1)((*)n)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)n)5
(((zero)5)1)((*)5)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)5
(((zero)5)1)((*)5)((f.n.(((zero)n)1)((*)n)(f)(pred)n)(Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)5
(((zero)5)1)((*)5)(n.(((zero)n)1)((*)n)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)n)(pred)5
(((zero)5)1)((*)5)(((zero)(pred)5)1)((*)(pred)5)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)(pred)5
((false)1)((*)5)((false)1)((*)(pred)5)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)(pred)5
((*)5)((*)(pred)5)((f.n.(((zero)n)1)((*)n)(f)(pred)n)(Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)(pred)5
((*)5)((*)(pred)5)(n.(((zero)n)1)((*)n)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)n)(pred)(pred)5
((*)5)((*)(pred)5)(((zero)(pred)(pred)5)1)((*)(pred)(pred)5)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)(
pred)(pred)5
((*)5)((*)(pred)5)((false)1)((*)(pred)(pred)5)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)(pred)(pred)5
04
(c) 2007 Gustavo Motta
((*)5)((*)(pred)5)((*)(pred)(pred)5)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)(pred)(pred)5
9
-calculus
Definições recursivas e o
combinador Y
Exemplo – aplicação da função fatorial
((*)5)((*)(pred)5)((*)(pred)(pred)5)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)(pred)(pred)5
((*)5)((*)(pred)5)((*)(pred)(pred)5)((f.n.(((zero)n)1)((*)n)(f)(pred)n)(Y)f.n.(((zero)n)1)((*)n)(f)(pred
)n)(pred)(pred)(pred)5
((*)5)((*)(pred)5)((*)(pred)(pred)5)(n.(((zero)n)1)((*)n)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)n)(p
red)(pred)(pred)5
((*)5)((*)(pred)5)((*)(pred)(pred)5)(((zero)(pred)(pred)(pred)5)1)((*)(pred)(pred)(pred)5)((Y)f.n.(((z
ero)n)1)((*)n)(f)(pred)n)(pred)(pred)(pred)(pred)5
((*)5)((*)(pred)5)((*)(pred)(pred)5)((false)1)((*)(pred)(pred)(pred)5)((Y)f.n.(((zero)n)1)((*)n)(f)(pred
)n)(pred)(pred)(pred)(pred)5
((*)5)((*)(pred)5)((*)(pred)(pred)5)((*)(pred)(pred)(pred)5)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)
(pred)(pred)(pred)5
((*)5)((*)(pred)5)((*)(pred)(pred)5)((*)(pred)(pred)(pred)5)((f.n.(((zero)n)1)((*)n)(f)(pred)n)(Y)f.n.
(((zero)n)1)((*)n)(f)(pred)n)(pred)(pred)(pred)(pred)5
((*)5)((*)(pred)5)((*)(pred)(pred)5)((*)(pred)(pred)(pred)5)(n.(((zero)n)1)((*)n)((Y)f.n.(((zero)n)1)((
*)n)(f)(pred)n)(pred)n)(pred)(pred)(pred)(pred)5
10
04
(c) 2007 Gustavo Motta
-calculus
Definições recursivas e o
combinador Y
Exemplo – aplicação da função fatorial
((*)5)((*)(pred)5)((*)(pred)(pred)5)((*)(pred)(pred)(pred)5)(((zero)(pred)(pred)(pred)(pred)5)1)((*)
(pred)(pred)(pred)(pred)5)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)(pred)(pred)(pred)(pred)5
((*)5)((*)(pred)5)((*)(pred)(pred)5)((*)(pred)(pred)(pred)5)((false)1)((*)(pred)(pred)(pred)(pred)5)((Y)
f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)(pred)(pred)(pred)(pred)5
((*)5)((*)(pred)5)((*)(pred)(pred)5)((*)(pred)(pred)(pred)5)((*)(pred)(pred)(pred)(pred)5)((Y)f.n.(((z
ero)n)1)((*)n)(f)(pred)n)(pred)(pred)(pred)(pred)(pred)5
((*)5)((*)(pred)5)((*)(pred)(pred)5)((*)(pred)(pred)(pred)5)((*)(pred)(pred)(pred)(pred)5)((f.n.(((zer
o)n)1)((*)n)(f)(pred)n)(Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)(pred)(pred)(pred)(pred)5
((*)5)((*)(pred)5)((*)(pred)(pred)5)((*)(pred)(pred)(pred)5)((*)(pred)(pred)(pred)(pred)5)(n.(((zero)n)
1)((*)n)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)n)(pred)(pred)(pred)(pred)(pred)5
((*)5)((*)(pred)5)((*)(pred)(pred)5)((*)(pred)(pred)(pred)5)((*)(pred)(pred)(pred)(pred)5)(((zero)(pred
)(pred)(pred)(pred)(pred)5)1)((*)(pred)(pred)(pred)(pred)(pred)5)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n
)(pred) (pred)(pred)(pred)(pred)(pred)5
((*)5)((*)(pred)5)((*)(pred)(pred)5)((*)(pred)(pred)(pred)5)((*)(pred)(pred)(pred)(pred)5)((true)1)((*)(
pred)(pred)(pred)(pred)(pred)5)((Y)f.n.(((zero)n)1)((*)n)(f)(pred)n)(pred)
11
04
(c) 2007 Gustavo Motta
(pred)(pred)(pred)(pred)(pred)5
-calculus
Definições recursivas e o
combinador Y
Exemplo – aplicação da função fatorial
((*)5)((*)(pred)5)((*)(pred)(pred)5)((*)(pred)(pred)(pred)5)((*)(pred)(pred)(pred)(pred)5)1
((*)5)((*)4)((*)(pred)4)((*)(pred)(pred)4)((*)(pred)(pred)(pred)4)1
((*)5)((*)4)((*)3)((*)(pred)3)((*)(pred)(pred)3)1
((*)5)((*)4)((*)3)((*)2)((*)(pred)2)1
((*)5)((*)4)((*)3)((*)2)((*)1)1
((*)5)((*)4)((*)3)((*)2)1
((*)5)((*)4)((*)3)2
((*)5)((*)4)6
((*)5)24
120
04
(c) 2007 Gustavo Motta
12
-calculus
Definições recursivas e o
combinador Y
 O combinador Y converte toda recursividade em
iteração, mas não é capaz por si mesmo de terminar
a sucessão de iterações
 Paradoxo de Curry


As propriedades lógicas usuais do operador 
(implica) são inconsistentes com a igualdade-
Prova
O operador deve satisfazer o axioma
(P  (P  Q))  (P  Q)
e a regra de inferência modus ponens
04
se ambos P e (P  Q) são verdadeiros, então Q também
é
13
(c) 2007 Gustavo Motta
-calculus
Definições recursivas e o
combinador Y
 Paradoxo de Curry
 Considere que imp denota a versão curried de 

O axioma anterior pode ser escrito como
((imp)((imp)P)((imp)P)Q)((imp)P)Q
Para um Q arbitrário, pode-se definir N como
N = x.((imp)x)((imp)x)Q
sendo
P = (Y)N
o ponto fixo de N. Então, obtém-se
((imp)P)((imp)P)Q = (N)P = (N)(Y)N = P
04
(c) 2007 Gustavo Motta
14
-calculus
Definições recursivas e o
combinador Y
 Paradoxo de Curry
Pela substituição no axioma, tem-se
((imp)((imp)P)((imp)P)Q)((imp)P)Q =
((imp)P)((imp)P)Q = P
Agora, como o axioma deve ser verdadeiro para
quaisquer P e Q
P = (Y)N = true
deve ser o caso para qualquer Q, usado em N
Mas, a partir do modus ponens e do axioma, podese concluir que
Q = true
04
para um Q arbitrário, o que é um paradoxo
(c) 2007 Gustavo Motta
15
-calculus
Definições recursivas e o
combinador Y
 Observações

A aplicabilidade universal do combinador Y não
oferece solução prática para toda equação de
ponto fixo
x = 3x – 10
que é
x = ((–)((*)3)x)10
então, podemos obter
x = (x.((–)((*)3)x)10)x
e a forma explícita
x = (Y)x.((–)((*)3)x)10
04
(c) 2007 Gustavo Motta
16
-calculus
Definições recursivas e o
combinador Y
 Observações
O lado esquerdo da equação
x = (Y)x.((–)((*)3)x)10
reduz para
(x.((–)((*)3)x)10)(Y)x.((–)((*)3)x)10
que reduz para
((–)((*)3)(Y)x.((–)((*)3)x)10)10

04
e assim indefinidamente ...
O lado direito não tem forma normal, logo não se
pode obter um resultado finito desse
desenvolvimento infinito
(c) 2007 Gustavo Motta
17
-calculus
Definições recursivas e o
combinador Y
 Observações

Entretanto, numa recursividade bem fundada, a
iteração gerada pelo combinador Y terminará
precisamente no momento certo


04
É o caso da forma explícita da função fatorial, graças
as presenças da segunda abstração, com prefixo n.,
e do predicado zero
Infelizmente, não é decidível, em geral, se uma
definição recursiva é computável num número
finito de passos (i. e., tem uma forma normal),
quando aplicada a um certo argumento
(c) 2007 Gustavo Motta
18
-calculus
Definições recursivas e o
combinador Y

Existem outros combinadores de ponto fixo, além
do combinador Y, como
T  (x.y.(y)((x)x)y)x.y.(y)((x)x)y
proposto por Turing. É fácil observar que
(T)E  (E)(T)E
para toda expressão- E. De fato, existe uma
seqüência infinita de combinadores de ponto fixo
Y1  Y
Y2  (Y)G, em geral, Yn + 1  (Yn)G
04
onde
G  x.y.(y)(x)y
(c) 2007 Gustavo Motta
19
-calculus
Bibliografia

04
Revesz, G. E. Lambda-Calculus, Combinators, and
Functional Programming. Cambridge University
Press, 1988.
(c) 2007 Gustavo Motta
20