Horários: |
246T34 [14h55–16h35] @ B203 246N12 [18h45–20h25] @ A308 |
Sala do prof: | A225 |
Contato: | thanos@imd.ufrn.br |
Aulas gravadas: | 2019.1; 2018.2 |
Study group: | Telegram, atraves de link disponível em notícia do SIGAA [regras] |
Monitoria/TA: | fmc.imd.ufrn.br |
Horário de atendimento: | mande email para marcar (tente primeiro discutir tua dúvida no study group, e na monitoria) |
Turmas anteriores: | .. |
Prerequisitos
É prerequisito ter aprendido bem o conteudo transversal de FMC1. Sem aprender esses assuntos primeiro, não faz sentido se matricular em FMC2. (Obs.: aprender ≠ passar.)
Então—ANTES de começar—é bom estudar os:
- Do fmcbook os capítulos:
- Linguagens
- Demonstrações
- Os números naturais: recusão; indução
- Combinatória enumerativa
- Teoria elementar de números
- Congrüências
- How to prove it, de (1, 2, 3)
- Mathematical Proofs, de (0, 2)
- Comments on style de .
- A parte “Writing mathematics” do livro The tools of mathematical reasoning, de .
(Obs.: estudar ≠ ler.)
Conteúdo
- Conteúdo transversal (durante todas as unidades)
- Lógica proposicional e de predicados (linguagem; sintaxe e semântica). Definições e provas. Demonstrações diretas e indiretas, refutações. Definições por recursão – provas por indução. A linguagem de conjuntos, funções, e relações.
- Linguagem; Lógica; Recursão; Indução (U0)
- Crash course!
- Conjuntos, Funções, e Relações (U1)
- Conjuntos, sua notação, suas operações, e seus leis. Uniões disjuntas, famílias e partições. Tuplas ordenadas e produto cartesiano. As operações unitárias de união e interseção. As relações de subconjunto, e de pertencer. Multiconjuntos e sequências. Funções, o conceito de função e suas propriedades. Intensão x extensão. Domínio, codomínio. Imagem, pre-imagem. Funções totais e parciais, injetivas, sobrejetivas, bijetivas. Aridade. Função constante, função identidade, projeções, funções características. Funções recursivas; recursão mutual. Funções de ordem superior. A notação de λ-calculus. Funções x predicados. Relações e suas propriedades. Relações de equivalência, clásses de equivalência. Operações em relações, inversão, composição, fechos.
- Elementos de Álgebra abstrata (U2)
- Conjuntos com estrutura. Operações. Teoria dos grupos. Demonstrações com o uso de identidades algébricas. Homomorfísmos. Outras estruturas: aneis, monoides, reticulados. Álgebras booleanas.
- Elementos de Teoria de Conjuntos (U3)
- Enumerações e conceito intuitivo de cardinalidade. Paradoxos e os axiomas Zermelo–Fraenkel. Representações de matemática (traduções). Os números naturais; axiomas Peano.
- Elementos de Teoria de Ordem (U3)
- Ordens parciais, totais, densas, bem-fundadas. Diagramas de Hasse. Elementos notáveis (majorantes, máximos, supremos). Conjuntos ordenados, reticulados, reticulados completos. Construções de conjutos ordenados. Dualidade. Ordens canônicas, ordens lexicográficas. Monotonicidade. Teoremas de ponto fixo. Conjuntos bem-ordenados.
- Aplicações e assuntos auxiliares
- Relações bem-fundadas e indução transfinita. Números ordinais. Limites de computação. Noções de decidibilidade e de semi-decidibilidade. λ-calculus, lógica combinatória. Elementos de teoria dos tipos. Noções de semántica de linguagens de programação. Y-combinator, fixpoints e recursão. Axiom of choice e suas conseqüências. Tipos de dados algébricos. Programação funcional. Programação lógica. Bancos de dados.
Bibliografia
(Conhece o libgen.is?)
Principal
- Matemática fundacional para computação [fmcbook]
- U0: (1–6), 7, 11
- U1: 12, 13, 15
- U2: 17, 18, 19
- U3: (20), 21, 22, 33
:
Auxiliar
Para cada um dos assuntos que tratamos, procure a secção «Leitura complementar» no capítulo correspondente do fmcbook para mais referências.
- Software Foundations, Volume 1: Logical Foundations [SF1] :
- Conceptual Mathematics: A first introduction to categories (I, II) :
- How to prove it (1–3) :
- A book of abstract algebra (2–5, 6, 12, 17) :
- Introduction to lattices and order (1, 2) [DP] :
- Naïve set theory :
- Notes on set theory (1, 2, 3–5, 6–7) [NST] :
- Classic set theory, for guided independent study (4, 7, 8) :
- Satan, Cantor, and Infinity :
- A beginner's guide to mathematical logic (Volume 1) :
- Linear Algebra Problem Book (1) :
- A survey of modern algebra (1.11; 1.1–1.5, 1.10, 1.12) :
- Algebra: Chapter 0 :
- Algebra (1.1–1.3) :
- Topics in Algebra (2.1–2.5 [skip # and *]) :
- Introduction to topology and modern analysis (1) :
- Topology (1) :
- Advanced Calculus (0) :
- Lógica Aplicada à Computação website (TdC, R&I) :
Programação
- Thinking Functionally in Haskell :
- Programming in Haskell :
- Learn you a Haskell for great good :
- The art of Prolog :
Links
Dicas
- How to write mathematics badly (video lecture) :
- How to write mathematics :
- Comments on style :
- Mathematical writing :
- Por que tantos livros? Qual é o melhor? Vale a pena ler esse excerto do livro Linear Algebra de .
Avaliação
Pontos
A disciplina é dividida em 3 unidades (vejá Conteudo). Em cada unidade o aluno vai receber de 0 a 100 pontos. As provas escritas de cada unidade terão 100 pontos em total. (Para pegar uma idéia dessas provas, olhe nos sites das minhas turmas de semestres passados.)
Alem desses pontos, um aluno pode ganhar pontos extra: por participação; por homework; ou por provas-surpresas. Esses pontos valem igualmente com os pontos de prova escrita. Estou tentando ao máximo ser justo com esses pontos, mas nenhuma justificativa será dada por ganhar (ou não ganhar, ou perder!) pontos extra.
Umas regras: (1) nunca dê uma resposta que tu não pensou sozinho; (2) não tente “forçar a barra” dando respostas aleatórias nas minhas perguntas tendo como objetivo ganhar pontos extra.
Umas provas escritas podem ter pontos bônus. Esses são pontos que são condicionalmente considerados: para considerá-los um aluno precisa ter pelo menos 50pts normais (não-bônus). As questões que valem pontos-bônus são em geral em assuntos auxiliares que, mesmo que merecem ser reconhecidos, não devem ser determinantes para aprovar na disciplina.
Presenças
Veja notícia no SIGAA para informações sobre presenças, chamadas, plickers, etc.
Provas
As provas principais serão avisadas com antecedência de pelo menos 48 horas.
Provinha 0
- Provinha 0 (pts: 0; bônus: 0) (dia: 19/02/2020)
{ uncensored, answers }
correções: p1, p2, p3.
Unidade 1
- Prova 1.1 (pts: 28; bônus: 0) (dia: 13/03/2020)
T = { censored, uncensored, answers };
N = { censored, uncensored, answers }
Unidade 2
Unidade 3
Reposição
Pontos extra
Pontos de participação (CP) e homework (HW):
Unidade: | U1 | U2 | U3 | |||
---|---|---|---|---|---|---|
Quem: | CP | HW | CP | HW | CP | HW |
T34 | ||||||
Andreon | 6 | 1 | ||||
André | 3 | 4 | ||||
Arnaldo | 7 | 1 | ||||
Bruno | 5 | |||||
Débora | 5 | 7 | ||||
Gabriel B | 4 | |||||
Gabriel H | 5 | 1 | ||||
Gabriel V | 5 | 1 | ||||
Italo | 2 | |||||
Levir | 1 | 1 | ||||
Matheus A M | 4 | 1 | ||||
Matheus A S | 2 | |||||
Paulo | 1 | |||||
Tarsila | 4 | 1 | ||||
Vitor | 1 | |||||
N12 | ||||||
André | 5 | 1 | ||||
Andrécio | 3 | 4 | ||||
Chianc | 10 | |||||
Esdras | 1 | |||||
Gabriel | 2 | |||||
JVK | 4 | |||||
JVV | 2 | |||||
Jeff | 1 | |||||
Jonathan | 2 | |||||
Luan | 3 | 1 | ||||
Lucas L | 2 | |||||
Marcell | 1 | |||||
Rafael | 5 | |||||
Raimundo | 4 | |||||
Victor | 2 |
Homework
Obs.:
- Estudar um assunto dum livro obviamente inclui resolver todos os exercícios e problemas.
- «Até» é sempre inclusivo.
- Homeworks marcados assim são opcionais; considero o resto obrigatório.
- Depois de cada aula, um homework é sempre válido, obrigatório, e essencial:
sem olhar para teu caderno, defina todas as noções e demonstre TODOS os teoremas da aula;
while (não conseguiu) { estude o assunto; tente novamente; }
15/01/2020
- Assista minhas aulas relevantes do FMC1/2019.2 (até 16/09/2019)
- Estude o capítulo «Estratégias de provas».
- Estude o capítulo «Linguagens».
- Estude o capítulo «A linguagem de lógica proposicional».
- Estude brutalmente o capítulo «Os números naturais: recursão; indução».
- Estude os capítulos 1–3 de Velleman.
- Brinque com Haskell ou PureScript.
- Installe o Coq; dê uma lida no «Preface» do SF1 (link na Bibliografia); estude o capítulo «Basics» do SF1.
23/02/2020
- Podemos ler o « ⇔ » como «se e somente se». Qual das duas partes dele (⇐ e ⇒) corresponde no «se» e qual no «somente se»?
- Podemos ler o « ⇔ » como «é suficiente e necessário para». Qual das duas partes dele (⇐ e ⇒) corresponde no «é suficiente para» e qual no «é necessário para»?
- Resolva os A,B da provinha 0.
- Pense sobre o resto dos conectivos: como faria sentido atacar e como usar?
- Já fez o homework anterior?
28/02/2020
- Defina as (∃!x)[φ(x)] e (∃!x∈A)[φ(x)] como açúcares sintácticos do que temos até agora.
- Defina o predicado Singleton(–)
- Estude as secções §§113–117.
- Estude a secção §118.
02/03/2020
- (∃!x)[φ(x)] ⇐?⇒ (∃z)(∀x)[φ(x)⇔x=z]
04/03/2020
- Estude a secção §119.
- Estude a secção §120.
- Estude a secção §121.
- Estude a secção §122.
- Estude a secção §123.
06/03/2020
- Nesse problema é proibido usar os «feitiços fortes»: nem LEM, nem dupla negação, e logo não podes demonstrar algo por Reductio ad absurdum. E logo, para atacar uma disjunção precisa escolher um dos dois componentes e matá-lo!
Suponha que P denota uma proposição arbitrária. Quais das propriedades seguintes consegues demonsrar?- P⇒¬¬P
- P⇐¬¬P
- ¬¬(P∨¬P)
- se P⇒Q então ¬Q⇒¬P
- se ¬Q⇒¬P então P⇒Q
- Para aquela das duas últimas que tu não conseguiu demonstrar (por justa causa!), tem como demonstrar «quase» isso, ou seja, tem como demonstrar uma coisa parecida mas mais fraca. Adivinha qual é, e demonstre!
07/03/2020
- Estude brutalmente o capítulo «Os números naturais: recursão; indução». (Foi hw desde 24/02/2020.)
- Resolva as questões de recursão/indução de FMC1 dos semestres passados, especialmente do 2019.2.
09/03/2020
- Resolva os problemas: Π10.1; Π10.2; Π10.3
- Resolva os problemas: Π10.11; Π10.12
10/03/2020
- Estude a secção §125: Tuplas
- Estude a secção §126: Produto cartesiano
11/03/2020
- Estude a secção: Seqüências
- Π10.4
- Π10.5
- Π10.6
- Π10.7
- Π10.8
- Π10.13
- Π10.14
- Π10.15
- Π10.16
- Π10.17
- Π10.18
13/03/2020
- Defina a União e Intersecção de famílias indexadas de conjuntos. Verifique tua definição (olhando no fmcbook).
- Estude o resto do capítulo «Conjuntos»!
- Resolva o resto dos problemas!
16/03/2020
- Estude a secção §135: Conceito, notação, igualdade
- Estude a secção §136: Diagramas internos e externos
31/03/2020
- Estude o capítulo «Introduções» (que atualizei esses dias).
- Faça os homeworks anteriores que tem deixado pra lá!
Histórico de aulas
17/02/2020: Intro; U0
- ToC de FMC2
- Tipos (objeto vs proposição)
- atômicas vs compostas
- definições e teoremas
- noções primitivas e axiomas
- teorema, lemma, corolários, conjectura
- demonstrações como jogos e programação
- dados – alvos
- linhas de código vs comentários
- conectivos: como atacar e como usar
- números vs numerais vs dígitos
- gramáticas BNF
- Nats
- Recursão
- árvores sintácticas e linhas de inferência
19/02/2020: Provinha 0
21/02/2020: Erros comuns [video]
- Type error
- igualdade vs equivalência, com e sem «def»
- igualdade intensional vs extensional, sintáctica vs semântica
- Erro de semântica
- Diferença entre as duas frases:
- «Se __A__, (então) __B__.»
- «Como __A__, (logo) __B__.»
- Existêncial: como atacar
- Existêncial: como usar
- Três enunciados dum teorema: mesma coisa ou não?
- Universal: como atacar
- Implicação: como atacar
- Conjunção: como atacar
- Conjunção: como usar
- erros de caligrafia e tipografia
- «vírgula mágica», «para» seco, «com», «sendo», «setinha mágica», etc.
- secas equações
- «⇒» vs «logo»
- a redundância de «... é verdadeiro»
- O significado da palavra «equivalente» em matemática
- Um exemplo de demonstração e seu tabuleiro
- REPL
- linha de código vs comentário
- variáveis livres e ligadas
- «para algum» e CUIDADO
- escrevendo gerundiando qualquerando palavrando (wtf)
- «Calculamos»
- nomes desnecessários
28/02/2020: Demonstrações; Conjuntos
- Demonstrações
- Erro: afirmação do conseqüente
- duas maneiras que uma definição pode ser errada
- (∃x∈A)[φ(x)] e (∀x∈A)[φ(x)] como açúcar sintáctico
- linguagem e metalinguagem, variáveis e metavariáveis
- (∃!x)[φ(x)] e (∃!x∈A)[φ(x)] como açúcar sintáctico
- Conjuntos
- idéia informal (Cantor)
- Noções primitivas: ser conjunto, pertencer (∈)
- Tipos de objetos e como introduzi-los
- Conjuntos como “black boxes”
- Igualdade entre conjuntos: A=B
- conjuntos homo- e hetero- gêneos
- Cuidado: O uso de ⊂ na literatura
- As relações binárias: =, ⊆, ⊇, ⊊, ⊋
- ⊈ vs. ⊊
- Notação
- sinônimos de conjunto e convenções de fonts
- Set comprehension (Set-builder notation)
- Definindo o conjunto vazio: nossos deveres
- Três predicados: Empty(–); Singleton(–); Universal(–)
- Obrigação de definir notação (nome) para objeto: artigo definido vs. indefinido
- Provas de existência & unicidade: «fight club»
- hw: existência do conjunto vazio
- hw: unicidade do conjunto vazio
- O conjunto vazio (Ø)
02/03/2020: Conjuntos
- Existe único x tal que...
- Negação: empurrando pra dentro
- Reductio ad absurdum, LEM, dupla negação
- mais set-builder e açucar sintáctico
- variáveis livres e ligadas; sombreamento de variável; capturação de variável
- Singletons
- O conjunto universal
- Oito proposições sobre o Ø e um conjunto A
- Escolhendo a ordem de atacar teoremas
- {Ø} ≠ Ø
04/03/2020: Conjuntos
- limitações da linguagem da lógica proposicional e o que ganhamos na FOL
- termos
- definição de mais notações set-builder
- Erro comum: quantos elementos {x,y,z} tem?
- Cardinalidade |A| e primeiras propriedades
- Operações entre conjuntos e dois jeitos de defini-las
- As operações binárias: ∩, ∪, \, Δ
- diagramas de Venn e definições formais
- A operação unária de complemento: ~
- O operador Powerset (℘)
- Iterando o ℘ no Ø
- Cardinalidade de ℘A
- Generalizando as operações de união e intersecção: as operações unárias ⋂, ⋃
- Iterando o ℘ no Ø
06/03/2020: Conjuntos
- tese vs hipotese
- intensão vs extensão
- Intuição sobre os ⋂, ⋃, e ℘ e as {, }
- Iterando os ⋂ e ⋃ no Ø
- «por vacuidade»
- Tuplas: interface, black box, notação
07/03/2020, 09h15–13h45: Naturais; Recursão; Indução
aulas gravadas correspondentes:
- [12/08/2019]
- [14/08/2019]
- [16/08/2019]
- [19/08/2019]
- [21/08/2019]
- Números vs numerais
- Linguagens: sintaxe e semântica
- Nat(urais): uma definição humana
- um acordo sobre afirmações com (meta)variáveis não declaradas
- voltando: variável vs metavariável
- Nat(urais): uma definição com gramática
- Nat(urais): uma definição com regras de inferência
- os valores canônicos de Nats
- função/operação vs construtor
- Igualdade
- cuidado: os «para todo» e «existe»
- Recursão
- 2+3=5
- Recursão vs tijolo
- Calculando a soma com recursão
- onde focar para reduzir?
- Multiplicação
- 2 · 3 = 6
- qual resultado incompleto é melhor?
- precedência e associatividade de operadores
- Θ. Associatividade da +
- tem como continuar a demonstração?
- escolhendo variáveis com «linhas»: x', x'', etc.
- o problema que temos demonstrando esse teorema
- a recursão foi no segundo argumento, então...
- «para ALGUM»
- Recursão – Indução: dois lados da mesma moeda
- Indução
- quando podemos usar indução
- indução informalmente
- Esqueçam a receitinha de 3 passos!
- Indução como regra de inferência
- «Base» e «Passo indutivo»
- a regra de indução na verdade é um esquema
- indução para demonstrar nosso teorema atual
- «hipótese indutiva»
- Como podemos continuar agora?
- presente da recursão vs presente da indução
- E se eu nem precisei usar a hipótese indutiva?
- Faz diferença se escolher usar indução mais cedo?
- recap: associatividade da +
- tentar começar «por indução»
- «por indução no z»
- podemos trocar quantificadores consecutivos da mesma forma
- discussão: comparação das duas demonstrações
- comparando as H.I.'s
- o que ganhamos
- Θ: + é comutativa
- lemmas em demonstrações
- comparação com programação
- subinduções
- lendo as H.I. «com palavras da rua»
- escopos e escolhas de variáveis
- escopos e as várias hipoteses indutivas
- entender no coração, com palavras da rua
- passo indutivo da segunda sub-indução
- usando o ` ≟ '
- adição, multiplicação, exponenciação, e depois?
- escolhendo nomes lindos para nossas variáveis
09/03/2020: Lógica; Conjuntos
- Lógica
- Disjunção: como atacar e como usar
- Lógica clássica vs intuicionista
- LEM, LDN
- Dicas para uns homeworks
- Conjuntos
- Princípio de inclusão–exclusão
- Princípio da adição
- Cardinalidade de ℘A: como demonstrar a propriedade
- Demonstração de inclusões e igualdades
- Θ: C\(A∪B) = (C\A)∩(C\B)
- tuplas como noções primitivas
- tuplas como black boxes
- Equações fundamentais de tuplas
- igualdade de tuplas
- projeções: πi
- implementação de tipo
- Implementando de 3-tuplas
- def'inho criminoso
- Podemos definir n-tuplas para outros n's?
- Produto cartesiano (×)
- Cardinalidade do A×B: princípio da multiplicação
- Definindo o Aⁿ informalmente
11/03/2020: Conjuntos
- Implementação-agnóstico
- n-Tuplas e Aⁿ
- O tipo de 1-tuplas
- O tipo de 0-tuplas
- A única 0-tupla: ()
- Seqüências
- outras notações
- de operação binária para n-ária
- de n-ária para ``seq-ária''
- União e Intersecção de seqüências de conjuntos
- Σ vs. ⋃
- Riemann's rearrangement theorem
13/03/2020: Prova 1.1; Conjuntos
- «Seja (x,y) em A×B.» Pode?
- Prova 1.1
- Exemplo: Os conjuntos Aₚ de todos os ancestrais da pessoa p, e Vₚ de todos os vilarejos do país p.
- Família indexada
- Traduzindo afirmações da linguagem natural para relações entre conjuntos e vice-versa
- Família indexada como generalização de n-tuplas e seqüências
- Produto cartesiano generalizado (de família indexada de conjuntos)
- Conjuntos disjuntos dois-a-dois («pairwise disjoint»): definição com e sem índices
16/03/2020: Sermão; Funções
- Sermão
- Quando um «Seja k natural.» fica esquisito e idéia péssima.
- Arbitrário?!
- Umas dicas para problemas em seqüências de conjuntos, seus limites, etc.
- Funções
- Conceito, notação
- Setinhas com e sem bundas
- Duas religiões sobre funções e seus black boxes
- Igualdade
- Diferença entre f(x) e f
int foo(int x)
. Qual o tipo dafoo
- regra de inferênca de tipo de função
- O conjunto (A→B) (também denotado por BA)
- graph(f)
- range(f)
- aridade de função e uso de tuplas
- Diagramas internos e externos
- Igualdade extensional vs. intensional
Futuro (fluido)
A turma mudou para o 2020.6 por causa do maldito corona.