2025.1 FMC2, turma de Thanos

Horários de aula: 246T12♯ [13h05–14h45]
Sala: B203
Contato:thanos@imd.ufrn.br
Playlists: FMC2: ( CFR | IEA )
Pré-reqs: ( Intro | IDMa | IRI | IDMb )
Monitoria/TA: fmc.imd.ufrn.br
Turmas anteriores: ..
Self-study sites: /teaching/self

Info

Pré-requisitos

É essencial¹ ter aprendido bem o conteudo transversal de FMC1. Sem aprender esses assuntos primeiro, não faz sentido se matricular em FMC2.

¹ Imagine chegar em Polo Aquático II, 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.)

Então—ANTES de começar—é bom ter estudado:

Para revisar: veja o IntroProof (isso inclue o logic.lean (veja lá) e o NNG).

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

(Obs.: estudar ≠ ler.)

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

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

Conteúdo

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

CFR1: Conjuntos, Funções (30h)

Especificações e implementações matemáticas de coleções (conjuntos, ênuplas, multiconjuntos, sequências), e de suas principais operações e predicados; extensão vs intensão. A notação construtor-de-conjunto (set-builder) e sua interpretação. Implementação da noção de cardinalidade, no caso finito. Operações sobre coleções, finitas ou não, de conjuntos: união, interseção, produto e coproduto de conjuntos (produto cartesiano e união disjunta). Para o caso de coleções finitas, definições recursivas e demonstrações indutivas das suas propriedades. Complemento relativo, diferença simétrica. Conjunto potência. Especificações de famílias indexadas. Operações sobre famílias indexadas de conjuntos. Coberturas e partições. Especificações e implementações matemáticas de associações (funções parciais, totais, e não-determinísticas); extensão vs intensão. Funções vs procedimentos em programação; funções puras e efeitos colaterais. Funções anônimas (notação lambda). Funções de ordem superior, e funções como cidadãos de primeira classe. Curryficação e aplicação parcial de funções. Função identidade, composição de funções, iterações de uma função. Função inclusão, função vazia, função 0-ária, função constante. Projeções e demais funções associadas ao produto e ao coproduto de conjuntos (pairing, copairing, …). Funções indicadoras (ou características). Restrições de funções. Imagem direta e pré-imagem de conjuntos. A inversão de uma função, e a função inversa.

CFR2: Funções, Relações (30h)

Funções injetivas e sobrejetivas, monos e epis. Retrações e seções. Condições de invertibilidade de uma função. O teorema de Cantor sobre a cardinalidade do conjunto potência, e as cardinalidades transfinitas. Breve introdução à teoria da computabilidade: funções computáveis, números computáveis, e conjuntos computáveis; semi-decidibilidade e decidibilidade. Relações e a sua implementação conjuntista. Operações sobre relações, com ênfase no caso binário: inversa, composição, iterações, fechos. Descrição e propriedades do fecho transitivo: usando interseção (top-down) e usando união (bottom-up). Exemplos de conjuntos estruturados (e.g. espaços normados, espaços métricos, espaços topológicos, espaços de medida, grafos). Relações de equivalência e partições, classes de equivalência, e o conjunto quociente. Equivalências mais finas e mais grossas, e a relação de equivalência induzida pelo núcleo de uma função. Construções de classes de números usando quocientes. Relações de ordem: pré-ordens, ordens parciais e ordens estritas, ordens totais, elementos minimais e elementos maximais, supremos e ínfimos. Cadeias e funções que preservam ordem. Reticulados e reticulados completos. Ordens parciais completas. A construção de uma função a partir do limite de uma cadeia de funções parciais. Relações bem-fundadas: definição usando cadeias e definição usando elementos minimais, conexão com recursão e indução. Relações bem-fundadas induzidas pela imagem inversa de uma relação bem-fundada, pelo produto lexicográfico de relações bem-fundadas, e pelo fecho transitivo de uma relação arbitrária. Os Fundamentos da Matemática: uma breve introdução à Teoria Axiomática dos Conjuntos.

