Lösung Blatt 2 - lhs

Dateiinhalt

\documentclass{article}
%include lhs2TeX.fmt
%include polycode.fmt
\usepackage[ngerman]{babel}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{fullpage}
\setlength{\parindent}{0pt}
\begin{document}

\setcounter{section}{1}
\section{ Einfache Typen }

\begin{code}
module Uebung2 where
import Prelude hiding (div, subtract)
\end{code}

Wir definieren noch einmal den Datentypen |Nat| und die Konversionen von und nach |Int|:
\begin{code}
data Nat = O | S Nat deriving (Show, Eq)
\end{code}

\begin{code}
intToNat	:: Int -> Nat
intToNat 0	= (O)
intToNat n	= S ( intToNat (n-1) ) 
\end{code}

\begin{code}
natToInt	:: Nat -> Int
natToInt O	= 0
natToInt (S n)	= 1 + ( natToInt n )
\end{code}

\subsection{Datentypen und Operationen}

\begin{enumerate}

	\item Definieren Sie eine Funktion |intToNatg| analog zu |intToNat| unter Benutzung 
        von guards. Stellen Sie sicher, dass |intToNatg| bei Eingabe einer negativen 
        Zahl eine Fehlermeldung ausgibt. (1pt)
\begin{code}
intToNatg :: Int -> Nat
intToNatg n | n  < 0 = error "Negative integer is undefined for intToNatg"
            | n == 0 = O
            | n  > 0 = S $ intToNatg $ n-1
\end{code}

	\item Definieren Sie die Subtraktion und die (ganzzahlige) Division 
        |subtract, div :: Nat -> Nat -> Nat| so, dass für endliche Elemente |n,m :: Nat| 
        (endliche Elemente sind |O, S O, S (S O),...|) folgende Eigenschaften gelten:
        \begin{enumerate}
         \item |subtract (n+m) n = m |
         \item |div (n*m) n = m|
         \end{enumerate}
        Beweisen Sie diese Eigenschaften! (3pt)

Lösung von HG:

\begin{code}
natPred :: Nat -> Nat
natPred O     = undefined
natPred (S n) = n

subtract :: Nat -> Nat -> Nat
subtract z n | n == O    = z
             | z == O    = undefined
             | otherwise = subtract (natPred z) (natPred n)

div :: Nat -> Nat -> Nat
div z n | n == O    = undefined
        | z == O    = O
        | otherwise = S $ div (subtract z n) n
\end{code}

\begin{quote}
-- Assume |n = O| \\
subtract (O+m) O \\
= {def subtract} \\
(O+m) \\
= {def addition} \\
m \\
\\
-- Assume |n > O| \\
subtract (n+m) n \\
= {def subtract} \\
subtract (natPred (n+m) (natPred n) \\
= {def natPred, n = 1 + n'} \\
subtract (n'+m) n' \\
= {Induction} \\
subtract (O+m) O \\
= {see assumption for n = O} \\
m \\
\\
\\
Die zweite Eigenschaft |(div (n*m) n = m)| kann nicht bewiesen werden,
da sie den Regeln der Division widerspricht. Für n = 0 wäre |div (0*m) 0 = m|
zu beweisen, wobei die Regeln der Division bereits |div _ 0 = undefined|
festlegen. Die Aufgabe ist also nicht lösbar, wenn sowohl die Regeln
der ganzzahligen Division als auch die geforderte Eigenschaft gelten
sollen.
\end{quote}
  \item Viele Funktionen auf dem Datentyp |Nat| kann man durch folgendes Rekursionsprinzip 
        definieren:

\begin{code}
foldNat :: a -> (a -> a) -> Nat -> a
foldNat start next O     = start
foldNat start next (S n) = next ( foldNat start next n)
\end{code}

        Es ist z.B. |id = foldNat O S| und | natToInt = foldNat 0 (+1) |. Definieren Sie 
        Funktionen | isEven |, die für gerade Zahlen |True| und sonst |False| zurückgibt, 
        und |isZero|, die für |O| |True| und sonst |False| zurückgibt, mit Hilfe von 
        |foldNat| (2pt):

\begin{code}
isEven :: Nat -> Bool
isEven = foldNat True not

isZero :: Nat -> Bool
isZero = foldNat True (&&False)
\end{code}

	\item{Vervollständigen Sie die Definition der Implikation: (1pt)

\begin{code}
implies :: Bool -> Bool -> Bool
True  `implies` x  = x
False `implies` _  = True
\end{code}}


\item Beweisen Sie, dass |Jane| und |Dick| verschiedene Typen sind, indem Sie zeigen, dass
      |j2j| nicht die identische Funktion auf |Jane| ist! Definieren Sie dazu eine Funktion 
      |test :: Jane -> Bool| und geben Sie |t :: Jane| so an, dass |test| sich auf |t| 
      anders verhält als auf |j2j t|.(1pt)
        
\begin{code}
data    Jane   = MkJane Int deriving Show
newtype Dick   = MkDick Int deriving Show

j2d :: Jane -> Dick
j2d (MkJane x) = (MkDick x)

d2j :: Dick -> Jane
d2j (MkDick x) = (MkJane x)

j2j :: Jane -> Jane
j2j            = d2j . j2d

test :: Jane -> Bool
test (MkJane _) = False
\end{code}
\end{enumerate}

( t = undefined )

\subsection{Strictness}
\begin{enumerate}
\addtocounter{enumi}{5}
\item Im Seminar hatten wir die boolschen Operatoren |and| und |or| strikt in einer, aber 
      nicht-strikt in der anderen Komponente definiert. Kann man |and| und |or| auch strikt 
      in beiden Argumenten definieren? Falls ja, implementieren Sie diese, falls nein, 
      begründen Sie!(1pt)

\begin{code}

and' :: Bool -> Bool -> Bool

and' True False = False
and' True True = True
and' False True = False
and' False False = False


\end{code}
or' folgt analog

\item Kann man eine nicht-strikte Funktion |not'| definieren, die sich auf True und False wie 
      |not| verhält? Begründen Sie! (1pt)


Funktion soll sich auf True und False unterschiedlich verhalten, muss also ihr Argument 
auswerten. Ist das Argument undefined, kann dann nur undefined zurückgegeben werden.

\end{enumerate}

\subsection{Tupels und Either}

Wir hatten die folgenden Gesetze:\\
1)   |fst . pair (f, g)        =  f|\\
2)   |snd . pair (f, g)        =  g|\\
3)   |pair (f, g) . h          =  pair (f.h,g.h)|\\
4)   |cross (f,g) . pair (h,k) =  pair (f.h,g.k)|\\
i)   |scase (f,g) . Left       = f|\\
ii)  |scase (f,g) . Right      = g|\\
iii) |h . scase (f,g)          = scase (h.f,h.g)|\\
iv)  |scase (f,g) . plus(h,k)  = scase (f.h,g.k)|

