Máme teď ve škole (VŠ) logiku a nějak zatím nevidím souvislost s IT. Mohl by mi tu někdo dát nějaký příklad, proč by mě měla jako programátora zajímat?
Programy lze chápat jako důkazy v určité logice (říká se tomu Curry-Howardův izomorfismus). Důsledkem toho jsou programovací jazyky jako například Coq, kde můžete psát certifikované programy - příkladem takového programu je CompCert.
Existuje nějaký podobný příklad praktického uplatnění i pro teorii množin?
Bavíme-li se o nauce o nekonečných množinách (triviální operace nad konečnými množinami, což je látka základní školy, se pochopitelně hodí například při práci s databázemi), tak mě, upřímně řečeno, žádný přímý příklad použití nenapadá. Nicméně některé výsledky nám umožňují lépe chápat některé jevy v logice, jež už své (dost podstatné) místo v IT má. Například díky Cantorově větě víme, že v logice druhého řádu může jít kvantifikátor přes nespočetnou množinu, čímž umožňuje existenci bezesporných teorií, jež nemají model (v té nejjednodušší množinově-teoretické sémantice). Na druhou stranu ale víme, že to vlastně vůbec nevadí, protože nějaké tvrzení je dokazatelné v logice druhého řádu, právě když je dokazatelné v příslušné "zprvořádněné" (firstorderized) teorii, takže různých logik vyššího řádu a teorie typů (používaných zejména pro reprezentaci znalostí a automatické vyvozování v umělé inteligenci) se bát nemusíme (ostatně se s úspěchem používají). Navíc s použitím prostředků teorie množin je možné uspořádat různé (algebraizovatelné) logiky do určité hierarchie, a tak vidět, je-li možné nějakou syntakticky (na první pohled) bohatší logiku převést na výrokovou či predikátovou logiku bez ztráty expresivity.
Zobrazit příspěvky
Jestli se někdo ptá, jak to hergot pythonisti dělají, aby jim to nepadalo na to, že někam místo stringu dají int, tak odpověď je "dělají to v principu podobně jako javisti zabezpečují, aby jim to nepadalo na NullPointerException"
