2024.2 FMC1, turma de Thanos

Info

Pré-requisitos

• É necessário que os alunos matriculados têm tempo e vontade para estudar, fazer os trabalhos atribuídos, etc.

(Obs.: estudar ≠ ler.)

Veja minhas dicas para estudantes, que inclui pré-requisitos para esta disciplina.

Alunos que não aprenderam o conteúdo das disciplinas de matemática do primeiro semestre e (obviamente) do ensino médio podem consultar as referências seguintes:

(Obs.: aprender ≠ passar.)

• Lang: Basic Mathematics (de uma olhada nesta playlist no YouTube que tem um curto videozinho para cada secção deste livro)
• Lima et al: A Matemática do Ensino Médio, vol I (para esta disciplina os mais relevantes pré-requisitos são os Cap. 1–4)

Conteúdo

A disciplina FMC1 será dividida em 3 módulos–unidades. Podem considerar cada tal módulo como um componente curricular independente (e sem pré-requisitos entre si). Essa divisão é influenciada pelos módulos correspondentes à FMC1 baseados nos módulos correspondentes desta proposta.

IDMa: Elementos da teoria dos números inteiros

(Lecionado 4h/semana, durante a primeira metade do semestre.)

Axiomas sobre os inteiros (domínio de integridade bem ordenado). Demonstrações de teoremas pelos axiomas, sobre as operações e as relações de ordem nos inteiros. A relação de divisibilidade e a verificação de suas principais propriedades. Teorema de Euclides sobre infinidade de primos e sua demonstração construtiva. Lema de divisão de Euclides. Números, numerais, dígitos: demonstração que qualquer inteiro $b > 1$, serve como base para um sistema posicional de numerais para inteiros. Lema de Euclides e sua generalização. Teorema Fundamental da Aritmética. mdc e mmc e demonstrações das suas propriedades Algoritmo de Euclides: corretude e terminação Algoritmo estendido de Euclides Demonstração do teorema Fundamental de Aritmética Congruência módulo um inteiro e demonstrações das suas propriedades Aritmética modular e propriedades do ℤ/mℤ. Algumas conjecturas da teoria dos números: o teorema pequeno de Fermat; a função totiente de Euler; o teorema de Euler.

IRI: Introdução à Recursão e Indução

(Lecionado 2h/semana, durante o semestre inteiro.)

Os naturais e o tipo Nat; seus construtores (zero, sucessor) e sua teoria: implementação recursiva das suas principais operações, e verificação indutiva das suas principais propriedades. O tipo dos booleanos, Bool. Ordens sobre os naturais: especificação e verificação de suas propriedades. Outras funções e relações, e suas propriedades. Indução como princípio e técnica de demonstração em matemática. A unicidade dos naturais (a menos de isomorfismo). List Nat e List α: tipos de dados de listas: implementação recursiva e verificação indutiva de suas principais propriedades. Outros tipos de dados recursivos: tipos de árvores; tipos de expressões aritméticas; tipos de fórmulas; termos de cálculo-λ. Numerais binários, definição de semântica e seu uso para verificação de corretude.

IDMb: Elementos da teoria dos números reais

(Lecionado 4h/semana, durante a segunda metade do semestre.)

Axiomas de corpo e suas consequências. Axiomas de corpo ordenado e suas consequências. Representação geométrica. Algumas noções métricas e topológicas da reta real. Subconjuntos notáveis do ℝ: N, Z, Q. Racionais e irracionais. Conjuntos cotados, cota superior, cota inferior. Ínfimo, supremo. Seqüências e seus limites. O axioma da completude. Séries.

Objetivos de aprendizagem

IRI: Introdução à Recursão e Indução

Neste módulo estudamos como definir tipos de dados, funções, e relações recursivamente, e como demonstrar propriedades sobre tais coleções de dados por indução.

