☞ SEDM! ☞

Pro vás, mí oddaní stalkeři.

Ladíte téměř pravidelný semestrální shrnovač, tentokrát prvního půlroku mého magisterského studia. Protože chci svým tisícerým čtenářům přinášet jim relevantní informace (jak je ostatně patrné ze zbytku příspěvků), rozhodl jsem se studovat obor program, jenž ještě ani pořádně neexistuje a jeho podoba byla veřejně přístupná v temném sklepě bez schodů na dně kartotéky za dveřmi s nápisem „pozor, leopard“. Tímto oborem programem je Teoretická informatika v příchuti Principy programovacích jazyků. Ne že bych snad věděl, k čemu mne to bude kvalifikovat, ale po prozkoumání starého i nového studijního katalogu jsem usoudil, že má toto zaměření nejlepší poměr hezkých a přijatelných povinných předmětů vůči těm nepříjemným.

Chtěl jsem napsat i něco o tom, jak se mi podruhé učilo funkcko a opravovalo C++, ale narazil jsem na to, že nemám moc co. Měl bych se naučit nějaké zajímavé poznatky psát už během semestru.

Neprodlévejmež tedy více a bez okolků se vrhněmež na tradiční cupování jednotlivých předmětů.

DUCIT Praktikum vedení cvičení [3 kr, Z]

Z nějakého důvodu jsem si podruhé zapsal Teaching Lab. Neměl jsem z něj takový požitek jako loni, rozhodně se ale nedá říct, že by to byl úplně ztracený čas. Jednak mé chatrné paměti prospělo zopakování některých stěžejních témat (např. zavádění precedentů, tvorba úloh nebo kladení otázek), druhak jsem mohl o představovaných konceptech, vida je podruhé a s odstupem času, uvažovat trochu kritičtěji.

IA006 Vybrané kapitoly z teorie automatů [5 kr, B]

V první polovině semestru očekávejte hromadu různých podtříd bezkontextových gramatik a jejich analysatorů. Na první, druhý i třetí pohled vypadají jeden jako druhý, časem možná začnete vnímat jemné rozdíly (nebo se aspoň nadrtíte definice). Druhá polovina je mnohem zajímavější – automaty nad nekonečnými slovy, bisimulace a logika MSO (která se do tohoto předmětu po mém soudu nehodí, považuji ji nicméně za nejzajímavější část předmětu).

Na přednášky jsem sice občas chodil, nebyl jsem však s to dávat pozor. Většinou jsem na nich proto opravoval C++. Cvičení se konají ob týden a jsou poměrně nabitá. Zápisky z nich mohou sloužit téměř jako jediný učební materiál (je ovšem potřeba si dohledat ještě několik definic, které se na písemkách objevují). Mezi cvičící mimochodem patří doc. Strejček a prof. Barnat, kteří jinak skoro necvičí, takže nepromeškejte tuto šanci na dobrá cvika.

Nepodléhejte ilusi, že otázky z vnitra se neobjeví u zkoušky. Na obou jsem měl například zadefinovat DPDA (což se dá vymyslet na místě) a jakési „platné položky pro řetěz γ“ (což jsem vymyslel na místě jen zázrakem).

IA008 Computational Logic [6 kr, A]

Předmět je natolik zajímavý, že jsem se na jeho cvičení donutil vstávat o šesti (ne však tak náročný, abych navštěvoval páteční přednášky). Různé druhy logik a jejích důkazových systémů, dotknete se mj. Prologu, modálních a temporálních logik, takže možná konečně pochopíte, co vás Popel nebyl schopen naučit. Často je to hodně mechanické, ale i tak dost zajímavé a přitom vcelku oddechové.

Zkouška je směšně jednoduchá a silně zaměřená na příklady. Značnou část tvoří logické důkazy v různých systémech (k nimž máte i pomocné materiály, stačí si ze cvika pamatovat, o co šlo): resoluce v predikátové logice (pracné, ale datelné), převod formule predikátové logiky na množinu klausulí (dá se něco přehlédnout, jinak snadné, pokud místo ekvisatisfítek nepoužijete ekvivalentítka), důkaz predikátové formule pomocí tabel, důkaz modální formule pomocí tabel (naprosto mechanické), důkaz predikátové formule přirozenou dedukcí (která není vůbec přirozená, ale jednoduše se ji naučíte). A abych nezapomněl, několik kraťoučkých a jednoduchoučkých teoretických otázek (typu „jaká je složitost SAT“).

