2020.5 Conjuntos, Funções, Relações (IMD0101)

Pontos

Pontos de participação e homework

Homework

Obs.:

• Estudar um assunto dum livro obviamente inclui resolver seus exercícios e problemas.
• «Até» é sempre inclusivo.
• Proibido consultar qualquer recursos externo para a resolução dos homeworks. O nosso #studying não é um recurso externo: podem—aliás, devem—usá-lo!
• Homeworks marcados assim são opcionais; considero o resto obrigatório.
• Os HW marcados assim são os únicos que podem ser submetidos para serem avaliados. O prazo para cada um deles será: +2 dias na data, até 23h59m, independente do horário que foi postado no site.
• NÃO MANDEM nenhum Problem Set fora do seu prazo!
• Depois de cada aula, o homework seguinte é sempre válido, obrigatório, e essencial: sem olhar para teu caderno, defina todas as noções e demonstre TODOS os teoremas da aula;

  while (não conseguiu) {
    estude o assunto;
    tente novamente;
  }

11/06/2020

• URGENTE: Nem tente resolver nada desta disciplina sem terminar esses HW relacionados aos prerequisitos:
  1. Assista minha (única) aula gravada do FMC2/2020.1.
  2. Estude os capítulos 1–3 («Introducções», «Linguagens», «Demonstrações»). As minhas aulas relevantes do FMC1/2019.2 (24/07/2019–12/08/2019) podem ajudar, estão no playlist do link acima.
  3. Resolva sozinho o A da Prova 1.1 de FMC1/2019.2.
  4. Estude a resposta do A no seu gabarito.
  5. Assiste a aula com o sermão e a resolução (09/09/2019)
• Os seguintes (também sobre pré-requisitos) podem ser trabalhos em paralelo com os da disciplina:
  1. Estude brutalmente o capítulo «Os números naturais: recursão; indução» do fmcbook e e assista minhas aulas relevantes do FMC1/2019.2 (24/07/2019–11/09/2019).
  2. Estude as «Prova 0» de FMC2 dos semestres passados: 2020.1; 2019.1; 2018.2; 2018.1; 2017.2; 2017.1. Tente resolvê-las sozinho.
  3. Depois, leia bem todas as correções digitalizadas (que tem nos sites) para aproveitar dos comentários disponíveis e evitar erros comuns.

15/06/2020

1. Brinque com o edukera.
2. Brinque com Haskell ou PureScript.
3. Installe e brinque com o Coq; dê uma lida no «Preface» do SF1 (link na Bibliografia); estude o capítulo «Basics» do SF1.
4. Installe e brinque com a Agda; dê uma lida nos tutoriais.
5. §109. Conceito, notação, igualdade
6. §110. Intensão, extensão
7. §111. Relações entre conjuntos e como defini-las
8. §114. Mais set-builder

17/06/2020

1. §112. Vazio, universal, singletons
2. §113. Oito proposições simples
3. §115. Operações entre conjuntos e como defini-las
4. §116. Demonstrando igualdades e inclusões
5. Entenda bem o «Não escreva assim!» da 7.63, e não escreva assim!
6. §117. Cardinalidade
7. §118. Powerset
8. Π7.3; Π7.4; Π7.7

19/06/2020

1. §119. União grande; intersecção grande
2. §120. Tuplas
3. Π7.1–7
4. Problem Set 1: x7.11; x7.14; x7.19; x7.20; x7.22; x7.26; x7.29; x7.30; x7.31; x7.35; x7.37.

21/06/2020

1. Nesse problema é proibido usar os «feitiços fortes»: nem LEM, nem dupla negação, e logo não podes demonstrar algo por Reductio ad absurdum. E logo, para atacar uma disjunção precisa escolher um dos dois componentes e matá-lo!
   Suponha que P denota uma proposição arbitrária. Quais das propriedades seguintes consegues demonsrar?
   1. P ⇒ ¬¬P
   2. P ⇐ ¬¬P
   3. ¬¬(P∨¬P)
   4. se P⇒Q então ¬Q⇒¬P
   5. se ¬Q⇒¬P então P⇒Q
2. Para aquela das duas últimas que tu não conseguiu demonstrar (por justa causa!), tem como demonstrar «quase» isso, ou seja, tem como demonstrar uma coisa parecida mas mais fraca. Adivinha qual é, e demonstre!

22/06/2020

