Szerkesztő:Prohlep/ALAP

Figyelem: ez egy egyéni véleményt tartalmazó oldal.

ALAP egy 1998-ban bevezetett rövidítés: Algebra + Logika + Algoritmusok + Programozás.

Algebra	Logika
Algoritmusok	Programozás

E négy téma 2x2-es elrendezésben szorosan összefügg egymással.

E négytagú felsorolás hiányosan, de azért találóan felöleli a matematika modern alkalmazásának alapjait. Hiányos, mert például a halmazelméletet expliciten nem említi. Felöleli, mert a példánál maradva, implicite ott a Halmazelmélet is, ha tudjuk, hogy az Algebra, Logika és az Algebrai logika mi mindenre kiterjed, mi mindent érint közleről. Sztochasztika is közvetve megjelenik, például a logika és algoritmusok kapcsolatában is: egyes posztmodern logikai rendszerekben fontos a játékelméleti szemantika, amelynél az igazság egy megfelelő nyerőalgoritmus lététől van függővé téve. Játékelméletnek azonban egyik alapvető üzenete, hogy determinisztikus jellegű kérdésben az optimumot szolgáltathatja a véletlen. Ez egy lehetséges útvonal a logikától és algoritmusoktól indulva a sztochasztika nélkülözhetetlenségéig. Egy másik útvonal az, hogy a gödeli korlátok miatt a mesterséges intelligencia nem remélheti a problémái megoldását a determinisztikus algoritmusok és logika összeházasításától. A korlátok megkerülésére egy lehtséges remény a Sztochasztika céltudatos alkalmazása.

Matematika modern alkalmazásának zöme a Számítógép-programozáson alapul. Programozáshoz tudni kell, hogy milyen eljárást célszerű alkalmazni, és hogy azt milyen nyelven célszerű elmondani a számítógépnek. E két dolog elméleti alapjait rendre az Algoritmus elmélet és a Matematikai logika szolgáltatja. Algoritmusok és Logika kölcsönhatása mentén fejlődött ki a modern Algebra. Így támasztja alá egészen alapvető módon a szóbanforgó 2x2 téma az Alkalmazott matematikát.

ALAP-ra támaszkodó nemzetközi projektek

Az alcím sugallásával ellentétben szó sem lehet teljességről, mert az ALAP minden olyan projektnek alapeszköze, amelynek célja a matematizálás támogatása számítógépes vagy akár egyenesen mesterséges intelligencia irányból. Ilyen projektekből igen sok van, és nehéz az utókor helyett most előre megítélni, hogy közülük melyek a legjelentősebbek a matematika modernizálódása szemszögéből. Tehát az alábbi lista sem kiterjedtség, sem pedig jelentőség szemszögéből nem tekintendő mérvadónak, csak ízelítőnek, csak bemutató az érdekődők számára.

