2022.1 FMC1, turma de Thanos

Horários de aula: 246N12 [18h45–20h25]
Contato:thanos@imd.ufrn.br
Playlists: FMC1 2019.2 (aulas gravadas)
Monitoria/TA: fmc.imd.ufrn.br (Começou!)
Turmas anteriores: ..

Info

Pré-requisitos

É pré-requisito desta disciplina ter aprendido o conteudo das disciplinas de matemática do primeiro semestre e (obviamente) do ensino médio também. Umas referências para esses conteudos são as seguintes:

  • Lang: Basic Mathematics (de uma ulhada 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)

Realidade. Depois de perceber que, sistematicamente, praticamente todos os alunos que foram aprovados na disciplina de Geometria Euclideana sequer escreveram nem uma linha de demonstração matemática, eu não tenho como considerar que os alunos da turma cumprem mesmo essa parte essencial¹ de pré-requisito.

¹ Imagine chegar em Polo Aquático I, sem ter aprendido mesmo as Natação I e II primeiro; ainda mais sem sequer ter entrado na agua na sua vida inteira!

(Obs.: aprenderpassar.)

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

(Obs.: estudarler.)

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

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

Conteúdo

A disciplina FMC1 será dividida em 3 módulos–unidades: Essa divisão é influenciada pelos módulos correspondentes à FMC2 baseados nos módulos correspondentes desta proposta.

IDMa: Elementos da teoria dos números inteiros

Axiomas sobre os inteiros (domínio de integridade bem ordenado). Demonstrações dos primeiros 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

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 boolianos, 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

Axiomas de corpo e suas primeiras consequências. Axiomas de corpo ordenado e suas primeiras 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. Ínfimo, supremo, e o axioma da completude. Sequências, limites, e 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

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

  • Mendelson (1973): Number Systems and the Foundations of Analysis (Cap. 2)
  • Avigad, Lewis, van Doorn (2017): Logic and Proof (Cap. 17)
  • Avigad, Leonardo de Moura, and Soonho Kong (2017): Theorem proving in Lean (Cap: 7,8)
  • Steffen, Rüthing, Huth (2018): Mathematical Foundations of Advanced Informatics, vol 1 (Cap: 4, 5)
  • Bird & Wadler (1986): Introduction to Functional Programming (Cap. 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)

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

Links

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 Haskell para algumas atividades.
  5. Git (leia o FAQ).
  6. Muito recomendado mas não necessário: um sistema Unix (veja o minicurso Unix 2019.2).
  7. Muito recomendado mas não necessário: (neo)vim e Emacs.
  8. Pouco de (La)TeX (veja o minicurso TeX 2018.2). Online editor/compilador: Overleaf.

A parte IRI será auxiliada usando a linguagem de programação funcional Haskell e o 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!)

A parte IDM será auxiliada pelo uso do proof assistant Lean.

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 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 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 créditos correspodentes.
  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 em cada homework. O único recurso 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 o 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. Checar e atender seu email cadastrado no SIGAA pelo menos uma vez por dia durante o semestre.
  3. 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.
  4. Estudar o conteúdo lecionado e tentar resolver todos os trabalhos atribuidos.
  5. Participar no Zulip diariamente.
  6. Participar nas aulas de exercícios de monitoria e utilizar seus horários de tirar dúvidas.

(Veja também os FAQs relevantes.)

Sobre plágio

  1. Plágio detectado implica que o aluno será reprovado 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 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 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 tem 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.

Obviamente, alunos que não aparecem nas aula não terão como ganhar pontos de participação—duh!—nem acesso nos 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

Dynamic content

Pontos de participação

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.

U1 (IDMa)

U2 (IRI)

U3 (IDMb)

  • Prova 3.1 (?)
  • Prova 3.2 (?)

Homework (HW)

Leia bem o FAQ sobre hw. Note também que:

  • Homeworks são atribuidos também durante as aulas e no Zulip.
  • Homeworks marcados assim são auxiliares; tente apenas se tu tem resolvido uma parte satisfatória dos outros.

2022-03-31

  1. Capítulo 1.

