Aufgabe 1

--
concat l = foldr append Nil l;
Kons x xs = Cons{4,2} x xs;
append xs ys = foldr Kons ys xs;
foldr f z l =
   case l of
      <3>      -> z;
      <4> x xs -> f x (foldr f z xs);

length l =
   case l of
      <3>      -> 0;
      <4> x xs -> 1 + (length xs);
sum l = foldl plus Top l;
plus x y = x + y;
foldl f z l =
   case l of
      <3>      -> z;
      <4> x xs -> foldl f (f z x) xs;

--
-- Analyse
--
Nil = Cons{3,0};
nils = Kons Nil nils;
inf =

   case Top of
      <1> -> Kons Top inf;
      <2> -> Bot;
botelem =
   case Top of
      <5> -> Kons Bot Top;
      <6> -> Kons Top botelem;
      <7> -> Bot;

main1 x = concat nils;
main2 x = length inf;
main3 x = sum botelem;
main4a x = length (append inf Top);
main4b x = length (append Top inf);
lit x ys = case ys of
       <3> -> Nil;
       <4> y ys ->(lit2 x y ys);
lit2 x y ys = case (gl x y) of
       <2> -> (Kons ys Nil);
       <1> -> Nil;
gl x y = Top x y;
alt p q x = append (p x) (q x);
seq p q xs = case (p xs) of
       <3> -> Nil;
       <4> x xs -> seq2 q x xs;
seq2 q x xs = append (q x) (seq3 q xs);
seq3 q xs = case xs of
       <3> -> Nil;
       <4> x xs -> seq2 q x xs;
prek xs = alt (seq prek (lit Top)) (lit Top) xs;
loopsprek x = prek Top;

-------Ergebnisse
--concat [strict]
--Kons [?, ?]
--append [strict, ?]
--foldr [?, ?, strict]
--length [strict]
--sum [strict]
--plus [strict, strict]
--foldl [?, ?, strict]
--main1 [strict]
--main2 [strict]
--main3 [?]
--main4a [strict]
--main4b [strict]
--lit [?, strict]
--lit2 [?, ?, ?]
--gl [?, ?]
--alt [strict, ?, ?]
--seq [strict, ?, ?]
--seq2 [strict, ?, strict]
--seq3 [?, strict]
--prek [strict]
--loopsprek [strict]
--

Aufgabe 2

Wir wollen ein Beispiel für die Analyse einer detailierten Striktheitsbeschreibung einer Funktion auf binären markierten Bäumen geben. Hierzu deklarieren wir in Haskell-Syntax den entsprechenden Typ:

data BinBaum
  =  BNil
    |BCons BinBaum Int BinBaum

Der entsprechende algebraische Typ sei in der Kernsprache gegeben und damit die case-Konstante vom Typ: BinBaum→ τ → (BinBaum → Int → BinBaum → τ) → τ

Für den algebraischen Datentypen müssen wir jetzt einen abstrakten Domain kreieren. Wir gehen dabei erst einmal von der gegebenen, natürlichsprachlichen Beschreibung aus:

⊥: ein Ausdruck hat keine Kopfnormalform.

⋊ ⋉: ein Ausdruck hat höchstens eine Kopfnormalform.

R⊥: es kann höchstens der linkeste Pfad eines Baumes in der Länge bis zum Ende ausgewertet werden.

L⊥: es kann höchstens der rechteste Pfad eines Baumes in der Länge bis zum Ende ausgewertet werden.

R⊥∈: es kann höchstens der linkeste Pfad eines Baumes komplett mit allen auf diesem Pfad enthaltenen Elementen ausgewertet werden.

L⊥∈: es kann höchstens der rechteste Pfad eines Baumes komplett mit allen auf diesem Pfad enthaltenen Elementen ausgewertet werden.

