A1: Wstęp

• Cel
• Wybór
• Programowanie i dowodzenie
  • Alan Turing i jego maszyna
  • Alonzo Church i rachunek λ
  • Martin-Löf, Coquand, CoC, CIC i Coq
• Filozofia i matematyka
  • Konstruktywizm
  • Praktyka
  • Homofobia... ekhm, homotopia, czyli quo vadimus?
• Literatura
  • Książki
  • Blogi
  • Inne
• Sprawy techniczne
• Plan niniejszego podręcznika (TODO)

A2: Demo [TODO]

• Kilka prostych funkcji na listach
• Sortowanie przez wstawianie (TODO)
• Mapowanie funkcji monotonicznej zachowuje porządek

BC1a: Konstruktywny rachunek zdań [TODO]

• Stary wstęp
  • Logika klasyczna i konstruktywna
  • Dedukcja naturalna i taktyki
• Wstęp (TODO)
  • Zdania logiczne
  • Rozumowanie i dowodzenie
  • Reguły i taktyki
  • Przydatne komendy
    • Komendy Check i Locate
• Zdania i spójniki logiczne (TODO)
  • Implikacja (TODO)
  • Dysjunkcja (TODO)
  • Koniunkcja (TODO)
  • Prawda i fałsz (TODO)
    • Prawda
    • Fałsz
  • Równoważność (TODO)
  • Negacja (TODO)
• O implikacji nieco więcej (TODO)
  • Implikacja odwrotna
  • Implikacja przeciwna
  • Kontrapozycja
• Logika a język naturalny (TODO)
  • Paradoksy implikacji
  • Przemienność koniunkcji a język naturalny
  • Paradoks Curry'ego
  • Inne paradoksy autoreferencji
• Harmonia logiki konstruktywnej i "prawo zachowania informacji" (TODO)
• Logika intuicjonistyczna jako logika certyfikatów (TODO)
• Ściąga
• Kombinatory taktyk
  • ; (średnik)
  • || (alternatywa)
  • idtac, do oraz repeat
  • try i fail
• Zadania (TODO)
• Zadania po raz drugi
  • Kluczowe prawa
  • Dysjunkcja
    • Reguły
    • Właściwości działaniowe
    • Właściwości relacjowe
    • Pozostałe właściwości
  • Koniunkcja
    • Reguły
    • Właściwości działaniowe
    • Właściwości relacjowe
    • Pozostałe właściwości
  • Równoważność
    • Reguły
    • Właściwości działaniowe
    • Właściwości relacjowe
    • Pozostałe właściwości
    • Bardzo nudne właściwości
  • Implikacja
    • Reguły
    • Właściwości działaniowe
    • Właściwości relacjowe
    • Pozostałe właściwości
  • Negacja
    • Reguły
    • Negacja stałych i spójników
    • Podwójna negacja
    • Potrójna negacja
    • Pozostałe właściwości
  • Pozostałe mało istotne prawa
    • Wesołe podwójnie zanegowane prawa

BC1b: Inne spójniki? [TODO]

• Różnica między "lub" i "albo" (TODO)
• Zdecyduj się pan, czyli spójnik "i/lub" (TODO)
• Zdecyduj się pan po raz drugi, czyli spójnik "i/albo" (TODO)
• Ani w tę ani we wtę, czyli negacja dysjunkcji (TODO)
  • W nieco innej wersji (TODO)
• nand, czyli negacja koniunkcji
• Antyimplikacja, czyli negacja implikacji
• Zadania (TODO)

BC1c: Podstawy programowania funkcyjnego [TODO]

• Wstęp
  • Typy i typowanie statyczne (TODO)
    • Typy vs testy
• Typy, programy, zdania, dowody i specyfikacje (TODO)
  • Przydatne komendy
• Typy wbudowane (TODO)
• Funkcje (TODO)
• Enumeracje (TODO)
  • Ważne enumeracje
    • Typ pusty
    • Singleton
  • Reguły eliminacji dla enumeracji
• Sumy (TODO)
• Enumeracje z argumentami (TODO)
• Produkty (TODO)
• Rekordy (TODO)
• Prymitywne rekordy (TODO)
• Programowanie a dowodzenie - eliminacja zdań (TODO)
• Typy hybrydowe
• Typy pozytywne i negatywne (TODO)
• Moduły (TODO)
• Styl, czyli formatowanie, wcięcia i komentarze (TODO)
  • Formatowanie kodu i wcięcia
  • Komentarze
  • Ars nazywandi, czyli trudna sztuka wymyślania nazw

BC1d: Induktywna logika [TODO]

• Induktywne zdania
• Prawda i fałsz
• Induktywne definicje spójników logicznych

BC1e: Logika boolowska

• Definicje
• Twierdzenia
  • Właściwości negacji
  • Eliminacja
  • Elementy neutralne
  • Anihilacja
  • Łączność
  • Przemienność
  • Rozdzielność
  • Wyłączony środek i niesprzeczność
  • Prawa de Morgana
  • eqb, xorb, norb, nandb
  • Różne
• Zadania

BC2a: Konstruktywny rachunek kwantyfikatorów [TODO]