IV125 Seminář laboratoře Formela [3 kr, P]

Ne že by mi snad flákání přednášek výpočtové logiky zajistilo volný pátek. Se skupinkou šíle zájemců jsme totiž pronikali do tajů počítačem asistovaného dokazování a vedeni knihou (a dvěma lidmi, kteří tutéž cestu již byli podnikli) se učili používat dokazovací asistent Coq. Abychom z této bohulibé činnosti vytřískali i nějaké ty kredity, bylo naše páteční coqání zastřešeno seminární skupinou tohoto Formelího předmětu. Pro četné momenty prozření, uvědomění a uspokojení z dokončeného důkazu, občasnou očekávatelnou blbou narážku a (jako důsledek spádu pod Formelu) přístup ke kávovaru musím tento předmět hodnotit jako nejlepšejší v celém širém rozvrhu.

Mimochodem, Nikola slíbil, že v podobném duchu budeme příští semestr pravidelně rozjímat nad teorií kategorií, tak jsem zvědav.

MA007 Matematická logika [5 kr, A]

Tento semestr byl vskutku bohatý na logiku nejrůznějších podob. Stejně jako u té výpočtové jsem se neobtěžoval chodit na přednášky, ze cvik (která jsou opět jen jednou za čtrnáct dní) jsem si toho nicméně neodnesl dost. Podle jedné suplované hodiny se odvažuji tvrdit, že kdybych si byl býval zapsal cvičení s Davidem Klaškou, byl bych si přeci jen odnesl o ždibíček více. Vše potřebné jsem se nicméně zvládl naučit ze slajdů a sbírky zřídka-i-řešených^gr. příkladů při pozdněvečerním^gr. řešení sad domácích úloh. Ty se píší, jakkoli je to na fakultě, kde do vás téměř od prváku, nebo přinejmenším od automatů, hustí LaTeX, neuvěřitelné, ručně. Na zkoušce se pak objevují podobné příklady a k tomu něco definic. Zpočátku se mi ten předmět nepáčil ani zdaleka jako ostatní logika téhož semestru, ale sedě nad sadami jsem si k němu cestu našel a nakonec se mi to docela líbilo. A ke známce mi David osobně poblahopřál, tak to bylo docela milé :).

MV008 Algebra I [6 kr, D]

První déčko, ju-fakin-pí. Ale co mě mrzí víc, je, že mě celé to utrpení nijak zásadně neobohatilo. Sice jsem si to zapisoval jen jako rozjezd před Algebrou II (což bylo asi stejně pomýlené rozhodnutí), ale i tak jsem čekal nějaké hlubší proniknutí do grup. Jak se ukázalo, mnohem zajímavější věci se dělaly už na MB204 (diskrétka for co-dummies) a zde se velkou část semestru dělaly polynomy, jimž doposud nepřicházím na chuť. Nejhorší je samozřejmě to, že je na zkoušku potřeba umět mechanicky počítat a nedělat blbé přehlížecí chyby. Najít největší společný dělitel dvou mnohočlenů napoprvé se mi nepodařilo ani jednou.

Ale jedna dobrá věc z toho přece jen vzešla: Cayleyho representace, již jsem (přes nějakou analogii s funkckem) jakž takž pochopil, což mi v kategorii pomůže pochopit Yonedovo lemma.^spoiler

PA008 Překladače [5 kr, A]

Předmět, na jehož přednášky jsem sice chodil, ale většinou jsem na nich řešil funkcko. Velká spousta starých věcí, o nichž ale nevím, jestli jsou i zastaralé. SSA se řešilo jen krátce, takže velká část asi ano, ale třeba atributové gramatiky se, pokud je mi známo, píší stále. Ty se mi poměrně líbily a i to psaní jednoprůchodového překladu nějaké řídicí struktury na zkoušce bylo vlastně docela zajímavé mentální cvičení.

Největší přínos předmětu nicméně spočívá v jeho poněkud obstarožních učebních materiálech, v nichž jsem konečně nalezl tu strašlivou pravdu. Hašovací tabulka se česky řekne TABULKA S ROZPTÝLENÝMI POLOŽKAMI.