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
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