• Predykaty i relacje (TODO)
• Kwantyfikatory
  • Kwantyfikacja uniwersalna
  • Kwantyfikacja egzystencjalna
• Równość - najważniejsza relacja (TODO)
  • Równość według Arystotelesa
  • Równość według Leibniza
  • α-konwersja i inne rodzaje równości
  • Równość induktywna
• Kwantyfikator unikatowy (TODO)
• Paradoksy autoreferencji (TODO)
  • Paradoks golibrody
• Logika pierwszego rzędu a logika wyższego rzędu (TODO)
  • Logika pierwszego rzędu
  • Logika drugiego rzędu
  • Logika wyższego rzędu
• Predykatywizm i kodowania impredykatywne (TODO)
• Spójniki pozytywne i negatywne (TODO)
• Konkluzja (TODO)
  • Ściąga
• Zadania (TODO)
  • Kwantyfikator uniwersalny
    • Reguły
    • Prawa
  • Kwantyfikator egzystencjalny
    • Reguły
    • Prawa
  • Związki forall i exists
  • Zagadki

BC2b: Inne kwantyfikatory? [TODO]

• Kwantyfikator xorowy
• Kwantyfikatory liczące (TODO)
• Jakich kwantyfikatorów nie da się wyrazić w logice pierwszego rzędu? (TODO)

BC2c: Polimorfizm, funkcje wyższego rzędu i klasy typów [TODO]

• Typy polimorficzne i właściwości konstruktorów
• Parametryzowane enumeracje (TODO)
  • Reguły eliminacji (TODO)
• Parametryzowane rekordy (TODO)
• Klasy (TODO)

BC2d: Opcje [TODO]

• Typ opcji (TODO)
• Podstawowe funkcje na opcjach (TODO)

BC2e: Izomorfizmy typów [TODO]

• Definicja izomorfizmu typów (TODO)
• Podstawowe typy
  • Produkty
  • Sumy
  • Funkcje
  • Rozdzielność
  • bool
  • Adiunkcje
• Zachowywanie izomorfizmów
• Izomorfizmy charakterystyczne typów induktywnych (TODO)
  • bool
  • Opcje

BC2f: Funkcje [TODO]

• Funkcje
• Aksjomat ekstensjonalności
• Odwrotności i izomorfizmy (TODO)
• Skracalność (TODO)
• Injekcje
• Surjekcje
• Bijekcje
• Inwolucje
• Uogólnione inwolucje
• Idempotencja

BC2g: Relacje [TODO]

• Relacje binarne
• Identyczność relacji
• Operacje na relacjach
• Relatory, czyli więcej operacji na relacjach (TODO)
• Relacje homogeniczne (TODO)
• Relacje równoważności (TODO)
  • Relacje zwrotne
  • Relacje symetryczne
  • Relacje przechodnie
  • Relacje równoważności
• Relacje porządku (TODO)
  • Relacje słaboantysymetryczne
  • Relacje totalne
  • Porządki
  • Relacje gęste
• Domknięcia (TODO)
  • Ogólne pojęcie domknięcia
  • Domknięcie zwrotne
  • Domknięcie symetryczne
  • Domknięcie zwrotnosymetryczne
• Redukcje (TODO)
  • Redukacja zwrotna
  • Redukcja przechodnia
  • Redukacja zwrotno-przechodnia
• Podsumowanie

BC2h: Relacje a funkcje [TODO]

• Rodzaje relacji heterogenicznych
  • Relacje lewo- i prawostronnie unikalne
  • Relacje lewo- i prawostronnie totalne
• Rodzaje relacji heterogenicznych v2
  • Relacje funkcyjne
  • Relacje injektywne
  • Relacje surjektywne
  • Relacje bijektywne
• Nieco więcej o relacjach funkcyjnych (TODO)
  • Relacje funkcyjne a aksjomat wyboru (TODO)
  • Relacje funkcyjne a funkcje (TODO)
  • Relacje wykresowe (TODO)
• Zależności między różnymi rodzajami relacji

BC2i: Mało ciekawe relacje [TODO]

• Relacje prawie równoważności (TODO)
  • Częściowe relacje równoważności
  • Relacje tolerancji
• Wariacje nt relacji zwrotnych (TODO)
  • Relacje kozwrotne
  • Relacje kwazizwrotne
    • Relacje lewostronnie kwazizwrotne
    • Relacje prawostronnie kwazizwrotne
    • Relacje kwazizwrotne
• Relacje powiązane z relacjami przechodnimi (TODO)
  • Relacje antyprzechodnie
  • Relacje kwaziprzechodnie
• Wariacje nt relacji przechodnich (TODO)
  • Relacje cyrkularne
  • Relacje euklidesowe
    • Relacje prawostronnie euklidesowe
    • Relacje lewostronnie Euklidesowe
    • Relacje euklidesowe
• Zależności między różnymi rodzajami relacji
• Związki z relacjami heterogenicznymi
• Domknięcia (TODO)
  • Domknięcie lewostronnie kwazizwrotne

BC3a: Programowanie funkcyjne z typami zależnymi [TODO]

