Lösungsvorschlag Formal Methods And Functional Programming FS11 midterm

Aus VISki
Wechseln zu: Navigation, Suche

Assignment 1

1a)

Prelude> :t \x y z -> (y x, x z)
\x y z -> (y x, x z) :: (t2 -> t1) -> ((t2 -> t1) -> t) -> t2 -> (t, t1)
Prelude> :t \x y -> x (\z -> y)
\x y -> x (\z -> y) :: ((t1 -> t2) -> t) -> t2 -> t
Prelude> :t map (1 :)
map (1 :) :: Num a => [ [a] ] -> [ [a] ]
Prelude Data.List> :t \x ys -> inits (map (x <) ys)
\x ys -> inits (map (x <) ys) :: Ord a => a -> [a] -> [ [Bool] ]

1b)

Let \Gamma =( y:\sigma_1, x:\sigma_2)

                                                                -----------------------------------       ----------------------
                                                                \Gamma |- x :: \sigma_5 -> \sigma_4       \Gamma |- y ::\sigma_5
                                   ------------------------     ----------------------------------------------------------------
                                   \Gamma |- 1 :: \sigma_3      \Gamma |- x y :: \sigma_4
                                   -------------------------------------------------------
                                   \Gamma |- 1 + x y :: \sigma_4
-----------------------------      -------------------------------------------
y:\sigma_1 |- True :: \tau_2       y:\sigma_1 |- \lambda x . 1 + x y :: \tau_3
------------------------------------------------------------------------------
y:\sigma_1 |- (True, \lambda x . 1 + x y) :: \tau_1
------------------------------------------------------------------------------
|- (\lambda y . (True, \lambda x . 1 + x y)) :: \alpha_0

with side conditions

\alpha_0 = \sigma_1 -> \tau_1
\tau_1 = (\tau_2,\tau_3)
\tau_2 = Bool
\tau_3 = \sigma_2 -> \tau_4
\tau_4 = Int
\sigma_3 = Int
\sigma_4 = Int
\sigma_2 = \sigma_5 -> \sigma_4
\sigma_1 = \sigma_5
Num \sigma_3

and thus

\alpha_0 
= \sigma_1 -> \tau_1 
= \sigma_1 -> (\tau_2,\tau_3) 
= \sigma_1 -> (Bool, (\sigma_2->\tau_4)) 
= \sigma_1 -> (Bool, ((\sigma_1 -> \sigma_4) -> Int) 
= \sigma_1 -> (Bool, ((\sigma_1 -> Int) -> Int)

Assignment 2

Let

                                             ------------------------------------------ ax
                                                        
                                               ------------------------------------------  EL
                                                         
-------------------------------------ax     ------------------------------------------  I
                                      
-------------------------------------------------------------------------  E, sc ok, bc x not free in  or 

-------------------------------------------------  I

Assignment 3

3 a)

Variante 1:

 maximumM []     = error "empty list"
 maximumM (l:ls) = helper l ls
   where   
     helper max (l:ls) = if max>l then helper max ls else helper l ls
     helper max []     = max 


Variante 2:

 maximumM2 []     = error "empty list"
 maximumM2 (l:ls) = foldr (\x max-> if x>max then x else max) l (l:ls)


Variante 3:

 maximum' [] = error "empty"
 maximum' (x:xs) = aux x xs
   where
     aux a [] = a
     aux a (x:xs)
       | a < x = aux x xs
       | otherwise = aux a xs


Variante 4:

  maximum4 [] = error "empty list"
  maximum4 xs = head [x | x <- xs, all (x >=) xs]

3 b)

       concatMapM2 f = foldr (\x l -> f x ++ l) []
       concatMapM3 f = foldl (\l x -> l ++ (f x)) []
       concatMapM  f = concat . map f

3 c)

       iter3 f g x y = concat $ ([x,y]):(iterHelp f g [ [x,y] ])
                       where iterHelp f g (l:ls) = next:(iterHelp f g (next:ls))
                                                   where next = [f (head l), g (last l)]
       -- this one does not work, can somebody fix it?
       iter2 f g x y = reverse $ foldl (\(l:ls) _ -> (f (fst l),g (snd l)):(l:ls)) [(x,y)] [1..10]

       iter2 f g x y = [x , y] ++ iter2 f g (f x) (g y)
       -- For better performance use : instead of ++
       iter2 f g x y = x:y:(iter2 f g (fx) (gy))

