Programmeerimises on andmete esitamise viis sama tähtis kui nendel opereerivate algoritmide esitus. Eri programeerimiskeeled realiseerivad erinevaid andmetüübisüsteeme ja eri abstraktsioonitasemetel. Paljud andmetüübid evivad mingit liiki sisemist sümmeetriat. Võtame näites ringpuhvrid, mida sageli esitatakse väärtuste listina ja pointeritega sellesse. Algoritm, mis ringpuhvriga töötavad, ei tohiks olla liiga tundlik andmete täpse paigutuse suhtes sellises listis. Algoritmi vastus ei peaks muutuma, kui väärtusi listis roteerida.
Selles doktoritöös uurime fundamentaalsel tasemel sümmeetriatega andmetüüpide esitamise eri viise. Tavaliselt modelleeritakse sümmeetriaid faktorhulga kaudu relatsiooni suhtes, mis väljendab, et kaks konkreetset väärtuste paigutust esitavad samu andmeid. Niisugune esitusviis kipub vajama teatud suvalisi otsustusi ning seda eriti potentsiaalselt tõkestamata suurusega andmestruktuuride puhul. Me kasutame homotoopilises tüübiteoorias. See teooria põimib ideid homotoopiateooriast (mis uurib geomeetrilisi ruume ja nende sümmeetriaid) ja sõltuvast tüübiteooriast (mis on suure äljendusvõimsusega deduktiivne süsteem). Selle teooria vahenditega saab teatud suvalise otsustamise kohad ära hoida.
Me esitame andmetüüpe nn konteineritena ja tõlgime tavapärase faktorhulkadel põhineva andmete esituse selliseks, kus sümmeetriad muutuvad andmete osaks. Tulemusena saame samaväärsed väärtuste paigutused formaalselt võrdseks lugeda. Paljude küsimuste jaoks kaob elle lähenemise juures erinevus sümmeetriatega andmetüüpide ja sümmeetriateta andmetüüpide vahel täiesti: sümmeetrilisel juhul saame rakendada samu konstruktsioone ja tõestusi, mida mittesümmeetrilisel juhul. Me näitame, et rida olulisi standardseid konstruktsioone andmetüüpidel on meie raamistikus adekvaatselt teostatavad, nt. püsipunkti leidmine puukujuliste andmetüüpide konstrueerimiseks ja tuletise operatsioon, mis on oluline puid läbikäivate algoritmide juures. Osa sellest tööst peaks olema rakendatav programmeerimiskeelte loomiseks, kus sümmeetriatega andmetüüpe saab esitada natiivselt.

Doktoritöö on avaldatud Tehnikaülikooli raamatukogu digikogus

Juhendaja nooremprofessor Niccoló Veltri (TalTech)

Oponendid:

• Dr. Vikraman Choudhury (Strathclyde´i Ülikool, Suurbritannia)
• professor Nicolai Kraus (Nottinghami Ülikool, Suurbritannia)

Jälgi avalikku kaitsmist Zoomis

Meeting ID: 947 2192 6111
Passcode: 37439