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
| exprexpr
| lvariavel.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.
Download

Garbage Collection