Cálculo Lambda: Uma Introdução

Prévia do material em texto

Sumário
1. Introdução
2. História
3. Definição
4. Estilo Church vs Estilo Curry
5. Redução
6. Confluência
7. Conversão
8. Atribuição de Tipo
9. Tipos de Dados
10. Recursão
11. Conclusão
12. Referências
Introdução
Para a ciência da computação, o cálculo lambda, também escrito como cálculo-
λ, é um sistema formal que estuda funções recursivas computáveis, pelo Teorema de
Recursão, e fenômenos relacionados, como variáveis ligadas e substituição. A
principal característica são as entidades que podem ser utilizadas como argumento e
retornadas como valores de outras funções. Ambos os conceitos são definidos
indutivamente.
Programação funcional é um paradigma de programação que trata a
computação como uma avaliação de funções matemáticas e que evita estados ou
dados mutáveis. Ela enfatiza a aplicação de funções, em contraste da programação
imperativa, que enfatiza mudanças no estado do programa.
Linguagens de programação funcionais, especialmente as puramente
funcionais, tem sido mais usadas academicamente que no desenvolvimento comercial
de software. Entretanto, algumas linguagens notáveis usadas na indústria e no
comércio incluem Erlang (aplicações concorrentes), R (estatística), Mathematica
(matemática simbólica) J,K(análise financeira) e XSLT. O cálculo lambda teve uma
importante influência na programação funcional, principalmente nas linguagens de
programação APL e Lisp, e mais recentemente ML, Haskell, OCaml, F# e Elixir. As
funções são tratadas como valores de primeira importância, o que é o mesmo que
dizer que funções podem ser parâmetros ou valores de entrada para outras funções e
podem ser os valores de retorno ou saída de uma função.
Funções podem ser nomeadas, como em outras linguagens, ou definidas
anonimamente (algumas vezes durante a execução do programa) usando uma
abstração lambda e usadas como valores em outras funções. Linguagens funcionais
também permitem que funções sejam do tipo curry. Currying é uma técnica para
reescrita de funções com múltiplos parâmetros como a composição de funções de um
parâmetro. A função do tipo curry pode ser aplicada apenas a um subconjunto de seus
parâmetros. O resultado é uma função onde os parâmetros neste subconjunto são
agora fixados como constantes, e os valores do resto dos parâmetros ainda não são
especificados. A maioria da Linguagens de Programação Funcional são semelhantes e
diferem somente em aspectos sintáticos. 
Começamos por introduzir os termos e explicar o papel do símbolo λ como um
operador de ligação que realiza a substituição.
História
Funções desempenham um papel proeminente na descrição da semântica de
uma linguagem. O cálculo lambda é uma coleção de diversos sistemas formais
baseadas em funções, criada por Alonzo Church em 1936, professor em Princeton,
EUA (1929–1967) e UCLA (1967–1990),com a intenção de capturar os aspectos mais
simples que operadores e funções podem ser combinados para formar outros
operadores, servindo como ligação entre linguagens funcionais de alto nível e suas
implementáveis de baixo nível. É uma linguagem que preza pela simplicidade,
exigindo somente algumas construções sintáticas de uma semântica simples.
As linguagens de programação funcionais, como Miranda, Haskell,Lisp,
Orwell, ML, são baseadas no Lambda Cálculo, sendo esta ser considerada a menor
linguagem de programação universal. 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, com uma
implementação do cálculo lambda, pode-se implementar qualquer linguagem
funcional através da implementação de um compilador desta para o cálculo lambda. 
Definição
O cálculo lambda consiste de uma linguagem de termos lambda junto com uma
teoria equacional, tendo funções como fórmulas.
Pode ser visto como uma linguagem de programação abstrata em que funções podem
ser combinadas para formar outras funções, de uma forma pura.
A linguagem do cálculo lambda usa um alfabeto S constituído de um conjunto
de variáveis(v1, v2,v3,vn) um abstraidor (lambda) e agrupadores(.). O cálculo lambda
estende a ideia de uma linguagem de expressões para incluir funções. Onde
normalmente escreveríamos, por exemplo, f : x → x^3, e então consideramos A =
f(4), em cálculo lambda escreveríamos apenas A = (λx.x^3 )(4). Uma vantagem da
notação lambda é que ela nos permite falar facilmente sobre funções de ordem
superior, isto é, funções cujas entradas e / ou saídas são suas próprias funções.
Expressões lambda são escritas na forma prefixa, com os argumentos lado a lado.
Termos Lambda:
 