• A Mizar projekt 1973-ban indult a hazai matematikusok körében is igen elismert Bourbaki projekt számítógépes változataként . 1935-től kezdődően, a többségében francia bourbakisták a göttingeni iskola, részben Hilbert, és két algebrista, Artin és van der Waerden legjobb ötletei mentén haladva, a közös Nicolas Bourbaki álnéven 9 kötetben megírták az akkori matematika egy jelentős részét olyan sorrendben, hogy minden az alapoktól eredeztetve teljesen egzaktul legyen levezetve. Ennek azért látták szükségét, mert a XIX/XX. századfordulón a logikai paradoxonok borzolták a precíz bizonyítottságra kényes matematikusok idegeit. A projekt meg azért volt kivitelezhető 1935-től kezdődően, mert azt jóval megelőzően, a XX. század elejére a matematika logikai és halmazelméleti alapjait megnyugtatóan tisztázták. 1973-ban a Mizar projekt csak annyit tett hozzá a bourbakisták eszköztárához, hogy mindezt számítógéppel ellenőrízve tervezték megvalósítani. Fontos az 1973-as dátum. Akkorra már látszott, hogy a mesterséges intelligencia gyors megvalósíthatóságával kapcsolatos 60-as évekbeli nagy remények tarthatatlanok. Ennek megfelelően a Mizar projektben a bizonyítást nem kerestetik számítógéppel, hanem csak a szövegszerkesztővel megírt bizonyításokat ellenőríztetik számítógéppel. Ez utóbbi „csak” szakmailag nem is annyira „csak”, hanem komoly számítógépes logikai és számítógépes nyelvészeti feladat. Nem véletlen, hogy a projekt őstagjai többségében nyelvészek, hiszen aki már írt matematika cikket szövegszerkesztővel, az saját magán tapasztalhatta, hogy a számítógépes szemszögből jól megírt cikk a begépelést végző szemszogéből mennyire az olvashatatlanság határát súrolja, így a munka lassú. Ezt messze előre látva, elkezdték egy olyan mesterséges nyelv kidolgozását, amely amennyire csak lehet, hasonlít ahhoz, mintha valaki a természetes angol nyelven beszélne matematikáról. Szép nyelvtervezési, nyelvfejlesztési feladat, siker. Nem kisebb feladat volt ezzel párhuzamosan olyan intelligens nyelvi elemzőt készíteni, amely determinisztikus bizonyossággal felismeri az ezen a mesterséges nyelven beírt szöveg tényleges jelentését. Innét már szinte gyerekjáték a jelentés helyességének, azaz a bizonyítások helyességének ellenőrzése. Matematikát ténylegesen az alapjaitól felépíteni annyira babra munka, mellesleg Neumann János zseniális számosság definíciós ötletét sem nélkülözheti, hogy a bölcs nyelvészek az egymással párhuzamos munkavégzés érdekében úgy döntöttek, hogy mankóként jópár nemtriviális fogalom tulajdonságainak bizonyítottságát átmenetileg elfogadták leellenőrzöttnek. Nagyjából 27 év után jutottak el oda, hogy ezen mankókat kivehették a rendszerből. Azaz az ezredfordulótól már minden, ami a Mizar rendszerben fellelhető bizonyítás, az bizony számítógéppel ellenőrzött, és így reményeink szerint megbízhatóbb, mint az emberi kézzel ellenőrzött matematika. Hogy ez mennyire nem oktalan rémlátomás, arra bizonyíték, hogy a Mizar projekt emberei több ismert bizonyítás hibáit javították ki a számítógépes ellenőrzésnek köszönhetően.

• Az OMDoc projekt a német mesterséges intelligencia kutatás Computer Center e-Learning és a Siekmann vezette Omega csoport igényeiből nőtt ki. A CCEL csoportnak a nevében is benne van, hogy számítógépel segített tanítással foglalkoznak, de amitől nehéz, hogy matematikára koncentrálnak. Az Omega rendszer egy meglepően komplex bizonyítások megtalálására képes magasrendű bizonyításkereső rendszer. Ahogy autóipar számára fontosak a különféle autóversenyek, úgy számítógépes bizonyítás keresésben is vannak versenyek, vannak nevezetes tesztfeladat gyűjtemények. Ezen feladatokat mindig a tesztelni kivánt rendszer nyelvére kell fordítani, sokszor kézzel kiigazítani a fordítást. Ehhez hasonlóan, a tanító rendszerek, az e-Learning is szeretne bárhonnét származó anyagot felhasználni, azaz ismét fordítási probléma lép fel. Világossá vált, hogy nem halogatható egy olyan nyelvi szabvány kidolgozása, amely később ISO szabványnak felterjeszthető, és alkalmas bármilyen matematikai tartalom, tehát nem csupán forma tárolására, mint a TeX/LaTeX, hanem a tényleges matematikai szerkezet tárolására. Ez lett az OMDoc, amely elnevezésben az OM az Open Math, nyitott matematika kezdeményezésre utal, a Doc pedig hogy dokumentum formátumrol van szó. Az OMDoc egy XML alapú nyelv, amely a fentebbi Mizarral ellentétben ember számára szinte olvashatatlan, de cserébe egy sima XML értelmező is képes a feldolgozására. További különbség, hogy magához az nyelvhez itt nem tartozik tartalom helyesség ellenőrző, csak a formai helyesség lehet a kérdés. Ez nem hiányosság, hanem sokoldalú felhasználásra szánták azzal, hogy aztán mindenki azt ellenőriz a tartalmon, arra használja a tartalmat, amire akarja. Egyik ilyen fontos felhasználás az ActiveMath e-Learning rendszer. De természetesen bármely matematikai bizonyításkereső rendszerhez adaptálható, így az Omega rendszerhez is adaptálták. Az OMDoc mögötti elismert szakmai potenciál (számítógépes világhálózatba szervezett matematikai szerverek rendszerének fejlesztése) miatt várható a szabvány elterjedése.