2022-04-04

  1. Capítulo 3.
  2. Complete o «Introduction World» do Natural Number Game.
  3. Para cada uma das proposições acima tente demonstrar escrevendo na linguagem de demonstrações que elaboramos nas aulas até agora. Evite os LEM e RAA quando possível.
    1. Proposições de dupla negaço:
      1. P ⇒ ¬¬P
      2. ¬¬P ⇒ P
    2. Comutatividade dos ∨,∧:
      1. (P ∨ Q) ⇒ (Q ∨ P)
      2. (P ∧ Q) ⇒ (Q ∧ P)
    3. Proposições de interdefinabilidade dos ⇒,∨:
      1. (P ⇒ Q) ⇒ (¬P ∨ Q)
      2. (P ⇒ Q) ⇐ (¬P ∨ Q)
      3. (P ∨ Q) ⇒ (¬P ⇒ Q)
      4. (P ∨ Q) ⇐ (¬P ⇒ Q)
    4. Proposições de contraposição:
      1. (P ⇒ Q) ⇒ (¬Q ⇒ ¬P)
      2. (¬Q ⇒ ¬P) ⇒ (P ⇒ Q)
    5. A irrefutabilidade do LEM:
      1. ¬¬(P∨¬P)
    6. A lei de Peirce e sua versão “fraca”:
      1. ((P ⇒ Q) ⇒ P) ⇒ P
      2. ((P ⇒ Q) ⇒ P) ⇒ ¬¬P
    7. Proposições de interdefinabilidade dos ∨,∧:
      1. P∨Q ⇒ ¬(¬P∧¬Q)
      2. P∨Q ⇐ ¬(¬P∧¬Q)
      3. P∧Q ⇒ ¬(¬P∨¬Q)
      4. P∧Q ⇐ ¬(¬P∨¬Q)
    8. As leis de De Morgan para ∨,∧:
      1. ¬(P∨Q) ⇒ (¬P ∧ ¬Q)
      2. ¬(P∨Q) ⇐ (¬P ∧ ¬Q)
      3. ¬(P∧Q) ⇒ (¬Q ∨ ¬P)
      4. ¬(P∧Q) ⇐ (¬Q ∨ ¬P)
    9. Proposições de distributividade dos ∨,∧:
      1. P∧(Q∨R) ⇒ (P∧Q)∨(P∧R)
      2. P∧(Q∨R) ⇐ (P∧Q)∨(P∧R)
      3. P∨(Q∧R) ⇒ (P∨Q)∧(P∨R)
      4. P∨(Q∧R) ⇐ (P∨Q)∧(P∨R)
    10. Currificação
      1. ((P∧Q)⇒R) ⇒ (P⇒(Q⇒R))
      2. ((P∧Q)⇒R) ⇐ (P⇒(Q⇒R))
    11. Reflexividade da ⇒:
      1. P ⇒ P
    12. Weakening and contraction:
      1. P ⇒ (P∨Q)
      2. Q ⇒ (P∨Q)
      3. (P∧Q) ⇒ P
      4. (P∧Q) ⇒ Q
      5. P ⇒ (P∧P)
      6. (P∨P) ⇒ P
    13. As leis de De Morgan para ∃,∀:
      1. ¬(∀x)[φ(x)] ⇒ (∃x)[¬φ(x)]
      2. ¬(∀x)[φ(x)] ⇐ (∃x)[¬φ(x)]
      3. ¬(∃x)[φ(x)] ⇒ (∀x)[¬φ(x)]
      4. ¬(∃x)[φ(x)] ⇐ (∀x)[¬φ(x)]
    14. Proposições de interdefinabilidade dos ∃,∀:
      1. (∃x)[φ(x)] ⇒ ¬(∀x)[¬φ(x)]
      2. (∃x)[φ(x)] ⇐ ¬(∀x)[¬φ(x)]
      3. (∀x)[φ(x)] ⇒ ¬(∃x)[¬φ(x)]
      4. (∀x)[φ(x)] ⇐ ¬(∃x)[¬φ(x)]
    15. Proposições de distributividade de quantificadores:
      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)]

2022-04-10

  • (i) instale o Lean no teu computador; (ii) configure teu editor (sendo ou um editor que presta (emacs ou neovim), ou o VS Code) para ativar o modo Lean; (iii) numa pasta no teu computador use o comando leanpkg new fmclean; (iv) baixe o arquivo logic.lean que tem os enunciados prontos, e o coloca na pasta fmclean/src; (v) substitua todos os sorry, do arquivo com código que compila para demonstrar tudo. Dúvidas nos #proofassistants e #tech, obviamente!

2022-04-11

  • Demonstre os teoremas seguintes sobre os inteiros a partir dos axiomas (procure esclarecimentos no Zulip). Tome cuidado com umas das quantificações que deixei implicitas.
    1. unicidade da $(+)$-identidade (0)
    2. unicidade da $(⋅)$-identidade (1)
    3. leis de $(+)$-cancelamento
    4. unicidade dos $(+)$-inversos (opostos)
    5. 0 é um $(⋅)$-anulador: $0⋅x = 0 = x⋅0$
    6. $-(-x) = x$
    7. $(-1)x = -x$
    8. $(-x)y = -(xy) = x(-y)$
    9. $(-x)(-y) = xy$
    10. leis de $(⋅)$-cancelamento
    11. (|) é reflexiva: (∀a)[a | a]
    12. (|) é transitiva: (∀a,b,c)[a | b & b | c ⇒ a | c]
    13. qualquer inteiro divide o 0
    14. tem inteiros que o 0 divide?
    15. os $1$ e $-1$ dividem qualquer inteiro?
    16. d | a & d | b ⇒ d | ax + by
    17. a | b & b | a ⇒ a = b ?

