Csörnyei Zoltán
Pi-kalkulus
a mobil rendszerek elmélete
TARTALOM, ELŐSZÓTartalom
ELŐSZÓ
1. BEVEZETÉS
2. A PI-KALKULUS
2.1. Folyamatkalkulusok
2.2. Címkézett átmeneti rendszerek
2.3. Szintaxis
2.3.1. Szabad és kötött nevek
2.3.2. Helyettesítés
2.3.3. Az α-konverzió
2.3.4. Szerkezeti kongruencia
2.4. Műveleti szemantika
2.4.1. A szemantikát leíró szabályok
2.4.2. A műveleti szemantika szabályai
2.4.3. A kötött output prefix
2.5. Konstansok és függvények
2.5.1. Poliadikus pi-kalkulus
2.5.2. Folyamatkifejezés absztrakciója
2.5.3. Logikai konstansok
2.5.4. Megszűnő és ismétlődő folyamatkifejezések
2.5.5. Természetes számok
2.5.6. Rekurzió és replikáció
2.5.7. Lista
2.5.8. Lambda-kalkulus
2.6. Biszimuláció
2.6.1. Nyomkövetésen alapuló ekvivalencia
2.6.2. Biszimuláció és kongruencia
2.6.3. Korai szemantika és korai biszimuláció
2.6.4. Nyilazott biszimuláció
2.6.5. Nyitott biszimuláció
2.6.6. Gyenge biszimuláció
3. A PI-KALKULUS ALGEBRAI ELMÉLETE
3.1. A kölcsönös hasonlóság axiómarendszere
3.2. A kongruencia axiómarendszere
4. SPECIÁLIS PI-KALKULUSOK
4.1. Az aszinkron pi-kalkulus
4.1.1. Szintaxis és műveleti szemantika
4.1.2. Biszimuláció
4.2. A lokalizált pi-kalkulus
4.2.1. Szintaktika, műveleti szemantika, biszimuláció
4.2.2. A késleltetett input
4.2.3. A lokalizált pi-kalkulus és a lambda-kalkulus
4.3. A lineáris továbbító pi-kalkulus
4.3.1. Az Lƒπ-gép
4.4. A fúzió-kalkulus
4.4.1. Szintaktika és műveleti szemantika
4.4.2. Biszimuláció
4.4.3. A fúzió-kalkulus és a lambda-kalkulus
4.5. A belső mobilitás kalkulusa
4.5.1. Szintaktika és műveleti szemantika
4.5.2. Biszimuláció
5. TÍPUSOS PI-KALKULUSOK
5.1. Formális típusrendszerek
5.2. Az Fπ0 típusrendszer
5.2.1. A típusrendszer szintaxisa
5.2.2. Következtetések és típusszabályok
5.2.3. Műveleti szemantika
5.2.4. Az Fπ0 típusrendszer tulajdonságai
5.3. Az Fπ típusrendszer
5.3.1. Az alaptípus-halmaz bővítése
5.4. A lineáris típusrendszer
5.4.1. Szintaxis és műveleti szemantika
5.4.2. Típusszabályok
5.4.3. A Linπ típusrendszer tulajdonságai
6. A MAGASABB RENDŰ PI-KALKULUS
6.1. A HOπ-kalkulus szintaxisa és műveleti szemantikája
6.2. A HOπ-kalkulus és a pi-kalkulus kapcsolata
Irodalomjegyzék
Tárgymutató
Előszó
Ez a könyv egy oktatási segédlet, az Eötvös Loránd Tudományegyetem Eötvös József Collegiumában tartott Mobil rendszerek elmélete tantárgy anyagát tartalmazza.
A könyvben leírtak megértéséhez különösebb előismeret nem szükséges, de mivel a leírt rendszer sok jellemzője, felépítése, működése nagyon hasonlít a lambda-kalkulus és a típusos lambda-kalkulus tulajdonságaihoz, a lambda-kalkulus ismerete megkönnyítheti az anyag elsajátítását. A lambda-kalkulust a Collegium elsőéves informatikus hallgatóinak, ezt az anyagot, a mobil rendszerek elméletét a másodéves collegistáknak ajánljuk.
A mobil rendszereket, az 1950 környékén végzett kezdeti kísérletektől eltekintve, az 1990-es évek elején kezdték el alaposabban vizsgálni, ennek oka a párhuzamos és disztributív programozás hardver és szoftver feltételeinek ugrásszerű javulása volt. Az elmélet jelenleg is intenzíven fejlődik, szakfolyóiratokban újabb és újabb eredmények jelennek meg. Könyvünkben az elmélet már állandósult, kidolgozott területeiről igyekszünk egy átfogó képet adni.
Elsősorban az elvekre, módszerekre, a kapcsolatokra koncentrálunk, a tételek bizonyításával nem foglalkozunk, ezek a könyv végén, az Irodalomjegyzékben megadott anyagokban megtalálhatók.
Az Irodalomjegyzékben a témához kapcsolódó felhasznált publikációk adatai vannak, amelyek az elmélet további tanulmányozásához is segítséget nyújtanak.
Könyvünkkel azt szeretnénk elérni, hogy az informatikus egyetemi hallgatók és az informatikus szakemberek megismerjék ezt az új kutatási területet, a mobil rendszerek elméletét.
...
Budapest, 2017. január 31.
Csörnyei Zoltán