
Introdução ao -calculus
Prof. Gustavo Motta
Departamento de Informática/UFPB
01
(c) 2007 Gustavo Motta
1
-calculus
Sumário
 Sintaxe
 Renomeação, -congruência e substituição
01
(c) 2007 Gustavo Motta
2
-calculus
Sintaxe
 Considerações
 Funções representadas por uma notação simbólica
(expressões-) e não por conjuntos de pares

Define-se
 Uma sintaxe sem preocupações semânticas
 Operações sobre as expressões-

Teoria de transformações de funções para investigar
suas propriedades sob essas operações
 Toda expressão- denota alguma função
 Não considera os domínios e os co-domínios -  livre de
tipos

01
O -calculus é uma importante ferramenta para
estudar as propriedades matemáticas das linguagens
3
de programação (c) 2007 Gustavo Motta
-calculus
Sintaxe
 Sintaxe

Assume-se que há de uma seqüência infinita de




expressões- mais complexas são formadas a partir
dos átomos pelo uso de duas operações de
formação de expressões


01
variáveis representadas por identificadores
constantes representadas por uma cadeia finita de
dígitos ou outros símbolos
Variáveis e constantes são denominados de átomos, pois
são as expressões- mais simples
Aplicação
Abstração
(c) 2007 Gustavo Motta
4
-calculus
Sintaxe
 Sintaxe

Abstração

Formada pelo símbolo  seguido de uma variável,
seguindo por um ponto, seguido por uma
expressão- arbitrária
 x.x



01
x.y.x
x.y.y
Visa criar um função unária a partir de uma
expressão- dada
A variável que segue o símbolo  corresponde ao
nome do argumento da função
Funções com mais de um argumento são formadas
pela repetição de abstrações
(c) 2007 Gustavo Motta
5
-calculus
Sintaxe
 Sintaxe

Aplicação

É apenas a aplicação de uma expressão- a outra
 A primeira das expressões é denominada operador
 A segunda é chamada de operando da aplicação
 (f)3

(x.y.x)2
(x.y.y)x.x
Qualquer expressão- pode ser usada como
operando ou operador
01
(c) 2007 Gustavo Motta
6
-calculus
Sintaxe
 Sintaxe formal

<expressão-> ::= <variável>|<constante>|<aplicação>|<abstração>
<aplicação> ::= (<expressão->)<expressão->
<abstração> ::= <variável>.<expressão->

Exemplos



x.y.(y)x
f.(f)2
x.(f)x
(y.(x)y)x.(u)x
Observe notação de aplicação de função



01
x.x
(f)3
f(x) passa ser (f)x na notação 
Letras minúsculas para nomes de variáveis
expressões- arbitrárias são denotadas por letras
maiúsculas
(c) 2007 Gustavo Motta
7
-calculus
Sintaxe
 Definição de igualdade

Duas expressões-, P e Q, são idênticas, em
símbolos, P  Q, se e somente se Q é uma cópia
exata de P, símbolo por símbolo
 Associatividade

01
A aplicação de funções é associativa à direita

(P)(Q)R corresponde à aplicação de P a (Q)R

((P)Q)R denota a aplicação de (P)Q a R
(c) 2007 Gustavo Motta
8
-calculus
Sintaxe
 Variáveis livres
A ocorrência de uma variável x numa expressão-
está amarrada se ela está dentro de um subtermo
com a forma x.P, caso contrário, ela está livre

Definição – O conjunto de variáveis livres de uma
expressão- E, denotado por (E), é definida por
indução na construção de E
(c) = {}
2. (x) = {x} para qualquer variável x
1.
(x.P) = (P)  {x}
4. ((P)Q) = (P)  (Q)
3.
01
(c) 2007 Gustavo Motta
9
-calculus
Sintaxe
 Variáveis livres

Exemplos
(x.(z)x)y.(y)x
y.(x.(x)y)y.(y)x
01
(c) 2007 Gustavo Motta
10
-calculus
Renomeação, -congruência e
substituição
 Motivação

A computação dos valores de uma função para
um dado argumento requer a substituição do
argumento para a variável correspondente na
expressão que representa a função
x.y.((+)x)y
(x.y.((+)x)y)10
y.((+)10)y
(y.((+)10)y)15
((+)10)15  25
01
(c) 2007 Gustavo Motta
11
-calculus
Renomeação, -congruência e
substituição
 Aspecto fundamental