• Typy zależne, czyli typowanie statyczne na sterydach
• Uniwersum (TODO)
• Funkcje zależne (TODO)
• Pary zależne i podtypy (TODO)
• Indeksowane enumeracje (TODO)
• Rekordy zależne
• Kwantyfikacja egzystencjalna (TODO)
• Równość (TODO)
• Równość a ścieżki

BC3b: Równość i ścieżki [TODO]

• Równość - powtórka (TODO)
• Ścieżki (TODO)
  • Równość a ścieżki
  • Ścieżki między funkcjami (TODO)
  • Ścieżki dla prostych typów (TODO)

BC4a: Logika klasyczna [TODO]

• Aksjomaty i prawa logiki klasycznej (TODO)
• Logika klasyczna jako logika diabła (TODO)
  • Logika zdań stabilnych
• Logika klasyczna jako logika Boga (TODO)
  • Zdania określone
  • Metoda zerojedynkowa (TODO)
• Logika klasyczna jako logika kontrapozycji
  • Zdania kontrapozowalne dziedzinowo (TODO)
  • Zdania kontrapozowalne przeciwdziedzinowo
• Logika klasyczna jako logika cudownych konsekwencji (TODO)
  • Logika cudownych konsekwencji
    • Zdania cudowne
  • Logika Peirce'a
    • Logika zdań penetrowalnych
• Aksjomaty i pojęcie "tabu" (TODO)
• Pułapki negacji. O negowaniu słabym i mocnym (TODO)
• Stary podrozdział, do naprawy
• Klasyczna logika pierwszego rzędu (TODO)
  • Paradoks pijoka
  • Double negation shift
• Klasyczna logika wyższego rzędu (TODO)
  • Aksjomat wyboru (TODO)
• Interpretacja obliczeniowa logiki klasycznej, a raczej jej brak (TODO)
• Porównanie logiki konstruktywnej i klasycznej (TODO)
• Uniwersum SProp (TODO)
• Konkluzja (TODO)
  • Ściąga
• Zadania (TODO)

BC4b: Logika klasyczna jako logika silnych i słabych spójników [TODO]

• Silna implikacja
• Słaba implikacja
• Słaba dysjunkcja
• Słaba dysjunkcja przemienna
• Słaba koniunkcja
• Silna równoważność
• Silna antyimplikacja
• Klasyczna dysjunkcja (TODO)
• Bonus: klasyczna koń-junkcja (TODO)
• Bonus 2: klasyczny kwantyfikator egzystencjalny (TODO)
• Słaby kwantyfikator egzystencjalny
• Słaby kwantyfikator uniwersalny
• Wymyśl to sam...

BC4c: Rozstrzygalność i reflekcja [TODO]

• Różnice między bool, Prop i SProp
• Rozstrzygalność
  • Techniczne apekty rozstrzygalności
  • Kiedy nie warto rozstrzygać? (TODO)
  • Rozstrzygalność jako pułapka na negacjonistów (TODO)
  • Techniczne aspekty rozstrzygalności 2 (TODO)
• Ślepota boolowska (TODO)
• Reflekcja w małej skali (TODO)
  • Poradnik hodowcy, czyli jak nie rozmnażać definicji (TODO)

BC4d: Nierówność i różność [TODO]

• Nierówność (TODO)
• Różność
  • (Słaba) różność funkcji
  • Silna różność funkcji (TODO)
  • Różność funkcji zależnych (TODO)

BC4e: Relacje różności i ostre porządki [TODO]

• Relacje różności (TODO)
  • Relacje koprzechodnie
  • Relacje apartheidu
• Relacje trychotomiczne
• Słabe wersje relacji trychotomicznych i totalnych (TODO)
  • Relacje spójne
  • Relacje słabo totalne
  • Relacje słabo trychotomiczne
• Ostre porządki (TODO)

BC5a: Logika modalna

