Programação Funcional em Haskell

Programação Funcional em Haskell

(Parte 6 de 9)

Deve ser notado que as definicoes recursivas sao implıcitas, por natureza. No entanto, como seu lado esquerdo e simples, ou seja, composto apenas pelo nome da funcao e seus argumentos, elas podem ser convertidas facilmente em regras de reescritas. Por exemplo, as duas equacoes seguintes constituem uma definicao recursiva de fatorial,p ara n ≥ 0.

elas podem ser convertidas as seguintes regras de reescritas:

Estas regras de reescritas nos dizem como transformar uma formula contendo fat.A realizacao destas transformacoes, no entanto, nao elimina, necessariamente, a funcao da formula. Por exemplo,

No entanto, se a computacao termina, entaoaa plicacao repetida das regras de reescrita eliminara fat da formula

Este Capıtulo se relaciona com a fundamentacao teorica das linguagens funcionais. Esta fundamentacao e fortemente conectada com a Matematica e isto tem como vantagem primeiramente a constatacao de essas linguagens tem um embasamenteo teorico sob o qual elas se fundamentam e depois, sendo este embasamento oriundo da Matematica, torna estas linguagens mais trataveis matematicamente e mais faceis de terem seus programas provados.

O objetivo deste Capıtulo foi mostrar a programacao funcional como uma programacao sem atribuicoes, da mesma maneira que a programacao estruturada e uma programacao sem gotos. Uma maquina, ao executar um programa estruturado, esta, de fato, executando gotos, enquanto uma maquina, ao executar um programa funcional, esta, de fato, realizando atribuicoes. Em ambos os casos, estas construcoes sao escondidas do programador, ou seja, elas estao em um nıvel inferior de abstracao.

Ap arte historica mostrada no inıcio do Capıtulo foi baseada na Apostila de Rafael Lins [2] e no livro de Brainerd [5]. A fundamentacao teorica foi, grande parte, baseada no livro de Bruce Maclennan [24] que e um livro composto de duas partes, a primeira sendo pratica e a segunda teorica. Ele adota esta metodologia de praticar e depois justificar a parte pratica. Esta metodologia e inusitada e faz com que o livro seja uma referencia muito interessante nao apenas pelo metodo utilizado mas, principalmente, pelo conteudo muito bem escrito.

Outro livro fundamental neste estudo foi o livro de Antony Davie [7] que apresenta um conteudo proximod ap arte teorica do livro de Maclennan. O Capıtulo tambem se baseia nos ensinamentos do livro de Chris Okasaki [26] que apresenta uma teoria de linguagens funcionais bastante profunda e objetiva.

Capıtulo 2 λ-calculo

”Type theories in general date back to the philosopher Bertrand Russell and beyond.

They were used in the early 1900’s for the very specific purpose of getting round the paradoxes that had shaken the foundations of mathematics at that time, but their use was later widened until they came to be part of the logicians standard bag of techinica tools, especially in proof-theory.” (J. Roger Hindley in [13])

2.1 Introducao

O λ-calculo foi desenvolvido por Alonzo Church no inıcio dos anos 30, como parte de um sistema de logica de ordem superior com o proposito de prover uma fundamentacao para a matematica, dentro da filosofia da escola logicista de Peano-Russel [2]. O λ-calculo eu ma teoria que ressurge do conceito de funcao como uma regra que associa um argumento a um valor calculado atraves de uma transformacao imposta pela definicao da funcao. Nesta concepcao, uma funcao e representada por um grafo, onde cada noe um par (argumento, valor).

Al ogica combinatorial foi inventada antes do λ-calculo, em cerca de 1920, por Moses

