deletions | additions       diff --git a/Munk_m_sor_n_els__.tex b/Munk_m_sor_n_els__.tex  new file mode 100644  index 0000000..39645e1  --- /dev/null  +++ b/Munk_m_sor_n_els__.tex 
...
Munkám során elsősorban funkcionális nyelvek elemzésével foglalkoztam.  Funkcionális nyelvek alatt azokat a programozási nyelveket nevezzük, amelyek támogatják a funkcionális programozási paradigmát. Ez egy olyan deklaratív programozási stílus, amelyben eljárások helyett mellékhatásmentes függvényeket adunk meg, és olyan adatszerkezeteket használunk, amelyek nem módosíthatóak. Az ilyen nyelvekben a függvények első rendű elemként jelennek meg, és jellemző a magasabb rendű függvények használata, valamint a fejlett típusrendszer is.   A funkcionális nyelvek között kiemelkedő helyet foglalnak el a tisztán funkcionális nyelvek. Ezek a nyelvek nem támogatnak mellékhatásokat, és teljesül rájuk a hivatkozási helyfüggetlenség. Ez azt jelenti, hogy ha egy függvényt kétszer meghívok ugyanazzal a paraméterezéssel, az eredmény ugyanaz lesz. Ezeken a nyelvek nem támogatnak változókat és állapotokat, valamint a mellékhatásokat (fájlrendszer használat, képernyőkezelés) is közvetett módon oldják meg. Egy ilyen elterjedt megoldás a monádok használata (pl. Haskell), ahol a monádok ábrázolják a külső vagy belső állapottal végezhető műveleteket, és a programunkat ezeknek a műveleteknek a segítségével építhetjük fel anélkül, hogy a hivatkozási helyfüggetlenség sérülne.  A tisztán funkcionális nyelvek az egyszerű és tiszta elméleti alapok miatt jól tárgyalhatóak, ennek egyik bizonyítéka, hogy a típusrendszerek legnagyobb eredményei is ezekhez a nyelvekhez köthetőek. A tisztán funkcionális nyelvek a legtöbb esetben erősen típusosak, azaz ellenőrzi, hogy a függvényeket megfelelő típusú paraméterekkel hívtuk-e meg. Sőt, a legtöbb tisztán funkcionális nyelve úgy képes a programok típushelyességét ellenőrizni, hogy a programozónak a függvények típusait nem is kell megadnia, hanem a fordítás része a típuskikövetkeztetés (Hindley--Milner típusrendszer). Ezeknek a nyelveknek egy másik gyakori jellemzője, hogy megenged olyan típusokat, amelyek egy típusparamétertől függnek (ún. polimorf típusok). Ezt a rendszert System F-nek (vagy $\lambda_2$-nek) nevezzük.  Ha a típusrendszerben megengedjük azt is, hogy a típusaink ne csak típusparaméterektől, hanem kifejezésektől is függjenek, eljutunk a függő típusokig (). Ennek egy speciális esete a méretkódolt típusok (sized types), ahol a típusaink nemnegatív egész kifejezésektől függnek, amelyek az adott típusú argumentum méretét (pl. lista esetében a hosszát) tárolják. Egy másik lehetséges bővítés az, hogy típusparaméternek nem csak típusokat, hanem tetszőleges polimorf típusokat is megengedünk (System $F_\omega$, vagy $\lambda_\omega$). Ezekben a nyelvekben a típuskikövetkeztetés azonban már eldönthetetlen probléma.  A típusrendszerek fontosságára mutat rá a Curry-Howard izomorfizmus, amely azt mondja ki, hogy a függvények típusai és a függvények törzse a matematikai logika állításainak és bizonyításainak feleltethetőek meg. Ez arra használható, hogy a függvény típusába bele tudjuk kódolni a függvény bizonyos tulajdonságait is, amennyiben a típusrendszerünk elegendő kifejezőerővel bír. A fenti általánosításokra épül a Coq nyelv típusrendszere (Calculus of (Inductive) Constructions) illetve hasonló kifejezőerővel bír az Agda nyelv is, amely Martin-Löf--féle konstruktív típusrendszert használja, amely kifejezőereje megegyezik a konstruktív logikával.  A fenti példa azt mutatja, hogy tetszőleges programtulajdonság vizsgálható és bizonyítható megfelelő típusrendszerrel. A programok statikus elemzésére egy másik módszer a programok absztrakt interpretációja. Ebben a módszerben a program viselkedését közelítjük úgy, hogy tulajdonképpen egy absztrakt állapottéren futtatjuk le. Ezt a megoldás gyakran használják fordítóprogramok a programok elemzésére (a control-flow és data-flow elemzés mellett).  A fejlett típusrendszerek lehetővé teszik, hogy egy gazda nyelv segítségével megfogalmazzunk egy olyan programozási nyelvet, amelyet a gazdanyelv eszközeivel írunk le és a gazda nyelv típusrendszere ellenőriz.  diff --git a/abstract.tex b/abstract.tex  deleted file mode 100644  index f83e66f..0000000  --- a/abstract.tex  +++ /dev/null 
...
No Abstract Found  diff --git a/layout.md b/layout.md  index 45233b4..f7d6f9d 100644  --- a/layout.md  +++ b/layout.md 
...
abstract.tex  .tex  intro.tex  test__.tex  modszerek.tex  Munk_m_sor_n_els__.tex  tezisek.tex  diff --git a/test__.tex b/test__.tex  deleted file mode 100644  index ac92781..0000000  --- a/test__.tex  +++ /dev/null 
...
test it  diff --git a/tezisek.tex b/tezisek.tex  index a489c6e..8ec771d 100644  --- a/tezisek.tex  +++ b/tezisek.tex 
...
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 
...
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ó. 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.