2022-04-19

  1. Estude bem o gabarito da Prova 1.1

2022-04-19

  1. Demonstre, ainda com os 8 primeiros axiomas (4 aditivos, 3 multiplicativos, e a distributividade) a equivalência entre:
    • NZD: (∀a,b)[ ab = 0 ⇒ a = 0 ou b = 0 ]
    • LC: (∀a,b,d)[ ca = cb ⇒ c = 0 ou a = b ]
  2. Demonstre os teoremas seguintes (cuidado: nuns enunciados tem quantificadores implícitos!):
    1. Os quadrados de membros não nulos são positivos.
    2. 1 é positivo.
    3. $<$ é transitiva: para quaisquer $a,b,c$, se $a < b$ e $b < c$, então $a < c$.
    4. Adicionar em inegualdade: $a < b \implies a + c < b + c$.
    5. Multiplicar em inegualdade: se $c > 0$, então $a < b$ implica $ac < bc$.
    6. Lei da tricotomia: para quaisquer $a,b$, exatamente uma das seguinte é válida: $a < b$; $a = b$; $a > b$.
    7. $|ab| = |a||b|$.
    8. $|a+b| \leq |a| + |b|$.
    9. $a - x < a - y$ sse $x > y$.
    10. $a < 0 \implies (ax > ay \iff x < y)$.
    11. Se $c > 0$, então $ac < bc$ implica $a < b$.
    12. Se $x + x + x + x = 0$, então $x = 0$.
    13. Se $a < b$, então $a^3 < b^3$.
    14. Se $c \geq 0$, então $a \geq b$ implica $ac \geq bc$.
    15. $||a|-|b|| \leq |a - b|$.
    16. Se $|x| = |y|$, então $x = y$ ou $x = -y$.
  3. Demonstre que a equação $x^2 + 1 = 0$ não possui resolução no incógnito $x$.
  4. Demonstre que, adicionando o predicado ou relação sobre ordem e seus axiomas, o axioma NZD/LC é dispensável (ou seja, demonstre um deles como teorema).
  5. Demonstre que as duas abordagens são equivalentes:
    1. $(\mathbb Z ; 0, 1, +, -, \cdot, <)$ com ${<} : \mathsf{Int} \times \mathsf{Int} \to \mathsf{Prop}$ e os axiomas:
      • os 4 aditivos, os 3 multiplicativos, distributividade, não zerodivisores
      • tricotomia da ($\lt$)
      • transitividade da ($\lt$)
      • $a < b \implies a + c < b + c$
      • se $0 < c$, então $a < b \implies ac < bc$
    2. $(\mathbb Z ; 0, 1, +, -, \cdot, P)$ com $P : \mathsf{Int} \to \mathsf{Prop}$ e os axiomas:
      • os 4 aditivos, os 3 multiplicativos, distributividade, não zerodivisores
      • $P$ é (+)-fechado
      • $P$ é (·)-fechado
      • para todo $a$, exatamente uma das seguinte é válida: $a$ é positivo; $a=0$; $-a$ é positivo.

2022-04-26

  1. Usando o princípio da boa ordem (qualquer conjunto não vazio de inteiros positivos possui mínimo) demonstre: não existe inteiro $c$ tal que $0 < c < 1$.
  2. O «não vazio» acima é redundante?

2022-05-02

  1. Capítulo «Os inteiros»: tudo até o primeiro intervalo de problemas.

2022-05-10

  1. Demonstre como teorema o princípio da indução com 2 bases.
  2. Demonstre como teorema o princípio da indução forte.
  3. Escreva a demonstração completa, com todos os detalhes, do Lema da Divisão de Euclides.
  4. Como definirias a idéia de “tijolinho atómico” para uma operação binária?
  5. Demonstre que todo inteiro positivo pode ser escrito como produtório de primos em maneira “única”. Por quê o única tá dentro de aspas?

2022-05-12

  1. Demonstre o Teorema Fundamental da Aritmética
  2. Demonstre o Teorema dos Sistemas Posicionais (expansão em base $b$)
  3. Tente demonstrar equivalências entre as afirmações seguintes para um p≠0:
    • (i) Irreducible(p) (⇐≝⇒ (∀a,b)[ p = ab ⇒ a unit ou b unit ])
    • (ii) Primo(p) (⇐≝⇒ divs(p) = { 1, -1, p, -p })
    • (iii) Prime(p) (⇐≝⇒ (∀a,b)[ p | ab ⇒ a unit ou b unit ])

2022-05-21

  1. Capítulo «Os inteiros»: até o 3o intervalo de problemas.
  2. Jogue o NNG. Tente completar o mais rápido possivel. Veja o FAQ relevante também.

