Algorithmus zum Überprüfen der Subtyp-Relation

Zunächst wird zu dem nichtdeterministischen endlichen Automaten, der durch einen regulären Typ gegeben ist, ein deterministischer endlicher Automat konstruiert, indem Mengen von Zuständen anstelle der einzelnen Zustände betrachtet werden.

Die Definitionen von $init()$ und $\rightarrow$ werden dann auf Zustandsmengen erweitert:

$$init(X)=\{r\mid \exists x\in X,x',x\overset {r}{\rightarrow }x'\}$$

$$X\overset {r}{\rightarrow }X':\Leftrightarrow X'=\{x'\mid \exists x\in X,x\overset {r}{\rightarrow }x'\}$$

Der folgende Algorithmus überprüft, ob $x:<y$ gilt

1. falls nicht $init(y)\subseteq init(x)$, dann FAIL

2. add $(\{x\},\{y\},init(y))$ to $LIST$

3. falls möglich, ein $(X,Y,R)$ mit $R\neq \emptyset$ in $LIST$ auswählen,

sonst SUCCEED

4. ein $r$ aus $R$ auswählen

und $(X,Y,R)$ in $LIST$ durch $(X,Y,R\setminus \{r\})$ ersetzen

5. $X'$ und $Y'$ mit $X\overset {r}{\rightarrow }X'$ und $Y\overset {r}{\rightarrow }Y'$ berechnen

6. falls $(X',Y',R')$ mit $R'$ beliebig bereits in $LIST$, dann goto 3

7. falls nicht $init(Y')\subseteq init(X')$, dann FAIL

8. falls nicht $\forall x\in X'$ $\exists y\in Y'$: $init(y)\subseteq init(x)$, dann FAIL

9. add $(X',Y',init(Y'))$ to $LIST$

10. goto 3

Die Arbeitsweise dieses Algorithmus soll beispielhaft für die regulären Typen $NewNDStack$ und $Buf$ gezeigt werden. Es soll überprüft werden, ob $NewNDStack:<Buf$ gilt.

Wir beginnen mit $x=s1$ und $y=b1$, und erhalten die folgende Liste

$LIST=$ $(\{s1\},\{b1\},\{put\})$

$\rightarrow$ $LIST=$ $(\{s1\},\{b1\},\{\})$ $(\{s2\},\{b2\},\{get\})$

$\rightarrow$ $LIST=$ $(\{s1\},\{b1\},\{\})$ $(\{s2\},\{b2\},\{\})$ $(\{s1,s2\},\{b1\},\{put\})$

$\rightarrow$ $LIST=$ $(\{s1\},\{b1\},\{\})$ $(\{s2\},\{b2\},\{\})$ $(\{s1,s2\},\{b1\},\{\})$

$(\{s2\},\{b2\},\{get\})$ ist unter 6. bereits in $LIST$ und unter 3. gibt es kein $(X,Y,R)$ mit $R\neq \emptyset$ in $LIST$ mehr. Also gilt die Beziehung $NewNDStack:<Buf$.