Ez a tárgy a típusrendszerek elméletével, azaz a típuselmélettel foglalkozik. Ez a tématerület a számítástudomány jelenleg is intenzíven fejlődő területe, mivel a típusrendszerek komoly szerepet játszanak a szoftverfejlesztésben, a programok írásában és fordításában, valamint az utóbbi időben pedig rendkívül nagy szerepet kaptak a programnyelvek tervezésében.

Irodalom

A tárgy elsajátításához az alábbi könyvek javasoltak, segítségükkel az előadáson szereplő témák részletesebben ezekben tanulmányozhatóak.

  • Csörnyei Z. Lambda-kalkulus: A funkcionális programozás alapjai. Typotex Elektronikus Kiadó, 2007, ISBN 978-963-9664-46-3.

  • Csörnyei Z. Bevezetés a típusrendszerek elméletébe. ELTE Eötvös Kiadó, 2012, ISBN 978-963-312-134-4.

Ajánlott irodalom

Ezek a könyvek segíthetnek még a fentebb említett könyveket kívül az egyes anyagrészek alaposabb megértésében.

  • B. C. Pierce. Types and Programming Languages. MIT Press, 2002.

  • B. C. Pierce. (szerk.) Advanced Topics in Types and Programming Languages. MIT Press, 2005.

  • R. Harper. Practical Foundations for Programming Languages. Cambridge University Press, 2012. (online)

Órai jegyzet (2015/2016 ősz)

  1. előadás: Bevezetés, λ-kalkulus (szintaktika, szemantika), formális matematikai rendszer
  2. előadás: Formális típusrendszerek, F1 típusrendszer (szintaktika, szemantika)
  3. előadás: Kibővített alaptípusú F1 típusrendszer, típusok induktív definíciója (példák (Agda))
  4. előadás: Típusok induktív defincíója (F1), F1 <  : : altípusok, a Curry-típusrendszer szintaktikája (példák (Agda))
  5. előadás: Curry-típusrendszer, típuskikövetkeztetés a Curry-típusrendszerben
  6. előadás: let-polimorfizmus, Hindley-Milner-típuskikövetkeztetés, hagyományos és szintaktika-vezérelt Hindley-Milner-típusrendszer, W-algoritmus
  7. előadás: J-algoritmus, M-algoritmus, rekurzió, polimorfikus rekurzió, Milner-Mycroft-típusrendszer
  8. előadás: Az F2 típusrendszer: szintaktika, operációs szemantika, típusok
  9. előadás: Az F2 típusrendszer: típusok (folytatás), rekurzív függvények, az F2 <  :  típusrendszer (szintaktika, típusok ekivalenciája, tulajdonságok), típusok
  10. előadás: Az F2∃ típusrendszer (szintaktika, tulajdonságok, alkalmazása), magasabbrendű típusrendszerek, az Fω típusrendszer, az Fω <  : , ∃ típusrendszer
  11. előadás: A λP típusrendszer (szintaktika, szemantika), függő típusok és azok alkalmazása: a Vec és Fin induktív típuscsaládok, a típusrendszerek egységes leírása (példák (Agda))
  12. előadás: A típusrendszerek egységes leírása, a λ-kocka, Curry-Howard-izomorfizmus, az intuicionista, konstruktív logika (példák (Agda))

Követelmények

A tárgy kollokvium, amelyhez írásbeli vizsga tartozik, ahol a következő témakörökben szerepelhetnek kérdések, feladatok:

  1. Az F1 típusrendszer. Szintaktika, szemantika, tulajdonságok. Következtetések helyességének ellenőrzése. (A következtetési szabályok segédlapon elérhetőek lesznek.)

  2. Az F1 kibővített alaptípusai, típus induktív definíciója. Unit, Bool, Nat, Pair, List, Record, Variant. Induktív típusdefiníciók.

  3. Az F1 <  :  típusrendszer. Altípus, szintaktika, szemantika, tulajdonságok. Következtetések helyességének ellenőrzése. (A következtetési szabályok segédlapon elérhetőek lesznek.) Kontravariáns típus, biztonságos helyettesítés elve, típus gyengítése.

  4. A Curry-típusrendszer. Szintaktika, szemantika, tulajdonságok. Következtetések helyességének ellenőrzése. (A következtetési szabályok segédlapon elérhetőek lesznek.)

  5. Típuskikövetkeztetés a Curry-típusrendszerben. Helyettesítések, egységesítő helyettesítés, principális típus. (A korlátozások generálása és az egységesítés algoritmusa segédlapon elérhetőek lesznek.)

  6. A Hindley-Milner-típusrendszer. let-polimorfizmus, W-, J- és M-algoritmusok, polimorfikus rekurzió (Milner-Mycroft-típusrendszer). (Az algoritmusok leírása egy segédlapon elérhető lesz.)

  7. Az F2 típusrendszer. Szintaktika, szemantika, tulajdonságok. Típusok: Unit, Bool, Nat, Pair, List, rekurzív függvények. Egzisztenciális típusok, az F2∃ típusrendszer szintaktikája és tulajdonságai.

  8. Magasabbrendű típusrendszerek. Az Fω típusrendszer szintaktikája és szemantikája, tulajdonságok, fajták. Az Fω <  :  típusrendszer szintaktikája és szemantikája, tulajdonságai.

  9. A λP típusrendszer. Szintaktika, szemantika. Függő típusok, függő típusos függvények, a Vec és Fin induktív típuscsaládok.

