Lösung Blatt 3 - lhs

Dateiinhalt

\documentclass{article}
%include lhs2TeX.fmt
%include polycode.fmt
\usepackage[ngerman]{babel}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{fullpage}
\usepackage{url}
\setlength{\parindent}{0pt}
\begin{document}
\begin{verbatim}
----------------------------------------------------------------------
--
--  Seminar Theoretische Informatik                         \ \
--  "Funktionale Programmierung mit Haskell"                 \ \ ---
--  Universität Potsdam SS 2014                              / /\ --
--  Tim Richter / Mario Frank                               / /  \
--
-- Übungsblatt 3 (Listen)
-- Abgabe bis: 28.05.2014, 23:59
-- Name: Muster
-- Erreichte Punkte:      / 15
----------------------------------------------------------------------
\end{verbatim}

> module Uebung3 where
> import Prelude
> 
> data Nat = O | S Nat deriving (Show)
> 
> intToNat	:: Int -> Nat
> intToNat n
> 	| (n < 0)   = undefined
> 	| (n == 0)  = O
> 	| otherwise = S ( intToNat (n-1) )
> 
> natToInt	:: Nat -> Int
> natToInt O	= 0
> natToInt (S n)	= 1 + ( natToInt n )

\section{Vorbemerkung}

Beweise sind stets im Stil des ''equational reasoning'', wie es im Buch
eingeführt wird, zu führen. Insbesondere ist für \textbf{jede} Gleichung
in geschweiften Klammern hinter dem Gleichheitszeichen eine Begründung anzugeben.
Abweichung von dieser Form führt zu Punktverlust!

\section{Listenoperationen (1+2+2+2 pt)}

\subsection{Last}

Gegeben seien die folgenden Definitionen für die Funktion,
die das letzte Element einer Liste zurückgibt:

> last' (x:xs) = if null xs then x else last' xs
> last'' (x:xs) = if xs == [] then x else last'' xs

Der Unterschied zwischen |last'| und |last''| besteht darin, dass sich die
Typen unterscheiden.

> last' :: [a] -> a
> last'' :: (Eq a) => [a] -> a

Die Typ der Funktion |last''| beschränkt die Eingabe auf Listen von
Elementen, die zum Typ |Eq| gehören.

Geben Sie einen Ausdruck |n| an, auf dem sich |last'| und |last''| unterschiedlich
verhalten. (1 pt)

\subsubsection{Lösung}

> n :: [Nat]
> n = [O]
> -- last'  n = O
> -- last'' n   resultiert in Fehlermeldung, da Nat nicht zur Typklasse Eq gehört

\subsection{Verkettung}
Beweisen Sie, dass folgende Gleichung gilt: (2 pt)

\textbf{concat (xss ++ yss) = concat xss ++ concat yss}\\

\noindent concat ist dabei als |foldr (++) []| und (++) durch Rekursion über das erste 
Argument definiert (siehe Prelude). Schreiben Sie diese Definitionen aus und 
geben Sie den einzelnen Regeln Label, um im Beweis auf sie referenzieren zu können!\\

\subsubsection{Lösung}
Wir haben für beliebige Listen von Listen |xss| und |yss| zu zeigen:

< concat (xss ++ yss) = concat xss ++ concat yss

Wir schreiben die Definitionen von |(++)|, |concat| und |foldr| auf und geben
jeder Regel ein Label: 

< (++) :: [a] -> [a] -> [a]
< [] ++ ys = ys                                 { Def (++)_[]   }
< (x:xs) ++ ys = x:(xs ++ ys)                   { Def (++)_(:)  }
<
<
< concat :: [[a]] -> [a]
< concat = foldr (++) []                        { Def concat    }
<
<
< foldr :: (a -> b -> b) -> b -> [a] -> b
< foldr op e []      = e                        { Def foldr_[]  }
< foldr op e (x:xs)  = x `op` (foldr op e xs)   { Def foldr_(:) }

Wir führen den Beweis durch Listen-Induktion nach |xss|. In jedem der drei
Fälle zeigen wir, dass linke Seite (LHS) und rechte Seite (RHS) der zu beweisenden 
Gleichung zum selben Term reduzieren:

Fall |xss = undefined|

< LHS:
< concat (undefined ++ yss)
< = { pattern exhaustion (++)} 
< concat undefined
< = { Def concat }
< foldr (++) [] undefined
< = { pattern exhaustion foldr}
< undefined
<
< RHS:
< concat undefined ++ concat yss
< = { pattern exhaustion concat }
< undefined ++ concat yss
< = { pattern exhaustion (++) }
< undefined
	
Fall: |xss = []|

< LHS:
< concat ([] ++ yss)
< = {Def (++)_[]}
< concat yss
	
