O l-Cálculo & Linguagens Funcionais Rafael Dueire Lins Departamento de Informática Universidade Federal de Pernambuco - Recife - Brasil 1 Motivação: 2 O l-Cálculo é fundamental para o conceito de computabilidade. Ele servirá como linguagem intermediária no nosso estudo. Uma linguagem funcional será descrita sobre o l-Cálculo. Serão analisados mecanismos de avaliação de expressões. Programa: 3 Lunes: Introdução ao l-Cálculo. Martes: O l-Cálculo como uma linguagem de programação. Miercoles: Lógica Combinatorial. Jueves: Garbage Collection. Viernes:The Fall and Rise of Functional Programming. Introdução John Backus - 1978 • Crise de Software • Gargalo de von-Neumann Linguagens Funcionais • Sintaxe mais agradável do que a do Lambda-Calculus • Programação com funções 4 • LISP (1960) foi a primeira linguagem funcional Programação Funcional Funções de Alta-Ordem • Funções são cidadãs de primeira classe Transparência Referencial • Ausência de assinaladores destrutivos (Linguagens Puras) 5 O l-Cálculo Alonzo Church (1930) Parte de um sistema para Lógica de Alta-Ordem Fundação matemática (Peano-Russell) Inconsistente como Teoria Fundacional 6 O l-Cálculo Subconjunto funcional consistente. Turing (1936) unificou os conceitos de definibilidade no l-Cálculo e de computabilidade Linguagens funcionais são sintaxes “mais bonitas” 7 O l-Cálculo Sintaxe: expr :: variável | constante | exprexpr | lvariavel.expr Exemplos: id x x lx.x Proj x y z y lxlylz.y 8 O l-Cálculo Semântica Operacional: • Variáveis Livres e Ligadas - x é dita livre em uma expressão-l M se: 1. M = x 2. M = ly.N se x ocorrer livre em N e x!= y 3. M = N O se x ocorrer livre tanto em N quanto em O 9 O l-Cálculo Semântica Operacional: • A Conversão- - Trocando o nome de uma variável ligada lx.x 10 ly.y O l-Cálculo Semântica Operacional: • A Conversão- - Substituição de parâmetros reais por parâmetros formais (lx.t ) s [ s / x ] t onde [ s / x ] t significa t com cada ocorrência livre de x substituída por s 11 O l-Cálculo Semântica Operacional: • A Conversão- Exemplo: (lx ly lz.xyz)(la lb lc.a(bc))(lf.f) (ly lz.(la lb lc.a(bc)yz)(lf.f) (lz.(la lb lc.a(bc))(lf.f)z) (lz.(lb lc.(lf.f)(bc))z) 12 O l-Cálculo Semântica Operacional: • A Conversão- - Condição de extensionalidade do sistema (lx.x ) se não houver nenhuma ocorrência de x livre em 13 O l-Cálculo Exemplos de redução: 1. (la.lb.a)(li.i)c 2. (la.aa) (la.aa) 3. (la.aaa) (la.aaa) 4. (la.lb.a)(li.i) ((la.aaa) (la.aaa)) 8 14 O l-Cálculo Teoremas de Church-Rosser 1. Formas normais são únicas (módulo conversão-) 2. -reduzir a expressão mais externa e mais à esquerda a cada ponto numa sequência de reduções leva a forma normal, se ela existir. 15 O l-Cálculo Captura • Reduções- realizadas de forma incorreta Exemplo: (lx.(ly.yx))y [y/x](ly.yx) ly.yy Solução trivial: conversão- 16 O l-Cálculo de DeBruijn: Evita Captura. O nome das variáveis não é importante. O que importa é a distância sintática entre as variáveis e seus limitadores. Utilizado em Provadores de Teoremas (Automath) e linguagens de programação. 17 Amanhã: 18 O l-Cálculo servirá como base para uma linguagem de programação.