CSI/2223 - Folha de exercícios práticos nr. 3

20-Abr-2023

$ \def\conv#1{#1^\circ} \def\comp{\mathbin\cdot} \def\atmost{\subseteq} \def\to{\rightarrow} \def\sep{\rule{15em}{0.3pt}} \def\rcb#1#2#3#4{\mathopen{\langle}#1 #2 : #3 : #4\mathclose{\rangle}} \def\larrow#1#2#3{#3\ \xleftarrow{#2}\ #1} \def\rarrow#1#2#3{#1\ \xrightarrow{#2}\ #3} \def\Nat{\mathbb{N}} \def\conj#1#2{\mathopen{\langle} #1, #2\mathclose{\rangle}} $

Q3.1 - Pretende-se especificar o metro de Tóquio onde (cf. figura) há várias linhas ($L$) representadas com cores diferentes, cujas paragens ($P$) estão numeradas sequencialmente e onde as estações ($E$) podem incluir paragens de linhas diferentes $-\!-$ e.g. a estação $\mathsf{Otemachi}$ tem as paragens $\fbox{$\frac C {11}$}$, $\fbox{$\frac M {18}$}$, etc $-\!-$ permitindo aos viajantes mudar de linha.

Sabendo-se que cada paragem está sempre associada a uma e uma só estação, definiu-se o modelo simplificado

que a cada paragem associa a respectiva linha, número e estação. Por exemplo, sendo $p$ a paragem $\fbox{$\frac M {18}$}$ da figura, ter-se-á

$\begin{array}{l}st\ p = Otemachi\\\mathit{ln}\ p = M\\nr\ p = 18\end{array}$.

Claramente, o sistema de numeração das paragens das linhas necessita do seguinte invariante:

Se $n+1$ é o número de uma paragem de uma dada linha, então há outra paragem da mesma linha com o número $n$.

Qual das seguintes formulações desse invariante escolheria,

\begin{eqnarray} && \frac{nr}{succ \cdot nr} \subseteq \frac{ln}{ln} \label{eq:181128a} \\&& \nonumber\\&& \frac{nr}{succ} \subseteq nr \cdot \frac{ln}{ln} \end{eqnarray}

onde $succ\ n = n+1$ é a função sucessor em $\Nat$?

Converta cada "quadrado mágico" na expressão lógica equivalente e decida, justificando.

$\Box$

Resolução:

Repare-se, antes de mais, que

Logo, a opção deverá ir para $\frac{nr}{succ} \subseteq nr \cdot \frac{ln}{ln}$, que converte para o pointwise

\begin{eqnarray} \rcb\forall{n,p} {n+1=nr\ p} {\rcb\exists q {n=nr\ q}{ln\ q = ln\ p}} \end{eqnarray}

(TPC: converter a outra alternativa para lógica quantificada e avaliar o desvio em relação ao pretendido.) </span>

Q3.2 - A figura é retirada da página da Wikipedia sobre o protocolo de troca de chaves de Diffie–Hellman, onde informação numérica é simplificada sobre a forma de cores,

cf. também o quadro seguinte:

Informaçao pública Informação privada (Alice) Informação privada (Bob)
yellow red cyan
orange = yellow + red blue = yellow + cyan
orange, blue
blue + red orange + cyan

O protocolo assume que $f = (yellow +)$ tem uma inversa à esquerda $g$ (i.e. tal que $g \cdot f = id$), mas $g$ é computacionalmente muito complexa.

Contudo, para o "common secret" poder ser obtido de forma independente por Alicee Bob é preciso que o quadrado mágico

\begin{eqnarray} R\ \cdot S \subseteq P \cdot Q \end{eqnarray}

se verifique para uma determinada escolha de $R$, $S$, $P$ e $Q$. Identifique essa escolha e justifique-a.

$\Box$

Resolução:

\begin{eqnarray*} && blue + red = orange + cyan \\&\equiv& \mbox{\{substituting\}} \\&& % new term (yellow + cyan) + red = (yellow + red) + cyan \\&\equiv& \mbox{\{go pointfree\}} \\&& % new term (+ red) \cdot (+ cyan) \cdot \underline{yellow} = (+ cyan) \cdot (+ red) \cdot \underline{yellow} \end{eqnarray*}

Em geral:

\begin{eqnarray} (+ a) \cdot (+ b) = (+ b) \cdot (+ a) \end{eqnarray}

isto é, a operação $x+y$ de combinação de "cores" é permutativa.

NB: recordar que, pela lei da inclusão de funções, $(+ a) \cdot (+ b) = (+ b) \cdot (+ a)$ é a mesma coisa que $(+ a) \cdot (+ b) \subseteq (+ b) \cdot (+ a)$.

Q3.3 - A forma mais habitual de desenvolver um programa é usar uma bateria de testes para "verificar" se o programa passa os testes e, caso isso não aconteça, corrigi-lo e sujeitando-o de novo aos testes, etc etc (cf. o ciclo "edit-compile-run").

Um programa $P: A \rightarrow B$ é uma relação simples que para entradas em $A$ dá saídas (ou não) de tipo $B$.

Queremos melhorar $P$ com base numa bateria de testes $R : A \rightarrow B$ que indica que saídas em $B$ são aceitáveis para que entradas em $A$.

Suponha que modifica $P$, obtendo $Q$ tal que

\begin{eqnarray} id \cap P^\circ \cdot R \subseteq Q^\circ \cdot R \end{eqnarray}

se verifica.

Acha que $P$ piorou ou melhorou? E porquê?

Como escreveria $id \cap P^\circ \cdot R \subseteq Q^\circ \cdot R$ como um quadrado mágico?

$\Box$

Resolução:

\begin{eqnarray} \forall\ a : \mathopen{\langle} \exists b : b R a : b P a \mathclose{\rangle} \Rightarrow \mathopen{\langle} \exists b' : b' R a : b' Q a \mathclose{\rangle} \end{eqnarray}

Não piorou: $Q$ responde bem pelo menos onde $P$ já respondia bem.

\begin{eqnarray*} \def\conj#1#2{\mathopen{\langle} #1, #2\mathclose{\rangle}} \def\conv#1{#1^\circ} \def\comp{\mathbin\cdot} \def\atmost{\subseteq} %----------- && id \cap P^\circ \cdot R \subseteq Q^\circ \cdot R \\&\equiv& \mbox{\{ identidade \}} \\&& % new term id^\circ \cdot id \cap P^\circ \cdot R \subseteq Q^\circ \cdot R \\&\equiv& \mbox{\{(5.108) do formulário\}} \\&& % new term \conv{\conj {id} P} \comp \conj {id} R \atmost \conv Q \comp R \end{eqnarray*}