Lösungsvorschlag Functional Programming Midterm 2006

Aus VISki
Wechseln zu: Navigation, Suche

Assignment 1 (Typing)

a)

I.

  1. from f :: Eq b => b → a → b follows x :: b and f x :: Eq b => a → b (note: a and b are reversed here for consistency with how it will fit into b, as variables can be named however one wants it doesn't change anything)
  2. from g :: (a → b) → [a] → [b] follows y :: [a] and g (f x) y :: Eq => [b]
  3. in lamba writing this looks like \x y → g (f x) y :: Eq => b → [a] → [b]
  4. we now compare it to y such that g (f x) y = y :: Boolean which means the result of g (f x) y has to be of the same type as y itself
  5. \x y → g (f x) y = y :: Eq b => b → [b] → Boolean.

II.

  1. g x :: [a] -> [b] ist eine Funktion, ebenso g y. Funktionen können nicht miteinander verglichen werden, da dieses Problem prinzipiell unentscheidbar ist. (Theorem von ...). Da also g x nicht in Eq ist, ist dieser Ausdruck nicht 'well typed'. ( /= ist nicht geklammert und wird somit als Infix interpretiert, also auch nicht als Argument von g x aufgefasst.)

III.

  1. \z → z :: a → a
  2. g (\z → z) :: [a] → [b]. Again, a and b must be equal.
  3. [g (\z → z)] :: [[a] → [a]]
  4. [g (\z → z)] is not a function but a list: we cannot apply it to x. This expression is not well typed.


b)

        y : a, x : (a -> (a,a)) -> Int +- y :: a      y : a, x : (a -> (a,a)) -> Int +- y :: a
        --------------------------------------------------------------------------------------1
                y : a, x : (a -> (a,a)) -> Int +- (y,y) :: (a,a)
                ------------------------------------------------2
                x : (a -> (a,a)) -> Int +- \y.(y,y) :: a -> (a,a)      x : (a -> (a,a)) -> Int +- x :: (a -> (a,a)) -> Int             
                ----------------------------------------------------------------------------------------------------------3
x : (a -> (a,a)) -> Int +- 2 :: Int              x : (a -> (a,a)) -> Int +- x (\y.(y,y)) :: Int
-----------------------------------------------------------------------------------------------4
x : (a -> (a,a)) -> Int +- 2 + x (\y.(y,y)) :: Int
--------------------------------------------------5
+- \x.(2 + x (\y.(y,y))) :: ((a -> (a,a)) -> Int) -> Int
  1. Tuple rule
  2. Abstraction rule
  3. Application rule
  4. Op rule (addition)
  5. Abstraction rule

Variante: (dasselbe in grün)

Let .
                                           -----------------     ------------------- (Axiom)
                                                 
                                           ----------------------------------------- (Pair)
                                                         
                      ------------------------------    ---------------------------- (Axiom, Abstraction)
                          
------------------    -------------------------------------------------------------- (Axiom, Application)
                          
------------------------------------------------------------------------------------ (Op)
                    
------------------------------------------------------------------------------------ (Abstraction)
     


c)

  1. f has to be a function, since we have an application f (fix ..), i.e. f :: a → b
  2. therefore, fix :: (a → b) → b
  3. but now fix f :: b
  4. since we apply f to fix f, a and b must be equal.
  5. ergo fix :: (a → a) → a

Assignment 2 (Lazy / eager Eval.)

(a) eager:

(\x y -> y x ) (( \z -> z ) y)
(\x y -> y x ) y
(\a.ay)
evalE ("(%x y -> y x)"++"((%z -> z) y)")
"\\y' -> y' y"

(b) lazy:

(\x y -> y x ) (( \z -> z ) y)
(\a -> a ((\z -> z) y))
evalL ("(%x y -> y x)"++"((%z -> z) y)")
"\\y' -> y' ((\\z -> z) y)"

Assignment 3 (foldr/map/..)

a)

  • f1: Konkatenation der Elemente einer Liste (z.B. [[1,2],[5,3]] --> [1,2,5,3])
  • f2: Umkehrung einer Liste (z.B. [1,2,3,4] --> [4,3,2,1])

b)

myMapB f l = foldr (\x y -> (f x):y) [] l

c)

myMapC f l = foldl (\x y -> x++[f y]) [] l

Assignment 4 (Various)

a) Folgendes ist gegeben:

(1): length [] = 0 
(2): length (x:xs) = 1 + length xs
(3): [] ++ ys = ys
(4): (x:xs) ++ ys = x : (xs ++ ys)


Es sei P(x): length x + length y = length(x++y)

Basecase: P([]):

length [] + length y 
= 0 + length y      (Def. von length (1))
= length y          (basic mathe über Int)
= length ([]++y])   (rückweg von (3))
= length (x++y)     (da x=[])

Stepcase: Es gelte P(x), wir zeigen nun P(a:x)

length (a:x) + length y 
= 1 + length x + length y   (Def. von length über (a:x) (2))
= 1 + length (x++y)         (Induktionsannahme P(x))
= length (a:(x++y))         (Def. von length rückwärts (3))
= length ((a:x)++y)         (Rückweg von (4))

Wegen Kommutativität der Addition gilt dies analog auch für alle y

qed.

