(* =========================================================================== *)
(* Aufgabe 1:                                                                  *)
(*                                                                             *)
(* Es gilt                                                                     *)
(*                                                                             *)
(* -  ggT (x, 0) = x                                                           *)
(*               = 1 * x + 0 * 0                                               *)
(*                                                                             *)
(* also können wir im Falle y = 0 die Koeffizienten 1 und 0 wählen.            *)
(*                                                                             *)
(* Für y > 0 gilt                                                              *)
(*                                                                             *)
(* -  ggT (x, y) = ggT (y, x mod y)                                            *)
(*                                                                             *)
(* und wir nehmen an, dass wir schon Koeffizienten m und n gefunden haben mit  *)
(*                                                                             *)
(* -  ggT (y, x mod y) = m * y + n * (x mod y)                                 *)
(*                                                                             *)
(* Dann ergibt sich                                                            *)
(*                                                                             *)
(* -  ggT (x, y) = m * y + n * (x mod y)                                       *)
(*               = m * y + n * (x - y * (x div y))                             *)
(*               = n * x + (m - n * (x div y)) * y                             *)
(*                                                                             *)
(* also können wir hier die Koeffizienten n und m - n * (x div y) wählen.      *)
(* (Die Klammern sind wichtig, denn n * (x div y) und (n * x) div y stimmen im *)
(* Allgemeinen nicht überein.) Damit erhalten wir die folgende Rekursion.      *)
(* =========================================================================== *)

let rec ggT_koeff (x, y) = 
  if y = 0 
  then (x, 1, 0) 
  else let (g, m, n) = ggT_koeff (y, x mod y) in (g, n, m - n * (x / y));;

List.map ggT_koeff [(3,4); (6,15); (21,33); (100,245)];;

let test_ggT_koeff (x, y) = 
  let (g, m, n) = ggT_koeff (x, y) in 
    if g = m * x + n * y
    then print_string (string_of_int g ^ " = " ^
		       string_of_int m ^ " * " ^
		       string_of_int x ^ " + " ^
		       string_of_int n ^ " * " ^
		       string_of_int y ^ "\n")
    else print_string "Fehler\n";;

ignore (List.map test_ggT_koeff [(3,4); (6,15); (21,33); (100,245)]);;


(* =========================================================================== *)
(* Aufgabe 2:                                                                  *)
(*                                                                             *)
(* Die Vergleichsoperatoren sind Observatoren. Also dürfen wir annehmen, dass  *)
(* ihre Argumente die Darstellungsinvariante erfüllen, d.h. dass es gekürzte   *)
(* Brüche mit positivem Nenner sind.                                           *)
(* =========================================================================== *)

(* =========================================================================== *)
(* Da diese Darstellung einer rationalen Zahl eindeutig ist, können wir die    *)
(* Gleichheit einfach als die Gleichheit von Paaren implementieren (zwei Paare *)
(* sind gleich, wenn sie komponentenweise übereinstimmen).                     *)
(* =========================================================================== *)

let eq: rat -> rat -> bool = (=);;

(* =========================================================================== *)
(* Bei allen anderen Vergleichsoperatoren bringen wir die beiden Brüche auf    *)
(* den Hauptnenner und vergleichen dann die Zähler der erweiterten Brüche,     *)
(* z.B. für die <-Operation:                                                   *)
(* =========================================================================== *)

let less ((a1,b1): rat) ((a2,b2): rat): bool = 
  let g = ggT b1 b2 in b2/g * a1 < b1/g * a2;;

(* =========================================================================== *)
(* Ganz analog könnte man jetzt <=, > und >= auf dem Typ rat implementieren.   *)
(* Aber statt den Code mehrmals fast unverändert zu wiederholen, definiert     *)
(* man besser eine "generische" Vergleichsfunktion compare, die einen Operator *)
(* op: int -> int -> bool als Parameter hat. Dann erhält man <, <=, > und >=   *)
(* auf rat, indem man die entsprechenden integer-Operation für op einsetzt.    *)
(* =========================================================================== *)

