Horário de Atendimento

  • Em qualquer altura: via correio electrónico pressionando aqui. Qualquer outro meio de contacto será considerado informal, não se sentindo a equipa docente vinculada a dar uma resposta em tempo útil.

  • Durante o período de aulas: marcação verbal junto do respectivo docente com um mínimo de 24h de antecedência.

Atendimento electrónico (FAQs) tinynew.gif

Q1 - Estou com dificuldade em resolver um dos exercicios que aparecem na blibliografia (exercicio 2.21, pagina 38 do segundo capitulo), onde é pedido para verificar a seguinte propriedade: < f , ( p -> q , h ) > = p -> < f, q >, < h , f > tendo em conta que p -> f , f = f...

R: Não é de admirar pois, infelizmente, havia uma gralha (!) no exercício, que já se corrigiu no PDF desse capítulo: deverá provar < f , ( p -> q , h ) > = p -> < f, q >, < f , h > e não o que lá estava (troca de f com h).


Q2 - Estou sem conseguir resolver a questão 8 do teste de 2011/12: 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]º ):

f = [( (id+p2). [nil,cons]º )]

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

f = in. (id + f ) . (id+p2). [nil,cons]º

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

f . [nil,cons] = in. (id + f ) . (id+p2)

== { ... }

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 ficha 9, ex. 3, consegui obter as seguintes igualdades:

look k . nil = Nothing

look k . cons = (==k) . π1 . π1 -> Just . π2 . π1, (look k) . π2

Mas não consigo perceber qual será o próximo passo a tomar a partir daqui.

R: Como o functor é F f = id + id >< f, vamos precisar de ter

(look k). in = g . (id + id >< (look k))

É fácil decompor g = [ const Nothing, g2], passando agora a dificuldade a ser resolver a equação

g2. (id >< (look k) = (==k) . π1 . π1 -> Just . π2 . π1, (look k) . π2

em ordem a g2. Por natural-π2, (look k) . π2 = π2. (id >< (look k)). Por natural-π1, π1 = π1 . (id >< (look k)). Substituindo:

g2. (id >< (look k) = (==k) . π1 . (π1 . (id >< (look k))) -> Just . π2 . (π1 . (id >< (look k))), (π2. (id >< (look k)))

que simplifica pela 2ª lei de fusão de McCarthy:

g2. (id >< (look k) = ((==k) . π1 . π1 -> Just . π2 . π1 , π2) . (id >< (look k))

Cancelando (id >< (look k) obtém-se:

g2 = (==k) . π1 . π1 -> Just . π2 . π1 , π2

Esta é de facto a versão de look que aparece na secção (4.2) da biblioteca List.hs.


Q4 - Na ficha 9, ex. 6, chego a

f2 . in = [nil, f1 . π2]

Dado que tenho que aplicar, mais tarde, a lei de Fokkinga, ainda fiz o seguinte passo:

f2 . in = [nil, π1 . <f1, f2> . π2] (*)

mas não consegui avançar mais.

R: A lei que refere vai pedir, para um gene g2 que queremos calcular, f2 . in = g2 . F <f1, f2>, isto é,

f2 . in = g2 . (id + id >< <f1, f2>)

pois estamos a trabalhar como listas. Por natural-π2, <f1, f2> . π2 = π2 . (id >< <f1, f2>). Logo, (*) é o mesmo que

f2 . in = [nil, π1 . π2 . (id >< <f1, f2>)]

Por absorção-+, teremos finalmente

f2 . in = [nil, π1 . π2] . (id + id >< <f1, f2>)

Logo g2 = [nil, π1 . π2]. O raciocínio para f1 é idêntico.


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

f = ([ (const k), id ])
<=> { Universal-cata }
f.in = [(const k), id] . (id + f)
<=> { simplificação }
f.in = [(const k), f]
<=> { cancelamento-cata (f) }
[const k, const k].(id+f) = [(const k), f]
<=> { simplificação seguida de eq-(+) etc }
f = const k

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


-- JoseNunoOliveira - 14 Feb 2014