Prática com o uso da linguagem matemática e das principais técnicas de demonstração e refutação. Prática com a escrita de definições por recursão e demonstrações por indução. Recursão e indução estrutural sobre tipos de dados recursivos. Apreciação de coleções potencialmente infinitas do ponto de vista implementacional, recursivo, e verificação matemática de suas propriedades de interesse. Casamento de padrões e seu uso em definições, demonstrações, e cálculos. Recursão mútua, indução aninhada. Ganhar familiaridade com inferência de tipos e evitar erros de tipagem. Notação e nomenclatura matemática e computacional. Apreciar a diferença e a conexão entre sintaxe e semântica.

IDM: Introdução à Demonstração Matemática

Nestes módulos usamos elementos da teoria dos números inteiros (IDMa) e da teoria axiomática dos números reais (IDMb) para introduzir o aluno ao pensamento matemático e o processo de definir conceitos, enunciar e demonstrar teoremas. Aproveitamos o desenvolvimento do conteúdo concreto para chegar até os seguintes conceitos fundamentais:

• congruência e aritmética modular (IDMa)
• ínfimo, supremo, sequência, limite (IDMb)

Familiarizar com a linguagem usada em definições e demonstrações matemáticas: aprender ler e escrever (usar e interpretar corretamente a linguagem matemática, sua nomenclatura e notação). Apreciar a diferença entre intensional e extensional (sobre igualdades e equivalências). Uso de (meta)variáveis em matemática; ocorrência de variável ligada vs livre; α-conversão (renomeamento); substituição de variável por termos; linguagem vs metalinguagem. Introduzir o lado computacional de uma demonstração, como sequência de comandos que alteram o estado de Dados/Alvos. Entender dois lados de matemática: intuitivo e formal. Propriedades da igualdade e seu uso no raciocínio equacional. Aprender como usar e escrever cálculos dentro de uma demonstração. Apreciar a demonstração como justificativa da veracidade de proposições matemáticas (incluindo de proposições como $p\to p$, leis de distributividade, de De Morgan, frequentemente chamadas «leis» de lógica). Aprender para cada um dos ¬,⇒,∨,∧,∃,∀: como introduzi-lo e como eliminá-lo no texto de uma demonstração. Apreciar a lógica construtiva e os usos dos princípios da lógica clássica (terceiro excluído, redução ao absurdo, dupla negação, contrapositivo); apreciar a diferença entre redução ao absurdo e demonstração direta de negação. Desenvolver definições e teorias matemáticas a partir de noções primitivas e axiomas. Familiarizar com definições e demonstrações que envolvem conjuntos, sequências, funções, e relações. Ter um primeiro contato com conjuntos estruturados e estruturas algébricas e as propriedades das suas operações. Entender como e por quê os sistemas posicionais de numerais funcionam.

Bibliografia e referências

Conhece o libgen?

Principal

• Eu: Matemática fundacional para computação [fmcbook] (Capítulos 1–6)

IRI: Introdução a Recursão e Indução

• Bird & Wadler (1986): Introduction to Functional Programming (Cap. 1,2,3,5,9)
• Mendelson (1973): Number Systems and the Foundations of Analysis (Cap. 2)
• Christiansen (2023) Functional programming in Lean (Cap: 7,8)
• Steffen, Rüthing, Huth (2018): Mathematical Foundations of Advanced Informatics, vol 1 (Cap: 4, 5)
• Hutton (2016): Programming in Haskell, 2nd ed.
• Pierce et al.: Software Foundations, Vol 1 (Cap: Basics, Induction, Lists)
• Fejer, Simovici (1991): Mathematical Foundations of Computer Science, Vol 1 (Cap. 4)
• Avigad, Leonardo de Moura, and Soonho Kong (2017): Theorem proving in Lean (Cap: 7,8)
• Avigad, Lewis, van Doorn (2017): Logic and Proof (Cap. 17)

IDMa: Introdução à teoria dos números inteiros

• Birkhoff & Mac Lane (1977): A Survey of Modern Algebra, 4th ed. (Cap: 1)
• Mendelson (1973): Number Systems and the Foundations of Analysis (Cap: 3)
• Avigad, Lewis, van Doorn (2017): Logic and Proof (Cap. 19)
• Tao (2016): Analysis I, 3rd ed. (Cap: B1)
• Dasgupta, Papadimitriou, Vazirani: Algorithms [DPV]