2022-05-28

  1. Capítulo «Os naturais; recursão; indução»: até o 1o intervalo de problemas.
  2. (i) instale a Haskell no teu computador; (ii) Completa o getting started e o first steps do ghcup; (iii) configure teu editor (sendo ou um editor que presta (emacs ou neovim), ou o VS Code) para integrar com Haskell. Dúvidas nos #programming e #tech, obviamente!
  3. Brinque com Elm, especialmente se tu tens interesse em web-devel ou se tu tá sofrendo escrevendo JavaScript (mesmo se não percebes tal sofrimento).

2022-05-31

  1. Olhando para as funçoẽs binárias e famosas que definimos até agora (adição, multiplicação, exponenciação), perceba que tem um “padrão”. Use isso para definir a “próxima” operação. Denote por ⇈.
  2. Defina a função Pd : Nat → Nat de “predecessor”, onde consideramos que o predecessor de zero é o próprio zero mesmo.
  3. Defina a função ∸ : Nat → Nat → Nat que comporta como subtração, mas caso que o resultado era pra ser negativo, retorna O mesmo.
  4. Defina as funções:
    • fact : Nat → Nat
    • fib  : Nat → Nat
    • div  : Nat × Nat → Nat × Nat
    • quot : Nat × Nat → Nat
    • rem  : Nat × Nat → Nat
    • mod  : Nat → Nat → Nat que dou de presente: mod m n = rem (n,m)
    • gcd  : Nat × Nat → Nat
    • lcm  : Nat × Nat → Nat
    • comb : Nat → Nat → Nat
    • perm : Nat → Nat → Nat
  5. Como definirias um tipo de dados Bool para os booleanos?

2022-06-03

  1. Até a §«Demonstrando propriedades de naturais sem indução».

2022-06-04

  1. Até a §«Indução».

2022-06-09

  1. §«Ordem nos naturais»
  2. Demonstre que a (≤) : Nat → Nat → Prop é:
    • reflexiva
    • transitiva
    • antissimétirca
    • total
  3. Demonstre que todo Nat é par ou ímpar.
  4. Demonstre a corretude das:
    • leq      : Nat → Bool
    • isMul₃   : Nat → Bool
  5. Defina as:
    • length   : ListNat → Nat
    • elem     : Nat → ListNat → Bool
    • sum      : ListNat → Nat
    • product  : ListNat → Nat
    • (++)     : ListNat → ListNat → ListNat
    • reverse  : ListNat → ListNat
    • min      : Nat → Nat → Nat
    • max      : Nat → Nat → Nat
    • allEven  : ListNat → Bool
    • anyEven  : ListNat → Bool
    • allOdd   : ListNat → Bool
    • anyOdd   : ListNat → Bool

2022-06-11

  1. Defina as:
    • ifthenelse  : Bool → α → α → α
    • isZero      : Nat → Bool
    • allZero     : ListNat → Bool
    • anyZero     : ListNat → Bool
    • addNat      : Nat → ListNat → ListNat
    • multNat     : Nat → ListNat → ListNat
    • expNat      : Nat → ListNat → ListNat
    • enumFromTo  : Nat → Nat → ListNat
    • enumTo      : Nat → ListNat
    • take        : Nat → ListNat → ListNat
    • drop        : Nat → ListNat → ListNat
    • elemIndices : Nat → ListNat → ListNat
    • pwAdd       : ListNat → ListNat → ListNat
    • pwMult      : ListNat → ListNat → ListNat
    • isSorted    : ListNat → Bool
    • filterEven  : ListNat → ListNat
    • filterOdd   : ListNat → ListNat
    • minimum     : ListNat ⇀ Nat
    • maximum     : ListNat ⇀ Nat
    • isPrefixOf  : ListNat → ListNat → Bool
    • mix         : ListNat → ListNat → ListNat
    • intersperse : Nat → ListNat → ListNat
  2. Demonstre os teoremas (escolhe algo interessante para botar nos ??)
    1. (∀xs,ys:ListNat)        [ length (xs ++ ys) = ?? ]
    2. (∀xs,ys:ListNat)        [ reverse (xs ++ ys) = ?? ]
    3. (∀xs,ys:ListNat)        [ sum (xs ++ ys) = ?? ]
    4. (∀xs,ys:ListNat)        [ product (xs ++ ys) = ?? ]
    5. (∀n:Nat)(∀xs,ys:ListNat)[ addNat n (xs ++ ys) = ?? ]
    6. (∀ℓ:ListNat)            [ reverse (reverse ℓ) = ?? ]
    7. (∀ℓ:ListNat)            [ length (reverse ℓ) = ?? ]
    8. (∀ℓ:ListNat)            [ length (filterEven ℓ ++ filterOdd ℓ) = ?? ]
    9. (∀ℓ:ListNat)            [ reverse (filterEven ℓ) = ?? ]
    10. (∀n:Nat)(∀ℓ:ListNat)    [ length (addNat n ℓ) = ?? ]
    11. (∀n:Nat)(∀ℓ:ListNat)    [ sum (addNat n ℓ) = ?? ]
    12. (∀n:Nat)(∀ℓ:ListNat)    [ sum (multNat n ℓ) = ?? ]
    13. (∀n:Nat)(∀ℓ:ListNat)    [ product (multNat n ℓ) = ?? ]
    14. (∀n:Nat)(∀ℓ:ListNat)    [ product (expNat n ℓ) = ?? ]
    15. (∀n:Nat)(∀ℓ:ListNat)    [ isSorted (addNat n ℓ) = ?? ]
    16. (∀ℓ:ListNat)            [ isEven (product ℓ) = anyEven ℓ ]
    17. (∀ℓ:ListNat)            [ isEven (sum ℓ) = isEven (length (filterOdd ℓ)) ]
    18. (∀ℓ:ListNat)            [ isZero (sum ℓ) = ?? ]
    19. (∀ℓ:ListNat)            [ isZero (product ℓ) = ?? ]
    20. Associatividade da (++)
    21. [] é uma (++)-identidade
  3. Pense em mais propriedades, enuncie, e demonstre!
  4. Defina a (<) : Nat → Nat → Prop e sua internalização, e demonstre a sua corretude.

