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.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Rozvrh

Po 10:00–12:50 B411

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)
• Bezpečnost informačních technologií (program FI, N-IN)
• Bioinformatika (program FI, N-AP)
• Informační systémy (program FI, N-IN)
• Paralelní a distribuované systémy (program FI, N-IN)
• Počítačová grafika (program FI, N-IN)
• Počítačové sítě a komunikace (program FI, N-IN)
• Počítačové systémy (program FI, N-IN)
• Programovatelné technické struktury (angl.) (program FI, N-IN)
• Programovatelné technické struktury (program FI, N-IN)
• Služby - výzkum, řízení a inovace (angl.) (program FI, N-AP)
• Služby - výzkum, řízení a inovace (program FI, N-AP)
• Sociální informatika (program FI, B-AP)
• Teoretická informatika (program FI, N-IN)
• Učitelství výpočetní techniky pro střední školy (program FI, N-SS) (2)
• Umělá inteligence a zpracování přirozeného jazyka (program FI, N-IN)
• Zpracování obrazu (program FI, N-AP)

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

Studijní materiály

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