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:
- Essa marcação deve ser feita previamente (eg. por email) com um mínimo de uma semana de antecedência.
Atendimento electrónico (FAQs)
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