# Lösungsvorschlag Formal Methods And Functional Programming FS14: Unterschied zwischen den Versionen

## Assignment 1: Typing

a)

• i. a -> (a -> b) -> b
• ii. (Num a, Ord a) => a -> ([b] -> a -> a) -> Bool

b)

• i. \(x, y) f -> (f x, y)
• ii. \f x -> if x > x then (f [x,x])+1 else (f [x,x,x])+2

(or \f x -> (f [x]) + (\_ -> 1) (x < x) )

c) Let $\Gamma :\equiv x : \tau_1$

                        _____________________Var  _____________Int
$\Gamma\vdash$ x :: $\tau_5 \to (\tau_4, \tau_3)$       $\Gamma\vdash$ 0 :: $\tau_5$
__________________________________________App
$\Gamma\vdash$ (x 0) :: $(\tau_4, \tau_3)$
__________________Var        __________________________snd
$\Gamma\vdash$ x :: $\tau_3 \to \tau_2$                $\Gamma\vdash$ snd (x 0) :: $\tau_3$
______________________________________________________App
$\Gamma\vdash$ x (snd ( x 0)) :: $\tau_2$
______________________________________________________Abs*
$\vdash\lambda$ x.x (snd (x 0)) :: $\tau_0$


Constraints: $\tau_0 = \tau_1 \to \tau_2, \tau_1 = \tau_3 \to \tau_2, \tau_1 = \tau_5 \to (\tau_4, \tau_3), \tau_5$ = Int

Unifying all the constraints, we get $\tau_0 = ($Int$\to (\tau_4,$Int$)) \to (\tau_4,$Int$)$.

Thus the most general type is (Int -> (a, Int)) -> (a, Int).

## Assignment 2: Proof by Induction

Let $P(xs) := \forall f. \forall ys. zipWith (flip~f)~xs~ys = zipWith~f~ys~xs.$ We show $\forall xs. P(xs)$ by induction.

Base Case: We have to show P([]). Let f and ys be arbitrary.

zipWith (flip f) [] ys =               -- zipWith.2
[] =                                   -- zipWith.2
zipWith f ys []

Step case: Let x and xs be arbitrary. We assume P(xs) and show P(x:xs). Let f and ys be arbitrary. We do a case destinction over ys. Case ys = []

zipWith (flip f) (x:xs) [] =            -- zipWith.2
[] =                                    -- zipWith.2
zipWith f [] (x:xs)

Case ys = (a:as)

zipWith (flip f) (x:xs) (a:as) =              -- zipWith.1
((flip f) x a):(zipWith (flip f) xs as) =     -- flip
(f a x):(zipWith (flip f) xs as) =            -- I.H.
(f a x):(zipWith f as xs) =                   -- zipWith.1
zipWith f (a:as) (x:xs)

This completes the proof.

## Assignment 3: Haskell Lists (7 points)

a)

dvdNxt :: [Int] -> [Int]
dvdNxt [] = []
dvdNxt (a:[]) = [a]
dvdNxt (a:b:xs) = if (b mod a) == 0 then a:(dvdNxt (b:xs)) else dvdNxt (b:xs)
dvdNxt :: [Int] -> [Int]
dvdNxt (x:xs)
| xs == []          = [x]
| ((mod) (head xs) x) == 0 = x:(dvdNxt xs)
| otherwise         = dvdNxt xs
dvdNxt :: [Int] -> [Int]
dvdNxt a = [a!!i|i<-[0..length a -2], 0==mod (a!!(i+1)) (a!!i)] ++ lastelem a
where
lastelem a = if (a==[]) then [] else [last a]

b)

stableDN :: [Int] -> [Int]
stableDN list = stableDNHelper list (dvdNxt list)
where
stableDNHelper l1 l2
| l1 == l2  = l1
| otherwise = stableDNHelper l2 (dvdNxt l2) -- l2 = (dvdNxt l1)
stableDN :: [Int] -> [Int]
stableDN x
| x == dvdNxt x     = x
| otherwise         = stableDN (dvdNxt x)

c)

prepend :: String -> [[String]] -> [String]
prepend p l = prependHelper p (concat l)
where
prependHelper p [] = []
prependHelper p (x:xs) = (p++x):(prependHelper p xs)

alternatively an easier way (also works on infinite lists thanks to lazy evaluation):

