Logika a informatika

[davkol]

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?

https://i.stack.imgur.com/KDi5d.png

Na tom je vtipné to, že ten obrázek je špatně. V relačním modelu jde o... wait for it... relace.

[Reklama]

[davkol]

...resp. dá se najít výklad, ve kterém špatně není (A, B jsou až výsledky operace), což ale není zrovna intuitivní, když JOIN není množinová operace jako ty, jež se typicky Vennovými diagramy znázorňují.