$ % 17-Mar-2024 \def\start{&&} \def\more{\\&&} \def\sse#1#2{{#1}\subseteq{#2}} \def\iso{\cong} \newenvironment{lcbr}{\left\{\begin{array}{l}}{\end{array}\right.} \def\ana#1{(\hskip -1ex[#1]\hskip -1ex )} \def\cata#1{(\hskip -1.1pt[\hskip 0.1pt #1 \hskip 0.1pt]\hskip -1.1pt)} \def\Seq#1{{#1}^{\star}} \def\fB{\fun B} \def\mcond#1#2#3{#1 \rightarrow #2\;,\;#3} \newenvironment{lcbr}{\left\{\begin{array}{l}}{\end{array}\right.} \def\bang{{!}} \def\Nat{\mathbb{N}} \def\N{\Nat} \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\inT{\mathsf{in}} \def\outT{\mathsf{out}} \def\implied{\Leftarrow} \def\implies{\Rightarrow} \def\just#1#2{\\& \mathopen{\{}~\mbox{#2}~\mathclose{\}}\\&&} \def\ker#1{\mathbf{ker}\ {#1}} \def\img#1{\mathbf{img}\ {#1}} \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 \,⦆} \def\sep{\rule{15em}{0.3pt}} $
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 - Na questão 2 deste exame, $h: A \times B \to B \times A$ e a sua propriedade natural é semelhante à do $swap$, correto?
R: O tipo de $h$ é o tipo de entrada de $f$. Se definir
f h = cond (p1.p2) swap he pedir ao GHCi o tipo de $f$ (:t f), não é isso que obtém. Ora veja melhor como inferiu esse tipo.
Q3 - Não consigo ver o que fazer para iniciar a questão 4 deste exame.
R: Experimente começar por usar fusão-exp no único sítio onde isso é possível e prosseguir sem usar as leis que se referem.
Q4 - Tenho bastante dificuldade em fazer inferência dos tipos mais gerais de expressões funcionais polimórficas como as que temos visto nas aulas. Há algum texto que sugiram para eu perceber melhor o método, e.g. um road-map de como o fazermos?
R: Sugiro que leia esta nota pedagógica. Nele o métodos de ir fazendo a inferência por partes unificando os tipos é dado com detalhe, incluindo exemplos.
Q5 - Na questão 1 do teste de 1 de Junho de 2022 não há uma troca entre $\mathsf{assocr}$ e $\mathsf{assocl}$? Ou seja, onde está $\mathsf{assocr}$ seria $\mathsf{assocl}$ e vice e versa? Cf. Cp.hs.
R: Sim, estão trocados os nomes! Obrigado por identificar a gralha, que entretanto já foi corrigida.
Q6 - Como é que, na questão 4 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$.
Q7 - Seria possível explicar a passagem do tipo de dados no passo 5 ? Este exercício é referente ao teste 13 Junho de 2020.
R: Nesse passo a parte relevante é o isomorfismo $Bool \iso 1 + 1$. Como $Bool = \{True,False\}$, tem-se que $\larrow{1+1}{\inT}{Bool}$ é $\inT = \alt{\kons{True}}{\kons{False}}$. A sua inversa $\outT$ pode ser obtida resolvendo $\outT \comp \inT = id$ como se fez nas aulas. Sendo assim, $\fbox 5 = id \times out$.
Q8 - Qual é a estratégia para resolver a questão 7 da ficha 7? Eu converti os for's para catamorfismos, cf.
$\begin{lcbr}{f =\cata{\alt{\kons i}{id}}}\\{g =\cata{\alt{\kons i}{\kons i}}}\end{lcbr}$.
O que devo fazer a seguir?
R: Como quer igualar catamorfismos, deverá usar cata-universal, escolhendo um deles. Reparando que $\alt{\kons i}{\kons i} = \kons i$, comece por $g =\cata{\kons i}$ - que deve ser mais fácil! - e obterá facilmente $g$. Sabendo $g$, veja se $f=g$ de novo por universal-cata.
Q9 - Podem-me por favor explicar o exercicio 4 da ficha 11? Não sei bem como atacar este tipo de problemas ainda...
R: Vamos admitir que já se interpretou a declaração dada em Haskell do tipo block tree,
$\verb! data Btree a = Nil | Block {leftmost :: Btree a, block :: [(a, Btree a)]}!$
para $Btree\ A \iso 1 + Btree\ A \times \Seq{(A \times Btree\ A)}$. Pretendemos o functor de base $\fB(X,Y)$ desta definição recursiva. Seguindo a "cábula" que se explica neste vídeo (t =5:50), vamos substituir em $1 + Btree\ A \times \Seq{(A \times Btree\ A)}$ todas as ocorrências do tipo que está a ser declarado, $Btree\ A$, por $Y$:
$~~~~~ 1 + Y \times \Seq{(A \times Y)}$
De seguida, substituimos todas as ocorrências do parâmetro $A$ do tipo que está a ser declarado por $X$:
$~~~~~ 1 + Y \times \Seq{(X \times Y)}$
E temos o functor de base deste tipo: $\fB(X,Y) = 1 + Y \times \Seq{(A \times Y)}$, i.e. $\fB(f,g) = id + g \times map\ (f \times g)$.
Q10 - No trabalho prático, problema 3, construímos esta solução
cat = prj . for loop inic where loop (a, b) = (a + 1, b * ((4 * a) - 2) `div` (a + 1)) inic = (1,1) prj = p2
inspirada pela razão \begin{eqnarray} \frac{C_{n+1}}{C_n} = \frac{4n+2}{n+2} \end{eqnarray} que encontrámos na Wikipedia, mas não soubemos calcular essa solução ou justificá-la formalmente. Como é que isso se pode fazer?
R: De facto, \begin{eqnarray}C_{n+1} = \frac{4n+2}{n+2}C_n\end{eqnarray} obtém-se da definição dada manipulando os factoriais. À partida, esta fórmula sugere recursividade mútua de 3 funções, uma para $C$, outra para o numerador $4n+2$ e outra para o denominador $n+2$. Mas não é isso que acontece na solução proposta, onde o primeiro argumento de $loop$ parece ter "caído de céu".
Ora bem, percebe-se de onde ele vem se se reescrever a igualdade acima como se segue, \begin{eqnarray} C_{n+1} = \frac{4(n+1)-2}{(n+1)+1}C_n \end{eqnarray} que é equivalente a \begin{eqnarray} C_{n+1} = \frac{4(s\ n)-2}{(s\ n)+1}C_n \end{eqnarray} para $s\ n = n+1$. Ou seja: \begin{eqnarray} C_{n+1} = h(s\ n, C_n) \end{eqnarray} para \begin{eqnarray} \begin{lcbr}h(a,b) = \frac{4a-2}{a+1}b \\ s\ n = n+1 \end{lcbr}\end{eqnarray}
Vê-se agora como $C$ está em recursividade mútua com a função sucessor, como acontece com o factorial. Se continuarem o exercício chegam de imediato à solução que construiram intuitivamente.