Lösungsvorschlag Functional Programming Midterm 2009

Aus VISki
Wechseln zu: Navigation, Suche

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.
Show P(Add e1 e2)
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
   = size(Add e1 e2)

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))