2025.1 Teoria dos Tipos, turma de Thanos

Info

Pré-requisitos

• {will, time} to {pratice, study, research};
• English (reading/writing), which is why this list is in English;
• some mathematical maturity™: you should be able to reason and to express mathematical ideas in natural mathematical language using appropriate notation and nomenclature;;
• you must have learned well the main subjects of FMC1 and FMC2—do contact me if you are unsure, especially given the weak (or inexistent) grading that frequently takes place in this department;
• familiarity with the general ideas and tools of structural induction and recursion (see IRI);
• familiarity with the general ideas and tools of abstract algebra (see IEA);
• if you have not passed FMC2 yet, at the very least you must enroll [in my FMC2 class this semester][fmc2-2023.1] to take it in parallel with cats;

(Obs. 1: learn ≠ pass.)

(Obs. 2: study ≠ read.)

Need to revise?

If you want to revise some material related to the prerequisites, specifically any of IRI, IEA, CFR1, CFR2, do check the self-study pages I have prepared. Dive in! 🤿

Conteúdo

MLTT (Martin-Löf Type Theory)

Contextualização: noções da teoria das demonstrações a da teoria das categorias relevantes à teoria dos tipos (sistemas Gentzen de dedução natural e de seqüentes, propriedades universais, construções categoriais), Curry–Howard–et-al. Matemática construtiva e seu aspecto computacional.

Teorias de tipos dependentes de Martin-Löf. Tipos indutivos, incluindo: produtos, somas, unidade, vazio, famílias de tipos, tipos Sigma e tipos Pi (pares e funções dependentes), booleanos, naturais. Casamento de padrão (pattern matching) e recursão. Outros tipos numéricos.

Tipos de identidade e universos de tipos.

Decidabilidade.

Teoria dos tipos dependentes como linguagem de programação e como fundamento da matemática e suas implementações (Agda, Lean).

Formalização de matemática e(m) proof assistants.

Programação funcional com tipos dependentes.

HoTT/UF (teoria dos tipos homotópica e fundamentos univalentes).

Objetivos de aprendizagem

Familiarização com a linguagem e com as principais idéias da teoria dos típos dependentes. Familiarização com os procedimentos de formalização de matemática e o uso de proof assistants.

Bibliografia e referências

Conhece o libgen?

Principal

• Rijke (2022): Introduction to Homotopy Type Theory (CUP, 2022)
• The Univalent Foundations Program (2013): Homotopy Type Theory (2013)
• Girard (1989): Proofs and types
• Christiansen: Functional Programming in Lean (2023)
• Avigad, de Moura, et al: Theorem Proving in Lean 4

Referências auxiliares

• Eu: [fmcbook]
• Moschovakis (2005): Notes on Set Theory, 2nd ed. (cap: 2,3,4,5,A)
• Halmos (1960): Naive Set Theory
• Goldblatt (1979): Topoi
• Crole (1993): Categories for Types
• Barr & Wells (1998): Category Theory for Computing Science, 2nd ed., 2020 reprint
• Wadler et al: Programming Language Foundations in Agda
• Harper: PFPL
• Awodey: Category theory
• Wells (1993): Communicating Mathematics: Useful ideas from computer science (in American Mathematical Monthly, Vol 120, No. 5, pp.397–408)

Dicas

• James Munkres: Comments on style
• Jean-Pierre Serre: How to write mathematics badly
• Don Knuth: Mathematical writing
• Paul Halmos: How to write mathematics
• Por que tantos livros? Qual é o melhor? Vale a pena ler esse excerto do livro Linear Algebra de Jänich.

Links

• NNG
• Lean (veja também o Lean web editor e o livro Theorem Proving in Lean)

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 (pode ser versões eletrônicas disso);
2. Zulip (leia o FAQ);
3. git e GitHub;
4. Lean e/ou Agda;

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.

Uns deveres dos alunos

Atualizarei logo.

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.

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) sua participação durante o semestre inteiro (Zulip & aulas); (ii) seu progresso contínuo durante o semestre inteiro (github & hw); (iii) provas escritas; (iv) trabalhos atribuidos;

Cada aluno será responsável para manter organizado seu caderno/repositório com os assuntos estudados da disciplina.

Presenças e faltas

As presenças/faltas serão cadastradas usando o sistema Plickers (veja o FAQ relevante).

Dado a natureza da disciplina a palavra “presença” aqui não refere apenas na presença física dentro da sala de aula, mas também na presença no Zulip e no github. É essencial manter um repositório atualizado e compartilhar teu progresso com a turma.

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

Atualizarei logo esta secção.

Dynamic content

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.