FI:IA038 Typy a důkazy - Informace o předmětu

IA038 Typy a důkazy

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.

Rozvrh

Po 10:00–11:50 B411

Předpoklady

! I038 Typy a důkazy

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

• Aplikovaná informatika (program FI, N-AP)
• Informatika (program FI, D-IN)
• Informatika (program FI, M-IN)
• Informatika (program FI, N-IN)
• Učitelství výpočetní techniky pro střední školy (program FI, M-SS)
• Učitelství výpočetní techniky pro střední školy (program FI, M-TV)
• Učitelství výpočetní techniky pro střední školy (program FI, N-SS)

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

• Statistika zápisu (jaro 2006, nejnovější)
  
• Permalink: https://is.muni.cz/predmet/fi/jaro2006/IA038