PROGRAMMIERAUFGABE 6.1

signature VECTOR =
  sig
    type vector
    val zero : vector
    val scale : real * vector -> vector
    val add : vector * vector -> vector
    val dot : vector * vector -> real
    val euclid2 : vector -> real
  end

signature POINT =
  sig
    structure Vector : VECTOR
    type point
    (* move a point along a vector *)
    val translate : point * Vector.vector -> point
    (* the vector from a to b *)
    val ray : point * point -> Vector.vector
  end

signature SPHERE =
  sig
    structure Vector : VECTOR
    structure Point : POINT
    sharing Point.Vector = Vector
    type sphere
    val sphere : Point.point * Vector.vector -> sphere
    val contains : sphere * Point.point -> bool
  end

signature GEOMETRY =
  sig
    structure Point : POINT
    structure Sphere : SPHERE
    sharing Point = Sphere.Point
        and Point.Vector = Sphere.Vector
  end

structure Vector2 : VECTOR =
  struct
    type vector = real * real;
    val zero = (0.0,0.0)
    fun scale (c:real,(x,y)) = (c*x,c*y)
    fun add ((x:real,y:real),(x',y')) = (x+x',y+y')
    fun dot ((x:real,y:real),(x',y')) = x * x' + y * y'
    fun euclid2 v = dot(v,v)
  end

structure Point2 : POINT =
  struct
    structure Vector = Vector2
    type point = Vector.vector
    val translate = Vector.add
    fun ray (p,p') = Vector.add(Vector.scale(~1.0,p),p')
  end

structure Sphere2 : SPHERE =
  struct
    structure Vector = Vector2;
    structure Point = Point2;
    datatype sphere = sphere of Point.point * Vector.vector;
    fun contains (sphere(p,r),p') =
          Vector.euclid2(Point.ray(p,p')) <= Vector.euclid2(r)
  end

structure Geometry : GEOMETRY =
  struct
    structure Point = Point2;
    structure Sphere = Sphere2;
  end


PROGRAMMIERAUFGABE 6.2

signature ZSP =
  sig
    type t
    val zero : t
    val sum : t * t -> t
    val prod : t * t -> t
  end

signature POLY =
  sig
    type t
    type poly
    val eval : poly -> t -> t
  end

functor Poly (Z : ZSP) : POLY =
  struct
  
    type t = Z.t;

    type poly = Z.t list;

    fun eval p x = foldl (fn (y,z) => Z.sum(y,Z.prod(z,x))) Z.zero p

  end

structure Int : ZSP =
  struct
    type t = int
    val zero = 0
    val sum = op+
    val prod = op*
  end

structure IntPoly = Poly(Int)

val x = 3 + IntPoly.eval [1,2,3,4] 10;


AUFGABE 6.3

Sigma = (S,Omega) mit 
  S = { int, bool, set }
  Omega = { singleton : int -> set,
            union : set * set -> set,
            elementof : int * set -> bool }

A und B sind Sigma-Algebren mit

  A_int = B_int = Menge der ganzen Zahlen
  A_bool = B_bool = { true, false }

  B_set = Menge der endlichen Mengen ganzer Zahlen

  singleton_B(x) = {x}
  union_B(x,y) = x union y
  elementof_B(x,y) = x element y

  A_set = Menge der endlichen Listen ganzer Zahlen

  singleton_A(x) = [x]
  union_A(x,y) = merge(x,y)
  elementof_A(x,y) = containedin(x,y)

    dabei sind merge und contains definiert durch

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

    fun containedin x [] = false
      | containedin x (y::l) =
          if x = y then
            true
          else if x < y then
	    false
          else
            containedin x l

A implementiert B auf set. Dazu ist zu zeigen:

  A_s = B_s für alle s != set in S (offensichtlich)

  Es gibt eine Abstraktionsfunktion a : A_set -> B_set:
    a([x1,...,xn]) = {x1,...,xn}

  Es gibt eine Repräsentationsinvariante I subseteq A_set:
    I = Menge aller aufsteigend sortierten endlichen Listen ganzer Zahlen
        ohne Duplikate

  Es gilt:

    für alle x in A_int:
      a(singleton_A(x)) = singleton_B(x) und I(singleton_A(x))

      Beweis: offensichtlich.

    für alle x,y in A_set:
      I(x) und I(y) impliziert
        a(union_A(x,y)) = union_B(a(x),a(y)) und I(union_A(x,y))

      Beweis: durch Induktion über die Summe der Längen von x und y.

    für alle x in A_int, y in A_set:
      I(y) impliziert
        elementof_A(x,y) = elementof_B(x,a(y))

      Beweis: durch Induktion über die Länge von y.