Schonfinkel, com um proposito semelhante ao do λ-calculo [5]. No entanto, ela foi redescoberta 10 anos depois, em 1930, por Haskell B. Curry, que foi o maior responsavel pelo seu desenvolvimento ate cerca de 1970. Em 1935, Kleene e Rosser provaram que o λ-calculo e a logica combinatorial eram inconsistentes, o que provocou um desinteresse academico pelo tema. No entanto, Curry nao desistiu de seu estudo e construiu uma extensao na logica combinatorial para fins de seus estudos, conseguindo sistemas mais fracos que a logica classica de segunda ordem. Em 1975, Dana Scott e Peter Aczel mostraram que seu ultimo sistema apresentava modelos interessantes [5]. Em 1941, Church desistiu de sua pesquisa inicial e apresentou uma sub-teoria que lidava somente com a parte funcional. Essa sub-teoria, chamada de λ-calculo foi mostrada ser consistente pelo teorema de Church-Rosser [2]. Usando o λ-calculo, Church propos uma formalizacao da nocao de computabilidade efetiva pelo conceito de definibilidade no λ-calculo. Klene mostrou que ser definıvel no λ-calculo e quivalente a recursividade de Godel-Herbrand. Concomitantemente, Church formulou a sua conjectura associando a recursividade como a formalizacao adequada do conceito de computabilidade efetiva. Em 1936, Allan Turing modelou a computacao automatica e mostrou que a nocao resultante (computabilidade de Turing) e quivalente a definibilidade no λ-calculo. Desta forma, o λ-calculo pode ser visto como uma linguagem de programacao. Isto implica que podem-se analisar diversos tipos de problemas de programacao, em particular, os relacionados com chamadas a procedimentos [2].

Curry e seus colegas [6], Barendregt [3] e outros desenvolveram extensivamente os aspectos sintaticos do λ-calculo, enquanto Scott [32], principalmente reportado por Stoy [34] e Schmidt [31], se dedicou as emantica da notacao, o que veio a facilitar a vida dos usuarios futuros do λ-calculo.

2.2 λ-expressoes

O λ-calculo tem apenas quatro construcoes: variaveis, constantes, aplicacoes e abstracoes. Suponhamos que sejam dadas uma sequencia infinita de sımbolos distintos chamados de variaveis e uma sequencia finita, infinita ou vazia de sımbolos distintos, chamados constantes [29]. Quando as equencia de constantes for vazia, o sistema e chamado de puro; em caso contrario, e chamado de aplicado. O conjunto de expressoes, chamadas de λ-expressoes, e definido indutivamente da seguinte forma:

• todas as variaveis e constantes sao λ-expressoes (chamadas de atomos);

• se M e N forem λ-expressoes, entao (MN )t ambem eu ma λ-expressao, chamada combinacao ou aplicacao;

• se M for uma λ-expressao e x for uma variavel qualquer, entao (λx.M) tambem eu ma λ-expressao, chamada abstracao ou funcao.

As λ-expressoes, assim definidas, podem ser formuladas utilizando a notacao BNF. Isto e feito da seguinte maneira, onde elas sao representadas por <e xp >:

<e xp > :: <c onstante > - constantes embutidas |<v ariavel > -n omes de variaveis

| (<e xp >< exp> )- combinacao ou aplicacao

| (λ<v ariavel >. <e xp >)- abstracao ou funcao.

Apesar das definicoes acima serem claras, elas sao muito rıgidas e, am alguns casos, podem surgir duvidas sobre as regras de escopo, ou seja, ateq ue ponto em uma λ-expressao uma variavel tem influencia. Assim, as observacoes a seguir devem ser utilizadas para dirimir duvidas, por acaso existentes.

Observacoes importantes:

1. As variaveis sao representadas por letras romanas minusculas.

2. As λ-expressoes completas sao representadas por letras romanas maiusculas ou por letras gregas minusculas (exceto α, β, γ e λ que tem significados especiais) ou por letras gregas maiusculas.

(λx.(λy.((λz.(E))... ))) pode e deve ser escrita como λxy ... z.E, significando que gru-

3. Apesar da rigidez mostrada na BNF das λ-expressoes, os parenteses devem ser usados apenas para resolver ambiguidades [38]. Esta e uma convencao que diminui muito o tamanho das λ-expressoes e deve ser utilizada, sempre que possıvel. Por exemplo, pos de abstracoes ou funcoes sao associados pela direita. No entanto, grupos de com-

