Horários de aula: | 246M56♭ [10h40–12h20] |
Sala: | A306 |
Contato: | thanos@imd.ufrn.br |
Playlists: | ( IntroProof | IDMa | IDMb | IRI ) |
Monitoria/TA: | fmc.imd.ufrn.br |
Turmas anteriores: | .. |
Info
Pré-requisitos
- É necessário que os alunos matriculados têm tempo e vontade para estudar, fazer os trabalhos atribuídos, etc.
(Obs.: estudar ≠ ler.)
Veja minhas dicas para estudantes, que inclui pré-requisitos para esta disciplina.
Alunos que não aprenderam o conteúdo das disciplinas de matemática do primeiro semestre e (obviamente) do ensino médio podem consultar as referências seguintes:
(Obs.: aprender ≠ passar.)
- Lang: Basic Mathematics (de uma olhada nesta playlist no YouTube que tem um curto videozinho para cada secção deste livro)
- Lima et al: A Matemática do Ensino Médio, vol I (para esta disciplina os mais relevantes pré-requisitos são os Cap. 1–4)
Conteúdo
A disciplina FMC1 será dividida em 3 módulos–unidades. Podem considerar cada tal módulo como um componente curricular independente (e sem pré-requisitos entre si). Essa divisão é influenciada pelos módulos correspondentes à FMC1 baseados nos módulos correspondentes desta proposta.
IDMa: Elementos da teoria dos números inteiros
(Lecionado 4h/semana, durante a primeira metade do semestre.)
Axiomas sobre os inteiros (domínio de integridade bem ordenado). Demonstrações de teoremas pelos axiomas, sobre as operações e as relações de ordem nos inteiros. A relação de divisibilidade e a verificação de suas principais propriedades. Teorema de Euclides sobre infinidade de primos e sua demonstração construtiva. Lema de divisão de Euclides. Números, numerais, dígitos: demonstração que qualquer inteiro $b > 1$, serve como base para um sistema posicional de numerais para inteiros. Lema de Euclides e sua generalização. Teorema Fundamental da Aritmética. mdc e mmc e demonstrações das suas propriedades Algoritmo de Euclides: corretude e terminação Algoritmo estendido de Euclides Demonstração do teorema Fundamental de Aritmética Congruência módulo um inteiro e demonstrações das suas propriedades Aritmética modular e propriedades do ℤ/mℤ. Algumas conjecturas da teoria dos números: o teorema pequeno de Fermat; a função totiente de Euler; o teorema de Euler.
IRI: Introdução à Recursão e Indução
(Lecionado 2h/semana, durante o semestre inteiro.)
Os naturais e o tipo Nat
; seus construtores (zero, sucessor) e sua teoria: implementação recursiva das suas principais operações, e verificação indutiva das suas principais propriedades. O tipo dos booleanos, Bool
. Ordens sobre os naturais: especificação e verificação de suas propriedades. Outras funções e relações, e suas propriedades. Indução como princípio e técnica de demonstração em matemática. A unicidade dos naturais (a menos de isomorfismo). List Nat
e List α
: tipos de dados de listas: implementação recursiva e verificação indutiva de suas principais propriedades. Outros tipos de dados recursivos: tipos de árvores; tipos de expressões aritméticas; tipos de fórmulas; termos de cálculo-λ. Numerais binários, definição de semântica e seu uso para verificação de corretude.
IDMb: Elementos da teoria dos números reais
(Lecionado 4h/semana, durante a segunda metade do semestre.)
Axiomas de corpo e suas consequências. Axiomas de corpo ordenado e suas consequências. Representação geométrica. Algumas noções métricas e topológicas da reta real. Subconjuntos notáveis do ℝ: N, Z, Q. Racionais e irracionais. Conjuntos cotados, cota superior, cota inferior. Ínfimo, supremo. Seqüências e seus limites. O axioma da completude. Séries.
Objetivos de aprendizagem
IRI: Introdução à Recursão e Indução
Neste módulo estudamos como definir tipos de dados, funções, e relações recursivamente, e como demonstrar propriedades sobre tais coleções de dados por indução.
Prática com o uso da linguagem matemática e das principais técnicas de demonstração e refutação. Prática com a escrita de definições por recursão e demonstrações por indução. Recursão e indução estrutural sobre tipos de dados recursivos. Apreciação de coleções potencialmente infinitas do ponto de vista implementacional, recursivo, e verificação matemática de suas propriedades de interesse. Casamento de padrões e seu uso em definições, demonstrações, e cálculos. Recursão mútua, indução aninhada. Ganhar familiaridade com inferência de tipos e evitar erros de tipagem. Notação e nomenclatura matemática e computacional. Apreciar a diferença e a conexão entre sintaxe e semântica.
IDM: Introdução à Demonstração Matemática
Nestes módulos usamos elementos da teoria dos números inteiros (IDMa) e da teoria axiomática dos números reais (IDMb) para introduzir o aluno ao pensamento matemático e o processo de definir conceitos, enunciar e demonstrar teoremas. Aproveitamos o desenvolvimento do conteúdo concreto para chegar até os seguintes conceitos fundamentais:
- congruência e aritmética modular (IDMa)
- ínfimo, supremo, sequência, limite (IDMb)
Familiarizar com a linguagem usada em definições e demonstrações matemáticas: aprender ler e escrever (usar e interpretar corretamente a linguagem matemática, sua nomenclatura e notação). Apreciar a diferença entre intensional e extensional (sobre igualdades e equivalências). Uso de (meta)variáveis em matemática; ocorrência de variável ligada vs livre; α-conversão (renomeamento); substituição de variável por termos; linguagem vs metalinguagem. Introduzir o lado computacional de uma demonstração, como sequência de comandos que alteram o estado de Dados/Alvos. Entender dois lados de matemática: intuitivo e formal. Propriedades da igualdade e seu uso no raciocínio equacional. Aprender como usar e escrever cálculos dentro de uma demonstração. Apreciar a demonstração como justificativa da veracidade de proposições matemáticas (incluindo de proposições como $p\to p$, leis de distributividade, de De Morgan, frequentemente chamadas «leis» de lógica). Aprender para cada um dos ¬,⇒,∨,∧,∃,∀: como introduzi-lo e como eliminá-lo no texto de uma demonstração. Apreciar a lógica construtiva e os usos dos princípios da lógica clássica (terceiro excluído, redução ao absurdo, dupla negação, contrapositivo); apreciar a diferença entre redução ao absurdo e demonstração direta de negação. Desenvolver definições e teorias matemáticas a partir de noções primitivas e axiomas. Familiarizar com definições e demonstrações que envolvem conjuntos, sequências, funções, e relações. Ter um primeiro contato com conjuntos estruturados e estruturas algébricas e as propriedades das suas operações. Entender como e por quê os sistemas posicionais de numerais funcionam.
Bibliografia e referências
Conhece o libgen?
Principal
- Eu: Matemática fundacional para computação [fmcbook] (Capítulos 1–6)
IRI: Introdução à 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
Veja minha página de dicas para estudantes.
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.
- A linguagem de programação funcional e proof assistant Agda 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.
O módulo IRI será auxiliado pelo uso da linguagem de programação funcional Haskell e/ou Agda, e pelo proof assistant Lean e/ou Agda. Usando uma linguagem de programação funcional é imediato implementar todas as suas definições para rodá-las no computador. Usando um proof assistant, formalizamos tanto as definições recursivas, quanto as demonstrações indutivas usando a mesma linguagem. (Mas o foco continua sendo o papel; não o computador!)
O módulo IDMa será auxiliado pelo uso do proof assistant Lean e Agda.
O módulo IDMb não será auxiliado por nenhum proof assistant. Ficará só no papel mesmo. (Dependendo do progresso no início do semestre, isso pode mudar.)
Regras
- Nunca escreva ou diga algo que você mesmo não sabe explicar: (i) o que significa; (ii) seu papel na tua resolução. Por exemplo: um aluno escreveu a frase seguinte na sua demonstração: «Como f é cancelável pela esquerda temos que g=h». Ele deve saber o que significa ser cancelável pela esquerda e também explicar como isso foi usado e/ou o que isso tem a ver com essa parte da sua demonstração.
- Qualquer trabalho ou resposta dada poderá ser questionado em forma de prova oral, em modo privado ou aberto. Se um aluno não consegue explicar o que ele mesmo escreveu numa resolução, será considerado plágio (veja abaixo).
- Participando, nunca dê uma resposta que tu não pensou sozinho, exceto dando os devidos créditos correspodentes.
- Não tente “forçar a barra” perguntando ou respondendo coisas aleatórias com objetivo de ganhar pontos. Os pontos de participação não correspondem em apenas perguntas ou dúvidas que mostram interesse. O interesse é implícito pelo fato que tu escolheu matricular nesta turma—não vale pontos.
- Não procurem resoluções em qualquer lugar fora dos indicados em cada homework. O único recurso automaticamente aceitável para procurar ajuda é no nosso Zulip (especificamente seus canáis públicos—não DM) e a monitoria.
- 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 este site e o Zulip da disciplina pelo menos uma vez por dia durante o semestre. (Qualquer coisa postada no site ou no Zulip da disciplina será considerada como conhecida por todos os alunos da turma.)
- 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 atendimento para tirar dúvidas.
(Veja também os FAQs relevantes.)
Sobre plágio
- Plágio detectado implica que o aluno será reprovado na disciplina 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 e nas brigas (nas aulas, no Zulip, e na monitoria).
Avaliação
A nota final de cada aluno vai ser principalmente baseada em um ou mais dos: (i) provas escritas; (ii) sua participação; (iii) trabalhos atribuidos; (iv) hw resolvidos (veja o FAQ relevante).
Cada aluno será responsável para manter organizado e bem escrito o seu caderno com todos os teoremas e exercícios que estudou durante a disciplina.
Presenças e faltas
A presença pela regulação da UFRN é obrigatória. Os alunos que não gostam/querem/podem aparecer nas minhas aulas ainda têm chances de ganhar até nota máxima e aprovar na disciplina. Ou seja: alunos que escolhem não participar ou aparecer nas aulas, e mesmo assim aparecem nas provas escritas e conseguem nota final de aprovação vão ter sua porcentagem de faltas ajustada para não reprovar por faltas. Esclarecimento: alunos que não conseguem nota final de aprovação não terão sua porcentagem de presença ajustada de jeito nenhum e por nenhum motivo.
Obviamente, alunos que não aparecem nas aulas não terão como ganhar pontos de participação em aula—duh!—nem pontos de possíveis provas-surpresas.
As presenças/faltas serão cadastradas usando o sistema Plickers (veja o FAQ relevante).
Atrasados
Definição (atrasado). Seja $a$ aluno desta turma. Dizemos que $a$ é atrasado sse $a$ não está já sentado na sua mesa, com seu caderno já aberto, seu celular já desligado e na mochila, no momento que a aula começa.
Tentem estar presentes na sala da aula ANTES do horário do seu começo, e fiquem até o fim da aula.
Caso que alguém chega atrasado: não faz sentido bater na porta da sala de aula; não faz sentido cumprimentar nem o professor (não é mostra educação cumprimentar nesse caso—pelo contrário!) nem os amigos/colegas da aula. Entrando numa sala onde a aula já começou, tentem fazer sua entrada o menos possível notada por os participantes pois atrapalha a concentração de todos.
FAQs
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.
Provas não-surpresa. Tais provas serão avisadas com curtíssima antecedência (de pelo menos 16h). A melhor maneira de lidar com isso é tratar todo dia de aula como possível dia de prova.
U1 (IDMa)
- Prova IDMa.1 / 24pts (2023-09-15) { censored , uncensored , answers , correções }
- Prova IDMa.2 / 64pts (2023-11-17)
{
censored, uncensored ,answers, correções } - Prova IDMa.3 / 12pts { logic.lean }
U2 (IRI)
- Prova IRI.1 / 24pts (2023-09-15) { censored , uncensored , answers , correções }
- Prova IRI.2 / 10pts
- Prova IRI.3 / 66pts (2023-12-18) { censored , uncensored , answers , correções }
U3 (IDMb)
- Prova IDMb.1 / 24pts (2023-12-08) { censored , uncensored , answers , correções }
- Prova IDMb.2 / 76pts (2023-12-18) { 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.
2023-08-17: IntroProof
- Capítulo 1
2023-08-21: IntroProof
- 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.
- Complete o «Tutorial World» do Natural Number Game. Veja o FAQ relevante também. Salve este progresso no teu github.
- Capítulo 2: até o primeiro intervalo de problemas
- Para cada uma das proposições seguintes 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:
- Instale no seu computador: Lean, Haskell, Agda
2023-08-27: IntroProof
- Infira a simetria e a transitividade da igualdade a partir das reflexividade e substituição.
- Capítulo 2: inteiro
2023-08-28: IDMa
- Capítulo 3: até o Exercício x3.6
2023-09-02: IRI
- Jogue o NNG. Tente completar o mais rápido possivel; sua entregá pode acabar sendo a Prova 2.2. Veja o FAQ relevante também.
- Defina (sem consulta) a adição, a multiplicação, e a exponenciação.
- Defina uma função
double
que retorna o dobro da sua entrada. - Calcule os:
double (double (S O))
double ((S O) + (S (S O)))
- Demonstre uma das: (·)-idL, (·)-idR
- Demonstre uma das: (^)-idL, (^)-idR
- Defina a função
pred : 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 e de 2022.2 usou apred
em outras definições, estava errando - Defina as funções:
fact : Nat → Nat
fib : 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
2023-09-04: IDMa
- Capítulo 3: até Θ3.13
2023-09-09: IDMa
- Capítulo 3: até x3.14
2023-09-09: IRI
- Capítulo 4: até o §«Demonstrando propriedades de naturais com indução»
2023-09-11: IDMa
- Capítulo 3: até §«Divisibilidade»
2023-09-11: IRI
- Capítulo 4: até o §«Ordem nos naturais»
2023-09-12: IntroProof
- Demonstre os teoremas do hw 2023-08-21 (e mais!) 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! ntroProof
2023-09-13: 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 )
2023-09-18: IDMa
- Capítulo 3: até §«Ordem e positividade»
2023-09-20: IRI
- Capítulo 4: até o §«Empty»
- Defina os operadores booleanos.
- Como definarias uma função
if_then_else_ : Bool → Nat → Nat → Nat
? - Defina e demonstre a corretude das funções:
leq : Nat → Nat → Bool
ev : Nat → Bool
od : Nat → Bool
isMul₃ : Nat → Bool
divides : Nat → Nat → Bool
isZero : Nat → Bool
- Demonstre que a
leq : Nat → Nat → Prop
é: reflexiva; transitiva; antissimétrica; total - Demonstre que todo Nat é par ou ímpar.
2023-09-23: IDMa
- Capítulo 3: até o primeiro intervalo de problemas.
2023-09-25: 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$.
- Demonstre que um conjunto vazio é subconjunto de qualquer conjunto.
- Demonstre ou refute: «o Ø é bem-ordenado».
- Demonstre ou refute: «qualquer conjunto de inteiros X finito é bem ordenado».
- Demonstre como teorema o princípio de indução.
- Demonstre como corolário o princípio de indução “shiftado” (i.e., a partir dum inteiro ℓ)
- Demonstre como corolário o princípio de indução com 2 bases.
- Enuncie e demonstre um princípio de indução “flippado”, para demonstrar que todo inteiro negativo “é legal”
2023-09-28: IRI
- 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. - Implemente como Nats:
- os inteiros (já sabes a sua especificação pelo IDMa!)
- os parzinhos-de-Nats
- os 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
2023-10-04: IRI
- Enuncie (sem olhar) como regras de inferência os princípios de indução para os:
ListNat
,Nat
,Bool
,Unit
,Empty
. - 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!
- (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)] ⇒ ψ
2023-10-09: IDMa
-
Π5.9; Π5.17
-
Na aula definimos na Maneira Certa™ o que significa ser um mdc dos a,b. Para isso, se baseamos na pré-ordem (|). Traduza o mesmo conceito para as ordens seguintes:
(≤)
no mundo dos inteiros(⊆)
no mundo dosSet α
-
Resolva a Prova 2.X do 2019.2.
2023-10-13: 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 α
2023-10-13: IDMa
- Demonstre a corretude do algoritmo de Euclides para achar o m.d.c. (use a versão com os restos).
2023-10-16: IDMa
- Resolva (finalmente) o 2023-10-09.hw2, junto com a nova questão sobre o (⊢): traduza o “m.d.c.” para…
- o mundo dos inteiros, com a pré-ordem (≤)
- o mundo dos
Set α
, com a pré-ordem (⊆) - o mundo das Props, com a pré-ordem (⊢)
- Desafio: ache qual seria «o pesadelo de Euclides», ou seja, entradas para o algoritmo de m.d.c. dele onde precisaria a maior quantidade de passos possível. Observe que, na verdade, continua sendo nada-de-pesadelo mesmo, até nesse caso!
- Implemente o algoritmo de euclides em Haskell, incluindo sua versão estendida com tipo
Int × Int → Int × Int × Int
. - Calcule na mão o mdc para uns números, e ache seus coeficientes Bézout. Compare com a método da «criança do Ensino Fundamental BR»:
- 10668127, 159451
- 252121, 318719
- Para cada uma das equações, ache x, y que a satisfazem:
- 1 = 127x + 73y
- 6 = 321x + 312y
2023-10-18: IDMa
- Capítulo 3: até a «§57. Invertíveis, units, sócios»
2023-10-23: IDMa
- Encontre x com |x| < 50 tal que 6¹⁵⁴⁰ ≡₅₀ x; faça todas as contas na mão—confie, pois se acabar sendo difícil, tá fazendo algo errado!
- Capítulo 3: até a «§70. Exponenciação»
- $a$ invertível módulo $m$ sse (a,m) = 1.
- Unicidade de inversos módulo $m$.
- Mostre que (≡ₘ) é uma congruência para a estrutura algébrica dos inteiros
- Mostre que a (≡ₘ) não é compatível com a exponenciação.
- 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$?
- (qm + r, m) = (r,m)
- (a,nm) = 1 ⇔ (a,m) = 1 & (a,n) = 1
2023-10-26: IDMa
- 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).
2023-10-26: IRI
- 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
2023-10-30: IDMa
- Demonstre o teorema de Wilson
- Demonstre que para todo inteiro
m
, se o testeq
-Fermat diz não, então pelo menos metade dos{1,…,m}
-Fermat dizem não também - 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 ]
- (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).
- Calcule de novo, essa vez todos os φ(2), φ(3), φ(4), …, φ(13). (Não se engane: fatoraçã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é?
2023-11-10: IDMb
- Capítulo 6: até o §«Ordem e positividade»
2023-11-15: IDMa
- Capítulo 3: até o fim.
2023-11-15: IDMb
- Capítulo 6: até o §«Valor absoluto»
- Os números seguintes são algébricos?:
- $\sqrt 2 + \sqrt 3$;
- $\sqrt[3] 2 + \sqrt 3$;
- $\sqrt {2 + \sqrt 3}$;
- $\varphi \quad (= \dfrac {1 + \sqrt 5} 2)$.
2023-11-20: IDMb
- Capítulo 6: até o §«Mínima e máxima»
2023-11-22: IRI
- Investigue para cada um dos seguintes se pode ser munido com um
fmap
para conseguir ser um Functor:(δ →) : Type → Type
(→ γ) : Type → Type
(α ×) : Type → Type
(× β) : Type → Type
(α +) : Type → Type
(+ β) : Type → Type
Id : Type → Type
K κ : Type → Type
- Investigue: composição de functors é functor?
2023-11-24: IDMb
- Capítulo 6: até o §«Sobre modelos»
2023-11-24: IDMb
- Capítulo 6: até o §«Infimum e supremum» (obs: re-restude o §«Distância» pois atualizei).
2023-12-04: IRI
- Resolva a Prova 2.3 do self/iri.
- Capítulo 4:
- §106 «Functors»
- §107 «Arvores»
- §109 «Um toque de complexidade»
- §110 «Eficiência via indução»
- Arvores
- Defina as:
tips : BinTree α → Nat
forks : BinTree α → Nat
depth : BinTree α → Nat
leaves : BinTree α → List α
mapTree : ?
mirror : BinTree α → BinTree α
flatten : BinTree α → List α
findTree : α → GenTree α → 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! - Θ.
depth ≤ length ∘ flatten
(← o que significa isso?) - Θ.
forks t ≤ 2 ^ depth 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!)
- LabBinTree α β
- GenTree α
- 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 = ??
fmap f ∘ flatten = ??
- 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
2023-12-04: IDMb
- Resolva a Prova 3.1 do self/idmb.
- Θ. eventualmente convergente ⇔ convergente
2023-12-11: IRI
- 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
2023-12-11: IDMb
- ainda com v2/3
- 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.
- Resolva sozinho os teoremas seguintes que demonstramos na aula passada:
- Reais (oficiais) (v3/3), com completude via cotado:
sup-cotado ⇒ sup
- «Agora sim!» Demonstre os: Nested Interval Property de Cantor; Monotone Convergence Theorem; Bolzano–Weierstrass Theorem; 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:
- Αρχιμήδης:
- Θ. Os reais naturais não são cotados
- Θ. (∀ε>0)(∃n)[ 1/n < ε ]
- Θ. (∀ε>0)(∃n)[ nε > 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?
- Θ. «Ἵππασος 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
- «Agora sim!» Demonstre os: Nested Interval Property de Cantor; Monotone Convergence Theorem; Bolzano–Weierstrass Theorem; Cauchy convergence critérion
2023-12-18: IDMb
- Criar seu próprio gabarito para a Prova 3.2
2023-12-18: IRI
- Criar seu próprio gabarito para a Prova 2.3
- O que precisa mudar para a linguagem
ArEx
saber lidar com expressões envolvendo variáveis como a3(x₂ + 2x₀) + 4x₂x₇
, e naseval
estep
? - O que significaria a equação do ensino fundametal
2a = a + a
para sistea de típos que temos? Ela é válida? Como verificar isso?
Histórico
2023-08-16: Meta & IntroProof (1)
- Overview
- tipos e type errors
- proposiões vs objetos
- Prop vs Bool
- juízos (judgements) vs proposições
- comandos vs proposições
- Os construtores de tipos (→) e (×)
2023-08-19: IntroProof (2)
- 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
- os ¬,⇒,⇔,&,ou,∀,∃,=
2023-08-21: IntroProof (3)
- os ⇒,&,ou,∀,∃,=,⊥ como primitivos
- os ⇔,¬,⇐ como açúcar sintáctico
- (⇒): como usar
- (ou): como usar
- (⊥): como usar e como atacar
- contra o poeminha: «não podes supor seu próprio alvo»
- variáveis frescas e nomes bons
- ocorrência de variável ligada e livre
2023-08-23: IntroProof (4)
- conexões entre ataques/usos de disjunção/conjunção e usos/ataques de conjunção/disjunção
- conexões entre disjunção/conjunção e quantificação existencial/universal
- conexões entre implicação e quantificação universal
- o «xou»
- o resto dos conectivos para nossa linguagem de demonstrações
2023-08-25: IntroProof (5)
- igualdade
- introdução e eliminação
- a linguagem low-level
- umas “leis de lógica” e como demonstrá-las
- magias ⛤
- a briga Brouwer vs Hilbert
2023-08-28: IDMa (1)
- especificação vs implementação
- especificação dos inteiros (1/5)
2023-08-30: IDMa (2)
- cálculos em demonstrações
2023-09-01: IRI (1)
- 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
- o tipo Nat: espectativas e 4 maneiras de definir um tipo de dados recursivamente
- «Nada mais»
- sintaxe: o que queremos descrever
- o desafio dos «…» numa definição
- Naturais vs Nats; Números vs Numerais
- 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
- Um exemplo de inferência:
SSSSO : Nat
- casamento de padrões
- Mal entendido: «os inteiros que a gente conheceu»—Nope.
- Definição recursiva vs tijolo
- construtor vs função
- A adiçaõ: (+)
- Um cálculo e teorema: 2 + 3 ≟ 5
- A multiplicação: (·)
- Um cálculo e teorema: 2 · 3 ≟ 6
- Arvore sintáctica (Abstract Syntax Tree), parsing, (veja também: lexer)
- A disjunção escondida em cada Nat
- tentativa de demonstrar (+)-idL e o problema que temos
2023-09-04: IDMa (3)
- Especificação e modelos
- O conjunto dos strings não é um modelo da especificação dos inteiros
- como justificar o «somar nos dois lados o mesmo inteiro (pelo mesmo lado)»
- aplicação de função nos dois lados de uma igualdade
- notação λ e notação ↦
- notação com buracos
- o
(∃!x)[φ(x)]
definido como conjunção - uma alternativa para demonstrar unicidade tendo já um testemunha da existência
- Θ. unicidade da (+)-identidade
2023-09-06: IntroProof (6) ; IDMa (4)
- Currificação
- aplicação: uma operação invisivelmente escrita e sua associatividade sintáctica
- uns preconceitos sobre funções e sua notação
- aridades de funções: significado e duas maneiras de entender o slogan «todas as funções recebem só um argumento»
- Relaxe:
Imediato.
eSplit.
- Resoluções únicas
- Demonstração com dependências vs sem dependências
2023-09-08: IRI (2)
- Formato geral do tipo dum construtor
- Constantes como funções
- Indução
- Demonstração da associatividade da (+)
2023-09-11: IDMa (5)
- Anulador nos inteiros
- Cancelamento multiplicativo
- (Z-NZD)
- Igualdade não é simétrica (♡)
- Dica sobre como enxergar alvos
- Aproveitando unicidades de protagonistas e de resoluções
- A utilidade de lemmas sobre unicidade de resolução de equações num incógnito
- Exemplos: (∀a)[(-1)a = -a]; (∀a)[0a = a]
2023-09-13: IRI (3)
2023-09-15: Prova IDMa.1 & Prova IRI.1
2023-09-18: IDMa (6)
- Umas propriedades ordem-teóricas da relação de divide
- Conjuntos e sua notação, incluindo o set builder
Set : Type → Type
- O que significa saber qual é um conjunto
- Conjuntos fechados sob operações
- Θ. mℤ é (+)-fechado
- Positividade e ordem, e sua “equivalência”
- Especificação de inteiros v3/5: Pos & seus axiomas
- Θ. (∀a ≠ 0)[ a² positivo ]
- Θ. 1 é positivo
- Especificação de inteiros v4/5: 0 ≠ 1
2023-09-20: IRI (4)
- Sobre os princípios dos construtores de cada tipo
- abuso de tipo existente para implementar outro vs definição de novo tipo
- Novos tipos: Bool, Day, Unit, Empty, Ordering
- convenção Haskellosa:
_
como padrão anônimo - convenção Haskellosa: ordem das equações numa definição
- 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
- 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
2023-09-22: IDMa (7)
- Como demonstrar a indemonstrabilidade de proposições
- mundos e modelos
- A indemonstrabilidade do 0 ≠ 1
- minima e maxima
- unicidade de mínimo de conjunto
- valor absoluto
2023-09-25: IDMa (8)
- Propriedades algébricas dos (∧),(∨) (min₂ e max₂)
- Especificação de inteiros v.5/5
- Uns predicados sobre conjuntos e sua notação
- Conjuntos habitados
- Conjuntos bem ordenados
- O princípio da boa ordem (PBO)
- Como usar o PBO na prática
- Θ. Não há inteiros entre 0 e 1
- Θ. “Princípio” da Indução para os inteiros positivos
- “hackeando” os princípios da boa ordem a da indução para obter variações como corolários
2023-09-27: IRI (5)
- o mónus (∸)
- Mais sobre pattern-matching (
match-with
/case-of
) - Boolean blindness
- if-then-else expressions vs statements
PairNat
e suas projeções- wrapping de tipo existente em vez de abusá-lo
- Novo tipo:
ListNat
- Os construtores
Empty
(ouNil
) eCons
- ListNat: sintaxe, açúcar e associatividade sintáctica
- definindo funções por recursão em argumento de tipo
ListNat
length : ListNat → Nat
sum : ListNat → Nat
- como escolher o valor certo para o
sum []
e oproduct []
- concatenação binária
(⧺)
- ListNat é um tipo recursivo
- Como representar a lista [2,0,8] com nosso tipo
- Plicker: quantos construtores preciso para definir o tipo Int?
2023-09-29: IDMa (9)
- Versões de PBO
- Versões de Indução
- Wishlist
2023-10-02: IDMa (10)
- Mais sobre o wishlist:
- induções
- mdc
- fatoração única
- a,b coprime ⇒ (∀x)(∃u,v)[ x = au + bv ]
- divisão euclideana (& size)
- sistema posicional de cada base b ≥ 2
2023-10-04: IRI (6)
- A
div : Nat × Nat → Nat × Nat
let…in…
- como escolher qual argumento analisar numa definição recursiva
- O princípio da Indução para tipos indutivos (recursivamente definidos)
- Quantos quantificadores e por quê?
- Quantas implicações e por quê?
- Quantas bases e porquê?
- Quantos casos e porquê?
- «Os construtores preservam a φ»
- Indução do
Nat
(novamente) - Indução do
ListNat
- Indução do
Bool
2023-10-06: IRI (7) ; IDMa (10⁺)
- Tipos polimórficos
- List α
- Recursão e indução: dois lados da mesma moeda: mais que um “catchy motto”
- Uma maneira mais elegante para organizar uma demonstração indutiva
- Combinações e coeficientes de binomial: o teorema binomial
2023-10-09: IDMa (11)
- O que é um m.d.c. mesmo?
- Diagramas Hasse
- Uma situação impossívei de acontecer “na vida real”
- O recíproco dum teorema sobre o mℤ ser
(+)
-fechado e(_-_)
-fechado
2023-10-11: IRI (8) ; IDMa (11⁺)
IRI (8)
- polimorfismo: função(ões)
id
- Desafio: defina funções diferentes para o tipos
α → α
; mesma coisa para o tipo(α × β) → α
; mesma coisa para o tipoα → β
. - a função map:
map : (α → β) → List α → List β
- a função 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}$.
- por que não podemos tipar a sum com List α → α?
IDMa (11⁺)
- Θ. existência de m.d.c. (via coeficientes/Lemma de Bézout)
- O algoritmo de Euclides para achar um m.d.c.
- Uma maneira para demonstrar que mdc(a,b) = mdc(c,d)
2023-10-16: IDMa (12)
- Θ. existência de m.d.c. (via Euclides)
- O algoritmo (estendido) de Euclides: como achar os coefs de Bézout e o mdc simultaneamente
- Θ. Lemma de Euclides: p irredutível ⇒ p primo
- Θ. Teorema de Euclides: há uma infinidade de primos
2023-10-18: IRI (9) ; IDMa (12⁺)
IRI (9)
- Sobre destrutores
- Tipos e funções polimórficas
- Tipos dependentes e argumentos implícitos
- gambiarras no caminho para uma
safeHead
legal - a doença de Booleanismo / Boolean blindness (metáfora com correios)
Maybe α
- a fmap do Maybe:
fmap : (α → β) → (Maybe α → Maybe β)
IDMa (12⁺)
- Densidade de primos nos inteiros
- Θ. Para todo n, existem n consecutivos inteiros redutíveis
- Θ. Para todo n, existe primo entre n e n!+?
- Umas conjecturas da teoria dos números
- Conjectura dos prímos gêmeos
- Conjectura Collatz (3n+1)
- Conjectura Goldbach
2023-10-20: IDMa (13)
- Teaser sobre (ir)racionais e o √2
- L. n² par ⇔ n par
- Planetas 0, 1, 2, …
- Aritmética modular
- Congruência módulo um inteiro
- (≡ₘ) é uma relação de equivalência
- O planeta 0 é a terra!
- O planeta 1 é o {🙂}
2023-10-23: IDMa (14)
- D. compatibilidade com estrutura algébrica (com operação n-ária)
- D. congruência
- Θ. (≡ₘ) é uma congruência
- invertibilidade ⇒ cancelamento (sempre)
- Θ. (·)-invertibilidade módulo m
- Θ. (+)-cancelamento módulo m
- Θ. unicidade de inversos módulo m
- performando cálculos de aritmética modular em maneira eficiente
- exponenciação
- 106¹⁵⁴⁰ ≡ₘ ?
2023-10-25: IRI (10) ; IDMa (14⁺)
IDMa (14⁺)
- Critéria de divisibilidade
- Resolvendo congruências com incógnitos
- Eficiência de Euclides
IRI (11¯)
- Composição de funções
- Θ. Associatividade da (∘)
- programação tácita: point-free, point-less, …
2023-10-27: IDMa (15)
- Classes de equivalência, classes de congruência
- representante de classe
- notação [a]ₘ
- O conjunto quociente ℤ/(≡ₘ) ou ℤ/mℤ
- Exemplo: ℤ/4ℤ = { 4ℤ, 4ℤ + 1, 4ℤ + 2, 4ℤ + 3 }
- Os casos extremos:
- ℤ/0ℤ = { {x} | x ∈ ℤ }
- ℤ/1ℤ = { ℤ }
- Sistema completo de resíduos
- Θ. Resolução de sistema de congruências $\left\{\, x \cong_{m_i} b_i\right.$
- Θ. O sonho do calouro
- Lemma:
(∀ 1 < i < p)[ p | C(p,i) ]
- Analise Combinatória done right™
- Princípio de Adição
- Definição recursiva de C(n,r), a partir do princípio da adição
- O possível perigo da
C(n,r) = n! / (r! (n-r)!)
- Demonstração de divisibilidade via análise combinatória
- Sobre eficiências:
- fatoração
- divisão
- m.d.c.
- coeficientes Bézout
- inverso módulo m
- exponenciação módulo m
- primalidade
- Θ. Wilson: p primo ⇔ …
- Θ. Fermatinho: p primo ⇒ …
- O converso quase, mas não: enganadores de Fermat
2023-10-30: IDMa (16)
- Critéria de primalidade
- A hipotese (errada) “chinesa”
- Enganadores do Fermatinho: Carmichael
- Teste de primalidade de Fermat
- Se tem ilegais, pelo menos a metade é ilegal
- Densidade de primos e a probabilidade dum número arbitrariamente gerado ser primo
- Como gerar primos
- Sistemas de resíduos módulo m: completos e reduzidos
- A função totiente de Euler
2023-11-01: IRI (11)
- Functors e suas leis
- Eficiência via álgebra de programação
- O tipo
NatOrBool
- Duas maneiras de definir a
firstNat : NatOrBool → Maybe Nat
- Soma de tipos: α + β
- Implementando a (+) de tipos:
data Sum : α → β → Type
2023-11-03: IDMa (17)
- propriedades de s.r.r. e de s.c.r.
- Θ. aR ≡ₘ R
- Esboço de Θ: φ é multiplicativa (m,n coprimos ⇒ φ(mn) = (φm)(φn))
- Esboço de Θ: φ(pᵃ) = pᵃ - pᵃ⁻¹
- Θ (Euler): $\text{$a,m$ coprimos} \implies a^{(\varphi m)} \equiv_m 1$
- Criptografia vs Steganografia
- Criptosistema de Cæsar, rot13
- One-time pad
2023-11-06: IDMa (17⁺)
- en/decrypt vs en/decode
- números e primos ilegais
- O sistema criptográfico RSA
2023-11-08: IDMa → IRI (12) → IDMb (1⁻)
- Implementação dos inteiros
- Como conjuntos de Nat × Nat
- Como Nat × Nat
- (ℕ×ℕ)/(≅)
- Construção dos racionais
- Smart constructors
- Encapsulamento usando módulos: expor/esconder
2023-11-10: IDMb (1)
- Existem “números” fora dos racionais
- Um lemma útil
- √n “existe”?
- √n é (ir)racional?
- Abstraindo de demonstraçãozinhas para demonstração geral
- D. pedriano
- Θ.
(∀ℓ perdiano > 1)[ √ℓ é irracional ]
- Especificação dos reais, versões 1 & 2
2023-11-13: IDMb (2)
- Valor absoluto
- a indemonstrabilidade da existência do √2
- Números algébricos e transcendentais
- ${\mathbb N}\not\subseteq{\mathbb Z}\not\subseteq{\mathbb Q}\not\subseteq\mathbb R\not\subseteq\mathbb C$
- Uns subconjuntos interessantes de ℝ: $\mathbb R_{\mathbb N}\subseteq\mathbb R_{\mathbb Z}\subseteq\mathbb R_{\mathbb Q}\subseteq\mathbb R_{\mathbb A} (= \mathbb A)\subseteq \mathbb R$
- K[x]: ℤ[x], ℚ[x], ℝ[x]
- Polinômios vs funções
- para todo ε > 0 …
2023-11-17: Prova IDMa.2; IDMb (3⁻)
- O desafio de definir os reais naturais $\mathbb R_{\mathbb N}$
- O tipo $\mathsf{Seq}(\alpha)$
- Generalizando as (∪) e (∩) para os casos finitos
2023-11-20: IDMb (3)
- De operações binárias para arbitrárias
- ⋃ e ⋂
- min e max
- Especifiação de distância para um tipo α
- Distâncias para os reais
2023-11-22: IRI (13)
- Demonstração da 2a lei de functor para a $\mathit{map}_{\mathsf{List}}$
- Correspondência entre demonstração por indução e definição com
match…with…
- Casos: patterns vs Props
- Indução em mais que um objeto
- Uns candidatos para ser functors:
Id
,Const κ
- Uma gambiarra para considerar tipos como possíveis functors
- Composição de functors
- maps gratuitas e automáticas
- Análise da complexidade da
reverse : List α → List α
2023-11-24: IRI (13⁺); IDMb (5⁻)
IRI (13⁺)
- Dica sobre o hw de functors: o map para o (δ→) é a $(\circ)_{\delta\to\alpha\to\beta}$
- Eficiência via indução: uma
reverse
de O(n) em vez de O(n²)
IDMb (5⁻)
- Definição dos reais naturais e o princípio da indução para o $\mathbb R_{\mathbb N}$
2023-11-27: IDMb (5)
- intervalos e o conjunto ordenado $\overline {\mathbb R}$ dos reais estendidos
- seqüências (estritamente) crescentes e decrescentes
- dicionário de gírias sobre distâncias: ε-perto, ε-bola
- cotas superiores e inferiores
- melhor cota superior (sup, lub); melhor cota inferior (inf, glb)
2023-11-29: IRI (14)
- product types
- sum types
- a propaganda mentirosa de «tipos dinâmicos» e a verdade decepcionante
- como funcionam linguagens de “tipos dinâmicos” e runtime errors
2023-12-01: IRI (15) ; IDMb (6⁻)
IRI (15)
- tipos de arvores
- o princípio da indução para arvores
- D.
tips
,forks
,depth
- Θ.
tips t = 1 + nodes t
- Θ.
tips t ≤ 2 ^ depth t
IDMb (6⁻)
- operações e relações pointwise para seqüências
2023-12-04: IDMb (6)
- duas interpretações de
u · (aₙ)ₙ
- gírias e vocabulário sobre seqüências
- D. limite, convergente
- Θ. constante ⇒ convergente
- Θ. eventualmente constante ⇒ convergente
- D. autoconvergente
2023-12-06: IDMb (7)
- D. diverge ao +∞
- Θ. unicidade de limites
- Θ. event conv ⇔ conv
- Θ. const ⇒ conv
- Θ. event const ⇒ conv
- Θ. diverge ao +∞ ⇒ divergente
- Θ. 0,1,0,1,… diverge
- Θ. event conv ⇔ conv
- Θ. event const ⇒ cotada
- Θ. conv ⇒ cotada
- diagramas comutativos: limites comutam com (+)
2023-12-08: IRI (16⁻); IDMb (7⁺); Prova IDMb.1
IRI (16⁻)
- funções fold: foldl e foldr de List α, fold de Nat
IDMb (7⁺)
- limites e a estrutura algébrica dos reais
- Θ. (aₙ)ₙ⊕(bₙ)ₙ → a + b
2023-12-11: IDMb (8)
- limites e a estrutura algébrica
- continuidade de funções
- composição respeita continuidade
- Especificação dos Reais (v3/3)
- Umas proposições equivalentes na da v2/3
- Θ. Compl-autoconv
- Θ. Compl-cotados
- Θ. Intervalos-aninhados
- Θ. Cotada ⇒ subseq conv
- Θ. sup-cotada & crescente ⇒ conv
- interpretação geométrica dos reais e sua expansão em base n-ária
2023-12-13: IRI (16)
- sorting
- divide and conquer
- merge sort
- quicksort
- corretude e eficiência
- um teaser sobre tipos dependentes
- seu uso em programação
- seu uso em demonstrações e a idéia de «propositions-as-types»
2023-12-15: IDMb (9)
2023-12-18: Prova IRI.2 ; Prova IDMb.2
2023-12-20: Prova IRI.rep
2023-12-22: Prova IDMb.rep
Futuro (fluido)
Sem futuro! Este semestre acabou!