1. §121. Produto cartesiano
2. §122. Implementação de tipo
3. §123. n-tuplas
4. §124. Seqüências
5. §125. Intervalos na reta real
6. Π7.8–10
7. §126. Famílias indexadas
8. §127. Conjuntos indexados vs famílias indexadas
9. §128. Disjuntos dois-a-dois
10. §129. Traduzindo de e para a linguagem de conjuntos
11. §130. Produto cartesiano generalizado
12. §131. Multisets
13. Π7.11–15

24/06/2020

1. Resolva as provas 1.1 seguintes:
   • FMC2/2019.1/1.1T [answers];
   • FMC2/2019.1/1.1N [answers];
   • FMC2/2018.2/1.1T [answers];
   • FMC2/2018.2/1.1N [answers].
   Use o #studying! Depois de tentar cada uma, estude bem o seu gabarito!
2. §132. Conceito, notação, igualdade
3. §133. Diagramas internos e externos
4. §134. Como definir e como não definir funcões
5. §136. Expressões com buracos

26/06/2020

1. Demonstre sem feitiços as
   • ¬¬(P∨¬P)
   • Interdefinabilidade dos ⇒,∨
     • (P ⇒ Q) ⇒ (¬P ∨ Q)
     • (P ⇒ Q) ⇐ (¬P ∨ Q)
     • (P ∨ Q) ⇒ (¬P ⇒ Q)
     • (P ∨ Q) ⇐ (¬P ⇒ Q)
   • De Morgan:
     • ¬(P∨Q) ⇒ (¬P ∧ ¬Q)
     • ¬(P∨Q) ⇐ (¬P ∧ ¬Q)
     • ¬(P∧Q) ⇒ (¬Q ∨ ¬P)
     • ¬(P∧Q) ⇐ (¬Q ∨ ¬P)
     • ¬(∀x)[φ(x)] ⇒ (∃x)[¬φ(x)]
     • ¬(∀x)[φ(x)] ⇐ (∃x)[¬φ(x)]
     • ¬(∃x)[φ(x)] ⇒ (∀x)[¬φ(x)]
     • ¬(∃x)[φ(x)] ⇐ (∀x)[¬φ(x)]
   Obs: não todas são demonstráveis!
2. §137. Um toque de lambda
3. §139. Composição
4. §140. Funcções de graça
5. §141. Aplicação parcial
6. §142. Leis de composição
7. §145. Diagramas comutativos

28/06/2020

1. Demonstre sem feitiços as leis de interdefinabilidade dos ∃,∀:
   • (∃x)[φ(x)] ⇒ ¬(∀x)[¬φ(x)]
   • (∃x)[φ(x)] ⇐ ¬(∀x)[¬φ(x)]
   • (∀x)[φ(x)] ⇒ ¬(∃x)[¬φ(x)]
   • (∀x)[φ(x)] ⇐ ¬(∃x)[¬φ(x)]
   Obs: talvez não todas são demonstráveis!
2. Demonstre sem feitiços as leis:
   • Interdefinabilidade dos ∨,∧:
     • P∨Q ⇒ ¬(¬P∧¬Q)
     • P∨Q ⇐ ¬(¬P∧¬Q)
     • P∧Q ⇒ ¬(¬P∨¬Q)
     • P∧Q ⇐ ¬(¬P∨¬Q)
   • Distributividades:
     • P∧(Q∨R) ⇒ (P∧Q)∨(P∧R)
     • P∧(Q∨R) ⇐ (P∧Q)∨(P∧R)
     • P∨(Q∧R) ⇒ (P∧Q)∧(P∧R)
     • P∨(Q∧R) ⇐ (P∧Q)∧(P∧R)
   Obs: talvez não todas são demonstráveis!
3. Problem Set 2: x7.74; Π7.14; x8.10; x8.15; x8.19; x8.20; a primeira das (26/06/2020-HW1); uma das (28/08/2020-HW2)
4. Demonstre sem feitiços se conseguir, caso contrário, com feitiços:
   • ((P ⇒ Q) ⇒ P) ⇒ P
   • ((P ⇒ Q) ⇒ P) ⇒ ¬¬P

29/06/2020

1. §135. (Co)domíios vazios
2. §138. Novas implementações: seqüências e famílias
3. Problemas: Π8.1–Π8.8
4. §147. Injecções, Sobrejecções, bijecções

30/06/2020

