# 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 $\Gamma =\exists z.Q(z)\land P(z)$

                                             ------------------------------------------ ax
$\Gamma ,Q(x)\land P(x)\vdash Q(x)\land P(x)$
------------------------------------------ $\land$ EL
$\Gamma ,Q(x)\land P(x)\vdash Q(x)$
-------------------------------------ax     ------------------------------------------ $\exists$ I
$\Gamma \vdash \exists x.Q(x)\land P(x)$                                      $\Gamma ,Q(x)\land P(x)\vdash \exists w.Q(w)$
------------------------------------------------------------------------- $\exists$ E, sc ok, bc x not free in $\Gamma$ or $\exists w.Q(w)$
$\Gamma \vdash \exists w.Q(w)$
------------------------------------------------- $\to$ I
$\vdash (\exists zQ(z)\land P(z))\to \exists w.Q(w)$


# 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)
= (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) =  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)