# Assignment 1

## (a)

Ergebnisse mit ghci erhalten.

### 1.

```  \x y z -> x (y z)
:: (t1 -> t2) -> (t -> t1) -> t -> t2
```

### 2.

```  \f -> (\h -> (f, h))
:: t -> t1 -> (t, t1)
```

### 3.

```  map (elem 0)
:: (Num t) => [[t]] -> [Bool]
```

### 4.

```  \x -> x (<)
:: (Ord a) => ((a -> a -> Bool) -> t) -> t
```

## (b)

``` (\x -> snd (\y -> y x,1==10) 10)
```

This function is not well typed because it attempts to apply a Bool to 10

• "snd(_,1==10)" yields a Bool.
• "snd(...) 10" attempts to apply the result of the function "snd" to 10.

## (c)

```Where Γ:=x:Int→Bool→a

Γ ⊢ x::(Int→Bool→a)  Γ ⊢ 1::Int  Γ ⊢ False::Bool   Γ,y:b ⊢ x::(Int→Bool→a)
-------------------------------------------------   -------------------------
Γ ⊢ x 1 False::a                                    Γ ⊢ λy.x::b→(Int→Bool→a)
----------------------------------------------------------------------------
x:Int→Bool→a ⊢ (x 1 False,λy.x)::(a,b→(Int→Bool→a))
------------------------------------------------------
⊢ λx.(x 1 False,λy.x)::(Int→Bool→a)→(a,b→(Int→Bool→a))
```

# Assignment 2

## (a)

```Γ,i:Int ⊢ P(Const i)     Γ,P(a),P(b) ⊢ P(Add a b)
-------------------------------------------------
Γ ⊢ ∀ x :: Expr.P(x)
```

## (b)

Claim:

∀ e::Expr.length (pfix e) = size e

Proof:

Let P(e) := length (pfix e) = size e
We show ∀ e::Expr.P(e) by induction.
Base Case:
Show P(Const 0)
```length( pfix(Const 0) )       -- p.1
= length( [OpConst 0] )    -- l.2
= 1 + length( [] )         -- l.1
= 1 + 0                    -- Arithmetic
= 1                        -- inverse s.1
= size (Const 0)
```
Step Case:
Let e1::Expr, e2::Expr be arbitrary.
```length(pfix(Add e1 e2))                                        -- p.2
= length(pfix e1 ++ (pfix e2 ++ [OpAdd]))                   -- Lemma 1
= length(pfix e1) + length (pfix e2 ++ [OpAdd])             -- Lemma 1
= length(pfix e1) + length (pfix e2) + length([OpAdd])      -- Claim
= size e1 + size e2 + length [OpAdd]                        -- l.2
= size e1 + size e2 + 1 + length []                         -- l.1
= size e1 + size e2 + 1 + 0                                 -- Arithmetic
= size e1 + size e2 + 1                                     -- inverse s.2
```

qed.

# Assignment 3

## (a)

```takeWhile::(a->Bool)->[a]->[a]
takeWhile _ [] = []
takeWhile p (x:xs)
| p x = x:(takeWhile p xs)
| otherwise = []

```

## (b)

```intersperse::a->[a]->[a]
intersperse _ [] = []
intersperse _ [a] = [a]
intersperse e (x:xs) = x:e:(intersperse e xs)
```

## (c)

```filterMap' ::(b->Bool)->(a->b)->[a]->[b]
filterMap' p f = foldr aux e
where
aux = (\a b ->if (p (f a)) then [f a]++b else b)
e = []
```

# Assignment 4

```toInt :: Number -> Int
toInt (N base digits) = sum (zipWith (*) digits [base ^ i | i <- [0..] ])
```

oder auch:

```toInt :: Number -> Int
toInt (N base digits) = sum [(\x -> (head (drop x digits) * (base ^ x))) i | i <- [0 .. ((length(digits))-1)]]
```

# Assignment 5

## a

```data FO a = Var a
| Neg (FO a)
| And (FO a) (FO a)
| Forall a (FO a)
```

## b

```--The go function keeps track of bound variables.

subst :: Eq a => (a -> FO a) -> FO a -> FO a
subst s f = go f []
where go (Var i)      bound | i `elem` bound = Var i
| otherwise = s i
go (Neg f)      bound = Neg (go f bound)
go (And f1 f2)  bound = And (go f1 bound)  (go f2 bound)
go (Forall i f) bound = Forall i (go f (i:bound))
```