self study IRI: Introdução à Recursão e Indução

Sessões

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.

IRI (1) [video]

• introdução
• 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
• sintaxe: o que queremos descrever
• o desafio dos «…» numa definição
• exemplo de chefe de programação sem noção comunicando pedido
• Naturais vs Nats; Números vs Numerais
• Linguagem vs Metalinguagem; Variáveis vs Metavariáveis
• «Nada mais»
• 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
• casamento de padrão com expressão: primeiro encontro
• gramáticas e a notação BNF: nada demais!
• Mal entendido: «os inteiros que a gente conheceu»—Nope.
• Mal entendido: «uns inteiros são naturais»—Nope.
• type casting
• a aplicação duma função no seu argumento, e a inferncia de tipo relevante
• Tem como implementar os inteiros usando os naturais, e mais uns teasers
• Regras e arvores de inferência, comandos vs proposições
• Um exemplo de inferência: SSSO : Nat
• Definição recursiva vs tijolo
• um exemplo: fact : Nat → Nat
• Como traduzir uma linha sem premissas para código

hw

1. Jogue o NNG. Tente completar o mais rápido possivel; sua entregá é a Prova 2.2. Veja o FAQ relevante também.

IRI (2) [video]

• ocorrências livres e ligadas de variáveis
• construtor vs função
• uns açúcares sintácticos
• uns preconceitos sobre funções e sua notação
• ocorrências ligadas e livres de variáveis
• double : Nat → Nat; id : Nat → Nat
• padrões de argumentos
• o presente da recursão
• Como calcular (modelo computacional)
• double 2 = ?
• valores canônicos
• casamento de padrões
• Duas maneiras de escrever cálculos
• A adiçaõ: (+)
• prefix, postfix, infix, mixfix
• Um cálculo e teorema: 2 + 3 ≟ 5
• Arvore sintáctica (Abstract Syntax Tree), parsing, (veja também: lexer)
• Precedência sintáctica
• Associatividade sintáctica
• Associatividade vs associatividade sintáctica: axiomas e especificação vs implementação
• Currificação
• como definir o addFive nível boss
• Aplicação parcial

hw

1. Calcule os:
   1. double (double (S O))
   2. double ((S O) + (S (S O)))
2. Defina multiplicação e exponenciação.
3. Olhando para as funçoẽs binárias e famosas que temos até agora (adição, multiplicação, exponenciação), perceba que tem um “padrão”. Use isso para definir a “próxima” operação. Denote por ⇈.
4. Defina a função Pd : 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 usou a Pd em outras definições, estava errando
5. Defina a função ∸ : Nat → Nat → Nat que comporta como subtração, mas caso que o resultado era pra ser negativo, retorna O mesmo.
6. Defina as funções:
   1. fact : Nat → Nat
   2. fib  : Nat → Nat
   3. dist : Nat → Nat → Nat
   4. min  : Nat → Nat → Nat
   5. max  : Nat → Nat → Nat
   6. div  : Nat × Nat → Nat × Nat
   7. quot : Nat × Nat → Nat
   8. rem  : Nat × Nat → Nat
   9. gcd  : Nat × Nat → Nat
   10. lcm  : Nat × Nat → Nat
   11. comb : Nat → Nat → Nat
   12. perm : Nat → Nat → Nat

IRI (3,4) [video]

• construtor vs função
• D: multiplicação
• o uso de lemmas: m-idR, e-idR
• uma demonstração simples: (·)-idR
• ∀: como usar
• ∀: como atacar
• 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
• acordos sintácticos sobre a aplicação-de-função: precedência, associatividade sintáctica à esquerda: f x y z ≡ ((f x) y) z, e os seus porquês
• Θ. Associatividade da (+)
• A disjunção escondida em cada Nat.
• ∃: como usar
• ∨: como usar
• tem como continuar a demonstração?
• escolhendo variáveis com «linhas»: x’, x’’, etc.
• igualdade entre Nats
• o problema que temos demonstrando esse teorema

hw

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 )
   

IRI (5): Nat [video]

• dois princípios sobre os construtores e os valores construidos
• escolhendo o padrão na direita duma equação para substituir na direção (←)
• o problema que temos demonstrando a (+)-associatividade
• A regra de inferência Ind-φ. (Onde φ : Nat → Prop.)
• Demonstração por indução
• A associatividade da (+): umas demonstrações por indução diferentes.
• Análise das duas melhores demonstrações da (+)-associatividade: legalzinho vs legalzão
• Inventar teoremas-propriedades sobre nossos programas

hw