2022-06-14

  1. Defina as:
    • and        : List Bool → Bool
    • or         : List Bool → Bool
    • replicate  : Nat → α → List α
    • map        : (α → β) → List α → List β
    • concat     : List (List α) → List α
    • a generalização all das: allZero, allEven, allOdd
    • a generalização any das: anyZero, anyEven, anyOdd
    • a generalização filter das: filterEven, filterOdd
    • a generalização pointwise das: pwAdd, pwMult
    • a generalização fold das: sum, product, and, or, concat
  2. Demonstre:
    1. (∀n,m:Nat)(∀ℓ:List Nat)[ addNat (n + m) ℓ = ?? ]
    2. (∀n,m:Nat)(∀ℓ:List Nat)[ multNat (n · m) ℓ = ?? ]

2022-06-19

  1. Defina tipos para cada um estilo de árvore que a gente viu nas aulas
  2. Defina funções treemap, que seriam para seus tipos de arvores o que a map é para as listas.
  3. Defina as:
    • takeWhile   : (α → Bool) → List α → List α
    • dropWhile   : (α → Bool) → List α → List α
    • head        : List α → Maybe α
    • tail        : List α → Maybe (List α)
    • init        : List α → Maybe (List α)
    • last        : List α → Maybe α
    • pick        : Nat → List α → Maybe α
    • findFirst   : α → List α → Maybe Nat
    • find        : α → List α → List Nat

2022-06-23

  1. Defina tipos para representar expressões de aritmética sem variáveis, expressões de aritmética com variáveis, e expressões de lógica proposicional
  2. Defina as:
    • splitAt       : Nat → List α → (List α × List a)
    • flip          : Tree α → Tree α 
    • findFirstTree : α → Tree α → Maybe (List Nat)
    • findTree      : α → Tree α → List (List Nat)
    • sumTree       : Tree Nat → Nat
  3. Demonstre:
    1. (∀t:Tree α)                [ height t ≤ length (flatten t) ]
    2. (∀t:Tree α)                [ flip (flip t) = ?? ]
    3. (∀t:Tree α)                [ flatten (flip t) = ?? ]
    4. (∀t:Tree α)                [ height (flip t) = ?? ]
    5. (∀t:Tree α)(∀f:α→β)        [ height (fmap f t) = ?? ]
    6. (∀t:Tree α)(∀f:α→β)        [ height (fmap f t) = ?? ]
    7. (∀t:Tree α)(∀f:α→β)        [ fmap f (flip t) = ?? ]
    8. (∀ℓ:List α)                [ fmap id ℓ = ?? ]
    9. (∀ℓ:List α)(∀f:α→β)(∀g:β→γ)[ fmap g (fmap f ℓ) = ?? ]
    10. (∀t:Tree α)(∀f:α→β)(∀g:β→γ)[ fmap g (fmap f t) = ?? ]

2022-06-25

  1. Demonstre:
    1. (∀ℓ:List α)(∀n:Nat)(∀m:Nat)[ drop n (drop m ℓ) = ?? ]
    2. (∀ℓ:List α)(∀n:Nat)(∀m:Nat)[ take n (take m ℓ) = ?? ]
    3. (∀ℓ:List α)(∀n:Nat)(∀m:Nat)[ take n (drop m ℓ) = ?? ]
    4. (∀ℓ:List α)(∀n:Nat)(∀m:Nat)[ drop n (take m ℓ) = ?? ]
    5. (∀f:α→β)(∀p:β→Bool)        [ filter p ∘ map f = map f ∘ filter (p ∘ f) ]
    6. (∀f:α→β)(∀g:β→γ)           [ map g ∘ map f = map (g∘f) ]

