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

[main]: /HTv-fjHGRseioBgvKYqf0w
[IDM]: /DoiTIssySf-ZBReMHKMxQw
[IRI]: /WGbnTIrRSr21PUk3wI3cYQ
[CFR1]: /tDO3s1p3QhGk_9vd989lFw
[IEA]: /JhQTQ-3UQBe2V8afrkgneQ

--------

[TOC]

--------

# CFR2: Funções e Relações (30h)

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

## Ementa detalhada

1. Funções injetivas e sobrejetivas, monos e epis. Retrações e seções. Condições de invertibilidade de uma função.
1. O teorema de Cantor sobre a cardinalidade do conjunto potência, e as cardinalidades transfinitas.
1. Breve introdução à teoria da computabilidade: funções computáveis, números computáveis, e conjuntos computáveis; semi-decidibilidade e decidibilidade.
1. Relações e a sua implementação conjuntista. Operações sobre relações, com ênfase no caso binário: inversa, composição, iterações, fechos. Descrição e propriedades do fecho transitivo: usando interseção (*top-down*) e usando união (*bottom-up*).
1. Exemplos de conjuntos estruturados.
(e.g. espaços normados, espaços métricos, espaços topológicos, espaços de medida, grafos).
1. Relações de equivalência e partições, classes de equivalência, e o conjunto quociente. Equivalências mais finas e mais grossas, e a relação de equivalência induzida pelo núcleo de uma função. Construções de classes de números usando quocientes.
1. Relações de ordem: pré-ordens, ordens parciais e ordens estritas, ordens totais, elementos minimais e elementos maximais, supremos e ínfimos. Cadeias e funções que preservam ordem. Reticulados e reticulados completos. Ordens parciais completas. A construção de uma função a partir do limite de uma cadeia de funções parciais.
https://en.wikipedia.org/wiki/Complete_lattice
https://en.wikipedia.org/wiki/Complete_partial_order
1. Relações bem-fundadas: definição usando cadeias e definição usando elementos minimais, conexão com recursão e indução. Relações bem-fundadas induzidas pela imagem inversa de uma relação bem-fundada, pelo produto lexicográfico de relações bem-fundadas, e pelo fecho transitivo de uma relação arbitrária.
1. Os Fundamentos da Matemática: uma breve introdução à Teoria Axiomática dos Conjuntos.

## Objetivos de aprendizagem

1. Prática com a escrita de especificações matemáticas e com o uso das técnicas de demonstração matemática, incluindo o método da diagonalização.
1. Familiarização com as principais classes, operações e propriedades de relações.
1. Familiarização com cardinalidades de conjuntos infinitos.
1. Apreciar a conexão entre especificação e implementação.
1. Familiarização com o raciocínio "sem pontos" (a saber, sem mencionar elementos dos conjuntos), através do composições de funções, e suas aplicações em programação.
https://en.wikipedia.org/wiki/Tacit_programming

## Bibliografia

* Avigad, Lewis & van Doorn (2017):
*[Logic and Proof][lean-lap]* (Cap. 13,14,15,16)
* Steffen, Rüthing & Huth (2018):
*Mathematical Foundations of Advanced Informatics, Vol. 1* (Cap: 3)
* Moschovakis (2006):
*Notes on Set Theory, 2nd ed.* (Cap: 1,2,4)
* Davey & Priestley (2002):
*Introduction to Lattices and Order, 2nd ed.* (Cap. 1, 2, 8)
* Fejer & Simovici (1991):
*Mathematical Foundations of Computer Science, Vol 1* (Cap. 2,3,4,5)

### Auxiliar

* Halmos (1960): *Naive Set Theory*
* Goldblatt (1979): *Topoi* (Cap: 1)
* Moschovakis (2006): *Notes on Set Theory, 2nd ed.* (Cap: 3,5,6,A)
* Spivak (2008): *Calculus, 4th ed.* (Cap: 29,30)

## Pointers

* Programação Lógica
* Abordagens para Fundamentos da Matemática
* Semântica Denotacional de Linguagens de Programação
* Teoria dos Domínios
* Teoria da Computabilidade
* Teoria dos Grafos
* Espaços Métricos e Topologia Geral

----

> [color=#8bf]
> ## Notas
>
> 1. Sobre a conexão entre **especificação e implementação** veja a nota relevante de [**CFR1**][CFR1].
> 1. Apreciar as idéias de **coerção e casting de tipos**, através das clásses números implementados como quocientes, onde fica claro que não temos (e não precisamos ter) ℕ⊆ℤ⊆ℚ; o que temos é ℕ↪ℤ↪ℚ.
> https://en.wikipedia.org/wiki/Type_conversion
>

----

[lean-lap]: https://leanprover.github.io/logic_and_proof/