• A Geometry Constructions LaTeX converter, azaz a GCLC projekt neve kissé megtévesztő, a program már a jelenlegi állapotában is ennél lényegesen mélyebb dolgot tud. E projekt nem összemérhető az előző kettővel, kisebb, de tartalmilag tanulságos. A geometria manapság picit árvagyermek, pedig a látszat ellenére nehéz. A XIX. század első harmadában két jelentős matematikai mérföldkő született, mindkettő kapcsolatos a geometriával, de nagyon eltérő módon. Az egyik a magyar Bolyai János és az orosz Nikolai Lobachevsky kutatásai a párhuzamossági axióma környékén, amely geometriai szemszögből szemléletileg előkészítette a természettudományt a speciális relativitáselmélethez, és szemléletileg felkészítette a matematikusokat a modell elméletre és a XX. századi meglepő konzisztencia tételek elvi lehetőségére. A másik a francia Évariste Galois vizsgálatai az algebrai egyenletek gyökjelekkel való megoldhatóságáról. Ez elvezetett ahhoz az igen meglepő tényhez, hogy amennyiben el akarjuk dönteni, hogy egy geometriai szerkesztési feladat elvégezhető-e csak körző és vonalzó használatára szorítkozva, akkor ez pontosan attól függ, hogy a szerkesztési feladatból leszármaztatható csoport rendelkezike-e egy sok más szemszögből is érdekes tulajdonsággal, nevezetesen hogy feloldható-e. Az egész modern algebra kifejlődésének az így kialakult Galois Elmélet adta a legnagyobb lökést. Az algebra ilyen gyökeres modernizálódása aztán húzta magával a matematika alapjainak kitisztázását is. Ezen algebrai fejlődés egyik ága a Gröbner bázis technikájának kialakulása, amelyet a számítógépes világhálózatban végzett adatbányászaton túlmenően, lehet geometriai tételek bizonyításának megkeresésére is használni. A linzi Bruno Buchberger-féle Gröbner bázis alapú geometriai tételbizonyító algoritmus is be van építve a GCLC projekt, első ránézésre bárgyú geometirai rajzolgató-szerkesztgető programjába. Aki a GCLC programban felhasznált matematikai fogalmakat és tételeket el tudja magyarázni, annak MSc szinten is kapásból odaítélhető egy jeles(5) algebra szigorlati eredmény. Ennyire megtévesztő tud lenni egy projekt elnevezése.

• Kifejezetten nagy és matematikailag általános célú projekt a Wolfram Mathematica, a Waterloo Maple és a paderborni MuPAD, de egyik sem szabad szoftver, ennek előnyeivel és hátrányaival. Mindhárom rendszer eltérő hangsúlyokkal és preferenciákkal, de végülis egymáshoz hasonló dolgot tud: a nem matematikusoknak tanított matematika tananyag első négy féléves anyaga aktív tankönyv szerűen feldolgozható bennük, továbbá a kiszámolási, ábrázolási és animációs feladatok zöme elvégezhető. Magasabb matematikához és kutatáshoz is jól használhatóak, de akkor már fokozottan szükség van arra a felhasználói értelemre, hogy mit szabad és hogyan érdemes megcsináltatni ezekkel a programokkal. Ezek magas szinten programozható kalkulátorok, de nem deduktorok. Azaz számolni igen jól tudnak, de ha valakinek tételbizonyításra van szüksége, akkor ezek nem valók arra. Ennek ellenére, és ez az amiért egyáltalán a felsorolásban helyet kaphattak, a zárt és normál felhasználónak hozzáférhetetlen forráskód ellenére, pusztán a program viselkedéséből világos, hogy mindegyik a színfalak mögé rejtve tartalmaz valamilyen szintű deduktort, azaz következtető rendszert. Ezek szintjét és tudásást körbe lehet tapogatni azzal, hogy milyen szimbólikus számolási feladatnál milyen mértékig előrehaladott eredménye van. Számítógépes logika és algebra nélkül még a komolyabb szimbólikus integrálás sem lehetséges, márpedig azt még az elsős diák is elvárja egy szimbólikus kalkulátortól. Azaz egy komolyabb rendszer akkor is tartalmaz nemtriviális algebrát és logikát, ha a felhasználónak csak kalkulátor szerű kiszámolásokat kínál föl. E három példa plasztikusan mutatja az ALAP értelmét.