2022-06-26

  1. Qual seria uma melhor tipágem para a pw : (α → α → α) → List α → List α → List α?
  2. Defina as:
    • zip       : List α → List β → List (α × β)
    • unzip     : List (α × β) → (List α × List β)

Histórico

2022-03-28: Aula 01: Overview; tipos

  • tipos e type errors
  • proposiões vs objetos
  • sintaxe vs semântica

2022-03-30: Aula 02: Definições

  • comandos vs proposições
  • se..então.. vs como..logo..
  • variáveis ligadas vs livres
  • escopos de variáveis
  • sombreamento (shadowing) de variáveis
  • abuso de gerúndios, vírgula mágica, etc.
  • definição e seu contexto
  • açúcar sintáctico, abreviações
  • convenção: notação infixa
  • os conectivos ⇐,⇒,⇔

2022-04-01: Aula 03: Tipos; definições; linguagem de demonstrações

  • = vs ⇔
  • «def»
  • intensão vs extensão
  • o resto dos conectivos para nossa linguagem de demonstrações
  • escolha boa de variável, variável fresca
  • bairros de variáveis

2022-04-04: Aula 04: Tipos; linguagem de demonstrações

2022-04-06: Aula 05: Os inteiros (1)

  • Proposição mais forte vs mais fraca que outra
  • Necessário e suficiente, se e somente se
  • P ⇒ ¬¬P
  • ¬¬P ⇒ P
  • RAA (Reductio ad Absurdum)
  • LEM (Law of Excluded Middle)
  • Tentativa de demonstrar: para todo a inteiro, a divide a
  • Axiomas sobre os inteiros $(\mathbb Z;+,\cdot,-,0,1)$.
  • Operações primitivas vs definidas: a operação binária da subtração

2022-04-08: Os inteiros (2)

  • As primeiras conseqüências dos axiomas

2022-04-11: Aula cancelada

2022-04-13: Aula cancelada

2022-04-15: Feriado

2022-04-18: Prova 1.1

2022-04-20: Os inteiros (3)

  • Mini-sermão sobre a prova 1.1
  • Operações e relações primitivas vs. definidas
  • Axiomas sobre ordem: duas maneiras de axiomatizar
  • Conjunto fechado sob operação
  • A nos naturais é definível
  • Como tratar um subconjunto como predicado unário
  • O módulo (absolute value) |_| : Int → Int

2022-04-22: "Feriado"

2022-04-25: Os inteiros (4)

  • Recap
  • Como demonstrar a indemonstrabilidade de proposições
  • 1 é positivo
  • A indemonstrabilidade do 0 ≠ 1

2022-04-27: Os inteiros (5)

  • Dica sobre como enxergar alvos
  • Exemplo: (∀a)[(-1)a = -a]
  • A utilidade de lemmas sobre unicidade de resolução de equações num incógnito
  • Exemplo: (∀a)[0a = a]
  • Transitividade da $\lt$
  • Como escrever cálculos corretamente numa demonstração

2022-04-29: Os inteiros (6)

  • Mais sobre a independência duma proposição: indemonstrabilidade e irrefutabilidade
  • Umas propriedades do valor absoluto
  • Princípio da boa ordem ($\mathbb Z_{>0}$ é bem ordenado)
  • Como usar o PBO na prática
  • Não existe inteiro estritamente entre 0 e 1

2022-05-02: Os inteiros (7)

  • Como escrever definições
  • Duas maneiras que uma definição pode ser errada
  • Quando precisamos demonstrar algo para justificar uma definição ou uma notação
  • Existência e unicidade
  • Duas maneiras diferentes para conseguir unicidade
  • o mínimo dum conjunto, quando existe é único
  • uso de lemmas numa demonstração

2022-05-04: Os inteiros (8)

  • como definir «ser fechado sob uma operação n-ária (para n=1,2)
  • a notação set-builder: como ler e escrever, e como não ler e como não escrever
  • um pleno «tal que» é capaz de destruir uma frase e torná-la pior-que-errada
  • O que significa «_ ∈ { 3x | x ∈ ℤ }»
  • A diferença intensional entre os extensionalmente iguais conjuntos: {x ∈ A | x ∈ B} e {x ∈ B | x ∈ A}
  • o 3ℤ é fechado sob adição e subtração
  • como generalizar para o mℤ
  • Lema de divisão de Euclides: enunciado
  • a justificativa «pela escolha de»
  • Números, numerais, dígitos
  • O logaritmo como tamanho de númerais melhor que o length deles como strings

2022-05-06: Os inteiros (8)

  • Princípio da indução para os inteiros: se $S$ é (+1)-fechado e $1 \in S$, então $\mathbb Z_{>0} \subseteq S$
  • Outras versões de PBO e de Indução e como obtê-las “hackeando” as originais

