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

[main]: /HTv-fjHGRseioBgvKYqf0w

--------

[TOC]

--------

# CFR1: Conjuntos e Funções (30h)

Aka **ConFun**. Corresponde ao módulo **FMC2a** da proposta *FMCnx*.
Colaboração dos: João Marcos, Thanos, Regivan, Umberto.

## Ementa detalhada

1. Especificações e implementações matemáticas de coleções (conjuntos, ênuplas, multiconjuntos, sequências), e de suas principais operações e predicados; extensão vs intensão. A notação construtor-de-conjunto (*set-builder*) e sua interpretação. Implementação da noção de cardinalidade, no caso finito.
1. Operações sobre coleções, finitas ou não, de conjuntos: união, interseção, produto e coproduto de conjuntos (produto cartesiano e união disjunta). Para o caso de coleções finitas, definições recursivas e demonstrações indutivas das suas propriedades. Complemento relativo, diferença simétrica. Conjunto potência.
1. Especificações de famílias indexadas. Operações sobre famílias indexadas de conjuntos. Coberturas e partições.
1. Especificações e implementações matemáticas de associações (funções parciais, totais, e não-determinísticas); extensão vs intensão. Funções vs procedimentos em programação; funções puras e efeitos colaterais.
https://en.wikipedia.org/wiki/Pure_function
https://en.wikipedia.org/wiki/Side_effect_(computer_science)
1. Funções anônimas (notação lambda).
https://en.wikipedia.org/wiki/Anonymous_function
1. Funções de ordem superior, e funções como cidadãos de primeira classe.
https://en.wikipedia.org/wiki/Function_space
https://en.wikipedia.org/wiki/Higher-order_function
https://en.wikipedia.org/wiki/First-class_function
https://en.wikipedia.org/wiki/Closure_(computer_programming)
1. Curryficação e aplicação parcial de funções.
https://en.wikipedia.org/wiki/Currying
https://en.wikipedia.org/wiki/Partial_application
1. Função identidade, composição de funções, iterações de uma função.
https://en.wikipedia.org/wiki/Iterated_function
1. Função inclusão, função vazia, função 0-ária, função constante.
Projeções e demais funções associadas ao produto e ao coproduto de conjuntos.
https://ncatlab.org/nlab/show/pairing
https://ncatlab.org/nlab/show/copairing
https://math.stackexchange.com/questions/697600/natural-uses-for-the-co-product-of-sets
Funções indicadoras (ou características).
https://en.wikipedia.org/wiki/Indicator_function
Restrições de funções.
https://en.wikipedia.org/wiki/Restriction_(mathematics)
1. Imagem direta e pré-imagem de conjuntos.
1. A inversão de uma função, e a função inversa.

## Objetivos de aprendizagem

1. Prática com o uso das técnicas de demonstração e refutação matemática.
1. Familiarização com a linguagem e com as principais classes, operações e propriedades de conjuntos e funções, definidas extensionalmente ou intensionalmente.
1. Familiarização com as noções do cálculo lambda usadas em programação e lógica: variáveis ligadas e livres, captura de variáveis, renomeamento de variáveis, sombreamento de variáveis, aplicações de funções aos seus argumentos.
1. Reconhecer os objetos matemáticos relevantes às linguagens de programação e suas propriedades.
1. Familiarização com a formulação de especificações, e suas implementações matemáticas.
1. Familiarização com o uso de diagramas comutativos em definições e demonstrações, e com especificações via propriedades universais.

## Bibliografia

* Avigad, Lewis & van Doorn (2017):
*[Logic and Proof][lean-lap]* (Cap. 11,12,15,16)
* Steffen, Rüthing & Huth (2018):
*Mathematical Foundations of Advanced Informatics, vol 1* (Cap: 2)
* Fejer & Simovici (1991):
*Mathematical Foundations of Computer Science, vol 1* (Cap: 2,3,4,5)

### Auxiliar

* Lawvere & Schanuel (2009): *Conceptual Mathematics, 2nd ed.*

## Pointers

* Cálculo-λ
* Teoria das Categorias
* Programação Funcional

----

> [color=#8bf]
> ## Notas
>
> 1. Sobre a conexão entre **especificação e implementação** veja o \[Wells 1993]. Veja também: item 1.2.12 de [Barr & Wells 2012]; a discussão no fim da §6 de \[Halmos 1960].
> 1. Sobre as funções associadas ao produto e ao coproduto veja também a §2.5 de \[Bird & de Moore 1997]. Um gabarito:
> **Funções associadas ao produto de conjuntos:**
> *Projeções.* Dados conjuntos $A,B$, as funções
> $$
> A
> \stackrel{outl}{\longleftarrow}
> A \times B
> \stackrel{outr}{\longrightarrow}
> B.
> $$
> *Pairing.* Dadas $A \stackrel f {\longleftarrow} C \stackrel g {\longrightarrow} B$, a função
> $$
> (f,g) : C \to A\times B.
> $$
> *Produto.* Dadas $A \stackrel f {\longrightarrow} C$ e $B \stackrel g {\longrightarrow} D$, a função
> $$
> (f \times g) : A\times B \to C\times D.
> $$
> **Funções associadas ao coproduto de conjuntos:**
> *Coprojeções.* Dados conjuntos $A,B$, as funções
> $$
> A
> \stackrel{inr}{\longrightarrow}
> A + B
> \stackrel{inl}{\longleftarrow}
> B.
> $$
> *Copairing.* Dadas $A \stackrel f {\longrightarrow} C \stackrel g {\longleftarrow} B$, a função
> $$
> [f,g] : A + B \to C.
> $$
> *Coproduto.* Dadas $A \stackrel f {\longrightarrow} C$ e $B \stackrel g {\longrightarrow} D$, a função
> $$
> (f + g) : A + B \to C + D.
> $$
>
> ### Referências
>
> Barr & Wells 1998
> : [Category Theory for Computing Science, 2nd ed., 2020 reprint][ctcs]
>
> Bird & de Moore 1997
> : *The Algebra of Programming*
>
> Halmos 1960
> : Naive Set Theory
>
> Wells 1993
> : *Communicating Mathematics: Useful ideas from computer science* (in American Mathematical Monthly, Vol 120, No. 5, pp.397--408)
>

----

[ctcs]: http://www.tac.mta.ca/tac/reprints/articles/22/tr22.pdf
[lean-lap]: https://leanprover.github.io/logic_and_proof/