2021.1 FMC2, turma de Thanos

Horários sincronizados: (quando tiver) será dentro dos 246N34 [20h35–22h15]
Contato:thanos@imd.ufrn.br
Playlists: FMC2 2019.1 (aulas gravadas)
TeX / LaTeX / ConTeXt (minicurso e sermões)
Monitoria/TA: fmc.imd.ufrn.br
Turmas anteriores: ..

Info

Pré-requisitos

É pré-requisito ter aprendido bem o conteudo transversal de FMC1. Sem aprender esses assuntos primeiro, não faz sentido se matricular em FMC2.

(Obs.: aprenderpassar.)

Então—ANTES de começar—é bom estudar os capítulos seguintes do fmcbook:

  • Introducções
  • Linguagens
  • Demonstrações
  • Naturais; recusão; indução

Alem disso, é pré-requisito que os alunos matriculados tem tempo e vontade para estudar, fazer os (muitos) trabalhos atribuídos, etc.

(Obs.: estudarler.)

Antes de começar é bom dar uma lida nos:

  1. Comments on style de James Munkres.
  2. A parte “Writing mathematics” do livro The tools of mathematical reasoning, de Lakins.

Disclaimer. Eu suponho que os alunos desta turma verificaram os pré-requisitos da disciplina e assumam responsabilidade sobre o seu conhecimento. Lembrete:

pré-requisito

substantivo masculino

  1. condição prévia indispensável para se alcançar algo, seguir uma formação, fazer um curso, ocupar uma função etc.
  2. *(pedagogia)* num currículo, disciplina cursada obrigatoriamente antes de outra, por envolver conhecimentos prévios necessários ao estudo da segunda.

Conteúdo

Conteúdo transversal (durante todas as unidades)
Lógica proposicional e de predicados. Linguagem matemática de definições, teoremas, demonstrações, etc. Definições por recursão – provas por indução. A linguagem de conjuntos, funções, e relações.
Conjuntos, Funções, e Relações
Conjuntos, sua notação, suas operações, e seus leis. Uniões disjuntas, famílias e partições. Tuplas ordenadas e produto cartesiano. As operações unitárias de união e interseção. As relações de subconjunto, e de pertencer. Multiconjuntos e sequências.

Funções, o conceito de função e suas propriedades. Intensão x extensão. Domínio, codomínio. Imagem, pre-imagem. Funções totais e parciais, injetivas, sobrejetivas, bijetivas. Aridade. Função constante, função identidade, projeções, funções características. Funções recursivas; recursão mutual. Funções de ordem superior. A notação de λ-calculus. Funções x predicados.

Relações e suas propriedades. Relações de equivalência, clásses de equivalência. Operações em relações, inversão, composição, fechos.

Aplicações e assuntos auxiliares
Enumerações e conceito intuitivo de cardinalidade. λ-calculus, lógica combinatória. Elementos de teoria dos tipos. Fixpoints e recursão. Programação funcional. Programação lógica. Bancos de dados.

Bibliografia

(Conhece o libgen.rs?)

Principal

Auxiliar

