Ugrás a fő tartalomra

Programozók nem tudnak bizonyitani

Ebben a kis bejegyzésben bizonyításról és annak szerepéről az informatikában lesz a téma.

Bizonyítás
  A bizonyítás nem más mint egy állítás helyességének az igazolása. Bizonyításokat a jó öreg ókori görög matematikusok találták ki és közülük is kiemelkedik Euclid munkája(Elemek).
Bizonyítások érdekessége, hogy készítésük során használhatunk bármilyen már bizonyított állítást, hiszen azoknak a helyességét már bizonyítottuk. Ezáltal a bizonyított állításokból még összetettbe állításokat tudunk megfogalmazni és bizonyítani.
  Bizonyítások szépsége, hogy megad egy biztos alapot, amire az ember építkezhet.

Félelem
  Eddigi tanulmányaim során mindig imádkoztam, hogy a matekos tárgyaknál ne legyen elvárás, hogy tudjam a bizonyításokat. Ami nem meglepő, mivel elég hosszúak voltak(tételhez képest), nehezen érthetőek és nem is értettem, hogy hogyan is csinálták őket. Nem is beszélve, hogy ha a bizonyítás nagyon informális volt, akkor a bizonyítás leírásából hiányozhatott néhány lépés, mert azok "egyértelműek" voltak(vagy csak drága volt a papír és az író takarékos akart lenni).
  Bizonyítások iránti félelmem abból fakadt, hogy egyszerűen nem értettem őket vagyis nem tudtam ,hogy hogyan kell bizonyítani. Van egy megérzésem, hogy ezzel nagyon sok kollégám küzd.

Oktatás
  A magyar egyetemek arról híresek, hogy elméletet nagyon komolyan veszik és ehhez képest eddigi tanulmányai során egyetlen olyan kurzusom se volt, ami magával a bizonyítás készítéssel foglalkozott volna. Viszont ennek ellenére rengeteg bizonyítással találkoztam.
  Lehet példákon keresztül kellet volna megértenem, hogy hogyan kell bizonyítani egy tételt, ami a magam részéről mondhatom, hogy nem vált be. Ez olyan mintha egy középiskolás osztálynak a lisp programozási nyelvet úgy próbálnám megtanítani, hogy csak a példa programok kódját adnám meg nekik.

Idő
  Bizonyítások nagyon időigényes elfoglaltságok, mivel egy bizonyítás elfogadásához kell egy matematikus, aki eldönti, hogy helyes-e a bizonyítás. Tudományos körökben egy komolyabb állítás és annak a bizonyításának elfogadásához általában 2 évet kell várnia a tudósnak és ez még a jobbik eset. Kirívó ellenpéldának itt van Mocsizuki Sinicsi esete, aki egy évtizednyi munkával bizonyította be az abc sejtést, de 3 év elteltével is csak 4 ember érti a bizonyítást.
  Ebben az esetben a folyamatot az emberi tényező teszi nagyon lassúvá. Bizonyítani csak gyakorlással lehet megtanulni, de ehhez kell egy matek tanár is, aki átnézi az általunk készített bizonyítást. Viszont a matek tanárral csak hetente 1-2-szer tudunk találkozni, így a bizonyítás kipróbálásához néha napokat kellene várni.

Megoldás
  Emberiség a történelme alatt mindig kitalálta, hogy hogyan tudná az embert kiküszöbölni a folyamatokból. Ahogy eddig is mindig, most is egy gép vonja ki az embert az egyenletből.
Mi esetünkben ez nem más mint a számítógép által segített bizonyítás avagy más néven tétel bizonyítók(proof assistant) használata.
  Tétel bizonyítók segítségével egy tételt interaktív módon tudunk bebizonyítani és a bizonyításunkat a számítógép ellenőrzi le. Így sikerült kiküszöbölni a matek tanárt és sikerült magát a bizonyítás folyamatát interaktívvá tenni, ahol a számítógép minden lépésnél visszajelzést ad, hogy éppen hogyan állunk a bizonyításban.
  Az egész folyamat nagyon hasonlít a programozáshoz, hiszen a munkafolyamat ugyan az vagyis egy nagyobb problémát kisebb egyszerűbb problémákra bontunk fel. Bizonyítások esetében  egy nagyobb bizonyítást sok kisebb bizonyított állítások segítségével építünk fel.

Motiváció
  Persze jöhet a kérdés, hogy minek tanuljon meg egy programozó bizonyítani?
Bizonyítás szépsége, hogy bármilyen állításra lehet használni őket és maguk a programok is állítások sokaságából állnak össze. Egy metódus/függvény is egy állítás, ami azt állítja, hogy bizonyos bemenet hatására bizonyos kimenetet produkál. Tétel bizonyítóval ezt az állítást tudjuk megvizsgálni, hogy ténylegesen teljesül-e.
  Ezt a folyamatot formális verifikációnak hívjuk, ahol egy specifikáció alapján tudjuk verifikálni a rendszert vagyis le tudjuk ellenőrizni, hogy a rendszer tényleg azt csinálja, amit mi akarunk.
