== { universal-ana (naturais); álgebra in dos naturais é [0,succ] }

== { passando isomorfismo [nil,cons]º para o outro lado, "trocando o sinal" }

Aqui começa a preparação das coisas para se obter f como catamorfismo de listas. A dificuldade desta questão é que começa com um anamorfismo de naturais (F f = id + f) e termina com um catamorfismo de listas (F f = id + id x f). A mudança de F dá-se a partir do ponto em que se parou acima. Como sempre, as propriedades naturais não se devem ignorar, neste caso a do p2: f.p2 = p2.(g><f). Continuando:

== { f.p2 = p2.(id><f) , cf. natural-p2 }

== { natural-id; functor-+ }

== { universal-cata }

Q02 - Estou a tentar resolver a questão 6 do teste de 17 de Junho de 2013: fiz os diagramas de cada catamorfismo e chego às definições das funções com variáveis através da lei universal-cata e consigo perceber que realmente fazem a mesma coisa, mas não sei se era assim que era suposto resolver...

R: Não, isso mostra... mas não prova! O que queremos provar é que f=g, sendo ambas catamorfismos. Logo podemos usar a lei-universal aplicada a f ou g, à nossa escolha, por exemplo

Agora basta verificar se const k = g, pelo mesmo processo.

Q03 - Não consigo resolver o exercício 8 da ficha 7 pois só conheço a definição do undistl e não sei o que fazer com distl.

R: Pois, esta é uma situação em que saber que uma função é um isomorfismo natural é bom (natural quer dizer que tem propriedade natural, ou grátis, isto é, é genérico). Vejamos primeiro em que situação é que aparece distl. Após a aplicação das leis universal-cata, ... eq-+, a segunda igualdade fica assim:

A única maneira de dos livrarmos de distl é "deslocá-lo para uma ponta" e depois passá-lo para o outro lado da igualdade, convertido em undistl, por serem inversos entre si. A estratégia é, então : (a) para mover distl para a direita usar a sua propriedade grátis, que se pode deduzir pelo seu tipo e diagrama do costume; (b) de seguida passa-se distl do lado direito para undistl no lado esquerdo. O que se obterá é desta forma:

Como undistl = [ i1 >< id , i2 >< id ], vai haver fusão-+ com f.cons, etc etc o que acabará por dar duas das três linhas da função dada, escrita em pointwise. Fica como exercício.

Q04 - Na questão 7 do exame de recurso de 2011/12 não percebo a primeira parte: instanciar com a função fac a função lms.

R: O que se pretende é resolver a equação

em ordem às variáveis p, g, h, i, j - o que é a mesma coisa que encontrar essas funções na equação

Partimos da definição de fac sem variáveis (onde 1 representa a função constante 1, (const 1)):

== { passagem de in para o outro lado (isomorfismo) ; out dos naturais }

== { lei do condicional que facilmente se identifica }

== { cancelamento-+ ; função constante 1 }

== { Fusão-x ; succ.pred = id, para argumentos > 0 }

Comparando, obtém-se:

e assim

Sugestão: corram esta versão no interpretador de Haskell.

Q05 - No exercício 7 (parte 2 do teste de 2010/2011) tentei chegar da função escrita em Haskell à versão point-free mas não consegui.

R: Escolheu a versão mais complicada, já que no sentido inverso é mais simples: faça absorção-cata no lado direito para obter

(aqui o objectivo é calcular o gene g do catamorfismo). Depois, dessa equação, deriva hwmny p usando a lei universal-cata e introduzindo variáveis no fim. Importante: como o tipo em causa é LTree, in = [Leaf, Fork] e o functor de base a usar na lei de absorção-cata é B(f,g) = f + g >< g - ver baseLTree no ficheiro LTree.hs.

Q06 - Tentei resolver o exercicio 6 do exame de 2012 mas não chego ao resultado que era pretendido. De tri f = (| in . B(id,T f) |) inferi, por cancelamento-cata, (tri f) . in = in . B(id,T f) . F(tri f). Sabendo que B(id,T f) = id + id >< T f e F (tri f) = id + id >< tri f (listas) chego a [tri f . nil, tri f . cons] = [nil, cons . (T f x tri f) ] de onde não consigo chegar ao código Haskell dado.

