Utilidade do Cálculo Lambda em
Programação Funcional
Implementação de um Programa Lambda
A
Semântica Operacional do Cálculo Lambda
A elaboração de modelos de computação (resolução
de problemas por uma máquina) baseia-se em trabalhos de dois pesquisadores
com enfoques bastante diferentes:
-
Máquinas de Turing (Alan Turing, 1936)
- Cálculo
Lambda (Alonzo Church, 1936)
Alan
Turing provou em 1937 a equivalência entre uma Máquina de Turing e o Cálculo Lambda em termos de computabilidade.
• Interessantes pela sua simplicidade sintática
• Facilidade de descrever problemas recursivos.
• Maioria das implementações são poucos aceitas
devido à ineficiência em comparação com linguagens de programação
''tradicionais".
• Novas implementações de interpretadores/compiladores e novas linguagens mais
modernas tem ressurgido.
Exemplos:
- LISP (LISt
Processing - década de 60). Muito simples em muitos
aspectos. Atuamente é ainda a mais utilizada.
- Miranda (Turner 1985)
- Haskell (1990)
- Orwell (Wadler 1985)
- Outras: ML, KRC, LML, SASL.
Utilidade do Cálculo Lambda em Programação Funcional:
Ponto de Partida: Maioria da
Linguagens de Programação Funcional são semelhantes e diferem somente em
aspectos sintáticos .
O cálculo lambda é uma coleção de
diversos sistemas formais baseados em uma notação para funções inventada por
Alonzo Church em 1936
com o intuito de capturar os aspectos mais básicos da maneira pela qual
operadores ou funções podem ser combinados para formar outros operadores.
O cálculo lambda serve
como uma ponte entre linguagens funcionais de alto nível e suas implementavéis de baixo nível. Raízes para a apresentação
do cálculo lambda como uma linguagem intermediária: uma linguagem extremamente simples, consistindo de somente algumas
poucas construções sintáticas e de uma semântica simples.
Uma implementação do cálculo lambda
necessita somente suportar algumas construções simples.
A sua semântica simples nos permite analisar
facilmente a correção de sua implementação.
Trata-se de uma linguagem expressiva, a qual é
suficientemente poderosa para expressar todos os programas funcionais e, por
conseguinte, todas as funções computáveis. Isto significa que, se uma boa
implementação do cálculo lambda é disponível, pode-se
implementar qualquer linguagem funcional através da implementação de um
compilador desta para o cálculo lambda.
2.1. A Sintaxe do Cálculo Lambda
A linguagem do cálculo lambda usa um alfabeto S
constituído de:
- um conjunto de variáveis: vo, v1,
v2,....vn....
- abstrator l (lambda)
- agrupadores (,)
Ao conjunto de cadeias finitas sobre S denota-se por S* e a cadeia que não contem elementos denota-se por e. Usam-se as variáveis x, y, z, ... para denotar cadeias de S*.
Definicão (Equivalência
de duas cadeias)
Duas cadeias x e y são equivalentes e se escreve
(x,y) Œ ∫ € x = y
Definicão
(Comprimento de uma cadeia)
É uma função:
ln: S* Æ Z+
em que o número inteiro
exprime o número de elementos da cadeia.
Definicão (Termo Lambda)
Um termo lambda,
denotado pelas letras M, N, O, P,.. é
um elemento da linguagem L, onde S*
L definido da seguinte forma:
-
vi é termo lambda;
-
dado M, (lvi M) é termo lambda;
-
dados dois termos lambda M, N então (MN) é termo
lambda;
-
e nada mais é termo lambda.
Exemplos:
Verificar quais das expressões são termos lambda.
vo (vov1) (vo)
(lvo(vov1)) (lv1(vo(lv1(vov1)))) (lvo(vov1)
Esta notação é precisa, mas bastante pesada.
Algumas vezes, é conveniente introduzir mais algumas convenções com a
finalidade de simplificar a notação. São quatro as principais convenções:
1-Precedência à esquerda.
Assim,
((MN)L) pode ser escrita MNL
2-Sucessão de abstratores:
(lx(ly(lz........))) se
escreve lxyz...
3-Separador: usa-se um ponto para designar o
final de uma lista de argumentos lambda
Assim lx.xly.y = (lx(x(ly.y)))
4-Supõe-se que letras diferentes designam
entidades diferentes.
Assim x π y em lx.y
Exemplo Concreto
Um
exemplo simples de uma expressão em cálculo lambda é:
(+ 4 5)
2.2 Implementação de um Programa Lambda
Um programa Lambda se
escreve como um conjunto de expressões lambda.
Normalmente, usando notação simplificada encontra-se o símbolo lambda seguido de lista de variáveis. Limitando estas
variáveis vem um ponto ".'', seguido pelo corpo da função. As variáveis
são chamadas de parâmetros formais e diz-se que o lambda
os liga. Assim, seja :
lx.(x + 1)
O exemplo acima pode ser lido: ''Aquela ( ) função de (x) a qual (.) adiciona x a 1. Algumas vezes
costuma-se usar operadores sempre prefixados, e neste caso se escreveria (+ x
1). Para calcular o valor da função para x = 5 se escreve:
lx.(x + 1).5
Uma
abstração lambda sempre consiste dessas partes: o l,
o parâmetro formal, e
o corpo. Uma abstração lambda pode ser considerada
similar a uma definição de função em uma linguagem de programação. convencional, como ''C":
inc ( x )
int x;
( return( x +
1); )
Funções
Embutidas e Constantes
Funções embutidas como + não existem no cálculo lambda na sua forma mais pura. Para fins práticos, uma
extensão que as suporte é útil. Estas incluem funções aritméticas (como +, -,
*, /), constantes (como 0, 1,...), funções lógicas
(como AND, NOT, OR,...) e constantes lógicas (TRUE, FALSE).
Exemplos:
-
5 4 -> 1
AND
TRUE FALSE -> FALSE
Também incluímos uma função condicional, cujo
valor é descrito pelas regras de redução abaixo:
IF TRUE E t E f ->E t
IF FALSE E t E f ->E f
Construtores de dados em cálculo lambda serão introduzidos inicialmente através da definição
de três funções embutidas: CONS, HEAD e TAIL (as quais se comportam exatamente
como as funções LISP: CONS, CAR e CDR).
CONS constrói um objeto composto, o qual pode
ser desmantelado com HEAD e TAIL. A operação é descrita pelas seguintes
regras de redução:
HEAD (CONS a b) ->a
TAIL (CONS a b) ->b
Além dessas funções ,
define-se a constante NIL, o valor nulo.
A escolha
exata de funções embutidas é arbitrária.
Abstrações
Lambda
Abstrações lambda são
construções em cálculo lambda que denotam funções
novas, não embutidas em um cálculo específico.
Exemplo:
(lx . + x 1)
O l indica o início de uma função e é
imediatamente seguido de uma variável.
A expressão (+ 3) denota a "funçåo + aplicada ao argumento 3",
cujo resultado é uma ''funçåo aplicada ao valor
4".
Como em todas as linguagens funcionais, o
cálculo lambda permite que uma função retorne uma
função como resultado.
Este dispositivo nos permite imaginar todas as
funções como possuindo somente um argumento.
Esta notação foi introduzida por Schonfinkel em 1924 e utilizada amplamente nos trabalhos de
Curry, de
onde provém a expressão currying.
Todas as
aplicações de funções no cálculo lambda são escritas
em notação prefixada. Assim a função + precede os argumentos 4
e 5. Um exemplo um pouco mais complexo é:
(+ (* 5 6) (* 8 3))
Do ponto
de vista de implementação, um programa funcional pode ser visto como uma
expressão, que é "executada'' através da sua avaliação. A avaliação ocorre
através da seleção repetida de uma expressão redutível (redex) (abreviação do termo em
inglês “reduced expression”' e de sua redução.
Expressão redutível é aquela que pode ser
avaliada imediatamente. No exemplo
anterior existem dois redexes:
(* 5 6) e (* 8 3)
A expressão inteira (+ (* 5 6) (* 8 3)) não é um
redex, uma vez que a função + necessita ser aplicada
a dois números para poder ser redutível. Através da escolha arbitrária do
primeiro redex para redução escreve-se:
(+ (* 5 6) (* 8 3)) -> (+ 30 (* 8 3))
onde -> le-se "reduz para''.
. Agora há somente um redex
(* 8 3), do qual resulta: (+ 30 24)
. Esta redução gera um novo redex,
que reduz: (+ 30 24) -> 54
2.3. A Semântica Operacional do Cálculo Lambda
Até agora foi descrita a sintaxe do cálculo-l.
Para chamá-lo de "cálculo'', devemos, porém dizer como
"calcular'' com ele. Basicamente isto é realizado através de três
regras de conversão, que descrevem como converter uma expressão-l em outra.
2.3.1.
Introdução a
l-conversão: Variáveis atadas e livres (bound/free)
Seja a expressão-l:
(lx. + x y) 4
Para avaliar a expressão é necessário:
• saber o valor "global'' de y.
• não é necessário saber o valor global de x,
pois é o parâmetro formal da função.
Vê-se que: x e y possuem um status bastante
diferente.
A razão é
que x ocorre atado pelo lx, é somente um encaixe
dentro do qual o argumento 4 é colocado quando a
abstração-l for aplicada ao argumento. Por outro lado, y não é atado por nenhum
e assim ocorre livre na expressão. A ocorrência de uma variável é atada se há
uma expressão-l envolvente que a amarra, senão é livre. No exemplo a seguir, x
e y ocorrem atados, z, porém,
ocorre livre:
lx. + ((ly. + y z) 7) x
Observe que os termos atado e livre se referem a
ocorrências específicas da variável em uma expressão.
Resumindo
a nomenclatura:
Uma aplicação-l é simplesmente a aplicação de
uma expressão-l sobre outra. A primeira dessas duas expressões-l é chamada de
operador, a segunda de operando. Note
que qualquer expressão-l pode ser utilizada tanto como operador como operando.
Uma abstração-l é formada com o símbolo especial seguido por uma variável,
seguida por um ponto, seguido por uma expressão arbitrária. . O propósito da
operação de abstração é o de formar uma expressão unária
a partir de uma expressão-l dada. A variável que ocorre próxima ao inicial do
nome ao argumento. Funções com mais de um argumento são
formadas por abstrações repetidas.
2.3.2.
Conversão-Alfa
Considere:
(lx. + x 1) e (ly. + y 1)
Evidentemente
elas devem ser equivalentes. A conversão-a é o nome dado à operação de mudança
de nome (consistente) de um parâmetro formal.
Notação:
(lx. + x 1) a (ly. + y 1)
a-congruência:
duas expressões-l M e N são a-congruentes (ou a-equivalentes), denotado por M N se ou M=N
ou M->N, ou N é obtido de M através da reposição de uma sub-expressão S de M
por uma expressão-l T tal que S -> T, ou existe alguma expressão-l R tal que
M -> R e R -> N.
Nomenclatura:
Nomes de parâmetros formais podem não ser únicos:
( x.( x. + ( - x 1)) x 3) 9
( x. + (- x 1)) 9 3
+ (- 9 1) 3
11
Observe-se que o x interno não foi substituído na
primeira redução, pois estava protegido pelo x envolvente, ou seja, a
ocorrência interna de x não é livre no corpo da abstração x externa.
Dada uma
abstração-l, (lx.E), é possível identificar-se exatamente as ocorrências de
x que deveriam ser substituídas através da identificação de todas as
ocorrências de x que estão livres. Dessa forma, para o exemplo acima,
examinamos o corpo da abstração:
( x. + (- x 1)) x 3
e vemos que a segunda
ocorrência de x é livre, podendo ser substituída. A idéia do aninhamento do escopo de variáveis em uma linguagem de
programação estruturada é análoga a esta regra.
Outro exemplo:
(lx. y.+ x (( x.- x 3) y)) 5 6
(ly.+ 5 ((
x.- x 3) y)) 6
+
5 (( x.- x 3) 6)
+
5 (- 6 3)
8
Novamente, o x mais interno não é substituído,
uma vez que não é livre no corpo da abstração mais externa.
Nesse
caso não há ocorrências do parâmetro formal (x), pelo qual o argumento 5 poderia ser substituído. Assim o argumento é descartado
sem uso. O corpo de uma abstração poder ser constituído por outra abstração :
(lx. (ly. - y x)) 4 5
(ly. - y 4) 5
-
5 4
1
Observa-se que, ao se construir a instância do
corpo da abstração x, o corpo inteiro inclusive a abstração y envolvida por
esta, substituindo-se x, é copiado. Aqui se observa também o efeito do Currying: a aplicação da abstração x retornou uma função (a
abstração y) como seu resultado. Esta por sua vez, aplicada resultou em ( - 5 4). Funções encapsuladas umas dentro das outras são
comumente abreviadas:
(lx. (ly. E)) para (lx. y. E)
2.3.3.
Conversão-Beta
Uma abstração-b denota uma função. Assim
necessitamos descrever como aplicá-la a um argumento.
A função (lx. + x 1) 4 é a justaposição do função (lx.
+ x 1) e do argumento 4 e, por conseguinte, denota a aplicação de uma certa
função, denotada pela abstração-l, ao argumento 4.
A regra para a aplicação de uma função é muito simples:
·
O
resultado da aplicação de uma abstração-l a um argumento é uma instância do
corpo da abstração-l no qual ocorrências (livres) do parâmetro formal no corpo
são repostas pelo argumento. O resultado de se aplicar a
abstração ao argumento é: + 4 1 onde o (+ 4 1) é um instância do corpo (+ x 1)
no qual ocorrências do parâmetro formal x foram repostas pelo argumento 4.
Escreve-se as conversões utilizando o símbolo como antes:
(lx. + x 1) 4
+
4 1
5
Esta operação é chamada de b-redução e a sua
implementação eficiente é um aspecto importante na elaboração de linguagens de
programação funcional.
Exemplos simples de b-redução:
O parâmetro formal pode ocorrer várias vezes no corpo:
(lx. + x x)
5
+
5 5
10
Da mesma
forma, pode não haver ocorrências do parâmetro formal no corpo. Ex: (lx.
3) 5 3
Uma variável pode possuir tanto uma ocorrência
atada como uma livre em uma expressão. Considere o exemplo:
+ x ((lx. + x 1) 4)
Aqui x ocorre livre (a primeira vez) e atada (a
segunda). Cada ocorrência individual de uma variável deve ser ou atada ou
livre.
As definições formais de livre a atado são dadas
abaixo:
Definição
de ocorre livre:
• x ocorre livre em x (mas não em outra variável
ou constante qualquer)
• x ocorre livre em (E F) se x ocorre livre em E
ou x ocorre livre em F
• x ocorre livre em y.E
x se x, y são variáveis diferentes e x ocorre livre em E
Nota: nenhuma variável ocorre
atada em uma expressão consistindo e uma única constante.
Definição
de ocorre atada:
• x ocorre atada em (E F) se x ocorre atada em E
ou x ocorre atada em F
• x ocorre atada em y.E
(x e y) são a mesma variável e x ocorre livre em E ou
x ocorre
atada em E
2.3.4. Conversão-Eta
Sejam: (lx. + 1 x) e
(+ 1). Estas expressões se comportam exatamente da mesma maneira, quando
aplicadas a um argumento: ambas adicionam 1 ao
argumento. Conversão-z é o nome dado à regra que expressa essa equivalência. Assim:
(lx. + 1 x) -> (+ 1)
De forma
mais geral, a regra da conversão-z pode ser expressa assim:
(lx. F x) -> F
desde que x não ocorra livre
em F e F denote uma função. A condição de que x não deve ocorrer livre em F
previne conversões errôneas. Exemplo:
(lx. + x x) não é e-conversível
para (+ x),
pois x ocorre livre em (+
x).
A
condição de que F deve denotar uma função previne outras conversões errôneas
envolvendo constantes embutidas (pré-definidas). Exemplo: TRUE não é e-conversível para (lx. TRUE x)
Quando a
conversão-z é utilizada da esquerda para a direita, é chamada de redução-l
2.3.5 Resumo
As três regras de conversão que possibilitam a inter-conversão de expressões envolvendo abstrações-l:
1. Mudança
de nome:
a conversão-a permite que se troque o nome de par‚metros formais de uma abstração- , enquanto isto for feito de forma consistente.
2.
Aplicação de funções:
A redução-b permite a aplicação de abstrações- a um
argumento através de geração de uma nova instância do corpo da abstração,
substituindo o argumento por ocorrências livres do parâmetro formal. Cuidado
especial deve ser tomado quando o argumento contém variáveis livres.
3.
Eliminação de abstrações-l redundantes: A redução-z pode às vezes eliminar uma abstração-l . Dentro deste contexto, podemos considerar as funções
embutidas (pré-definidas) como mais uma forma de conversão. Esta forma de
conversão recebe o nome de conversão-z .
2.3.6.
Provas de Inter-convertibilidade
Freqüentemente será necessário poder-se
demonstrar a inter-convertibilidade de duas
expressões-l. Quando as duas expressões denotam funções, esta prova pode se
tornar extremamente longa. Há, porém, métodos para abreviar provas, que não
sacrificam o seu rigor.
Exemplo: Sejam as duas expressões abaixo:
((lp.p) 3) e (lx. 3)
Ambas as expressões denotam a mesma função, que
invariavelmente retorna o valor 3, não importa o valor
de seu argumento e seria de se esperar que ambas sejam inter-convertíveis. Isto realmente ocorre:
IF
TRUE (( p.p) 3) IF TRUE 3
( x. IF TRUE 3 x)
( x. 3)
onde o passo final é a regra
de redução para IF.
Um método
alternativo de se provar a inter-convertibilidade de
duas expressões, muito mais conveniente, é o de se aplicar as duas expressões a
um argumento w.
∑ Se
uma expressão não contém mais redexes, então a
avaliação está completa. Uma expressão nesta forma é dita estar na forma
normal.
∑ Assim,
a avaliação de uma expressão consiste na
redução sucessiva de redexes, até que a
expressão esteja na forma normal.
∑ Definição (forma normal): uma
expressão-l é dita estar na forma normal, se nenhum redex-b,
isto é, nenhuma sub-expressão da forma (lx.P)Q ocorre nela.
∑ Uma
expressão pode conter mais do que um redex, assim a
redução pode acontecer por caminhos diferentes.
∑ Exemplo:
(+ (* 3 4)
(* 7 8))
pode ser reduzido à forma
normal pelas seguintes seqüências: (+ (*
3 4) (* 7 8))
-> (+
12 (* 7 8))
-> (+ 12 56)
-> 68
ou
(+ (* 3 4)
(* 7 8))
-> (+ (* 3 4) 56)
-> ( 12 56)
-> 68
∑ Nem
toda expressão possui uma forma normal,
considere:
(D D)
∑ onde
D é (lx.x x). A avaliação desta expressão jamais
terminaria, uma vez que (D D)
reduz para (D D):
(lx.x x)(lx.x x) -> (lx.x x)(lx.x x)
-> (lx.x x)(lx.x x)
∑ Por
conseguinte, algumas seqüências de redução poderão atingir a forma normal,
outras não. Considere:
(lx.3) (D D)
∑ Se
nós primeiro reduzirmos a aplicação de (lx.3) a (D D) (sem avaliar (D D)), obteremos o resultado 3; porém se
primeiro reduzimos a aplicação de D sobre D, nós simplesmente obtemos (D D)
novamente.
∑ Se
nós continuamos insistindo em escolher a aplicação de D sobre D, a avaliação
vai continuar indefinidamente, não terminando.
∑ Esta
situação corresponde à de um programa imperativo que entra em um laço infinito.
Dizemos que a avaliação ou execução não
termina.
∑ Para
contornar esta situação, existe a ordem
normal de redução, que garante que uma forma normal, caso exista, será
encontrada.
2.4.1.
Ordem Normal de Redução
∑ Uma
questão que se coloca, além da questão "poderei encontrar uma forma normal
?", é a questão de se existe mais de uma forma normal para uma expressão,
ou:
Poderá uma seqüência de redução
diferente levar a uma forma normal diferente?
Ambas as questões estão interligadas.
∑ A
resposta para a última pergunta é: não.
Isto é uma conseqüência dos teoremas
de Church-Rosser TCR1 e TCR2.
Teorema de
Church-Rosser 1 (TCR1):
Se E1
<-> E2, então existe uma expressão E, tal que
E1
-> E e E2 -> E
Corolário:
Nenhuma
expressão pode ser convertida em duas formas normais distintas. Isto significa
que não existem duas formas normais para uma expressão que não sejam a-convertíveis entre si.
Prova:
Suponha que E1
<-> E e E2 <-> E , onde E1 e E2
estão na forma normal.
Então E1
<-> E2 e, pelo TCR1, deve haver
uma expressão F tal que E1 -> F e E2 -> F.
Como tanto E1 como E2 não possuem redexes, logo E1
= F = E2
∑ Informalmente,
o teorema TCR1 diz que todas as seqüências de redução
que terminam, haverão de atingir o mesmo resultado.
O segundo teorema de Church-Rosser, TCR2, diz respeito
a uma ordem particular de redução, chamada ordem
normal de redução.
Teorema de
Church-Rosser 2 (TCR2):
Se E1
-> E2, e E2
está na forma normal, então existe uma ordem normal de seqüência de redução de E1 para E2.
Conseqüências:
∑ Existe
no mínimo um resultado possível e
∑ a
ordem normal de redução encontrará este resultado, caso ele exista.
∑ Observe
que nenhuma seqüência de redução poderá levar a um resultado incorreto, o
máximo que poderá acontecer é a não-terminação. A Ordem Normal de Redução
especifica que o redex mais à esquerda mais externo
deverá ser reduzido primeiro.
∑ No
exemplo anterior (lx.3) (D D),
escolheríamos o redex-lx primeiro, não o (D D).
∑ Esta
regra encorpa a intuição de que argumentos para funções podem ser descartados,
de forma que deveríamos aplicar a função (lx.3) primeiro, ao invés de primeiro avaliarmos
o argumento (D D).
2.4.2.
Ordens de redução ótimas
∑ Enquanto
a ordem normal de redução garante que ou uma solução seja encontrada ou o
não-término ocorra, ela não garante que isto ocorra no número mínimo de passos
de redução, o que é um fato relevante na utilização do cálculo-l para a
implementação de linguagens de programação interpretadas.
∑ No
caso da implementação da resolução através de redução de grafos - que
estudaremos mais tarde - porém, aparentemente a ordem normal de redução é
"geralmente ótima" em questão de tempo de execução.
Analisar
uma expressão para encontrar o redex ótimo para ser
reduzido é aparentemente muito mais trabalhoso e gasta mais tempo do que
arriscar uma redução com mais passos seguindo "cegamente" a ordem
normal.
∑ Alguns
autores como (Levy, J.J.; Optimal Reductions in the Lambda Calculus in Essays on Combinatory
Logic, Academic Press, 1980) se ocuparam de algoritmos para encontrar
ordens ótimas ou quase-ótimas de redução que preservassem as qualidades da
ordem normal de redução. Isto é assunto de um tópico avançado que não cabe
nesta disciplina.
∑ Se
o propósito da utilização de cálculo lambda é a
conversão de programas funcionais neste para que possamos resolvê-los, devemos
ser capazes de representar uma das características mais marcantes das
linguagens funcionais, a recurssão.
∑ O
cálculo lambda suporta a representação de
recursividade sem maiores extensões através da utilização de alguns pequenos
truques.
2.5.1.
Funções Recursivas e o Y
∑ Considere
a definição da função fatorial abaixo:
FAC = (ln.IF (= n 0) 1 (* n (FAC
(- n 1))))
∑ Esta
definição baseia-se na capacidade de se dar um nome a uma abstração lambda e de fazer referência a esta dentro dela mesma.
∑ Nenhuma
construção deste tipo é provida pelo cálculo lambda.
∑ O
maior problema aqui é que funções lambda são anônimas.
∑ Dessa
forma elas não podem nomear-se e assim não podem se referenciar a si mesmas.
Para resolver este problema iniciamos com um
caso onde encontramos a recursão na sua forma mais pura:
FAC = (ln. ... FAC ... )
∑ Aplicando
uma abstração-b sobre FAC, usada de modo inverso, pode-se transformar esta
definição em:
FAC = (lfac.(ln.
(...fac...)))FAC
∑ Esta
definição pode ser escrita da forma:
FAC
= H FAC (2.1)
∑ onde:
H = (lfac.(ln.
(...fac...)))
∑ A
definição de H é trivial. É uma abstração lambda
ordinária e não usa recursão.
∑ A
recursão é expressa somente pela definição 2.1.
A
definição 2.1 pode ser encarada mais como uma equação matemática. Por exemplo,
para resolver a equação matemática
x2 - 2 = x
procura-se por valores de x que satisfaçam