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:
,
kölcsönösen egyértelmű (bijektív),
megengedett típuskonstrukció (azaz direktszorzat, unió és iterált konstrukciókból
épül fel)
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 |
| a
|
| a |
| a
|
| ü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:
az és az
közötti kapcsolat:
az és a
közötti kapcsolat:
a és a
közötti kapcsolat:
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.