# Lösungsvorschlag Functional Programming Midterm 2010

## 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)
------------------------- ${\displaystyle \exists }$I               ------------------- Ax
Gamma, Q(x) |- ${\displaystyle \exists }$y. Q(y)                    Gamma, P(x) |- P(x)
--------------------- Ax   --------------------------------- or IL    --------------------------------- or IR
Gamma |- Q(x) or P(x)      Gamma, Q(x) |- (${\displaystyle \exists }$y. Q(y)) or P(x)          Gamma, P(x) |- (${\displaystyle \exists }$y. Q(y)) or P(x)
----------------------------------------------------------------------------------------------------------- or E
Gamma |- (${\displaystyle \exists }$y. Q(y)) or P(x)
------------------------------------------------------------------------ ->I
|- Q(x) or P(x) -> (${\displaystyle \exists }$y. Q(y)) or P(x)
------------------------------------------------------------------------ ${\displaystyle \forall }$I*
|- ${\displaystyle \forall }$x. Q(x) or P(x) -> (${\displaystyle \exists }$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
```