Seminar 3

Dateiinhalt

----------------------------------------------------------------------
--
--  Seminar Theoretische Informatik                         \ \
--  "Funktionale Programmierung mit Haskell"                 \ \ ---
--  Universität Potsdam SS 2014                              / /\ --
--  Tim Richter / Mario Frank                               / /  \
--
--  3: Zahlen
----------------------------------------------------------------------

----------------------------------------------------------------------
-- type und newtype ( Nachtrag Kapitel 2)
----------------------------------------------------------------------

analyse oben war Funktion auf (Int,Int,Int). Aussagekräftiger ist

> type Triangle = (Int,Int,Int)

und dann

< analyse' :: Triangle -> Triangletype
< ....

|Triangle| ist ein *Typsynonym* für |(Int,Int,Int)|.
Gleiche Typklassen, der Compiler verhält sich gleich auf beiden!

Im Unterschied dazu möchte man gelegentlich vordefinierte Typen
anders benutzen, z.B. möchte man Floats für Winkel verwenden, aber
die Gleichheit dann modulo 2*pi definieren. Mit

< type Angle = Float

geht das nicht, denn Float ist bereits in Eq ...

> data Angle  = MkAngle { toFloat :: Float }
>
> instance Eq Angle where
>   (MkAngle x) == (MkAngle y) =  normalize x == normalize y
>
> normalize :: Float -> Float
> normalize x
>     | x < 0      = normalize (x + rot)
>     | x >= rot   = normalize (x - rot)
>     | otherwise  = x  
>       where rot  = 2*pi 

Dies hat aber andere Nachteile:

1. Häufiges "wrap" mit |MkAngle und "unwrap" mit toFloat
   kosten unnötig Zeit
2. | MkAngle undefined /= undefined |, d.h.
   Angle und Float haben *nicht* die gleichen Elemente!

Haskell stellt hierfür "newtype" zur Verfügung. Die Syntax ist
analog zu data, es ist allerdings nur *ein* Konstruktor erlaubt: 

