Logika a informatika

[stud]

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?

[Reklama]

[Ondra Satai Nekola]

Vycislitelnost?
(plus samozrejme takove ty trivialni "stredoskolske" znalosti logickych funkci a operaci s nimi.)

[Ivan Nový]

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?

Logika je dobrá pro každého. Nejen pro programátora. Logika pro programátora je jako noty pro hudebníka, ovšem samouci hrají i bez not. Jinak je to, jako byste se zeptal, proč potřebuji tolik peněz. Znalostí a peněz není nikdy dost. Třeba se za 20 let dostanete do koncentračního tábora, a díky znalostem, které nyní získáte, přežijete :-))) Ale teď vážně, je dobrá proto, abyste za pár let uspěl v konkurenci s myslícími stroji a měl práci.

[Radek Miček]

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.

[davkol]

Jednou informatika, pak IT, pak programátor. Pokud bych se držel té informatiky, tak logika je skoro všude.

U nás základní kurz logiky

• vrcholil u vět korektnosti a úplnosti, analogie téhle látky jsou pomalu na každém kroku (např. funkční závislosti @ relační algebra/kalkul, Hoarova logika @ dokazování správnosti programů);
• pokračoval úvodem do fuzzy logiky nebo logického programování…
• …a pak jsou věci jako SAT.

[Reklama]

[Yarda]

A jakou logiku to máte? Jsou různé. Třeba filosofická, matematická (třeba Booleova) a ženská.
 

[zboj]

Jde hlavně o logické programování, tedy Prolog apod., případně nějaké dokazovače. Je dobré vědět, proč je predikátová logika (FOL) úplná, co plyne z její nerozhodnutelnosti, jaké její fragmenty rozhodnutelné jsou, proč jsou modální, temporální a nemonotonní logika fragmenty FOL, jak se převádí logika vyššího řádu na FOL atd. Nejlépe se to člověk naučí na reálných příkladech, typicky z oblasti umělé inteligence.

[ava]

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.

Jo, nedávno jsem na to narazil a moc se mi to zalíbilo. Jako lehké a srozumitelné intro mi posloužila tato přednáška (druhá polovina): https://www.youtube.com/watch?v=TbASMeJSh9s - Adelbert Chang: Reasoning with Types.

Jsem zvědav, zda to někdy použiju v praxi :-)

[Radek Miček]

Jsem zvědav, zda to někdy použiju v praxi :-)

Použití ukazuje třeba Miles Sabin v článku Unboxed union types in Scala via the Curry-Howard isomorphism:

Kód: [Vybrat]

// Definice negace v intuicionistické logice.
// Pro nás je důležitá kontravariance A.
type ¬[A] = A => Nothing
// Union typ získáme pomocí De Morganových pravidel.
type ∨[T, U] = ¬[¬[T] with ¬[U]]
// Podmínka: X má typ T nebo U.
// Bohužel, nejde jednoduše psát A: B |∨| C |∨| D |∨| E.
type |∨|[T, U] = { type λ[X] = ¬¬[X] <:< (T ∨ U) }


[stud]

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?

[alex]

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://www.google.cz/search?q=sql+inner+diagram&client=ubuntu&hs=h61&channel=fs&biw=1847&bih=948&tbm=isch&imgil=mogSTbjuV7hmkM%253A%253BdiCPZV2HP4qaSM%253Bhttp%25253A%25252F%25252Fstackoverflow.com%25252Fquestions%25252F22222225%25252Fsql-outer-join-2-tables&source=iu&pf=m&fir=mogSTbjuV7hmkM%253A%252CdiCPZV2HP4qaSM%252C_&usg=__9_Ux2xH0b4i1f272vRLuSfmXvJQ%3D&ved=0ahUKEwiomJyF8dHLAhUnlHIKHSJoAwUQyjcILg&ei=3vbvVqixCKeoygOi0I0o#imgrc=mogSTbjuV7hmkM%3A

[David]

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?

Jedno z moznych uplatneni je contract based programing. Programator pouziva logiku k definici interface (precoditions, postconditions, ...). Specifikace interface se pak pouziva k testovani nebo dokonce k dokazani toho, ze implementace respektuje specifikaci. Tohle umoznuje relativne dobre napriklad programovaci jazyk SPARK 2014. Existuji nastroje pro contract based programming i pro Javu (OpenJML) nebo C++ (VCC), ale ty jsou z ruznych duvodu dost obtizne pouzitelne pro lidi, kteri nemaji dost presnou predstavu o tom, jak pracuji...

[zboj]

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://www.google.cz/search?q=sql+inner+diagram&client=ubuntu&hs=h61&channel=fs&biw=1847&bih=948&tbm=isch&imgil=mogSTbjuV7hmkM%253A%253BdiCPZV2HP4qaSM%253Bhttp%25253A%25252F%25252Fstackoverflow.com%25252Fquestions%25252F22222225%25252Fsql-outer-join-2-tables&source=iu&pf=m&fir=mogSTbjuV7hmkM%253A%252CdiCPZV2HP4qaSM%252C_&usg=__9_Ux2xH0b4i1f272vRLuSfmXvJQ%3D&ved=0ahUKEwiomJyF8dHLAhUnlHIKHSJoAwUQyjcILg&ei=3vbvVqixCKeoygOi0I0o#imgrc=mogSTbjuV7hmkM%3A

Předpokládám, že byla myšlena teorie množin na úrovni VŠ (vzhledem k profilu tazatele), ne tři primitivní operace v SQL. Relační algebra pak není záležitostí teorie množin.

[zboj]

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.

[BLEK.]

vysvetlim ti to polopate
teoria mnozin je starodavny programovaci jazyk pre ludsky mozeg. a kedze sme debili tak su tam mozgove ojeby ako napr. tato veta nie je pravdiva.

potom maz logiku , v kocke asi takto. mnozina po slovensky tiez bitmapa to je ked mas cislo a chodis sprava do lava tak to su tie bity. powerset - potom chodis dolu a hore tomu sa kamarade hovori brute force a z najvacsieho ti to prejebe na nulu to je pretecenie.

a za tym su vsetky mozne boolovske funkcie ale toto ta nemusi stresovat.

s pozdravom, php javascript opica