Q02 - Consigo ver que o exercício 5.21 deverá basear-se nas leis (5.62) e (5.63) mas não consigo completar o raciocínio. Como devo prosseguir?

R: Ou S vai ser simples e R injectiva ou vice-versa. Coloquemos a primeira hipótese:

(P ∩ Q)·S = (P·S) ∩ (Q·S)

<= { (5.62) }

P · img S ⊆ P ∨ Q · img S ⊆ Q

<= { img S ⊆ id por hipótese; regra do ponto-médio B }

P · id ⊆ P ∨ S · id ⊆ S

<= { P · id = P etc }

true

Agora é só verificar R·(P∩Q) = (R·P)∩(R·Q) para R injectiva, seguindo o mesmo método.

Q03 - Na resolução da questão 4 do teste do ano passado há uma altura em que chego a qualquer coisa como dE . V . i1◦ ⊆ Di . i1◦. Por monotonia da composição (. i1◦) consigo ver que dE . V ⊆ Di implica dE . V . i1◦ ⊆ Di . i1◦. Mas eu preciso que sejam equivalentes. Sugestões?

R: Por 'shunting' de i1◦ do termo inferior para o superior (sem o converso), obtém-se i1◦ . i1 nesse lado. Ora i1◦ . i1 = id pois i1 (e i2) são injecções (funções injectivas, cujo núcleo é id). Basta então 'cortar' i1◦ . i1, não havendo perda da equivalência.

Q04 - Não sei como pegar no exercício 5.24...

R: Este tipo de exercícios deve ser abordado usando monotonia ou regras de algibeira como (5.82, 5.83) etc. Exemplo: sabemos que R ∩ S ⊆ R fazendo X := R ∩ S na propriedade (5.58) e simplificando. Vamos supor que R é simples. Como "menor que simples é sempre simples" (5.82) então R ∩ S será simples. Etc para os outros casos.

Q05 - Como é que se aplica a igualdade indirecta no exercício 5.46? Não consigo ver como.

R: A igualdade c◦ · (⊤ − c) = ⊥ é equivalente a c◦ ·(⊤−c) ⊆ ⊥. Por (5.151) podemos subir o lado inferior, para c◦ ·(c⇒⊥) ⊆ ⊥. A partir daí aplica-se a (5.154), obtendo-se (c◦ ·c⇒⊥) ⊆ ⊥. Agora é que se pode aplicar a igualdade indirecta para mostrar que c◦ ·c⇒⊥ = ⊥.

Q06 - Não estou a conseguir fazer a primeira prova do exercício 5.37. Como é que se pega na questão?

R: Ora vejamos:

[R,S]·[T,U]◦

= { (5.117) }

(R·i1◦ ∪ S·i2◦) · [T,U]◦

= { justificar }

(R·i1◦·[T,U]◦) ∪ (S·i2◦·[T,U]◦)

= { justificar }

R·([T,U]·i1)◦ ∪ S·([T,U]·i2)◦

.... (Agora é só continuar)

Q07 - Ao resolver uns exercícios deparei-me com uma dúvida: R◦ × S◦ = (R × S)◦ verifica-se?

R: Sim, verifica-se, como facilmente se prova: ( R × S )◦ = ⟨R·π1,S·π2⟩◦ = (π1◦ · R·π1 ∩ π2◦ · S·π2)◦ = R◦ × S◦

Q08 - Consegui resolver a primeira prova do 5.39 mas não estou a conseguir resolver a segunda...

R: Na segunda usam-se as propriedades dos coprodutos. Por exemplo, se se começar por (g+k)◦ . (f + h), como (f + h) = [ i1.f, i2.h], usa-se fusão-+ (relacional, igual à funcional) e fica-se com [(g◦+k◦).i1.f,(g◦+k◦).i2.h] (onde também se usou 5.123). De seguida obtém-se [i1.g◦.f,i2.k◦.h], que é igual a f/g + h/k.

Q09 - No teste, para quem realizar a 2ª parte da matéria, excluindo a matéria do mini-teste, que capítulos sairão?

R: A matéria que foi dada depois do miniteste é a seguinte: secções 5.20, 5.21, 5.24 e capítulo 7.

Q10 - Não consigo perceber a justificação ao fundo da página 255.

R: É de esperar, já que a justificação está muito imprecisa. Em geral, as funções constantes são tudo menos injectivas (!). Mas, aqui, o tipo de const c é 1 -> N0 (vejam porquê). Logo, const c é injectiva, pois o seu núcleo é de tipo 1 -> 1 e a maior relação possível nesse tipo é id : 1->1. (Agradeço esta dúvida, pois permitiu melhorar já a justificação que irá sair na próxima versão dos apontamentos.)

Q11 - Na última questão do teste de 17/18 não consigo justificar o terceiro e o quarto passo.

R: As justificações são as seguintes: 3) teorema grátis de swap; 4) (F8), após fazer-se 'shunting' de θº.

Q12 - Na questão 6 do teste do ano passado não consigo justificar o segundo passo.

R: Fazendo 'shunting' de splitAt da esquerda para a direita em splitAt ⊆ ((R* × R*) ← R*) · splitAt ficamos com id ⊆ splitAtº .((R* × R*) ← R*) · splitAt. De seguida introduzimos variáveis, eg. n e n'. Como n id n' é n=n', uma dessas variáveis desaparece.

Q13 - Não sei como justificar o penúltimo passo da questão 7 (segunda parte) do teste de 17/18.

R: Dos quatro termos que estão a ser reunidos, se se isolar i1·(R◦·R)·i1◦ ∪ i2·(S·S)·i2◦, verifica-se que essa reunião é ker R + ker S por aplicação das leis dos coprodutos (R+S = [ i1· R, i2· S ] etc).

Q14 - Não percebo qual a razão para a cláusula 'injective(const e· (const c)◦)' desaparecer no penúltimo passo da prova sugerida para a questão 7 do teste de 18/19.

R: Uma relação R é injectiva sse ker R ⊆ id. Neste caso, R = const e· (const c)◦, logo ker R = const c . (const e)◦ . const e· (const c)◦ ⊆ id. Se fizermos os 'shuntings' do costume, obtém-se ker R ⊆ id ≡ ⊤ ⊆ ⊤, por (6.28).