1. Para cada uma das proposições seguintes (i) demonstre se for possível sem feitíços (lógica intuicionista); (ii) caso contrário demonstre se for possível com feitícos (lógica clássica); (iii) caso contrário refute.
   1. (∃x)[φ(x) ∧ ψ(x)] ⇒ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
   2. (∃x)[φ(x) ∧ ψ(x)] ⇐ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
   3. (∃x)[φ(x) ∨ ψ(x)] ⇒ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
   4. (∃x)[φ(x) ∨ ψ(x)] ⇐ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
   5. (∀x)[φ(x) ∧ ψ(x)] ⇒ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
   6. (∀x)[φ(x) ∧ ψ(x)] ⇐ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
   7. (∀x)[φ(x) ∨ ψ(x)] ⇒ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]
   8. (∀x)[φ(x) ∨ ψ(x)] ⇐ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]

01/07/2020

1. §143. Iterações
2. §144. Fixpoints
3. §146. Produtos e demais construções
4. §148. Funcções inversas
5. Problemas: Π8.9, Π8.10, Π8.11, Π8.12

06/07/2020

1. §145. Diagramas comutativos
2. §146. Produtos e demais construções
3. §148. Funcções inversas
4. §149. Funcções de ordem superior
5. §150. Imagens, preimagens
6. §152. Uma viagem épica
7. Problemas: Π8.13–Π8.20

09/07/2020

1. §151. Currificação
2. §153. Funcções estilo pointfree
3. §154. Funcções parciais
4. §155. Definições recursivas [até a nota 8.241: «O que tá acontecendo?»]
5. Problem Set 3: x8.89 (escolhe uma das três); uma das x8.23–24; x8.57; Π8.11; Π8.13; Π8.14; Π8.18; uma das Π8.22–23.

10/07/2020

1. §155. Definições recursivas
2. Resolva as provas 1.2 seguintes:
   • FMC2/2019.1/1.2T [answers];
   • FMC2/2019.1/1.2N [answers];
   • FMC2/2018.2/1.2T [answers];
   • FMC2/2018.2/1.2N [answers].
   Use o #studying! Depois de tentar cada uma, estude bem o seu gabarito!

13/07/2020

1. §156. Coproduto; união disjunta
2. §157. Duma resolução para um problema para uma teoria
3. §158. Pouco de cats—um primeiro toque de categorias
4. Π8.21–Π8.30

15/07/2020

1. §159. Conceito, notação, igualdade
2. §160. Definindo relações
3. §161. Diagramas internos
4. §162. Construções e operações em relações
5. §163. Propriedades de relações
6. §164. Fechos
7. §165. Bottom-up vs. top-down
8. §167. Relações de equivalência

20/07/2020

1. §166. Relações de ordem
2. Π10.1–Π10.14
3. §168. Partições
4. §169. Conjunto quociente
5. Π10.15–Π10.25

23/07/2020

1. Problem Set 4: x8.94; x8.95; x8.99; x8.100; x8.122; x8.127; x8.129; Π8.24; Π8.25.
2. Leia o artigo Revenge of the nerds, de Paul Graham
3. Brinque com Haskell/PureScript/Agda/Idris, usando as idéias que temos encontrado na disciplina
4. Conheça uma LISP: Racket e/ou Clojure
5. Para programadores de Java, C++, e C#: palestra introduzindo Scala por Venkat Subramaniam

26/07/2020

1. Problem Set 5: uma das Π10.1–11; uma das Π10.12–13; duas das Π10.15–25;

Histórico

Obs.: O que aparece nessa cor corresponde em possíveis e-ncontros sincronizados, no horário marcado. O resto é sugestão de quando estudar um assunto, mas o aluno deve efetura esses estudos antes de cada e-ncontro sincronizado, para discutir e possivelmente apresentar suas resoluções de homeworks.

15/06/2020: Meta

15/06/2020: Conjuntos

• Intro: [video]
• Conjuntos: [video]
  • os «def» em cima de = e de ⟺
  • Tipos de objetos e como introduzí-los
  • Conceito de conjunto
  • Noções primitivas: ser conjunto, pertencer (∈)
  • Conjuntos como “black boxes”
  • Igualdade entre conjuntos: A=B
  • Intensão vs extensão
  • Notação
  • Set comprehension (Set-builder notation)
  • Não use «|» como abreviação de «tal que» nem em texto nem nas fórmulas existenciais!
  • Açucar sintáctico no set-builder
  • Erro comum: quantos elementos {x,y,z} tem?
  • As relações binárias: =, ⊆, ⊇, ⊊, ⊋
  • ⊈ vs. ⊊
  • Cardinalidade |A|

17/06/2020: Conjuntos

