PROGRAMMIERAUFGABE 5.1

datatype 'a stream = Nil | Cons of 'a * (unit -> 'a stream) ref;

fun tail(Cons(_,f)) = 
      let val res = (!f)() 
      in (f := (fn () => res); res)
      end;

fun head(Cons(a,_))=a;

(* fun Consq(x,f) = Cons(x, ref(fn () => f)) *)

fun nth xs n =
      if n = 0 then head(xs) else nth (tail xs) (n-1);

fun sum f 0 = f 0
  | sum f n = (f n) + (sum f (n-1));

fun cata n =
      Cons(if n = 0 then 1 else gencata n (cata 0),
           ref(fn () => (cata (n+1))))

and gencata n c =
      sum (fn k => (nth c k) * (nth c (n-k-1))) (n-1);


(* Dieses Programm ist nicht so effizient, wie man sich wünscht,
   da innerhalb von cata jedesmal (cata 0) neu aufgerufen und
   (wenigstens teilweise) auch berechnet wird. Mit einer
   Variablen cata0, die den Wert von (cata 0) ein für allemal
   speichert, ginge das schneller; das würde aber wechselseitig
   rekursive Definitionen der Funktion cata und der Variablen
   cata0 erfordern. Bedauerlicherweise erlaubt ML rekursive
   Deklarationen (ob mit fun oder val rec) nur für Funktionen.
   Man kann das aber mittels einer ref-Variable simulieren,
   indem man die ref-Variable (cata0ref) erst deklariert, dann die
   Funktion (cata') definiert, in der !cata0ref benutzt wird, und
   schließlich cata0ref auf den gewünschten Wert setzt.
   Die Funktion cata braucht dann nur noch den gewünschten
   Teilstream von !cata0ref zu liefern: *)

fun nth xs n =
      if n = 0 then head(xs) else nth (tail xs) (n-1);

fun fromNth xs n =
      if n = 0 then xs else fromNth (tail xs) (n-1);

fun sum f 0 = f 0
  | sum f n = (f n) + (sum f (n-1));

val cata =
  let
    val cata0ref = ref (Nil : int stream)

    fun cata' n =
          Cons(if n = 0 then 1 else gencata n (!cata0ref),
               ref(fn () => (cata' (n+1))))

    and gencata n c =
          sum (fn k => (nth c k) * (nth c (n-k-1))) (n-1)
  in
    cata0ref := cata' 0;
    fn i => fromNth (!cata0ref) i
  end;


AUFGABE 5.2

Notation: alpha -> 'a
          tau   -> 't

  (1)   't1 = 't2 -> 't3
  (2)   't1 = 't6 -> 't6 -> 't7
  (3)   't2 = 'a1 -> 'a2
  (4)   't3 = 't4 -> 't5
  (5)   't4 = 'a2 -> 'a3
  (6)   't5 = 'a1 -> 'a3

Aus (1) und (2) folgt 't2 -> 't3 = 't6 -> 't6 -> 't7 und somit:
  (7)   't2 = 't6
  (8)   't3 = 't6 -> 't7

Aus (4) und (8) folgt:
  (9)   't4 = 't6
 (10)   't5 = 't7
           
Aus (3), (5), (7) und (9) folgt:
 (11)   'a1 = 'a2
 (12)   'a2 = 'a3
    
Damit: 'a1 = 'a2 = 'a3
       't2 = 't4 = 't5 = 't6 = 't7 = 'a1 -> 'a1
       't3 = ('a1 -> 'a1) -> ('a1 -> 'a1)
       't1 = ('a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1)


AUFGABE 5.3

Taut:
(1)    x : 't0 |- x : 't0

Abs aus (1):
(2)    |- lambda x.x : 't0 -> 't0

Gen aus (2):
(3)    |- lambda x.x : forall 't0. 't0 -> 't0

Taut:
(4)    i : forall 't0. 't0 -> 't0 |- i : forall 't0. 't0 -> 't0

Inst aus (4):
(5)    i : forall 't0. 't0 -> 't0 |- i : ('a -> 'a) -> ('a -> 'a)

Inst aus (4):
(6)    i : forall 't0. 't0 -> 't0 |- i : 'a -> 'a

App aus (5) und (6):
(7)    i : forall 't0. 't0 -> 't0 |- (i i) : 'a -> 'a

Let aus (3) und (7):
(8)    |- let i = lambda x.x in (i i) : 'a -> 'a


AUFGABE 5.4

Angenommen, eine Aussage der Form

  |- (lambda i.(i i))(lambda x.x) : 't

wäre (für ein beliebiges 't) ableitbar. Dann gäbe es eine kürzeste
Ableitung einer solchen Aussage. Der letzte Schritt dieser kürzesten
Ableitung kann weder ein Inst- noch ein Gen-Schritt sein (denn die
Ableitung ohne diesen letzten Schritt hätte dann immer noch die
geforderte Form, wäre aber echt kürzer). Der letzte Schritt kann
also nur ein App-Schritt sein, und dieser hat die Form

  |- (lambda i.(i i)) : 't0' -> 't0     |- (lambda x.x) : 't0'
  ------------------------------------------------------------
           |- (lambda i.(i i))(lambda x.x) : 't0

Eine Ableitung einer Aussage der oben angegebenen Form erfordert also
zunächst einmal eine Ableitung einer Aussage

  |- (lambda i.(i i)) : 't0' -> 't0

wobei 't0' und 't0 Typausdrücke ohne Quantoren sind. Wir zeigen nun,
daß so eine Ableitung nicht existiert. Dazu gehen wir wie oben vor:
Wir nehmen an, daß es eine kürzeste Ableitung einer solchen Aussage
gibt. Diese kann wiederum nicht mit einer Folge von Inst- oder
Gen-Schritten enden (denn durch Weglassen dieser Folge bekämen wir
eine kürzere Ableitung, die immer noch die geforderte Form hat).
Der letzte Schritt muß also ein Abs-Schritt sein, mit der Form

       i : 't0' |- (i i) : 't0
  ---------------------------------
  |- (lambda i.(i i)) : 't0' -> 't0

Die gleiche Methode zum drittenmal: Wir nehmen an, daß es eine
kürzeste Ableitung eine Aussage der Form

  i : 't0' |- (i i) : 't0

gibt. Diese kann wiederum nicht mit einer Folge von Inst- oder
Gen-Schritten enden (denn durch Weglassen dieser Folge bekämen wir
eine kürzere Ableitung, die immer noch die geforderte Form hat).
Der letzte Schritt muß ein App-Schritt sein:

  i : 't0' |- i : 't0'' -> t0      i : 't0' |- i : 't0''
  ------------------------------------------------------
                 i : 't0' |- (i i) : 't0

Zur Ableitung der beiden Prämissen dieses Schrittes stehen nur noch
Taut-, Inst- und Gen-Schritte zur Verfügung. Da Inst- und Gen-Schritte
den Teil der Formel vor |- unverändert lassen, gilt genauer, daß
die Ableitung für

  i : 't0' |- i : 't0'' -> t0

und die Ableitung für

  i : 't0' |- i : 't0''

beide mit einer Taut-Anwendung

  i : 't0' |- i : 't0'

beginnen müssen. Nun stellen wir aber fest, daß auf diese Aussage
weder die Inst- noch die Gen-Regel anwendbar ist: Inst erfordert eine
gebundene Variable, Gen eine Variable, die nicht frei vor |- vorkommt.
Damit steht fest, daß beide Ableitungen nur aus einem Taut-Schritt
bestehen können, sprich, 't0' muß identisch mit 't0'' -> t0 und
gleichzeitig identisch mit 't0'' sein. Das würde aber bedeuten,
daß die Typausdrücke 't0'' und 't0'' -> t0 identisch sein müssen;
da 't0'' ein echter Teilausdruck von 't0'' -> t0 ist, ist das offenbar
nicht möglich.