Gymnázium Jana Keplera

 

Absolventu našeho gymnázia Janu Růžičkovi se podařilo zvítězit v kategorii Ingenium „Svět počítačů a komunikace“ soutěže Česká hlavička. Jeho soutěžní práce pojmenovaná „Opetopické komplexy v kontextu teorie typů“ stavěla na maturitní práci z informatiky, kterou Honza úspěšně obhájil v minulém školním roce.

Drobný vhled do tématu, se kterým Honza soutěž vyhrál, nám může dát medailonek projektu uvedený na webových stránkách soutěže: „Jan Růžička se věnuje teorii typů. Co je teorie typů? Jde o matematický formalismus, který lze použít k popisu počítačových programů. Jeho prostřednictvím lze průkazně dokazovat vlastnosti existujících programů. K čemu je to dobré? Programy musí být spolehlivé – např. systémy v letadle, automobilu či lékařských nástrojích. Opetopy jsou matematické struktury, které se podobají vícedimenzionálním stromům. To se v teorii typů hodí, neboť téměř všechny koncepty, s nimiž pracuje, se řídí stromovou strukturou. Stromovou strukturu si lze představit jako hierarchii komponentů a právě na hierarchiích je založena většina (nejen) počítačové infrastruktury (souborové systémy, běžící aplikace, koordinátory semaforů), opetopy nejsou prvním pokusem o formalizaci programů. Zhruba od 90. let se začalo objevovat mnoho efektivních a robustních programů, které slouží k formalizaci jiných programů. Říká se jim asistenční důkazové systémy. Navzájem se liší svou vnitřní teorií, která udává, jak snadno/rychle lze určitá tvrzení dokázat a jakou „sílu“ daný asistent má (kolik tvrzení je teoreticky schopen dokázat). Společné mají to, že důkazy reprezentují textuálně, a to i přesto, že většina objektů, které počítače využívají, jsou hierarchicky strukturované. Jsou opetopy v tomto ohledu lepší? Ano; důkaz týkající se nějakého programu, zakódovaný v opetopu, často odráží podobu daného programu. Je tedy nejen snazší jej pochopit, navíc se nám otevírají nové možnosti k větší automatizaci či znovupoužití důkazů, založené na strukturní podobnosti dvou programů. Navíc důkazy zapsané v opetopech jsou poměrně kompaktní a triviálně přenositelné. Díky tomu na jednom může snadno pracovat více lidí naráz. Opetopy jsou zatím ve fázi matematického výzkumu.  Existuje však několik nástrojů, které umožňují praktickou manipulaci s nimi: jeden vyvinul Jan Růžička v rámci své maturitní práce. K průmyslově použitelnému nástroji ještě zbývá vyřešit několik otázek, ale po technické stránce lze jeho omezenou podobu vytvořit již dnes.“

 

Soutěž Česká hlavička je jedním z nejprestižnějších tuzemských ocenění pro nadané studenty zabývající se především technickými a přírodovědnými obory. Letos byly ceny předány již po patnácté. Jedná se o historicky teprve druhý úspěch studentů našeho gymnázia v této soutěži. V roce 2014 zvítězila Lucie Studená v kategorii Sanitas „Život a zdraví člověka“.

 

Záznam slavnostního galavečera z předávání ocenění je dostupný na stránkách České televize.