$ % 10-Jul-2023 \newenvironment{lcbr}{\left\{\begin{array}{l}}{\end{array}\right.} \def\bang{{!}} \def\Nat{\mathbb{N}} \def\atmost{\subseteq} \def\alt#1#2{[#1,#2]} \def\comp{\mathbin\cdot} \def\conj#1#2{\mathopen{\langle} #1, #2\mathclose{\rangle}} \def\conv#1{#1^\circ} \def\crflx#1{\Phi_{#1}} \def\dom#1{\delta {#1}} \def\from{\leftarrow} \def\fun#1{\mathsf{#1}} \def\i#1{\mathit{i}_{#1}} \def\implied{\Leftarrow} \def\implies{\Rightarrow} \def\just#1#2{\\& \mathopen{\{}~\mbox{#2}~\mathclose{\}}\\&&} \def\kons#1{\underline{#1}} \def\larrow#1#2#3{#3\ \xleftarrow{#2}\ #1} \def\ldiv{\mathbin{/}} \def\p#1{\pi_{#1}} \def\plus{\mathbin{\dagger}} \def\rarrow#1#2#3{#1\ \xrightarrow{#2}\ #3} \def\rcb#1#2#3#4{\mathopen{\langle}#1 #2 : #3 : #4\mathclose{\rangle}} \def\rdiv{\mathbin{\setminus}} \def\sep{\rule{15em}{0.3pt}} \def\shrunkby{\mathbin{\upharpoonright}} \def\syd#1#2{\frac{#1}{#2}} \def\to{\rightarrow} \def\trans#1{\overline{#1}} \def\scata#1{⦅\, #1 \,⦆} $
Q1 - Vamos poder levar o formulário para o teste?
R: Como se disse nas aulas e está nos avisos, os alunos poderão levar para as provas de avaliação, se assim o entenderem, o formulário da disciplina em papel, desde que dele não conste qualquer anotação manuscrita ou outra.
Q2 - Que matéria irá sair para o teste de Cálculo de Programas de LCC? E que fichas?
R: Como se disse nas aulas e na sessão de dúvidas, a matéria que sai para o teste é a que está nos sumários e consta dos slides das aulas teóricas. Infelizmente, o calendário não permitiu chegar aos mónades e por isso, em termos de fichas há que excluir a ficha 11.
Q3 - Na ficha 7, questão 4, não consegui sequer começar a desenvolver o raciocínio para provar que $\mathsf{foldr}\ \trans{\p2}$ é necessariamente uma função constante...
R: Primeiro vai ser necessário converter o $\mathsf{foldr}\ ...$ para um catamorfismo de listas, ver questão 1 da mesma ficha: $\mathsf{foldr}\ \trans{\p2}\ i = \scata{\alt{\kons i}{\p2}}$. Queremos agora encontrar $k$ tal que $\kons k = \scata{\alt{\kons i}{\p2}}$. Aqui o raciocínio irá ser usar as leis dos catamorfismos. Ora vejam lá agora...
Q4 - No exercício 5 da mesma ficha, para demonstrar a propriedade $\mu \comp {\fun T} u = id = \mu \comp u$, apenas consegui provar que $ id = \mu \comp u$. Será que me poderia elucidar quanto à prova de $\mu \comp {\fun T} u = id$?
R: Temos $\fun T f = f \times f$, $\mu = \p1 \times \p2$ e $u = \conj{id}{id}$.
Logo, $\mu \comp {\fun T} u = (\p1 \times \p2) \comp (\conj{id}{id} \times \conj{id}{id})$.
Agora, é só aplicar a lei functor-$\times$ e outras do grupo "Produtos" e terá a prova feita.
Q5 - Como é que verifico analiticamente esta igualdade $(f + h) \comp \alpha = \alpha \comp (f + g \times h)$? Tendo em conta que a expressão é a propriedade grátis de $\alpha$.
R: Deverá desenhar o diagrama dessa propriedade para obter o tipo (polimórfico) de $\alpha$. A partir desse tipo irá inferir a definição de $\alpha$. Com essa definição já pode verificar analiticamente a lei.
Q7 - Não percebo como é que, na questão 5 da ficha 2, a igualdade $(id \times \p1) \comp \mathsf{assocr} = \p1$ se desdobra em duas, no 2º passo.
R: Pela lei Def-$\times$ do formulário, $id \times \p1 = \conj{\p1}{\p1\comp\p2}$. Por aplicação da lei de fusão-$\times$, $\mathsf{assocr}$ vai distribuir por esse 'split', dando um 'split' maior que, por aplicação da lei universal-$\times$, faz o desdobramento.
Q8 - Como é que, na questão 6 da ficha 2, obtenho $\mathsf{xr}$ a partir da propriedade $\mathsf{xr} \comp \conj{\conj{{f}}{{g}}}{{h}}\mathrel{=}\conj{\conj{{f}}{{g}}}{{h}}$ ?
R: Como se mostra no início deste vídeo, a melhor solução é resolver a equação auxiliar $\conj{\conj{{f}}{{g}}}{{h}} = id$, e substituir as soluções no lado direito $\conj{\conj{{f}}{{h}}}{{g}}$, pois $\mathsf{xr}$ fica sozinho no lado esquerdo. A igualdade $\conj{\conj{{f}}{{g}}}{{h}} = id$ é facilmente resolvida aplicando a propriedade universal-$\times$.
Q9 - Como é que justifico um passo em que preciso da igualdade $\bang\comp f = \bang$ ?
R: Pelo tipo $\bang : A \rightarrow 1$ infere-se que $\bang$ é uma função constante. Logo a lei Natural-const do formulário aplica-se a $\bang$.
Q11 - Seria possível facultarem a resolução do exercício 7 deste teste quanto ao hilomorfismo dado?
R: O hilomorfismo é de listas, logo $\mathsf B(X,Y) = 1 + X \times Y$. O gene $g$ do anamorfismo obtém-se como se mostra neste vídeo (t=3.58):
$\begin{lcbr} {g}\;[\mskip1.5mu \mskip1.5mu]\mathrel{=}i_1()\ \\ {g}\;({h}\mathbin{:}{t})\mathrel{=}i_2\;({{h}}\in{{t}},{t}) \end{lcbr} $
Finalmente, o gene do catamorfismo capta a parte que produz os outputs: ${f}\mathrel{=}\alt{{\kons{False}}}{\widehat{\mathrel{\vee}}}$.