Q2 - Estou sem conseguir resolver a quest�o 8 do teste do ano passado: definir um anamorfismo de naturais como um catamorfismo de listas. Tentei usar a lei universal-ana(44) mas fiquei bloqueado a meio.

R: Sim, universal-ana (naturais) � bom come�o (expandindo out = [nil,cons]� ):

== { 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 termos f como catamorfismo de listas: fica como exerc�cio.

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).

Q3 - Na quest�o 7 do exame de recurso do ano passado 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.

Q4 - Tenho dificuldades ao provar a igualdade f.g=id na quest�o 6b da Ficha 2.

R: Ver resolu��o do miniteste, onde se faz essa prova para o caso dual, com injec��es e eithers em lugar de projec��es e splits: o argumento � em tudo semelhante.

Q5 - Tenho dificuldades a resolver a quest�o 6 da Ficha 3.

R: O diagrama representa a equa��o

que se quer resolver em ordem a x e y. Por absor��o (etc), o lado direito fica [k,g.(id >< f)] ; pela igualdade de eithers tem-se, de imediato,

Quanto aos pontos de interroga��o, comecemos pelo tipo gen�rico da seta vertical, que � a soma de uma identidade com um produto:

(repetimos A e B por estarem ligados a identidades). Como nada sabemos sobre k e g, ter-se-�

Logo, os pontos de interroga��o s�o os tipos gen�ricos (param�tricos) A + (B >< D) (em cima); E (em baixo, � esquerda) e A + (B >< C) (� direita).

Q6 - Na quest�o 2a da Ficha 5, o isomorfismo pretendido parte de uma soma para um produto, logo posso usar tanto um split como um either. Qual devo escolher?

R: Pela lei da troca, as suas solu��es s�o id�nticas. (Se se pretender depois escrever a fun��o em Haskell, a convers�o � mais simples se se optar pelo combinador either). Detalha-se a seguir essa vers�o: designemos o isomorfismo por iso, que vamos decompor em iso = [f,g], com tipos, f : A >< B -> A >< (B+1) e g : A -> A >< (B+1). Tanto f como g v�o para produtos e como tal ser�o splits. Come�ando por g = <g1,g2>, g1 = id e g2 tem tipo A -> B+1. Como nada sabemos sobre B, g2 ter� que dar o seu resultado em 1, injectando-o � direita: g2 = i2.!. Um processo semelhante decompor� f em id >< i1. Juntando tudo:

Q7 - 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.

Q8 - N�o percebo bem o que se pretende na quest�o 4 da Ficha n� 5.

R: A quest�o resume-se a tentar calcular o tipo polim�rfico do combinador comb f g, para qualquer f e g � entrada. Temos que comb f g = <f,[g,f]>. Sejam ent�o dadas f : A->B e g : C -> D. Ter-se-� de imediato: [g,f] : (C + A) -> B, j� que B=D na constru��o do either.

Agora derive-se o tipo do split <f,[g,f]>. Para isso � preciso que f e [g,f] tenham o mesmo tipo de entrada, isto �, ter� que verificar-se:

Ora esta equa��o define A como um tipo recursivo: mas, se substituirmos A por C+A e assim sucessivamente, teremos A = C + (C + (C + ...)), isto �, A � um tipo infinito: � esta, assim, a explica��o para a mensagem de erro que o interpretador de Haskell d�: "cannot construct the infinite type: a = Either c a".

Q9 - Na quest�o 5(a) da Ficha n� 5 eu escrevi Maybe A isomorfo a A + 1 e na 5(b) escrevi 1+1 isomorfo a Bool, mas n�o sei prosseguir com nenhum dos exerc�cios.

R: Para acabar os exerc�cios tem que se lembrar da estrutura dos tipos Maybe e Bool em Haskell: data Maybe a = Just a | Nothing e data Bool = False | True. Repare nos tipos: Just :: a -> Maybe a e const Nothing :: () -> Maybe a, const True :: () -> Bool e const False :: () -> Bool. Usando estas fun��es constantes � f�cil definir os isomorfismos pedidos sob a forma de eithers.

Q10 - Na quest�o 4 da Ficha n�6 eu substitui as tr�s ocorr�ncias de exp pela sua defini��o mas n�o sei prosseguir...

R: Sabendo-se que exp f = curry (f.ap), � conveniente olharmos para as leis da exponencia��o primeiro antes de fazermos substitui��es: para a lei fus�o-exp (31) ser �til, basta come�ar por expandir apenas exp f:

Q11 - 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

Q12 - No exercicio 5 da ficha 12, em que join = (| [id, Fork] |), pede-se para demonstrar as leis da multiplica��o e unidade do mon�de LTree, sendo u -> Leaf e mu -> join. Usando universal-cata e decompondo, chega-se a join . Leaf = id, que prova a lei mu.u = id. Mas n�o consigo chegar a mu.mu = mu . (T mu).

R: Dever� usar absor��o-cata � direita seguida de fus�o-cata � esquerda (tudo em LTree):

== { defini��o de join }

== { absor��o-cata: T f = LTree f ; B(f,g) = f + g >< g }

== { B(f,id) = f + id ; defini��o de join }

<= { fus�o cata }

== { leis dos coprodutos }

== { Eq-+ }

== { cancelamento-cata sobre (| [id, Fork] |) }