let compare (op: int -> int -> bool) ((a1,b1): rat) ((a2,b2): rat): bool =
  let g = ggT b1 b2 in op (b2/g * a1) (b1/g * a2);;

let less = compare (<);;

let leq = compare (<=);;

let grt = compare (>);;

let geq = compare (>=);;

List.map (eq (rat (3,4))) [rat (6,8); rat (10,7); rat (0,10); rat (-2,5)];;

List.map (less (rat (3,4))) [rat (6,8); rat (10,7); rat (0,10); rat (-2,5)];;

List.map (leq (rat (3,4))) [rat (6,8); rat (10,7); rat (0,10); rat (-2,5)];;

List.map (grt (rat (3,4))) [rat (6,8); rat (10,7); rat (0,10); rat (-2,5)];;

List.map (geq (rat (3,4))) [rat (6,8); rat (10,7); rat (0,10); rat (-2,5)];;


(* =========================================================================== *)
(* Aufgabe 4:                                                                  *)
(*                                                                             *)
(* Die Idee bei dieser Typdefinition ist, dass wir eine Menge A mit Elementen  *)
(* vom Typ 'a durch ihre charakteristische Funktion                            *)
(*                                                                             *)
(*   c_A: 'a -> bool                                                           *)
(*   x -> true   falls x aus A                                                 *)
(*   x -> false   sonst                                                        *)
(*                                                                             *) 
(* darstellen. Eine Implementierung der Funktion c_A können wir genau dann     *)
(* finden, wenn sie berechenbar ist, d.h. wenn die Menge A entscheidbar ist,   *)
(* z.B. ist die Menge G der geraden Zahlen entscheidbar, weil wir c_G durch    *)
(*                                                                             *) 
(*    fun x: int -> x mod 2 = 0                                                *)
(*                                                                             *) 
(* implementieren können. Wenn wir eine OPERATION auf Mengen wie z.B. diff     *)
(* implementieren können, so beweisen wir damit, dass aus der Berechenbarkeit  *)
(* von c_A und c_B stets die Berechenbarkeit von c_(A \ B) folgt, d.h. dass    *)
(* die Klasse der entscheidbaren Mengen unter Vereinigung ABGESCHLOSSEN ist.   *)
(* Ähnlich würde eine Implementierung der Funktionen preimage und image be-    *)
(* deuten, dass aus der Berechenbarkeit von c_A und einer totalen Funktion f   *)
(* die Berechenbarkeit von c_(f^-1(A)) bzw. c_(f(A)) folgt, d.h. wir würden    *)
(* damit beweisen, dass die Klasse der entscheidbaren Mengen unter dem Urbild  *)
(* bzw. Bild einer totalen berechenbaren Funktion abgeschlossen ist. Aus GTI   *)
(* wissen wir, dass Letzteres NICHT gilt: f(A) ist im Allgemeinen nur semi-    *)
(* entscheidbar und nicht entscheidbar. Deshalb kann der Versuch, die Funktion *)
(* image zu definieren nur scheitern.                                          *)
(* =========================================================================== *)

type 'a set = 'a -> bool;;

let member (x: 'a) (p: 'a set): bool = p x;;

let diff (p: 'a set) (q: 'a set): 'a set = fun x -> p x && not (q x);;

let preimage (f: 'a -> 'b) (p: 'b set): 'a set = fun x -> p (f x);;


(* =========================================================================== *)
(* Aufgabe 5:                                                                  *)
(*                                                                             *)
(* In der Vorlesung haben wir eine Funktion iterate definiert mit              *)
(*                                                                             *)
(*   iterate n f = f^n                                                         *)
(*                                                                             *)
(* d.h. für jede natürliche Zahl n ist                                         *)
(*                                                                             *)
(*   iterate n = lambda f. lambda x. f^n x                                     *)
(*                                                                             *)
(* gerade die n-te Church numeral.                                             *)
(* =========================================================================== *)

let rec iterate n f x = if n = 0 then x else f (iterate (n - 1) f x);;

(* =========================================================================== *)
(* Der Ergebnistyp der Funktion iterate sollte also der passende Typ für alle  *)
(* Church numerals sein. Also versuchen wir:                                   *)
(* =========================================================================== *)

type church = ('a -> 'a) -> 'a -> 'a;;

(* =========================================================================== *)
(* So geht's nicht, wir müssen church als parametrisierten Typ definieren.     *)
(* =========================================================================== *)

type 'a church = ('a -> 'a) -> 'a -> 'a;;

(* =========================================================================== *)
(* int_to_church ist dann nichts anderes als die Funktion iterate.             *)
(* =========================================================================== *)

let int_to_church: int -> 'a church = iterate;;

(* =========================================================================== *)
(* Wenn wir church_n für die n-te Church numeral schreiben, so gilt            *)
(*                                                                             *)
(*    n = succ^n 0                                                             *)
(*      = church_n succ 0                                                      *)
(*                                                                             *)
(* also können wir die Umkehrfunktion church_to_int wie folgt definieren.      *)
(* =========================================================================== *)

let church_to_int church_n = church_n (fun x -> x + 1) 0;;

(* =========================================================================== *)
(* Addition, Multiplikation und Potenzieren von Church numerals erhalten wir   *)
(* durch die Gleichungen                                                       *)
(*                                                                             *) 
(*  -  church_(m+n) f x = f^(m+n) x                                            *)
(*                      = f^m (f^n x)                                          *)
(*                      = church_m f (church_n f x)                            *)
(*                                                                             *)
(*  -  church_(m*n) f = f^(m*n)                                                *)
(*                    = (f^m)^n                                                *)
(*                    = church_n (church_m f)                                  *)
(*                                                                             *)
(*  -  church_(m^n) f = f^(m^n)                                                *)
(*                    = f^(m*...*m)                     (n-mal)                *)
(*                    = (...(f^m)...)^m                                        *)
(*                    = church_m (... (church_m f)...)                         *)
(*                    = (church_m o ... o church_m) f                          *)
(*                    = (church_m)^n f                                         *)
(*                    = (church_n church_m) f                                  *)
(*                                                                             *)
(*     also  church_(m^n) = church_n church_m                                  *)
(*                                                                             *)
(* Wir versuchen diese Operationen auf dem Typ 'a church zu definieren.        *)
(* =========================================================================== *)

let add (church_m: 'a church) (church_n: 'a church): 'a church = 
  fun f -> fun x -> church_m f (church_n f x);;

let mul (church_m: 'a church) (church_n: 'a church): 'a church = 
  fun f -> church_n (church_m f);;

let exp (church_m: 'a church) (church_n: 'a church): 'a church = 
  church_n church_m;;

(* =========================================================================== *)
(* Bei exp geht es schief, weil wir church_n nicht auf die Funktion church_m   *)
(* vom gleichen Typ anwenden können. Das lässt sich korrigieren, indem wir     *)
(* eine andere "Instanz" der polymorhen Funktion church_n wählen ...           *)
(* =========================================================================== *)

let exp (church_m: 'a church) (church_n: ('a -> 'a) church): 'a church = 
  church_n church_m;;

(* =========================================================================== *)
(* ... oder indem wir einfach dem O'Caml Typechecker die Arbeit überlassen.    *)
(* =========================================================================== *)

let add church_m church_n = fun f -> fun x -> church_n f (church_m f x);;

let mul church_m church_n = fun f -> church_n (church_m f);;

let exp church_m church_n = church_n church_m;;

(* =========================================================================== *)
(* Und man kann tatsächlich mit Church numerals rechnen ...                    *)
(* =========================================================================== *)

church_to_int (exp (int_to_church 2) (int_to_church 20));;

church_to_int (exp (int_to_church 2) (add (int_to_church 3) (int_to_church 5)));;

church_to_int (exp (int_to_church 2) (mul (int_to_church 3) (int_to_church 5)));;

church_to_int (exp (int_to_church 2) (exp (int_to_church 4) (int_to_church 2)));;

(* =========================================================================== *)
(* ... allerdings nicht ganz so flexibel wie im ungetypten lambda-Kalkül.      *)
(* =========================================================================== *)

let self_exp n = exp n n;;