2023.2 FMC1, turma de Thanos

Pontos de participação

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

1. Capítulo 1

2023-08-21: IntroProof

1. 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.
2. Complete o «Tutorial World» do Natural Number Game. Veja o FAQ relevante também. Salve este progresso no teu github.
3. Capítulo 2: até o primeiro intervalo de problemas
4. 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!
   1. Proposições de dupla negaço:
      1. P ⇒ ¬¬P
      2. ¬¬P ⇒ P
   2. Comutatividade dos ∨,∧:
      1. (P ∨ Q) ⇒ (Q ∨ P)
      2. (P ∧ Q) ⇒ (Q ∧ P)
   3. Proposições de interdefinabilidade dos ⇒,∨:
      1. (P ⇒ Q) ⇒ (¬P ∨ Q)
      2. (P ⇒ Q) ⇐ (¬P ∨ Q)
      3. (P ∨ Q) ⇒ (¬P ⇒ Q)
      4. (P ∨ Q) ⇐ (¬P ⇒ Q)
   4. Proposições de contraposição:
      1. (P ⇒ Q) ⇒ (¬Q ⇒ ¬P)
      2. (¬Q ⇒ ¬P) ⇒ (P ⇒ Q)
   5. A irrefutabilidade do LEM:
      1. ¬¬(P∨¬P)
   6. A lei de Peirce e sua versão “fraca”:
      1. ((P ⇒ Q) ⇒ P) ⇒ P
      2. ((P ⇒ Q) ⇒ P) ⇒ ¬¬P
   7. Proposições de interdefinabilidade dos ∨,∧:
      1. P∨Q ⇒ ¬(¬P∧¬Q)
      2. P∨Q ⇐ ¬(¬P∧¬Q)
      3. P∧Q ⇒ ¬(¬P∨¬Q)
      4. P∧Q ⇐ ¬(¬P∨¬Q)
   8. As leis de De Morgan para ∨,∧:
      1. ¬(P∨Q) ⇒ (¬P ∧ ¬Q)
      2. ¬(P∨Q) ⇐ (¬P ∧ ¬Q)
      3. ¬(P∧Q) ⇒ (¬Q ∨ ¬P)
      4. ¬(P∧Q) ⇐ (¬Q ∨ ¬P)
   9. Proposições de distributividade dos ∨,∧:
      1. P∧(Q∨R) ⇒ (P∧Q)∨(P∧R)
      2. P∧(Q∨R) ⇐ (P∧Q)∨(P∧R)
      3. P∨(Q∧R) ⇒ (P∨Q)∧(P∨R)
      4. P∨(Q∧R) ⇐ (P∨Q)∧(P∨R)
   10. Currificação
       1. ((P∧Q)⇒R) ⇒ (P⇒(Q⇒R))
       2. ((P∧Q)⇒R) ⇐ (P⇒(Q⇒R))
   11. Reflexividade da ⇒:
       1. P ⇒ P
   12. Weakening and contraction:
       1. P ⇒ (P∨Q)
       2. Q ⇒ (P∨Q)
       3. (P∧Q) ⇒ P
       4. (P∧Q) ⇒ Q
       5. P ⇒ (P∧P)
       6. (P∨P) ⇒ P
   13. As leis de De Morgan para ∃,∀:
       1. ¬(∀x)[φ(x)] ⇒ (∃x)[¬φ(x)]
       2. ¬(∀x)[φ(x)] ⇐ (∃x)[¬φ(x)]
       3. ¬(∃x)[φ(x)] ⇒ (∀x)[¬φ(x)]
       4. ¬(∃x)[φ(x)] ⇐ (∀x)[¬φ(x)]
   14. Proposições de interdefinabilidade dos ∃,∀:
       1. (∃x)[φ(x)] ⇒ ¬(∀x)[¬φ(x)]
       2. (∃x)[φ(x)] ⇐ ¬(∀x)[¬φ(x)]
       3. (∀x)[φ(x)] ⇒ ¬(∃x)[¬φ(x)]
       4. (∀x)[φ(x)] ⇐ ¬(∃x)[¬φ(x)]
   15. Proposições de distributividade de quantificadores:
       1. (∃x)[φ(x) ∧ ψ(x)] ⇒ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
       2. (∃x)[φ(x) ∧ ψ(x)] ⇐ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
       3. (∃x)[φ(x) ∨ ψ(x)] ⇒ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
       4. (∃x)[φ(x) ∨ ψ(x)] ⇐ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
       5. (∀x)[φ(x) ∧ ψ(x)] ⇒ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
       6. (∀x)[φ(x) ∧ ψ(x)] ⇐ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
       7. (∀x)[φ(x) ∨ ψ(x)] ⇒ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]
       8. (∀x)[φ(x) ∨ ψ(x)] ⇐ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]