Formális verifikáció egy nagyon nagy, érdekes és fontos területe az informatikának, amiről érdemes tudni és figyelni az onnan érkező eredményeket mint például a Compcert, ami egy formálisan verifikált C fordító.

Ajánlott irodalom
  Software Foundations: Ebben a témában ez a könyv alapműnek számít. Iszonyat mennyiségű tartalom található meg a könyveben és legjobb benne, hogy online ingyen elérhető. Még mindig olvasom a könyvet, de nagyon pozitív tapasztalataim vannak a könyvel kapcsolatban.

Zárszó
  Szoftverfejlesztés kezd olyan irányba elmozdulni, hogy a jövő szoftverei már bizonyítottam biztos alapokon fognak nyugodni. Ahogy a matematikának úgy a szoftverfejlesztésnek is kellet egy kis idő, hogy fontos szerepet kapjon benne a bizonyítás.

Ahogy harcban, úgy a programozásban is fontos a fegyver megválasztása :D

Megjegyzések

Népszerű bejegyzések ezen a blogon

Python kezdőknek

Itt a nyár és mivel lehetne ezt a legjobban megünnepelni, mint egy kígyóról elnevezett programozási nyelv bemutatásával. Következőkben tehát a Python programozási nyelvről lesz szó és annak lehetséges alkalmazásairól.

Miért tartsunk otthon Python-t? Python pályafutása 1991-ben kezdődött el egy Guido van Rossum nevű fejlesztőnek hála, aki egy olyan általános programozási nyelvet akart készíteni, amit nagyon könnyen el lehet sajátítani és használni. Az elmúlt év tizedek alatt a Python nyelv az egyik legjobb és legnépszerűbb általános programozási nyelvé nőtte ki magát, amit bizonyít, hogy számos operációs rendszeren(linux, mac os) alapból megtalálható a nyelv. De nézzük meg, hogy mitől ilyen népszerű: Egyszerűség: A nyelvnek az egyik legnagyobb előnye, hogy nagyon egyszerű és ezért például nagyon sok egyetemen a kezdő programozó legényeket Python segítségével vezetik be a programozás világába.Dinamikus: Mint minden dinamikus nyelvnek úgy Python-nak is van egy beépített REPL-je, ami nagyo…

HTML5 játék fejlesztés alapjai

Ahogy a cím is sugallja a HTML5 játék fejlesztés alapjairól lesz szó ,hogy mi is kell hozzá.
Az én tudásom ebben a témában még elég kicsi ,de egyre növekszik ,talán egyszer majd én is össze fogok szedni annyi tapasztalatot a témából ,hogy akár még könyvet is írhatnék róla. Na persze egy izgalmas könyvet. :D

Na akkor vágjunk is bele!
    Első kérdés ,hogy mi a legalapvetőbb dolog ,amit ehhez meg kell tanulni? Persze sokan mondhatják ,hogy html , javascript ,css ismerete ,ebben igazat is adnék ,de nekünk még van ennél sokkal alapibb tudás ,ami a magyar programozókra főként igaz ez pedig az angol tudás.
Ezt nagyon sokszor tapasztalja az ember ,hogyha nem elég jó az angolja ,akkor egyetlen mondat is megtudja akasztani ,ahol az író nagyon szakmai akart lenni.
Főleg emiatt szeretem azokat az írókat ,akik semmi köntörfalazás nélkül belevágnak a lecsóban és simán és egyszerűen elmagyarázzák a dolgokat.

   Ha az első szint megvan akkor jöhet a HTML tanulása ,ami elég gyorsan letudható ,hiszen c…

Javascript kezdő lépések

Ma kis bejegyzésem arról fog szólni ,hogy mit érdemes kezdő lépésenként megtanulni ,illetve ,hogyan érdemes haladni Javascripttel és néhány érdekesség is lesz node.js-sel kapcsolatban.

Tanulás
   Szerencsére olyan világba élünk már ,ahol a web és webes technológiák nagyon gyorsan fejlődnek és ezért ezeknek a tanulása is egy fajta fejlődésen ment keresztül. Már nem könyvből kell tanulni ,hanem vannak olyan oldalak ahol interaktív módon lehet egy nyelvet megtanulni ,ami tökéletes a tanulás szempontjából. Előző cikkemben raktam be anyagokat ahhoz ,hogy mit érdemes elolvasni ,ha a tanuló inkább olvasós fajta és volt bent 2 interaktív.  Én például codecademy segítségével tanultam meg Jquery-t használni. Javascripthez Eloquent és codeacademy-t használtam.

   Mivel a Javascript elég megengedő ezért nagyon sok fajta stílusban kódolnak hozzá és ezek a stílusok  néha teljesen eltérőék. Szóval aki tanult már Java ,c vagy c++-t annak is lehet újdonság ,mivel ezeknél a nyelveknél nagyon szépen megv…