Konečná teorie modelů

Garant předmětu:

Přednášející:

Cvičící:

Předmět zajišťuje:

katedra teoretické informatiky

Anotace:

Cı́lem předmětu je uvést studenty do základů konečné teorie modelů. Původnı́ motivacı́ jsou otázky vyjádřitelnosti a ověřitelnosti logických vlastnostı́ databázových systemů. Od svého počátku, v 70. letech minulého stoletı́ předmět prošel rapidnı́m vývojem a dotýká se řady dalšı́ch oborů teoretické informatiky, jako jsou napřı́klad teorie deskriptivnı́ složitosti, studie Constraint satisfaction Problem (CSP), teorie algoritmických meta-theorémů a kombinatorika.

Požadavky:

Předpokládá se, že studenti prošli základnı́mi kurzy teoretické informatiky nabı́zenými na FIT ČVUT,

jako jsou Diskrétnı́ matematika a logika (BI-DML) a Algoritmy a grafy 1 (BI-AG1).

Osnova přednášek:

1. Přehled kurzu, motivace a vztah k teorii databázových systemů [L][FE][G&al]

Zopakujeme si základy matematické logiky a jejı́ vztah k vyjadřovánı́ vlastnostı́ grafů a relačnı́ch struktur a vysvětlı́me jak databázové systémy mohou být popsány jako konečné relačnı́ struktury. Dále si vysvětlı́me omezenı́ logiky na konečných strukturách.

2. Ehrenfeucht-Fraı̈ssé hry [L, kapitola 3]

Uvedeme Ehrenfeucht-Fraı̈ssé (E-F) hry jako jeden ze základnı́ch nástrojů teorie modelů. Jako přı́klad diskutujeme také problém izomorfismu a logické ekvivalence dvou konečných struktur. Dále si ukážeme prvnı́ restrikci, na počet kol, která nám identifikuje fragment prvořádové logiky na formulı́ch omezené hloubky kvantifikátorů.

3. Věty o nevyjádřitelnosti v prvořádové logice [L, kap. 3]

Důležitou aplikacı́ E-F her je schopnost vyjádřit zda daná vlastnost grafů nebo relačnı́ch struktur je vyjádřitelná v prvořádové logice. Tuto techniku vysvětlı́me a předvedeme na přı́kladech. Jako motivujı́cı́ přı́klad vezmeme fakt, že souvislost nenı́ vyjádřitelná v logice prvnı́ho řádu.

4. Hanfova věta o lokálnosti [FE, kap. 2]

Uvedeme a dokážeme si Hanfovu větu o lokálnosti a jejı́ thresholdovou variantu, tzn. Fagin-Stockmeyer-Vardiho větu. Ukážeme, že nevyjádřitelnost souvislosti je nynı́ přı́mým důsledkem této věty a přidáme dalšı́ přı́klady nevyjádřitelnost, jako napřı́klad paritu velikosti univerza.

5. Gaifmanova věta o lokálnosti [FE, kap. 2]

Jako motivaci pro Gaifmanovu větu si ukážeme přı́klady, kde si nevystačı́me s Hanfovou větou. Zavedeme konstrukci Gaifmanova grafu k dané relačnı́ struktuře a dokážeme Gaifmanovu větu. Jako aplikaci ukážeme Ajtai–Gurevichovu větu.

6. Deskriptivnı́ složitost a druhořádová logika [L, kap. 6,9]

Základnı́m cı́lem je vysvětlit vztah logiky a výpočetnı́ složitosti. Vysvětlı́me vztah prvořádové logiky a výpočetnı́ třı́dy P. Dále uvedememe Faginovu věta, vyjadřujı́cı́, že existenčnı́ druhořádová logika odpovı́dá třidě složitosti NP. Zmı́nı́me také rozšı́řenı́ prvořádové logiky o fixpoint operátory a výpočetnı́ složitost tomu odpovı́dajı́cı́.

7. Logiky se schopnostı́ počı́tat [L, kap. 8]

Zavedeme bijektivnı́ E-F hry a rozšı́řenı́ prvořádové logiky o kvantifikátory vyjadřujı́cı́ počet splňujı́cı́ch ohodnocenı́ a dokážeme si vztah mezi vı́těznou strategiı́ v bijektivnı́ E-F hře a přı́slušnou logickou ekvivalencı́. Zanalyzujeme algoritmickou sı́lu počı́tacı́ch kvantifikátorů.

8. Turingovské stroje a konečné modely [L, kap. 9]

Dokážeme Trakhtenbrotovu větu a selhánı́ kompaktnosti na konečných modelech. Probereme i dalšı́ věty z nekonečné teorie modelů a zda existujı́ jejich restrikce na konečné struktury. Hlavnı́m pozitivnı́m přı́kladem bude Rossmanův Homomorphism Preservation Theorem.

9. Logiky s omezeným počtem proměnných [L, kap. 11]

