Lösungsvorschlag Functional Programming Midterm 2010

Aus VISki
Wechseln zu: Navigation, Suche

Assignment 1

  • 1.

 \x y z -> y z x :: a -> (b -> a -> c) -> b -> c

  • 2.

 zipWith (==) :: Eq a => [a] -> [a] -> [Bool]

  • 3.

 \x y -> y ((==) x) :: Eq a => a -> ((a -> Bool) -> c) -> c

  • 4.

 takeWhile (\x -> x 1) :: Num a => [a -> Bool] -> [a -> Bool]


Assignment 2

                            ------------------- Ax
                            Gamma, Q(x) |- Q(x)
                            ------------------------- I               ------------------- Ax
                            Gamma, Q(x) |- y. Q(y)                    Gamma, P(x) |- P(x)
 --------------------- Ax   --------------------------------- or IL    --------------------------------- or IR
 Gamma |- Q(x) or P(x)      Gamma, Q(x) |- (y. Q(y)) or P(x)          Gamma, P(x) |- (y. Q(y)) or P(x)
 ----------------------------------------------------------------------------------------------------------- or E
                      Gamma |- (y. Q(y)) or P(x)
 ------------------------------------------------------------------------ ->I
                      |- Q(x) or P(x) -> (y. Q(y)) or P(x)
 ------------------------------------------------------------------------ I*
                      |- x. Q(x) or P(x) -> (y. Q(y)) or P(x)
 
 Gamma = Q(x) or P(x)
 *Side condition ok


Assignment 3

(a)

  dropFirstChild :: RoseTree a -> RoseTree a
  dropFirstChild (Node a []) = Node a []
  dropFirstChild (Node a (x:xs)) = Node a (map dropFirstChild xs)

(b)

  mapRoseTree :: (a -> b) -> RoseTree a -> RoseTree b
  mapRoseTree f (Node a xs) = Node (f a) (map (mapRoseTree f) xs)


Assignment 4

(a)

 Gamma |- P(Zero)          Gamma, P(n) |- P(Succ n)
 -------------------------------------------------- **
       Gamma |- forall x element of Nat. P(x)    
 
 **n not free in Gamma or P.
 
 (n element of Nat)

(b)

Proof by Induction over z. Let x,y element of Nat be arbitrary.

  • Base case: Show P(Zero)
  mult (mult x y) Zero 
 = Zero                   (mult.1)
 = mult x Zero            (mult.1)
 = mult x (mult y Zero)   (mult.1)
  • Step case: We assume P(n) and show P(Succ n)
  mult (mult x y) (Succ n)        
 = mult x y + mult (mult x y) n   (mult.2)
 = mult x y + mult x (mult y n)   (Induction Hypothesis)
 = mult x (y + mult y n)          (Lemma.1)
 = mult x (mult y (Succ n))       (mult.2)

q.e.d.


Assignment 5

(a)

  insertions :: a -> [a] -> [[a]]
  insertions x [] = [[x]]
  insertions x (y:ys) = (x:y:ys) : (map ((:) y) (insertions x ys))

There is also a one line solution (no need for efficiency mentioned...)

  insertions :: a -> [a] -> [[a]]
  insertions m list = map (\n -> (take n list) ++ [m] ++ (drop n list)) [0..(length list)]

(b)

  perms :: [a] -> [[a]]
  perms xs = foldr (\y ys -> concat [insertions y s | s <- ys]) [[]] xs

(c)

  scanl2 :: (b -> a -> b) -> b -> [a] -> [b]
  scanl2 f z [] = [z]
  scanl2 f z (x:xs) = z : (scanl f (f z x) xs)

Assignment 6

(a)

  evalOp :: Op -> (Int -> Int -> Int)
  evalOp Plus = (+)
  evalOp Minus = (-)
  evalOp Times = (*)

(b)

  foldAExpr :: (Int -> a) -> (String -> a) -> (Op -> a -> a -> a) -> AExpr -> a
  foldAExpr fCons fVar fBin = go
   where
    go (Const i) = fCons i
    go (Var s) = fVar s
    go (BinOp o l r) = fBin o (go l) (go r)

(c)

  eval :: (String -> Int) -> AExpr -> Int 
  eval env aexp = foldAExpr id env evalOp aexp

(d)

  exec :: (String -> Int) -> [Instr] -> [Int] -> [Int]
  exec env [] s = s
  exec env (x:xs) s = go x
   where
    go (ConstI i ) = exec env xs (i:s)
    go (LoadI y) = exec env xs ((env y):s)
    go (BinOpI o) = exec env xs (bin s)
     where 
      bin (x1:x2:zs) = ((evalOp o) x1 x2) : zs

(e)

  compile :: AExpr -> [Instr]
  compile aexp = foldAExpr (\i -> [(ConstI i)]) (\s -> [(LoadI s)]) (\o l r -> r ++ l ++ [(BinOpI o)]) aexp