Assignment 4

To prove: Vxs::[Int]. Vi::Int. sum(addShifted xs i) = i + 2*sum xs

We prove this by induction over xs. Let i be arbitrary.

  • Base case with xs = []:
  sum(addShifted [] i) (AS1)
= sum([i]) (def. list)
= sum(i:[]) (S2)
= i + sum([]) (S1)
= i + 0 (Arith.)
= i + 2*0 (S1 inv)
= i + 2*sum([])
  • Step case:

To prove this we assume that the property holds for xs. We take this as our I.H P(xs). To show: P(x:xs):

  sum(addShifted (x:xs) i) (AS2)
= sum((x+i):addShifted xs x) (S2)
= (x+i) + sum(addShifted xs x) (IH)
= (x+i) + x + 2*sum(xs) (arith.)
= x + i + x + sum(xs) + sum(xs) (arith.)
= i + (x+sum(xs)) + (x+sum(xs)) (S2 inv)
= i + sum(x:xs) + sum(x:xs) (arith.)
= i + 2*sum(x:xs)

qed.

Assignment 5

       data Tree a = Leaf a | Node (Tree a) (Tree a)
                     deriving Show
       leafDepths t = leafDepthsHelper t (-1)
                       where   leafDepthsHelper (Leaf t) d     = [d+1]
                               leafDepthsHelper (Node t0 t1) d = (helper t0) ++ (helper t1)
                                                                 where helper x = leafDepthsHelper x (d+1);
       boundDepth i f t = bDHelper i f t (-1)
                        where bDHelper i f (Leaf t) d                 = if i == d+1 then Leaf (f (Leaf t)) else Leaf t
                              bDHelper i f (Node t0 t1) d | i==d+1    = Leaf (f (Node t0 t1))
                                                          | otherwise = Node (helper t0) (helper t1)
                                                                      where helper x = bDHelper i f x (d+1);

simpler versions without where:

       leafDepths :: Tree a -> [Int]
       leafDepths (Leaf a) = [0]
       leafDepths (Node left right) = (map (+1) (leafDepths left)) ++ (map (+1) (leafDepths right))
       boundDepth :: Int -> (Tree a -> a) -> Tree a -> Tree a
       boundDepth 0 f t = (Leaf (f t))
       boundDepth i f (Node l r) = (Node (boundDepth (i-1) f l) (boundDepth (i-1) f r))

Assignment 6

a)

evalPoly f polynom = foldr aux 0 polynom
  where 
    aux (coeff, list) e = e + coeff * (foldr (*) 1 $ map f list)

alternative solution :

evalPoly :: (a->Integer) -> Poly a -> Integer
evalPoly f p = sum [a * product (map f xs) | (a,xs) <-p]

b)

foldAExpr :: (a -> b) -> (Integer -> b) -> (b -> b -> b) -> (b -> b -> b) -> AExpr a -> b
foldAExpr var lit add mul (Var a) = var a
foldAExpr var lit add mul (Lit a) = lit a
foldAExpr var lit add mul (Add a b) = add (foldAExpr var lit add mul a) (foldAExpr var lit add mul b)
foldAExpr var lit add mul (Mul a b) = mul (foldAExpr var lit add mul a) (foldAExpr var lit add mul b)

alternative solution:

foldAExpr :: (a -> b) -> (Integer -> b) -> (b -> b -> b) -> (b -> b -> b) -> AExpr a -> b
foldAExpr fVar fLit fAdd fMul = go
 where
  go (Var a)        = fVar a
  go (Lit i)        = fLit i
  go (Add ae1 ae2)  = fAdd (go ae1) (go ae2)
  go (Mul ae1 ae2)  = fMul (go ae1) (go ae2)

c)

toPoly :: Eq a => AExpr a -> Poly a
toPoly = foldAExpr var lit add mul
 where
   var a = [(1, [a])]
   lit n = [(n, [] )]
   add a b = unify $ a ++ b
   mul a b = unify $ [(n * m, vars1 ++ vars2) | (n, vars1) <- a, (m, vars2) <- b ]
   -- Sum up common factors
   unify [] = []
   unify ((n, vars):xs) = (sum $ map fst $ filter (\x -> (snd x) == vars) xs, vars):(unify $ filter (\x -> (snd x) /= vars) xs)