Duas expressões- são consideradas essencialmente
as mesmas se elas diferem apenas nos nomes de
suas variáveis amarradas


As expressões-x.(y)x e z.(y)z representam a mesma
função
A liberdade de uso do nome de variáveis amarradas é
formalizada transformação -congruência
 Renomeação de variáveis amarradas que não modifica o
sentido de expressões-
01
(c) 2007 Gustavo Motta
12
-calculus
Renomeação, -congruência e
substituição
 Renomeação

Definição – A renomeação de uma variável x para z
numa expressões- P, em símbolos {z/x}P, é
definida por indução na construção de P
1. {z / x}x  z
2. {z / x}y  y
se x  y
3. {z / x}x.E  z.{z / x}E para toda expressão- E
4. {z / x}y.E  y.{z / x}E para toda expressão- E, x  y
5. {z / x}(E1)E2  ({z / x}E1){z / x}E2 para quaisquer
expressões-, E1e E2
01
(c) 2007 Gustavo Motta
13
-calculus
Renomeação, -congruência e
substituição
 Renomeação

O prefixo {z / x} não é parte da notação 

É apenas uma forma de indicar a renomeação
{a / b}(v.b.(b)v)u.((c)u)b
indica a expressão
(v.a.(a)v)u.((c)u)a
 A regra 

01
x.E  z.{z / x}E
para qualquer z que não
esteja amarrado ou livre em E
(c) 2007 Gustavo Motta
14
-calculus
Renomeação, -congruência e
substituição
 -congruência (-igualdade)

Definição – Duas expressões-, M e N, são
-congruentes (ou -iguais), em símbolos M  N,
se M  N, ou M  N, ou N é obtido de M pela
troca de uma sub-expressão de S de M por uma
expressão- T, tal que S  T, ou existe alguma
expressão- R, tal que M  R e R  N

Relação de equivalência

01
Reflexiva, simétrica e transitiva
(c) 2007 Gustavo Motta
15
-calculus
Renomeação, -congruência e
substituição
 Substituição (conversão-)

Definição – A substituição com Q de todas as ocorrências
livres da variável x em P, em símbolos [Q / x]P, é definida por
indução em P
1. [Q / x]x  Q
2. [Q / x]y  y
se x  y
3. [Q / x]x.E  x.E
para qualquer expressão- E
4. [Q / x]y.E  y.[Q / x]E para qualquer expressão- E, se x  y e
pelo menos uma das seguintes condições valha: x  (E), y  (Q)
5. [Q / x]y.E  z.[Q / x]{z / y}E
para qualquer expressão- E e
para qualquer z, com x  z  y, que não seja nem livre ou
amarrado em (E)Q, se x  y e ambos x  (E) e y  (Q) valem
6. [Q / x](E1)E2  ([Q / x]E1) [Q / x]E2
01
(c) 2007 Gustavo Motta
16
-calculus
Renomeação, -congruência e
substituição
 Substituição (conversão-)

O prefixo [Q / x]P não é parte da notação 

É apenas uma forma de indicar a substituição
[z.y.(y)z / x](u.(x)u)(u)x
-congruente com
([z.y.(y)z / x]u.(x)u)[z.y.(y)z / x](u)x
que é
(u.[z.y.(y)z / x](x)u)([z.y.(y)z / x]u)[z.y.(y)z / x]x
que é
(u.([z.y.(y)z / x]x)[z.y.(y)z / x]u)(u)z.y.(y)z
finalmente, -congruente com
(u.(z.y.(y)z)u)(u)z.y.(y)z
01
(c) 2007 Gustavo Motta
17
-calculus
Renomeação, -congruência e
substituição
 Substituição (conversão-)

A operação de substituição nem sempre é trivial

Os casos mais complexos envolvem o item 5. da definição
[u.(y)u / x]y.(x)y
resulta em
y.[u.(y)u / x](x)y
e então
y.([u.(y)u / x]x)[u.(y)u / x]y
e finalmente
y.(u.(y)u)y
Qual é o problema da substituição anterior?
[u.(y)u / x]{z / y}y.(x)y resulta em z.(u.(y)u)z
01
(c) 2007 Gustavo Motta
18
-calculus
Bibliografia

01
Revesz, G. E. Lambda-Calculus, Combinators, and
Functional Programming. Cambridge University
Press, 1988.
(c) 2007 Gustavo Motta
19
Download

E, x - Departamento de Informática — UFPB