⊥∈: die komplette Baumstruktur läßt sich unter Umständen auswerten aber auch nicht mehr, d.h. mindestens einmal ist Bot die Markierung eines Knotens oder der Baum enthält mindestens einen unendlichen Pfad. Wir können dies auch folgendermaßen charakterisieren: Mehr als ein Pfad eines Baumes kann komplett mit allen auf diesem Pfad enthaltenen Elementen ausgewertet werden, aber auch für mindestens einen Pfad trifft dies nicht zu. Somit leuchtet ein, daß ⊥∈ sowohl L⊥∈ als auch R⊥∈ umfaßt.

⊤: der Ausdruck kann eine Normalform haben.

Sei D_{BinBaum} nun die Menge {⊥, ⋊ ⋉ , L⊥, R⊥, L⊥∈ , R⊥∈ , ⊥∈ , ⊤} dann können wir nach der obigen Beschreibung eine Ordnung angeben, die in Abbildung 1 zu sehen ist.

Schließlich gilt es, exakte abstrakte Interpretationen der eingebauten Konstanten und Funktionen zu geben. Wir werden uns dies anhand der obigen Beschreibung intuitiv überlegen, um uns vorerst nicht mit dem Formalismus belasten zu müssen. Ganz wichtig ist, zu sehen, daß BNil nicht nur eine Kopfnormalform, sondern sogar eine Normalform ist. Daher kann für dessen abstrakte Interpretation einzig gelten: BNil_{abs} = ⊤ oder [[BNil]]^{a} = ⊤ oder α(BNil) = ⊤, um alle Schreibweisen einmal bedient zu haben.

Abbildung 1: Der abstrakte Domain für BinBaum.

Für BCons_{abs} x ⊥ y versuchen wir es auf eine ähnliche Art und Weise: Indem wir uns z.B. überlegen, was dabei herauskommt, wenn die Wurzel eines Baumes mit Bot markiert ist, der linke Teilbaum einer ist, dessen linkester Pfad in der Länge bis zum Ende ausgewertet werden kann, und der rechte Teilbaum nur eine Kopfnormalform hat. Man sieht, daß man wieder einen Baum erhält, dessen linkester Pfad in der Länge bis zum Ende ausgewertet werden kann, sprich BCons_{abs} R⊥ ⊥ ⋊ ⋉ ∈ R⊥. Mit Hilfe dieser Überlegungen erhalten wir eine Wertetabelle zunächst für BCons_{abs} x ⊥ y:

\begin{matrix}⊥ & ⊥ & ⋊ ⋉ & L⊥ & R⊥ & L⊥∈ & R⊥∈ & ⊥∈ & ⊤ \\ ⊥ & ⋊ ⋉ & L⊥ & L⊥ & ⊥∈ & L⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ ⋊ ⋉ & R⊥ & ⊥∈ & L⊥ & ⊥∈ & L⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ L⊥ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & L⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ R⊥ & R⊥ & R⊥ & ⊥∈ & ⊥∈ & L⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ L⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ R⊥∈ & R⊥∈ & R⊥∈ & R⊥∈ & R⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ ⊤ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \end{matrix}

BCons_{abs} x ⊥ y

Ein paar grundsätzliche Gedanken dazu sind hilfreich:

• BCons_{abs} x ⊥ y bzw. im symmetrischen Fall BCons_{abs} y ⊥ x für x ∈ {⊥∈ , ⊤} ist immer ⊥∈ (für alle y). Man könnte auch sagen: Da wir die Markierung der Wurzel als ⊥ annehmen, kann der Baum ja gar nie eine Normalform haben.

• BCons_{abs} R⊥∈ ⊥ x ist R⊥∈ für x ∈ {⊥, ⋊ ⋉ , R⊥, L⊥} und ⊥∈ sonst. Symmetrisch dazu: BCons_{abs} x ⊥ L⊥∈ ist L⊥∈ für x ∈ {⊥, ⋊ ⋉ , L⊥, R⊥} und ⊥∈ sonst.

• Ein analoges Ergebnis erhält man für BCons_{abs} R⊥ ⊥ x mit x ∈ {⊥, ⋊ ⋉ } bzw. BCons_{abs} x ⊥ L⊥.

• Dagegen ist klar, daß BCons_{abs} x ⊥ R⊥∈ bzw. BCons_{abs} L⊥∈ ⊥ x immer ⊥∈ ist.

