Cálculo de Programas

Licenciaturas em Engenharia Informática e Ciências da Computação
View   r9  >  r8  >  r7  >  r6  >  r5  ...

Atendimento 9 - 11 May 2019 - Main.JoseNunoOliveira
Line: 1 to 1
 
META TOPICPARENT name="WebHome"

Horário de Atendimento

Line: 208 to 208
 
id + (T f) >< (tri f)
Changed:
<
<
Resolvido este engano, deverá ser imdediato.
>
>
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?

Atendimento 8 - 15 Jun 2015 - Main.JoseNunoOliveira
Line: 1 to 1
 
META TOPICPARENT name="WebHome"

Horário de Atendimento

Line: 266 to 266
 
Added:
>
>
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

Atendimento 7 - 15 Jun 2015 - Main.JoseNunoOliveira
Line: 1 to 1
 
META TOPICPARENT name="WebHome"

Horário de Atendimento

Line: 40 to 40
  f . [nil,cons] = in. (id + f ) . (id+p2)
Changed:
<
<
== { ... }
>
>
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:
 
Added:
>
>
f . [nil,cons] = in. (id + f.p2)

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

f . [nil,cons] = in. (id + p2.(id><f))
 
Changed:
<
<
Aqui começa a preparação das coisas para termos f como catamorfismo de listas: fica como exercício.
>
>
== { natural-id; functor-+ }
 
Changed:
<
<
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 . [nil,cons] = in. (id + p2) .(id + id><f))

== { universal-cata }

f = (| in. (id + p2) |)
 
Line: 77 to 95
 
Changed:
<
<
Q03 - 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.
>
>
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.
 
Changed:
<
<
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] }

>
>
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:
 
Changed:
<
<
f = in. (id + f ) . (id+p2). [nil,cons]º
>
>
f . cons = [ p2, cons ] . distl . (id + id >< f)
 
Changed:
<
<
== { passando isomorfismo [nil,cons]º para o outro lado, "trocando o sinal" }
>
>
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:
 
Changed:
<
<
f . [nil,cons] = in. (id + f ) . (id+p2)
>
>
f . cons . undistl = [ p2, cons ] . ...........
 
Changed:
<
<
== { ... }

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

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

Atendimento 6 - 10 Jun 2015 - Main.JoseNunoOliveira
Line: 1 to 1
 
META TOPICPARENT name="WebHome"

Horário de Atendimento

Line: 238 to 238
 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.

Added:
>
>

 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:


Atendimento 5 - 10 Jun 2015 - Main.JoseNunoOliveira
Line: 1 to 1
 
META TOPICPARENT name="WebHome"

Horário de Atendimento

Line: 234 to 234
 
Changed:
<
<
Q12 - _Venho por este meio pedir um breve esclarecimento acerca do exercício numero 1 da ficha 5, pois não estou a conseguir pegar no exercício e chegar a propriedade natural a partir do diagrama.
>
>
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.

Added:
>
>
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.

 

-- JoseNunoOliveira - 14 Feb 2014


Atendimento 4 - 10 Jun 2015 - Main.JoseNunoOliveira
Line: 1 to 1
 
META TOPICPARENT name="WebHome"

Horário de Atendimento

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

Atendimento electrónico (FAQs)

>
>

Atendimento electrónico (FAQs) tinynew.gif

 
Changed:
<
<
Esta secção será actualizada regularmente com as dúvidas mais frequentes que nos forem colocadas.
>
>
<-- Esta secção será actualizada regularmente com as dúvidas mais frequentes que nos forem colocadas. !-->

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


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


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

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 numero 1 da ficha 5, pois não estou a conseguir pegar no exercício e chegar a 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.


-- JoseNunoOliveira - 14 Feb 2014


Atendimento 3 - 05 May 2015 - Main.JoseNunoOliveira
Line: 1 to 1
 
META TOPICPARENT name="WebHome"

Horário de Atendimento

Line: 8 to 8
 
Dia Hora Cursos Docente
Changed:
<
<
a indicar a indicar LEI L.S. Barbosa
>
>
2.ª-feira 09h00-11h00 LEI L.S. Barbosa
 
6.ª-feira 16h00-19h00 LEI+LCC J.N. Oliveira
5.ª-feira 09h00-12h00 LEI O.M. Pacheco
Changed:
<
<
  • Essa marcação deve ser feita com um mínimo de uma semana de antecedência.
>
>
  • Essa marcação deve ser feita previamente (eg. por email) com um mínimo de uma semana de antecedência.
 

Atendimento electrónico (FAQs)


Atendimento 2 - 05 May 2015 - Main.JoseNunoOliveira
Line: 1 to 1
 
META TOPICPARENT name="WebHome"

Horário de Atendimento

Line: 8 to 8
 
Dia Hora Cursos Docente
Changed:
<
<
a indicar a indicar LEI L.S. Barbosa
6.ª-feira 16h00-19h00 LEI+LCC J.N. Oliveira
a indicar 16h00-17h00 LCC O.M. Pacheco
>
>
a indicar a indicar LEI L.S. Barbosa
6.ª-feira 16h00-19h00 LEI+LCC J.N. Oliveira
5.ª-feira 09h00-12h00 LEI O.M. Pacheco
 

  • Essa marcação deve ser feita com um mínimo de uma semana de antecedência.

Atendimento 1 - 02 May 2015 - Main.JoseNunoOliveira
Line: 1 to 1
Added:
>
>
META TOPICPARENT name="WebHome"

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 Cursos Docente
a indicar a indicar LEI L.S. Barbosa
6.ª-feira 16h00-19h00 LEI+LCC J.N. Oliveira
a indicar 16h00-17h00 LCC O.M. Pacheco

  • Essa marcação deve ser feita com um mínimo de uma semana de antecedência.

Atendimento electrónico (FAQs)

Esta secção será actualizada regularmente com as dúvidas mais frequentes que nos forem colocadas.


Revision 9r9 - 11 May 2019 - 21:26:08 - JoseNunoOliveira
Revision 8r8 - 15 Jun 2015 - 22:20:38 - JoseNunoOliveira
Revision 7r7 - 15 Jun 2015 - 20:26:16 - JoseNunoOliveira
Revision 6r6 - 10 Jun 2015 - 18:29:23 - JoseNunoOliveira
Revision 5r5 - 10 Jun 2015 - 16:51:09 - JoseNunoOliveira
Revision 4r4 - 10 Jun 2015 - 15:43:55 - JoseNunoOliveira
Revision 3r3 - 05 May 2015 - 22:39:21 - JoseNunoOliveira
Revision 2r2 - 05 May 2015 - 09:17:07 - JoseNunoOliveira
Revision 1r1 - 02 May 2015 - 13:36:11 - JoseNunoOliveira
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM