PROGRAMMIERAUFGABE 2.1

fun sort smaller [] = []
  | sort smaller [e] = [e]
  | sort smaller l =
      let fun split [] = ([],[])
            | split [e] = ([e],[])
            | split (e1::e2::l0) = 
                let val (l1,l2) = split l0 in (e1::l1,e2::l2) end;

          fun merge [] l0 = l0
            | merge l0 [] = l0
            | merge (e1::l1) (e2::l2) =
                if smaller e1 e2 then
                  e1 :: (merge l1 (e2::l2))
                else
                  e2 :: (merge (e1::l1) l2);

          val (l1,l2) = split l
          val s1 = sort smaller l1
          val s2 = sort smaller l2
      in merge s1 s2 end;


PROGRAMMIERAUFGABE 2.2

fun uniq [] = []
  | uniq [x] = [x]
  | uniq (x::y::l) = if x = y then uniq (y::l) else x::(uniq (y::l));


PROGRAMMIERAUFGABE 2.3

datatype term = var of string | a | b | f of term | g of term * term;

local
  (* varsd t liefert die Liste aller Variablen*vorkommen* im Term t,
     ohne Löschung von Duplikaten. *)

  fun varsd a = []
    | varsd b = []
    | varsd (f x) = varsd(x)
    | varsd (g(x,y)) = varsd(x) @ varsd(y)
    | varsd (var s) = [s];
  fun strsmaller (x:string) y = (x < y);
in
  fun vars t = 
        uniq (mergesort strsmaller (varsd t));

  fun isground t = 
        varsd t = [];

  fun islinear t = 
        let val v = mergesort strsmaller (varsd t) in v = uniq v end;

  fun positionsof t (var s) =
        if t = var s then [[]] else []
    | positionsof t a =
        if t = a then [[]] else []
    | positionsof t b =
        if t = b then [[]] else []
    | positionsof t (f x) =
        if t = f x then [[]] else map (fn x => 1::x) (positionsof t x)
    | positionsof t (g (x,y)) =
        if t = g (x,y) then
          [[]] 
        else 
          (map (fn x => 1::x) (positionsof t x))
            @ (map (fn x => 2::x) (positionsof t y));
end

  
AUFGABE 2.4

Die Definition ist genau dann zulässing, wenn f bereits vorher mit
passendem Typ deklariert wurde; dieses vorher deklarierte f wird in
der zweiten Klausel aufgerufen. Dies ist keine rekursive Definition,
auch wenn sie auf den ersten Blick so aussieht.


AUFGABE 2.5

val (x1,...,xn) = (e1,...,en)


AUFGABE 2.6

Die Relation ist terminierend, da bei jeder Regelanwendung die Anzahl
derjenigen f-Operatoren, die unmittelbar unter einem anderen f-Operator
stehen, um mindestens 1 (möglicherweise auch um 2) verringert wird.
Die Relation ist nicht konfluent: ausgehend von f(f(f(x))) existieren
die beiden Ableitungen f(f(f(x))) -> f(g(f(g(f(x))))) und
f(f(f(x))) -> f(f(g(f(g(x))))) -> f(g(f(g(g(f(g(x))))))); die beiden so
erreichten Terme sind verschieden und in Normalform; es existiert also
kein Term, auf den sich beide reduzieren lassen.