• Conjuntos: [video]
  • Cuidado: O uso de ⊂ na literatura
  • Definindo o conjunto vazio: nossos deveres
  • O predicado Empty(–)
  • Variáveis livres e ligadas; sombreamento de variável
  • Obrigação de definir notação (nome) para objeto: artigo definido vs. indefinido
  • Provas de existência & unicidade
  • Teorema: existência do conjunto vazio
  • Teorema: unicidade do conjunto vazio
  • O conjunto vazio (Ø)
  • Singletons
  • O conjunto universal
  • Oito proposições sobre o Ø e um conjunto A
  • Escolhendo a ordem de atacar teoremas
  • {Ø} ≠ Ø
  • Operações entre conjuntos e dois jeitos de defini-las
  • As operações binárias: ∩, ∪, \, Δ
  • A operação unária de complemento: ~
  • O operador Powerset (℘)
  • Iterando o ℘ no Ø
  • Cardinalidade de ℘A

18/06/2020: Desastre

19/06/2020: Conjuntos

• Conjuntos: [video]
  • Demonstrando igualdades e inclusões
  • Convenções de notação e nomenclatura
  • As operações unárias de união e intersecção ⋂, ⋃
  • O que é «dual(mente)»?
  • Seguindo as definições
  • Mecanicamente vs. no coração
  • «prova por repetição da definição»
  • Iterando os ⋂ e ⋃ no Ø
  • «por vacuidade»
  • Mais um jogo de demonstração
  • Tuplas
  • igualdade, tamanho, black boxes
  • projeções: πᵢ; projᵢ; fst, snd; outl, outr
  • n-tuplas
  • Implementando um tipo: 3-tuplas

22/06/2020: Conjuntos

• Conjuntos: [video]
  • Recap
  • O tipo de 1-tuplas
  • O tipo de 0-tuplas
  • A única 0-tupla: ()
  • Como pensar no tipo void da C
  • Equações fundamentais de tuplas
  • Produto cartesiano (×)
  • Cardinalidade do A×B
  • Definindo o Aⁿ
  • Implementação-agnóstico
  • Seqüências
  • outras notações
  • União e Intersecção de seqüências de conjuntos
  • Famílias indexadas
  • Exemplo: Os conjuntos Aₚ e Cₚ de todos os ancestrais e todos os filhos de p
  • Traduzindo afirmações da linguagem natural para relações entre conjuntos e vice-versa
  • União e Intersecção de famílias indexadas de conjuntos
  • Família indexada como generalização de n-tuplas e seqüências
  • Σ vs. ⋃
  • Riemann's rearrangement theorem
  • Produto cartesiano generalizado (de família indexada de conjuntos)
  • Um exercício para aprender como atacar e como usar alvos que involvem operações grandes
• Conjuntos: [video até 00:50:55]
  • Conjuntos disjuntos dois-a-dois («pairwise disjoint»): definição com e sem índices
  • Os operadores binários ∪ e ∩ como açucar sintático (definido pelos operadores unários ⋃ e ⋂ respeitivamente)
  • Como usar um fato do tipo D≠Ø em nossas provas: «Seja d∈D.»
  • lim inf, lim sup

24/06/2020: Funções

• Funções: [video a partir de 00:50:56]
  • Conceito, notação, igualdade.
  • Igualdade extensional vs. intensional
  • Duas religiões sobre funções e seus black boxes
  • O conjunto (A→B) (também denotado por B^A)
  • (Co)domínios vazios.
  • Diagramas internos e externos.
  • Como definir e como não definir funções
  • Expressões com buracos.
• Conjuntos, Funções: [video]
  • Seqüências de conjuntos: lim inf, lim sup, lim
  • Cuidado: “sejando” membros de conjuntos sem usar apenas uma variável
  • Diagramas internos e externos
  • Como definir e como não definir funções
  • Diferença entre f(x) e f
  • Expressões com buracos
  • A notação lambda

25/06/2020

• Umas correções do PS1
• Dados / Alvos
• Reductio ad absurdum vs. prova direta de negação

26/06/2020: Funções

• Funções: [video]
  • Mini-sermão sobre provas escritas
  • Um toque de λ-cálculo
  • Computação com λ
  • β-redex; β-reducção
  • α-renomeamento (α-equivalência) e captura de variável
  • η-equivalência
  • essas idéias vistas em conjuntos (set builder)
  • first-class citizens
  • desafio: achar almas (lambdas) para habitar corpos (típos)
  • funções de graça: identidade
  • composição
  • mais funções de graça: inclusão A↪B
  • leis de composição
  • operações totais vs parciais
  • associatividade da composição
  • comutatividade?
  • possui identidade(s)?
  • aplicação parcial
  • mais funções de graça: restricção
  • diagramas comutativos