Um termo lambda, denotado pelas letras M, N,O, P,..é um elemento da linguagem L,
onde S* L definido da seguinte forma: 
 - ti é termo lambda;
- dado A, (λ ti .A) é termo lambda, chamado de abstração lambda;
- dados dois termos lambda A, B então (AB) é termo lambda, chamado de aplicação;
- e nada mais é termo 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. 
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.
Funções que operam em funções: 
Em cálculo lambda, funções são consideradas como valores, então elas podem servir
de entrada para outras funções, e funções podem retornar funções como saída. Por
exemplo, λy.y representa a função identidade y → y, e ( λy.y)x representa a função
identidade aplicada a x. E assim, (λy.x) representa a função constante y→x, uma
função que sempre retorna, independentemente da entrada. . É importante ressaltar
que a aplicação de funções é associativa à esquerda, então ( λy.y)x z=(( λy.y)x)z.
Variáveis Livres e ligadas: 
As variáveis livres de um termo são aquelas variáveis que não são ligadas por uma
abstração lambda. Ou seja, as variáveis livres de y são apenas y; as variáveis livres de
λy.t são as variáveis livres de t, com y removido, e as variáveis livres de tp são a
união das variáveis livres de t e p. Por exemplo, o termo lambda representado pela
função identidade λy.y não possui variáveis livres, mas a função constante λy.x tem a
variável livre x. As variáveis ligadas são as que são ligadas por λ na expressão. Em
λy.t , por exemplo, y é a variável ligada.
Substituição de variáveis:
Suponha que p, q e r são termos lambda e x e y são variáveis. A notação p[x:=r]
indica a substituição de x por r em p,de modo que:
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). 
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. Cons constrói um objeto
composto, o qual pode ser desmantelado com Head and Tail 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.
Estilo Church vs Estilo Curry 
De um modo geral, existem duas maneiras de atribuição de significado para ocálculo lambda simplesmente tipado, às vezes chamado intrínseco vs extrínseco, ou
estilo Church vs estilo Curry.Uma semântica estilo Church apenas atribui significado
a termos bem tipados, ou mais precisamente, atribui significado diretamente por
derivações de tipagem. O efeito disso é que é possível se atribuir significados
diferentes a termos que se diferenciam apenas por anotações de tipos. Por exemplo, o
termo identidade nos inteiros (λx : int.x) e o termo identidade nos booleanos(λx :
bool.x) podem significar coisas diferentes. Entretanto, uma semântica estilo Curry
atribui significado para termos independente da tipagem, como seriam interpretados
em uma linguagem não tipada. Nesta visão significam a mesma coisa (isto é, λx.x).
A distinção entre semântica intrínseca e extrínseca é às vezes associada a
presença ou não de anotações nas abstrações lambda, mas estritamente falando esse
uso é impreciso. É possível se definir uma semântica estilo Curry em termos anotados
simplesmente ignorando os tipos (através da remoção de tipos, como também é
possível prover uma semântica estilo Church a termos não anotados quando os tipos
podem ser deduzidos do contexto. A diferença essencial entre essas duas abordagens
é apenas como as regras de tipagem são vistas na definição da linguagem, ou como
um formalismo para verificação de propriedades de uma linguagem fundamental
mais primitiva. Maior parte da diferença das interpretações semânticas discutidas
abaixo podem ser vistas sob uma ótica Church ou Curry. 
Redução
A redução também é útil para uma análise de convertibilidade. O teorema de
Church-Rosser diz que se dois termos são conversíveis, então há um termo para o
qual ambos reduzem. Em muitos casos, a inconvertibilidade de dois termos pode ser
provada mostrando que eles não reduzem para um termo comum.
Definição: 
Uma relação binária R em Λ é chamada compatível se:
M R N (ZM) R (ZN), ⇒
(MZ) R (NZ) e
 (λx.M) R (λx.N). 
Uma relação de congruência em Λ é uma relação de equivalência compatível.
Uma relação de redução em Λ é uma relação compatível, reflexiva e transitiva.
Definição:
As relações binárias → β, → β e = β em Λ são definidas indutivamente do seguinte
modo:
(i) 1. (λx.M)N →β M[x := N];
2. M →β N ZM →β ZN, MZ →β NZ e λx.M →β λx.N.⇒
(ii) 1. M → β M;
2. M →β N M → β N;⇒
3M → β N, N → β L M → β L ⇒
(iii) 1. M → β N M =β N;⇒
2.M =β N N =β M;⇒
3 M =β N, N =β L M =βL. ⇒
Essas relações são declaradas da seguinte maneira:
M → β N : Mβ-reduz para N;
 M →β N : Mβ-reduz para N em um passo;
 M =β N : M é β-conversível para N. 
Por definição → β é compatível, → β é uma relação de redução e = β é uma relação
de congruência.
Definição: O termo redex, significa expressão redutível. refere-se a sub-termos que
podem ser reduzidos por uma das regras de redução.
 (i) Um β-redex é um termo da forma (λx.M) N. Nesse caso M [x: = N] é o seu
contratual.
(ii) Um termo λ M é uma forma β-normal (β-nf) se não tiver um β-redex como
subexpressão.
(iii) Um termo M tem uma forma β-normal se M = β N e N for um β-nf, para alguns
N.
Seja M um β-nf. Então:
M → β N N ≡ M.⇒
Prova: Isto é verdadeiro se → β é substituído por → β. Então o resultado segue por
transitividade.
Confluência
Pode ser que um termo lambda ofereça muitas oportunidades de redução ao
mesmo tempo. Para que todo o cálculo tenha sentido, é necessário que o resultado de
um cálculo seja independente da ordem de redução. Gostaríamos de expressar esta
propriedade para todos os termos, não apenas para aqueles que têm uma forma
normal. Isso é possível, segundo o teorema de Church-Rosser: 
“Se um termo M pode ser reduzido (em várias etapas) para termos N e P, então existe
um termo Q ao qual tanto N como P podem ser reduzidos (em várias etapas).”
Por razões gráficas óbvias, a propriedade expressa no Teorema da Church-Rosser é
confluênte. Dizemos que a β-redução é confluente.
Conversão
α-conversão: Conversão de renomeação, permitindo alterar nomes de variáveis
ligadas. Por exemplo, a α-conversão de λy.y poderá produzir λx.x. 
As regras para a alfa-conversão não são tão simples. Primeiro, quando a α-conversão
atua em uma abstração, as únicas ocorrências de variáveis que podem ser renomeados
são aqueles que são vinculados a esta mesma abstração. Por exemplo, λy.λy.y poderia
resultar em λx.λy.y, mas não poderia resultar em λx.λy.λx, pois este possui
significado diferente do original.
η−conversão: Conversão de extensionalidade, que quer dizer que duas funções são as
mesmas se e somente se eles dão o mesmo resultado para todos os argumentos
.η−conversão converte entre λy.(f(y) e f sempre que y não aparece livre em f. Por
exemplo:
Sejam: (ly. + 1 y) e (+ 1). Ambas expressões adicionam1 ao argumento. Então , por
η−conversão, a regra da conversão pode ser expressa da seguinte maneira: (ly. F y) ->
F ,desde que y não ocorra livre em F e F denote uma função. 
A conversão-η pode às vezes eliminar uma abstração-l .
Regras de Conversão:
Há três regras de conversão que possibilitam a interconversão de expressões
envolvendo abstrações-λ :
1. Mudança de nome: a conversão-α 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-β 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-λ redundantes: A redução-η pode as vezes eliminar
uma abstração-λ.
Dentro deste contexto, podemos considerar as funções embutidas
(predefinidas) como mais uma forma de conversão. Esta forma de conversão recebe o
nome de conversão-δ.
Atribuição de Tipo
O cálculo lambda é geralmente referido como uma teoria sem tipo, porque cada
expressão (considerada como uma função) pode ser aplicada a outra expressão
(considerada como um argumento). Por exemplo, a função identidade I ≡ λy.y pode
ser aplicada a qualquer argumento y para dar como resultado que mesmo
Y. Em particular, pode ser aplicado a si próprio.
Existem também versões tipadas do cálculo lambda, chamadas de cálculo
lambda simplesmente tipado. Isso é possível com adição de apenas um elemento (o
construtor de tipos: → para construir tipos de funções.Tipos são geralmente objetos
de uma sintática e podem ser atribuídos a termos lambda. Se P é um termo e um tipo I
é atribuído a P, então dizemos 'P tem tipo I' ou 'P em I'; A denotação utilizada para
isso é M: A.
Tipos também podem ser usados para melhorar a eficiência da compilação de
termos representando algoritmos funcionais. Se, por exemplo, se sabe que um
subexpressão de um termo é puramente aritmética, então uma avaliação rápida é
possível. Isso ocorre porque a expressão pode ser executado pela ULA da máquina e
não da maneira mais lenta, em que as expressões simbólicas são avaliadas em geral.
Tipos de Dados
Aritmética do cálculo lambda:
Existem várias formas possíveis para definir os números naturais no lambda cálculo,
mas, de longe, os mais comuns são os Church Numerals. Esperamos que uma
linguagem de programação seja capaz de fazer cálculos aritméticos. Os números
podem ser representados no cálculo lambda a partir de zero e escrevendo "suc (zero)"
para representar 1, suc (suc (zero)) para representar 2, e assim em diante. No cálculo
lambda só podemos definir novas funções. Os números serão definidos como funções
usando a abordagem: zero pode ser definido como λs.(λz.z), ou λsz.z resumidamente;
Esta é uma função de dois argumentos s e z. Entende-se aqui que s é o primeiroargumento a ser substituído durante a avaliação e z o segundo. Usando esta notação,
os primeiros números naturais podem ser definidos como:
1 ≡ λsz.s(z)
2 ≡ λsz.s(s(z))
3 ≡ λsz.s(s(s(z)))
e assim por diante.
A função sucessora seria definida como:
S ≡ λwyx.y(wyx). Aplicando essa função na representação da expressão zero,
teriamos: S0 ≡ λyx.y((λsz.z)yx) = λyx.y((λz.z)x) = λyx.y(x) ≡ 1, e assim por diante,
por exemplo, aplicando na representação da expressão um, teriamos S1 ≡
(λwyx.y(wyx))(λsz.s(z)) = λyx.y((λsz.s(z))yx) = λyx.y(y(x)) ≡ 2.
Operações Lógicos:
É possível definir operações lógicas usando uma representação da tabela verdade.
A função AND de dois argumentos pode ser definida como:
 ≡ λxy.xy (λuv.v) ≡ λxy.xyF∧
A função OR de dois argumentos pode ser definida como:
 ≡ λxy.x (λuv.u) y ≡ λxy.xTy∨
A negação de um argumento pode ser definida como:
Λ λx.x (λuv.v) (λab.a) ≡ λx.xFT
A função de negação aplicada a “verdadeiro” é:
¬T ≡ λx.x (λuv.v) (λab.a) (λcd.c)
Que se reduz a:
TFT ≡ (λcd.c) (λuv.v) (λab.a) = (λuv.v) ≡ F,
isto é, o valor “falso”.
Pairs:
Um par (2-tupla) pode ser definido por True e False,usando o “Church encoding for
pairs”. Por exemplo, Pair encapsula o par (x,y), First retorna o primeiro elemento do
par, e Second retorna o segundo.
PAIR := λx.λy.λf.f x y 
FIRST := λp.p TRUE
SECOND := λp.p FALSE
NIL := λx.TRUE
NULL := λp.p (λx.λy.FALSE)
Uma lista ligada pode ser definida como qualquer NIL para a lista vazia,ou PAIR de
um elemento e uma lista menor. O predicado NULL testa se o valor é NIL.
Recursão
As funções recursivas podem ser definidas no cálculo lambda usando uma
função que chama uma função y e depois se regenera. Isto pode ser melhor
compreendido considerando a seguinte função Y:
Y ≡ (λy.(λx.y(xx))(λx.y(xx))) 
Esta função aplicada a uma função R produz:
YR = (λx.R(xx))(λx.R(xx)) ,
que produziu utilizando redução:
R((λx.R(xx))(λx.R(xx)))) ,
significando que YR = R (YR), ou seja, a função R é avaliada usando a chamada
recursiva YR como o primeiro argumento.
O cálculo lambda suporta a representação de recursividade sem maiores
extensões através da utilização de alguns pequenos truques. Assumindo, por exemplo,
uma função fatorial definida por:
FAC = (ln.IF (= n 0) 1 (* n (FAC (- n 1)))) 
Na expressão lambda que representa esta função, um parâmetro será presumido
para receber em si a expressão lambda como o seu valor, de modo que é chamando –
aplicando-o a um argumento – será equivalente a recursão. Assim, para alcançar a
recursividade, o argumento destinado-como-auto-referência (chamado r aqui) sempre
deve ser passada para si mesmo dentro do corpo da função, em um ponto de
chamada: 
G := λr. λn.(1, se n = 0; então n × (r r (n−1)))
com  r r x = F x = G r x  para manter, assim r = G  e
F := G G = (λx.x x) G.
Esta definição baseia-se na capacidade de se dar um nome a uma abstração
lambda e de fazer referência à ela dentro dela mesma. Nenhuma construção deste tipo
é provida pelo cálculo lambda. O cálculo lambda reescreve cada chamada
recursiva..Aplicando uma abstração- β sobre FAC, usada de modo inverso, pode-se
transformar esta definição em: 
FAC = (lfac.(ln. (...fac...)))FAC , que pode ser escrita como:
FAC = H FAC, onde:
H = (lfac.(ln. (...fac…))).
A definição de H é trivial. É uma abstração lambda ordinária e não usa
recursão, sendo uma equação matemática.Por exemplo, para resolver a equação
matemática: x^2 - 2 = x , procuramos por valores de x que satisfazem a equação. De
forma similar, busca-se uma expressão lambda para FAC que satisfaça FAC = H
FAC.A equação FAC = H FAC postula que, quando a função H é aplicada a FAC, o
resultado é FAC. Diz-se então que FAC é um ponto fixo de H. Uma função pode ter
mais de um ponto fixo. Por exemplo, na função abaixo, tanto 0 quanto 1 são pontos
fixos da função: λy. * y y a qual calcula o quadrado de seu argumento.
Em resumo, estamos procurando por um ponto fixo para H. Claramente isto
depende somente de H. Para isto, invente-se, a título provisório, uma função Y, a qual
toma uma função como argumento e devolve o seu ponto fixo como resultado. 
Assim Y tem o comportamento de: Y H = H (Y H) e e Y é chamado de combinador
de ponto fixo. Assim, caso possamos produzir um Y, temos uma solução para o
problema da recursividade. 
Para a transformação de uma expressão recursiva em uma não-recursiva,
utilizamos o combinador de ponto fixo, uma função que chamamos de Y.A
propriedade que Y necessita ter é: Y H = H (Y H) e isto representa evidentemente a
recursão da forma mais pura, uma vez que esta fórmula pode ser utilizada para
representar, de forma abstrata, qualquer fórmula recursiva que queiramos. O truque é
que podemos representar Y como uma abstração lambda sem utilizar a recursão: 
Y = (λh. (λx.h (x x)) (λx. h (x x))) .
Para demonstrar que Y possui a qualidade desejada, evaluemos: 
Y H 
= (λh. (λx.h (x x)) (λx. h (x x))) H
<-> (λx.H (x x)) (λx. H (x x)) 
<-> H ((λx.H (x x)) (λx. H (x x))) 
<-> H (Y H) 
O fato de Y poder ser definido como uma abstração lambda é, do ponto de vista
matemático, realmente digno de nota. Do ponto de vista da implementação, é
relativamente ineficiente implementar Y como uma abstração lambda. Para a
construção de linguagens funcionais, utiliza-se geralmente uma função embutida com
a regra de redução: Y H -> H (Y H).
Conclusão
O cálculo lambda foi discutido largamente. Vimos principalmente o cálculo lambda 
não tipado, que é a parte mais relevante para a ciência da computação. O cálculo 
lambda tipado foi discutido brevemente. O cálculo lambda tem um grande papel no 
desenvolvimento da teoria de linguagens de programação, especialmente nas 
linguagens funcionais, em particular Lisp, mas também em outras linguagens 
funcionais, como Haskell e Miranda.
Referências
MICHAELSON, G..An Introduction to Functional Programming through Lambda
Calculus. Addison-Wesley: 1989. 
JONES, N.D.. Computability and Complexity: From a Programming Perspective.
MIT Press: 1997. 
BARENDREGT, H.P.. The Lambda Calculus: Its Syntax and Semantics. North-
Holland, revised edition: 1984. 
KRIVINE, J.L.. Lambda-Calculus, Types and Models. Masson: 1993.
REVESZ, G.. Lambda-Calculus Combinators and Functional Programming,
Cambridge University Press, Cambridge: 1988, chapters 1–3. 
HINDLEY, J.R ; SELDIN, J.P.. Introduction to Combinators and λ-Calculus.
Cambridge University Press: 1986. 
KOGGE,P. M.. The Architecture of Symbolic Computers, McGraw-Hill, New York:
1991, chapter 4.