aula2 - Programação Funcional, Notas de aula de Análise de Sistemas de Engenharia

Baixe aula2 - Programação Funcional e outras Notas de aula em PDF para Análise de Sistemas de Engenharia, somente na Docsity! INE 5363 - Programação Funcional - INE/CTC/UFSC - Curso de Bacharelado em Ciências da Computação Prof. Dr. rer.nat. Aldo von Wangenheim - http://www.inf.ufsc.br/~awangenh/Funcional 2.2. A Semântica Operacional do Cálculo Lambda Até agora foi descrita a sintaxe do cálculo- . 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 conver- ter uma expressão- em outra. 2.2.1. Introdução à conversão: Variáveis atadas e livres (bound/free) Consideremos a expressão- : ( x. + x y) 4 Para avaliar esta expressão necessitamos: • saber o valor “global” de y. • não necessitamos saber o valor global de x, pois é o parâmetro formal da função. • Assim vemos que: x e y possuem um status bastante diferente. A razão é que x ocorre atado pelo x, é somente um encaixe dentro do qual o argumento 4 é colocado quando a abstração- for aplicada ao argumento. Por outr 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- envolvente que a amarra, senão é livre. No exemplo a seguir, x e y ocorrem atados, z porém, ocorre livre: x. + (( y. + 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. Uma variável pode possuir tanto uma ocorrência atada como uma livre em uma expressão. Considere o exemplo: + x (( x. + 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. λ λ λ λ λ λ λ λ λ λ λ INE 5363 - Programação Funcional - INE/CTC/UFSC - Curso de Bacharelado em Ciências da Computação Prof. Dr. rer.nat. Aldo von Wangenheim - http://www.inf.ufsc.br/~awangenh/Funcional As definições formais de livre a atado são dadas abaixo: 2.2.2. Conversão-Beta Uma abstração- denota uma função. Assim necessitamos descrever como aplicá-la a um argumento. A função ( x. + x 1) 4 é a justaposição do função ( x. + x y) e do argumento 4 e, por conse- guinte, denota a aplicação de uma certa função, denotada pela abstração- , ao argumento 4. A regra para a aplicação de uma função é muito simples: • O resultado da aplicação de uma abstração- um argumento é uma instância do corpo da abstração- no qual ocorrências (livres) do parâmetro formal no corpo são repostos 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. Nós escrevemos as conversões utilizando o símbolo como antes: 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) x ocorre livre em E ou x ocorre livre em F x ocorre livre em y.E x e y são variáveis diferentes e x ocorre livre em E Nota: nenhuma variável oorre atada em uma expressão consistindo e uma única constante. Definição de ocorre atada: x ocorre atada em (E F) 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 ⇔ λ ⇔ ⇔ λ ⇔ λ λ λ λ λ λ → INE 5363 - Programação Funcional - INE/CTC/UFSC - Curso de Bacharelado em Ciências da Computação Prof. Dr. rer.nat. Aldo von Wangenheim - http://www.inf.ufsc.br/~awangenh/Funcional Exemplo maior: Modelagem de Construtores de Dados Definimos CONS, HEAD e TAIL da seguinte forma: CONS = ( a. b. f.f a b) HEAD = ( c.c ( a. b.a)) TAIL = ( c.c ( a. b.b)) as fórmulas acima obedecem às regras para CONS, HEAD e TAIL definidas anteriormente (Seção 2.1.3). Exemplo: HEAD (CONS p q) = ( c.c ( a. b.a))(CONS p q) CONS p q ( a. b.a) = ( a. b. f.f a b) p q ( a. b.a) ( b. f.f p b)q ( a. b.a) ( f.f p q)( a. b.a) ( a. b.a)p q ( b p) q p Isto significa: • Não existe necessidade real para as funções embutidas HEAD e CONS ou TAIL. • Todas as funções embutidas podem ser modeladas como abstrações-lambda. • De um ponto de vista teórico, isto é satisfatório, para efeitos práticos porém, não é utilizado (eficiência). 2.2.3. Conversão-Alfa Considere: ( x. + x 1) e ( y. + y 1) Evidentemente elas devem ser equivalentes. A conversão- é o nome dado à operação de mudança de nome (consistente) de um parâmetro formal. Notação: ( x. + x 1) ( y. + y 1) λ λ λ λ λ λ λ λ λ λ λ λ → λ λ λ λ λ λ λ → λ λ λ λ → λ λ λ → λ λ → λ → λ λ α λ ↔ α λ INE 5363 - Programação Funcional - INE/CTC/UFSC - Curso de Bacharelado em Ciências da Computação Prof. Dr. rer.nat. Aldo von Wangenheim - http://www.inf.ufsc.br/~awangenh/Funcional -congruência: duas expressões- M e N são -congruentes (ou -iguais), denotado por M N se ou M N ou M N, ou N é obtido de M através da reposição de uma subx- pressão S de M por uma expressão- T tal que S T, ou existe alguma expressão- R tal que M R e R N. 2.2.4. Conversão-Eta Sejam: ( x. + 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- é o nome dado à regra que expressa essa equivalência: ( x. + 1 x) (+ 1) De forma mais geral, a regra da conversão- pode ser expressa assim: ( x. 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 em F previneconversões errôneas. Exemplo: ( x. + x x) não é -convertí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 envovlendo constantes embutidas (predefinidas). EXemplo: TRUE não é -convertível para ( x. TRUE x) Quando a conversão- é utilizada da esquerda para a direita, é chamada de redução- . 2.2.5. Provas de Interconvertibilidade • Freqüentemente será necessário poder-se demonstrar a interconvertibilidade de duas expressões- . α λ α α ≅ ≡ ↔ α λ ↔ α λ ≅ ≅ λ η λ ↔ η η λ ↔ η λ η η λ η η λ INE 5363 - Programação Funcional - INE/CTC/UFSC - Curso de Bacharelado em Ciências da Computação Prof. Dr. rer.nat. Aldo von Wangenheim - http://www.inf.ufsc.br/~awangenh/Funcional • 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: IF TRUE (( p.p) 3) e ( x. 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 interconvertí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 interconvertibilidade de duas expressões, muito mais con- veniente, é o de se aplicar as duas expressões a um argumento w, como: IF TRUE (( p.p) 3) w ( x. 3) w ( p.p) 3 3 3 Portanto: IF TRUE (( p.p) 3) ( x. 3) Esta prova tem a vantagem de somente utilizar a redução e de evitar o uso explícito da conver- são- . O raciocínio por detrás da generalização da interconvertibilidade acima segue abaixo. Suponha que possamos demonstrar que: F1 w E e F2 w E λ λ λ ↔ β ↔ η λ → λ λ λ → λ → → λ ↔ λ η → → INE 5363 - Programação Funcional - INE/CTC/UFSC - Curso de Bacharelado em Ciências da Computação Prof. Dr. rer.nat. Aldo von Wangenheim - http://www.inf.ufsc.br/~awangenh/Funcional 2.3.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 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 CRT1 e CRT2. Teorema de Church-Rosser 1 (CRT1): 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 CRT1, 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 CRT1 diz que todas as seqüências de redução que terminam, haverão de atingir o mesmo resultao. O segundo teorema de Church-Rosser, CRT2, diz respeito a uma ordem particular de redução, chamada ordem normal de redução. Teorema de Church-Rosser 2 (CRT2): 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 (λx.3) (D D), escolheríamos o redex-λx 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). INE 5363 - Programação Funcional - INE/CTC/UFSC - Curso de Bacharelado em Ciências da Computação Prof. Dr. rer.nat. Aldo von Wangenheim - http://www.inf.ufsc.br/~awangenh/Funcional 2.3.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. 2.4. Funções Recursivas ² 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 recursã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.4.1. Funções Recursivas e o Y ² Considere a definição da função fatorial abaixo: FAC = (λn.IF (= n 0) 1 (* n (FAC (- n 1)))) ² Esta definição baseia-se na capacididade 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 = (λn. ... FAC ... ) ² Aplicando uma abstração-b sobre FAC, podemos transformar esta definição em: FAC = (λfac.(λn. (...fac...)))FAC ² Esta definição podemos escrever da forma: FAC = H FAC (2.1) ² onde: INE 5363 - Programação Funcional - INE/CTC/UFSC - Curso de Bacharelado em Ciências da Computação Prof. Dr. rer.nat. Aldo von Wangenheim - http://www.inf.ufsc.br/~awangenh/Funcional H = (λfac.(λn. (...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 nós procuramos por valores de x que satisfazem a equação (neste caso x = -1 e x = 2) . De forma similar, para resolver 2.1, nós procuramos uma expressão lambda para FAC que satisfaça 2.1. A equação 2.1 FAC = H FAC postula que, quando a função H é aplicada a FAC, o resultado é FAC. Nós dizemos 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: λx. * x x 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 Y é chamado de combinador de ponto fixo. Assim, caso possamos produzir um Y, temos uma solução para o problema da recursividade. Para 2.1 podemos prover a seguinte solução: FAC = Y H a qual é uma definição não-recursiva de FAC. Como teste para esta estratégia, podemos computar o valor de (FAC 1). Tomemos as definições de FAC e H: FAC = Y H H = (λfac.λn. IF (= n 0) 1 (* n (fac (- n 1)))) Assim: FAC 1 -> Y H 1 -> H (Y H) 1 ->(lfac.ln.IF (= n 0) 1 (* n (fac (- n 1))))(Y H) 1 ->(ln.IF (= n 0) 1 (* n (Y H (- n 1)))) 1 -> IF (= 1 0) 1 (* 1 (Y H (- 1 1))) -> * 1 (Y H 0) = * 1 (H (Y H) 0) = * 1 ((lfac.ln.IF (= n 0) 1 (* n (fac (- n 1))))(Y H) 0) -> * 1 ((ln.IF (= n 0) 1 (* n (Y H(- n 1)))) 0)