IEA: Introdução a Estruturas Algébricas (30h)

  1. Grupos (6h) Permutações: notação de cíclos e verificação das leis de grupo para os Sₙ. De Sₙ para grupos: definições alternativas de grupo baseadas em assinaturas diferentes; notação, exemplos e não-exemplos, incluindo casos numéricos (em particular da aritmética modular), famílias de conjuntos, espaços de funções e relações, strings. Definições de grupo abeliano, monóide, semigrupo, magma. Definição de teoria e de modelo, e as primeiras conseqüências (teoremas) das leis (axiomas) dos grupos: unicidade de identidade e dos inversos, leis de cancelamento e de resolução de equações, inverso da identidade, de inversos, e de produtos, e sua expressão com diagramas comutativos. Independencia de axiomas: como demonstrar a não-demonstrabilidade. Critérios para verificar se uma estrutura é um grupo. Como definir um grupo: tabelas de Cayley. Construções: o produto direto de grupos, grupo livre. Potências (com expoentes de naturais até inteiros) e ordem de membro de grupo incluindo demonstrações das suas propriedades (por indução e usando o lema da divisão de Euclides).
  2. Subgrupos e o grupo quociente (6h) Subgrupos: definição, exemplos, nao-exemplos, critérios; “subgrupo de” como relação de ordem; propriedade de interseção de subgrupos; relações de equivalência determinadas por subgrupos. Subgrupo gerado por subconjunto: como definir tanto top-down quanto bottom-up e demonstração por indução da sua equivalência. Exemplos fora da teoria dos grupos, incluindo conjuntos convexos e o fecho convexo. Congruência (modulo subgrupo) e coclasses. Verificação que se trata de relação de equivalencia e partição. Subgrupos normais: definições alternativas e verificação da sua equivalencia. O grupo quociente. O teorema de Lagrange e o indice dum subgrupo num grupo. Aplicações em teoria dos números incluindo obter o teorema de Euler (e logo o pequeno Fermat também) como corolário de Lagrange.
  3. Homomorfismos e isomorfismos (6h) Simetrias, os grupos simetricos, e os diagramas Hasse dos reticulados dos seus subgrupos. Homomorfismos e preservação da estrutura algebrica. Critérios de homomorfismos para grupos. Monomorfismos, epimorfismos, isomorfismos, endomorfismos, e automorfismos. O grupo Aut(G). Núcleo, imagem, e o primeiro teorema de isomorfismos de Noether para grupos. Um esboço do teorema de representação para grupos (teorema de Cayley).
  4. Outras estruturas (6h) Outras estruturas, seus primeiros teoremas e as definições de homomorfismo: semigrupo, monoide, anel, anel booleano. O monoide livre e o fecho de Kleene (Kleene star). Corpos, corpos ordenados completos e o enunciado da sua unicidade a menos de isomorfismo (os números reais). Espaços Vetoriais. Reticulados como álgebras. Construções e mapeamentos (monotonos, order-embeddings, e ordem-isomorfismos). O reticulado de subgrupos e de subgrupos normais. Homomorfismos e subreticulados. Reticulados booleanos. Enunciado do teorema de representação de Stone. Algebras de termos.
  5. Categorias (6h) Definição de categoria e exemplos, incluindo categorias associadas à programação e à lógica, e categorias a partir de preordens e posets. Dualidade e a definição de categoria oposta. Mono, epi, split mono, split epi, e iso. Definições (como especificações) por propriedades universais e diagramas comutativos: objetos terminais e inicias, produtos e coprodutos. Suas unicidades a menos de isomorfismo. Subobjetos, objetos quocientes, objeto livre, e suas propriedades universais. Verificação da sua existencia nas categorias encontradas.

Objetivos de aprendizagem

CFR1: Conjuntos, Funções

Prática com o uso das técnicas de demonstração e refutação matemática. Familiarização com a linguagem e com as principais classes, operações e propriedades de conjuntos e funções, definidas extensionalmente ou intensionalmente. Familiarização com as noções do cálculo lambda usadas em programação e lógica: variáveis ligadas e livres, captura de variáveis, renomeamento de variáveis, sombreamento de variáveis, aplicações de funções aos seus argumentos. Reconhecer os objetos matemáticos relevantes às linguagens de programação e suas propriedades. Familiarização com a formulação de especificações, e suas implementações matemáticas. Familiarização com o uso de diagramas comutativos em definições e demonstrações, e com especificações via propriedades universais.

CFR2: Funções, Relações