1. Resolva tudo na §«Demonstrando propriedades de naturais com indução»
2. Asserte propriedades sobre teus programas do hw do IRI (2), e demonstre cada uma delas!
3. Enuncie e demonstre que quaisquer fibonaccis consecutivos são coprimos.

IRI (6,7): Nat, Bool [video]

• currificação: versão currificada vs descurrificada da mesma função
• associatividade sintáctica
• inferência de tipo de aplicação de função
• conexão com uso de implicação; propositions-as-types
• 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
• O uso de underscore nos padrões
• uma convenção sobre a ordem de equações numa definição recursiva
• Sobre funções parciais vs totais
• side effects (efeitos colaterais) e funções puras
• Type inference; como/quando aproveitar a inferência de tipos
• even e odd (pares e impares): como internalizar e como demonstrar corretude
• ev, od : Nat → Bool
  • treis maneiras diferentes de definir: precisando 3 equações; precisando o not; com recursão mútua
• recursão mútua
• backticks para notação infixa
• Como usar o underscore (_) como «variável sem nome» num padrão.

hw

1. 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
   • congmod : ?
   • isZero  : Nat → Bool
2. Demonstre que a (≤) : Nat → Nat → Prop é: reflexiva; transitiva; antissimétrica; total
3. Demonstre que todo Nat é par ou ímpar.
4. Defina os operadores booleanos.
5. Como definarias uma função if_then_else_ : Bool → Nat → Nat → Nat?
6. Demonstre a corretude das funções definidas no hw do IRI (2).
7. O lemma de divisão de Euclides para os Nats:
   • enuncie
   • demonstre

Prova 2.2

Complete o NNG.

IRI (8): Nat, Bool, Weekday, Unit, Empty, ListNat [video]

• Type synonym
• Desafio: Int parzinhos-de-Nats, vetores-de-Nats
• isBool : Nat → “Bool”
• O que acontece em linguagem que autoafirmam ter «tipos dinâmicos»
• Corretude de definição de função (programa): correção e completude
• Mais tipos de dados simples: Weekday
• O tipo Unit com seu único habitánte/construtor: ⋆ : Unit
• Quem é mesmo esse void?
• Indução do Nat e quando não usar
• Q: faz sentido adicionar como açúcar sintáctico para o lem n m assumir papel de Prop? A: Não.
• Como implementar listas: ListNat
• Os construtores Empty (ou Nil) e Cons
• ListNat: sintaxe, açúcar e associatividade sintáctica
• Como escolher a ordem dos argumentos: aplicação parcial e currificação
• ListNat é um tipo recursivo
• Como representar a lista [2,0,8] com nosso tipo
• definindo a length : ListNat → Nat
• Calculando o length [3,2,0]
• Plicker: quantos construtores preciso para definir o tipo Int?

hw

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

IRI (9): Nat, Bool, Unit, Empty, ListNat [video]

• Definições de sum : ListNat → Nat e product : ListNat → Nat
  • como escolher o valor certo para o sum [] e o product []
• reverse, append, e concatenação binária (⧺)
• parenteses e convenções sintácticas do ␣
• mal-entendido entre função currificada-vs-descurrificada e notação infixa-vs-prefixa
• aplicação parcial e um cálculo relacionado
  • «redex»
• a notação de “sections” de operadores binários
• um problema com as head e tail
• um teaser sobre a soma de tipos
• Construtores vs Destrutores
• Corretude de programas sobre ListNat: propriedades que gostariamos de demonstrar
• Tentativa de demonstrar uma delas
• Como chegar aos principios de indução para os outros tipos
• O conceito de «respeitar/preservar uma propriedade».
• Do $\mathrm{Ind}^{\mathsf{Nat}}_{\varphi}$ para o $\mathrm{Ind}^{\mathsf{ListNat}}_{\varphi}$.
  • Indução do Bool
  • Indução do Unit
  • Indução do Empty
  • Indução do ListNat
• Como interpretar a indução e suas várias versões dos inteiros agora
• Uma maneira de pensar sobre indução: como separação-em-casos-com-extras
• Conexão entre recursão e indução
  • Definição por recursão vs Demonstração por indução
  • O presente de recursão vs o presente da indução
• Quantos quantificadores e por quê?
• Quantos destrutores e por quê?

hw

1. 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) ℓ = ?? ]
2. 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
3. Pense em mais propriedades, enuncie, e demonstre!
4. (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)] ⇒ ψ

Prova 2.1 (IRI)

IRI (10a) [video]

• Polimorfismo de tipos, e o type constructor List : Type → Type
• Construtores de tipos (type constructors) vs Construtores de valores (data constructors)
• type variables vs data variables
• polimorfismo: de lengthNat : List Nat → Nat para length : List α → Nat

