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