Bws bzgl. Fkt. über allg. Datentypen
------------------------------------
Strukturelle Induktion
Beweistechnik: Wenn A ein alg. Datentyp mit Kontstruktoren K_1 K_T ist, dann kann eine Aussage P
zu Elementen des Datentyp A bewiesen werden, indem eine Fallunterscheidung vorgenommen wird.
Zeige P für ELemente der Form K_1...,
zeige P für ELemente der Form K_o
wobei für rek. Konstruktoren die Eigenschaft P für allg. Ag. Des Types A vorrausgesetzt werden kann.
-- fallunterscheidung mit cases
-- case ausdruck = true, dann gleichung einsetzen, alle anderen cases als false
Binärbäume: Bws.:
data Tree a = Nil | Node a (Tree a) (Tree a)
collapse Nil = []
collapse (Node x t1 t2) = collapse t1 ++ [x] ++ collapse t2
mapTree f Nil = Nil
mapTree f (Node x t1 t2) = Node (f x) (mapTree f t1) (mapTree f t2)
map f [] = []
map f (x:xs) = fx:(map f xs)
Satz: collapse (mapTree f t) = map f (collapse t) für alle
f :: a -> b und t :: Tree a
Bws: -- strukt. Ind über aufbau von t
Nil - Fall:
collapse (mapTree f Nil) = collapse Nil (mapTree.1)
map f (collapse Nil) = map f [] (collapse.1)
= [] (map.1)
Node - Fall: I.V.
collapse (mapTree f t1) = map f (collapse t1) und ... für t2
collapse (mapTree f (Node x t1 t2) =
collapse (Node (f x) (mapTree f t1) (mapTree f t2)) (mapTree.2) -- t1 links t2 rechts
collapse (mapTree f t1) ++ [f x] ++ collapse (mapTree f t2) (collapse.2)
map f (collapse t1) ++ [f x] ++ map f (collapse t2) (I.V. 2mal)
map f (collapse (Node x t1 t2)) = map f (collapse t1 ++ [x] ++ collapse t2) -- struktur vergl. (oben)
Lemma: (map++): map f (xs ++ ys) = map f xs ++ map f ys
Bws: Übung
Also: = map f (collapse t1) ++ [f x] ++ map f (collapse t2) (map++ 2mal, map.1, map.2) q.e.d
Huffmann - Kodierung:
--------------------
Vorspann: Modulasierung
-- jede komponente in module packen, schnittstellen festlegen, module untereinander export/import
-- arbeitsteilig, jedes modul von einem anderen team
-- änderungen nicht auf gesamtsystem, also nur lokal pro modul ohne das es effekte auf gesamt hat
Ant.hs:
module Ant where
data Ants = BlackAnt | RedAnt
deriving (show, EQ)
ant1 = BlackAnt
ant2 = RedAnt
antEater = "Bear"
...
f x =
Bee.hs:
module Bee where
import Ant
...
ant3 = ant1
beeKeeper = "Fred"
...
Cow.hs
module Cow where
import Bee
.
... beeKeeper
-- kein import von Ant!
Export - Vereinbarungen:
------------------------
-- in klammern das was nach aussen gegeben werden soll, hilfsfkt usw, liste der namen die export sollen
-- bei import ant werden nur die dinge importiert aus klammern
module Ant ( Ants (..), antEater) -- (..) -> alle Konstrutoren, nur der Datentyp Ant und anEater wird exportiert.
module Bee (module Ant, module Bee) -- alle Def. aus Ant und Bee
import - Vereinbarungen:
------------------------
import Ant (antEater, f)
import Ant hiding (f)
qualifizierter import:
----------------------
-- namensräume kollidieren, bsp: map, mapTree.
-- namensraum struktorieren, namen des modules vor den namen seiner funktion
import qualified Ant
ant3 = Ant.ant1
import qualified Ant as A
ant1 .. -- neu definieren
ant3 = A.ant1
Huffmann:
-- Strings durch Binärfolgen codieren
-- codierung für c ist kein prefix einer Kodierung von c'
-- ein zeichen wird durch seinen pfad im baum kodiert
-- wenn zeichen nur in den blättern stehen gibt es immer nur ein weg, pfad = 0 1 für links rechts, left right
-- t wird durch L kodiert (Left)
-- a wird durch RL kodiert (rechts links)
-- b wird durch RR kodiert
-- "battat" RRRLLRLL -- string und seine kodierung
-- dekodieren: vorne anfangen: R (kodierung) nein, zweites zeichen RR (ja: b), usw (batt)
-- morse kode ist bsp für huffmann - kodierung:
module Types (Tree (Leaf, Node), Bit (L,R), HCode, Table)) where
data Bit = L | R deriving (EQ, show)
type HCode = [Bit] -- typ synnonynm, als mögliche kodierung
type Table = [(Char, HCode)] -- folge für jedes zeichen, entsprechend Hcode
data Tree = Leaf Char Int | Node Int Tree Tree'
...