IA038 Typy a důkazy

Fakulta informatiky
jaro 2009

Předmět se v období jaro 2009 nevypisuje.

Rozsah
2/0. 3 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k, z.
Vyučující
prof. RNDr. Jiří Zlatuška, CSc. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Jiří Zlatuška, CSc.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
Přednáška pojednává seznamuje s vazbou teorie důkazů na typovaný lambda-kalkul resp. obecně se souvislostí teorie důkazů a mechanismů popisujících kroky výpočetních procesů jako zjednodušování důkazů v různých formalismech. Seznamuje s aparátem, který je podstatný pro práci v řadě oblastí teoretické informatiky.
Osnova
  • Význam a denotace v logice, Tarski a Heyting.
  • Přirozená dedukce: kalkul, pravidla, výpočetní interpretace.
  • Curryho-Howardův izomorfismus: lambda-kalkul, operační a denotační interpretace, konverze, izomorfismus.
  • Věta o normalizaci: Churchova-Rosserova vlastnost, věta o slabé normalizaci, věta o silné normalizaci.
  • Kalkul sekventů: strukturální pravidla, intuicionistická varianta, identity, logická pravidla, vlastnosti systému bez řezu, překlad mezi kalkulem sekventů a přirozenou dedukcí.
  • Věta o silné normalizaci: reducibilita a její vlastnosti.
  • Gödelův systém T, kalkul, normalizace, výrazové schopnosti.
  • Koherentní prostory, stabilní funkce, paralelní disjunkce, součinové a funkční prostory, denotační sémantika systému T.
  • Součty v přirozené dedukci: problémy, standardní konverze, komutující konverze, funkční kalkul.
  • Systém F: kalkul, jednoduché typy, volné struktury, induktivní typy, Curryho-Howardův izomorfismus, silná normalizace.
  • Koherentní sémantika součtů; věta o odstranění řezu; reprezentace.
Literatura
  • ZLATUŠKA, Jiří. Lambda-kalkul. 1. vyd. Brno: Masarykova univerzita, 1993, 264 s. ISBN 8021008261. info
  • GIRARD, Jean-Yves, Paul TAYLOR a Yves LAFONT. Proofs and types. Cambridge: Cambridge University Press, 1990, xi, 176. ISBN 0521371813. info
Další komentáře
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích jaro 2003, jaro 2006, jaro 2011, jaro 2013, jaro 2016, jaro 2018, jaro 2021, jaro 2023, podzim 2024.