\begin{enumerate}
\addtocounter{enumi}{7}

\item  Beweisen Sie iv) unter Benutzung von i)-iii) ( analog zum Beweis von 4) im letzten 
       Seminar).(1pt)

Lösung von HG:

\begin{quote}
scase(f,g) . plus(h,k) \\
= {def plus} \\
scase(f,g) . scase(Left.h,Right.k) \\
= { iii) } \\
scase(scase(f,g).Left.h,scase(f,g).Right.k) \\
= { i) ii) } \\
scase(f.h,g.k)
\end{quote}

\item Beweisen Sie |cross(f,g) . cross(h,k) = cross (f.h,g.k)|. (2pt)

Lösung von HG:

\begin{quote}
cross(f,g) . cross(h,k) \\
= { def cross } \\
pair(f.fst,g.snd) . pair(h.fst,k.snd) \\
= { 3) } \\
pair(f.fst.pair(h.fst,k.snd),g.snd.pair(h.fst,k.snd)) \\
= { 1) 2) } \\
pair(f.h.fst,g.k.snd) \\
= { def cross reverse } \\
cross(f.h,g.k)
\end{quote}

\item Schreiben Sie eine Funktion |testEither :: Either Bool Char -> a| in einen geeigneten 
      Typen |a|, die sich auf |Left undefined|, |Right undefined| und |undefined| 
      unterschiedlich verhält! (1pt)

\begin{code}

testEither :: (Either Bool Char) -> Bool
testEither (Left _)  = True
testEither (Right _) = False

\end{code}


\item Ein Datum kann durch ein Tripel (Jahr,Monat,Tag) angegeben werden. Wir definieren das 
      Typsynonym

\begin{code}
type Date = (Int,Int,Int)
\end{code}

      Implementieren Sie eine Funktion |age:: Date -> Date -> Int| so, dass 
      |age birthday current| das Alter einer Person angibt, wenn |birthday| der Geburtstag 
      der Person und |current| das aktuelle Datum ist. (2pt)

\begin{code}

age :: Date -> Date -> Int
age (by,bm,bd) (cy,cm,cd) 
  | (bm>cm) || ((bm==cm) &&(bd>cd)) = cy - by - 1
  | otherwise                       = cy - by


\end{code}

\end{enumerate}

\subsection{Fibonacci}

\begin{enumerate}
\addtocounter{enumi}{11}

\item Implementieren Sie eine Funktion |fib :: Int -> Integer|, sodass |(fib n)| das 
      $n$-te Glied der Fibonacci-Folge ist: es sei |fib 0 = 0|, |fib 1 = 1| und für alle 
      endlichen (auch negativen!) |n::Int| gelte\\ |fib n = fib (n-1) + fib (n-2)| . (2pt)

\begin{code}

fib :: Int -> Integer
fib n
  | n == 0  = 0
  | n == 1  = 1
  | n > 1   = (fib (n-1)) + (fib (n-2))
  | n < 0   = (fib (n+2)) - (fib (n+1)) 


fibS :: [Integer]
fibS = 1:0:zipWith (-) fibS (tail(fibS))


\end{code}


\end{enumerate}
\end{document}