CP/2425 - FAQs

$ % 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{\\&#1& \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.

Q8 - 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 h e pedir ao GHCi o tipo de $f$ (:t f), não é isso que obtém. Ora veja melhor como inferiu esse tipo.

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

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

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

Q12 - No trabalho prático, quando escrevo A ^ B o que aparece no PDF é $\Conid{A}\mathbin{\uparrow}\Conid{B}$ e não o desejado ${\Conid{A}}^{\Conid{B}}$. Como posso alterar isto?

R: Uma sugestão é escrever-se expn A B em lugar de A ^ B, após se ter acrescentado, no anexo onde se pode escrever, a seguinte regra de formatação para o lhs2tex:

%format (expn (a) (n)) = "{" a "}^{" n "}"

Q13 - Gostaria de saber se seria possível disponibilizar o enunciado do 2º teste de Cálculo de Programas com a resolução, tal como fez com o primeiro teste, para poder utilizar como material de estudo para o exame de recurso.

R: Sim - pode ser encontrado aqui.

Q14 - Em relação à questão 6 do de teste de 13-Jan-2023, já identifiquei o tipo de $out$, \begin{eqnarray*} \ensuremath{\rarrow{\mathsf{B\_tree}\;\Conid{A}}{\mathsf{out}}{\mathrm{1}\mathbin{+}(\mathsf{B\_tree}\;\Conid{A}) \times {(\Conid{A} \times (\mathsf{B\_tree}\;\Conid{A}))}^{*}}} \end{eqnarray*} mas estou com dificuldade em identificar o $\fun B$ e o $\fun F$ deste tipo.

R: Vamos seguir a regra estudada nas aulas, começando por, em \begin{eqnarray*} {\mathrm{1}\mathbin{+}(\mathsf{B\_tree}\;\Conid{A}) \times {(\Conid{A} \times (\mathsf{B\_tree}\;\Conid{A}))}^{*}} \end{eqnarray*} substituir por $Y$ todas as ococrrências do lado esquerdo (o tipo indutivo que estamos a definir): \begin{eqnarray*} {\mathrm{1}\mathbin{+} Y \times {(\Conid{A} \times Y)}^{*}} \end{eqnarray*} De seginda substituimos as ocorrências do parâmetro $A$ do tipo indutivo por $X$, \begin{eqnarray*} {\mathrm{1}\mathbin{+} Y \times {(\Conid{X} \times Y)}^{*}} \end{eqnarray*} e de imediato obtemos o bifunctor: \begin{eqnarray*} \ensuremath{\begin{lcbr}\fun B \;(\Conid{X},\Conid{Y})\mathrel{=}\mathrm{1}\mathbin{+}\Conid{Y} \times {(\Conid{X} \times \Conid{Y})}^{*}\\\fun B \;(\Varid{f},\Varid{g})\mathrel{=}{id}\mathbin{+}\Varid{g} \times {(\Varid{f} \times \Varid{g})}^{*}\end{lcbr}} \end{eqnarray*} Para sabermos o padrão de recursividade do tipo basta usar a definição $\fun F\ f = \fun B(id,f)$, o que neste caso dá: \begin{eqnarray*} \fun F\ f = \fun B \;(\Varid{id},\Varid{f})\mathrel{=}{id}\mathbin{+}\Varid{f} \times {(\Varid{id} \times \Varid{f})}^{*} \end{eqnarray*}