IDMb: Introdução à teoria dos números reais

• Abbott (2015): Understanding Analysis, 2nd ed. (Cap: 1, 2, 4)
• Mendelson (1973): Number Systems and the Foundations of Analysis (Cap: 5)
• Rudin (1976): Principles of Mathematical Analysis, 3rd ed. (Cap: 1, 3)
• Tao (2016): Analysis I, 3rd ed. (Cap: 6,7,9,B2)

Comum & Auxiliar

• Avigad, de Moura, Kong (2017): Theorem proving in Lean
• Abbott (2015): Understanding Analysis, 2nd ed. (Cap: 3)
• Daepp, Gorkin (2011): Reading, Writing, and Proving, 2nd ed.
• Devlin (2012): Introduction to Mathematical Thinking (Cap: 4)
• Spivak (2008): Calculus, 4th ed. (Cap: 1)

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

Dicas

Veja minha página de dicas para estudantes.

Links

• NNG
• Lean
• Haskell
• Minicurso TeX 2018.2
• Detexify
• Overleaf online (La)TeX editor/compilador
• Minicurso Unix 2019.2
• The Missing Semester of your CS Education

Tecnologias & ferramentas

Obs.: As tecnologías/ferramentas seguintes podem mudar durante a disciplina—exceto a primeira. (Instalem e/ou criem uma conta para usar onde necessário.)

1. PAPEL (um caderno para dedicar à disciplina) e LAPIS/CANETA.
2. Zulip (leia o FAQ).
3. O proof assistant Lean para algumas atividades (leia o FAQ).
4. A linguagem de programação funcional Lean para algumas atividades.
5. A linguagem de programação funcional Haskell para algumas atividades.
6. Git (leia o FAQ).
7. Muito recomendado mas não necessário: um sistema Unix (veja o minicurso Unix 2019.2).
8. Muito recomendado mas não necessário: (neo)vim e Emacs (alternativa popular: VS Code).
9. Pouco de (La)TeX (veja o minicurso TeX 2018.2). Online editor/compilador: Overleaf.

O módulo IRI será auxiliado pelo uso da linguagem de programação funcional Lean e Haskell (e talvez Agda), e pelo proof assistant Lean. Usando uma linguagem de programação funcional é imediato implementar todas as suas definições para rodá-las no computador. Usando um proof assistant, formalizamos tanto as definições recursivas, quanto as demonstrações indutivas usando a mesma linguagem. (Mas o foco continua sendo o papel; não o computador!)

O módulo IDMa será auxiliado pelo uso do proof assistant Lean.

O módulo IDMb não será auxiliado por nenhum proof assistant. Ficará só no papel mesmo. (Dependendo do progresso no início do semestre, isso pode mudar.)

Regras

1. Nunca escreva ou diga 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 e 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 ou resposta dada poderá ser questionado em forma de prova oral, em modo privado ou aberto. Se um aluno não consegue explicar o que ele mesmo escreveu numa resolução, será considerado plágio (veja abaixo).
3. Participando, nunca dê uma resposta que tu não pensou sozinho, exceto dando os devidos créditos correspodentes.
4. Não tente “forçar a barra” perguntando ou respondendo coisas aleatórias com objetivo 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 em cada homework. O único recurso automaticamente aceitável para procurar ajuda é no nosso Zulip (especificamente seus canáis públicos—não DM) e a monitoria.
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!)

Uns deveres dos alunos

1. Visitar este site e o Zulip da disciplina pelo menos uma vez por dia durante o semestre. (Qualquer coisa postada no site ou no Zulip da disciplina será considerada como conhecida por todos os alunos da turma.)
2. Estudar o conteúdo lecionado e tentar resolver todos os trabalhos atribuidos.
3. Participar no Zulip diariamente, compartilhando tuas resoluções para receber feedback, e checando as resoluções de outros colegas para dar feedback.
4. Checar e atender seu email cadastrado no SIGAA pelo menos uma vez por dia durante o semestre.
5. Participar nas aulas! Obs.: tendo uma dúvida durante a aula, levante a mão para solicitar “a fala” e assim que a receber, pergunte! Não espere o fim da aula para discutir tua dúvida em “modo particular”! A maioria das vezes eu vou negar isso e pedir ao aluno iniciar a discussão no Zulip ou na próxima aula.
6. Participar nas aulas de exercícios de monitoria e utilizar seus horários de atendimento para tirar dúvidas.