Prática com a escrita de especificações matemáticas e com o uso das técnicas de demonstração matemática, incluindo o método da diagonalização. Familiarização com as principais classes, operações e propriedades de relações. Familiarização com cardinalidades de conjuntos infinitos. Apreciar a conexão entre especificação e implementação. Familiarização com o raciocínio “sem pontos” (a saber, sem mencionar elementos dos conjuntos), através do composições de funções, e suas aplicações em programação.

IEA: Introdução a Estruturas Algébricas

Compreensão do papel da álgebra no estudo de estruturas de interesse computacional. Prática das técnicas de demonstração matemática e do uso do raciocínio equacional. Apreciar a conexão entre axiomas e seus modelos, e o conceito de independência lógica. Familiarização com a linguagem básica e as idéias elementares da Teoria das Categorias, incluindo o uso de diagramas comutativos para expressar proposições (leis e teoremas), especificações e definições.

Bibliografia e referências

Conhece o libgen?

Principal

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.

CFR1: Conjuntos, Funções

  • [fmcbook]: Cap: «Conjuntos»; «Funções»
  • Moschovakis (2005): Notes on Set Theory, 2nd ed. (cap: 1)

CFR2: Funções, Relações

  • [fmcbook]: Cap: «Relações»; «Posets; reticulados»; «O paraíso de Cantor»; «Teoria dos conjuntos axiomática»
  • Moschovakis (2005): Notes on Set Theory, 2nd ed. (cap: 2,3,4,5,A)
  • Davey & Priestley (2002): Introduction to Lattices and Order, 2nd ed. (cap: 1, 2, 4, 8)
  • Moschovakis (2005): Notes on Set Theory, 2nd ed. (cap: 6)

IEA: Introdução a Estruturas Algébricas

  • [fmcbook]: Cap: «Teoria dos Grupos»; «Estruturas Algébricas»; «Teoria das Categorias»
  • Aluffi (2009): Algebra, Chapter 0 (Cap: II)
  • Herstein (1975): Topics in Algebra, 2nd ed.
  • Halmos & Givant (2009): An introduction to Boolean Algebras
  • Birkhoff & Mac Lane (1977): A Survey of Modern Algebra, 4th ed.
  • Mac Lane & Birkhoff (1999): Algebra, 3rd ed.
  • Davey & Priestley (2002): Introduction to Lattices and Order, 2nd ed.
  • Barr & Wells (1998): Category Theory for Computing Science, 2nd ed., 2020 reprint

Auxiliar

  • Goldblatt (1979): Topoi
  • Crole (1993): Categories for Types (Cap: 1,2,3)
  • Lawvere & Schanuel (2009): Conceptual Mathematics, 2nd ed.
  • Barr & Wells (1998): Category Theory for Computing Science, 2nd ed., 2020 reprint
  • Bird & de Moore (1997): The Algebra of Programming
  • Halmos (1960): Naive Set Theory
  • Wells (1993): Communicating Mathematics: Useful ideas from computer science (in American Mathematical Monthly, Vol 120, No. 5, pp.397–408)
  • Mendelson (1973): Number Systems and the Foundations of Analysis (Cap. 2, 3, 4, 5, E, F)

Dicas

Veja minha página de dicas para estudantes.

Links

Tecnologias e ferramentas

Obs.: As tecnologías/ferramentas seguintes podem mudar durante a disciplina—exceto a primeira.

  1. PAPEL (um caderno para dedicar à disciplina) e LAPIS/CANETA.
  2. Zulip (leia o FAQ).
  3. Pouco de (La)TeX (veja o minicurso TeX 2018.2). Online editor/compilador: Overleaf.

Regras

  1. Nunca escreva algo que você mesmo não sabe explicar: (i) o que significa; (ii) seu papel na tua resolução. Por exemplo: um aluno escreveu a frase seguinte na sua demonstração: «Como f é cancelável pela esquerda temos que g=h». Ele deve saber o que significa ser cancelável pela esquerda e também explicar como isso foi usado e/ou o que isso tem a ver com essa parte da sua demonstração.
  2. Qualquer trabalho poderá ser questionado em forma de prova oral, em modo privado ou aberto. Se um aluno não consegue explicar o que ele mesmo escreveu numa resolução, será considerado plágio (veja abaixo).
  3. Participando, nunca dê uma resposta que tu não pensou sozinho, exceto dando os créditos correspodentes.
  4. Não tente “forçar a barra” perguntando ou respondendo coisas aleatórias com objetivo único de ganhar pontos. Os pontos de participação não correspondem em apenas perguntas ou dúvidas que mostram interesse. O interesse é implícito pelo fato que tu escolheu matricular nesta turma—não vale pontos.
  5. Não procurem resoluções em qualquer lugar fora dos indicados em cada homework. O único recurso aceitável para procurar ajuda é no nosso Zulip (especificamente seus canáis públicos—não DM) e a monitoria.
  6. Proibido consultar o apêndice de resoluções do fmcbook durante a disciplina exceto quando for explicitamente permitido por mim. (Os apêndices de dicas são permitidos sim.)

