Ami a geometriának a topológia, az a topológiának a ... ?

Ami a síkidomnak az alakja, az az alaknak a… Értelmetlen kérdés…

Ami a törtnek a nevezője, az a nevezőnek a… Értelmetlen kérdés…

Ami a kéznek az ujja, az az ujjnak a… Értelmetlen kérdés…

Ami az egérnek a gombja, az az egérgombnak a… Értelmetlen kérdés…

Ami az autónak a kereke, az a keréknek a… Értelmetlen kérdés…

> Amit #2-esben írsz, azokat mind meg lehetne viszonylag logikusan magyarázni.

Nem kell magyarázni. Nincs mit magyarázni. Erőltetett módon ki lehetne találni rá valamiféle akár még helyesnek is tűnő választ valamilyen analógián keresztül, de nem tartunk számon ilyen analógiákat. Nem véletlenül. Ahogy egy tanárunk mondta a maga sajátosan ködös megfogalmazásában: „Lila ló nincs. Persze van, ha befested a lovadat lilára. De menj ki vele az utcára, ki fognak röhögni.”

De hajrá. Ha van kedved, válaszolhatsz a #2-es kérdésekre. Attól még értelme nem sok lesz.

Nagyon jó a kérdés.

Kategóriaelmélet! A kategóriaelmélet az algebrai topológia igényeiből született meg eredetileg valamikor 1945 körüli években. Ez azért érdekes, mert a kategóriaelmélet eaztán olyan általánosításokra adott lehetőséget, hogy ma a kategóriaelmélet (a különféle típuselméletekkel együtt) a matematika megalapozásának az egyik színtere.

Funkcionális porgramnyelveknél, és tételbizonyító rendszereknél szemantikai kérdésekben is jelen van mind a kategóriaelmélet, mind pedig maga a topológia is.

FOLYTATÁS

Mi hétköznapi emberek a kategóriaelmélettel akkor talákozunk többnyire, ha pl. programozási feladatok miatt valami deklaratívabb, funkcionális programnyelvet tanulunk. Algebrai adattípusok, típusosztályok, monászok, indexelt típusok... Ezek jelen vannak pl. a Haskell nyelvben is, de a monászok törvényeit már nem kényszeríti ki ez a nyelv -- ezt a hagyományos nyelvekhez hasonlóan a programozó tartalmi tapasztalatára bízza. Indexelt típusok, pláne értékfüggő típusok pedig már csak a nyelvi kiegészítések részeként érhetőek el a Haskellben általában bizonyos korlátok között.

Mindenesetre épp ez a mezsgye, ahol a programozás ,ár átlép valami többe, és akát tátelbizonyító rendszer irámnyába is továbbfejlődhetik.

Aki haskell programozóként akar továbbhaladni, és biztonságkritkus rendszerek fejlesztése okán különlegesesn magas megbízhatósági szintő programokat akar fejleszteni, sokszor belevág efféle, a nyelv lehetőségei határán billegő vagy azt akár meghaladó paradigmák tanulásába. Ilyenkor kerülhet kapcsolatba tételbizonító rendszerekkel (Coq, Agda, Idris). Ezekben már olyan összefoggések is közvetlenül megfogalmazhatóak, amelyek a programozó lehetőségeit nagyban kibővítik - vagy látszólag épp ellenkezőleg: leszűkítéseket, korlátozásokat fogalmaznak bele a programba, ezáltal a hibalehetőségeket leszűkítik le, akár elvileg teljesen ki is küszöbölhetik azokat.

Közvetlenül Agda-ban, Coq-ban, Idrisben programozni jó élmény, és termékeny is lehet, de a lehetőségekkel a tudás- és tanulásigény is megnő. Ezeknek a nyelveknek az alapjainak, lényegi paradigmáinak mélyebb megértésében már segíthet olyan témák tanulása is, mint a kategóriaelmélet és a típuselmélet.

A kategóriaelmélet és a típuselmélet ugyan egész különöző indítékok és ,,történetből'' fejlődött ki, és sokban lényegesen különböznek is egymástól, azonban a matematika megalapozásának, illetve a modern deklarativ programozás, illetve a tételbizonyító rendszerek megértésében mindekettőnek szerepe van.

Ami az érdekes mindez uztán a kis bevezető után: a kategóriaelméletet NEM programözók vagy valami filozófusok vagy logicisták hozták létre, hanem eredetileg az algebrai topológiából nőtt ki. A topológiának már a II. világháború utáni években volt egy olyan igénye, hogy egyes tételekből átlatlánosabb összefüggéseket lehessen kiemelni, és ennek mefgogalmazására született meg a kategóriaelmélet.

Ebből a szempontból jól megfogtad a lényeget: a kategóriaelmélet valóban hasonló szerepet töltött be a topológia történetében, mint ahogy a geometriához maga a topológia viszonyul. De a történet persze bonyolult, sőt, ezeket a részleteket nem is ismerem, csak annyit, mint amit korábban írtam: én a programozás miatt botlottam be a területbe, de eredeti indítéka, kialakulása szerint a topológiából fejődött ki.