$ % 20-Mai-2025 \def\Nat{\mathbb{N}} \def\N{\Nat} \def\B{Bool} \def\Seq#1{{#1}^{\star}} \def\alt#1#2{[#1,#2]} \def\ana#1{(\hskip -1ex[#1]\hskip -1ex )} \def\atmost{\subseteq} \def\bang{{!}} \def\cata#1{(\hskip -1.1pt[\hskip 0.1pt #1 \hskip 0.1pt]\hskip -1.1pt)} \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\fB{\fun B} \def\from{\leftarrow} \def\fun#1{\mathsf{#1}} \def\i#1{\mathit{i}_{#1}} \def\img#1{\mathbf{img}\ {#1}} \def\implied{\Leftarrow} \def\implies{\Rightarrow} \def\inT{\mathsf{in}} \def\iso{\cong} \def\just#1#2{\\& \mathopen{\{}~\mbox{#2}~\mathclose{\}}\\&&} \def\cjust#1#2{\just{#1}{ ..................................................................... }} \def\ker#1{\mathbf{ker}\ {#1}} \def\kons#1{\underline{#1}} \def\larrow#1#2#3{#3\ \xleftarrow{#2}\ #1} \def\ldiv{\mathbin{/}} \def\mcond#1#2#3{#1 \rightarrow #2\;,\;#3} \def\more{\\&&} \def\outT{\mathsf{out}} \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\scata#1{⦅\, #1 \,⦆} \def\sep{\rule{15em}{0.3pt}} \def\sep{\rule{15em}{0.3pt}} \def\shrunkby{\mathbin{\upharpoonright}} \def\sse#1#2{{#1}\subseteq{#2}} \def\start{&&} \def\syd#1#2{\frac{#1}{#2}} \def\to{\rightarrow} \def\trans#1{\overline{#1}} \newenvironment{lcbr}{\left\{\begin{array}{l}}{\end{array}\right.} %-------- \def\Varid#1{\mathbin{#1}} \def\ensuremath#1{#1} \def\Conid#1{\mathbin{#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 - Qual é exactamente a matéria que sai para o teste de 22 de Março (2025)?
R: A matéria que sai para o 1º teste é a de todas as fichas até à Ficha nrº 6 inclusive, a que correspondem os slides das aula teóricas T01 a T06 inclusive.
Q3 - Nas aulas práticas não foram resolvidos os exercícios 6 e 8 da Ficha nrº 3. É possível termos as respectivas resoluções?
R: Em exercícios deste tipo o melhor é começar pelo pointfree até chegar ao pointwise. Comecemos pela questão 6 (NB: justificar os passos que são dados): \begin{eqnarray*} \start \ensuremath{\Varid{fac} \comp \alt{\kons{\mathrm{0}}}{\mathsf{succ}}\mathrel{=}\alt{\kons{\mathrm{1}}}{\mathsf{mul} \comp \conj{\mathsf{succ}}{\Varid{fac}}}} \cjust\equiv{} \ensuremath{\alt{\Varid{fac} \comp \kons{\mathrm{0}}}{\Varid{fac} \comp \mathsf{succ}}\mathrel{=}\alt{\kons{\mathrm{1}}}{\mathsf{mul} \comp \conj{\mathsf{succ}}{\Varid{fac}}}} \cjust\equiv{} \ensuremath{\begin{lcbr}\Varid{fac} \comp \kons{\mathrm{0}}\mathrel{=}\kons{\mathrm{1}}\\\Varid{fac} \comp \mathsf{succ}\mathrel{=}\mathsf{mul} \comp \conj{\mathsf{succ}}{\Varid{fac}}\end{lcbr}} \cjust\equiv{} \ensuremath{\begin{lcbr}\Varid{fac}\;(\kons{\mathrm{0}}\;\Varid{x})\mathrel{=}\kons{\mathrm{1}}\;\Varid{x}\\\Varid{fac}\;(\mathsf{succ}\;\Varid{n})\mathrel{=}\mathsf{mul}\;(\conj{\mathsf{succ}}{\Varid{fac}}\;\Varid{n})\end{lcbr}} \cjust\equiv{} \ensuremath{\begin{lcbr}\Varid{fac}\;\mathrm{0}\mathrel{=}\mathrm{1}\\\Varid{fac}\;(\Varid{n}\mathbin{+}\mathrm{1})\mathrel{=}\mathsf{mul}\;(\mathsf{succ}\;\Varid{n},\Varid{fac}\;\Varid{n})\end{lcbr}} \cjust\equiv{} \ensuremath{\begin{lcbr}\Varid{fac}\;\mathrm{0}\mathrel{=}\mathrm{1}\\\Varid{fac}\;(\Varid{n}\mathbin{+}\mathrm{1})\mathrel{=}(\Varid{n}\mathbin{+}\mathrm{1})\mathbin{*}\Varid{fac}\;\Varid{n}\end{lcbr}} \end{eqnarray*}
Passemos agora à questão 8, que é prática: trata-se de correr no GHCi a versão pointfree que foi assunto das questões anteriores:
import Cp
out 0 = i1 ()
out (n+1) = i2 n
fac = either (const 1) mul . (id -|- (split succ fac)) . out
Q4 - Pretendendo-se desdobrar a igualdade $(id \times \p1) \comp \mathsf{assocr} = \p1$ em duas, não estou a ver como fazê-lo...
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.
Q5 - Surgiu-me uma dúvida na resolução do exercício abaixo:
Não consigo entender de que forma tenho que aplicar a lei da troca de modo a obter a resposta. Sei que devo usar a lei Def-+, mas depois o que obtenho não faz sentido.
R: De facto tem de aplicar Def-+ duas vezes. Compare a sua resolução com a seguinte, onde deve preencher as reticências nas justificações: \begin{eqnarray*} \start \ensuremath{\alt{\Varid{f}}{\Varid{g}}\mathrel{=}\conj{\p1+{id}}{\p2+{id}}} % \cjust\equiv{ definição de \ensuremath{\Varid{f}\mathbin{+}\Varid{g}} , 2 vezes} % \ensuremath{\alt{\Varid{f}}{\Varid{g}}\mathrel{=}\conj{\alt{i_1 \comp \p1}{i_2}}{\alt{i_1 \comp \p2}{i_2}}} % \cjust\equiv{ lei da troca } % \ensuremath{\alt{\Varid{f}}{\Varid{g}}\mathrel{=}\alt{\conj{i_1 \comp \p1}{i_1 \comp \p2}}{\conj{i_2}{i_2}}} % \cjust\equiv{ def-\ensuremath{ \times } } % \ensuremath{\alt{\Varid{f}}{\Varid{g}}\mathrel{=}\alt{i_1 \times i_1}{\conj{i_2}{i_2}}} % \cjust\equiv{ igualdade-\ensuremath{\mathbin{+}} } % \ensuremath{\begin{lcbr}\Varid{f}\mathrel{=}i_1 \times i_1\\\Varid{g}\mathrel{=}\conj{i_2}{i_2}\end{lcbr}} \end{eqnarray*}
Q6 - Estou com dúvidas neste exercício de uma das fichas:
Não estou a conseguir entender o significado do ":=" nem o propósito do exercício.
R: Sempre que aparecer $x := e$, isso significa substituir $x$ por $e$ em todas as instâncias de $x$. Neste caso, isso significa substituir $f$ em $f = \ensuremath{\mathsf{ap}} \comp (\trans f \times id)$ por $\mathsf{uncurry}\ g$, obtendo-se $\mathsf{uncurry}\ g = {\mathsf{ap}} \comp (\trans{\mathsf{uncurry}\ g} \times id)$, isto é, $ = \mathsf{uncurry}\ g = {\mathsf{ap}} \comp (g \times id)$. Se introduzir variáveis, eg. $a$ e $b$, obterá $\mathsf{uncurry}\ g(a,b) = \mathsf{ap}(g\ a, b)$, e finalmente: $\mathsf{uncurry}\ g(a,b) = g\ a\ b$.
Q7 - Surgiu-me uma dúvida neste exercicio, como é que eu chego ao tipo mais geral?
R: Sugiro-lhe a leitura desta nota pedagógica. Se continuar com dúvidas, por favor diga.
TBC 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 com a função sucessor, como acontece com o factorial. Se continuarem o exercício obtêm de imediato a solução que construiram intuitivamente.
Q11 - Peço que me elucidem quanto à justificação do passo 3 da Questão 6 deste exame - obrigado.
R: A justificação é a própria lei que é dada, \begin{eqnarray} \cata{\Varid{g}} \comp \cata{\mathsf{in}_2 \comp \alpha } \mathrel{=} \cata{\Varid{g} \comp \alpha} & ~ {\Leftarrow} ~ & \fun G \;\Varid{f} \comp \alpha \mathrel{=} \alpha \comp \fun F \;\Varid{f} \end{eqnarray} em duas partes: (1) mostrar que $g \comp \alpha = \mathit{in}$, por forma a $\cata{g \comp \alpha}=id$; (2) mostrar que $\fun G \;\Varid{f} \comp\; \alpha \mathrel{=} \alpha \comp \fun F \;\Varid{f}$ se verifica (daí a conjunção de dois factos).