5. Instale no seu computador: Lean, Haskell, Agda

2023-08-27: IntroProof

1. Infira a simetria e a transitividade da igualdade a partir das reflexividade e substituição.
2. Capítulo 2: inteiro

2023-08-28: IDMa

1. Capítulo 3: até o Exercício x3.6

2023-09-02: IRI

1. 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.
2. Defina (sem consulta) a adição, a multiplicação, e a exponenciação.
3. Defina uma função double que retorna o dobro da sua entrada.
4. Calcule os:
   1. double (double (S O))
   2. double ((S O) + (S (S O)))
5. Demonstre uma das: (·)-idL, (·)-idR
6. Demonstre uma das: (^)-idL, (^)-idR
7. 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 a pred em outras definições, estava errando
8. Defina as funções:
   1. fact : Nat → Nat
   2. fib  : Nat → Nat
   3. min  : Nat × Nat → Nat
   4. max  : Nat × Nat → Nat
   5. div  : Nat × Nat → Nat × Nat
   6. quot : Nat × Nat → Nat
   7. rem  : Nat × Nat → Nat
   8. gcd  : Nat × Nat → Nat
   9. lcm  : Nat × Nat → Nat

2023-09-04: IDMa

1. Capítulo 3: até Θ3.13

2023-09-09: IDMa

1. Capítulo 3: até x3.14

2023-09-09: IRI

1. Capítulo 4: até o §«Demonstrando propriedades de naturais com indução»

2023-09-11: IDMa

1. Capítulo 3: até §«Divisibilidade»

2023-09-11: IRI

1. Capítulo 4: até o §«Ordem nos naturais»

2023-09-12: IntroProof

1. 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 os sorry, do arquivo com código que compila para demonstrar tudo. Dúvidas nos #proofassistants e #tech, obviamente! ntroProof

2023-09-13: IRI