Para cada um dos assuntos que tratamos, procure a secção «Leitura complementar» no capítulo correspondente do fmcbook para mais referências.

  • Pinter: A book of abstract algebra (2–5, 6, 12, 17)
  • Aluffi: Algebra: Chapter 0 (1, 2)
  • Davey & Priestley: Introduction to lattices and order (1, 2) [DP]
  • Lawvere & Schanuel: Conceptual Mathematics: A first introduction to categories (I, II)
  • Raymond Smullyan: A beginner’s guide to mathematical logic (Volume 1)
  • Birkhoff & Mac Lane: A survey of modern algebra (1.11; 1.1–1.5, 1.10, 1.12)
  • Herstein: Topics in Algebra (2.1–2.5 [skip # and ∗])
  • Simmons: Introduction to topology and modern analysis (1)
  • Loomis & Sternberg: Advanced Calculus (0)
  • João Marcos: Lógica Aplicada à Computação website (TdC, R&I)

Programação e proof assistants

Links

Dicas

Tecnologias e ferramentas necessárias

Obs.: As tecnologías/ferramentas seguintes podem mudar durante a disciplina—exceto a primeira.

  1. PAPEL (um caderno para dedicar à disciplina) e LAPIS/CANETA
  2. TeX / LaTeX / ConTeXt. (Online editor/compilador: Overleaf.)
  3. Um aparelho com câmera e uma ferramenta para escanear teu caderno
  4. Zulip: leia as instruções
  5. Google Meet
  6. O proof assistant Coq para algumas atividades. (Coq à la pastebin: CollaCoq.)
  7. Possivelmente usaremos outros proof assistants e linguagens de programação também.
  8. Git e uma conta no github ou gitlab.
  9. Muito recomendado mas não necessário: um sistema Unix (Minicurso Unix 2019.2)
  10. Muito recomendado mas não necessário: (neo)vim e Emacs

(Instalem e criem uma conta para usar onde necessário.)

Regras

  1. Nunca escreva algo que você mesmo não sabe explicar: (i) o que significa; (ii) seu papel na tua resolução. Por exemplo: um aluno escreveu a frase seguinte na sua demonstração: «Como f é cancelável pela esquerda temos que g=h». Ele deve saber o que significa ser cancelável pela esquerda é também explicar como isso foi usado e/ou o que isso tem a ver com essa parte da sua demonstração.
  2. Qualquer trabalho poderá ser questionado em forma de prova oral via videochamada, em modo privado ou aberto. Se um aluno não consegue explicar o que ele mesmo escreveu numa resolução, será considerado plágio e o aluno será reprovado imediatamente por nota e por faltas.
  3. Participando, nunca dê uma resposta que tu não pensou sozinho.
  4. Não tente “forçar a barra” perguntando ou respondendo coisas aleatórias com objetivo único de ganhar pontos. Os pontos de participação não correspondem em apenas perguntas ou dúvidas que mostram interesse. O interesse é implícito pelo fato que tu escolheu matricular nesta turma—não vale pontos.
  5. Não procurem resoluções em qualquer lugar fora dos indicados no cada homework. O único recurso aceitável para procurar ajuda é o nosso Zulip, especificamente seus canáis públicos (não DM).
  6. Proibido consultar o apêndice de resoluções do fmcbook durante a disciplina exceto quando for explicitamente permitido por mim. (Os apêndices de dicas são permitidos sim.)

Avaliação e faltas

Disclaimer. Eu suponho que os alunos desta turma escolheram se matricular por interesse em aprender seu conteudo. O ideal seria ignorar assuntos irrelevantes de avaliação, presenças, carga horária, etc., e se jogar nos estudos.

Avaliação

A nota final de cada aluno vai ser principalmente baseada em um ou mais dos: (i) provas orais com videochamada em modo privado e/ou aberto; (ii) sua participação (que inclue correação de trabalhos de outros alunos); (iii) suas resoluções de problem sets escritas e submetidas em TeX/LaTeX/ConTeXt; (iv) caderno escaneado com resoluções de homeworks; (v) resoluções em algum proof assistant, possivelmente publicadas em repositório git

Note que:

  • Os problem sets / homeworks podem envolver simular uma prova escrita em tempo real.
  • Cada aluno será responsável para manter organizado e bem escrito o seu caderno com todos os teoremas e exercícios que estudou durante a disciplina.

Presenças / Faltas

As presenças/faltas serão cadastradas baseadas na participação, na entrega dos trabalhos, e na entrega de caderno. Nenhuma dessas coisas é opcional, logo aluno que não as faz com a devida freqüência será reprovado por faltas.

FAQs

Dynamic content

Pontos

Pontos de participação

Problem Sets (PS)

Nenhum PS ainda.

Homework (HW)

Homeworks são atribuidos também: durante as aulas gravadas e no Zulip.

Obs.:

  • Estudar um assunto dum livro obviamente inclui resolver todos os exercícios e problemas.
  • «Até» é sempre inclusivo.
  • Homeworks marcados assim são opcionais; considero o resto obrigatório.
  • Depois de cada aula, um homework é 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;
    }
    
  • Exceto quando é explicitamente pedido, faça os homework sem consultar nenhum livro/texto/etc. auxiliar
  • Para os trabalhos em proof assistant vou postar mais informações logo.

08/06/2021

  • URGENTE: Nem tente resolver nada desta disciplina sem terminar esses HW relacionados aos prerequisitos:
    1. 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.
    2. Resolva sozinho o A da Prova 1.1 de FMC1/2019.2.
    3. Estude a resposta do A no seu gabarito.
    4. 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 e tente resolvê-las sozinho: 2020.1; 2019.1; 2018.2; 2018.1; 2017.2; 2017.1.
    3. Depois, leia bem todas as correções digitalizadas (que tem nos sites) para aproveitar dos comentários disponíveis e evitar erros comuns.

09/06/2021

  1. Estude os:
    • § Conceito, notação, igualdade
    • § Intensão, extensão
    • § Relações entre conjuntos e como defini-las
    • § Mais set-builder

11/06/2021

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

14/06/2021

  1. Capítulo 7: até o primeiro intervalo de problemas
  2. Π7.1,2,5,6,8
  3. § Tuplas

16/06/2021

  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!
  3. § Produto cartesiano
  4. § Implementação de tipo
  5. § n-tuplas
  6. § Seqüências
  7. § Intervalos na reta real
  8. Π7.8–10
  9. § Famílias indexadas
  10. § Conjuntos indexados vs famílias indexadas
  11. § Disjuntos dois-a-dois
  12. § Traduzindo de e para a linguagem de conjuntos
  13. § Produto cartesiano generalizado
  14. § Multisets
  15. Π7.11–15

17/06/2021

  1. Capítulo 7
  2. Resolva as provas 1.1 embaixo; use o #set-fun-rel; e depois de tentar cada uma, estude bem o seu gabarito!

18/06/2021

  1. § Conceito, notação, igualdade
  2. § Diagramas internos e externos
  3. § Como definir e como não definir funcões
  4. § Expressões com buracos

Histórico

Vamos acompanhar as aulas gravadas de FMC2, e discutir no Zulip.

07/06/2021: Intro, Demonstrações [video]

  • type errors
  • = vs ⇔
  • «def»
    • cuidado com os quantificadores
    • por que «praticamente»? qual a excessão?
  • intensão vs extensão
  • demonstrações: linha de código vs comentário
    • se..então.. vs como..logo..
    • «seja..» vs «existe..»
    • quantificador existencial: como atacar e como usar
    • variáveis ligadas vs livres
    • escolha de variável, variável fresca
    • escopos de variáveis
    • sombreamento (shadowing) de variáveis
    • indentação em cálculos
  • Três exercísios: mesma coisa ou não?
    • quantificador universal: como atacar
    • implicação: como atacar
    • conjunção: como usar e como atacar
  • vício de absurdo
  • a rendundância dos «… é verdade»
  • abuso de gerúndios, vírgula mágica, etc.
  • «para algum» e perigos de ambigüidade
    • não podemos trocar a ordem de quantificadores diferentes
  • definição e seu contexto
  • não misturem símbolos de fórmulas com texto, não são abreviações
  • setinhas mágicas
    • ⇒ vs «logo»
  • tipografia, caligrafia
    • matemática é case sensitive
    • afirmações secas

08/06/2021: Linguagens

  • (toda): [video]
    • Expressões aritméticas (ArEx)
    • Expressões aritméitcas com variáveis (AlgEx)
      • Usando recursão para matar os “…”
    • Números, numerais, dígitos
    • A linguagem da lógica proposicional (L₀)
    • Metalinguagem; metavariáveis
    • Usos e limitações da L₀
    • As linguagens de FOL
  • (00:25:40–01:11:58): [video]
    • Açúcar sintáctico, abreviações
    • Convenção: notação infixa
    • Existenciais e universais restritos
    • Existência e unicidade
    • A expressão x₁,…,xₙ
    • Metalinguagem enriquecida e as setinhas ⇐,⇒,⇔

09/06/2021: Conjuntos

  • (a partir de 00:41:53): [video]
    • 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
    • As relações binárias: ⊆, ⊇
    • Notação
    • Set comprehension (Set-builder notation)
      • Nunca use «|» como abreviação de «tal que» nem em texto nem nas fórmulas existenciais!
    • Intensão vs extensão
    • «um conjunto é determinado por seus membros»
    • os «def» em cima de = e de ⟺
    • Açucar sintáctico no set-builder
    • ⊊ vs ⊈ vs

11/06/2021: 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
  • Demonstrações de existência e 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

14/06/2021: 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

16/06/2021: 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

17/06/2021: Conjuntos

  • 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

18/06/2021

  • 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 BA)
    • (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

Futuro (fluido)

21/06/2021

23/06/2021

25/06/2021

28/06/2021

30/06/2021

02/07/2021

05/07/2021

07/07/2021

09/07/2021

12/07/2021

14/07/2021

16/07/2021

19/07/2021

21/07/2021

23/07/2021

26/07/2021

28/07/2021

30/07/2021

02/08/2021

04/08/2021

06/08/2021

09/08/2021

11/08/2021

13/08/2021

16/08/2021

18/08/2021

20/08/2021

23/08/2021

25/08/2021

27/08/2021

30/08/2021

01/09/2021

03/09/2021

06/09/2021

08/09/2021

10/09/2021

13/09/2021

15/09/2021

17/09/2021

Last update: Fri Jun 18 12:25:24 -03 2021