magyar \addbibresourcepubs.bib
1. Tézis: Készítettem egy kalkulust, mellyel függvények paraméterei és visszatérési értékének méretei közti összefüggéseket lehet leírni és ellenőrizni. Ezek az összefüggések lehetnek nem lineárisak és nem monotonok. A kalkulusban a méretek megadása méretkódolt típusok segítségével történik.afterindentfalseafterheading
Méretkódolt típusokat az algebrai adattípusokból kaphatjuk meg úgy, hogy az adatkonstruktort kibővítjük az elemek méretével. A legegyszerűbb ilyen típus az lista, amelynek klasszikusan két adatkonstruktora van: az üres lista (Nil) és a listába beszúrás (Cons), ez utóbbi egy elemből és egy listából készít egy új listát, amely elején található az új elem. Ha ezt a típust mérettel bővítjük akkor azt kapjuk, hogy az üres lista mérete 0, a Cons pedig a paraméterül kapott lista méreténél egyel nagyobbat hoz létre. Formálisan:
\(Cons::T->L_{n}(T)->L_{n+1}(T)\)
Amikor függvények típusát adjuk meg méretkódolt típusokkal, az egyszerű esetekben nagyon látványos eredményeket lehet elérni, ilyen például a lista megfordítása, amely a paraméterül kapott listával megegyező elemszámú listával tér vissza. Ilyenkor az okozza a nehézségeket, hogy ez az állítás semmit nem mond arról, hogy ha a lista elemei is listák, mit történik azoknak a méreteivel. Erre a klasszikus megoldás az altípusosság bevezetése, azaz azt mondjuk, hogy egy \(n\) elemű lista altípusa az \(n+1\) eleműnek. Ezáltal a listák listáját úgy kezelhetjük, hogy a legnagyobb elemszámú listát vesszük adjuk meg a lista elemtípusának: \(L_{n}(L_{m}(T))\), ahol a külső lista elemszáma legfeljebb \(n\), a belső lista elemszámának felső korlátja pedig \(m\). Sajnos ez a kézenfekvő megoldással a gyakorlatban előforduló függvények típusaiban szereplő méretekre csak elnagyol felső korlátot tud adni.
Munkámban \cite{lncs13,tfp2011} egy olyan kalkulust dolgoztam ki, amely lehetővé teszi azt, hogy a listában található listák elemszámát kifejezzük, így az altípusosság elhagyható, mégis a méretkódolt típusok tetszőleges mélységben egymásba ágyazhatóak. A megoldás lényege, hogy méretek kifejezésében lambda kalkulust használok, amely lehetővé teszi, hogy az indexek függvényében kifejezzük az elemszámot. A cikkben adok egy módszert arra, hogy egy ily módon típusozott függvényből egy SMT (Satisfiability Module Theory) problémát állítottam elő.
A probléma egy másik lehetséges megközelítése a függvények absztrakt interpretációja, amelyet szintén megvizsgáltam. A \cite{fopara_2011} cikkben a függvények absztrakt intepretációját vizsgálom intervallum aritmetikával, ezáltal az adatok méretére adok alsó és felső korlátot egy tisztán funkcionális nyelvre.
2. Tézis: Típuskikövetkeztetési algoritmust adtam arra az esetre, amiben a változók típusa a kikövetkeztetett típustól függhet. A megoldás a közismert Bottom–Up típuskikövetkeztető algoritmuson alapszik, és a típusegyenletek megoldásának késleltetésével lehetővé tehető a környezetfüggő egyenletek felírása. Az algoritmust az F# nyelv fogalomrendszerén belül definiáltam. afterindentfalseafterheading
A méretek intervallum aritmetikai vizsgálatát az F# nyelv egy tisztán funkcionális résznyelvén is vizsgáltam, azonban az absztrakt interpretációnak előfeltétele volt, hogy tetszőleges részkifejezések típusát ismerjük annak futtatása során. A bonyodalmakat az okozta, hogy az F# nyelvben lévő rekord adattípusok (osztályok) mezőihez a funkcionális nyelvek a rekordok mezőihez elérőfüggvényeket rendelnek, azonban, ha két rekord azonos nevű mezőt tartalmaz, az elérőfüggvények neve is meg fog egyezni, ez viszont a klasszikus Hindley–Milner típusrendszerben nem megengedett, ott a kikövetkeztetés megkezdésekor a szimbólumok típusait egyértelműen ismernünk kell. A helyzetet tovább bonyolították az F# nyelv rendkívül bonyolult láthatósági szabályai, amelyek ráadásul függenek a már kikövetkeztetett típusoktól is.
A megoldás keresésében az első lépcső \cite{icai2010_scope} az volt, hogy a kikövetkeztetést és a névfeloldást szét kellett választani. Ehhez közismert Bottom–Up típuskikövetkeztetési algoritmusnak kihasználtam azt a tulajdonáság, hogy az algoritmus két menetben dolgozik: első menetben típusegyenleteket ír fel a, a második menetben pedig ezeket megoldja. A második menetben az egyenletek megoldásának sorrendje nem teljesen kötött, így a nem egyértelmű típusok egyenletének a felírását elhalaszthatjuk. Amikor a már megoldható típusegyenletek elfogytak, elindítunk egy névfeloldást, ami a már rendelkezésre álló típusok alapján próbálja a névfeloldást elvégezni, a sikeresen feloldott nevekkel bővítve a típusegyenlet-rendszert. Ily módon a típuskikövetkeztetési és névfeloldási lépések egymás utáni ismétlésével a feladat szétbontható.
A fenti algoritmus használatával definiáltam \cite{macs2010} az F# nyelv egy tisztán funkcionális G\(\flat\) résznyelvét.
3. Tézis: Beágyazott doménspecifikus nyelvet (EDSL) definiáltam Haskell nyelven, méretkifejezések és redukciós szabályokat adtam meg en[nek egyszerűsítésére. A beágyazás tagless, így a neki megfelelő Haskell kódra minimális járulékos futási idejű költséggel fordítási időben átalakul. afterindentfalseafterheading
\cite{studia14}