Uns deveres dos alunos

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

(Veja também os FAQs relevantes.)

Sobre plágio

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

Cadernos vs. celulares

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

Avaliação e faltas

Disclaimer. Eu suponho que os alunos desta turma escolheram se matricular por interesse em aprender seu 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.

Informação sobre as provas será postada aqui.

U1 (CFR1)

U2 (IEA)

  • Prova IEA.1 / ?pts (2025-05-??) { censored , uncensored , answers , correções }
  • Prova IEA.2 / ?pts (2025-07-??) { censored , uncensored , answers , correções }

U3 (CFR2)

  • Prova CFR2.1 / 100pts (2025-07-??) { 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.
  • No PDF do quadro cor rosa costuma indicar hw.
  • Referências a páginas ⟦assim⟧ referem ao PDF do quadro.
  • Homeworks marcados assim são auxiliares; tente apenas se tu tem resolvido uma parte satisfatória dos outros.

2025-03-19: (IEA-hw1)

  1. C«Teoria dos Grupos»: §«Permutações»

2025-03-21 (CFR1-hw1)

  1. Demonstre que $(\subseteq_\alpha)$ é uma ordem parcial. Ela possui bottom/top?
  2. Demonstre que $(\cup_\alpha)$ é idempotente.
  3. Ela tem identidade?
  4. Ela tem absorvente (anulador)?
  5. Defina o resto das operações de conjuntos que tu conhece.
  6. Estipule propriedades de tais operações (enuncie como teoremas) e demonstre.
  7. Considere as variações seguintes da notação set-builder, que não definimos (ainda) e: (i) escreva quais conjuntos tu acha que elas descrevem (a extensão); (ii) mostre como definir o mesmo conjunto (intensionalmente) usando a maneira “oficial” de definir conjuntos que encontramos na aula:
    1. { x ∈ {2,3,4} | 2ˣ+1 é primo }
    2. { x²+1 | x ∈ {2,3,4} }
    3. { x²+y | x ∈ {2,3}, y ∈ {0,1}, x+y primo }
  8. Defina tais variações de set-builder.
  9. C«Coleções»:
    §«Conceito, notação, igualdade» §«Intensão vs. extensão» §«Relações entre conjuntos e como defini-las» §«Operações entre conjuntos e como defini-las» §«Demonstrando igualdades e inclusões»

2025-03-21 (CFR1-hw2)

  1. Defina o conceito dual de Empty (sim, chute, sem saber o que significa «dual»).
  2. Enuncie e demonstre a existência e unicidade relacionada ao Empty e ao conceito que definiu acima.
  3. C«Coleções»: §«Vazio, universal, singletons», §«Oito proposições simples», §«Mais set builder»
  4. C«Funções»: §«Conceito, notação, igualdade»

2025-03-26 (IEA-hw2)

  1. Verifique que S₃ é um grupo e se acostuma com a notação de permutações
  2. Escreva sozinho uma demonstração completa da unicidade de identidade numa estrutura de grupo. Quais leis tu precisou mesmo?
  3. Demonstre a unicidade dos inversos.
  4. Infira teoremas que envolvem mais que um dos três protagonistas da alma de grupo: a operação (binária), a identidade, e os inversos. Por exemplo: o inverso do inverso deve ser o quê? O inverso da identidade? Etc. (O Etc é importantíssimo!)
  5. Consegues definir operação binária no {Natal, Recife} e no {Haskell, Rust, Scala} para formar dois grupos com esses carrier sets?
  6. C«Teoria dos grupos»: até a §«Primeiras conseqüências»

2025-03-28 (CFR1-hw3)

  1. Θ. 𝒜∩ℬ hab ⇒ ⋂𝒜 ⊆ ⋃ℬ
  2. o que podemos concluir sobre a cardinalidade do conjunto {f(x,y) ∣ x,y∈{u,v}}?
  3. Acho algo interessante que carateriza os habitantes duma diferença simétrica.

2025-04-02 (CFR1-hw4)

  1. Verifique se as seguintes podem servir como implementações de ⟨,⟩:
    1. ⟨x,y⟩ ≝ {x,{y}}
    2. ⟨x,y⟩ ≝ {{x,y},{x}}
    3. ⟨x,y⟩ ≝ {{0,x}, {1,y}}
  2. C«Coleções»: até §«n-tuples»
  3. C«Funções»:
    • §«Expressões com buracos»
    • §«Um toque de lambda»
    • §«Aplicação parcial»
    • §«Funções de ordem superior»
    • §«Currificação»

2025-04-07 (CFR1-hw5)

  1. Dê uma especificação de produtos n-ários de tipos, denotados por Prod(α₁,…,αₙ) para n≥2.
  2. Dê uma especificação de somas n-ários de tipos, denotados por Sum(α₁,…,αₙ) para n≥2.
  3. Considere os casos especiais n=1, n=0 tanto no Prod quanto no Sum.
  4. Capítulo «Coleções»: todos os problemas do primeiro intervalo de problemas.
  5. (Revisão.) Escreva a tabelinha dos conectivos e seus usos/ataques, incluindo para cada comando escrito qual é o efeito que tem no estado da demonstração (i.e.: nos dados e no alvo).

2025-04-10 (IEA-hw3)

  1. Demonstre: (!-id), (!-inv); (inv-op), (inv-id), (inv-inv); (canL), (canR); (res-!)
  2. Resolva o desafio: Dado n : ℕ construir um grupo de ordem n.
  3. Demonstre que as duas maneiras de definir potências (expoentes ≥ 0) são equivalentes. ⟦p.17⟧
  4. Demonstre que as duas maneiras de definir potências (expoentes < 0) são equivalentes. ⟦p.18⟧
  5. Qual o tipo da $o_G$? ⟦p.19⟧
  6. C«Teoria dos grupos»: até o primeiro intervalo de problemas
  7. Qual proposição é a conjunção de 0 dadas proposições?
  8. Assinaturas diferentes para o conceito de grupo: (G;op) + leis; (G;op,id) + leis; (G;op,id,inv) + leis:
    1. Faça o que precisa fazer para defender a afirmação que «as três definições de grupo são equivalentes»
    2. Tem como ter uma quarta alternativa, com assinatura (G;op,inv)?
    3. Teria como achar um (G;op,inv) que acaba não sendo um grupo mesmo a op sendo associativa e inv merecendo seu nome?

2025-04-14 (CFR1-hw6)

  1. Infira quais são as equações (β, η) que governam o tipo Unit, e o que significa igualdade.
  2. Implemente o tipo Weekday de dias de semana
  3. Estabeleça (demonstre!) as leis de aritmética do ensino fundamental agora sobre os típos, considerando que $\alpha^\beta$ significa $\alpha \mathrel{\leftarrow} \beta$, i.e., $\beta \to \alpha$.
    1. $\delta^{\alpha+\beta} \cong \delta^\alpha \cdot \delta^\beta$
    2. $(\gamma^\beta)^\alpha \cong \gamma^{\beta\cdot\alpha}$
    3. $\alpha^0 \cong 1$
    4. $\alpha^1 \cong \alpha$
    5. $\alpha^2 \cong \alpha\cdot\alpha$
    6. $1^\alpha \cong 1$
    7. $0^\alpha \cong {?}$
    8. $0^0 \cong {?}$
    9. distributividade: $\delta(\alpha+\beta) \cong \delta\alpha + \delta\beta$
    10. (+)-associatividade
    11. (+)-comutatividade
    12. (×)-comutatividade
    13. (+)-identidade
    14. (×)-identidade
    15. anulador: $\alpha\cdot 0 \cong 0$
    16. $(\alpha+\beta)^2 \cong {?}$
  4. Capítulo «Funções»:
    • §«Diagramas internos e externos»
    • §«Definições estilo point-free (tácito)»
    • §«Leis de composição»
    • §«Diagramas comutativos»
    • §«Jecções: injecções, sobrejecções, bijecções»
    • §«Produtos e demais construções»
    • §«Funções de graça»
  5. Demonstre que (≅) (isomorfía de tipos) é uma relação de equivalência
  6. Demonstre que (≅) é uma congruência para as: 0, 1, (+), (×), (→)
  7. Em qual sentido ela é uma congruência melhor que a dos inteiros que estudamos em FMC1 (IDMa)?

2025-04-16 (IEA-hw4)

  1. C«Teoria dos grupos»: até §«Subgrupos», sem a §«Conjugação»

2025-04-26 (CFR1-hw7)

  1. Escolhe uma das $\Delta_{\alpha}$, $\langle\_,\_\rangle$, $\_\times\_$ como primitiva e defina as outras duas
  2. ⟨outl, outr⟩ = ?
  3. ⟨f,g⟩ = ⟨k,h⟩ ⇒ ?
  4. ⟨f∘h,g∘h⟩ = ?
  5. (f×h)∘⟨g,k⟩ = ?
  6. $1_A \times 1_B = {?}$
  7. (f×h)∘(g×k) = ?
  8. [⟨u,v⟩|⟨i,j⟩] = ?
  9. Capítulo «Funções»:
    • §«Coproduto; união disjunta»
  10. Jogue e termine o Lean Game Server: Set Theory Game
  11. Interprete as “leis de exponenciação” em termos Adultos™:
    1. (ab)ᵈ = aᵈbᵈ
    2. cᵃ⁺ᵇ = cᵃcᵇ
    3. cᵃᵇ = (cᵃ)ᵇ

2025-04-30 (CFR1-hw8)

  1. Investiga as propriedades das $\overrightarrow \wp$, $\overleftarrow \wp$ ⟦pp.72–73⟧
  2. Capítulo «Funções»: até o 3o Intervalo de problemas (antes da §«Funções parciais»
  3. Capítulo «Coleções»: até §«Disjuntos dois-a-dois»

Histórico

Quadros das aulas

  • Quadro CFR1: lecs 01–12
    Last update: 2025-04-30
  • Quadro IEA: lecs 01–06
    Last update: 2025-04-24
  • Quadro CFR2: (nenhuma aula ainda)

2025-03-17: CFR1 (1)

  • Tipagem e sua notação
  • Inferência de tipos
  • Regras de inferência
  • Arvores de inferência
  • Construtores de tipos
  • Tipo-produto (×), Tipo-função (→)
  • Set : Type vs Set : Type → Type
  • (∪), (∩), (∖), (∆), ℘, ⋃, ⋂
  • espaço (␣) como aplicação de função
  • f 3 vs f(3)
  • f (2,3) vs f(2,3)

2025-03-19: IEA (1)

  • Permutações como bijeções e sua notação
  • Cíclos e sua notação
  • Achando os protagonistas (operações) no mundo S₃
  • Composição: definição e notações
  • Igualdade de funções
  • Operações

2025-03-21: CFR1 (2) [video]

  • (=) e (≠) entre naturais e entre reais
  • Como definir funções
  • Como definir operações de conjuntos
  • Como definir relações entre conjuntos
  • Como definir conjuntos
  • Set-builder notation
  • Ocorrências livres e ligadas de variáveis (binding)
  • Açúcar sintáctico: (∀x∈X)[φ(x)]

2025-03-24: CFR1 (3) [video]

  • Igualdade entre conjuntos
  • Passo computacional (β) para conjuntos
  • Notação λ (fun builder)
  • Passo computacional (β) para funções
  • Substituição
  • Empty, Singleton, Subsingleton
  • Existência e unicidade

2025-03-26: IEA (2) [video]

  • Do exemplo-guia S₃ para a definição de grupo
  • carrier set/type
  • Definição de grupo algébrica (equacional) vs outras definições equivalentes
  • Faz sentido estipular «fechado»?
  • Θ. (id-!)
  • o que é «teoria dos grupos»?
  • uns exemplos e nãoexemplos
  • os 9 componentes que ganhamos assim que tiver um grupo

2025-03-28: CFR1 (4) [video]

  • versões de set builder que parecem mais poderosas
  • Powerset (℘)
  • união grande
  • interseção grande
  • Complemento relativo (∖)
  • Comutatividade de operações
  • Diferença simétrica (∆): duas definições
  • Precedência sintáctica
  • Tuplas: construção e black box

2025-03-31: CFR1 (5) [video]

  • definição de ⋃ e ⋂
  • os açúcares sintácticos: (∀a∈A)[φ(a)] e (∃a∈A)[φ(a)]
  • testando uma definição
  • 2-tuplas
  • (β) para 2-tuplas
  • igualdade para 2-tuplas
  • 3-tuplas
  • impementação de tipo
  • implementação de 3-tuplas

2025-04-02: IEA (3) [video]

  • Grupos multiplicativos e aditivos
  • Grupos comutativos (abelianos)
  • (=) não é simétrica para os olhos humanos
  • Como interpretar equações algébricas de diversas maneiras
  • Θ. Cancelamento
  • (a·) e aplicação de função nos dois lados de uma equação
  • Θ. Identidades baratas
  • Θ. Inversos baratos
  • Θ. Resoluções únicas

2025-04-04: CFR1 (6) [video]

  • erros tentando testar se uma implementação serve
  • construtor vs função: sobre pattern-matching
  • como determinar novos tipos
  • Formar, Contruir, Usar, Computar
  • (β), (η)
  • Unit, Empty
  • quem é void?
  • Composição de funções

2025-04-07: CFR1 (7) [video]

  • (∘)-Assoc
  • arvores e regras de inferência
  • regras admissíveis
  • id-Id

2025-04-09: IEA (4) [video]

  • ordem
  • Tabelas de Cayley e Grupoku
  • potências em grupo para n : ℕ
  • potências em grupo para x : ℤ
  • diagramas comutativos
  • ordem de membro num grupo

2025-04-11: CFR1 (8) [video]

  • diagramas internos e externos
  • -jetividades: inj, sobre, bij
  • de buracos para lambdas
  • currificação
  • isomorfismos e tipos isomórficos
  • aritmética de tipos

2025-04-14: CFR1 (9) [video]

  • funções saindo/entrando
  • funções de graça (construções)
  • f×g
  • tentativa para f∪g
  • mais aritmética de tipos
  • tipos de soma α+β

2025-04-16: IEA (5) [video]

  • Grupos de inteiros modulo n
  • Investigação de ordem de membro
  • Subgrupos
  • fechado sob operação n-ária

2025-04-23: IEA (6) [video]

  • recap: teoremas sobre ordens de membros de grupos
  • interseções e uniões de subgrupos
  • construções de grupo: produto 𝓖×𝓗, oposto 𝓖ᵒᵖ
  • critéria de subgrupo
  • subgrupo gerado por membro de grupo ⟨a⟩

2025-04-25: CFR1 (10) [video]

  • implementação (de especificação): união disjuntora
  • funções e diagramas relacionados ao produto (×) e à soma (+)
  • pointwise
  • Estilo tácito (aka: point-free, pointless)

2025-04-28: CFR1 (11⁻) [video]; Prova CFR1.1

  • aproveitar: saida de (+) e depois entradas em (×) vs entrada em (×) e depois saidas de (+)
  • mais construções de fun: identidade; constante; iterações
  • constante vs invariável

2025-04-30: CFR1 (12) [video]

  • invertibilidade de f
  • f-image
  • f-preimage
  • propriedades de $\overrightarrow{\wp}$ e de $\overleftarrow{\wp}$
  • famílias indexadas e 𝓘-tuplas

Futuro (fluido)

2025-05-05: CFR1 (13)

2025-05-07: IEA (7)

2025-05-09: CFR1 (14)

2025-05-12: CFR1 (15)

2025-05-14: IEA (8)

2025-05-16: CFR1 (16)

2025-05-19: CFR1 (17)

2025-05-21: IEA (9)

2025-05-23: CFR2

2025-05-26: CFR2

2025-05-28: IEA (10)

2025-05-30: CFR2

2025-06-02: CFR2

2025-06-04: IEA

2025-06-06: CFR2

2025-06-09: CFR2

2025-06-11: IEA

2025-06-13: CFR2

2025-06-16: CFR2

2025-06-18: IEA

2025-06-23: CFR2

2025-06-25: IEA

2025-06-27: CFR2

2025-06-30: CFR2

2025-07-02: IEA

2025-07-04: CFR2

2025-07-07: CFR2

2025-07-09: IEA

2025-07-11: CFR2

2025-07-14: CFR2

2025-07-16: IEA

2025-07-18: CFR2

2025-07-21:

2025-07-23:

2025-07-25:

Last update: Thu May 1 13:08:27 +03 2025