• Igen kiemelkedő szakmai minőségú szabad szoftverek a matematikában inkább a speciális igényeknél, és egyúttal piacilag nem perspektívikus témákban fordulnak elő. Sok más lehetséges példa közül önkényesen kiszemelve, ilyen kiemelkedő alkotás a müncheni Isabelle általános logikai keretprogram és az aacheni GAP absztrakt algebrai program. Ez utóbbinal figyelemreméltó a honlap puritánsága is, miközben szakmailag csúcsszoftverről van szó. Részletesebben, az Isabelle rendszert azért hívják keretprogramnak, mert önmagában nem képes normális bizonyításra, hanem először meg kell adni neki az általa alkalmazandó logika leírását. Ettől olyan jó, ezért használják azt a szlogent, hogy a következő ezeregy tételbizonyító, hiszen ehhez mindössze ezeregy különbözö logikai rendszer leírását kell létrehozni, és mindegyikkel elindítani a keretrendszert. Mire jó ez? Olyanra könnyű gondolni, hogy legyen X és Y két kijelentés, amelyek kölcsönösen egymás tagadásai. De nemtriviális matlogikai rutin kell ahhoz, hogy valaki arra gondoljon és olyan helyzetben is szikár logikussággal dolgozzon, ahol van három kijelentés, X, Y és Z úgy, hogy azok kölcsönösen egymás tagadásai. Ismét algebra jön elő, lásd ALAP, mert ehhez elég feladni azt a szinte velünkszületett reflexet, hogy egy kijelentéshez szorosan társítjuk azon elemi események halmazát, amelyeknél a kijelentés igaz. Az X, Y és Z, hármas eset így nem mehet (aki érti, annak: a halmazok szokásos műveletei disztributívak, mig a szóbanforgó hármas eset a disztributivitást kizárja). Lineáris algebra azonban segít, mert arra kell magunkat átállítani, hogy a kijelentésekhez ne a megszokott halmazt társítsuk, hanem az elemi események összességét valahogy vektortérnek látva, a szóbanforgó halmaz generálta lineáris alteret kell társítani, és akkor máris lehetséges a szóbanforgó hármas eset. Hát ezt jól el lehet keverni, ha az ember a saját fejével akar gondolkodni ilyen szokatlan szabályokkal. Az Isabelle keretprogramot éppen az ilyen helyzetekre írták, hogy a gép cinikus szikársággal kövesse a szokatlan helyzet szokatlan szabályait. Még mielőtt bárki is azt gondolná, hogy itt unatkozó matematikusok szellemi szórakozásáról van szó, azelőtt mindenki gondoljon bele, hogy a számunkra fontos informatikai forradalomban milyen jelentősége van a tranzisztoroknak, félvezetőknek, és hogy azok megalkotásában milyen centrális szerepe van a kvantummechanika kialakulásának, és a szóbanforgó hármas eset mindennapi vendég a kvantummechanika természetes logikája-ban. Az Isabelle rendszernek persze beadható a szokásos magasabb rendű logika, angol rövidítéssel a HOL. Az így adódó Izabelle/HOL elég erősnek bizonyult ahhoz, hogy az axiomatikus halmazelmélet felépítéséhez szükséges bizonyítások mindegyikét önállóan megtalálja. Áttérve az aacheni GAP rendszer részletesebb ismertetésére, az elnevezés a Csoprotok, Algoritmusok és Programozás angol megfelelőjének kezdőbetűs rövidítése. A porosz születésű Joachim Neubüser 1961-ben kezdett szimbólikus, tehát nem konkrét számokra vonatkozó algebrai feladatokat számítógéppel megoldani Kielben. Ezzel kezdetét vette az a negyed évszázad, amikor az évszázad tételének tartott, a véges egyszerű csoportok klasszifikációja című, mintegy végülis tizezer oldalra becsült, igen komplex bizonyítású tételhez azzal járult hozzá, hogy számítógépes vizsgálatokkal számos elvi szinten szóbajövő lehetőséget kizárt, és így nem kellett emberi gondolkodást pazarolni azon esetek átgondolására. 1986-ban már Aachenben tanár, és egy konferencia első napján beszél arról, hogy a sok összegyűlt igen értékes csoportelméleti algoritmust egy egységes rendszerbe kellene foglalni. Három tehetséges diákja éjt nappallá téve programozott, és az ötödik nap reggelén letették az asztalra a GAP-0.0 rendszert, amely egy pascal-jellegű keretet adott a meglévő csoportelméleti algoritmusoknak. 1996-ig kicsiszolódott ez a kezdeti rendszer, lett belőle a GAP-3. Természetesen idealista tudósokhoz méltóan a forráskód is nyilt, amelynek elolvasása először zavarbaejtő, majd kétségbeejtő, és ha még mindig nem hagyja félbe az ember, akkor egyenesen demoralizáló. A rendszer belső magja C programozási nyelven írták, és a megjegyzések között már 1994-ben is volt a kód helyességének indoklása gyanánt utalás egy 1992-es PhD disszertációra! A rendszer GAP nyelvű, igen kiterjedt algoritmus könyvtára pedig messze több, mint amit egy algeba PhD fokozat kapcsán bárkitől is el lehetne várni. Ezt úgy érték el, hogy valahányszor született egy jó algebrai algoritmus, akkor az algoritmus egy jó ismerőjét meghívták egy-két hétre Aachenbe, és azalatt az illető vezetésével megírták az algoritmust a GAP nyelven. Így a GAP mindig szinte hónapra kész volt abban, hogy a csoportelméleti alapkutatás mit tud. 1995/96-ban radikális változtatást hajtottak végre a GAP belső magján, amitől a GAP könyvtárakban alkalmazható GAP nyelvezet az objetum orientált C++ programozási nyelv mai (2008) objetum orientáltsági szinvonalát messze meghaladták. A C++ nyelven az egyes objektumon elvégezhető műveletek mindegyike csak egy-egy objetumhoz kötődhet. Egy adott kinézetű műveletből is csak egyfajta lehet. Azonban a matematika természete nem ilyen. A matematikai műveletek hajlamosak egyszerre több objektumot feldolgozni, amelyekhez egyformán kötődnek, így nem természetes ezek közül az egyikhez kötni. Továbbá matematikusok hajlamosak az ugyanolyan kinézetű műveletekre a konkrét helyzettől függően az adott helyzetet jól kihasználó algoritmusokat írni. Emiatt a C++ nyelvet messze meghaladva a GAP-4 nyelvnél az elvégzendő műveletek egyszerre sok objektumhoz kötődhetnek, és azonos kinézetű műveletből akár sok tucat variáns is beregisztrálható. Ennek az az eredménye, hogy egy C++ nyelven megírt algoritmust szinte szó szerint áttéve GAP-4 nyelvre, egy 10x lassabb futású programot kapunk, hiszen előszöris a GAP-4 nem kompilált hanem interpretált nyelv, és a futásidőben kell igen körültekintően kiválasztani, hogy a sok-sok megengedett algortimus verzió közül az adott helyzetben melyik a nyerő, melyiket futtassa a rendszer. Hát akkor ez mire jó? Arra, hogy a GAP-4 nyelven az interpretáltság miatt könnyebb matematizálni, mert minden azonnal kipróbálható, és a 10x lassuság pedig egy matematikusnak azt jelenti, hogy legalább képes kiszámoltatni azt, amire szüksége van. Ugyanis ez a 10x lassuság arra fordítódik, hogy az interpretáltság miatt a valóságos élet tapasztalatai szerint a matematikus eléggi ki fogja csiszolni a programját, és a helyzethez illő algoritmus kiválasztására fordított jelentős idő meg ott jön vissza többszörösen, hogy a program rettenetesen jól alkalmazkodik a futás közben folyamatosan alakuló matematikai lehetőségekhez, és azokra azonnal lecsap és erősek kiaknázza. Számítógépes matematikában sok esetben az a nyerő, ha a program nem nyers erővel siet, hanem hosszasan vacakol azzal, hogy mit lenne érdemes meglépni. Talán informatikusok számára lehet ez igen tanulságos, a GAP-4 egy tanulmányozásra érdemes nyelv.

Lábjegyzetek

{{csonk-matematika}} [[Kategória:Matematika]] [[Kategória:Algebra]] [[Kategória:Logika]] [[Kategória:Algoritmusok]] [[Kategória:Számítógép-programozás]] [[Kategória:Alkalmazott matematika]]