Einen Haken hat die Sache leider: Die Funktion, die wir definiert haben, ist nicht monoton. Auf den ersten Blick sieht es zwar schlimmer aus als es ist, da L⊥ und R⊥ sowie L⊥∈ und R⊥∈ ohnehin nicht vergleichbar sind, aber Schwierigkeiten macht uns

1. daß wir BCons_{abs} ⋊ ⋉ ⊥ ⋊ ⋉ mit ⊥∈ approximieren müssen, obwohl offenbar BCons_{abs} ⋊ ⋉ ⊥ ⋊ ⋉ ∈ ⋂{L⊥, R⊥, L⊥∈ , R⊥∈ , ⊥∈ } ist.

2. BCons_{abs} R⊥ ⊥ L⊥ = ⊥∈ wegen BCons_{abs} R⊥ ⊥ L⊥∈ = L⊥∈, obwohl ersteres intuitiv in L⊥∈ und R⊥∈ enthalten ist. Das gleiche gilt für den gleichsam symmetrischen Fall BCons_{abs} R⊥∈ ⊥ L⊥ = ⊥∈.

3. BCons_{abs} L⊥ ⊥ x für x ∈ {⊥, ⋊ ⋉ , L⊥} und BCons_{abs} y ⊥ R⊥ für y ∈ {⊥, ⋊ ⋉ , R⊥}.

Wir können diese Verletzungen der Monotonie am einfachsten dadurch beseitigen, daß wir BCons_{abs} x ⊥ y = ⊥∈ setzen für alle x, y ≥ ⋊ ⋉. Wir erhielten dann folgende Wertetabelle fürBCons_{abs} x ⊥ y:

\begin{matrix}⊥ & ⊥ & ⋊ ⋉ & L⊥ & R⊥ & L⊥∈ & R⊥∈ & ⊥∈ & ⊤ \\ ⊥ & ⋊ ⋉ & L⊥ & L⊥ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ ⋊ ⋉ & R⊥ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ L⊥ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ R⊥ & R⊥ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ L⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ R⊥∈ & R⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ ⊤ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \end{matrix}

BCons_{abs} x ⊥ y

Und ebenso für BCons_{abs} x ⊤ y:

\begin{matrix}⊤ & ⊥ & ⋊ ⋉ & L⊥ & R⊥ & L⊥∈ & R⊥∈ & ⊥∈ & ⊤ \\ ⊥ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ ⋊ ⋉ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ L⊥ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ R⊥ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ L⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ R⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \\ ⊤ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ & ⊥∈ \end{matrix}

BCons_{abs} x ⊤ y

Dadurch, daß wir schon BCons_{abs} ⊥ ⊤ ⊥ in ⊥∈ einordnen müssen und eine monotone Funktion definieren wollen, fällt die abstrakte Interpretation hier sehr einfach aus ^{1}.

Wir könnten auch noch weitere Werte in den abstrakten Domain aufnehmen, so zum Beispiel:

∞: ein Ausdruck ist lazy-terminierend, d.h. alle Äste des Baumes sind unendlich.

◯: es kann höchstens ein Pfad eines Baumes in der Länge bis zum Ende ausgewertet werden.

⨀: es kann höchstens ein Pfad eines Baumes komplett mit allen auf diesem Pfad enthaltenen Elementen ausgewertet werden.

So könnte man dann z.B. BCons_{abs} ⋊ ⋉ ⊥ ⋊ ⋉ = ∞ setzen und die Probleme mit der Monotonie auf eine andere Weise lösen. Wir werden hier aber nur ∞ für die Definition zu Hilfe nehmen:

• ⊥ :=< Bot >.

   • ⋊ ⋉ :=< Bot, BCons Bot Bot Bot >

• ∞ :=< Bot, BCons ∞ ⊤ ∞ >

• L⊥ :=< ∞, BCons ∞ ⊥ L⊥′ > mit L⊥′ :=< BNil, L⊥ > also L⊥ :=<

     Bot, BCons ∞ ⊤ ∞, BCons ∞ ⊥ BNil, BCons ∞ ⊥ L⊥ >.

