self study CFR1: Conjuntos, Funções, Relações I

Sessões

CFR1 (0) & IEA (0): Pré e Introdução [video]

• Introdução meta
• Revisão: type errors, linguagem de demonstrações matemáticas
• Exemplos: teoremas sobre a transitividade da (|)

hw

1. Trabalhe nos pré-requisitos.
2. Dê uma lida nos Capítulos 1 e 2.
3. A gente viu no #intro-lang-proofs › aplicando a mesma função nos dois lados como justificar (demonstrar) isso, descubrindo que é uma propriedade fundamental das funções. Desafio: usando uma linguagem de programação que já usou no IMD, mostre que ela não merece usar o termo «função» mostrando como quebrar essa regra. Proibido usar qualquer coisa de random. Postem tentativas/brigas/dúvidas no #programming.
4. Uma tentativa para resolver o hw anterior foi a seguinte: considerar, em JavaScript, que temos 1 == '1' mas f(1) != f('1') onde f é “a função” x => x + 1. O desafio deste hw é achar um motivo bom para desconsiderar essa como resposta válida para o hw anterior.

CFR1 (1): Introdução [video]

• Set: tipos de conjuntos
• Funções: Inferência
• Set como um type constructor
• Como introduzir um novo tipo: interface (como usar), como formar, igualdade
• Interface de conjunto
• buracos e funções de ordem superior
• Sobre conjuntos heterogêneo
• Prop vs Bool
• Set(Set(Int)), etc.
• uma mentira: subconjuntos vs embutimentos
• o que significa «saber o A»
• Igualdade, extensão, black boxes e suas conseqüências
• duas maneiras de errar, dando uma definição

hw.1

1. Cap. 8: §«Expressões com buracos»
2. Cap. 7: até §«Oito proposições simples»

CFR1 (2): Conjuntos [video]

• Operações entre conjuntos e como defini-las
• Complemento relativo (∖)
• Comutatividade de operações
• Diferença simétrica (∆)
• Parseamento e precedência sintáctica
• Diferença simétrica (2)
• Os habitantes duma diferença simétrica
• Complemento de conjunto
• Powerset (℘)
• Empty, Singleton, Universal, Inhabited
• LEM e dupla negação
• conjuntos finitos e o powerset-finito
• união grande
• interseção grande
• sem medo
• versões de set builder

hw.2

1. Capítulo «Conjuntos»: até o primeiro intervalo de problemas

CFR1 (3): Conjuntos; Tuplas [video]

• Sobre o LEM
• Habitado vs Não-vazio
• Brouwer vs Hilbert
• Θ. 𝒜∩ℬ hab ⇒ ⋂𝒜 ⊆ ⋃ℬ
• Um primeiro papo sobre especificação
• Interface das tuplas
• Equações fundamentais das tuplas
• Igualdade entre tuplas
• Criando tipos mais complexos usando Set e Pair
• Q: Podemos definir um novo «pertence» para tuplas?
• Podemos inferir Ø∈A? Ø⊆A?

hw.3

1. Capítulo «Conjuntos»: até §«Tuplas».

CFR1 (4) [video]

• 3-tuplas como tipo primitivo
• especificação vs implementação
• como implementar 3-tuplas usando 2-tuplas
• a importância de ser implementação-agnóstico
• n-tuplas para outros n
• desafio: implementar 2-tuplas (a implementação de Kuratowski)
• o que seria uma 1-tupla?
• sobre 0-tuplas
• existência e unicidade da 0-tupla
• o muito mal-nomeado void
• teaser: tuplas de tamanho infinito e seqüências
• teaser: sacolas
• o que podemos concluir sobre a cardinalidade do conjunto {f(x,y) ∣ x,y∈{u,v}}?

hw.4

1. Capítulo «Conjuntos»: até §«n-tuplas».
2. Como implementarias 2-tuplas usando (apenas) conjuntos “sujos”?

CFR1 (5) [video]

• Conjunto indexado por I
• Família indexada por I (I-tupla)
• família indexada vs conjunto indexado
• Como solicitar um membro arbitrário dum conjunto indexado
• Usando um produto I×J como conjunto de índices
• Seqüências
• Famílias indexadas para implementar outros tipos
• 2-tuplas como conjuntos e um roubo “definindo” funções
• produto generalizado (de famílias indexadas)
• nível-coração: escolhedores

hw.5

1. Capítulo «Conjuntos»: até o fim

Prova CFR1.1

CFR1 (6) [video]

• De operacões binárias para operações generalizadas
• definições recursivas de operações que operam em seqüências
• Somatórios sem órdem/agrupamento especificados
• Funções: black box, descrição, especificação, igualdade, notação
• Q: sobre funções parciais
• Espaço de funçoẽs (A→B) ou Bᴬ
• Vazio como domínio ou codomínio
• Tipo vazio e tipo unit: discussão sobre o mentiroso void
• Definindo funções com buracos

hw.6

1. Revise sobre conjuntos:
   • Exercícios: x7.57; x7.58; x7.59; x7.63; x7.66; x7.67;
   • Problemas: Π7.9; Π7.10; Π7.11; Π7.12; Π7.13; Π7.14; Π7.15; Π7.16
2. Capítulo «Funções»: até §«Expressões com buracos»
3. Justifique a notação Bᴬ para o espaço de funções (A→B)

CFR1 (7) [video]

