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: de acordo com o horário seguinte, sujeito a marcação verbal junto do respectivo docente:

Dia Hora Cursosdown Docente
6.ª-feira 16h00-19h00 LEI+LCC J.N. Oliveira
2.ª-feira 09h00-11h00 LEI L.S. Barbosa
5.ª-feira 09h00-12h00 LEI O.M. Pacheco

  • Essa marcação deve ser feita previamente (eg. por email) com um mínimo de uma semana de antecedência.

Atendimento electrónico (FAQs) tinynew.gif

Q01 - 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 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 . [nil,cons] = in. (id + f.p2)

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

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

== { natural-id; functor-+ }

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

== { universal-cata }

f = (| in. (id + p2) |)


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

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.


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:

f . cons = [ p2, cons ] . distl . (id + id >< f)

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:

f . cons . undistl = [ p2, cons ] . ...........

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

fac = lms p g h i j

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

fac = p -> g, h.<i,fac.j>

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

fac.in = [1,mul.<succ,fac>]

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

fac = [1,mul.<succ,fac>].((=0) -> i1.!,i2.pred)

== { lei do condicional que facilmente se identifica }

fac = (=0) -> [1,mul.<succ,fac>].i1.!, [1,mul.<succ,fac>].i2.pred

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

fac = (=0) -> 1, mul.<succ,fac>.pred

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

fac = (=0) -> 1, mul.<id,fac.pred>

Comparando, obtém-se:

p= (=0)

g= 1 (f. constante 1)

h=mul

i=id

j=pred

e assim

fac = lms (=0) (const 1) mul id pred

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

hwmny p = ([ g ])

(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

B(id,T f) . F (tri f)
que deverá dar
id + id >< (T f . (tri f))
e não
id + (T f) >< (tri f)
Resolvido este engano, deverá ser imediato.

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:

curry π2 · f
= { fusão-exp }
curry (π2.(f >< id))
= { natural-π2 ; natural-id }
curry π2
Segunda parte: que função constante é curry π2? Vejamos: (curry π2 a) b = π2(a,b) = b. Logo curry π2 a transforma sempre b em b: é a função identidade. Em suma: curry π2 = const id.


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

f = g

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

f = cata [const i, const i]

== { universal-cata }

f . in = [const i, const i]. (id + f)

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

[ const i, id ] . (id + f) = [const i, const i]. (id + f)

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

[ const i, f ] = [const i, const i]

== { Eq + }

const i = const i /\ f = const i

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


-- JoseNunoOliveira - 14 Feb 2014