PROGRAMMIERAUFGABE 3.1

datatype term = var of string | lambda of string * term | app of term * term;

(* fun sort, fun uniq: siehe letztes Übungsblatt *)

local
  fun strsmaller (x:string) y = (x < y);
  fun removedupl l = uniq (sort strsmaller l);
in
  fun freevars (var x) = [x]
    | freevars (lambda (x,t)) = List.filter (fn y => x <> y) (freevars t)
    | freevars (app (t,t')) = removedupl ((freevars t) @ (freevars t'));
end


PROGRAMMIERAUFGABE 3.2

local
  (* getnewname x l erzeugt durch Anhängen einer genügend großen Zahl
     von "'" an x einen Namen, der nicht in l vorkommt. *)

  fun getnewname x l =
        let val x' = x ^ "'"
        in if List.exists (fn y => x' = y) l then
          getnewname x' l
        else
          x'
        end
        
  (* replacefree x t0 t berechnet den Term, der durch Ersetzen der
     freien Vorkommen von x in t durch t0 entsteht. *)

  fun replacefree x t0 (var y) =
        if x = y then t0 else var y
    | replacefree x t0 (lambda (y,t)) =
        if x = y then lambda (y,t) else lambda (y,replacefree x t0 t)
    | replacefree x t0 (app (t,t')) =
        app (replacefree x t0 t, replacefree x t0 t')

  (* renameboundvars' t l benennt die gebundenen Variablen in t so um,
     daß keine gebundene Variable den gleichen Namen wie eine vorher
     aufgetretene gebundene Variable oder eine Variable aus l hat,
     und liefert ein Paar zurück, das aus dem geänderten Term und
     der Liste der in Zukunft reservierten Namen besteht. *)

  fun renameboundvars' (var x) l = (var x, l)
    | renameboundvars' (lambda (x,t)) l =
        if List.exists (fn y => x = y) l then
          let val x' = getnewname x l
              val t' = replacefree x (var x') t
              val (t0,l0) = renameboundvars' t' (x' :: l)
          in (lambda (x',t0), l0)
          end
        else
          let val (t0,l0) = renameboundvars' t (x :: l)
          in (lambda (x,t0), l0)
          end
    | renameboundvars' (app (t,t')) l =
        let val (t0,l0) = renameboundvars' t l;
            val (t1,l1) = renameboundvars' t' l0;
        in (app (t0,t1), l1)
        end

in
  fun renameboundvars t = #1 (renameboundvars' t (freevars t))
  
  fun applyBeta (t as lambda (_,_)) t' =
        let val (app (lambda(x,e),t'')) = renameboundvars (app (t,t'))
        in replacefree x t'' e
        end
    | applyBeta t t' =
        app (t,t')
end


AUFGABE 3.3

Lemma: Die Auswertung von insert x l terminiert für jedes x und l.

Beweis: Strukturelle Induktion über l: Falls l = [], so terminiert
insert x l offensichtlich. Falls l = y::l', so ist die Terminierung
offensichtlich für x < y, anderenfalls folgt sie aus der
Induktionsvoraussetzung.

Satz: Die Auswertung von inssort l terminiert für jedes l.

Beweis: Strukturelle Induktion über l: Der Fall l = [] ist wieder
offensichtlich. Falls l = y::l', so terminiert die Auswertung von
inssort l aufgrund der Induktionsvoraussetzung und die Auswertung von
insert x (inssort l) aufgrund des vorstehenden Lemmas.


AUFGABE 3.4

Def.: Für eine int-Liste l sei MM(l) die Multimenge aller Elemente von l.

Def.: Für einen Ausdruck e sei V(e) der Wert, der sich durch Auswertung
von e ergibt.

Lemma: Für jede int-Liste l ist MM(V(insert x l)) = MM(x::l).

Beweis: Strukturelle Induktion über l: Falls l = [], dann ist nach
Definition von insert MM(V(insert x []) = MM([x]) = MM(x::[]). 
Falls l = y::l', so unterscheiden wir zwischen zwei Fällen: 
Ist x < y, dann erhalten wir unmittelbar 

    MM(V(insert x (y::l'))) 
  = MM(x::y::l'). 

Anderenfalls ergibt sich

    MM(V(insert x (y::l'))) 
  = MM(V(y::(insert x l'))) 
  = MM(y::V(insert x l'))) 
  = {y} \cup MM(V(insert x l'))
  = {y} \cup MM(x::l')               [nach Induktionsvoraussetzung]
  = {y,x} \cup MM(l')
  = MM(x::y::l').

Satz: Für jede int-Liste l ist MM(V(inssort l)) = MM(l).

Beweis: Strukturelle Induktion über l: Der Fall l = [] ist wieder
offensichtlich. Falls l = x::l', dann ist 

    MM(V(inssort (x::l'))) 
  = MM(V(insert x (inssort l')))
  = MM(V(insert x (V(inssort l'))))
  = MM(x::(V(inssort l')))           [nach vorstehendem Lemma]
  = {x} \cup MM(V(inssort l'))
  = {x} \cup MM(l')                  [nach Induktionsvoraussetzung]
  = MM(x::l')


AUFGABE 3.5

Lemma: Für jede sortierte int-Liste l ist V(insert x l) sortiert.

Beweis: Strukturelle Induktion über l: Im Fall l = [] ist V(insert x [])
= [x] offensichtlich sortiert. Falls l = y::l', dann muß y das kleinste
Element von l sein. Wir unterscheiden zwischen zwei Fällen: Ist x < y,
dann ist V(insert x (y::l')) = x::y::l'; da x < y <= y' für jedes
beliebige Element y' von l' ist diese Liste sortiert. Anderenfalls ist
V(insert x (y::l')) = y::(V(insert x l')). Nach Induktionsvoraussetzung
ist V(insert x l') sortiert, außerdem ist laut Aufgabe 3.4
MM(V(insert x l')) = MM(x::l'). Da y <= x und y <= y' für jedes
beliebige Element y' von l' ist, ist also auch y <= y'' für jedes
beliebige Element y'' von V(insert x l'); damit ist y::(V(insert x l'))
sortiert.

Satz: Für jede int-Liste l ist V(inssort l) sortiert.

Beweis: Strukturelle Induktion über l: Der Fall l = [] ist trivial.
Falls l = y::l', dann ist V(inssort (x::l')) = V(insert x (inssort l'))
= V(insert x (V(inssort l'))). Nach Induktionsvoraussetzung ist
V(inssort l') sortiert, und nach dem vorstehenden Lemma ist
V(insert x (V(inssort l'))) ebenfalls sortiert.