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