1Eine andere Möglichkeit wäre, dort wo ein Wert sowohl in L⊥ (L⊥∈) als auch in R⊥ (R⊥∈) ist, einfach eine der beiden Mengen auszuwählen.

• R⊥ :=< ∞, BCons R⊥′ ⊥ ∞ > mit R⊥′ :=< BNil, R⊥ > also R⊥ :=<

     Bot, BCons ∞ ⊤ ∞, BCons BNil ⊥ ∞, BCons R⊥ ⊥ ∞ >.

• L⊥∈ :=< ∞, BCons ∞ ⊤ L⊥∈′ > mit L⊥∈′ :=< BNil, L⊥∈ >.

• R⊥∈ :=< ∞, BCons R⊥∈′ ⊤ ∞ > mit R⊥∈′ :=< BNil, R⊥∈ >.

• ⊥∈ :=< Bot, BCons ⊤ ⊥ ⊤, BCons ⊥∈′ ⊤ ⊤, BCons ⊤ ⊤ ⊥∈′ > mit ⊥∈′ :=< BNil, ⊥∈ >, das bedeutet ⊥∈ :=< Bot, BCons ⊤ ⊥ ⊤,

     BCons ⊥∈ ⊤ ⊤, BCons BNil ⊤ ⊤, BCons ⊤ ⊤ ⊥∈ , BCons ⊤ ⊤ BNil >.

• ⊤ :=< Top >.

Schließlich fehlt uns noch eine abstrakte Interpretation für case. Wir geben sie im folgenden an:

case_{abs} ⊥ e_{1} e_{2} = ⊥
case_{abs} ⋊ ⋉ e_{1} e_{2} = e_{2} ⊥ ⊥
case_{abs} L⊥ e_{1} e_{2} = ⊔{e_{2} ∞ ⊤ ∞, e_{2} ∞ ⊥ BNil, e_{2} ∞ ⊥ L⊥}
case_{abs} R⊥ e_{1} e_{2} = ⊔{e_{2} ∞ ⊤ ∞, e_{2} BNil ⊥ ∞, e_{2} R⊥ ⊥ ∞}
case_{abs} L⊥∈ e_{1} e_{2} = ⊔{e_{2} ∞ ⊤ ∞, e_{2} ∞ ⊤ BNil, e_{2} ∞ ⊤ L⊥∈ }
case_{abs} R⊥∈ e_{1} e_{2} = ⊔{e_{2} ∞ ⊤ ∞, e_{2} BNil ⊤ ∞, e_{2} R⊥∈ ⊤ ∞}
case_{abs} ⊥∈ e_{1} e_{2} = ⊔{e_{2} ⊤ ⊥ ⊤, e_{2} ⊥∈ ⊤ ⊤, e_{2} BNil ⊤ ⊤,
e_{2} ⊤ ⊤ ⊥∈ , e_{2} ⊤ ⊤ BNil}
case_{abs} ⊤ e_{1} e_{2} = ⊔{e_{1}, e_{2} ⊤ ⊤ ⊤}

Ein anderer Domain

Wir wollen für den alternativen Domain die Ordnung aus Abbildung 2 angeben und die noch fehlenden Werte definieren:

• ◯ :=< ∞, BCons ◯′ ⊥ ∞, BCons ∞ ⊥ ◯′ > mit ◯′ :=< BNil, ◯ >.

• ⨀ :=< ∞, BCons ⨀′ ⊤ ∞, BCons ∞ ⊤ ⨀′ > mit ⨀′ :=< BNil, ⨀ >.

Dabei fällt auf, daß noch eine sprachliche Charakterisierung von ⊥∈ möglich ist, die den Unterschied zu ⨀ besonders hervorhebt: Beliebig viele Pfade eines Baumes können komplett mit allen auf diesen Pfaden enthaltenen Elementen ausgewertet werden, aber auch für mindestens einen Pfad trifft dies nicht zu.

9

Abbildung 2: Der alternative abstrakte Domain für BinBaum.