deletions | additions       diff --git a/TODO.txt b/TODO.txt  index 888c83a..e64e681 100644  --- a/TODO.txt  +++ b/TODO.txt 
...
- Zalan cikket osszeszedni  - Csornyei cikk  - CSE12 missing  Macs: - selected papers  diff --git a/thesis/Makefile b/thesis/Makefile  index 610d8e5..74b5cd1 100644  --- a/thesis/Makefile  +++ b/thesis/Makefile 
...
.FORCE:  clean:  rm -f ./tezisfuzet_hu.log ./tezisfuzet_hu-blx.bib ./tezisfuzet_hu.blg ./tezisfuzet_hu.run.xml ./tezisfuzet_hu.bcf ./tezisfuzet_hu.bbl ./tezisfuzet_hu.aux $(addprefix tezisfuzet_hu,.log .bib .blg .run.xml .bcf .bbl .aux .fls .pdf .fdb_latexmk)  diff --git a/thesis/tezisfuzet_hu.tex b/thesis/tezisfuzet_hu.tex  index ccfff85..2b4b243 100644  --- a/thesis/tezisfuzet_hu.tex  +++ b/thesis/tezisfuzet_hu.tex 
...
% arara: biber  % arara: xelatex  % arara: xelatex  % vim: spell spelllang=hu :  \documentclass[a4paper,12pt]{article}  \usepackage{fontspec,lipsum}  \defaultfontfeatures{Scale=MatchLowercase,Ligatures=TeX} 
...
ö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.}  \cite{lncs13}  \cite{tfp2011} 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.  \printbibliography  \end{refsection} 
...
algoritmust az F\#{} nyelv fogalomrendszerén belül definiáltam.  }  \cite{icai2010_scope}  \cite{macs2010} 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.  \printbibliography