(Veja também os FAQs relevantes.)

Sobre plágio

1. Plágio detectado implica que o aluno será reprovado na disciplina imediatamente por nota e por faltas.
2. Entregar tuas resoluções para um aluno copiar é proibido do mesmo jeito, e também não ajuda mesmo ninguém.

Cadernos vs. celulares

Não faz sentido aparecer na aula sem caderno. E não faz sentido aparecer na aula com celular ligado; bote no modo avião antes de entrar na sala. As aulas são interativas e se não pretende participar e concentrar nesses 100 minutos, sugiro ficar fora e escolher uma outra maneira de passar teu tempo. Não é necessário (e obviamente nem suficiente) aparecer nas minhas aulas para passar.

Avaliação e faltas

Disclaimer. Eu suponho que os alunos desta turma escolheram se matricular por interesse em aprender seu conteúdo. O ideal seria ignorar assuntos irrelevantes de avaliação, presenças, carga horária, etc., e se jogar nos estudos e nas brigas (nas aulas, no Zulip, e na monitoria).

Avaliação

A nota final de cada aluno vai ser principalmente baseada em um ou mais dos: (i) provas escritas; (ii) sua participação; (iii) trabalhos atribuidos; (iv) hw resolvidos (veja o FAQ relevante).

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 e faltas

A presença pela regulação da UFRN é obrigatória. Os alunos que não gostam/querem/podem aparecer nas minhas aulas ainda têm chances de ganhar até nota máxima e aprovar na disciplina. Ou seja: alunos que escolhem não participar ou aparecer nas aulas, e mesmo assim aparecem nas provas escritas e conseguem nota final de aprovação vão ter sua porcentagem de faltas ajustada para não reprovar por faltas. Esclarecimento: alunos que não conseguem nota final de aprovação não terão sua porcentagem de presença ajustada de jeito nenhum e por nenhum motivo.

Obviamente, alunos que não aparecem nas aulas não terão como ganhar pontos de participação em aula—duh!—nem pontos de possíveis provas-surpresas.

As presenças/faltas serão cadastradas usando o sistema Plickers (veja o FAQ relevante).

Atrasados

Definição (atrasado). Seja $a$ aluno desta turma. Dizemos que $a$ é atrasado sse $a$ não está já sentado na sua mesa, com seu caderno já aberto, seu celular já desligado e na mochila, no momento que a aula começa.

Tentem estar presentes na sala da aula ANTES do horário do seu começo, e fiquem até o fim da aula.

Caso que alguém chega atrasado: não faz sentido bater na porta da sala de aula; não faz sentido cumprimentar nem o professor (não é mostra educação cumprimentar nesse caso—pelo contrário!) nem os amigos/colegas da aula. Entrando numa sala onde a aula já começou, tentem fazer sua entrada o menos possível notada por os participantes pois atrapalha a concentração de todos.

FAQs

• Zulip
• Install
• Lean
• Plickers
• Homework (hw)
• Git
• Vídeo
• NNG

Dynamic content

Provas

Provas surpresa. Note que em qualquer aula pode ter prova surpresa, cujos pontos são considerados «pontos extra», assim sendo possível tirar nota máxima (100), mesmo perdendo todas as provas surpresas.

Provas não-surpresa. Tais provas serão avisadas com curtíssima antecedência (de pelo menos 16h). A melhor maneira de lidar com isso é tratar todo dia de aula como possível dia de prova.

U1 (IDMa)

• Prova IDMa.1 / 28pts (2024-10-18) { censored , uncensored , answers , correções }
• Prova IDMa.2 / 72pts (?)

U2 (IRI)

• Prova IRI.1 / ?
• Prova IRI.2 / ?

U3 (IDMb)

• Prova IDMb.1 / ?