hw

1. Generalize todas as funções dos hw 2022-11-04 e 2022-10-31 que envolvem ListNat para funções que envolvem List α ou, se não for possível, List Nat.
2. Defina as:
   • concat     : List (List α) → List α
   • ifthenelse : Bool → α → α → α
   • and        : List Bool → Bool
   • or         : List Bool → Bool
   • splitAt    : Nat → List α → (List α × List a)
   • zip        : List α → List β → List (α × β)
   • unzip      : List (α × β) → (List α × List β)
3. Defina um tipo para conseguir uma resolução no problema de querer listas cujos membros podem ser Nat ou Bool.
4. Defina um tipo cujos habitantes serão usados para representar listas que garantam:
   1. ter tamanho ≥ 1 (IList)
   2. ter tamanho par (EList)
   3. ter tamanho ímpar (OList)

mais hw

1. URGENTE! Continua (ou começa, pelamor de Curry) o hw do IRI (3,4), para incluir as funções que envolvem listas. O arquivo poderia começar assim:

   {-# LANGUAGE GADTs, EmptyDataDecls #-}
   
   module IRI where
   
   data Nat where
       O :: Nat
       S :: Nat -> Nat
     deriving (Eq, Show) 
   
   data Unit where
       Star :: Unit
   
   data Empty
   
   data List a where
       Nil  :: List a
       Cons :: a -> List a -> List a
     deriving (Eq, Show) 
   
   

IRI (10b, 11) [video]

• polimorfismo: função(ões) id
• o tipo de bottom
• Nats bottomosos (⊥, nats parciais, o nat infinito)
• mais um tira-gosto/teaser da idéia de propositions-as-types
• funções de ordem superior (higher-order functions)
• como agir se precisar numa lista ter naturais e booleanos: NatOrBool
• abstração de ordem superior: de addNat : Nat → List Nat → List Nat para mapNat : (Nat → Nat) → List Nat → List Nat
• abstração de ordem superior: de mapNat : (Nat → Nat) → List Nat → List Nat para map : (α → β) → List α → List β
• 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}$.
• o Maybe : Type → Type
• comparação dos tipos Maybe (List α) e List (Maybe α)
• Idéia ruim: usar um valor arbitrário para o head []
• as versões não-gambiarrosas de head e tail
• Resolução legal: safeHead : List α → Maybe α
• Resolução legal: safeTail : List α → Maybe (List α)
• desafio: como generalizar as sum, product, concat
• por que não podemos tipar a sum com List α → α?
• Uma find melhor que as gambiarras C’osas: findFirst : α → List α → Maybe α

hw

1. Gambiarra 1: safeHead : ListNat → ListNat
2. Gambiarra 2: safeHead : ListNat → Bool × Nat
3. Gambiarra 3: defaultHead : Nat → ListNat → Nat

mais hw

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 α
   • head        : List α → Maybe α
   • tail        : List α → Maybe (List α)
   • init        : List α → Maybe (List α)
   • last        : List α → Maybe α
   • pick        : Nat → List α → Maybe α
   • findFirst   : α → List α → Maybe Nat
   • find        : α → List α → List Nat
   • curry       : ?
   • uncurry     : ?
   • flip        : ?
2. Qual seria uma melhor tipágem para a pw : (α → α → α) → List α → List α → List α?

mais hw

1. Descubra o foldNat: defina e mostre um uso dele

IRI (12,13) [video]

• os destrutores são, em geral, parciais; versões seguras
• de NatOrBool para Either α β
• Produto de tipos: α × β
• Soma de tipos (coproduto): α + β
• O que usar para representar erros em vez de gambiarras tipo Strings e Números
• pw (zipWith, zip; veja sobre zipping)
• findFirst: primeira tentativa
• uma idéia sobre como resolver nosso problema: (⟨$⟩)/fmap
• uma outra idéia sobre como resolver nosso problema: pattern matching: match-expression
• de volta para a primeira idéia: fmap e Functors
• Functors, fmap, deriving ( Functor )
  • Leis de Functor
• Abuso de List α para assumir papel de Maybe α
• Duas interpretações computacionais dos habitantes de List α
• Functorialidade do Either ε
• Composição de funções: (∘)
• programação tácita: point-free, point-less, …
• Como implementar os Ints usando Nats: igualdade
• Teaser sobre arvores

hw

1. Demonstre a associatividade da (∘)
2. Defina tipos para cada um estilo de árvore que tu já viu ou imaginou
3. Formulize os correspondentes princípios/regras de indução para cada um deles
4. Mostre como cada um deles pode virar um Functors
5. 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]
   