> newtype Angle' = MkAngle' { toFloat' :: Float }

|Angle'| *hat* exakt dieselben Elemente wie |Float|, hier gilt

< MkAngle' undefined = undefined

Elemente von |Angle'| werden nach dem Typechecking vom Compiler durch
|Floats| ersetzt -> keine Laufzeitverluste


Zahlen
------

Wir hatten bereits verschiedene Arten von Zahlen:

  Int        ganze Zahlen mit beschränkter Genauigkeit
  Integer         "       mit beliebiger Genauigkeit
  Rational   rationale Zahlen mit beliebiger Genauigkeit
  Float      floating-point Zahlen mit einfacher Genauigkeit
  Double          "                mit doppelter Genauigkeit
  Complex    komplexe Zahlen ...
  Nat        natürliche Zahlen (Übungsaufgaben)

Die grundlegende Typklasse für Zahlen in Haskell ist |Num| :

< class (Eq a, Show a) => Num a where
<   (+),(-),(*)  :: a -> a -> a
<   negate       :: a -> a
<   abs, signum  :: a -> a
<   fromInteger  :: Integer -> a

|Num| ist keine Teilklasse von |Ord|!
|Num| definiert keine Division!

"reelle Zahlen" sind geordnet und exakt durch rationale
Zahlen darstellbar.

< class (Num a, Ord a) => Real a where
<    toRational :: a -> Rational

"fractional numbers" sind solche, für die eine Division definiert
ist. 

< class (Num a) => Fractional a where
<   (/) :: a -> a -> a
<   recip :: a -> a
<   fromRational :: Rational -> a

Hierbei ist Rational der Typ der rationalen Zahlen mit beliebig
genauen Zählern und Nennern:

< data Ratio a
<
< type Rational = Ratio Integer

Für Typen in der Typklasse |Integral| (einer Teilklasse von |Real|)

< class (Real a, Enum a) => Integral a where
<    divMod :: a -> a -> (a,a)
<    toInteger :: a -> Integer

hat man hingegen Division mit Rest. Instanzen sind |Int| und |Integer|.

Zahlen eines Typs der Klasse |Integral| kann man in jeden numerischen 
Typen abbilden:

< fromIntegral :: (Integral a, Num b) => a -> b
< fromIntegral = fromInteger . toInteger

weitere Zahlklassen: RealFrac, Floating. Schauen Sie sich
diese bitte selbst an! 

----------------------------------------------------------------------
-- Beispiel: floor berechnen
----------------------------------------------------------------------

Wir wollen

< floor :: Float -> Integer

implementieren.  Spezifikation:

  floor x = m   <=>  m <= x < m + 1

Idee: Suche!

Wir brauchen eine Art Schleife. Die aus der imperativen Programmierung
geläufigen Kontrollstrukturen wie |for| oder |while| gibt es in Haskell
(zunächst) nicht. Aber Funktionen höherer Ordnung und Rekursion erlauben
uns den "Selbstbau" von Funktionen, die Kontrollstrukturen ersetzen. 
Hier wollen wir das (im Prelude definierte ) | until | verwenden:

< until :: (a -> Bool) -> (a -> a) -> a -> a
< until p f x = if p x then x else until p f ( f x)

|until P f x| gibt das erste Element der Folge
| x, f x, f (f x), ...| zurück, das das Prädikat |P| erfüllt.

Für negative x schreiben wir dann einfach:

< floor x = until (`leq` x) (subtract 1) (-1) where
<              m `leq` x = fromInteger m <= x

- wir benutzen subtract, weil (-1) keine section ist.
- warum |`leq`| statt |(<=)|? Weil |(<=)| den falschen Typ hat:  
    | (<=)  :: Num a => a -> a -> Bool  |
    | leq   :: Integer -> Float -> Bool |

Wir können uns die Definition von leq auch sparen, allerdings
auf Kosten der Klarheit des ersten Arguments von until::

< floor x = until ((<= x) . fromInteger) (subtract 1) (-1)

Im Englischen nennt man so etwas "to inline a definition".

Für positive x gehen wir analog vor: wir starten bei 1 und addieren solange 
1 bis wir "über" |x| sind und ziehen dann 1 ab.

Zusammen:

> floor' x = if x < 0
>            then until (`leq` x) (subtract 1) (-1)
>            else until (x `lt`) (+1) 1 - 1
>            where
>              m `leq` x = fromInteger m <= x
>              x `lt`  n = x < fromInteger n

Problem: Diese Implementation ist zu langsam.

Besser: Binärsuche - Finde zuerst |(m,n)| mit | m <= x < n | und 
        "halbiere" das Interval (wobei | x | natürlich immer drin 
        bleiben muss), bis | m+1 = n | ist

Wir können den Algorithmus schon einmal hinschreiben, bevor wir
uns um die Implementation der "Zutaten" (|shrink| und |bound|)
kümmern. Dieser Top-Down-Ansatz hilft, das Programmierproblem 
in übersichtliche Schritte zu zerlegen.

> floor'' :: Float -> Integer
> floor'' x = fst ( until unit (shrink x) (bound x))
>             where unit (m,n) = (m+1) == n

shrink soll "das Interval verkleinern". Wir definieren ein
Typsynonym

> type Interval = (Integer, Integer)

und können eine aussagekräftige Typdeklaration für |shrink| geben:

> shrink :: Float -> Interval -> Interval

Wir dürfen davon ausgehen, dass shrink nur Argumente |x| und |(m,n)|
bekommt, für die |m <= x < n| und |m+1 < n| gelten. Das Ergebnis 
|(m',n') = shrink x (m,n)| soll dann zwei Bedingungen erfüllen:
 
  1. | m' <= x < n'      |
  2. | m' - n'  <  m - n |

Bei der Implementation kümmern wir uns zunächst um die erste Bedingung

> shrink x (m,n)  = if (fromInteger p <= x) then (p,n) else (m,p) 
>                   where p = choose (m,n)

Egal, wie wir |choose| implementieren, wird (unter den angegebenen Bedingungen 
an die Argumente) dann 1. erfüllt. 

Da |shrink| jeweils eine Intervalgrenze unverändert lässt, ist 2 genau dann erfüllt, wenn gilt: 

  2'. | m < choose (m,n) < n |

|choose (m,n)| könnte einfach |m+1| oder |n-1| sein, dann würden wir
aber einen ähnlich langsamen Algorithmus erhalten wie |floor'| oben.
Besser ist es, möglichst "in die Mitte" zu gehen:

> choose :: Interval -> Integer
> choose (m,n) = (m+n) `div` 2

Zeigen wir 2'. für diese Implementation: Wir setzen |m+1 < n| voraus
und benutzen 

  3. für alle |x,y :: Integer| gilt:
     | (x `div` y) * y + (x `mod` y)  == x |

| m < choose (m,n) < n |

 <=> { Definition choose }

| m < (m + n) `div` 2 < n |
 
<=> { Arithmetik: (*2) }

| m*2 < ((m + n) `div` 2) * 2 < n*2 |

<=> { 3) }

| m*2 < (m + n) - ((m + n) `mod` 2) < n*2 |

<=> { Arithmetik }

| m < n - ((m + n) `mod` 2)   und     m - ((m + n) `mod` 2) < n |

<=> { da 0 <= ((m + n) `mod` 2) <= 1 }

| m + 1 < n    und     m < n |

<=> { Arithmetik }

| m + 1 < n |


Die Implementation von |shrink| erfüllt damit die Bedingungen.

|bound| teilen wir noch einmal in die Suche einer unteren
und einer oberen Schranke auf, die wir dann durch rekursives 
Verdoppeln von (-1) bzw. 1 implementieren:

> bound :: Float -> Interval
> bound x = (lower x, upper x)

> lower :: Float -> Integer
> lower x = until ( (<=x) . fromInteger ) (*2) (-1)
>
> upper :: Float -> Integer
> upper x = until ( (x<)  . fromInteger ) (*2) 1


Die einzige Bedingung an |bound|, nämlich
  
  | bound x = (m,n)  =>  m <= x < n  |

ist für diese Implementation unmittelbar klar.