R: O engano está no cálculo da composição

Q07 - No exercício 6 do teste de 2012/13 eu faço f = g, universal-cata, cancelamento-cata, absorção-+, const k . f = const k e obtenho o resultado [const k, const k] = [const k, f]. O que estou a fazer de errado?

R: Nada, só falta acabar: por cancelamento-+ obtém const k = const k (trivialmente verdadeiro) e const k=f. Isto é: a igualdade f=g é equivalente a f=const k. Por transitividade da equivalência obtém também g=const k, logo as duas funções são iguais à função constante k.

Q08 - No exercício 4 do mesmo teste podemos partir de qualquer propriedade da exponenciação (cancelamento por exemplo)? Ou partimos da igualdade curry f a b = f (a,b)?

R: A direcção do raciocínio fica à sua escolha - veja detalhes acima, na nota What is the meaning of curry / uncurry?

Q09 - O functor F p1 é igual a id + (p1><p1) e o F p2 = id + (p2 >< p2) ?

R: É isso se estiver a trabalhar com LTrees, pois B(f,g) = f + g><g para essa estrutura e F f = B(id,f). Para outras estruturas terá que ver seu functor de base B(f,g) e calcular o respectivo F f.

Q10 - *LTree p1 = (| in . (p1 + id) |)*, da pergunta 9 do teste resolvido do ano 2012/13, foi deduzido ou trata-se de matéria teórica que devemos saber?

R: LTree p1 = (| in . (p1 + id) |) é um caso particular de functor de tipo, deduzido a partir da sua definição no formulário T f = (| in.B(f,id) |). Como se viu na FAQ anterior, B(f,id) = f + id><id para este tipo de árvores (T = LTree). Como id><id=id, o cálculo é imediato.

Q11 - No mini-teste de 2012/13, na questão 6, como é que mostro que max . const(0,0) = const 0?

R: Não esquecer as propriedades naturais da função constante, entre elas esta: f.(const k) = const (f k). Assim, max . const(0,0) = const(max(0,0)) = const 0.

Q12 - Venho por este meio pedir um breve esclarecimento acerca do exercício nrº 1 da ficha 5, pois não estou a conseguir pegar no exercício e chegar à propriedade natural a partir do diagrama.

R: A abordagem tem duas partes: primeiro, saber qual o tipo de ▽; de seguida, inferir a propriedade natural a partir desse tipo. Ora é dado que ▽ · i1 = id e ▽ · i2 = id. Pela lei universal-+ obtemos ▽ = [id, id]. Logo o tipo de ▽ é A + A -> A. A segunda parte - derivar a propriedade natural de ▽ deverá ser simples.

Q13 - Não consigo provar a igualdade da questão 5 da ficha 12 nem perceber de que função constante se trata.

R: Primeira parte: para provar curry π2 · f = curry π2 recorremos à lei de fusão da exponenciação, cf:

Q14 - Não consigo mostrar que f e g são a mesma função na alínea c) da questão 4 da ficha nrº5. Tentei usar a função da questão 9 da ficha nº4 mas também não resultou.

R: Há que usar o cálculo de catamorfismos, pois é muito mais rápido que o uso de definições indutivas como a dessa questão. Queremos mostrar antes de mais que f = g. Como f e g ambas são catamorfismos, podemos usar a lei universal cata, começando pelo que queremos mostrar (objectivo da prova):

== { g = for (const i) i = cata [const i, const i] }

== { universal-cata }

== { f = for id i = cata [ const i, id ] ; cancelamento-cata }

== { absorção + ; funções constantes ; natural-id }

== { Eq + }

Logo f = g <=> f = const i: ambas as funções inicializam o ciclo a 'i' e o resultado não se altera, é sempre 'i'. (experimentem na biblioteca Nat.hs e verão que eg. for 0 id 5 = 0, for 0 (const 0) 5 = 0 etc.)