13. fejezet - Szekvenciális megfelelő

Egy feladat megoldása során sokszor szembesülünk azzal a problémával, hogy különböző típusértékhalmazokba eső értékek közötti kapcsolatot kell leírnunk, vagy ilyen értékeket kell összehasonlítanunk. Erre leggyakrabban akkor kerül sor, ha valamilyen állapottértranszformációt végzünk, és meg kell adnunk az eredeti és az absztrakt tér közötti kapcsolatot. Az ilyen megfeleltetések formális megadása általában elég nehézkes. A szekvenciális megfelelő fogalmának felhasználásával azonban ezek a kapcsolatok is egyszerűbben írhatók fel.

Legyenek elemi típusok (egy típus akkor elemi, ha önmagával van reprezentálva, azaz a hozzátartozó reprezentációs függvény az identikus leképezés). Az elemi értékek halmaza legyen

Tegyük fel hogy a típus reprezentációs függvényére igazak az alábbi megszorítások:

Legyen továbbá az úgynevezett bázishalmaz, ahol tetszőleges típusértékhalmaz, és jelölje az elemi típusok halmazát . Ekkor a elem bázisra vonatkoztatott szekvenciális megfelelője:

ahol

A jelölés egyszerűsítése végett, ha a bázis egyelemű, akkor a bázishalmaz helyett az elem is írható, azaz esetén

Tekintsük a következő példát:

Legyen , . Ekkor

a sorozatbeli rekordok névrészeinek sorozata ( )

a sorozatbeli rekordok névrészének és születési hely részének egymás után fűzésével kapott karaktersorozat

a sorozatbeli rekordok születési hely és év részének egymás után fűzésével kapott sorozat ( )

a sorozatbeli rekordok névrészeiből képzett karaktersorozat

üres sorozat

Hogyan használható a szekvenciális megfelelő az állapottértranszformáció leírására? Tekintsük a ?? fejezetben bemutatott példát. Ott egy szövegfile-t a benne levő szavak hosszainak file-jával helyettesítettük. Tegyük fel, hogy unió típus, ahol a szavakat alkotó betűk típusa, pedig az elválasztó jelek típusa. Ekkor az eredeti file és a absztrakt file között kell a kapcsolatot definiálnunk. Ehhez vezessünk be még két absztrakt filetípust: legyen , ahol és , továbbá legyen . Ekkor:

Fel kell még tennünk azt, hogy a lehető leghosszabb azonos típusú részsorozatokból áll, vagyis az típus invariáns tulajdonsága:

A fenti leírás matematikai egzaktsággal definiálja azt az állapottértranszformációt, amit a ?? fejezetben csak szavakkal írtunk le. Természetesen másképp is formalizálható egy állapottértranszformáció, de a szekvenciális megfelelő használata sokszor leegyszerűsíti a leírást.