cp2425faqs

$ % 17-Mar-2025 \def\Nat{\mathbb{N}} \def\N{\Nat} \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:

Use a lei da troca para resolver em ordem a $f$ e $g$ a equação: $ \ensuremath{\alt{\Varid{f}}{\Varid{g}}\mathrel{=}\conj{\p1+{id}}{\p2+{id}}} $.

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:

Mostre que a definição de $\ensuremath{\mathsf{uncurry}}$ se pode obter da lei de cancelamento da exponenciação $ fazendo \ensuremath{\Varid{f}\mathbin{:=}\mathsf{uncurry}\ \Varid{g}}$, introduzindo variáveis e simplificando.

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

CP/2425 - FAQs¶