Grand Slam

A mai analízis 8 vizsgával meglett a royal flush: mind a nyolc kollokvium, és (még anno, két éve) a szigorlat is jeles lett.

Gondolom, a kommentek között mindjárt feltűnik még száz ember, aki a progmaton ugyanezt megcsinálta, de szarok rá, én ma ennek örülök. Egyébként is egy állati izgalmas ride volt ez a négy év a matematika egy szeletének felépítményén át. Megérte! És sok más tantárggyal és előadóval ellentétben, az előadások 90+ százaléka izgalmas és érdekes volt nemcsak utólag, hanem akkor és ott ülve is.

Relativisztikus hiperszámítógépek

Tegnap egy nagyon érdekes előadáson vettem részt, ahol Németi István és team-je ismertette a hiperszámítás megvalósíthatóságának vizsgálata terén elért eredményeit.

A hiperszámítás olyan teoretikus kiszámítási modellekkel foglalkozik, amelyek kvalitatíven erősebbek a Turing-gépeknél (pl. meg tudják oldani a Turing-gépek megállási problémáját, vagy akár Gödel nemteljességi tételén is túl tudnak lépni. Németiék az általános relativitáselmélet eredményeit felhasználva konstruáltak egy olyan hipotetikus rendszert, amely a programozó, mint megfigyelő szempontjából nézve véges idő alatt képes végtelen sok számítást elvégezni. Mint többször hangsúlyozták az előadás alatt, a javaslatukról azt nem állítják, hogy megvalósító, de jelenleg ismert fizikai ismereteink szerint semmi nem zárja ki a megvalósíthatóságát.

Az alapötletük az, hogy a programozó egy számítógép felprogramozása után egy alkalmasan megválasztott pályán beleesik egy forgó fekete lyukba. "Kívülről" nézve a programozó az eseményhorizonton átesve "megfagy", órája végtelenül lelassul. "Belülről", a programozó szemszögéből viszont ennek a duálisa történik: a számítógép órája egyre gyorsul. Ennek eredményeképpen azalatt a (programozó számára) véges idő alatt, amíg átesik az eseményhorizonton, a számítógép számára végtelen idő telik el, ezért aztán bármilyen (nem korlátos) számítás eredményét megkaphatja. Ez azt jelenti, hogy pl. a ZFC konzisztenciáját megvizsgálhatjuk úgy, hogy az összes lehetséges (nyilván megszámlálhatóan végtelen számú) tételt egyenként vizsgáljuk, és az első inkonzisztencia megtalálásakor elindítunk egy űrhajót a programozó után. Ha a programozó nem találkozik az utánaküldött űrhajóssal azalatt a (számára véges!) idő alatt, amíg átesik az eseményhorizonton, akkor az azt jelenti, hogy a végtelen idő alatt (vagyis az összes lehetséges tétel vizsgálata során) nem találtunk ellentmondást, vagyis a ZFC konzisztens.

Nyilván az elmélet működéséhez egy csomó peremfeltételnek teljesülnie kell -- kezdve például azzal, hogy végtelen időre (és a számítás energiaigénye miatt végtelen anyagra) van szükség, vagyis ha a világegyetem jövője egy Nagy zutty jellegű összezuhanást tartogatna, akkor a módszer nem működne -- de a legújabb mérések azt mutatják, hogy a világegyetem folyamatosan tágul.

Mivel nem vagyok fizikus, a fenti, konyhanyelvű magyarázatban természetesen meg sem próbáltam kitérni azokra a problémákra, amiket például az jelent, hogy a programozó túlélje az utazást, vagy hogy az eredményekkel utánaküldött űrhajó ténylegesen utol is érje. Ezeket a részleteket természetesen tisztázza például ez a cikk.

A fenti leírás alapján talán nem egyértelmű, de mindenképp megemlítendő, hogy a programozó természetesen kijönni nem tud a fekete lyukból, a pl. a ZFC konzisztenciájáról szerzett ismereteit már csak a lyuk "túloldalán", egy másik univerzumban tudja felhasználni. Az előadók ennek kapcsán megemlítették annak a lehetőségét is, hogy egyfajta "Noé bárkája", akár maga a Föld haladjon át a (nyilván alkalmasan óriási) fekete lyukon, maguk mögött hagyva ebben az univerzumban egy gépet és annak kiszolgáló-civilizációját, a számítógépbe beprogramozva az összes, Turing-elven nem megoldható, érdekes problémát.

Ennyit az előadás tartalmáról -- de sajnos mindenképp mesélnem kell még a formájáról is. Az történt ugyanis, hogy egy óriási pofavizit lett az előadás: a fél IK tanári kar ott tobzódott, de csak hogy lássanak és látszódjanak -- az egyik végigpofázta az előadást a mellette ülőnek, a másik átlag ötpercenként dőlt a padra majdnem elaludva; az aktívabbak meg jöttek az olyan jellegű kérdésekkel, hogy "bár én nem értek a csillagászati részéhez, de...", amivel persze nincs is semmi baj, de utána ne kezdjen el még három visszakérdésben hitetlenkedni... Szerencsére az előadó nem volt szívbajos, a tényleg hülye kérdésre szemrebbenés nélkül vágta rá, hogy nem tud válaszolni, mivel a kérdés nem értelmes.

λ: A tiltott kalkulus

Az alábbi fényképet egy ELTE-s jegyzetbolt kifüggesztett árlistájáról készítettem:

Generikus programozás

A héten Rinus Plasmeijer tartott vendégelőadást a generikus programozásról funkcionális nyelvekben, bemutatva a Clean azon nyelvi elemeit, amivel explicit szupportálja ezt. Encsé a lelkemre kötötte, hogy blogjam meg, miről is van szó.

Kiinduló "Hello World"-ként tekintsük az alábbi Haskell kódot, benne két, strukturális rekurzióval definiált ekvivalenciavizsgálatot listákra és fákra:

Kellően messziről nézve a fenti két függvény láthatóan megegyezik. Az általános (mondhatnám, generikus) ötlet éppen az, hogy a strukturális rekurziót mint patternt nyelvi elemmé emeljük.

Programozás visszavezetéssel

Hát akkor nézzük, mivel is tervezek foglalkozni Fóthi Ákossal a hétfőn kezdődő félév során, progmatos nagyprogramom keretében.

Az alapötlet az, hogy gépi segítséggel bizonyítsunk programozási tételeket , visszavezetés segítségével, és az "ötleteket", az invenciózus lépéseket a felhasználó, ne pedig valamilyen hilbertiánus, féseggű MI-engine találja ki. Tehát a papírt-ceruzát váltanánk csak ki, a hibázás lehetőségét akarjuk csökkenteni és az eredmények menedzselhetőségét növelni.

A "Hello World" szintet például az jelenti majd, ha abból a tételből, hogy ismerjük tetszőleges f:ℤ→ℤ illetve β:ℤ→𝕃 függvények esetén az alábbi feladat (Hoare/Dijkstra/Fóthi értelemben) megoldását...

(egyrészt vegyük észre, hogy természetesen a feltételes maximumkeresésről van szó, másrészt gondolkodjunk el azon, milyen fun lehetett ezt egyenként, Unicode táblázatokat böngészve beírnom)

... be tudjuk látni, hogy akkor meg tudjuk oldani bármilyen, mondjuk g:ℤ→ℤ függvényre az egyszerű minimumkeresést is, vagyis az alábbi feladatot:

Erre egyébként van már annyi szanaszét heverő Lisp kódrészletem, amennyiből valószínűleg össze lehetne kalapálni valamit, ami ennyit már épp majdnem tudna is. Stay tuned.