< RHS:
< concat [] ++ concat yss
< = { Def concat }
< ( foldr (++) [] [] ) ++ concat yss
< = { Def foldr_[] }
< [] ++ concat yss
< = { Def (++)_[] }
< concat yss
	
Fall |xss = (xs:xss')|

< LHS:
< concat ( (xs:xss') ++ yss )
< = { Def (++)_(:) }
< concat ( xs:(xss' ++ yss) )
< = { Def concat }
< foldr (++) [] ( xs:( xss' ++ yss ) )
< = { Def foldr_(:) }
< xs ++ ( foldr (++) [] (xss' ++ yss))
< = { Def concat }
< xs ++ concat (xss' ++ yss)


< RHS:
< concat (xs:xss') ++ concat yss
< = { Def concat }
< foldr (++) [] (xs:xss') ++ concat yss
< = { Def foldr_(:) }
< xs ++ foldr (++) [] (xss') ++ concat yss
< = { Def concat }
< xs ++ concat xss' ++ concat yss
< = { Induktionsvoraussetzung }
< xs ++ concat (xss' ++ yss)

\subsection{Halbieren einer Liste}
Definieren Sie eine Funktion 

> splitHalf :: [a] -> (([a],[a]), Maybe a)

die eine Liste ''in der Mitte teilt'': Ist |splitHalf as = ((bs,cs), m)|, so 
sollen die Listen bs und cs gleich lang sein und es soll, falls |m = Just a| ist, 
|as = bs ++ [a] ++ cs| und sonst |as = bs ++ cs| gelten. (2 pt)

\subsubsection{Lösung}

> splitHalf list 
> -- Fall even (gerade Länge)
> 	       | even (length list) = ((left, right), Nothing)
> -- Fall odd (ungerade Länge)
> 	       | odd  (length list) = ((left, tail right), Just (head right))
> -- Splitting der Liste 
>                where (left, right) = splitAt ((length list) `div` 2) list
>
> testSplit1 = "splitHalf [1]                = " ++ show (splitHalf [1])
> testSplit2 = "splitHalf [1, 2, 3, 4, 5]    = " ++ show (splitHalf [1, 2, 3, 4, 5])
> testSplit3 = "splitHalf [1, 2, 3, 4, 5, 6] = " ++ show (splitHalf [1, 2, 3, 4, 5, 6])

\subsection{Bedingtes Umkehren einer Liste}

Definieren Sie eine Funktion |revEven :: [a] -> [a]|, die alle Listen gerader Länge 
umkehrt und alle anderen Listen unverändert lässt. Benutzen Sie |splitHalf| und 
''pattern guards'' (siehe \url{http://www.haskell.org/haskellwiki/Pattern_guard}). 
Verwenden Sie weder |where| noch |let|! (2 pt)

\subsubsection{Lösung}

> revEven :: [a] -> [a]
> revEven list 
>   | Just a  <- (snd (splitHalf list)) = list
>   | Nothing <- (snd (splitHalf list)) = reverse list
> 
> revEvenTest1 = "revEven [1,2,3,4,5] = " ++ show (revEven [1,2,3,4,5])
> revEvenTest2 = "revEven [1,2,3,4]   = " ++ show (revEven [1,2,3,4])


\section{Map und Filter (4+1 pt)}

\subsection{Map}

\begin{enumerate}
 \item Geben Sie den Typen von map map an! (1 pt)
 \item Beweisen Sie, dass folgende Gleichungen gelten:\\
\textbf{map f (xs ++ ys) = map f xs ++ map f ys} (1 pt)\\
\textbf{map f . concat = concat . map (map f)} (2 pt)\\
        
Führen Sie den Beweis der zweiten Gleichung, indem Sie unter Benutzung 
der ersten Gleichung und geeigneter Gesetze zeigen, dass beide Seiten 
sich als dieselbe |foldr|-Instanz schreiben lassen.
\end{enumerate}

\subsubsection{Lösung (1)}

< -- :type map
< map :: (a -> b) -> [a] -> [b]
< -- :type map map
< map map :: [a -> b] -> [[a] -> [b]]

\subsubsection{Lösung (2.1)}

Zu zeigen ist: Für beliebige Typen |a| und |b|, eine Abbildung
|f :: a -> b| und Listen |xs::[a]| und |ys::[a]| gilt:

< map f (xs ++ ys) = map f xs ++ map f ys

Wir verwenden die Definitionen und Label von oben und zusätzlich

< map :: (a -> b) -> [a] -> [b]
< map f []     = []               { Def map_[]  }  
< map f (x:xs) = f x : map f xs   { Def map_(:) }

Beweis per Induktion über |xs|. 

Fall |xs = undefined|

< map f (undefined ++ ys)
< = { pattern exhaustion (++) }
< map f (undefined)
< = { pattern exhaustion map }
< undefined
< = { pattern exhaustion (++) }
< undefined ++ map f ys
< = { pattern exhaustion map }
< map f undefined ++ map f ys
	
Fall |xs = []|

< map f ([] ++ ys)
< = { Def (++)_[] }
< map f ys
< = { Def (++)_[] }
< [] ++ map f ys
< = { Def map_[] }
< map f [] ++ map f ys
	
Fall |xs = (x:xs')|

< map f ((x:xs') ++ ys)
< = { Def (++)_(:) }
< map f (x:(xs' ++ ys))
< = { Def map_(:) }
< (f x) : (map f (xs' ++ ys))
< = { Induktionsvoraussetzung }
< (f x) : (map f xs' ++ map f ys)
< = { Def (++)_(:) }	
< ((f x) : (map f xs')) ++ map f ys
< = { Def map_(:) }
< map f (x:xs') ++ map f ys

\subsubsection{Lösung (2.2)}

Zu zeigen ist, dass für beliebige Typen |a| und |b| und eine beliebige 
Abbildung |f: a-> b| folgende Gleichheit (von Funktionen vom Typ 
|[[a]] -> [b]|) gilt:

< (map f) . concat = concat . (map (map f))

Wir führen den Beweis, indem wir zeigen, dass beide Seiten
der Gleichung gleich |foldr ((++).(map f)) []| sind. Für die
rechte Seite folgt dies aus dem Fold-Map-Fusion Theorem:

Für beliebige Typen |c|, |d|, |e|, Abbildungen |g :: c -> d|, 
|h :: d -> e -> e| und ein beliebiges Element |x :: e| gilt folgende
Gleichheit (von Funktionen vom Typ | [c] -> e |):

< (foldr h x) . map g = foldr (h . g) x             { fold-map-fusion }

< RHS:
< concat . (map (map f))
< = { Def concat }
< (foldr (++) []) . (map (map f))
< = { fold-map-fusion mit |c = [a]|, |d = e = [b]|, 
<     |g = map f|, |h = (++)|, |x = []| }
< foldr ((++).(map f)) []

Für die linke Seite benutzen wir das Fusion Theorem für foldr:

Sind für beliebige Typen |c|, |d|, |e|, Abbildungen | g :: d -> e |, 
|h :: c -> d -> d|, | k :: c -> e -> e | und Elemente |x::d|, |y::e| folgende
Eigenschaften erfüllt:

< g undefined = undefined   -- d.h. g ist strikt   { prop 1 }
< g x = y                                          { prop 2 }

und für alle |x'::c| und |y'::d|

< g ( h x' y') = k x' (g y')                       { prop 3 }

so gilt folgende Gleichheit (von Funktionen vom Typ |[c] -> e|)

< g . foldr h x = foldr k y                        { foldr-fusion }

Damit können wir

< LHS:
< (map f) . concat
< = { Def concat }
< (map f) . (foldr (++) [])
< = { foldr-fusion mit |c = d = [a]|, |e = [b]|, 
<     |g = map f|, | h = (++) |, | k = (++) . (map f) |,
<     |x = []|, |y = []| }
< foldr ((++).(map f) []

schliessen, wenn wir die Eigenschaften |{ prop 1 }| bis |{ prop 3 }| für diese Wahl von
|g|, |h|, |k|, |x| und |y| beweisen können. Zu zeigen bleiben also

< map f undefined = undefined 
< map f [] = [] 

und |{ prop 3 }|: für beliebige |xs, ys :: [a]| gilt

< (map f) ( xs ++ ys) = ((++) . (map f)) xs (map f ys)

Die ersten beiden Eigenschaften folgen jeweils in einem Schritt mittels pattern
exhaustion für map und |{ Def map_[] }|. Für |{ prop 3 }| schliessen wir wie folgt:

< ((++) . (map f)) xs (map f ys)
< = { Definition (.): (l . m) z = l ( m z ) }
< ((++) ( map f xs )) (map f ys)
< = { Teilaufgabe 1 }
< (map f) ( xs ++ ys )


\subsection{Filter (1 pt)}

Die Prelude-Funktion |filter :: (a -> Bool) -> [a] -> [a]| kann mit Hilfe von 
concat und map konstruiert werden:

< filter' p = concat . map box
< 		where box x = undefined

Vervollständigen Sie die Definition für |box|. (1 pt)


\subsubsection{Lösung}

> filter' :: (a -> Bool) -> [a] -> [a]
> filter' p = concat . map (box p)
>   where box p x = if p x then [x] else []
> 
> testFilter1 = "filter' even [1,2,3,4,5,6] = " ++ show (filter' even [1,2,3,4,5,6])


\section{Folds (3 pt)}

Die Funktionen |takeWhile| und |dropWhile| sind den Funktionen take und drop 
ähnlich. Statt eines Int-Indexes nehmen sie jedoch einen Boole'schen Ausdruck als
ersten Parameter. Das Ergebnis von

\textbf{takeWhile p xs}

ist das längste Initial-Segment von |xs|, dessen Elemente sämtlich die Bedingung 
|p| erfüllen. Zum Beispiel ist

\textbf{takeWhile even [2,4,7,4,1,6] = [2,4]}

\begin{enumerate}
	\item Definieren Sie |filter p| als Instanz von |foldr|! (1 pt)
	\item Definieren Sie |takeWhile| als Instanz von |foldr|! (1 pt)
	\item Kann |dropWhile| als Instanz einer Fold-Funktion definiert werden? 
        Implementieren oder begründen Sie! (1 pt)
\end{enumerate}

\subsubsection{Lösung (1)}

> filter'' p = foldr check [] 
>   where check = \x -> if p x then (x:) else id
>   
> testFilter2 = "filter'' even [1,2,3,4,5,6] = " ++ show (filter'' even [1,2,3,4,5,6])

\subsubsection{Lösung (2)}

> takeWhile' p = foldr app []
>   where app x y = if p x then x : y else []
> 
> testTakeWhile1 = "takeWhile' even [2,6,8,1,6,7] = " ++ show (takeWhile' even [2,6,8,1,6,7])
> testTakeWhile2 = "takeWhile' odd [1,7,3,2,4,6,7] = " ++ show (takeWhile' odd [1,7,3,2,4,6,7])

\subsubsection{Lösung (3) - HG}

|dropWhile p| kann nicht als Instanz einer Fold-Funktion definiert werden,
da Fold-Funktionen nur auf dem aktuellen Element und einer einseitig
abgearbeiteten Liste arbeiten. Wenn die Liste vom Beginn abgearbeitet
wird, so müsste der Operator einer Fold-Funktion (die Funktion, die
Fold übergeben wird) seine Überprüfung, ob ein Element |x| die Eigenschaft
|p| erfüllt, einstellen, sobald ein erstes Element die Eigenschaft |p| nicht
erfüllt und somit Folgelemente nur noch an die Ergebnisliste anhängen.
Da Haskell zustandslos arbeitet kann ein Operator diese Funktion nicht
erfüllen.
Wenn die Liste vom Ende abgearbeitet wird, so kann der Operator nicht
einmal feststellen, ob er gerade auf einem Element arbeitet, das zu
einer kommenden Gruppe von aufeinanderfolgenden Elementen gehört, die
die Eigenschaft p erfüllen. Er kann somit nicht erkennen, ob er bereits
auf einem fallenzulassenden Element arbeitet oder nicht.

\section{Hyperoperationen (just for fun)}

\noindent
Ausgehend von der Beobachtung, dass Multiplikation ''iterierte Addition''
und Potenzieren ''iteriertes Multiplizieren'' ist, definiert man die Folge der 
\textbf{Hyperoperation} (siehe Wikipedia: 
\url{http://en.wikipedia.org/wiki/Hyperoperation}). 
Definieren Sie unter Verwendung von |foldr1| und |foldNat| 

> foldNat :: a -> (a -> a) -> Nat -> a
> foldNat s f O     = s
> foldNat s f (S m) = f ( foldNat s f m )

eine Funktion

> hop :: Nat -> Integer -> Integer -> Integer

derart, dass | a `hop n` b | für |b >= 1| das Ergebnis der Anwendung der 
(n+1)ten (sic!) Hyperoperation auf das Paar |(a,b)| ist! Für |b < 1| darf 
die Funktion undefiniert sein.

\subsubsection{Lösung}

> hop = foldNat (+) (\op -> (\a b -> foldr1 op (take (fromInteger b) (repeat a))))

> testHop1  = "hop       (S O)   0 0 =(0)=  " ++ show (hop       (S O)   0 1)
> testHop2  = "hop          O    2 3 =(5)=  " ++ show (hop          O    2 3)
> testHop3  = "hop       (S O)   2 3 =(6)=  " ++ show (hop       (S O)   2 3)
> testHop4  = "hop    (S (S O))  2 3 =(8)=  " ++ show (hop    (S (S O))  2 3)
> testHop5  = "hop (S (S (S O))) 2 3 =(16)= " ++ show (hop (S (S (S O))) 2 3)

\section{Tests}

> testAll = sequence_ (map putStrLn [
>     testSplit1, testSplit2, testSplit3,
>     revEvenTest1, revEvenTest2,
>     testFilter1, testFilter2,
>     testTakeWhile1, testTakeWhile2,
>     testHop1, testHop2, testHop3, testHop4, testHop5
>     ])

\end{document}