2022-05-09: Os inteiros (9)

  • Regras de inferência; como escrever, o que significa, como ler de cima pra baixo e de baixo pra cima
  • Indução com mais que uma base
  • Indução forte (“course-of-values”)
  • Lema de Divisão de Euclides e sua demonstração usando o PBO
  • Quebrando os inteiros em tiholinhos atômicos usando como cimento: (i) adição; (ii) multiplicação
  • Enunciado do Teorema Fundamental de Aritmética (fatorização única)

2022-05-11: Os inteiros (10)

  • Definição de invertível
  • Definição de irredutível
  • Definição de primo
  • Explicação intuitiva sobre como sistemas posicionais funcionam
  • Esboço de demonstração do teorema dos sistemas posicionais (expansão em base $b$): qualquer inteiro $b>1$ serve como base para um sistema posicional de numerais para inteiros.
  • Esboço do Teorema Fundamental de Aritmética

2022-05-13: Os inteiros (11)

  • generalização da palavra “maior” para outras ordens
  • diagrama Hasse para os $\mathbb{Z}_{\geq 0}$
  • mdc: definição
  • O conjunto {ax + by | x ∈ ℤ, y ∈ ℤ} é fechado sob adição e subtração
  • Existência de mdc

2022-05-16: Os inteiros (11)

  • os coeficientes Bézout
  • mdc e mmc e demonstrações das suas propriedades
  • Algoritmo de Euclides: corretude e terminação
  • Algoritmo estendido de Euclides

2022-05-18: Os inteiros (12)

  • Algo que parece LEM, mas não é
  • Lema de Euclides e sua generalização
  • Dum lemma para uma ideia: n² (im)par ⇔ n (im)par

2022-05-20: Os inteiros (13)

  • Congruência módulo um inteiro e demonstrações das suas propriedades
  • Aritmética modular e propriedades do $\mathbb Z / m\mathbb Z$
  • Teorema de Euclides sobre infinidade de primos e sua demonstração construtiva
  • (·)-inversos módulo um inteiro m

2022-05-23: Os inteiros (14)

  • Invertibilidade módulo $m$
  • Unicidade de inverso módulo $m$ e o que significa
  • Uns casos extremos: módulo 1, módulo 0
  • Algumas conjecturas da teoria dos números

2022-05-25: Os inteiros (15)

  • Mais conjecturas
  • Revisão da invertibilidade e unicidade de inversos módulo um inteiro
  • Densidade de primos e gaps

2022-05-27: Prova 1.3; Recursão, Indução (1): Nat

  • 4 maneiras de definir um tipo de dados recursivamente
  • O tipo Nat
  • Naturais vs Nats
  • Linguagem vs Metalinguagem; Variáveis vs Metavariáveis
  • Como mostrar que algo é um Nat
  • Regras de inferência e lida de cima para baixo e de baixo para cima
  • Casamento de padrão com expressão
  • Definição da adição para os Nats

2022-05-30: Recursão, Indução (2): Nat

  • associatividade sintáctica vs associatividade
  • currificação
  • notação: prefixa, postfixa, infixa, mixfixa
  • valores canônicos
  • construtor vs função
  • o presente da recursão
  • definições: multiplicação, exponenciação, double
  • o uso de lemmas: m-idR, e-idR
  • umas demonstrações simples
  • ∀: como usar
  • ∀: como atacar
  • Recursão vs tijolo
  • redexes

2022-06-01: Recursão, Indução (3): Nat

  • AST (Abstract Syntax Tree)
  • Parser e Lexer
  • qual resultado incompleto é melhor?
  • estratégia de evaluação vs precedência de operador
  • notação de aplicação de função por espaço: f x
  • sua associatividade sintáctica à esquerda: f x y z ≡ ((f x) y) z
  • aplicação parcial
  • parity = mod 2
  • casamento de padrões: o que é um padrão mesmo?
  • escolhendo o padrão na direita duma equação para substituir na direção (←)
  • Θ. Associatividade da (+)
  • A disjunção escondida em cada Nat.
  • ∃: como usar
  • ∨: como usar
  • tem como continuar a demonstração?
  • escolhendo variáveis com «linhas»: x’, x’’, etc.
  • igualdade entre Nats
  • o problema que temos demonstrando esse teorema

2022-06-03: Recursão, Indução (4): Nat, Bool, Weekday

  • Como definir o tipo de dados Bool e suas operações
  • Como representar predicados sobre os naturais (Nat → Prop, Nat→Nat→Prop, etc.) como se fossem funções que retornam Bool.
  • Mais tipos de dados simples: Weekday
  • A regra de inferência Ind-Nat-φ. (Onde φ : Nat → Prop.)
  • Demonstração por indução
  • O presente de recursão vs o presente da indução
  • Definição por recursão vs Demonstração por indução
  • A associatividade da (+): duas demonstrações por indução diferentes.

Para quem perdeu esta aula, a última parte dela é parecida com esta aula gravada de FMC1-2019.2

