deletions | additions       diff --git a/tezisek.tex b/tezisek.tex  deleted file mode 100644  index 8ec771d..0000000  --- a/tezisek.tex  +++ /dev/null 
...
\section{Tézisek}  \begin{refsection}  \thesis{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.}  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.  Más módszerek lehetnek pontosabbak, ezek általában valami szúk függvényosztályon   belül képesek csak a méretkorlátok megállapítására (ilyen jellemző függvényosztály   például a monoton vagy a lineáris függvények). Az általam adott megoldásban azonban   a függvények tetszőleges polinomok lehetnek.  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.  \printbibliography  \end{refsection}  \begin{refsection}  \thesis{  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.  }  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 iteratívan megoldható.  A fenti algoritmus használatával definiáltam~\cite{macs2010} az F\#{} nyelv egy  tisztán funkcionális G$\flat$ résznyelvét.  \printbibliography  \end{refsection}  \begin{refsection}  \thesis{  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.  }  \cite{studia14}  \printbibliography  \end{refsection}