prepend s = map ((++) s) . concat

list comprehension:

prepend p xs = [p++zs | ys <- xs, zs<-ys]

list comprehension extended:

prepend :: String -> [[String]] -> [String]
prepend s (l:ls)      = [s ++ e | e <- l] ++ prepend s ls
prepend s []          = []

foldr:

prepend :: String -> [[String]] -> [String]
prepend s l = foldr (\x y -> (foldr (\x1 y1 -> (s++x1) : y1) [] x) ++ y) [] l

a)

make a b
| a > b = make b a
| otherwise = V a b

b)

instance (Show a) => Show (Interval a) where
show (V a b) = "[" ++ show a ++ "," ++ show b ++ "]"

c)

intersect :: Ord a => [Interval a] -> Maybe (Interval a)
intersect [] = Nothing
intersect [x] = Just x
intersect xs = foldl1 ov (map (\x -> Just x) xs)
where
ov (Just (V a b)) (Just (V c d)) = if legal newI then Just newI else Nothing
where
newI = V (max a c) (min b d)
legal (V x y) = x < y

Alternative:

intersect :: Ord a => [Interval a] -> Maybe (Interval a)
intersect [] = Nothing
intersect [x] = Just x
intersect xs
| a <= b = Just (V a b)
| otherwise = Nothing
where (V a b) = (foldr (\(V a b) (V c d) -> (V (max a c) (min b d))) (head xs) xs)

Straightforward alternative:

intersect::Ord a => [Interval a] -> Maybe (Interval a)
intersect [] = Nothing
intersect [V l u] = Just (V l u)
intersect ((V l1 u1):(V l2 u2):rest)
| l1 >= l2 && u1 <= u2 && u1 >= l1 = intersect ((V l1 u1):rest)
| l1 >= l2 && u2 <= u1 && u2 >= l1 = intersect ((V l1 u2):rest)
| l2 >= l1 && u1 <= u2 && u1 >= l2 = intersect ((V l2 u1):rest)
| l2 >= l1 && u2 <= u1 && u2 >= l2 = intersect ((V l2 u2):rest)
| otherwise = Nothing

Straightforwarder alternative:

intersect::Ord a => [Interval a] -> Maybe (Interval a)
intersect [] = Nothing
intersect [a] = Just a
intersect ((V l1 u1):(V l2 u2):rest)
| max l1 l2 <= min u1 u2   = intersect ((V (max l1 l2) (min u1 u2)):rest)
| otherwise                = Nothing

Another solution:

intersect :: Ord a => [Interval a] -> Maybe (Interval a)
intersect []  = Nothing
intersect [x] = Just x
intersect xs  = aux (map (\y -> Just y) xs)
where
aux (x:y:zs)
| x == Nothing = Nothing
| zs == []     = doInter x y
| otherwise    = aux ((doInter x y):zs)
doInter (Just a b) (Just c d)
| (max a c) <= (min b d) = Just (V (max a c) (min b d))
| otherwise = Nothing

d)

Create a new module with all the interval definitions and functions. Then we can use an export list to export the functions we want to be available to public. To make it impossible to create illegal intervals, we would export the make function defined earlier, but not the constructor. As our make function automatically fixes attempts to create invalid intervals it's not possible to construct invalid intervals.

## Assignment 5: File System Entries

-- (a)

fFSE :: (String -> [a] -> a) -> (String -> String -> a) -> FSEntry -> a
fFSE foldFolderFunc foldFileFunc (Folder n entries) = foldFolderFunc n (map (\x -> fFSE foldFolderFunc foldFileFunc x) entries)
fFSE foldFolderFunc foldFileFunc (File n c) = foldFileFunc n c

-- (b)

-- i.

number :: FSEntry -> Int
number root = fFSE (\_ y -> (sum y) + 1) (\_ _ -> 1) root

-- alternative i. (easier to comprehend imho)
numberME :: FSEntry -> Int
numberME (File _ _) = 1
numberME (Folder _ b) = foldr (\x e -> e + numberME x) 1 b

-- ii.

count :: Char -> FSEntry -> Int
count ch root = fFSE (\_ y -> (sum y)) (\_ y -> foldr (\c1 c -> if c1 == ch then c+1 else c) 0 y) root

-- alternative ii. with filter
countME c a = fFSE hdir hfile a
where
hdir a d = (sum d)