2022-06-06: Recursão, Indução (5): Nat, Bool

  • Análise das duas demonstrações da (+)-associatividade
  • Como usar o underscore (_) como «variável sem nome» num padrão.
  • ev, od : Nat → Bool
  • Recursão mútua
  • Relações vs funções-com-codomínio-Bool
  • (≤) : Nat → Nat → Prop
  • leq : Nat → Nat → Bool
  • A corretude da leq

2022-06-08: Prova 2.1; Recursão, Indução (6): Nat, Bool, Unit, ListNat

  • isMul₃ : Nat → Bool vs isMul : Nat → Nat → Bool
  • isMul₃ : Nat → Bool vs mod₃ : Nat → Nat
  • O tipo Unit com seu único habitánte/construtor: ⋆ : Unit
  • Uma primeira idéia para o tipo Int, e uns problemas
  • Como implementar listas: ListNat
  • Os construtores Empty (ou Nil) e Cons

2022-06-10: Recursão, Indução (7): Nat, Bool, Unit, ListNat

  • Podemos implementar o Prop como um data type?
  • A idéia de internalizar uma noção
  • Tipos dependentes: comparação e teaser
  • O problema com os head e tail
  • Runtime Error vs. Honesty Error vs. Type error
  • o tipo de error
  • o tipo de id
  • polimorfismo de tipos
  • Idéia ruim: usar um valor arbitrário para o head []
  • Gambiarra 1: safeHead : ListNat → ListNat
  • Gambiarra 2: safeHead : ListNat → Bool × Nat
  • Gambiarra 3: defaultHead : Nat → ListNat → Nat
  • Construtores vs Destrutores
  • Definições de sum : ListNat → Nat e product : ListNat → Nat
  • Um benefício da estratégia preguiçosa
  • Como escolher o valor certo para o sum [] e o product []
  • Defina a addNat : Nat → ListNat → ListNat

2022-06-13: Recursão, Indução (8): Nat, Bool, Unit, List α

  • O conceito de «respeitar uma propriedade».
  • Do $\mathrm{Ind}^{\mathtt{Nat}}_{\varphi}$ para o $\mathrm{Ind}^{\mathtt{ListNat}}_{\varphi}$.
  • Do $\mathrm{Ind}^{\mathtt{ListNat}}_{\varphi}$ para o $\mathrm{Ind}^{\mathtt{α}}_{\varphi}$.
  • Θ: (∀xs,ys:ListNat)[ length (xs ++ ys) = length xs + length ys ]
  • Do tipo ListNat para o tipo List Nat
  • List : Type → Type
  • Construtores de tipos (type constructors) vs Construtores de valores (data constructors)
  • type variables vs data variables
  • polimorfismo: de lengthNat : List Nat → Nat para length : List α → Nat
  • abstração de ordem superior: de addNat : Nat → List Nat → List Nat para mapNat : (Nat → Nat) → List Nat → List Nat
  • abstração de ordem superior: de mapNat : (Nat → Nat) → List Nat → List Nat para map : (α → β) → List α → List β

2022-06-15: Recursão, Indução (9): Nat, Bool, Unit, List α

  • mais uma análise entre a definição dum tipo de dados inductivo e o princípio da indução associado a ele
  • “inventando” propriedades dos nossos programas para demonstrar, e as demonstrando
  • Maybe
  • as versões não-gambiarrosas de head e tail
  • vários tipos de árvores freqentemente usados em computação

2022-06-22: Recursão, Indução (9): Nat, Bool, Unit, List α, Tree α

  • NonEmptyList α
  • O principio da indução para um tipo de arvores
  • height
  • flatten
  • map, mapTree
  • Functors, fmap, deriving ( Functor )
  • takeWhileTree
  • Either α β
  • O que usar para representar erros em vez de gambiarras

2022-04-22: "Feriado"

2022-06-24: Recursão, Indução (10)

  • Sintaxe vs semântica
  • ArEx, ArExV
  • Fórmulas de Lógica Proposicional
  • Numerais binários
  • Composição (∘)
  • fmap g (fmap f xs) = fmap (g ∘ f) xs

2022-06-25: Reposição de 3 aulas

  • Preguiça e infinidade
  • enumFrom, infty, ones
  • primes
  • pw (zipWith)
  • fibs
  • fold, fold1
  • sepBy
  • let-in expressions
  • Ordenação: Ord, sorted, quicksort, mergesort
  • igualdade entre funções
  • Recursão aninhada
  • Ackermann

Futuro (fluido)


2022-06-27: Prova 2.3; IDMb

2022-06-29

2022-07-01

2022-07-04

2022-07-06

2022-07-08

2022-07-11

2022-07-13

2022-07-15

2022-07-16: Reposição de 3 aulas

  • Teorema pequeno de Fermat
  • Função totiente de Euler
  • Teorema de Euler
  • Aplicações em criptografia

2022-07-18

2022-07-20

2022-07-22

2022-07-25

2022-07-27

2022-07-29

Last update: Mon Jun 27 13:18:40 -03 2022