• Modalność neutralna: nasza ulubiona
• Modalność trywialna: meh...
• Modalność wymówkowa: pies zjadł mi dowód... :(
• Modalność klasyczna: logika klasyczna jako logika modalna
• Modalność aksjomatyczna
• Modalność niezaprzeczalna
• Modalność pośrednia
• Modalność wszechpośrednia
  • Strukturalizm matematyczny
• Dodatkowe prawa modalności
• Związki między modalnościami
• Składanie modalności
• Podsumowanie

BC5b: Monady i efekty obliczeniowe [TODO]

BC6: Inne logiki [TODO]

• Inne aksjomaty? (TODO)
• Inne systemy dowodzenia? (TODO)
  • Systemy w stylu Hilberta
  • Rachunek sekwentów
• Inne logiki?
  • Logiki (sub- i super-)intuicjonistyczne oraz logiki pośrednie
  • Logiki modalne
  • Paradoks pieniądza i kebaba (TODO)
  • Logiki substrukturalne - kwantowa teoria relewantnego hajsu
  • Logiki wielowartościowe
  • Logika szalonego Gruzina
• Pluralizm logiczny
  • Pluralizm w praktyce: płytkie zanurzenie
  • Pluralizm w praktyce: uniwersum SProp i logika klasyczno-konstruktywna (TODO)
• Zadania: logiki pośrednie (TODO)
  • Logika słabego wyłączonego środka
    • Logika zdań słabo określonych
  • Silna negacja koniunkcji i logika de Morgana
  • Inne mało ważne logiki pośrednie
    • IOR
    • Logika zdań IORowych
    • Gödel-Dummet
• Jakieś podsumowanie (TODO)

BC7: Teoretyczne podstawy teorii typów [TODO]

• Typy i termy
• Typy i termy, kanoniczność i uzasadnienie reguł eliminacji
• Typy a zbiory
• Uniwersa
• Pięć rodzajów reguł
  • Reguły formowania
  • Reguły wprowadzania
  • Reguły eliminacji
  • Reguły obliczania
  • Reguły unikalności
• Metateoria
  • Preliminaria
  • Niesprzeczność
  • Niedowodliwość prawa wyłączonego środka
  • Konkluzja
• Parametryczność

D1a: Indukcja

• Konstruktory rekurencyjne
  • Reguły indukcji
• Listy, czyli parametry + rekursja
• Kiedy typ induktywny jest pusty?
• "Paradoksy" indukcji (TODO)
  • Paradoks sterty (TODO)
  • Wszystkie konie sa tego samego koloru (TODO)
  • Paradoks najmniejszej interesującej liczby naturalnej (TODO)
• Indukcja matematyczna a indukcja w nauce (TODO)

D1b: Arytmetyka Peano

• Podstawy
  • Definicja i notacje
  • 0 i S
  • Poprzednik
• Proste działania
  • Dodawanie
  • Alternatywne definicje dodawania
  • Odejmowanie
  • Alternatywna definicja odejmowania
  • Mnożenie
  • Alternatywna definicja mnożenia
  • Potęgowanie
• Minimum i maksimum
• Współczynnik dwumianowy (TODO)
• Wzory rekurencyjne (TODO)
• Sumy szeregów (TODO)

D1d: Rekursja prymitywna i reguły indukcji [TODO]

• Jaka piękna katastrofa
• Fantastyczny termination checker i jak go wyłączyć (TODO)
• Rodzaje rekursji
• Rekursja prymitywna (TODO)
• Myślenie rekurencyjne - bottom-up vs top-down (TODO)
• Jak działa taktyka induction? Standardowe reguły indukcji (TODO)
• Dekompozycja reguły indukcji na regułę rekursji i regułę unikalności (TODO)
• Rekursja jako najlepszość

D1e: Podstawowe funkcje na listach [TODO]

• Podstawowe funkcje na listach (TODO)
• foldr, czyli standardowa reguła rekursji dla list (TODO)
  • Lematy o foldach (TODO)

D1f: Rekursja monotoniczna [TODO]

• Rekursja monotoniczna
• Funkcja Ackermanna
• Scalanie posortowanych list

D1g: Rekursja strukturalna i customowe reguły indukcji [TODO]

• Rekursja strukturalna (TODO)
• Customowe reguły indukcji dla liczb naturalnych (TODO)
• Dzielenie przez 2
• Szybkie potęgowanie (TODO)
• Customowe reguły indukcji na listach (TODO)
  • Funkcja rot2
• foldl, czyli rekursja dla list... od tyłu (TODO)
• Sumy kroczące (TODO)

D1h: Rekursja ogonowa [TODO]

• Rekursja ogonowa (TODO)
• Liczby Fibonacciego (TODO)
• Sklejanie list (TODO)

D1i: Induktywne predykaty i relacje [TODO]

• Induktywne predykaty i relacje
  • Indukcja po dowodzie
  • Taktyki replace i assert

D1j: Domknięcie przechodnie i systemy przepisywania [TODO]

• Domknięcia (TODO)
  • Domknięcie przechodnie
  • Domknięcie zwrotnoprzechodnie
  • Domknięcie równoważnościowe
  • Domknięcie cyrkularne
• Cosik o systemach przepisywania (TODO)
  • Właściwość diamentu
  • Relacje lokalnie konfluentne
  • Relacje konfluentne

D1k: Arytmetyka Peano, część 2

• Porządek
  • Porządek <=
  • Porządek <
• Nieinduktywne predykaty i relacje (TODO)
  • Podzielność
  • Liczby pierwsze (TODO)
• Definicje induktywne vs definicje nieinduktywne (TODO)
• Rozstrzygalność
  • Rozstrzygalność porządku
  • Rozstrzygalność równości
• Silnia
• Dyskretny pierwiastek kwadratowy (TODO)
• Zadania

D1l: Predykaty na listach [TODO]

• Predykaty na listach (TODO)

D1m: Relacje na listach [TODO]

• Relacje na listach (TODO)

D1n: Indukcja wykresowa [TODO]

• Indukcja wykresowa
• Podsumowanie (TODO)

D1o: Zaawansowane funkcje na listach [TODO]

• Zaawansowane funkcje na listach (TODO)

D2d: Rekursja po paliwie [TODO]

• Mafia paliwowa, czyli jak oszukiwać na paliwie

D2g: Rekursja dobrze ufundowana [TODO]

• Rekursja dobrze ufundowana

D2h: Metoda induktywnej dziedziny

• Metoda induktywnej dziedziny
• Porządny predykat dziedziny
  • Eliminacja zdań i irrelewancja dowodów
  • Inwersja na predykacie dziedziny
  • Ekstrakcja
• Komenda Function
• Plugin Equations
• Podsumowanie (TODO)

D2i: Rekursja zagnieżdżona [TODO]

• Rekursja zagnieżdżona

D2z: Dobre, złe i podejrzane typy induktywne

• Nieterminacja jako źródło zła na świecie
• Twierdzenie Cantora
• Twierdzenie Cantora jako młot na negatywność
• Poradnik rozpoznawania negatywnych typów induktywnych
• Kilka bonusowych pułapek
  • Zabawy z parametrami
  • Pułapki dla indukcji wzajemnej
• Jeszcze więcej pułapek
  • Większa niedobrość
  • Upierdliwe kodziedziny
• Pozytywne typy induktywne
• Podsumowanie (TODO)

D5a: Proste funkcje na listach

• Bardzo proste funkcje
  • isEmpty
  • head
  • tail
  • uncons
• Proste funkcje
  • length
  • snoc
  • app
  • rev
  • map
  • join
  • bind
  • replicate
  • iterate i iter
  • last, init i unsnoc
    • last
    • init
    • unsnoc
    • Dualności head i last, tail i init oraz ciekawostki
  • nth
  • take
  • drop
    • Dualność take i drop
  • cycle
  • splitAt
  • insert
  • replace
  • remove
  • zip
  • unzip
  • zipWith
  • unzipWith
• Funkcje z predykatem boolowskim
  • any
  • all
  • find i findLast
  • removeFirst i removeLast
  • findIndex
  • count
  • filter
  • partition
  • findIndices
  • takeWhile i dropWhile
  • span
    • Związki span i rev
• Rozstrzyganie równości list (TODO)

D5b: Bardziej skomplikowane funkcje na listach [TODO]

• Sekcja mocno ad hoc
  • pmap
  • mask
  • Też mask, ale inaczej
  • imap, czyli mapowanie z indeksem
• Bardziej skomplikowane funkcje
  • intersperse
  • interleave (TODO)
  • groupBy
  • insertBefore

D5c: Predykaty na listach

• Proste predykaty
  • elem
  • In
  • NoDup
  • Dup
  • Rep
  • Exists
  • Forall
  • AtLeast
  • Exactly
  • AtMost
• Palindromy
• Rozstrzyganie predykatów na listach (TODO)
• Predykaty na listach - rekurencyjnie (TODO)
  • exists

D5d: Relacje między listami

• Relacje między listami
  • Sublist: listy jako termy
  • Prefiksy
  • Sufiksy
  • Subseq: listy jako ciągi
  • Zawieranie
  • Listy jako zbiory
  • Listy jako multizbiory
  • Listy jako cykle
  • Partycje list (TODO)
• Rozstrzyganie relacji na listach (TODO)
• Znajdowanie wszystkich podstruktur (TODO)
  • Podlisty/podtermy
  • Sufiksy
  • Prefiksy
  • Podciągi
  • Podzbiory
  • Cykle

D5: Więcej zabaw z listami [TODO]

• Permutacje (TODO)
  • Permutacje jako ciągi transpozycji
  • Permutacje jako ciągi transpozycji v2
  • Permutacje jako ciągi transpozycji elementów sąsiednich
  • Permutacje jako ciągi transpozycji elementów sąsiednich v2
  • Permutacje za pomocą liczenia właściwości
  • Permutacje za pomocą liczenia właściwości v2
  • Permutacje, jeszcze dziwniej
  • Permutacje za pomocą liczenia właściwości rozstrzygalnych
  • Permutacje przez wstawianie
  • Permutacje przez wstawianie v2 (TODO)
• Znajdowanie wszystkich permutacji (TODO)
  • Znajdowanie permutacji przez selekcję
  • Znajdowanie permutacji przez wstawianie
  • Znajdowanie permutacji przez cykle
• Wut da fuk? (TODO)
• Zbiory
  • Zbiory jako zdeduplikowane permutacje
  • Zbiory za pomocą Exists
  • Zbiory za pomocą transpozycji i deduplikacji
  • Zbiory za pomocą sąsiednich transpozycji i deduplikacji

D7: Listy niepuste [TODO]

• Typ list niepustych (TODO)
• Porządna reguła indukcji (TODO)
• Równość, różność i relatory (TODO)
• Podstawowe funkcje na listach niepustych
• Funkcje na listach niepustych z predykatem boolowskim
• Skomplikowańsze funkcje (TODO)
• foldr
• Predykaty na listach niepustych
• Właściwości funkcji na listach niepustych

D8: Indukcja wzajemna

• Indukcja wzajemna
• Reguły indukcji dla typów wzajemnych (TODO)

E0: Rodziny typów induktywnych

• Indeksowane rodziny typów (TODO)
  • Indukcja wzajemna a indeksowane rodziny typów
• Podsumowanie (TODO)

E1: Wektory, czyli listy indeksowane długością [TODO]

• Podstawowe funkcje
  • length
  • app
  • repeat
  • nth
  • head i last
  • tail i init
  • take i drop
• Predykaty i relacje (TODO)

E2: Wektory jako typ rekurencyjny [TODO]

• Rekurencyjna definicja typu wektorów
  • Reguła indukcji
• Podstawowe funkcje
  • len
  • app
• Predykaty i relacje (TODO)

F0: Równość, nierówność, różność i ścieżki [TODO]

• Ścieżki w typach induktywnych (TODO)
  • Ścieżki między liczbami naturalnymi - rekurencyjnie
  • Ścieżki między liczbami naturalnymi - induktywnie
  • Porządek <= na liczbach naturalnych
  • Jeszcze raz <=, lecz tym razem używając SProp
  • Ścieżki między listami
  • Ścieżki w uniwersum (TODO)
• Nierówność i różność
  • Liczby naturalne (TODO)
    • Nierówność liczb naturalnych - rekurencyjnie
    • Nierówność liczb naturalnych - induktywnie
    • Tadam
  • Listy
    • Różność list - induktywnie
    • Różność list a Exists2
    • Różność list - rekurencyjnie
  • Różność strumieni (TODO)
  • Nierówność liczb konaturalnych
  • Różność kolist

F1: Koindukcja i korekursja [TODO]

• Koindukcja (TODO)
  • Nanana Batman! (TODO)
  • Drzewka (TODO)
  • Rekursja ogólna (TODO)

F2: Strumienie [TODO]

• Bipodobieństwo
• sapp
• lsapp
• map
• zipWith i unzip (TODO)
• Inne funkcje (TODO)
• Predykaty i relacje na strumieniach (TODO)
• Permutacje strumieni
• Permutacje strumieni v2
• Pomysł dawno zapomniany: (ko)induktywne specyfikacje funkcji (TODO)
• Trochę losowości (TODO)

F3: Liczby konaturalne [TODO]

• Zero, następnik i nieskończoność
• Dodawanie
• Lepsze dodawanie
• Porządek
• Minimum i maksimum
• Dzielenie przez 2
• Skończoność i nieskończoność
• Parzystość i nieparzystość
• Odejmowanie (TODO)
• Mnożenie (TODO)
• Koindukcja wzajemna (TODO)
• Liczby naturalne i konaturalne
  • Losowe ćwiczenia

F4a: Kolisty [TODO]

• Kolisty nie znaczy okrągły

F4: Kolisty [TODO]

• Kolisty nie znaczy okrągły
  • Bipodobieństwo
  • Różność
  • conil i cocons
  • len
  • snoc
  • app
  • lmap
  • iterate
  • piterate
  • zipW
  • scan
  • intersperse
  • splitAt
  • Finite i Infinite
  • Exists i Forall

F5: Kodrzewa [TODO]

• Drzewa nieskończone (TODO)
  • Korekursja i koindukcja na drzewach nieskończonych (TODO)
  • Funkcje na drzewach nieskończonych

G0: Zippery, czyli łażenie po drzewach [TODO]

• Predykaty na listach i drzewach - przypomnienie (TODO)
• Indeksowanie drzew (TODO)
• Zippery dla list - chodzenie po linie (TODO)
• Szukanie dziury w typie, czyli różniczkowanie (TODO)
• Zippery dla typów induktywnych (TODO)
• Zippery dla typów koinduktywnych (TODO)

G1: Typy ilorazowe i smart konstruktory [TODO]

• Liczby całkowite (TODO)
• Liczby całkowite inaczej (TODO)
• Wolne monoidy (TODO)
  • Wolniejsze monoidy (TODO)

G1z: Wyrażenia regularne [TODO]

• Typ wrażeń regularnych (TODO)
• Dopasowanie i pochodna Brzozowskiego (TODO)
• Smart konstruktory (TODO)
• Funkcja normalizująca (TODO)
• Funkcja normalizująca jako owijka na smart konstruktory (TODO)

G2a: Typy induktywne wyższego rzędu [TODO]

• Rząd rżnie głupa, czyli o pierwszym i wyższym rzędzie (TODO)
• Przykładowy typ
• Szerokie drzewka (TODO)
• Szerokie wisienki (TODO)
• Drzewka z nieskończonym rozgałęzieniem (TODO)
• Drzewka z bardzo nieskończonym rozgałęzieniem (TODO)
• Wisienki z bardzo nieskończonym rozgałęzieniem (TODO)

G2b: Typy induktywne zagnieżdżone argumentowo [TODO]

• Rekursja wyższego rzędu (TODO)
• Reguły indukcji dla typów zagnieżdżonych
  • Podsumowanie
  • Papiery
• Metoda induktywnej dziedziny dla typów zagnieżdżonych (TODO)

G2c: Typy induktywne zagnieżdżone parametrowo [TODO]

• Parametry a indeksy (TODO)
• Rekursja polimorficzna
• Zupełne drzewa binarne (TODO)
• PTree, cokolwiek to jest (TODO)
• Zagnieżdżone listy (TODO)
• Zagnieżdżone listy niepuste (TODO)
• Swap-drzewka (TODO)

G2z: Struktury cykliczne [TODO]

• Listy cykliczne (TODO)
• Listy cykliczne bez udziwnień (TODO)
• Cykliczne drzewa binarne (TODO)

G3: Wyższe Typy Induktywne [TODO]

• Wstęp (TODO)
• Pary nieuporządkowane (TODO)
• Typy ilorazowe (TODO)
  • Domknięcie kozwrotne (TODO)

G3z: Zbiory skończone [TODO]

• Typ zbiorów skończonych
• Rekursor
• Reguła indukcji
• Zależny rekursor
• Działania na zbiorach skończonych

G4: Indukcja-indukcja

• Wstęp (TODO)
• Listy posortowane
  • Przykład był bez sensu... (TODO)
• Teoria typów w teorii typów za pomocą indukcji-indukcji
• Sterty binarne
• Drzewa wyszukiwań binarnych (TODO)

G5: Indukcja-rekursja

• Wstęp (TODO)
• Listy posortowane, znowu (TODO)
• Sterty binarne (TODO)
• Drzewa wyszukiwań binarnych (TODO)
• Uniwersa (TODO)
• Indeksowana indukcja-rekursja i metoda induktywno-rekurencyjnej dziedziny
• Indukcja-indukcja-rekursja
• Promocja 2 w 1 czyli paradoksy Russella i Girarda
  • Paradoks Russella
  • Paradoks Girarda

G6: Prawdziwie zagnieżdżone typy induktywne [TODO]

• Głęboka indukcja (TODO)
• Jerzy Krzak wrednym typem był (TODO)
  • Reguła indukcji (TODO)
  • Proste funkcje (TODO)
• Krzak przykościelny
• Twój stary to krzak (TODO)
• Funktor krzakotwórczy (TODO)
• Krzaczasty heredytarianizm (TODO)
• W baraku Obamy rosną dziwne krzaki (TODO)

G7: Mieszane typy induktywno-koinduktywne [TODO]

• Cthulhu zawsze płynie w lewo (TODO)
  • Pierwsze podejście (TODO)
  • Drugie podejście
  • Trzecie podejście (TODO)
• Wycinanki-indukcjanki, czyli jak wyciąć typ mieszany z typu koinduktywnego (TODO)
• Transformatory strumieni (TODO)
  • Pierwsze podejście
  • Drugie podejście
• Definiowanie dziwnych funkcji (TODO)
  • Podejście pierwsze
  • Podejście drugie

G8a: Programowanie generyczne [TODO]

• Spłaszczanie wielokrotnie zagnieżdżonych list
• zipWith z dowolną ilością argumentów
• Porządna negacja (albo i nie) TODO

G8b: W-typy [TODO]

• Nowy wstęp do rozdziału o W-typach (TODO)
• W-typy (TODO)
• Indeksowane W-typy (TODO)
• M-typy (TODO)
  • Ciekawostka: koindukcja i bipodobieństwo
• Indeksowane M-typy? (TODO)

G8c: Punkty stałe funktorów wielomianowych [TODO]

• Najmniejsze i największe punkty stałe funktorów
• Funktory bazowe często używanych typów
  • Zwykłe typy induktywne
  • Typy sparametryzowane
  • Typy wzajemnie induktywne
  • Rodziny indeksowane (TODO)
  • Rodziny indeksowane za pomocą typów parametryzowanych i równości (TODO)

G8d: Pierwszorzędowe kody [TODO]

• Kody dla typów induktywnych (TODO)
• Kody dla typów induktywno-rekursywnych (TODO)

G8e: Kontenery [TODO]

• Kontenery (TODO)

H2z: Izomorfizmy typów [TODO]

• Typy zależne
• Izomorfizmy charakterystyczne typów induktywnych (TODO)
  • Liczby naturalne
  • Listy
  • Strumienie
• Charakteryzacje "kontenerowe" (TODO)
  • Stream unit ~ unit
  • Stream A ~ nat -> A
• Charakteryzacje "wektorowe" (TODO)
  • list A ~ {n : nat & vec A n}
• Ciekawsze izomorfizmy
  • nat ~ nat + nat
  • nat ~ nat * nat
    • goto
    • comefrom
  • nat ~ nat * nat, alternatywnie (TODO)
  • nat ~ list nat

H4: Translacja dobrze ufundowana [TODO]

• Domknięcie przechodnie (TODO)
• Podtermy (TODO)
• Translacja dobrze ufundowana (TODO)

H5: Liczby porządkowe [TODO]

• Relacje dobrze ufundowane, ekstensjonalne i dobre porządki
  • Relacje słabo ekstensjonalne
  • Relacje dobrze ufundowane
  • Dobre porządki

I1: Spis przydatnych taktyk

• refine — matka wszystkich taktyk
• Drobne taktyki
  • clear
  • fold
  • move
  • pose i remember
  • rename
  • admit
• Średnie taktyki
  • case_eq
  • contradiction
  • constructor
  • decompose
  • intros
  • fix
  • functional induction i functional inversion
  • generalize dependent
• Taktyki dla równości i równoważności
  • reflexivity, symmetry i transitivity
  • f_equal
  • rewrite
• Taktyki dla redukcji i obliczeń (TODO)
• Procedury decyzyjne
  • btauto
  • congruence
  • decide equality
  • lia
  • Procedury decyzyjne dla logiki
• Ogólne taktyki automatyzacyjne
  • auto i trivial
  • autorewrite i autounfold
• Pierścienie, ciała i arytmetyka
• Zmienne egzystencjalne i ich taktyki (TODO)
• Taktyki do radzenia sobie z typami zależnymi (TODO)
• Dodatkowe ćwiczenia
• Inne języki taktyk
• Konkluzja

I2: Ltac — język taktyk

• Zarządzanie celami i selektory
• Podstawy języka Ltac
• Backtracking
• Dopasowanie kontekstu i celu
• Wzorce i unifikacja
• Narzędzia przydatne przy dopasowywaniu
  • Dopasowanie podtermu
  • Generowanie nieużywanych nazw
  • fail (znowu)
• Inne (mało) wesołe rzeczy
• Konkluzja

I3: Reflekcja w dużej skali, czyli jak odbijać z rozmachem [TODO]

• Ltac: manipulowanie termami (TODO)
• Taktyki dla unifikacji (TODO)
• Programowanie funkcyjne w Ltacu (TODO)
• Big scale reflection (TODO)

K1: Złożoność obliczeniowa

• Czas działania programu
• Złożoność obliczeniowa
• Złożoność asymptotyczna
• Duże O
  • Definicja i intuicja
  • Złożoność formalna i nieformalna
  • Duże Omega
• Duże Theta
• Złożoność typowych funkcji na listach
  • Analiza nieformalna
  • Formalne sprawdzenie
• Złożoność problemu
• Przyspieszanie funkcji rekurencyjnych
  • Złożoność rev
  • Pamięć
• Podsumowanie

K2: Algorytmy i struktury danych [TODO]

K3: Terminacja, nieterminacja i rekursja ogólna [TODO]

• Monada nieterminacji
• Kombinator punktu stałego
• Terminacja, nieterminacja
• Przykłady
  • Algorytm Euklidesa
  • Dzielenie
  • Głupia funkcja...
  • Funkcja Ackermanna

L2: Kontynuacje i kontrola [TODO]

• Wstęp
• Defunkcjonalizacja (TODO)
  • Defunkcjonalizacja filtrowania (TODO)
  • Defunkcjonalizacja silni (TODO)
• CPS (TODO)
• CPS i defunkcjonalizacja w służbie rekursji ogonowej (TODO)
• Kodowania Churcha (TODO)
• Kodowania Scotta (TODO)
• Listy różnicowe (TODO)

M0: Liczby [TODO]

• Liczby naturalne
  • Unarne
  • Dodatnie liczby naturalne, binarnie (TODO)
• Liczby całkowite
  • Unarne
  • Binarne
  • Klasyczne
  • Klasyczne znormalizowane
  • HITowe
  • HITowe zasymulowane
• Liczby wymierne (TODO)
  • Klasycznie
  • HITowo
  • Induktywnie
• Liczby rzeczywiste
• Liczby porządkowe
  • Jakieś takie proste
  • Skomplikowańsze
• Liczby nadrzeczywiste

M1: Typy skończone [TODO]

• Pięć dziwnych definicji skończoności
• Skończoność a rozstrzygalna równość (TODO)
• Typy skończone (TODO)

M2: Typy przeliczalne [TODO]

• Typy przeliczalnie nieskończone (TODO)
• Typy przeliczalne (TODO)

M3: Kombinatoryka [TODO]

• Klasy kombinatoryczne

M4: Teoria porządków [TODO]

• Typy porównań dla rozstrzygalnych porządków (TODO)
• Rozstrzygalne porządki, podejście pierwsze (TODO)
• Rozstrzygalne porządki, podejście drugie (TODO)

M5a: Podstawy algebry [TODO]

• Wstęp (TODO)
• Homomorfizmy (TODO)
• Relacje logiczne (TODO)
• Na listach
• Na monoidach

M5b: Pierścienie i ciała [TODO]

M5c: Algebra liniowa [TODO]

M6a: Zaawansowana logika i aksjomaty [TODO]

• Związki między aksjomatami
• Set to Type... czasem (TODO)
• SProp nie jest ścisłym zdaniem
• Ćwiczenia - trudne
• Drzewa Aczela
• Prop nie jest zdaniem - twierdzenie Coquand (TODO)
• Prawo wyłączonego środka implikuje Proof Irrelevance (TODO)
• Twierdzenie o hierarchii dla uniwersów (TODO)
• Wnioski z twierdzenia o hierarchii (TODO)
• Czy Prop to SProp? (TODO)
• Wincyj drzew Aczela (TODO)
• Ko-drzewa Aczela (TODO)
• Parametryczność, a raczej jej brak (TODO)

M6: Teoria zbiorów [TODO]

• Skala betów (TODO)

M7a: Nielegalna topologia [TODO]

M7b: Legalna topologia

• Wstęp (TODO)
• Typy przeszukiwalne (TODO)

M8: Teoria Kategorii [TODO]

M9a: Liczby rzeczywiste [TODO]

M9b: Analiza numeryczna [TODO]

• 1 Introductory material
• 2.1 The bisection method
• Pochodna
• 2.3 Newton's method
• 2.4 Rates of convergence
• 2.5 Secant method
• 2.7 Some more details on root-finding

M9c: Analiza rzeczywista [TODO]