Zavedeme pebble hry a ukážeme si jejich koresponenci s fragmenty logiky odpovı́dajı́cı́ omezenı́ počtu proměnných. Probereme souvislosti s rozšı́řenı́m o počı́tacı́ kvantifikátory. Dále ukážeme, že i přes neschopnost vyjádřit souvislost, souvislost resp. různé typy nesouvislostí jsou rozlišitelné podle informací v (logických) teoriích daných struktur.

10. Constraints satisfaction problem a logika [G&al, kap. 6]

Vysvětlı́me si vztah Constraints satisfaction problem a problém existence homomorfismu. Pomocı́ Chandra-Merlin korespondence tento problém přeložı́me do řeči existenčně pozitivnı́ logiky. Ukážeme si jak syntaktické restrikce na počet proměnných a hloubce vnořenı́ kvantifikátorů odpovı́dajı́ stromové šı́řce a hloubce.

11. Hernı́ komonády a jednosměrné hry [AS][ADW]

Zavedeme jedno-směrné hry a ukážeme jejich korespondenci s existečně-pozitivnı́mi fragmenty. Motivujeme komonády jako zakódovánı́ jednosměrných E-F a pebble her. Ukážeme, že takovéto zakódovánı́ splňuje axiomy komonád.

12. Koalgebry hernı́ch komonád [AS][ADW]

Zavedeme si pojem koalgebry a vysvětlı́me vztah koalgeber našich komonád ke kombinatorickým vlastnostem stromové šı́řky a hloubky.

13. Hernı́ komonády a logika [AS][ADW]

Uniformně popı́šeme bijektivnı́ i klasické formy E-F a pebble her v kategorii koalgeber pro naše hernı́ komonády. Jako aplikaci si dokážeme některé základnı́ věty z logiky pomocı́ komonád, tzn. bez nutnosti pracovat se syntaktickým popisem logiky.

Osnova cvičení:

1. Cvičnı́ z Ehrenfeucht-Fraı̈ssé her pro rozhodnutı́ nebo vyvrácenı́ logické ekvivalence.

2. Konzultace k semestrálnı́ práci, ustanovenı́ tématu práce.

3. Cvičenı́ z vět o lokálnosti logik jakožto nástroje pro dokazovánı́ vyhrávacı́ch strategiı́ Duplikátora v E–F hrách.

4. Konzultace k semestrálnı́ práci, se zaměřenı́m na diskuzi o zadané literatuře.

5. Cvičenı́ na varianty E–F her a předevšı́m jejich vstah k různým fragmentům prvořádové logiky.

6. Konzultace k semestrálnı́ práci, diskuze nad obsahem textu.

7. Cvičenı́ z herních komonád + zápočtový test

Cíle studia:

Studijní materiály:

[L] Leonid Libkin. Elements of Finite Model Theory. Springer-Verlag 2004.

[FE] Heinz-Dieter Ebbinghaus, Jörg Flum. Finite Model Theory: Second Edition. Springer-Verlag 1995.

[T] Szymon Toruńczyk. Lectures on Finite Model Theory, University of Warsaw, 2022.

https://duch.mimuw.edu.pl/~szymtor/fmt.pdf

[G&al] Erich Gradel, Phokion Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y Vardi,

Yde Venema, Scott Weinstein. Finite Model Theory and Its Applications. Springer-Verlag 2007.

[AS] Samson Abramsky, Nihil Shah. Relating Structure and Power, Comonadic Semantics for

Computational Resources. Journal of Logic and Computation, 2021.

[ADW] Samson Abramsky, Anuj Dawar, Pengming Wang. The pebbling comonad in Finite Model

Theory. 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2017.

Poznámka:

Informace o předmětu a výukové materiály naleznete na stránce:https://courses.fit.cvut.cz/NI-FMT

Další informace:

https://courses.fit.cvut.cz/NI-FMT

Pro tento předmět se rozvrh nepřipravuje

Předmět je součástí následujících studijních plánů:

• Mgr. specializace Teoretická informatika, 2018-2019 (volitelný předmět)
• Mgr. specializace Počítačová bezpečnost, 2020 (volitelný předmět)
• Mgr. specializace Návrh a programování vestavných systémů, 2020 (volitelný předmět)
• Mgr. specializace Počítačové systémy a sítě, 2020 (volitelný předmět)
• Mgr. specializace Manažerská informatika, 2020 (volitelný předmět)
• Mgr. specializace Softwarové inženýrství, 2020 (volitelný předmět)
• Mgr. specializace Systémové programování, verze od 2020 (volitelný předmět)
• Mgr. specializace Webové inženýrství, 2020 (volitelný předmět)
• Mgr. specializace Znalostní inženýrství, 2020 (volitelný předmět)
• Mgr. specializace Teoretická informatika, 2020 (volitelný předmět)
• Mgr. program, pro fázi studia bez specializace, ver. pro roky 2020 a vyšší (volitelný předmět)
• Study plan for Ukrainian refugees (volitelný předmět)
• Mgr. specializace Systémové programování, verze od 2023 (volitelný předmět)
• Mgr. specializace Teoretická informatika, 2023 (volitelný předmět)