1. (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!
2. 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

1. Capítulo 3: até §«Ordem e positividade»

2023-09-20: IRI

1. Capítulo 4: até o §«Empty»
2. Defina os operadores booleanos.
3. Como definarias uma função if_then_else_ : Bool → Nat → Nat → Nat?
4. 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
5. Demonstre que a leq : Nat → Nat → Prop é: reflexiva; transitiva; antissimétrica; total
6. Demonstre que todo Nat é par ou ímpar.

2023-09-23: IDMa

1. Capítulo 3: até o primeiro intervalo de problemas.

2023-09-25: IDMa

1. 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$.
2. Demonstre que um conjunto vazio é subconjunto de qualquer conjunto.
3. Demonstre ou refute: «o Ø é bem-ordenado».
4. Demonstre ou refute: «qualquer conjunto de inteiros X finito é bem ordenado».
5. Demonstre como teorema o princípio de indução.
6. Demonstre como corolário o princípio de indução “shiftado” (i.e., a partir dum inteiro ℓ)
7. Demonstre como corolário o princípio de indução com 2 bases.
8. Enuncie e demonstre um princípio de indução “flippado”, para demonstrar que todo inteiro negativo “é legal”

2023-09-28: IRI

1. 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
2. Defina as:
   • head        : ListNat → Nat
   • tail        : ListNat → ListNat
   • init        : ListNat → ListNat
   • last        : ListNat → Nat
3. Defina a (<) : Nat → Nat → Prop e sua internalização, e demonstre a sua corretude.
4. Implemente como Nats:
   1. os inteiros (já sabes a sua especificação pelo IDMa!)
   2. os parzinhos-de-Nats
   3. os vetores-de-Nats como Nat
5. Implemente como novo tipos, tendo já definido o Nat:
   1. os inteiros
   2. os parzinhos-de-Nats
   3. os vetores-de-Nats como Nat

2023-10-04: IRI

1. Enuncie (sem olhar) como regras de inferência os princípios de indução para os: ListNat, Nat, Bool, Unit, Empty.
2. Demonstre os teoremas (escolhe algo interessante para botar nos ??)
   1. (∀xs,ys:ListNat)        [ sum (xs ++ ys) = ?? ]
   2. (∀xs,ys:ListNat)        [ product (xs ++ ys) = ?? ]
   3. (∀ℓ:ListNat)            [ length (filterEven ℓ ++ filterOdd ℓ) = ?? ]
   4. (∀ℓ:ListNat)            [ reverse (filterEven ℓ) = ?? ]
   5. (∀n:Nat)(∀ℓ:ListNat)    [ length (addNat n ℓ) = ?? ]
   6. (∀n:Nat)(∀ℓ:ListNat)    [ sum (addNat n ℓ) = ?? ]
   7. (∀n:Nat)(∀ℓ:ListNat)    [ sum (multNat n ℓ) = ?? ]
   8. (∀n:Nat)(∀ℓ:ListNat)    [ product (multNat n ℓ) = ?? ]
   9. (∀n:Nat)(∀ℓ:ListNat)    [ product (expNat n ℓ) = ?? ]
   10. (∀n:Nat)(∀ℓ:ListNat)    [ isSorted (addNat n ℓ) = ?? ]
   11. (∀ℓ:ListNat)            [ isEven (product ℓ) = anyEven ℓ ]
   12. (∀ℓ:ListNat)            [ isEven (sum ℓ) = isEven (length (filterOdd ℓ)) ]
   13. (∀ℓ:ListNat)            [ isZero (sum ℓ) = ?? ]
   14. (∀ℓ:ListNat)            [ isZero (product ℓ) = ?? ]
   15. (∀n,m:Nat)(∀ℓ:List Nat) [ addNat (n + m) ℓ = ?? ]
   16. (∀n,m:Nat)(∀ℓ:List Nat) [ multNat (n · m) ℓ = ?? ]
3. Demonstre também:
   1. (∀xs,ys:ListNat)        [ length (xs ++ ys) = ?? ]
   2. (∀xs,ys:ListNat)        [ reverse (xs ++ ys) = ?? ]
   3. (∀n:Nat)(∀xs,ys:ListNat)[ addNat n (xs ++ ys) = ?? ]
   4. (∀ℓ:ListNat)            [ reverse (reverse ℓ) = ?? ]
   5. (∀ℓ:ListNat)            [ length (reverse ℓ) = ?? ]
   6. Associatividade da (++)
   7. [] é uma (++)-identidade
4. Pense em mais propriedades, enuncie, e demonstre!
5. (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):
   1. (∀x:A)[φ ⇒ ψ(x)] ⇐≟⇒ φ ⇒ (∀x:A)[ψ(x)]
   2. (∀x:A)[φ(x) ⇒ ψ] ⇐≟⇒ (∀x:A)[φ(x)] ⇒ ψ
   3. (∃x:A)[φ ⇒ ψ(x)] ⇐≟⇒ φ ⇒ (∃x:A)[ψ(x)]
   4. (∃x:A)[φ(x) ⇒ ψ] ⇐≟⇒ (∃x:A)[φ(x)] ⇒ ψ

2023-10-09: IDMa

1. Π5.9; Π5.17

2. 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:

   1. (≤) no mundo dos inteiros
   2. (⊆) no mundo dos Set α

3. Resolva a Prova 2.X do 2019.2.

2023-10-13: IRI

1. 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

1. Demonstre a corretude do algoritmo de Euclides para achar o m.d.c. (use a versão com os restos).

2023-10-16: IDMa

1. Resolva (finalmente) o 2023-10-09.hw2, junto com a nova questão sobre o (⊢): traduza o “m.d.c.” para…
   1. o mundo dos inteiros, com a pré-ordem (≤)
   2. o mundo dos Set α, com a pré-ordem (⊆)
   3. o mundo das Props, com a pré-ordem (⊢)
2. 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!
3. Implemente o algoritmo de euclides em Haskell, incluindo sua versão estendida com tipo Int × Int → Int × Int × Int.
4. 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»:
   1. 10668127, 159451
   2. 252121, 318719
5. Para cada uma das equações, ache x, y que a satisfazem:
   1. 1 = 127x + 73y
   2. 6 = 321x + 312y

2023-10-18: IDMa

1. Capítulo 3: até a «§57. Invertíveis, units, sócios»

2023-10-23: IDMa

1. 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!
2. Capítulo 3: até a «§70. Exponenciação»
3. $a$ invertível módulo $m$ sse (a,m) = 1.
4. Unicidade de inversos módulo $m$.
5. Mostre que (≡ₘ) é uma congruência para a estrutura algébrica dos inteiros
6. Mostre que a (≡ₘ) não é compatível com a exponenciação.
7. Encontre um inverso de 18, módulo 125.
8. Encontre inteiro x tal que $6^{1032} \equiv x \pmod {11}$.
9. Dados inteiros $a,b,m$ quantas multiplicações tu precisa fazer para achar um inteiro $x$ tal que $a^b \equiv x \pmod m$?
10. (qm + r, m) = (r,m)
11. (a,nm) = 1 ⇔ (a,m) = 1 & (a,n) = 1

2023-10-26: IDMa

1. Querendo escrever um guia para alunos (ou maquinas!) saber como resolver congruências e sistemas de congruências, o que tu escreveria sobre:
   1. $\phantom a x \equiv b \pmod m$
   2. $ax \equiv 1 \pmod m$
   3. $ax \equiv b \pmod m$
   4. Um sistema de $n$ congruências $x \equiv b_i \pmod {m_i}$. (Dica: resolva primeiro para o caso $n = 2$.)
2. Demonstre que existe uma infinidade de primos «da forma 4n+3».
3. Depois de resolver o problema anterior, explique por que sua resolução não é adaptável para primos «da forma 4n+1».
4. Demonstre: p primo ⇔ (p-1)! ≡ -1 (mod p).

2023-10-26: IRI

1. Demonstre as leis de Functor para o List : Type → Type com o map que definimos:

   map id = id                  [functor law 1]
   map (f . g) = map f . map g  [functor law 2]
   

2. Demonstre:

   (∀f:α→β)(∀p:β→Bool)  [ filter p ∘ map f = map f ∘ filter (p ∘ f) ]
   

3. 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 = 
   

4. 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)
   