• graph : (A→B) → Set(A×B)
• o espaço de funções (A→B)
• diagramas internos vs externos
• setas: → vs ↦
• igualdade extensional vs intensional
• «aquele x tal que»
• definição por casos
• abstração com buracos
• funções de ordem superior
• currificação e descurrificação
• aplicação parcial
• $∣B^A∣=∣B∣^{∣A∣}$

CFR1 (8) [video]

• recap: currificação e associatividades sintácticas
• de buracos para lambdas
• como funciona um cálculo
• funções anônimas e compração com set builder
• semântica vs sintaxe, nomes de símbolos vs nomes de noções
• a notação lambda
• metáforas com almas e corpos
• Q: funções anônimas de aridades maiores?
• Q: buracos vs lambdas e ordem dos parametros
• parenteses implícitas e convenções
• sobre binding e ocorrências de variáveis livres
• dois exemplos de abstrações e inferência de tipos polimórfica
• o açúcar sintáctico λ(x,y).coisa
• como cálcular: β-redex, β-redução
• chegando à idéia do α-renomeamento
• introdução de lambdas em linguagens de programação “populares”
• plicker: calcule a expressão-λ
• sobre a η-conversão

hw.7

1. Capítulo «Funções»: até §«Currificação»
2. Ache as noções de conjuntos que correspondem às: 0, 1, (+), dos números.
3. Demonstre as “igualdades-entre-aspas” correspondentes às leis conhecidas desde ensino fundamental.

CFR1 (9) [video]

• recap: curry & uncurry
• operações de números vs operações de conjuntos
• igualdade-entre-aspas de conjuntos
• mais leis e mais conceitos para investigar
• sobre a idéia de «usar conjuntos para fundamentar a matemática»?
• Funções de graça
• função identidade
• função inclusão
• Podemos considerar, sendo conjuntistas, que ℕ⊆ℤ?
• não é ousadia usar o nome identidade?
• plicker: calcule uma expressão-λ

CFR1 (10) [video]

• recap: λ, β, η, α
• η-conversão
• Como interpretar uma função aplicada nela mesmo
• Manifestações dos β,η para outros tipos: conjuntos e 2-tuplas
• função-imagem
• função-pré-imagem
• sobre composição
• Plicker: a função-imagem respeita uniões e interseções?

hw.8

1. Capítulo «Funções»: até §«Funções de graça»

CFR1 (11) [video]

• inversão de função
• injetividade, sobrejetividade, bijetividade
• funções de graça: f×g
• um desafio parecido: duas funções com o mesmo domínio
• tentando definir uma f∪g, em forma parecida
• o que podemos inferir sobre duas funções, sabendo que sua composição é bijetiva?

hw.9

1. §«Jecções: injecções, sobrejecções, bijecções»
2. Problemas: Π8.5, Π8.6, Π8.14, Π8.17

CFR1 (12) [video]

• função constante vs função invariável
• iterações de endomapas
• associatividade de composição
• composição respeita as -jetividades
• definições e demonstrações com pontos
• botando na mesa as definições recursivas

CFR1 (13) [video]

• Partições e coberturas de conjuntos
• Diagramas comutativos
• Leis da composição (assoc. e ident.)
• [tacit-programming][Estilo tácito] (aka: point-free, pointless)
• a função const : β → α → β e um desafio
• Uma das leis de identidade descrita como diagrama comutativo
• id é uma identidade para a composição
• recap: funções e diagramas relacionados ao produto (×)
• única função que faz um diagrama comutar
• união disjunta: no caminho de achar a soma de conjuntos
• Plicker: a ℘f respeita as uniões e as interseções?

hw.10

1. Seja (~) uma relação de equivalência num conjunto $A$. Para qualquer $a ∈ A$, denote por $[a]_{\sim}$ o conjunto $\{x \mid x \sim a \}$. O $\{ [a]_{\sim} \mid a \in A \}$ é uma partição do $A$?
2. Alguém definiu: «Uma partição num conjunto A é uma função …». Adivinhe o … e justifique tal frase!
3. Defina uma ordem interessante no Partition(A).
4. Demonstre que se os dois quadradinhos do diagrama da aula comutam, o diagrama todo comuta.
5. Qual deve ser a próxima pergunta para perguntar depois de descubrir que const = curry outl?
6. Demonstre as leis de composição estilo point-full.
7. Qual seria a especificação do produto?
8. Qual seria a especificação de soma?
9. Tente achar outras implementações de união-disjuntora (soma)
10. Quais seriam os diagramas e funções relacionados à união-disjuntora?
11. Melhore nossa definição de iterações de funções, e demonstre umas propriedades interessantes sobre elas.
12. Até §«Definições estilo point-free»
13. Reveja a §«Funções de graça» e seus exercícios.
14. Problemas: Π8.12; Π8.13; Π8.14; Π8.16; Π8.19; Π8.20; Π8.22

CFR1 (14) [video]

• Fixpoints
• Definindo iterações melhor (sem pontos)
• Mais funções de graça: pointwise, diagonal, pareamento, produto
• Uma vantagem de usar funções descurrificadas
• conjuntista-vs-tipista sobre funções (e pouco em geral)
• implementações usando funções
• funções parciais e não-deterministas
• união-disjunta: especificação-vs-implementação, copareamento, coproduto

CFR1 (15) [video]

• equações recursivas como sistemas de incógnitos
• mais funções de graça: função caraterística

hw.11

1. §«Funções parciais»
2. §«Funções inversas»
3. §«Definições recursivas»
4. Problemas: Π8.7; Π8.8; Π8.9; Π8.10; Π8.11; Π8.30

Prova CFR1.2