Horários de aula: | 246N12 [18h45–20h25] |
Sala: | A102 |
Contato: | thanos@imd.ufrn.br |
Playlists: | FMC1 2022.2: ( Intro | IDMa | IDMb | IRI ) |
Monitoria/TA: | fmc.imd.ufrn.br |
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 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)
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.: aprender ≠ passar.)
Além disso, é necessário que os alunos matriculados têm tempo e vontade para estudar, fazer os trabalhos atribuídos, etc.
(Obs.: estudar ≠ ler.)
Antes de começar é bom dar uma lida nos:
- Comments on style de Munkres.
- 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. 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
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
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
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 à 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)
- 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)
- 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
- James Munkres: Comments on style
- Jean-Pierre Serre: How to write mathematics badly
- Don Knuth: Mathematical writing
- Paul Halmos: How to write mathematics
- Por que tantos livros? Qual é o melhor? Vale a pena ler esse excerto do livro Linear Algebra de Jänich.
Links
- NNG (Offline? Tente esse mirror também.)
- Lean & Lean web editor
- Haskell
- Minicurso TeX 2018.2
- Detexify
- Minicurso Unix 2019.2
- The Missing Semester of your CS Education
- Overleaf online (La)TeX editor/compilador
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.)
- PAPEL (um caderno para dedicar à disciplina) e LAPIS/CANETA.
- Zulip (leia o FAQ).
- O proof assistant Lean para algumas atividades (leia o FAQ).
- A linguagem de programação funcional Haskell para algumas atividades.
- Git (leia o FAQ).
- Muito recomendado mas não necessário: um sistema Unix (veja o minicurso Unix 2019.2).
- Muito recomendado mas não necessário: (neo)vim e Emacs.
- 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 IDMa será auxiliada pelo uso do proof assistant Lean.
A parte IDMb não será auxiliada por nenhum proof assistant. Ficará só no papel mesmo.
Regras
- 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.
- 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).
- Participando, nunca dê uma resposta que tu não pensou sozinho, exceto dando os créditos correspodentes.
- 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.
- 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.
- 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
- 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.)
- Estudar o conteúdo lecionado e tentar resolver todos os trabalhos atribuidos.
- Participar no Zulip diariamente, compartilhando tuas resoluções para receber feedback, e checando as resoluções de outros colegas para dar feedback.
- Checar e atender seu email cadastrado no SIGAA pelo menos uma vez por dia durante o semestre.
- 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.
- 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
- Plágio detectado implica que o aluno será reprovado imediatamente por nota e por faltas.
- 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.
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 de jeito nenhum e por nenhum motivo.
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)
- Prova 1.0 (2022-08-30): Tutorial World (NNG)
- Prova 1.1 (2022-08-31) { censored , uncensored , answers , correções }
- Prova 1.2 (2022-08-29–2022-09-13): logic.lean
- Prova 1.3 (2022-09-28) { censored , uncensored , answers , correções }
- Prova 1.4 (2022-10-26) { censored , uncensored , answers , correções }
U2 (IRI)
- Prova 2.1 (2022-11-07) { censored , uncensored , answers , correções }
- Prova 2.2 (2022-10-08–2022-11-01): NNG
- Prova 2.3 (2022-12-07) { censored , uncensored , answers , correções , quadro }
U3 (IDMb)
- Prova 3.1 (2022-12-07) { censored , uncensored , answers , correções , quadro }
- Prova 3.2 (2022-12-16) { censored , uncensored , answers , correções }
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-08-23 (Intro)
- Capítulo 1.
2022-08-25 (Intro)
- Complete o «Tutorial World» do Natural Number Game. Veja o FAQ relevante também.
- Capítulo 3.
2022-08-25 (Intro)
- Demonstre o teoremas seguintes escrevendo demonstrações “low-level”, mantendo também os DADOS/ALVO atualizados com cada linha da sua demonstração:
- Θ. Todo inteiro divide ele mesmo.
- Θ. Para quaisquer inteiros a,b, se a divide b e b divide 0, então a divide 0 ou 1 divide b.
- Θ. Seja a inteiro. Para quaisquer inteiros x,y, se a | x e a | y, então a | x + y.
- Θ. Seja a inteiro. Para todo inteiro x, se a | x, então para todo inteiro u, a | ux.
- Θ. Para quaisquer inteiros a,x,y,r,s, se a | x e a | y, então a | rx + ys.
- Para cada um dos ¬,⇒,&,ou,⇔,∀,∃,= pense como que pode ser usado (sendo nos DADOS) ou atacado (sendo no ALVO). Escreva os comandos correspondentes e para cada um deles, esclareça: qual é o efeito no tabuleiro da demonstração (tanto na parte dos DADOS quanto no ALVO), como e quando é que tal comando pode ser executado.
2022-08-29 (Intro)
- Para cada uma das proposições acima tente demonstrar escrevendo na linguagem de demonstrações que elaboramos nas aulas até agora. Se colar em algum sem conseguir fechar, mostre teu progresso no zulip e peça ajuda; enquanto isso, continua para a próxima!
- Proposições de dupla negaço:
- P ⇒ ¬¬P
- ¬¬P ⇒ P
- Comutatividade dos ∨,∧:
- (P ∨ Q) ⇒ (Q ∨ P)
- (P ∧ Q) ⇒ (Q ∧ P)
- Proposições de interdefinabilidade dos ⇒,∨:
- (P ⇒ Q) ⇒ (¬P ∨ Q)
- (P ⇒ Q) ⇐ (¬P ∨ Q)
- (P ∨ Q) ⇒ (¬P ⇒ Q)
- (P ∨ Q) ⇐ (¬P ⇒ Q)
- Proposições de contraposição:
- (P ⇒ Q) ⇒ (¬Q ⇒ ¬P)
- (¬Q ⇒ ¬P) ⇒ (P ⇒ Q)
- A irrefutabilidade do LEM:
- ¬¬(P∨¬P)
- A lei de Peirce e sua versão “fraca”:
- ((P ⇒ Q) ⇒ P) ⇒ P
- ((P ⇒ Q) ⇒ P) ⇒ ¬¬P
- Proposições de interdefinabilidade dos ∨,∧:
- P∨Q ⇒ ¬(¬P∧¬Q)
- P∨Q ⇐ ¬(¬P∧¬Q)
- P∧Q ⇒ ¬(¬P∨¬Q)
- P∧Q ⇐ ¬(¬P∨¬Q)
- As leis de De Morgan para ∨,∧:
- ¬(P∨Q) ⇒ (¬P ∧ ¬Q)
- ¬(P∨Q) ⇐ (¬P ∧ ¬Q)
- ¬(P∧Q) ⇒ (¬Q ∨ ¬P)
- ¬(P∧Q) ⇐ (¬Q ∨ ¬P)
- Proposições de distributividade dos ∨,∧:
- 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)
- Currificação
- ((P∧Q)⇒R) ⇒ (P⇒(Q⇒R))
- ((P∧Q)⇒R) ⇐ (P⇒(Q⇒R))
- Reflexividade da ⇒:
- P ⇒ P
- Weakening and contraction:
- P ⇒ (P∨Q)
- Q ⇒ (P∨Q)
- (P∧Q) ⇒ P
- (P∧Q) ⇒ Q
- P ⇒ (P∧P)
- (P∨P) ⇒ P
- As leis de De Morgan para ∃,∀:
- ¬(∀x)[φ(x)] ⇒ (∃x)[¬φ(x)]
- ¬(∀x)[φ(x)] ⇐ (∃x)[¬φ(x)]
- ¬(∃x)[φ(x)] ⇒ (∀x)[¬φ(x)]
- ¬(∃x)[φ(x)] ⇐ (∀x)[¬φ(x)]
- Proposições de interdefinabilidade dos ∃,∀:
- (∃x)[φ(x)] ⇒ ¬(∀x)[¬φ(x)]
- (∃x)[φ(x)] ⇐ ¬(∀x)[¬φ(x)]
- (∀x)[φ(x)] ⇒ ¬(∃x)[¬φ(x)]
- (∀x)[φ(x)] ⇐ ¬(∃x)[¬φ(x)]
- Proposições de distributividade de quantificadores:
- (∃x)[φ(x) ∧ ψ(x)] ⇒ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
- (∃x)[φ(x) ∧ ψ(x)] ⇐ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
- (∃x)[φ(x) ∨ ψ(x)] ⇒ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
- (∃x)[φ(x) ∨ ψ(x)] ⇐ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
- (∀x)[φ(x) ∧ ψ(x)] ⇒ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
- (∀x)[φ(x) ∧ ψ(x)] ⇐ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
- (∀x)[φ(x) ∨ ψ(x)] ⇒ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]
- (∀x)[φ(x) ∨ ψ(x)] ⇐ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]
- Proposições de dupla negaço:
- Demonstre os teoreams em cima no Lean (veja o FAQ!): baixe o arquivo logic.lean que tem os enunciados prontos, e o coloca na pasta
fmclean/src
; substitua todos ossorry,
do arquivo com código que compila para demonstrar tudo. Dúvidas nos#proofassistants
e#tech
, obviamente!
2022-09-02 (IDMa)
- Cap «Os inteiros», «§. Primeiros passos»
- 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.
- unicidade da $(+)$-identidade (0)
- unicidade da $(⋅)$-identidade (1)
- leis de $(+)$-cancelamento
- unicidade dos $(+)$-inversos (opostos)
- 0 é um $(⋅)$-anulador: $0⋅x = 0 = x⋅0$
- $-(-x) = x$
- $(-1)x = -x$
- $(-x)y = -(xy) = x(-y)$
- $(-x)(-y) = xy$
- leis de $(⋅)$-cancelamento
(|)
é reflexiva:(∀a)[a | a]
(|)
é transitiva:(∀a,b,c)[a | b & b | c ⇒ a | c]
- qualquer inteiro divide o 0
- tem inteiros que o 0 divide?
- os $1$ e $-1$ dividem qualquer inteiro?
d | a & d | b ⇒ d | ax + by
a | b & b | a ⇒ a = b
?
2022-09-06 (IDMa)
- Cap «Os inteiros», até «§. Conjuntos fechados sobre operações»
- Demonstre, ainda com os 8 primeiros axiomas (4 aditivos, 3 multiplicativos, e a distributividade) a equivalência entre:
- (Z-NZD):
(∀a,b)[ ab = 0 ⇒ a = 0 ou b = 0 ]
- (Z-LC):
(∀a,b,c)[ ca = cb ⇒ c = 0 ou a = b ]
- (Z-NZD):
2022-09-09 (IDMa)
- Demonstre que as duas abordagens vistas na aula são equivalentes:
- (ℤ;0,1,+,-,·,<) + (ZO-Trans) + (ZO-A) + (ZO-M) + (ZO-Tri)
- (ℤ;0,1,+,-,·,Pos) + (ZP-ACl) + (ZP-MCl) + (ZP-Tri)
- Cap «Os inteiros», até «§. Ordem e positividade»
2022-09-12 (IDMa)
- Considere os inteiros das peimeiras aulas, até a especificação (2/5).
- Demonstre que o
0≠1
não é demonstrável a partir desses axiomas.
- Demonstre que o
- Considere o (A; ♡, κ) com a especificação seguinte, e demonstre que não tem como demonstrar a Comutatividade de (♡), nem como refutá-la.
- (♡) : A × A → A
- κ : A
- (Ass) : (∀a,b,c)[ (a ♡ b) ♡ c = a ♡ (b ♡ c) ]
- (IdR) : (∀a)[ a ♡ κ = a ]
2022-09-15 (IDMa)
- Até o «§. Valor absoluto»
- Π4.1, Π4.2, Π4.3, Π4.4
2022-09-16 (IDMa)
- 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$.
- O «não vazio» acima é redundante?
- Demonstre que um conjunto vazio é subconjunto de qualquer conjunto.
- Demonstre ou refute: «o Ø é bem-ordenado».
- Até o primeiro intervalo de problemas.
- Demonstre ou refute: «qualquer conjunto de inteiros X finito é bem ordenado».
- Escreva os comandos que temos sobre ataques e usos dos conectivos (∧),(∨),(⇒) como regras de inferência.
- Demonstre como teorema o princípio da indução.
- Demonstre como corolário o princípio da indução com 2 bases.
2022-09-23 (IDMa)
- Resolva em condições de prova as provas seguintes:
- Resolva em condições tranqüilas as mesmas provas.
2022-09-26 (IDMa)
- Escreva sozinho a definição de m.d.c.
- Troque o que precisa trocar para virar a definição de mínimo.
- Troque o que precisa trocar para virar a definição de máximo.
- Troque o que precisa trocar para virar a definição de m.m.c.
- Dados inteiros a,b, demonstre a existência dum m.d.c. deles, e mostre que ele pode ser escrito como combinação linear dos a,b.
- Demonstre as propriedades básicas dum m.d.c., que denotamos aqui simplesmente por (_,_), exceto uma, que é refutável (e logo refute e depois obviamente tente a ajustar para virar demonstrável, e demonstre–phew!):
- (a,b) = (a,-b) = (-a,b) = (-a,-b)
- (a,a) = ?
- (a,0) = ?
- (a,1) = ?
- (a,b) = (b,a)
- ((a,b),c) = ?
- (a,b) = (a, a + b)
- (a,b) = (a, a - b)
- (ca,cb) = c(a,b)
- (uv,a) = (u,a)(v,a)
- (a,b) = (b, rem(a,b))
- Demonstre: Invertible(x) ⇔ Unit(x)
- Demonstre: Irreducible(x) ⇔ Prime(x)
- Demonstre ou refute: apra quaisquer primos distintos p,q, pq | n² ⇒ pq | n.
- 🚀 Bora viajar legal!
- Num universo de conjuntos (por exemplo no
Set(Int)
) considere a mesma definição de m.d.c., mas essa vez usando como guia a ordem de (⊆). Qual conceito definiu? O que acontece se virar as direções? (⊇). - Tendo P, Q : Prop, escrevemos
P ⊢ Q
para a (meta)proposição «Dado aP
, podemos demonstrar aQ
.». No universo de proposições, mostre que (⊢) é uma pré-ordem. Qual seria o “m.d.c.” de duas props, e qual o “m.m.c” delas?
- Num universo de conjuntos (por exemplo no
2022-09-28 (IDMa)
- Troque o (Z-PBO) pelo princípio da indução (Z-Ind). Demonstre o (Z-PBO).
2022-09-29 (IDMa)
- 💻 Na aula foi óbvio que ninguém merece fazer contas na mão, mesmo utilizando um algoritmo eficiente. Mas somos programadores—right?—e logo: programe na tua linguagem favorita uma função que dados dois inteiros a, b, retorna seu m.d.c. d, e também coeficientes Bézout x,y tais que d = ax + by. Dica: caso que tua linguagem favorita não seja a Haskell, troque e tente novamente.
- L: a ≥ b > 0 ⇒ r < a/2. (Aqui a/2 é o quot(a,2).)
- Θ: Para todo n ≥ 1, e quaisquer inteiros a > b > 0, se o algoritmo de Euclide precisa n passos (divisões) para terminar, então a ≥ fib(n+2) e b ≥ fib(n+1), onde fib(i) é o i-ésimo número Fibonacci.
2022-09-30 (IDMa)
- Demonstre o que faltou para a demonstração do Lemma de Bézout: p irredutível & p ∤ a ⇒ (p,a) = 1.
- Como podemos generalizar o Lemma de Bézout sobre p’s não-necessariamente-irredutíveis?
- Demonstre o Teorema Fundamental da Aritmética
- Dado as «formas canônicas» de inteiros a e b, descreva os m.d.c. e m.m.c. deles
- Demonstre que dado um inteiro x, se não há primos divisores de 2 até ⌊√x⌋, então x é primo
2022-10-05 (IDMa)
- Seja n > 0. Ache n inteiros consecutivos tais que nenhum deles é primo.
- Seja m inteiro. Demonstre que (≡ₘ) é uma relação de equivalência: (i) reflexiva; (ii) transitiva; (iii) simétrica
- Seja m inteiro. Demonstre que (≡ₘ) é uma congruência para a estrutura (ℤ; 0, 1, +, ·, -), ou seja, que é compatível com essa estrutura, ou seja, que:
- a ≡ₘ a’ & b ≡ₘ b’ ⇒ a + b ≡ₘ a’ + b’
- a ≡ₘ a’ & b ≡ₘ b’ ⇒ a · b ≡ₘ a’ · b’
- a ≡ₘ a’ ⇒ -a ≡ₘ -a’
- Seja m inteiro. Demonstre ou refute, se puder:
- a ≡ₘ b ⇒ a + x ≡ₘ b + x
- a ≡ₘ b ⇒ a · x ≡ₘ b · x
- a ≡ₘ b ⇒ -a ≡ₘ -b
- a ≡ₘ b ⇒ aˣ ≡ₘ bˣ
- O «planeta 1» faz sentido? Como é?
- O «planeta 0» faz sentido? Como é?
- Demonstre o que consegues da equivalência das duas sugestões do que deveria significar o a ≡ₘ b.
2022-10-07 (IDMa)
- Sejam $a$ inteiro e $p$ primo tais que $(a,p) = 1$. Seja $R_p = \{0,1, \dotsc, p-1\}$. Demonstre que $aR_p$ possui exatamente um representante de cada classe (time).
- $a$ invertível módulo $m$ sse (a,m) = 1.
- Unicidade de inversos módulo $m$.
- Mostre que a (≡ₘ) não é compatível com a exponenciação.
- Elabore e justifique critério de divisibilidade para os 2,3,4,5,9,11
2022-10-08 (IRI)
- Jogue o NNG. Tente completar o mais rápido possivel; possivelmente sua entregá será a Prova 2.2. Veja o FAQ relevante também.
2022-10-14 (IDMa)
- Encontre um inverso de 18, módulo 125.
- Encontre inteiro x tal que $6^{1032} \equiv x \pmod {11}$.
- Dados inteiros $a,b,m$ quantas multiplicações tu precisa fazer para achar um inteiro $x$ tal que $a^b \equiv x \pmod m$?
- Querendo escrever um guia para alunos (ou maquinas!) saber como resolver congruências e sistemas de congruências, o que tu escreveria sobre:
- $\phantom a x \equiv b \pmod m$
- $ax \equiv 1 \pmod m$
- $ax \equiv b \pmod m$
- Um sistema de $n$ congruências $x \equiv b_i \pmod {m_i}$. (Dica: resolva primeiro para o caso $n = 2$.)
- Demonstre que existe uma infinidade de primos «da forma 4n+3».
- Depois de resolver o problema anterior, explique por que sua resolução não é adaptável para primos «da forma 4n+1».
- Demonstre: p primo ⇔ (p-1)! ≡ -1 (mod p).
2022-10-14 (IRI)
- Calcule os:
double (double (S O))
double ((S O) + (S (S O)))
- Defina multiplicação e exponenciação.
- Olhando para as funçoẽs binárias e famosas que temos 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 ⇈.
- Defina a função
Pd : Nat → Nat
de “predecessor”, onde consideramos que o predecessor de zero é o próprio zero mesmo: AVISO: a maioria das vezes que um aluno de 2022.1 usou aPd
em outras definições, estava errando - Defina a função
∸ : Nat → Nat → Nat
que comporta como subtração, mas caso que o resultado era pra ser negativo, retorna O mesmo. - Defina as funções:
fact : Nat → Nat
fib : Nat → Nat
dist : Nat → Nat → Nat
min : Nat → Nat → Nat
max : Nat → Nat → Nat
div : Nat × Nat → Nat × Nat
quot : Nat × Nat → Nat
rem : Nat × Nat → Nat
gcd : Nat × Nat → Nat
lcm : Nat × Nat → Nat
comb : Nat → Nat → Nat
perm : Nat → Nat → Nat
2022-10-17 (IDMa)
- Demonstre o «sonho do calouro»: Para qualquer primo $p$, $(x + y)^p \equiv x^p + y^p \pmod p$.
- Demonstre por indução o teorema binomial: $(x + y)^n = \sum_{i=0}^n {n \choose i} x^iy^{n-i}$, onde ${n \choose r} = C(n,r)$.
- Demonstre que $(\forall 0 < i < p)[p \mid C(p,i)]$.
- Consiga como corolario desses teoremas o «Teorema pequeno de Fermat»: $a^p \equiv a \pmod p$.
- AINDA?!: Sejam $a$ inteiro e $p$ primo tais que $(a,p) = 1$. Seja $R_p = \{0,1, \dotsc, p-1\}$. Demonstre que $aR_p$ possui exatamente um representante de cada classe (time). [foi postado 10 dias atrás].
- Ache a pior entrada para euclides e justifique tua resposta.
- Termine a implementação recursiva do $C({-},{-})$.
- Demonstre que $C(n,r) = \dfrac {n!}{r! (n-r)!}$.
- Sejam n,r inteiros. Demonstre: $r! (n-r)! \mid n!$.
- As duas métodos que descrevemos sobre a resolução de $ax \equiv 1 \pmod m$ e de $ax \equiv b \pmod m$ em algum ponto mandaram checar se $a,m$ são coprimos. Caso que não são, podemos concluir que tais congruências não possuem resolução?
- Infira o “princípio” multiplicativo de contagem a partir do princípio aditivo.
2022-10-17 (IRI)
- (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! - Implementa o
Nat
num módulo Haskell, junto com todas as funções que definimos até agora, incluindo os hw. Comece teu arquivo assim:module Nat where data Nat = O | S Nat deriving ( Eq , Show )
2022-10-20 (IRI)
- Resolva tudo na §«Demonstrando propriedades de naturais com indução»
- Asserte propriedades sobre teus programas do hw do dia 2022-10-14, e demonstre cada uma delas!
- Enuncie e demonstre que quaisquer fibonaccis consecutivos são coprimos.
2022-10-22 (IDMa)
- Seja $R_m = \{r_1,\dotsc,r_{\varphi(m)}\}$ é um sistema reduzido de resíduos módulo $m$. Demonstre:
- Se (a,m)=1, então aRₘ também é um s.r.r. módulo m.
- $\sum_{r\in R_m} r \equiv 0 \pmod m$.
- Rₘ é (·)-“fechado módulo m”.
- (∀r ∈ Rₘ)(∀x ∈ ℤ)(∃u ∈ ℤ)[ x ≡ₘ ru ]
- (qm + r, m) = (r,m)
- (a,nm) = 1 ⇔ (a,m) = 1 & (a,n) = 1
- φ(p) = p-1
- φ(pᵏ) = pᵏ - pᵏ⁻¹
- Calcule um dos φ(2), φ(3), φ(4), …, φ(13)
- φ é multiplicativa, ou seja: (m,n)=1 ⇒ φ(mn) = φ(m) φ(n). Dica: escreva todos os números de 1 até mn numa tabela de m × n.
- Calcule de novo, essa vez todos os φ(2), φ(3), φ(4), …, φ(13). (Não se engane: fatorização demora!)
- φ(n) é par para qualquer n > 2.
- Calcule o valor do somatório $\sum_{i=0}^k \varphi(p^i)$.
- $a^{\varphi(m)} \mathrel{\equiv_m} 1 \iff (a,m) = 1$. Dica: φ e sistemas reduzidos de resíduos são intimamente relacionados, né?
- Mostre que o Fermatinho é um corolário da proposição anterior!
- Seja $p$ primo e defina a função $V_p : \mathsf{Int} \to \mathsf{Int}$ pelas:
$V_p~a = \max\{ i\;\mid\; p^i \mid a\}$ para $a \neq 0$ e para $a = 0$, decida tu!
Demonstre:- V (a+b) ≥ min (V a) (V b)
- V (ab) = V a + V b
- V (a,b) = min (V a) (V b)
- V [a,b] = max (V a) (V b)
- Defina $\Vert a \Vert_p = p^{- (V_p\,a)}$. Demonstre: $$ \begin{gathered} \Vert ab \Vert = \Vert a \Vert \, \Vert b \Vert \\ \Vert a + b\Vert \leq \max \{\Vert a \Vert, \Vert b \Vert \} \leq \Vert a \Vert + \Vert b \Vert \\ \prod_{p~\text{primo}} \Vert a \Vert_p = \frac 1 {|a|} \\ \end{gathered} $$
2022-10-27 (IDMa)
- Demonstre, depois do esboço/dica da aula: φ é multiplicativa.
- Demonstramos a propriedade principal de descryptografar, mas nela a gente supôs que $m,N$ são coprimos. Temos mesmo como garantir isso? Se sim, por quê? Se não, o que acontece se por sorte (i.e., azar) a mensagem $m$ que queremos mandar não é coprima com o $N$?
- Considere que temos acesso numa função $h : D \to H$ que dada um valor de informação $d \in D$, retorna o seu hash $h(d) \in H$. Suponha que ela, mesmo sendo conhecida por todos, tem a propriedade seguinte: dado um $s \in H$, é difícil achar um valor $d_s \in D$ tal que $h(d_s) = s$. Pense numa maneira de usar o sistema RSA que a gente discutiu na aula para conseguir assinaturas digitais: queremos uma maneira de ter certeza que a mensagem que recebemos supostamente escritar por Alice, foi escrita por Alice mesmo. Dica 1. Temos que $e$ é um inverso de $d$, e logo $d$ é um inverso de $e$ também. Observem que $(m^e)^d=(m^d)^e$. Dica 2. A chave privada deve ser usada para trancar(cryptografar) algo, que qualquer pessoa pode destrancar(descryptografar) mas apenas quem está em posse da chave privada poderia ter sido o trancador.
2022-10-28 (IRI)
- Defina e demonstre a corretude das funções:
leq : Nat → Bool
ev : Nat → Bool
od : Nat → Bool
isMul₃ : Nat → Bool
divides : Nat → Nat → Bool
congmod : ?
isZero : Nat → Bool
- Demonstre que a
(≤) : Nat → Nat → Prop
é: reflexiva; transitiva; antissimétrica; total - Demonstre que todo Nat é par ou ímpar.
- Defina os operadores booleanos.
- Como definarias uma função
if_then_else_ : Bool → Nat → Nat → Nat
? - Demonstre a corretude das funções definidas no hw do dia 2022-10-14.
- O lemma de divisão de Euclides para os Nats:
- enuncie
- demonstre
2022-10-31 (IRI)
- Implemente como Nats:
- os inteiros (já sabes a sua especificação pelo IDMa!)
- os parzinhos-de-Nats
- s vetores-de-Nats como Nat
- Implemente como novo tipos, tendo já definido o Nat:
- os inteiros
- os parzinhos-de-Nats
- os vetores-de-Nats como Nat
- 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
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
- Defina as:
head : ListNat → Nat
tail : ListNat → ListNat
init : ListNat → ListNat
last : ListNat → Nat
- Defina a
(<) : Nat → Nat → Prop
e sua internalização, e demonstre a sua corretude.
2022-11-04
- IRI
- Demonstre os teoremas (escolhe algo interessante para botar nos
??
)(∀xs,ys:ListNat) [ sum (xs ++ ys) = ?? ]
(∀xs,ys:ListNat) [ product (xs ++ ys) = ?? ]
(∀ℓ:ListNat) [ length (filterEven ℓ ++ filterOdd ℓ) = ?? ]
(∀ℓ:ListNat) [ reverse (filterEven ℓ) = ?? ]
(∀n:Nat)(∀ℓ:ListNat) [ length (addNat n ℓ) = ?? ]
(∀n:Nat)(∀ℓ:ListNat) [ sum (addNat n ℓ) = ?? ]
(∀n:Nat)(∀ℓ:ListNat) [ sum (multNat n ℓ) = ?? ]
(∀n:Nat)(∀ℓ:ListNat) [ product (multNat n ℓ) = ?? ]
(∀n:Nat)(∀ℓ:ListNat) [ product (expNat n ℓ) = ?? ]
(∀n:Nat)(∀ℓ:ListNat) [ isSorted (addNat n ℓ) = ?? ]
(∀ℓ:ListNat) [ isEven (product ℓ) = anyEven ℓ ]
(∀ℓ:ListNat) [ isEven (sum ℓ) = isEven (length (filterOdd ℓ)) ]
(∀ℓ:ListNat) [ isZero (sum ℓ) = ?? ]
(∀ℓ:ListNat) [ isZero (product ℓ) = ?? ]
(∀n,m:Nat)(∀ℓ:List Nat) [ addNat (n + m) ℓ = ?? ]
(∀n,m:Nat)(∀ℓ:List Nat) [ multNat (n · m) ℓ = ?? ]
- Demonstre também:
(∀xs,ys:ListNat) [ length (xs ++ ys) = ?? ]
(∀xs,ys:ListNat) [ reverse (xs ++ ys) = ?? ]
(∀n:Nat)(∀xs,ys:ListNat)[ addNat n (xs ++ ys) = ?? ]
(∀ℓ:ListNat) [ reverse (reverse ℓ) = ?? ]
(∀ℓ:ListNat) [ length (reverse ℓ) = ?? ]
- Associatividade da
(++)
[]
é uma(++)
-identidade
- Pense em mais propriedades, enuncie, e demonstre!
- Demonstre os teoremas (escolhe algo interessante para botar nos
- INTRO
- Demonstre ou refute as leis seguintes (cada uma tem duas proposições independentes para investigar, e para cada uma tome o cuidado seguinte: se precisar saber que o tipo A é habitado, veja se e como isso afeta a tua resposta):
- (∀x:A)[φ ⇒ ψ(x)] ⇐≟⇒ φ ⇒ (∀x:A)[ψ(x)]
- (∀x:A)[φ(x) ⇒ ψ] ⇐≟⇒ (∀x:A)[φ(x)] ⇒ ψ
- (∃x:A)[φ ⇒ ψ(x)] ⇐≟⇒ φ ⇒ (∃x:A)[ψ(x)]
- (∃x:A)[φ(x) ⇒ ψ] ⇐≟⇒ (∃x:A)[φ(x)] ⇒ ψ
- Demonstre ou refute as leis seguintes (cada uma tem duas proposições independentes para investigar, e para cada uma tome o cuidado seguinte: se precisar saber que o tipo A é habitado, veja se e como isso afeta a tua resposta):
2022-11-05
- IDMb
- ³√2 é irracional? ³√3? ᵏ√n?
- §«Primeiros passos»
- §«Ordem e positividade»
- §«Subconjuntos notáveis e inaceitáveis»
- IDMa
- Para quais naturais
n
temos mesmo que(∀x : Int)[n | x² ⇒ n | x]
?
- Para quais naturais
2022-11-07 (IRI)
- Generalize todas as funções dos hw 2022-11-04 e 2022-10-31 que envolvem
ListNat
para funções que envolvemList α
ou, se não for possível,List Nat
. - Defina as:
concat : List (List α) → List α
ifthenelse : Bool → α → α → α
and : List Bool → Bool
or : List Bool → Bool
splitAt : Nat → List α → (List α × List a)
zip : List α → List β → List (α × β)
unzip : List (α × β) → (List α × List β)
- Defina um tipo para conseguir uma resolução no problema de querer listas cujos membros podem ser
Nat
ouBool
. - Defina um tipo cujos habitantes serão usados para representar listas que garantam:
- ter tamanho ≥ 1 (
IList
) - ter tamanho par (
EList
) - ter tamanho ímpar (
OList
)
- ter tamanho ≥ 1 (
2022-11-08 (IRI)
- URGENTE! Continua (ou começa, pelamor de Curry) o hw do dia 2022-10-17, para incluir as funções que envolvem listas. O arquivo poderia começar assim:
{-# LANGUAGE GADTs, EmptyDataDecls #-} module IRI where data Nat where O :: Nat S :: Nat -> Nat deriving (Eq, Show) data Unit where Star :: Unit data Empty data List a where Nil :: List a Cons :: a -> List a -> List a deriving (Eq, Show)
2022-11-10 (IRI)
- Defina as:
replicate : Nat → α → List α
map : (α → β) → List α → List β
filter : (α → Bool) → List α → List α
- a generalização
all
das:allZero
,allEven
,allOdd
- a generalização
any
das:anyZero
,anyEven
,anyOdd
- a generalização
pointwise
das:pwAdd
,pwMult
- a generalização
fold
das:sum
,product
,and
,or
,concat
- simplifique as definições antigas para aproveitar essas funções poderosas
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
curry : ?
uncurry : ?
flip : ?
- Qual seria uma melhor tipágem para a
pw : (α → α → α) → List α → List α → List α
?
2022-11-11
- IRI
- Descubra o
foldNat
: defina e mostre um uso dele
- Descubra o
- IDMb
- Até o «§. Valor absoluto»
2022-11-17 (IDMb)
- Resolva tudo até o §«Mínima e Máxima»
2022-11-18 (IRI)
- Demonstre a associatividade da
(∘)
- Defina tipos para cada um estilo de árvore que tu já viu ou imaginou
- Formulize os correspondentes princípios/regras de indução para cada um deles
- Mostre como cada um deles pode virar um Functors
- Demonstre as leis de Functor para o
List : Type → Type
com omap
que definimos:map id = id [functor law 1] map (f . g) = map f . map g [functor law 2]
- Demonstre:
(∀f:α→β)(∀p:β→Bool) [ filter p ∘ map f = map f ∘ filter (p ∘ f) ]
- Adivinha um lado direito certo e interessante, e demonstre:
take n xs ++ drop n xs = take m . take n = take m . drop n = drop m . take n = drop m . drop n = map g . map f = sum . map double = sum . map sum = sum . sort = map f . reverse = concat . map concat = filter p . map f = length . reverse = reverse . reverse =
- Quais das seguintes são válidas e quais não?
map f . take n =?= take n . map f map f . reverse =?= reverse .map f map f . sort =?= sort . map f reverse . concat =?= concat . reverse . map reverse filter p . concat =?= concat . map (filter p)
- Demonstre:
xs ++ (ys ++ zs) = (xs ++ ys) ++ zs [associatividade da (++)] length (xs ++ ys) = length xs + length ys filter p (xs ++ ys) = filter p xs ++ filter p ys map f (xs ++ ys) = map f xs ++ map f ys
- Demonstre:
sum (xs ++ ys) = sum xs + sum ys product (xs ++ ys) = product xs * product ys concat (xss ++ yss) = concat xss ++ concat yss
- Podemos definir uma generalização da
pw : (α → β → γ) → (F α → F β → F γ)
sabendo apenas que oF
possui umfmap
com qual ele se torna um Functor? - Implemente os racionais!
2022-11-20 (IRI)
- Na última aula percebemos que
Either
não tinha sequer chances de se candidatar para virar um Functor, poisEither
não é umType → Type
(mas sim umType → Type → Type
. Mesmo assim, conseguimos verificar que aplicando parcialmente oEither
num tipoε
só, chegamos mesmo noEither ε
que é mesmo umType → Type
, e logo tem chances de ser um Functor, e descubrimos qual seria afmap
certa pra isso (demonstre se não demonstrou—o que é pra demonstrar mesmo??). Aqui mais duas coisinhas que estão tambémType → Type → Type
: o próprio(→)
e o(×)
. Investigue para cada um deles, e para cada aplicação parcial dele, se pode ser munida com umfmap
para conseguir ser um Functor:(δ →) : Type → Type
(→ γ) : Type → Type
(α ×) : Type → Type
(× β) : Type → Type
2022-11-24 (IDMb)
- Resolva tudo até o §«Infimum e supremum»
- Formulem bem o critério-Davi sobre infimum/supremum (usando epsilons ♡), e demonstrem
- Demonstre a unicidade de infima/suprema
- (IRI) Tendo um tipo
Real
, defina um data typeXReal
para representar os reais extendidos. - Enuncie e demonstre o teorema da indução para os reais-naturais.
- Ache alguma propriedade que é satisfeita no $\mathbb R_{\mathbb Q}$ mas não no $\mathbb R$. Cuidado: a resposta “óbvia” é errada.
2022-11-28 (IRI)
- Prática para indução nos naturais: resolva o Problem Set 2 de 2021.2.
- Na aula de IDMb definimos uma
(·) : Real × Seq(Real) → Seq(Real)
em duas formas: implemente ambas em Haskell e demonstre a sua equivalência.
2022-11-29 (IDMb)
- Defina as $\mathtt{toNat} : \mathbb R_{\mathbb N} \to \mathsf{Nat}$ e $\mathtt{toRealNat} : \mathsf{Nat} \to \mathbb R_{\mathbb N}$; enuncie o que significa que comportam na maneira desejada; demonstre.
- Seja
(Aₙ)ₙ : Seq(α)
uma (⊇)-chain. Demonstre que ⋃ₙAₙ = A₀ - Seja
(Aₙ)ₙ : Seq(α)
uma (⊆)-chain. Demonstre que ⋂ₙAₙ = A₀ - Demonstre que não muda nada se a gente trocar o (≥) por (>) e o (≤) por (<) nas definições de «valores-suficientemente-grandes» e de «eventualmente».
- Na aula cairam na mesa 3 possíveis definições do que significa «(aₙ)ₙ é constante». Investigue se são equivalentes “duas a duas”:
- (∃k)(∀n)[ aₙ = k ]
- (∀n)(∀m)[ aₙ = aₘ ]
- (∀n)[ aₙ = aₙ₊₁ ]
2022-11-30 (IDMb)
- Θ. eventualmente constante ⇒ cotada
- Θ. convergente ⇒ cotada
- Θ. autoconvergente ⇒ cotada
- Θ. convergente ⇒ autoconvergente
- Θ. Comportamento algébrico de limites
- (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ + bₙ)ₙ → a + b
- (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙbₙ)ₙ → ab
- (aₙ)ₙ → a ⇒ (caₙ)ₙ → ca
- ?? & (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ/bₙ)ₙ → a/b
- Alguma das recíprocas das implicações acima é válida?
- Θ (sanduíche): (aₙ)ₙ → ℓ & (cₙ)ₙ → ℓ & (aₙ)ₙ ≤ (bₙ)ₙ ≤ (cₙ)ₙ ⇒ ??
- Θ: $\{a_n\}_n \subseteq {\mathbb R}_{\mathbb Z}$ e $(a_n)_n$ convergente ⇒ ??
- Definição.
Seja $(a_n)_n$ uma seqüência de reais.
Seja $(n_i)_i$ uma seqüência de naturais estritamente crescente.
Chamamos a $(a_{n_i})_i$ uma subseqüência de $(a_n)_n$.
- Θ. autoconvergente com subseq convergente ⇒ convergente
- Depois de resolver os anteriores, tente demonstrar/refutar os:
- autoconvergente ⇒ convergente
- cotada superiormente & crescente ⇒ convergente
2022-12-03 (IRI)
- Ordenação (sorting)
- Defina sozinhos os: merge sort; quick sort ;insertion sort
- ASTs
- Defina tipos para representar:
- expressões de aritmética sem variáveis:
- expressões de aritmética com variáveis;
- expressões de lógica proposicional
- Defina funções de
eval
estep
apropriadamente para cad um dos teus tipos
- Defina tipos para representar:
- Arvores
- Defina as:
nodeSize : BinTree α → Nat
size : BinTree α → Nat
depth : BinTree α → Nat
leaves : BinTree α → List α
mapTree : ?
mirror : BinTree α → BinTree α
flatten : BinTree α → List α
findTree : α → BinTree α → List (List Nat)
sumTree : BinTree Nat → Nat
- Adivinhe uma conexão entre o número
size t
e o númeronodes t
: enuncie e demonstre! - Θ.
size t ≤ 2 ^ depth t
- Θ.
depth t ≤ length (flatten t)
- Verifique que tu passou EM & ME mesmo, reescrevendo o que demonstrou acima utilizando
log₂
- Defina o resto dos tipos de arvores discutidos nas aulas (peça detalhes no Zulip!)
- BinSearchTree α
- BinLabTree α β
- RoseTree α
- Demonstre como todos teus típos de árvores viram Functors
- Demonstre:
length ∘ flatten = ??
flatten ∘ mirror = ??
mirror ∘ mirror = ??
depth ∘ mirror = ??
depth ∘ fmap f = ??
fmap f ∘ mirror = ??
- Defina as:
- Eficiência “por indução” / parametro acumuladora: use a metodo que encontramos na aula eliminando o (⧺) da
reverse
para:- eliminá-lo da tua
flatten
- eliminá-lo da tua
leaves
- eliminá-lo da tua
- Folds & lists
- Defina uma foldT para os tipos de arvores que faz sentido definir
- Defina uma foldE para os tipos de Either
- Discuta qual deveria ser o tipo de uma
unfold
que cria listas a partir de outros valores; depois defina! reverse (xs ⧺ ys) = reverse ys ⧺ reverse xs
- Demonstre a lei de fusão do
foldr
que é: dado ??, temos:f ∘ foldr g a = foldr h b
2022-12-12 (IDMb)
- Resolva sozinho os teoremas seguintes que demonstramos na aula passada:
- (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ + bₙ)ₙ → ??
- (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙbₙ)ₙ → ??
- …e o resto do Θ. Comportamento algébrico de limites:
- (aₙ)ₙ → a ⇒ (caₙ)ₙ → ??
- ?? & (bₙ)ₙ → b ⇒ (bₙ⁻¹)ₙ → ??
- ?? & (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ/bₙ)ₙ → ??
- (aₙ)ₙ → a & ?? ⇒ (aₙᵏ)ₙ → ??
- Θ. conv ⇒ autoconv
- Θ. autoconv ⇒ cotada
- C. conv ⇒ cotada
- Θ. autoconvergente com subseq convergente ⇒ convergente
- Θ. 0 < ϑ < 1 ⇒ (ϑⁿ)ₙ → ??
- Θ. Toda seq possui subseq “monótona”
- Dica 1: Def. Chamamos o natural k de pico para a (aₙ)ₙ sse (∀n≥k)[ aₖ ≥ aₙ ]
- Dica 2: Separe em casos: Caso (aₙ)ₙ tem quantidade infinita de picos; Caso contrário.
- «Agora sim!» Demonstre os: Nested Interval Property de [Cantor][Cantor]; Monotone Convergence Theorem; [Bolzano][Bolzano]–[Weierstrass][Weierstrass] Theorem; [Cauchy][Cauchy] convergence critérion
- Θ. (NIP): Teorema dos intervalos aninhados:
Se (Iₙ)ₙ é uma (⊇)-cadeia de intervalos fechados habitados da forma Iₙ = [aₙ,bₙ],
então ⋂ₙIₙ habitado.
Ainda mais: Se (diam(Iₙ))ₙ → 0, então ⋂ₙIₙ é um singleton!- Dica 1: a₀ ≤ a₁ ≤ a₂ ≤ ⋯ ≤ b₂ < b₁ ≤ b₀
- Dica 2: (aₙ)ₙ sup-cotada; (bₙ)ₙ inf-cotada
- Dica 3: Encontre a≤b tais que ⋂ₙIₙ = [a,b]
- Θ. (MC): cotada & “monótona” ⇒ convergente
- Θ. (BW): cotada ⇒ conv subseq
- Θ. (CC): autoconvergente ⇒ convergente
- Θ. (NIP): Teorema dos intervalos aninhados:
- [Αρχιμήδης][Archimedes]:
- Θ. Os reais naturais não são cotados
- Θ. (∀ε>0)(∃n)[ 1/n < ε ]
- Θ. (∀s≠0)(∃n)[ ns > 1 ]
- Θ. (∀ε>0)[ε$\mathbb R_{\mathbb N}$ não é cotado]
- Θ. (∀s≠0)(∀b)(∃n)[ b < ns ]
- Θ. (∀b)(∀s≠0)(∃n)[ ns > b ]
- Q. Há diferença entra as duas últimas? Como chamarias cada uma no «nível coração»?
- Existência de raizes
- Θ. Raizes de pequenos: a < 1 ⇒ (aₙ)ₙ → √a, onde: $$\begin{align*}
a_0 &= 0 \\
a_{n+1} &= a_n + \frac 1 2 (a - a_n^2)
\end{align*}$$
- Dica 1: cotada…
- Dica 2: …crescente…
- Dica 3: …logo conv. O que falta agora?
- Θ. «[Ἵππασος][Hippasus] precisa morrer» (aka: «√2 é real»)
- Dica 1: Considere o H ≝ { x | x² < 2 }
- Dica 2: Seja h = sup H. Elimine as possibilidades h² < 2 e h² > 2
- Dica 3: Lembrete: o dado h = sup H é uma conjunção e vamos precisar ambas as suas partes: uma para eliminar o caso h² < 2 e a outra para eliminar o caso h² > 2.
- Dica 4: Para eliminar caso h² < 2: calcule o
(h + 1/n)²
para conseguir supcotá-lo porh² + (algo controlavelmente pequeno)
, e logo por2
, contradizendo a parte de «cota superior». - Dica 5: Para eliminar caso h² > 2: calcule o
(h - 1/n)²
para conseguir infcotá-lo porh² - (algo controlavelmente pequeno)
, e logo por2
, contradizendo a parte de «melhor».
- Θ. Existência das raizes ²√
- Θ. Existência das raizes ᵏ√
- Θ. Raizes de pequenos: a < 1 ⇒ (aₙ)ₙ → √a, onde: $$\begin{align*}
a_0 &= 0 \\
a_{n+1} &= a_n + \frac 1 2 (a - a_n^2)
\end{align*}$$
- Densidades:
- Θ. dos reais racionais nos reais
- Θ. dos reais irracionais nos reais
- Cardinalidades (1):
- Ache seqüência de reais que “ocupa” os reais naturais
- Ache seqüência de reais que “ocupa” os reais inteiros
- Ache seqüência de reais que “ocupa” os reais racionais
- Chega sozinho nas definições de liminf / limsup e depois…:
- Θ. (aₙ)ₙ → ℓ ⇒ liminfₙ aₙ = ℓ = limsupₙ aₙ
- Θ. infₙ aₙ ≤ liminfₙ aₙ ≤ limsupₙ aₙ ≤ supₙ aₙ
- Θ. (∀ε>0)(∃K)(∀k≥K)[ liminfₙ aₙ - ε ≤ aₖ ≤ limsupₙ aₙ + ε ]
- Θ. x ≥ limsupₙ aₙ ⇔ (∀ε>0)[ temporariamente (aₙ)ₙ > x + ε ]
- Θ. x ≤ liminfₙ aₙ ⇔ (∀ε>0)[ temporariamente (aₙ)ₙ > x - ε ]
- Θ. x ≤ limsupₙ aₙ ⇔ (∀ε>0)[ freqüentemente (aₙ)ₙ > x - ε ]
- Θ. x ≥ liminfₙ aₙ ⇔ (∀ε>0)[ freqüentemente (aₙ)ₙ < x + ε ]
- Θ. liminfₙ aₙ + liminfₙ bₙ ≤ liminfₙ (aₙ+bₙ) ≤ limsupₙ (aₙ+bₙ) ≤ limsupₙ aₙ + limsupₙ bₙ
- Q. liminfₙ(pₙ₊₁ - pₙ) = ? onde pₙ é o n-ésimo primo
- Q. liminfₙ (sin(n)) = ?
- Q. limsupₙ (sin(n)) = ?
- Algébricos vs Transcedentais
- Existem transcedentais?
- Qualquer conjunto de reais habitado e finito possui mínimo e máximo
2022-12-15 (IDMb)
- Resolva o hw do dia 2022-12-12 que não foi resolvido na aula; re-resolva sozinho o que foi.
- Termine para cada uma das séries que encontramos o que faltou:
- $\sum_{n=1}^\infty \frac 1 {2^n}$
- $\sum_{n=1}^\infty \frac 1 {n^2}$
- $\sum_{n=1}^\infty \frac 1 n$
- O conjunto dos irracionais é (+)-fechado? (·)-fechado? (^)-fechado?
- Na aula anterior mostrei um esboço para demonstrar o (BW) a partir do (MCT). Ache em uma outra maneira, a partir do (NIP).
- Na aula anterior demonstramos o Θ. ϑ pequeno ⇒ (ϑⁿ)ₙ → 0. Ache uma outra demonstração, começando com a observação (justificada!) que $\frac 1 \vartheta = \delta + 1$ para algum $\delta > 0$. Use o teorema binomial! (Podemos mesmo?)
Histórico
2022-08-22: INTRO (1): Overview; tipos [video]
- Overview
- tipos e type errors
- proposiões vs objetos
- Prop vs Bool
2022-08-24: INTRO (2): Definições [video]
- intensão vs extensão
- = vs ⇔
- «def»
- comandos vs proposições
- REPL
- Exemplos de teoremas e seus tabuleiros (estados) iniciais
- Dados e Alvo
- açúcar sintáctico
- sintaxe vs semântica
- variáveis ligadas vs livres
- escopos de variáveis
- capturamento de variável
- definição e seu contexto
- escolha boa de variável, variável fresca
- bairros de variáveis
- os ¬,⇒,⇔,&,ou,∀,∃,=
2022-08-26: INTRO (3): Demonstrações [video]
- ocorrências ligadas vs livres de variáveis e ligadores
- sombreamento (shadowing) de variáveis
- Propriedades da igualdade: refl, sym, trans, e substituição
- «Calculamos»: seu uso, sua escrita, e seus efeitos
- definições como abreviações
2022-08-29: INTRO (4): Demonstrações [video]
- o resto dos conectivos para nossa linguagem de demonstrações
- os ⇔, ¬, ⇐, como açúcar sintáctico
- o ⊥ como conectivo primitivo
- umas “leis de lógica” e como demonstrá-las
2022-08-31: Prova 1.1
2022-09-02: INTRO (5): Demonstrações; IDMa (1) [video]
Demonstrações
- Proposição mais forte vs mais fraca que outra
- P ⇒ ¬¬P
- ¬¬(P ∨ ¬P)
- ¬¬P ⇒ P
- RAA (Reductio ad Absurdum)
- LEM (Law of Excluded Middle)
- Matemática não-construtiva
IDMa: IDMa (1)
- Especificação × Implementação
- Os inteiros $(\mathbb Z;0,1,+,-,\cdot)$
- Axiomas sobre os inteiros
- Axiomas vs Teoremas
2022-09-05: IDMa (2) [video]
- bom dia / recap
- Teoremas x axiomas; dependências de demonstrações
- Q: por que não aparece (=) na estrutura dos inteiros?
- Q: como rotular teoremas?
- Sintaxe vs Semântica; convenções sintácticas
- juxtaposição; notação infixa/postfixa/prefixa
- arvore sintáctica; parsing; precedência sintáctica de operadores
- associatividade sintáctica
- Operações primitivas vs. definidas
- subtração como operação definida e não primitiva
- uns numerais para ajudar: 2, 3, …
- potências com expoentes naturais; convenção sobre associatividade sintáctica da exponenciação
- Q: igualdade sintáctica vs intensional
- Q: o parsing se trata de quais operações?
- Cancelamento multiplicativo
- Q: qual a associatividade sintáctica da (⇒)?
- Q: refutação..?
- Não-zerodivisores.
- Q: o «ou» é exclusivo?
- (Plicker) axiomas ou teoremas?
- A resposta certa; mais teoremas
- Existência e unicidade; artigo indefinido vs definido; proof by fight club; alternativa conhecendo já um legal
2022-09-09: IDMa (3) [video]
- Dica sobre como enxergar alvos
- A utilidade de lemmas sobre unicidade de resolução de equações num incógnito
- Exemplos: (∀a)[(-1)a = -a]; (∀a)[0a = a]
- Axioma x Teorema; Noção primitiva x definida
- Axiomas sobre ordem: duas maneiras de axiomatizar
- A (≤) nos naturais é definível
- Conjunto fechado sob operação
- Notação set-builder (com comprehension)
- interpretação de (∈)
- Como tratar um subconjunto como predicado unário
- 1 é positivo: teorema ou axioma?
- O módulo (absolute value)
|_| : Int → Int
- Para refletir: a independência duma proposição: indemonstrabilidade e irrefutabilidade
2022-09-12: IDMa (4) [video]
- como definir «ser fechado sob uma operação n-ária (para n=1,2)
- uma primeira conversa “adulta” sobre conjuntos
- um preconceito sobre as
()
na notaçãof(x)
- a notação set-builder: como ler e escrever, e como não ler e como não escrever
- 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ℤ
- Θ. 1 é positivo
- Como demonstrar a indemonstrabilidade de proposições
- A indemonstrabilidade do 0 ≠ 1
- notação infixa x postfixa x prefixa x mixfixa
2022-09-14: IDMa (5) [video]
- Não existe inteiro estritamente entre 0 e 1: teorema ou axioma?
- 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
- o mínimo dum conjunto, quando existe é único
- Umas propriedades do valor absoluto
2022-09-16: IDMa (6) [video]
- um pleno «tal que» é capaz de destruir uma frase e torná-la pior-que-errada
- Princípio da boa ordem ($\mathbb Z_{>0}$ é bem ordenado)
- Como usar o PBO na prática
- Principios de indução como teoremas
- 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
- Indução com mais que uma base
2022-09-19: IDMa (7) [video]
- uma interpretação geométrica dos inteiros
- PBO shiftado e demais versões
- Indução forte (“course-of-values”)
- Quebrando os inteiros em tijolinhos atômicos usando como cimento: (i) adição; (ii) multiplicação
- Definição de invertível
- Definição de irredutível
2022-09-21: IDMa (8) [video]
- O que queremos? (Wishlist)
- Divisão (quot e rem)
- algoritmo para calcular os quot e rem
- definir e justificar sistemas posicionais de numerais
- mdc e mmc
- fatorização única (ao menos de coisas sensatas) de inteiros (teorema fundamental de aritmética)
- O lemma da divisão de Euclides: enunciado
- Números, numerais, dígitos
- Expansão e sistemas posicionais
- Notação Σ de somatórios
- O logaritmo como tamanho de númerais melhor que o length deles como strings
- Enunciado do Teorema Fundamental de Aritmética (fatorização única)
- Explicação intuitiva sobre como sistemas posicionais funcionam
- generalização da palavra “maior” para outras ordens
- diagrama Hasse para os $\mathbb{Z}_{\geq 0}$
- mdc: definição nível coração
2022-09-23: IDMa (9) [video]
- O lemma da divisão de Euclides: esboço de demonstração
- 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.
- “mℤ” ⇔ “fechado sob ops”: concretização e esboço
- Duas maneiras de obter membros arbitrários de um conjunto indexado
- Esboço do Teorema Fundamental de Aritmética (fatorização única de inteiros)
2022-09-26: IDMa (10) [video]
- Invertible, Unit, Irreducible
- Prime
- m.d.c.
- Um exemplo: m.d.c. dos 12,18; divs; comdivs
- Q: como assim um-maior? A: hmm-maior
- O que acontece se trocar de (|) para (≤)?
- O que acontece se trocar de direção nas ordens?
- Q: qual o tipo desse min?
- Dados a,b, existe mesmo um m.d.c. deles?
- Como vou escolher o m.d.c. se os comdivs são esses?
- Θ. Existência de m.d.c.
- Q: qual o nome da alma que os m.d.c. e o min compartilham?
- Duas maneiras de obter membro arbitrário de conjunto indexado
- Q: Como exatamente funciona essa notação set builder?
- m.d.c. vs m.m.c (teaser de dualidade)
- mesmo demonstrando a existência, queremos algoritmo e de preferência eficiente
2022-09-28: Prova 1.3; IDMa (11) [video]
- Como demonstrar (a,b)=(c,d).
- Algoritmo de Euclides: corretude e terminação
- Terminação, Corretude, Eficiência
- Algoritmo estendido de Euclides
- coprimos
2022-09-30: IDMa (12) [video]
- 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
- “unicidade” de m.d.c.
- Teorema de Euclides sobre infinidade de primos e sua demonstração construtiva
- sermão sobre x² par ⇒ x par
- generalizações
- m.d.c. e os coeficientes Bézout
- Lemma de Euclides: x irredutível ⇒ x primo
- Momentos que parecem LEM mas não são
- Sobre a contaminação de demonstrações com magias ⛤
- [Erdős][Erdos]: «proofs from [The Book][proofs-from-the-book]»
- Teorema de Euclides: há uma infinidade de primos
- Como decidir se um inteiro é primo.
- Sobre Euclides e seus Elementos
- Sobre o teorema fundamental de aritmética
- Como codificar listas de inteiros nos inteiros?
2022-10-05: IDMa (13) [video]
- Correção sobre o «algoritmo da criança» vs «algoritmo de Euclides»
- Fatorização é lenta
- Densidade de primos e gaps
- Algumas conjecturas da teoria dos números: Gêmeos, Goldbach, Collatz, Legendre
- O enunciado do teorema dos números primos (PNT)
- O enunciado do teorema Chebyshev (postulado de Bertrand)
- Congruência módulo um inteiro e demonstrações das suas propriedades
- Aritmética modular e propriedades do $\mathbb Z / m\mathbb Z$
- (·)-inversos módulo um inteiro m
2022-10-07: IDMa (14) [video]
- por que as duas definições de congruência não são mesmo equivalentes
- o planeta 0: a terra
- o planeta 1: o {⋆}
- as notações mA e A+k e os mℤ, mℤ+k
- Aritmética módular, pouco mais adulta
- Θ: Invertibilidade módulo m
- D: Congruência, compatibilidade com operações
- Θ: Unicidade de inversos módulo m
- Critéria de divisibilidade
- O Teorema Fundamental de Aritmética para os racionais
- Sobre um sistema de resíduos módulo p
- Plicker: «Existem quantos planetas onde todos os não nulos são invertíveis?»
2022-10-10: IRI (1) [video]
- introdução
- um resumo da abordagem (axiomática) que usamos em IDMa
- especificação vs implementação; implementação-agnóstico
- a abordagem desta disciplina (IRI): mais contrastes de abordagem
- [algebraic data types][algebraic-data-types]
- o tipo Nat: espectativas e 4 maneiras de definir um tipo de dados recursivamente
- sintaxe: o que queremos descrever
- o desafio dos «…» numa definição
- exemplo de chefe de programação sem noção comunicando pedido
- Naturais vs Nats; Números vs Numerais
- Linguagem vs Metalinguagem; Variáveis vs Metavariáveis
- «Nada mais»
- Regras de inferência e lida de cima para baixo e de baixo para cima
- Como mostrar que algo é um Nat
- arvores de inferência, folhas abertas e fechadas; regras e comandos
- casamento de padrão com expressão: primeiro encontro
- gramáticas e a [notação BNF][bnf]: nada demais!
- Mal entendido: «os inteiros que a gente conheceu»—Nope.
- Mal entendido: «uns inteiros são naturais»—Nope.
- type casting
- a aplicação duma função no seu argumento, e a inferncia de tipo relevante
- Tem como implementar os inteiros usando os naturais, e mais uns teasers
- Regras e arvores de inferência, comandos vs proposições
- Um exemplo de inferência: SSSO : Nat
- Definição recursiva vs tijolo
- um exemplo: fact : Nat → Nat
- Como traduzir uma linha sem premissas para código
2022-10-14: IRI (2) [video]
- ocorrências livres e ligadas de variáveis
- construtor vs função
- uns açúcares sintácticos
- uns preconceitos sobre funções e sua notação
- ocorrências ligadas e livres de variáveis
double : Nat → Nat
;id : Nat → Nat
- padrões de argumentos
- o presente da recursão
- Como calcular (modelo computacional)
- double 2 = ?
- valores canônicos
- casamento de padrões
- Duas maneiras de escrever cálculos
- A adiçaõ: (+)
- prefix, postfix, infix, mixfix
- Um cálculo e teorema: 2 + 3 ≟ 5
- [Arvore sintáctica (Abstract Syntax Tree)][ast], [parsing][parser], (veja também: [lexer][lexer])
- Precedência sintáctica
- Associatividade sintáctica
- Associatividade vs associatividade sintáctica: axiomas e especificação vs implementação
- Currificação
- como definir o
addFive
nível boss - Aplicação parcial
X 2022-10-15: IRI (3,4) [video]
- construtor vs função
- D: multiplicação
- o uso de lemmas: m-idR, e-idR
- uma demonstração simples: (·)-idR
- ∀: como usar
- ∀: como atacar
- qual resultado incompleto é melhor?
- lazy vs strict
- estratégia de evaluação vs precedência de operador
- notação de aplicação de função por espaço:
f x
- acordos sintácticos sobre a aplicação-de-função: precedência, associatividade sintáctica à esquerda:
f x y z ≡ ((f x) y) z
, e os seus porquês - Θ. 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-10-17: IDMa (15) [video]
- Decepção de falta de hw
- Achando inversos modulares
- Exponenciação modular
- Resolvendo congruências
- Resolvendo sistemas de congruências
- Θ. infinidade de primos da forma 4k+1 e da forma 4k+3
- Θ. teorema de Wilson
- Ferramentas até agora: rápidos vs lentos
- Pouco de análise combinatória
- Θ. Teorema pequeno de Fermat: enunciado
- Teorema e coeficientes de binomial
- Θ. O sonho do calouro
- $p$ divide o $C(p,i)$ para $0 < i < p$
2022-10-19: IRI (5): Nat [video]
- dois princípios sobre os construtores e os valores construidos
- escolhendo o padrão na direita duma equação para substituir na direção (←)
- o problema que temos demonstrando a (+)-associatividade
- A regra de inferência Ind-φ. (Onde φ : Nat → Prop.)
- Demonstração por indução
- A associatividade da (+): umas demonstrações por indução diferentes.
- Análise das duas melhores demonstrações da (+)-associatividade: legalzinho vs legalzão
- Inventar teoremas-propriedades sobre nossos programas
2022-10-21: IDMa (16) [video]
- Θ. Teorema binomial
- Θ. O sonho do calouro
- Θ. “Fermatinho” de Fermat (demonstração de Euler, por indução)
- A hipotese (errada) “chinesa”
- Enganadores do Fermatinho: Carmichael
- Teste de primalidade de Fermat
- Se tem ilegais, pelo menos a metade é ilegal
- Como gerar primos
- Sistemas de resíduos módulo m: completos e reduzidos
- A função totiente de Euler
2022-10-24: IDMa (17) [video]
- p-valuações, tamanho e distância p-adica
- raizes quadradas e resíduos quadráticos módulo p
- Euler entra!
- Umas aplicações da teoria dos números inteiros
- Sobre criptografia
- Criptografia vs [steganografia][steganography]
- (see also: [lipograma][lipogram], [La Disparition][la-disparition], [Oulipo][oulipo])
- Cæsar, rot13
- one-time pad
- Plicker survey
2022-10-26: IDMa (18); Prova 1.4 [video]
- φ(pᵃ) = pᵃ - pᵃ⁻¹
- φ é multiplicativa
- criptografia RSA
- assinaturas digitais: objetivo
X 2022-10-27: IRI (6,7): Nat, Bool [video]
- currificação: versão currificada vs descurrificada da mesma função
- associatividade sintáctica
- inferência de tipo de aplicação de função
- conexão com uso de implicação; [propositions-as-types][propositions-as-types]
- prerequisito para perguntar sobre igualdade: mesmos tipos!
- Como implementar o tipo
Bool
(e suas operações) em termos deNat
: problemas - pra quem esse return 0 está retornando tal 0 nas mains dos programas?
- os booleanos precisam suas operações também
- booleanos em python e type casting
- a diferença entre a parte (e tipagem) estática e a parte (e tipagem) dinâmica
- type sistem e checagem de tipo vs evaluação de expressão para achar um valar
- O tipo
Bool
(de verdade) - Ordem: (≤) vs leq: mundo-objeto e mundo-meta
- corretude (soundness & completeness) de programas
(≤) : Nat → Nat → Prop
leq : Nat → Nat → Bool
- Relações vs funções-com-codomínio-Bool
- Como representar predicados sobre os naturais (Nat → Prop, Nat→Nat→Prop, etc.) como se fossem funções que retornam
Bool
. - A corretude da
leq
- internalização de conceito
- O uso de underscore nos padrões
- uma convenção sobre a ordem de equações numa definição recursiva
- Sobre funções parciais vs totais
- side effects (efeitos colaterais) e funções puras
- Type inference; como/quando aproveitar a inferência de tipos
- even e odd (pares e impares): como internalizar e como demonstrar corretude
ev, od : Nat → Bool
- treis maneiras diferentes de definir: precisando 3 equações; precisando o not; com recursão mútua
- recursão mútua
- backticks para notação infixa
- Como usar o underscore (_) como «variável sem nome» num padrão.
2022-10-31: IRI (8): Nat, Bool, Weekday, Unit, Empty, ListNat [video]
- Type synonym
- Desafio: Int parzinhos-de-Nats, vetores-de-Nats
- isBool : Nat → “Bool”
- O que acontece em linguagem que autoafirmam ter «tipos dinâmicos»
- Corretude de definição de função (programa): correção e completude
- Mais tipos de dados simples:
Weekday
- O tipo
Unit
com seu único habitánte/construtor:⋆ : Unit
- Quem é mesmo esse
void
? - Indução do Nat e quando não usar
- Q: faz sentido adicionar como açúcar sintáctico para o lem n m assumir papel de Prop? A: Não.
- Como implementar listas:
ListNat
- Os construtores
Empty
(ouNil
) eCons
- ListNat: sintaxe, açúcar e associatividade sintáctica
- Como escolher a ordem dos argumentos: aplicação parcial e currificação
- ListNat é um tipo recursivo
- Como representar a lista [2,0,8] com nosso tipo
- definindo a
length : ListNat → Nat
- Calculando o
length [3,2,0]
- Plicker: quantos construtores preciso para definir o tipo Int?
2022-11-04: IRI (9): Nat, Bool, Unit, Empty, ListNat [video]
- Definições de
sum : ListNat → Nat
eproduct : ListNat → Nat
- como escolher o valor certo para o
sum []
e oproduct []
- como escolher o valor certo para o
reverse
,append
, e concatenação binária(⧺)
- parenteses e convenções sintácticas do ␣
- mal-entendido entre função currificada-vs-descurrificada e notação infixa-vs-prefixa
- aplicação parcial e um cálculo relacionado
- «redex»
- a notação de “sections” de operadores binários
- um problema com as
head
etail
- um teaser sobre a soma de tipos
- Construtores vs Destrutores
- Corretude de programas sobre ListNat: propriedades que gostariamos de demonstrar
- Tentativa de demonstrar uma delas
- Como chegar aos principios de indução para os outros tipos
- O conceito de «respeitar/preservar uma propriedade».
- Do $\mathrm{Ind}^{\mathsf{Nat}}_{\varphi}$ para o $\mathrm{Ind}^{\mathsf{ListNat}}_{\varphi}$.
- Indução do
Bool
- Indução do
Unit
- Indução do
Empty
- Indução do
ListNat
- Indução do
- Como interpretar a indução e suas várias versões dos inteiros agora
- Uma maneira de pensar sobre indução: como separação-em-casos-com-extras
- Conexão entre recursão e indução
- Definição por recursão vs Demonstração por indução
- O presente de recursão vs o presente da indução
- Quantos quantificadores e por quê?
- Quantos destrutores e por quê?
X 2022-11-05: IDMb (1,2) [video]
- Pythagoreanos e a interpretação de número na grécia antiga
- Os números: naturais, inteiros, racionais, reais
- Θ. O √2 é irracional
- Lemma-chave: x² par ⇒ x par
- A “existência” do √2, pelo teorema pythagoreano
- E quem se importa sobre a racionalidade do √2?
- Buracos na linha dos racionais
- A linha continua dos reais
- De √2 para √3
- E sobre o √4?
- Tentativa de generalização para outros √n
- Como demonstrar a parte de: «não há outra saida»
- Especificação dos reais (1/3): parte algébrica (aditiva e multiplicativa)
- O que podemos aproveitar «de graça» dos teoremas da teoria dos números inteiros?
- Uma divulgação/propaganda de álgebra abstrata
- Especificação dos reais (2/3): parte relacional (ordem)
- Definições usando as noções primitivas da especificação, e qual o trabalho dum implementador
- Notação: a⁻¹ e a/b; o uso do artigo definido, e a necessidade de demonstrar existência e unicidade
- A unicidade da identidade aditiva: o que significa
- Definições dos a⁻¹ e a/b
- O que precisamos demonstrar sobre nossas novas noções definidas
- potências de um real elavado a um natural
- potências de um real elavado a um inteiro
- potências de um real elavado a um racional
- potências de um real elavado a um real: impossível conseguir isso ainda
2022-11-07: Prova 2.1; IRI (10a) [video]
- Polimorfismo de tipos, e o type constructor
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
paralength : List α → Nat
2022-11-09: IRI (10b, 11) [video]
- polimorfismo: função(ões)
id
- o tipo de
bottom
- Nats bottomosos (⊥, nats parciais, o nat infinito)
- mais um tira-gosto/teaser da idéia de [propositions-as-types][propositions-as-types]
- funções de ordem superior (higher-order functions)
- como agir se precisar numa lista ter naturais e booleanos: NatOrBool
- abstração de ordem superior: de
addNat : Nat → List Nat → List Nat
paramapNat : (Nat → Nat) → List Nat → List Nat
- abstração de ordem superior: de
mapNat : (Nat → Nat) → List Nat → List Nat
paramap : (α → β) → List α → List β
- [a função map][map]:
map : (α → β) → List α → List β
- [a função filter][filter]: a
filter : (α → Bool) → List α → List α
- novas implementações das funções antigas
- Do $\mathrm{Ind}^{\mathtt{ListNat}}_{\varphi}$ para o $\mathrm{Ind}^{\mathtt{List~α}}_{\varphi}$.
- o
Maybe : Type → Type
- comparação dos tipos
Maybe (List α)
eList (Maybe α)
- Idéia ruim: usar um valor arbitrário para o
head []
- as versões não-gambiarrosas de
head
etail
- Resolução legal:
safeHead : List α → Maybe α
- Resolução legal:
safeTail : List α → Maybe (List α)
- desafio: como generalizar as sum, product, concat
- por que não podemos tipar a sum com List α → α?
- Uma find melhor que as gambiarras C’osas:
findFirst : α → List α → Maybe α
2022-11-11: IDMb (3,4) [video]
- Θ. cancelamento aditivo pela esquerda (RA-CanL)
- Θ. resoluções únicas
- duas maneiras diferentes de escrever uma demonstração
- como justificar o “somar o mesmo real nos dois lados”
- funções anônimas, notação lambda, notação “mapsto” (↦)
- umas demonstrações dos primeiros teoremas sobre reais
- valor absoluto nos reais: definição e sua interpretação geométrica
- distância: especificação e implementação
- a desigualdade triangular e sua interpretação geométrica
- demonstração de
(∀a,b,c)[ |a - c| ≤ |a - b| + |b - c| ]
- subconjuntos notáveis de reais; [type coercing e type casting][type-coercion]
2022-11-16: IDMb (5,6) [video]
- conjuntos: o que significa em saber qual é um conjunto
- como definir operações entre conjuntos
- como generalizar as operações binárias ∪,∩ para serem aplicáveis em coleções de conjuntos
- ⋃,⋂ : Set(Set(α)) → Set(α)
- ⋃,⋂ : Seq(Set(α)) → Set(α)
- as relações (⊆) e (⊇)
- distância e espaços métricos: especificação vs implementações
- Frases legais do ♡:
- ε-perto
- ε-vizinhança, ε-bola (aberta/fechada)
- Seqüências: notação e interface e type coercion
- notação sobre intervalos e seqüências
- cota inferior/superior de conjunto, e notação sobrecarregada dos (≤) e (<)
- Igualdades que não são igualdades
- Unicidade de mínima/máxima
- intervalos abertos e fechados e notações que envolvem os -∞/+∞
2022-11-18: IRI (12,13) [video]
- os destrutores são, em geral, parciais; versões seguras
- de
NatOrBool
paraEither α β
- [Produto de tipos][product-type]: α × β
- [Soma de tipos (coproduto)][sum-type]: α + β
- O que usar para representar erros em vez de gambiarras tipo Strings e Números
- pw (zipWith, zip; [veja sobre zipping][zip])
- findFirst: primeira tentativa
- uma idéia sobre como resolver nosso problema:
(⟨$⟩)
/fmap
- uma outra idéia sobre como resolver nosso problema: pattern matching: match-expression
- de volta para a primeira idéia: fmap e Functors
- [Functors][functor], fmap, deriving ( Functor )
- Leis de Functor
- Abuso de List α para assumir papel de Maybe α
- Duas interpretações computacionais dos habitantes de List α
- Functorialidade do Either ε
- Composição de funções: (∘)
- [programação tácita][tacit-programming]: point-free, point-less, …
- Como implementar os Ints usando Nats: igualdade
- Teaser sobre arvores
2022-11-23: IDMb (7,8) [video]
- seqüências são [cidadãos da primeira classe][first-class-citizen]
- cota superior/inferor dum conjunto
- infimum/supremum dum conjunto
- [coerção de tipo][type-coercion]
- duas maneiras de desenhar seqüências: uma 1-dimensional e uma 2-dimensional
- dando significado para 1 + (aₙ)ₙ e para o (aₙ)ₙ + (bₙ)ₙ
- como definir mesmo uma seqüência que desejamos
- seqüência limitada superiormente/inferiormente
- investigação: a (aₙ)ₙ é cotada?
- seqüência (estritamente) crescente/decrescente
- crescente não implica não-cotada-superiormente
- como demonstrar que uma alegada cota inferior é realmente uma cota inferior
- Conexões com IRI: listas, Empty, Unit, habitantes de
α
como habitantes doUnit → α
- a melhor cota inferior e a melhor cota superior
- unicidade de supremum e de infimum
- conjuntos sem sup/inf, e sup/inf do ℝ e do Ø
- um mal-entendido comum sobre demonstrações por vacuidade e propriedades dos membros do Ø
- Esboço para definir o conjunto dos reais-naturais
- Def: conjunto naturalmente indutivo
- o «melhor» naturalmente indutivo significa o «menor», e «menor» significa «(⊆)-menor»
- top-down: seja ℐ a coleção de todos os conjuntos indutivos, e considere sua interseção
- uns não-exemplos de indutivos
- definição dos reais-naturais $\mathbb R_{\mathbb N}$
- o que demonstrar sobre o $\mathbb R_{\mathbb N}$
- Plicker: infA ≤ supA ?
2022-11-25: IRI (14) [video]
- corretude: estipular e demonstrar propriedades dos nossos programas
- e sobre igualdade intensional entre funções
- uns tipos de arvores
- a map das listas e outras fmaps e as leis de Functor
- maneiras de escrever uso de indução é os detalhes possivelmente enganadores e implícitos
- a List com o map é um Functor: demonstração da 2a lei
- demonstração: a segunda lei de Functor para a map de List α
- Composição de Functors
- a propaganda mentirosa de «tipos dinâmicos» e a verdade decepcionante
- como funcionam linguagens de “tipos dinâmicos” e runtime errors
2022-11-28: IDMb (9) [video]
- (–)ₙ é um ligador da variável n no escopo de –
- Novamente sobre conjuntos:
- o que preciso fazer para definir/determinar um conjunto
- o que significa (=) entre conjuntos
- união e interseção de uma coleção de conjuntos de α
- Seq(Set(Real)) e Seq(Seq(Real))
- Seqüências são cidadãos da primeira classe; pointwise (∗)
- duas maneiras de definir (∗) entre um Real e um Seq(Real)
- união e interseção de uma coleção de conjuntos
- Exemplos de umas seqüências de conjuntos de reais, suas uniões e suas interseções:
- ( [0,n) )ₙ
- ( [n,n+1) )ₙ
- Como demonstrar que 1 ∈ ⋂ₙGₙ
- Desenhando os primeiros membros de seqüências de conjuntos de reais
- a união de uma seqüência decrescente ((⊇)-chain).
- Reais naturais vs naturais: type casting e type coercion
- os ⌊–⌋ e ⌈–⌉ (piso e teto)
- uma seqüência de abertos com interseção fechada e o dual: uma seqüência de fechados com união aberta
- Uma seqüência decrescente ((⊇)-chain) de intervalos abertos com interseção intervalo fechado
- Frases legais do ♡:
- para valores suficientemente grandes de
- eventualmente
- Seqüência constante: 3 candidatos para definição
- Seqüência eventualmente constante
- Mais umas gírias:
- «para valores suficientemente grande de»
- «eventualmente»
2022-11-30: IDMb (10,11) [video]
- “Escolhendo N(ε)’s”
- Tantando ficar implementação-agnósticos
- Q: «para valores suficientemente grandes de» vs «eventualmente»
- cuidado com a comparação com a notação-O (que é abusiva demais)
- (cont.)
- Q: o que significa «a igualdade não é exatmente simétrica»?
- como interpretar “igualdades” como a inf A = sup B.
- giria: «frequentemente»
- sinônimos de inf/sup: glb/lub, meet/join, ∧/∨
- Chegando na definição de limite
- O tipo de «_ tende ao _»
- Um primeiro palpite
- Duas maneiras que uma definição pode ter «erro de tradução» (de cabeça para o papel)
-
- Briga contra o primeiro palpite
- Girias que envolvem tempo/futuro com seqüências: «nunca», «sempre»
- Um segundo palpite
-
- Briga contra o primeiro palpite
- Terceiro (e último) palpite: usando «para valores suficientemente grandes de»
- Uma maneira que envolve o «eventualmente»
- Q: podemos definir o que significa «_ tende ao +∞» ?
- traduzindo de nível coração com gírias, para um nível low level e explicito
- uma métrica bem diferente nos reais: a métrica discreta
- Quantificadores, complexidade de entendimento, importância de gírias, estratégia vencedora de jogo
- Interpretação dos ∀∃ em termos jogos
- Def: «convergente»
- Θ. constante ⇒ convergente
- Q. A gente não precisou olhar no ε que o jogador ∀ escolheu
- Def: «divergente»
- Θ. eventualmente constante ⇒ convergente
-
- copycat strategy em jogos
-
- Demonstração
- Umas seqüências divergentes
- Θ. a ( (-1)ⁿ )ₙ não tende a nenhum ℓ (ela é divergente)
- Def: «autoconvergente»
- Θ. Unicidade dos limites
- Plicker: (i) cotada & crescente ⇒ convergente? (ii) autoconvergente ⇒ convergente?
2022-12-03: IRI (15,16) [video]
- Eficiência “por algebra”
- Eficiência “por indução”
- eliminando o (⧺) da
reverse
“por indução”
- eliminando o (⧺) da
- Arvores
- típos de árvores e umas funções relevantes
- size, nodes, depth, flatten, mapTree, foldTree, …
- Sintaxe vs semântica
- Numerais binários
- Um toque de expressões e ASTs
- BNF
- ArEx, ArExV
- semântica operacional
- semântica denotacional
- eval, step, bigstep
- [funções fold][fold]: fold
2022-12-07: ☠ Prova 2.3; Prova 3.1 ☠
2022-12-12: IDMb (12,13) [video]
- epsilons e como encontrá-los
- umas perguntas ainda abertas
- recap de uns teoremas demonstrados
- Θ. convergente ⇒ autoconvergente
- Θ. autoconvergente ⇒ cotada
- recap de umas proposições não demonstradas
- ?. crecente & supcotada ⇒ cotada
- ?. conjunto supcotado ⇒ possui supremum
- ?. propriedade dos intervalos aninhados
- ?. autoconvergente ⇒ convergente
- ?. cotada ⇒ subseq convergente
- a seqüência (log n)ₙ não é autoconvergente
- def: subseqüência
- [liminf e limsup][liminf-limsup]
- epsilons e «como encontrá-los»
- Θ. limₙ (aₙ+bₙ) = limₙ aₙ + limₙ bₙ
- Θ. limₙ (aₙ·bₙ) = limₙ aₙ · limₙ bₙ
- O último axioma da especificação dos reais: axioma da completude
- Preview de umas conseqüências:
- Θ. Existência de raizes
- Θ. Sistema posicional para numerais dos reais
- Θ. os reais racionais são densos nos reais
- Θ. os reais irracionais são densos nos reais
2022-12-14: IDMb (14,15) [video]
- Construções de conjuntos/tipos numéricos
- Podemos dizer que o ℝ não tem buracos?
- Igualdade para tipos; igualdade para o Seq(α)
- Seqüências com índices diferentes de naturais, seqs implementadas como funções
- lembrete: teoremas sobre o lado algébrico de limites
- o que significam igualdades que envolvem lim.
- duas notações de operadores aplicados em seqüências
- diagramas comutativos e o teorema de limites algébricos
- Dado um tipo A, o que seriam os tipos A², Aⁿ, A⁰?
- Axioma da completude dos reais: nível-♡
- Θ. sobre inf-cotada ⇒ possui ínfimo?
- Θ. Propriedades arquimedeanas
- Θ. Densidades: dos racionais e dos irracionais nos reais
- Θ. NIP: Nested Interval Property (Cantor); Θ. MCT: Monotone Convergence Theorem
- Sistemas posicionais de numerias para reais: interpretação geométrica (via NIP)
- Θ. [Bolzano–Weierstrass][bolzano-weierstrass]: cotada ⇒ possui subseq convergente
- Q: convergente ⇒ todas as subseq convergentes?
- Cauchy
- Θ. 0 < θ < 1 ⇒ (θⁿ)ₙ → 0
- Séries, somatórios parciais: uma maneira de interpretar um «somatório infinito»
- dois exemplos de séries convergentes
- um exemplo de série divergente: a séries harmônica
2022-12-15: IDMb (16,17) [video]
- (NIP) ⇒ (BW)
- Um toque de espaços métricos: como definir a diam
- Θ. raizes para reais pequenos
- Θ. √2
- O teorema de rearranjo de Riemann (e um problema com soma telescópica infinita)
- polinômios: algébricos vs transcedentais
- Algébricos vs transcedentais
- [Euler][Euler], a [constante e][number-e], [Liouville][Liouville]
- [Cantor][Cantor]: cobririndo uns subconjuntos de reais com seqüências
- Cantor: primeira demonstração que qualquer seqüência de reais
- Cantor: diagonalização
- [Borel][Borel], [Lebesgue][Lebesgue], [Kolmogorov][Kolmogorov]: um toque de teoria da medida: probabilidade de acertar um racional no [0,1] dos reais
- Integral Riemann vs Integral Lebesgue
2022-12-16: Prova 3.2
Futuro (fluido)
Sem futuro. Acabou!
Medley em um universo paralelo
- IDMa
- Universal hash
- Assinatura digital
- Um toque de álgebra abstrata
- IDMb
- Mais um toque de espaços métricos
- Mais um toque de teoria da medida e da integração
- Funções reais e seqüências de funções
- IRI
- Expressões e ASTs
- Fórmulas de Lógica Proposicional
- Funções em fórmulas
- Recursão aninhada
- Ackermann
- Recursão para contagem
- Expressões e ASTs