29/06/2020: Funções

• Funções: [video]
  • constante: três definições
  • função com (co)domínio vazio
  • função característica
  • Unix shell: um calculador de booleanos
  • if-then-else expressions vs branching statements
  • mais funções de graça:
    • cross (f×g);
    • pair (f,g);
    • pointwise (f*g)
    • diagonal Δ
  • Funções injetoras, sobrejetoras, bijetoras: formalmente e informalmente
  • Exemplo: codificação dos pares de Nats nos Nats
  • Cardinalidade de (A↣B)

01/07/2020: Funções

• Funções: [video
  • iterações
  • uma prova errada não quis dizer teorema errado
  • conseqüência de teorema errado não quis dizer que a conclusão é errada
  • a composição preserve as “-jetividades”
  • a frase «pela escolha de»
  • inversas com pontos–“por dentro”
  • exercícios
  • leis da inversa
  • o que podemos concluir se uma composição é bijetora

02/07/2020

• ¬¬(P∨¬P)
• liminf,limsup,lim de seqüência de conjuntos
• RAA vs demonstração direita de negação
• regras de inferência
• (co)domínios vazios

06/07/2020: Funções

• Funções: [video]
  • uma viagem épica: mono e epi
  • estilo pointfree (ou pointless)
  • imagem e preimagem
  • problema na notação
  • possível definição alternativa de preimagem
  • problema na notação alternativa f(X)?
  • funções de ordem superior
  • a função-imagem respeita as uniões e as intersecções?

08/07/2020: Funções [video]

• função-imagem: nível coração
• funções parciais
• funções não-determinísticas
• funções para implementar outros típos
• seqüências, famílias indexadas
• restrição com buraco: seu tipo
• tipos dependentes
• currificação
• programando funções: escopos; dados; alvos;
• definindo funções por recursão
• quantas das k,d,c aceitas como definidas?

09/07/2020: correções

10/07/2020: Funções [video]

• definindo funções por recursão
• associatividade algebrica de operador vs. associatividade sintáctica de conectivo
• higher-order fun
• um λ não terminante
• Quantas idempotentes no 3?
• de união para o coproduto

13/07/2020: Funções; Categorias

• Funções; Categorias [video até 01:21:21]
  • funções
    • Sermão: poluição do escopo
    • de união para o coproduto
    • o problema de definir a f∪g
    • união disjunta ; coproduto ; sum type
    • conjuntos isomórficos/isómorfos
    • definindo a f+g
    • produtos vs. coprodutos: nível coração
  • categorias
    • definição
    • exemplos
    • o conceito de produto

13/07/2020: correções

15/07/2020: Relações

• relações [video a partir de 01:21:21]
  • conceito, notação
  • diagramas internos
  • definindo relações
  • igualdade
  • intensional vs extensional
  • construções e operações em relações
  • relação oposta
  • composição
  • RT=T? RF=F?
• relações [video]
  • notação: R∘S vs S∘R
  • propriedades de relações
  • fechos informalmente
  • a ordem dos fechos importa?
  • fechos formalmente
  • potências/iterações de relação
  • preguiças nos diagramas internos
  • um exemplo de fecho
  • relações de equivalência
  • classes de equivalência

16/07/2020

20/07/2020: Relações; Programação [video]

• Relações
  • fechos: top-down vs bottom-up
  • partições
  • o conjunto quociente
  • enxergando o conjunto quociente
  • subconjuntos finitos vs cofinitos
  • relações de ordem
  • relações recursivas
  • relações de ordem superior
  • perigos de funções mal-definidas
  • ε-perto é uma relação de equivalência?
• Programação
  • paradigmas
  • programação imperativa (procedural; OO)
  • puramente OO
  • programação declarativa (funcional; lógica)
  • side effects
  • lazy vs strict
  • static vs dynamic types
  • puramente funcional

22/07/2020: Relações; Programação [video]

• Relações
  • Quantas relações de equivalência num conjunto com 3 membros?
• Programação
  • Lazy vs strict (call-by-name, call-by-value, call-by-need, call-by-push-value)
  • turing-completeness
  • higher-order
  • dependent types
  • Lisps
  • Abuso de linguagens
  • Conselhos
  • Programação Funcional
  • Indução e recursão nas listas
  • Programação Lógica
  • Funções como relações

27/07/2020

• Correção PS4
• Categorias: conexão entre f(x) e f∘x
• Categorias: composição de função: definição ou obrigação?

29/07/2020

• Correção PS5
• Mais dicas sobre escrita

Futuro (fluido)