Q13 - Na p�gina 78 do cap�tulo 3, onde se faz a demostra��o da composi��o de (|g|) . [(h)], diz-se que � uma fun��o que vai de B para C. No entanto, o diagrama leva-me a crer que se trata de uma fun��o de C para B. Est�-me a escapar alguma coisa?

R: N�o est� a escapar nada: � de facto uma gralha, que foi agora corrigida no original (LaTeX).

Q14 - N�o estou a conseguir resolver o exerc�cio 8 da ficha 4, nomeadamente na prova de map f . nil = nil. Quais s�o as leis a aplicar para chegar � solu��o?

R: Ter� que ser a equa��o (7), j� que nada sabemos (na pergunta) sobre map. E, de facto, a equa��o (8) corresponde ao lado esquerdo de (7) com k=id e f=id. Se fizermos a substitui��o, teremos o seguinte lado direito:

que � evidentemente verdadeira. Para verificarmos a (9), basta em (7) fazermos a substitui��o de k por map f no lado direito e seleccionarmos o caso nil:

Por fus�o-+ no lado esquerdo e absor��o-+ no direito obtemos, ap�s eq-+, duas equa��es, das quais uma delas � (9). Finalmente, (10) corresponde � outra equa��o que resta, ap�s introduzirmos vari�veis.

Q15 - No exerc�cio 5 da ficha 9, ap�s a remo��o das vari�veis, introdu��o de in, cancelamento-+ e absor��o-+, n�o estou a conseguir obter o resultado f1.in = ... (id + id x <f1, f2>) e g1.in = ... (id + id x <f1,f2>) para depois aplicar a lei de Fokkinga.

R: Ap�s remo��o de vari�veis, as equa��es dadas convertem em

Onde est� f1 ou f2 teremos que ter um termo que envolva <f1,f2>, o que n�o � dif�cil usando as leis de cancelamento-x:

Juntando cada par de equa��es num s�, fazendo in=[nil,cons], ter-se-�:

Falta agora factorizar a chamada recursiva id + id x <f1,f2> em ambas as equa��es:

Agora j� pode ser aplicada a lei da recursividade m�ltipla (acabar).

Q16 - No exerc�cio 2 da ficha 10, no anamorfismo suffixes consegui desenhar o diagrama mas n�o estou a conseguir descobrir o gene da fun��o g para proceder ao c�lculo da vers�o em Haskell.

R: Uma vez mais, pegue-se na defini��o do gene

e retirem-se as vari�veis:

j� que <cons,p2>(h,t) = (cons(h,t),p2(h,t)) = (h:t,t). Daqui procede-se da mesma maneira, juntando essas equa��es por Eq-+:

Q16 - No exerc�cio 6 do teste deste ano 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.

Q17 - 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?

Q18 - Tenho visto em testes de anos anteriores mais para o final uma quest�o do tipo: "Defina a fun��o .... (...) como resultado da "monadifica��o" da fun��o: (...) Eu tentei preparar-me para teste resolvendo todas as fichas que demos nas aulas mas n�o encontrei nenhuma pergunta na ficha de monades com semelhan�a a esta. Como tal sempre que chego aquela pergunta fico sem perceber como "pegar". Sa�r� algo parecido com isto no teste? Ser� que poderia dizer como se resolve?

R: Essa mat�ria n�o foi dada este ano, logo n�o sair� nenhuma pergunta desse g�nero.

Q19 - 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.

Q20 - *LTree p1 = (| in . (p1 + id) |)*, da pergunta 9 do teste resolvido do ano passado, 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.

Q21 - No mini-teste deste ano, 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.

Q22 - Nas justifica��es dos passos numa prova anal�tica, quando introduzimos vari�veis, a justifica��o tanto pode ser "igualdade extensional", bem como "introdu��o de vari�veis"? Ou h� uma justifica��o que seja mais correcta que a outra?

R: As duas est�o bem: a introdu��o de vari�veis � equivalente � igualdade extensional.

Q23 - Ao tentar resolver a quest�o 8 do este de recurso do ano passado, n�o consigo entender bem o que � pedido.

R: � dado um anamorfismo g = [( i2. <id,id> )] e pretende-se mostrar, usando as leis dos anas, que

Ora o anamorfismo � de listas, o que quer dizer que sabemos que: B(f,g)=id+f><g, F f = B(id,f) = id + id><f e map f = T f. Estamos ent�o em condi��es de usar a lei de absor��o-ana,

e acabar de resolver o exerc�cio.

Q24 - Quando queremos identificar um isomorfismo recorrendo a diagramas, depois de construir os tipos das duas testemunhas, para provar o isomorfismo basta escrever, por exemplo, (A x A)+(B x A) ~= (A+B) x A no fim e fica provado?

R: N�o fica. O diagrama apenas revela os tipos (polim�rficos) das duas fun��es. Para o isomorfismo ficar provado precisamos de mostrar que as duas fun��es, compostas por qualquer ordem, d�o a identidade.

Q25 - No recurso do ano passado, na quest�o 5, quando chegamos ao passo pair p = for (<succ.p1,k p>) (<1,0>) como � que introduzimos aqui as var�aveis (x,y)? � para introduzir dentro de cada argumento do for?

R: N�o! O for j� est� definido ao n�vel da vari�vel. O que se pretende no exerc�cio � obter loop e mostrar que, ap�s introdu��o de vari�veis (apenas em loop), essa fun��o � a dada no exame.

Q26 - (a preencher)

R: (a preencher)