A vizsgázás előfeltételeként a félév során teljesíteni kell három beadandó feladatot. Ezek az előadáson tárgyalt témákhoz kapcsolódó, önállóan megoldandó programozási feladatokat jelentenek, amelyekhez az oktatók segítségét is igénybe lehet venni elektronikus levél írásával vagy a konzultációs alkalmakon. A feladatokat és az értékelésüket a BE-AD rendszerben lehet elérni, a tárgyhoz tartozó csoportba történő sikeres feliratkozást követően. A BE-AD szerverre a kari, INF-es (Pandorás) azonosítóval és jelszóval lehet belépni, oda külön regisztrálni már nem kell. A beadandókat a félév során folyamatosan, a félév végéig lehet beadni, illetve a beadott megoldásokat a visszajelzések mentén javítani.

A beadandókban szereplő témakörökhöz tartoznak a félév során zárthelyi dolgozatok is, amelyek kapcsolódó elméleti kérdéseket és gyakorlati feladatokat tartalmaznak. Ezekből együtt számtani átlagban legalább 50%-os eredményt kell elérni a vizsgázáshoz. Az itt kiemelkedő eredményt elérő hallgatók jeles érdemjegyet szerezhetnek, külön vizsgázás nélkül.

Amennyiben valaki, nagyon indokolt esetben, nem tud részt venni valamelyik zárthelyin, az az előadónál Neptun-kóddal, elektronikusan, előre jelezve feljelentkezhet a pótlás időpontjára. Az ez időpont egyben arra is lehetőséget ad, hogy akinek a félév során nem sikerült elérnie a kívánt teljesítményt, a rosszul sikerült dolgozatokat javíthatja. (Csak javítani lehet.)

Vizsgaidőpontok

A vizsgák elérhetőek a Neptun rendszerben.

A félév ütemezése

Zárthelyi dolgozatok pótlása:

  •  2016. május 13. (péntek), 13:00 — 14:00 (első zárthelyi), D-1.820 (Hajós György)
  •  2016. május 13. (péntek), 14:00 — 15:00 (második zárthelyi), D-1.820 (Hajós György)
  •  2016. május 13. (péntek), 15:00 — 16:00 (harmadik zárthelyi), D-1.820 (Hajós György)

Tömbösített előadások

A vizsgakurzus részeként a szorgalmi időszak utolsó két hetében Kaposi Ambrus tömbösítve megtartja az előző féléves előadásokat. Ezeken a részvétel nem kötelező, csupán ajánlott, mivel ennek célja, hogy segítse a felkészülést a vizsgára. Természetesen ez egyúttal konzultációra is lehetőséget nyújt az érintett témakörökben.

Ezen előadások időpontjai és helyei az alábbiak:

  •  2016.05.02. (hétfő), 18:00 — 20:00, D-0.220 (Kárteszi Ferenc)
  •  2016.05.03. (kedd), 18:00 — 20:00, D-0.220 (Kárteszi Ferenc)
  •  2016.05.04. (szerda), 18:00 — 20:00, D-0.818 (Soó Rezső)
  •  2016.05.05. (csütörtök), 19:00 — 21:00, D-0.311 (Kőnig)
  •  2016.05.06. (péntek), 18:00 — 20:00, D-0.311 (Kőnig)
  •  2016.05.09. (hétfő), 18:00 — 20:00, D-0.220 (Kárteszi Ferenc)
  •  2016.05.10. (kedd), 18:00 — 20:00, D-0.220 (Kárteszi Ferenc)
  •  2016.05.12. (csütörtök), 18:00 — 20:00, D-0.311 (Kőnig)
  •  2016.05.13. (péntek), 18:00 — 20:00, D-0.311 (Kőnig)

Konzultáció

A vizsgakurzushoz a második héttel kezdődően tartozik tanrendbe beosztott konzultációs lehetőség is. Ezek csütörtökönként 17 és 18 óra között, a D-2.108 (PC5) teremben lesznek megtartva. A gyakorlati számonkérés szervezéséért felelős oktatók természetesen szükség esetén elektronikus levélben is megkereshetőek:

Vissza az oktatói honlapra

Utolsó módosítás: 2016.05.09.