5. 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
   

6. 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

1. Demonstre o teorema de Wilson
2. Demonstre que para todo inteiro m, se o teste q-Fermat diz não, então pelo menos metade dos {1,…,m}-Fermat dizem não também
3. Seja $R_m = \{r_1,\dotsc,r_{\varphi(m)}\}$ é um sistema reduzido de resíduos módulo $m$. Demonstre:
   1. Se (a,m)=1, então aRₘ também é um s.r.r. módulo m.
   2. $\sum_{r\in R_m} r \equiv 0 \pmod m$.
   3. Rₘ é (·)-“fechado módulo m”.
   4. (∀r ∈ Rₘ)(∀x ∈ ℤ)(∃u ∈ ℤ)[ x ≡ₘ ru ]
4. (a,nm) = 1 ⇔ (a,m) = 1 & (a,n) = 1
5. φ(p) = p-1
6. φ(pᵏ) = pᵏ - pᵏ⁻¹
7. Calcule um dos φ(2), φ(3), φ(4), …, φ(13)
8. φ é multiplicativa, ou seja: (m,n)=1 ⇒ φ(mn) = φ(m) φ(n).
9. Calcule de novo, essa vez todos os φ(2), φ(3), φ(4), …, φ(13). (Não se engane: fatoração demora!)
10. φ(n) é par para qualquer n > 2.
11. Calcule o valor do somatório $\sum_{i=0}^k \varphi(p^i)$.
12. $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

1. Capítulo 6: até o §«Ordem e positividade»

2023-11-15: IDMa

1. Capítulo 3: até o fim.

2023-11-15: IDMb

1. Capítulo 6: até o §«Valor absoluto»
2. 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

1. Capítulo 6: até o §«Mínima e máxima»

2023-11-22: IRI

1. Investigue para cada um dos seguintes se pode ser munido com um fmap para conseguir ser um Functor:
   1. (δ →) : Type → Type
   2. (→ γ) : Type → Type
   3. (α ×) : Type → Type
   4. (× β) : Type → Type
   5. (α +) : Type → Type
   6. (+ β) : Type → Type
   7. Id    : Type → Type
   8. K κ   : Type → Type
2. Investigue: composição de functors é functor?

2023-11-24: IDMb

1. Capítulo 6: até o §«Sobre modelos»

2023-11-24: IDMb

1. Capítulo 6: até o §«Infimum e supremum» (obs: re-restude o §«Distância» pois atualizei).

2023-12-04: IRI

1. Resolva a Prova 2.3 do self/iri.
2. Capítulo 4:
   • §106 «Functors»
   • §107 «Arvores»
   • §109 «Um toque de complexidade»
   • §110 «Eficiência via indução»
3. Arvores
4. 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
5. Adivinhe uma conexão entre o número size t e o número nodes t: enuncie e demonstre!
6. Θ. depth ≤ length ∘ flatten (← o que significa isso?)
7. Θ. forks t ≤ 2 ^ depth t
8. Verifique que tu passou EM & ME mesmo, reescrevendo o que demonstrou acima utilizando log₂
9. Defina o resto dos tipos de arvores discutidos nas aulas (peça detalhes no Zulip!)
   1. LabBinTree α β
   2. GenTree α