Kommentar: Vorsicht! Das Kommutativitätsargument stimmt nicht: Der Schritt 1 + length (x++y) = length (x ++ (a:y)) ist ohne Lemma nicht gültig. Es reicht aber völlig aus, bei Induktionsverankerung und -schritt darauf hinzuweisen, dass y beliebig ist. Eine Induktion über y wäre vollkommen überflüssig!


b) ist aus der 05er, allerdings hat man hier nicht schon ein tree fold

fringe :: LTree a -> [a]                    
fringe (LLeaf n) = [n]                          
fringe (LNode t1 t2) = fringe t1 ++ fringe t2

c)

count (LLeaf _) = 0                                  
count (LNode t1 t2) = 1 + count t1 + count t2            
data LTree a = LLeaf a | LNode (LTree a) (LTree a)

thesis

count t = length (fringe t) - 1


the lowest LTree component is LLeaf, every LTree ultimately ends in one of them, as LLeafs can't hold another LLeaf every LLeaf is hold by an LNode (if the LTree is bigger than just one LLeaf) -> base cases needed for (LLeaf a) and (LNode (LLeaf a) (LLeaf a))

Base cases

  1. t = LLeaf a
    1. count (LLeaf a) = length (fringe (LLeaf a) - 1
    2. 0 = length [a] - 1
    3. 0 = 0
  2. t = LNode (LLeaf a) (LLeaf a)
    1. count (LNode (LLeaf a) (LLeaf a)) = length (fringe (LNode (LLeaf a) (LLeaf a))) - 1
    2. 1 + count (LLeaf a) + count (LLeaf a) = length (fringe (LLeaf a) ++ fringe (LLeaf a)) - 1
    3. 1 + 0 + 0 = length [a, a] - 1
    4. 1 = 1

Step case

  1. t = LNode t1 t2
    1. count (LNode t1 t2) = length (fringe (LNode t1 t2)) - 1
    2. 1 + count t1 + count t2 = length (fringe t1 ++ fringe t2) - 1
    3. 1 + count t1 + count t2 = length t1 + length t2 - 1
    4. 1 + count t1 + count t2 = 1 + (length t1 - 1) + (length t2 -1)
    5. 1 = 1

(count t1 = length t1 - 1) and (count t2 = length t2 -1) based on the base cases

  • Anm.: Es sollte reichen, den step case t = Lnode t1 t2 zu zeigen, wobei für t1 und t2 die Induktionshypothese gilt. Andernfalls wäre der Beweis nicht vollständig, da die Fälle t = LNode (LLeaf ..) (LNode ..) und umgekehrt nicht abgedeckt sind....
  • Anm zur Anm: LNode... steht sowohl für nodes wie auch für leafes, könnte auch t1 und t2 stehn ^^ *editing*


Alternativer beweis

Es sei P(t): count t = length (fringe t) - 1

Basecase: P(LLeaf a): count (LLeaf a) = 0 (Def. von count)

                     length (fringe (LLeaf a)) - 1 = length ([a]) - 1           (Def. von fringe)
                                                   = 1 - 1 = 0                  (Basic)

Stepcase: P(t) gilt für P(t1) und P(t2) in P(LNode t1 t2)

P(LNode t1 t2): count (LNode t1 t2) = 1 + count t1 + count t2 (Def. von count)

                                   = 1 + length (fringe t1) - 1 + length (fringe t2) - 1 (Induktionsannahme P(t))
                                   = length (fringe t1) + length (fringe t2) - 1 (1-1 = 0)
                                   = length (fringe t1 ++ fringe t2) - 1        (Siehe Beweis von a)
                                   = length (fringe (LNode t1 t2)) - 1          (Def. von fringe)

qed.

Assignment 5 (String Implementation)

embed :: String -> String -> Int
embed [] _ = 1
embed _ [] = 0
embed (a:l) (b:m)
	| a==b = (embed l m) + (embed (a:l) m)
	| otherwise = embed (a:l) m


Alternative:

embed :: String -> String -> Int
embed "" _ = 0
embed _ "" = 0
embed (x:[]) (y:ys) = if x == y then 1 + (embed [x] ys) else embed [x] ys
embed (x:xs) (y:ys) = if x == y then (embed xs ys) + (embed (x:xs) ys) else embed (x:xs) ys

Assignment 6 (ADT)

Taken from the solutions of Assignment 4 in Series 6 (2009):

data Expr a = Var a | ConstE | Num Double |
              Mul (Expr a) (Expr a) | Add (Expr a) (Expr a) | 
              Div (Expr a) (Expr a) |
              Pow (Expr a) (Expr a) | Exp (Expr a) | Log (Expr a)
              deriving( Eq, Ord )


diff x (Var y)     = if x==y then Num 1.0 else Num 0.0
diff x ConstE      = Num 0.0
diff x (Num _)     = Num 0.0
diff x (Add e1 e2) = Add (diff x e1) (diff x e2)
diff x (Mul e1 e2) = Add (Mul (diff x e1) e2) (Mul e1 (diff x e2))
diff x (Log e)     = Div (diff x e) e
diff x (Exp e)     = Mul (diff x e) (Exp e)
diff x (Div e1 e2) = diff x (Mul e1 (Pow e2 (Num (-1.0))))
diff x (Pow e1 e2) = diff x (Exp (Mul e2 (Log e1)))