binacoes ou aplicacoes termos combinados sao associados pela esquerda, ou seja, E1E2E3En
significa (((E1E2)E3)... En). Alem disso, λa.CD representa (λa.CD)e nao (λa.C)(D),

estabelecendo que o escopo de uma variavel se extende ate o primeiro parentese descasado encontrado a partir da variavel, ou atingir o final da λ-expressao.

4. A escolha de constantes, de funcoes embutidas para serem utilizadas na manipulacao destas constantes e/ou numeros e das funcoes para o processamento de listas e arbitraria.

Estas observacoes sao importantes porque elas podem ser utilizadas para dirimir algumas duvidas que, com certeza, vao existir, principalmente por quem esta travando um primeiro contacto com o processo de avaliacao no λ-calculo. E comum nao se reconhecer imediatamente oe scopo deu ma variavel e estas observacoes podem ser um meio importante para dirimir estas duvidas.

Exemplos Sao exemplos de λ-expressoes:

2.3 A sintaxe do λ-calculo

Nesta secao seram ostradaas intaxe do λ-calculo, ficando a semantica para uma proxima.

• Todasa sa plicacoes de funcoes sao pre-fixas, significando que, por exemplo, a expressao (+(∗ 23 ) (∗ 8 2)) tem seus parenteses externos redundantes podendo, e ate devendo, serem retirados para evitar confusao visual.

• Do ponto de vista de implementacao, um programa funcional deve ser visto como uma expressao que vai ser avaliada.

• Esta avaliacao se da pela selecao repetida de expressoes redutıveis, conhecidas como redexes, e suas reducoes. Por exemplo, a λ-expressao (+(∗ 23 ) (∗ 8 2)) apresenta dois redexes: um (∗ 23 ) e o outro (∗ 8 2), apesar da expressao toda nao representar um redex porque seus parametros ainda nao estao todos avaliados. A avaliacao da λ-expressao acima ef eita com a seguinte sequencia de reducoes: (+(∗ 23 )( ∗ 82 )) → (+ 6(∗ 82 )) → (+ 6 16) → 2

2.3.1 Aplicacao de funcao e currificacao

A aplicacao de uma funcao f au m parametro x e denotada apenas por justaposicao, ou seja, fx . E se a funcao tiver mais de um argumento? Por exemplo, a λ-expressao (+ 3 4) e interpretada como (+ 3) 4, ou seja, como uma funcao (+ 3) que adiciona 3 ao seu argumento (4). Este resultado se deve ao fato de que o λ-calculo permite que o resultado da aplicacao de uma funcao seja tambem uma outra funcao. Este resultado foi descoberto por Schonfinkel, mas foi amplamente utilizado por Curry e, por este motivo, passou a ser conhecido como currificacao.

Dito de outra forma, currificacao e uma caracterıstica muito importante de algumas linguagens, onde uma funcao com n argumentos pode ser interpretada como n funcoes de apenas 1 (um) argumento. Isto significa que, para o λ-calculo, todas as funcoes tem apenas um argumento.

2.4 Funcoes e constantes pre-definidas

Uma caracterıstica importante do λ-calculo e a facilidade com que as funcoes podem ser construıdas pelo usuario. No entanto, algumas delas juntamente com algumas constantes ja foram pre-definidas e que podem ser utilizadas pelos usuarios. Entre elas podem ser citadas:

• constantes (0, 1, 2,), NIL

• constantes (TRUE, FALSE)

• caracteres constantes (‘a’, ‘b’,)

• funcao condicional IF: IF TRUE E1 E2 → E1 IF FALSE E1 E2 → E2

• construtores de dados: (CONS, HEAD, TAIL) onde

HEAD (CONS a b) → a TAIL (CONS a b) → b

Exemplos:

a) − 54 → 1 b) AND TRUE FALSE → FALSE

(Parte 6 de 9)

Comentários