Este documento faz parte da [Proposta 2022 de Thanos][main].

[main]: /HTv-fjHGRseioBgvKYqf0w
[CFR1]: /tDO3s1p3QhGk_9vd989lFw
[CFR2]: /EqTS3N2dRaiPFBcysOusCg
[FUN]: /n1cLwFbiQ5KmDeTlhJX6pw

--------

[TOC]

--------

# IRI: Introdução à Recursão e Indução (30h)

## Resumo

Nesta disciplina estudamos como definir tipos de dados, funções, e relações recursivamente, e como demonstrar propriedades sobre tais coleções de dados por indução.

**Recomendações:** a disciplina pode ser auxiliada usando uma linguagem de programação funcional e/ou um proof assistant (e.g. Haskell; Agda, Lean, Coq, ...). Usando uma linguagem de programação funcional é imediato implementar todas as suas definições para rodá-las no computador. Usando um proof assistant, formalizamos tanto as definições recursivas, quanto as demonstrações indutivas *usando a mesma linguagem*. (Mas o foco continua sendo o papel; não o computador.)

> [color=red] **Obs.:** proponho adicionar na grade do BTI *como disciplina obrigatória* a [**FUN**: Programação Funcional][FUN]---algo já de acordo com os as grades das universidades freqüentemente citadas em reuniões---para ser lecionada em paralelo com esta disciplina aqui. Mais sobre isso, na [página principal da proposta][main].

## Ementa detalhada

1. Os naturais e o tipo `Nat`; seus construtores (zero, sucessor) e sua teoria: implementação recursiva das suas principais operações, e verificação indutiva das suas principais propriedades.
* definição de adição, multiplicação, exponenciação
* precedência e associatividade sintática vs associatividade
* como calcular usando definições recursivas
* demonstração por casos (zero ou sucessor) vs por indução
* demonstração de propriedades das operações
* associatividade da (+)
* comutatividade da (+)
* `0` é a (+)-identidade
* relação entre aplicar o sucessor e adicionar `1`
* `1` é a (·)-identidade
* associatividade da (·)
* distributividade da (+) sobre a (·)
* comutatividade da (·)
* aⁿ⁺ᵐ = aⁿaᵐ
* aⁿᵐ = (aⁿ)ᵐ
* (ab)ⁿ = aⁿbⁿ
* leis de cancelamento para a (+)
* leis de cancelamento para a (·)
* demonstração do lema da divisão de Euclides para os naturais
1. O tipo dos booleanos, `Bool`.
* operações e suas propriedades
* predicados como funções com codomínio Bool
* recursão mutual e as funções de paridade `even` e `odd` nos naturais
* `if_then_else_`
1. Ordens sobre os naturais: especificação e verificação de suas propriedades.
* definição da ordem `≤` recursiva e usando existencial; equivalência
* definição da ordem `<` recursiva e usando `≤`; equivalência
* demonstrar que `≤` é uma ordem total e `<` é tricotômica
* demonstrar que a ordem nos naturais é uma boa ordem
1. Outras funções e relações, e suas propriedades.
* `quot`, `rem`, `log`
* fibonacci
* ackermann e suas seções
1. Indução como princípio e técnica de demonstração em matemática.
* indução finita e indução forte para demonstrar propriedades de números
* indução no tamanho de…, na soma de…, no max/min de…
* indução a partir da relação $|$ de divide
1. A unicidade dos naturais (a menos de isomorfismo).
1. `List Nat` e `List α`: tipos de dados de listas: implementação recursiva e verificação indutiva de suas principais propriedades (veja cap. 5 de \[Bird&Wadler]).
* funções: `head` ; `tail` ; `length` ; `append` ; `concatenation` ; `reverse` ; `take` ; `drop` ; `sum` ; `product`
* exemplos de propriedades para demonstrar:
`reverse ∘ reverse = id`
`length ∘ reverse = length`
`length (xs ++ ys) = length xs + length ys`
`reverse (xs ++ ys) = reverse ys ++ reverse xs`
* somatório e produtório definidos recursivamente na estrutura da lista; demonstração das suas propriedades por indução estrutural
1. Outros tipos de dados recursivos.
* tipos de árvores; tipos de expressões aritméticas; tipos de fórmulas; termos de cálculo-λ.
* Notação BNF; arvore sintática.
1. Numerais binários, definição de semântica e seu uso para verificação de corretude.

## Objetivos de aprendizagem

1. Prática com o uso da linguagem matemática e das principais técnicas de demonstração e refutação.
1. Prática com a escrita de definições por recursão e demonstrações por indução.
1. Recursão e indução estrutural sobre tipos de dados recursivos.
https://en.wikipedia.org/wiki/Structural_induction
1. Apreciação de coleções potencialmente infinitas do ponto de vista implementacional, recursivo, e verificação matemática de suas propriedades de interesse.
1. Casamento de padrões e seu uso em definições, demonstrações, e cálculos.
https://en.wikipedia.org/wiki/Pattern_matching
1. Recursão mútua, indução aninhada.
1. Ganhar familiaridade com inferência de tipos e evitar erros de tipagem.
1. Notação e nomenclatura matemática e computacional.
1. Apreciar a diferença e a conexão entre sintaxe e semântica.

## Pointers

* Programação Funcional
* Verificação de Software
* Semântica Denotacional de Linguagens de Programação
* Formalização de Matemática

## Bibliografia

* Mendelson (1973):
*Number Systems and the Foundations of Analysis* (Cap. 2)
* Avigad, Lewis, van Doorn (2017):
*[Logic and Proof][lean-lap]* (Cap. 17)
* Avigad, Leonardo de Moura, and Soonho Kong (2017):
*[Theorem proving in Lean][lean-tpil]* (Cap: 7,8)
* Steffen, Rüthing, Huth (2018):
*Mathematical Foundations of Advanced Informatics, vol 1* (Cap: 4, 5)
* Bird & Wadler (1986):
*Introduction to Functional Programming* (Cap. 5)
* Hutton (2016):
*Programming in Haskell, 2nd ed.*
* Pierce et al.:
*[Software Foundations, Vol 1][sf1]* (Cap: [Basics][sf1-b], [Induction][sf1-i], [Lists][sf1-l])
* Wadler et al:
*[Programming Languages Foundations in Agda][plfa]*
* Fejer, Simovici (1991):
*Mathematical Foundations of Computer Science, Vol 1* (Cap. 4)

## Referências

* Haskell: https://www.haskell.org/
* NNG: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
* Lean: https://leanprover-community.github.io/
* Agda: https://agda.readthedocs.io/
* Coq: https://coq.inria.fr/

----

[lean-lap]: https://leanprover.github.io/logic_and_proof/
[lean-tpil]: https://leanprover.github.io/theorem_proving_in_lean/
[sf1]: https://softwarefoundations.cis.upenn.edu/lf-current/
[sf1-b]: https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html
[sf1-i]: https://softwarefoundations.cis.upenn.edu/lf-current/Induction.html
[sf1-l]: https://softwarefoundations.cis.upenn.edu/lf-current/Lists.html
[plfa]: http://plfa.inf.ed.ac.uk/