
Introdução ao -calculus
Prof. Gustavo Motta
Departamento de Informática/UFPB
02
(c) 2007 Gustavo Motta
1
-calculus
Sumário
 Redução- e igualdade
 Teorema de Church-Rosser
02
(c) 2007 Gustavo Motta
2
-calculus
Redução- e igualdade
 A regra-
 ()
(x.P)Q  [Q / x]P

Para x, P e Q arbitrários, a expressão- (x.P)Q é
chamada de -redex e o lado direito é chamado
contractum
 O contractum de um -redex é, em geral, mais simples
que o próprio -redex
(x.x)Q  Q
(x.y)Q  y
mas
(x.(x)x)x.(x)x  [x.(x)x / x](x)x  (x.(x)x)x.(x)x
ou seja, o contractum é -congruente com o próprio -redex
02
(c) 2007 Gustavo Motta
3
-calculus
Redução- e igualdade
 Redução-

Definição – A relação M  N (leia M -reduz para
N) é definida por indução como segue
1. M  N se M  N
2. M  N se M  N é uma instância da regra-
3. Se M  N para algum M e N, então para qualquer expressão-
E, (M)E  (N)E e (E)M  (E)N também valem
4. Se M  N para algum M e N, então para qualquer variável x,
x.M  x.N também vale
5. Se M  E e E  N, então M  N também vale
6. M  N apenas para os casos especificados nos itens de 1 a 5
02
(c) 2007 Gustavo Motta
4
-calculus
Redução- e igualdade

M -reduz para N se N é obtido de M pela troca
de uma parte de M com a forma (x.P)Q pelo
contractum [Q / x]P, ou N é obtido de M através
de uma seqüência finita de dessas trocas


A relação  é reflexiva e transitiva, mas não é
simétrica
M  N é invariante sob a conversão-
 Definição - M é -conversível (ou apenas igual) a
N, em símbolos M = N, se e somente se M  N,
ou M  N, ou N  M, ou existe uma
expressão- E tal que M = E e E = N.
02
(c) 2007 Gustavo Motta
5
-calculus
Redução- e igualdade

Noção de igualdade definida de maneira
puramente formal

Não há referência ao sentido, ao significado

Embora seja relevante para o significado
 O significado das expressões- devem ser invariantes sob
a conversão-

Como decidir se duas expressões- são iguais ou não?
 Problema indecidível em geral
 A conversão- representa um caso especial de
extensional equality
02
(c) 2007 Gustavo Motta
6
-calculus
Redução- e igualdade
 O processo de Redução- visa simplificar as
expressões-

Termina quando não há mais -redexes
 Noção de forma normal

Diz-se que uma expressão- está em forma normal
quando não ocorre -redexes nela, i. e., quando
não existe na expressão- uma subexpressão com a
forma (x.P)Q

02
Uma expressão- em forma normal não pode mais ser
reduzida
 É a mais simples dentre as expressões- que são iguais a
ela
7
(c) 2007 Gustavo Motta
-calculus
Redução- e igualdade

Atenção, podem existir expressões- como
 (x.(x)x)x.(x)x
para as quais a redução- nunca termina
 Principal razão para a indecidibilidade da igualdade de
expressões- arbitrárias

Para certas expressões-, pode haver reduções- que
terminam assim como aquelas que não terminam
 Ressalva: se existir pelo menos uma redução- que
termine, então diz-se que essas expressões- têm uma
forma normal
02
(c) 2007 Gustavo Motta
8
-calculus
Redução- e igualdade

Por exemplo, a forma normal da expressão
 (y.(z.w)y)(x.(x)x)x.(x)x
é
w
apesar do fato de ela ter uma redução- que não
termina

02
Caso uma expressão- tenha pelo menos uma
redução- que termina, então pode-se encontrar tal
redução de maneira simples, sem retrocesso
(c) 2007 Gustavo Motta
9
-calculus
Redução- e igualdade

Caso uma expressão- tenha uma forma normal,
então toda redução- que termina resulta na mesma
forma normal (sob -congruência)

Em outras palavras, a ordem com que os -redexes são
contraídos é irrelevante, desde que a redução termine
 Corolário do teorema de Church-Rosser
02
(c) 2007 Gustavo Motta
10
-calculus
Teorema de Church-Rosser
 Motivação

Tendo-se um polinômio com duas variáveis x e y
x y
2
2
para calculá-lo, é indiferente a ordem com a qual
substituem-se x e y por seus valores
3 y
2
2
ou
x 4
2
2
o resultado final não é afetado
3  4  9  16  25
2
02
2
(c) 2007 Gustavo Motta
11
-calculus
Teorema de Church-Rosser


A ordem das substituições não afeta o resultado
final, caso a substituição seja definida corretamente
Para quaisquer expressões-, P, Q e R, e variáveis x
e y, tem-se que
(x.(y.P)R)Q  [Q / x](y.P)R  ([Q / x]y.P)[Q / x]R
 (z.[Q / x]{z / y}P)[Q / x]R  [[Q / x]R / z][Q / x]{z / y}P

Ao mesmo tempo, tem-se
(x.(y.P)R)Q  (x.[R / y]P)Q  [Q / x][R / y]P

02
De acordo com o teorema de Church-Rosser,
ambos os resultados devem ser iguais
(c) 2007 Gustavo Motta
12
-calculus
Teorema de Church-Rosser
 Versão I
 Teorema – Se E  M e E  N, então existe
algum Z tal que M  Z e N  Z
E
M
N
Z

02
Corolário – Se E  M e E  N, estando M e N
em forma normal, então M  N
(c) 2007 Gustavo Motta
13
-calculus
Teorema de Church-Rosser
 Versão II

02
Teorema – Se M = N, então existe algum Z tal que
MZeNZ
(c) 2007 Gustavo Motta
14
-calculus
Teorema de Church-Rosser
 Versão II

Corolário A – Se N está em forma normal e M = N,
então M  N

Duas expressões- iguais em forma normal são
-congruentes

Para duas expressões- quaisquer, M e N, é sempre
decidível se M  N ou não
02
(c) 2007 Gustavo Motta
15
-calculus
Teorema de Church-Rosser
 Versão II

Corolário B – Se M = N, então ambas M e N têm a
mesma forma normal (sob -congruência) ou
senão ambas não têm formal normal

A questão da igualdade de expressões- pode ser
reduzida ao problema de decidir se elas têm ou não
formas normais
 Infelizmente, não é decidível em geral
02
(c) 2007 Gustavo Motta
16
-calculus
Bibliografia

02
Revesz, G. E. Lambda-Calculus, Combinators, and
Functional Programming. Cambridge University
Press, 1988.
(c) 2007 Gustavo Motta
17