10. Demonstre como todos teus típos de árvores viram Functors
11. Demonstre:
    1. length ∘ flatten = ??
    2. flatten ∘ mirror = ??
    3. mirror ∘ mirror = ??
    4. depth ∘ mirror = ??
    5. depth ∘ fmap f = ??
    6. fmap f ∘ mirror = ??
    7. fmap f ∘ flatten = ??
12. Eficiência “por indução” / parametro acumuladora: use a metodo que encontramos na aula eliminando o (⧺) da reverse para:
    1. eliminá-lo da tua flatten
    2. eliminá-lo da tua leaves

2023-12-04: IDMb

1. Resolva a Prova 3.1 do self/idmb.
2. Θ. eventualmente convergente ⇔ convergente

2023-12-11: IRI

1. Defina uma foldT para os tipos de arvores que faz sentido definir
2. Defina uma foldE para os tipos de Either
3. Discuta qual deveria ser o tipo de uma unfold que cria listas a partir de outros valores; depois defina!
4. reverse (xs ⧺ ys) = reverse ys ⧺ reverse xs
5. 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
  1. Resolva sozinho os teoremas seguintes que demonstramos na aula passada:
     1. (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ + bₙ)ₙ → ??
     2. (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙbₙ)ₙ → ??
  2. …e o resto do Θ. Comportamento algébrico de limites:
     1. (aₙ)ₙ → a ⇒ (caₙ)ₙ → ??
     2. ?? & (bₙ)ₙ → b ⇒ (bₙ⁻¹)ₙ → ??
     3. ?? & (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ/bₙ)ₙ → ??
     4. (aₙ)ₙ → a & ?? ⇒ (aₙᵏ)ₙ → ??
  3. Θ. conv ⇒ autoconv
  4. Θ. autoconv ⇒ cotada
  5. C. conv ⇒ cotada
  6. Θ. autoconvergente com subseq convergente ⇒ convergente
  7. Θ. 0 < ϑ < 1 ⇒ (ϑⁿ)ₙ → ??
  8. Θ. 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.
• Reais (oficiais) (v3/3), com completude via cotado: sup-cotado ⇒ sup
  1. «Agora sim!» Demonstre os: Nested Interval Property de Cantor; Monotone Convergence Theorem; Bolzano–Weierstrass Theorem; Cauchy convergence critérion
     1. Θ. (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]
     2. Θ. (MC): cotada & “monótona” ⇒ convergente
     3. Θ. (BW): cotada ⇒ conv subseq
     4. Θ. (CC): autoconvergente ⇒ convergente
  2. Αρχιμήδης:
     1. Θ. Os reais naturais não são cotados
     2. Θ. (∀ε>0)(∃n)[ 1/n < ε ]
     3. Θ. (∀ε>0)(∃n)[ nε > 1 ]
     4. Θ. (∀ε>0)[ε$\mathbb R_{\mathbb N}$ não é cotado]
     5. Θ. (∀s>0)(∀b)(∃n)[ b < ns ]
     6. Θ. (∀b)(∀s>0)(∃n)[ ns > b ]
     7. Q. Há diferença entra as duas últimas? Como chamarias cada uma no «nível coração»?
  3. Existência de raizes
     1. Θ. 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?
     2. Θ. «Ἵππασος 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 por h² + (algo controlavelmente pequeno), e logo por 2, contradizendo a parte de «cota superior».
        • Dica 5: Para eliminar caso h² > 2: calcule o (h - 1/n)² para conseguir infcotá-lo por h² - (algo controlavelmente pequeno), e logo por 2, contradizendo a parte de «melhor».
     3. Θ. Existência das raizes ²√
     4. Θ. Existência das raizes ᵏ√
  4. Densidades:
     1. Θ. dos reais racionais nos reais
     2. Θ. dos reais irracionais nos reais

2023-12-18: IDMb

1. Criar seu próprio gabarito para a Prova 3.2

2023-12-18: IRI

1. Criar seu próprio gabarito para a Prova 2.3
2. O que precisa mudar para a linguagem ArEx saber lidar com expressões envolvendo variáveis como a 3(x₂ + 2x₀) + 4x₂x₇, e nas eval e step?
3. 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. e Split.
• 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 de Nat: 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 (ou Nil) e Cons
• 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 o product []
  • 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)