Kaposi Ambrus típuselméleti kutatása 1,9 millió eurós, azaz mintegy 781 millió forintnak megfelelő támogatást nyert az Európai Kutatási Tanács (European Research Council – ERC) Consolidator Grant pályázatán – közölte kedden az ELTE.
A kutató 2024-ben Magyarországról egyedüliként részesült az ERC pályázati támogatásában.
A kutatás kategóriájában (Élettelen természettudományok és műszaki tudományok) 928 benyújtott pályázat közül került a kiválasztott 131 közé.
Az ERC a Horizon Europe keretprogramban a felfedező kutatásoktól a hasznosítás kezdeti fázisáig díjazza a legígéretesebb kutatásokat. A Consolidator Grant pályázaton a már kutatócsoporttal és kiemelkedő eredményekkel rendelkező, tudományos áttörés ígéretét hordozó kutatásokat ismerik el. Kaposi Ambrus és csapata a Magasabb megfigyelés-alapú típuselmélet (Higher Observational Type Theory – HOTT) című kutatásával a számítógépes bizonyítórendszerek használatát forradalmasíthatja – emelték ki.
Ebből áll a kutatás háttere
Az MTI-vel közölt tájékoztatás szerint a számítógépes bizonyítórendszerek a típuselméletre (type theory) épülnek. A típuselmélet mind a matematikusok, mind pedig az informatikusok bizonyítási és helyességellenőrzési problémáira megoldást kínál, olyan formális nyelvi eszközt adva a kezükbe, amellyel egyszerre lehet programokat és matematikai bizonyításokat írni.
Egy program típusa maga az állítás, a típusnak megfelelő program pedig az állítás bizonyítása
– magyarázták.
A típuselmélet magasabb-dimenziós modelljeiben a típusok elemeit absztrakt terek pontjaival, az egyenlőség típust pedig a pontok közötti utakkal adják meg. Ilyen modellekre építve fejlesztették ki a homotópia-típuselméletet (homotopy type theory), amelyben teljesül az izomorf típusok egyenlőségének elve. Ezzel az elvvel a számítógépes bizonyítás közel kerül a mindennapos matematikusi gyakorlathoz, ahol az izomorf struktúrákat azonosnak tekintik – fejtették ki.
Milyen hozadéka lehet ennek?
A közlemény szerint 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ég típus nem geometriai módon, hanem számítással van megadva. A megoldás elmagyarázhatóvá teszi a homotópia-típuselméletet, és rövidíti a bizonyításokat, 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
azáltal, hogy lehetővé teszi az absztrakt, újra felhasználható bizonyítások készítését.
Kövesse az Economx.hu-t!
Értesüljön időben a legfontosabb gazdasági és pénzügyi hírekről! Kövessen minket Facebookon, Instagramon vagy iratkozzon fel Google News és YouTube-csatornánkra!
Gazdasági hírek azonnal, egy érintéssel
Töltse le az Economx app-ot, hogy mindig időben értesülhessen a gazdasági és pénzügyi világ eseményeiről!
Kérjen értesítést a legfontosabb hírekről!