6. Demonstre:

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

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

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

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

10. Demonstre:

    sum (xs ++ ys) = sum xs + sum ys
    product (xs ++ ys) = product xs * product ys
    concat (xss ++ yss) = concat xss ++ concat yss
    

11. Podemos definir uma generalização da pw : (α → β → γ) → (F α → F β → F γ) sabendo apenas que o F possui um fmap com qual ele se torna um Functor?
12. Implemente os racionais!

mais hw

1. Na última aula percebemos que Either não tinha sequer chances de se candidatar para virar um Functor, pois Either não é um Type → Type (mas sim um Type → Type → Type. Mesmo assim, conseguimos verificar que aplicando parcialmente o Either num tipo ε só, chegamos mesmo no Either ε que é mesmo um Type → Type, e logo tem chances de ser um Functor, e descubrimos qual seria a fmap certa pra isso (demonstre se não demonstrou—o que é pra demonstrar mesmo??). Aqui mais duas coisinhas que estão também Type → Type → Type: o próprio (→) e o (×). Investigue para cada um deles, e para cada aplicação parcial dele, se pode ser munida com um fmap para conseguir ser um Functor:
   1. (δ →) : Type → Type
   2. (→ γ) : Type → Type
   3. (α ×) : Type → Type
   4. (× β) : Type → Type

IRI (14) [video]

• corretude: estipular e demonstrar propriedades dos nossos programas
• e sobre igualdade intensional entre funções
• uns tipos de arvores
• a map das listas e outras fmaps e as leis de Functor
• maneiras de escrever uso de indução é os detalhes possivelmente enganadores e implícitos
• a List com o map é um Functor: demonstração da 2a lei
• demonstração: a segunda lei de Functor para a map de List α
• Composição de Functors
• a propaganda mentirosa de «tipos dinâmicos» e a verdade decepcionante
• como funcionam linguagens de “tipos dinâmicos” e runtime errors

hw

1. Prática para indução nos naturais: resolva o [Problem Set 2 de 2021.2][ps2-2021.2].
2. Na aula de IDMb definimos uma (·) : Real × Seq(Real) → Seq(Real) em duas formas: implemente ambas em Haskell e demonstre a sua equivalência.

IRI (15,16) [video]

• Eficiência “por algebra”
• Eficiência “por indução”
  • eliminando o (⧺) da reverse “por indução”
• Arvores
  • típos de árvores e umas funções relevantes
  • size, nodes, depth, flatten, mapTree, foldTree, …
• Sintaxe vs semântica
• Numerais binários
• Um toque de expressões e ASTs
  • BNF
  • ArEx, ArExV
  • semântica operacional
  • semântica denotacional
  • eval, step, bigstep
• funções fold: fold

hw

• Ordenação (sorting)
  1. Defina sozinhos os: merge sort; quick sort ;insertion sort
• ASTs
  1. Defina tipos para representar:
     1. expressões de aritmética sem variáveis:
     2. expressões de aritmética com variáveis;
     3. expressões de lógica proposicional
  2. Defina funções de eval e step apropriadamente para cad um dos teus tipos
• Arvores
  1. Defina as:
     • nodesize  : BinTree α → Nat
     • size      : BinTree α → Nat
     • depth     : BinTree α → Nat
     • leaves    : BinTree α → List α
     • mapTree   : ?
     • mirror    : BinTree α → BinTree α 
     • flatten   : BinTree α → List α
     • findTree  : α → GenTree α → List (List Nat)
     • sumTree   : BinTree Nat → Nat
  2. Adivinhe uma conexão entre o número size t e o número nodes t: enuncie e demonstre!
  3. Θ. size t ≤ 2 ^ depth t
  4. Θ. depth t ≤ length (flatten t)
  5. Verifique que tu passou EM & ME mesmo, reescrevendo o que demonstrou acima utilizando log₂
  6. Defina o resto dos tipos de arvores discutidos nas aulas (peça detalhes no Zulip!)
     1. BinSearchTree α
     2. BinLabTree α β
     3. RoseTree α
  7. Demonstre como todos teus típos de árvores viram Functors
  8. Demonstre:
     1. length ∘ flatten = ??
     2. flatten ∘ mirror = ??
     3. mirror ∘ mirror = ??
     4. depth ∘ mirror = ??
     5. depth ∘ fmap f = ??
     6. fmap f ∘ mirror = ??
• 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
• Folds & lists
  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
     

Prova 2.3

Em um universo paralelo

• Expressões e ASTs
  • Fórmulas de Lógica Proposicional
  • Funções em fórmulas
• Recursão aninhada
  • Ackermann
• Recursão para contagem