Új változatot kap a homotópia-típuselmélet
Kaposi Ambrus (Kép: ELTE)Az ELTE kutatójának, Kaposi Ambrusnak és csapatának Higher Observational Type Theory (HOTT – Magasabb megfigyelésalapú típuselmélet) című kutatása a számítógépes bizonyítórendszerek használatát forradalmasíthatja. A számítógépes bizonyítórendszerek arra a típuselméletre épülnek, amely a matematikusok és az informatikusok bizonyítási és helyesség-ellenőrzési problémáira kínál megoldást, miután olyan formális nyelvi eszközt ad a kezünkbe, amelyben egyszerre lehet programokat és matematikai bizonyításokat írni.
A HOTT-projekt célja a homotópia-típuselmélet egy új változatának kidolgozása, amelyben a magasabb dimenziós geometria nem kézzel van beépítve, hanem emergens. Az alapötlet, hogy az egyenlőségtípus nem geometriai módon, hanem számítással van megadva. Ez a megoldás a homotópia-típuselméletet elmagyarázhatóvá teszi, és a bizonyításokat rövidíti, hiszen a bizonyítások egyes részei automatikus számításokká válnak. Az új típuselmélet hosszú távon hozzá fog járulni a matematikai bizonyítások számítógépes ellenőrzésének és a szoftverek helyességbizonyításának fejlődéséhez azzal, hogy lehetővé teszi az absztrakt, újra felhasználható bizonyítások készítését.•
Címlapkép: ELTE
