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…

Amikor érdemes játékmotort késziteni

A mondás
A játékkészítő közösségben van egy mondás, hogy "Készíts játékot, ne játékmotort".
Szerintem ez a mondás nagyon is igaz abból a szempontból, hogy ha tényleg játékot akarsz készíteni, akkor válasz egy jól ismert játékmotort és kezd el a fejlesztést, mivel ezek az eszközök azért vannak, hogy megkönnyítésék a játékkészítést  és ugyebár mi értelme van feltalálni a kereket ismét?
Viszont itt is lehet találni kivételeket, amikor igenis el kell gondolkozni egy saját játékmotor fejlesztésén.

Mikor érdemes tehát belefogni?
 Most csak az én esetemet tudom felhozni, ami nem más mint a saját 2D HTML5 játékmotorom, amit DartRocket- nek hívok. Az én esetemben az ok egyszerű volt. Dart nyelven nem volt egy igazi játékmotor sem és én Dart-ban akartam játékokat készíteni.
Itt találtam is egy kiskaput mivel ha nincs játékmotor, akkor csinálni kell egyet. :D


Hogyan kezdődőt el?
Ha időrendben akarok menni, akkor azt kell mondanom, hogy négy időszak volt, ami meghatározó volt.

Phaser: Ebb…

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…