Zusammenfassung Functional Programming

Aus VISki
Wechseln zu: Navigation, Suche

Ausdrücke

Lazy Evaluation

  • Von aussen nach innen
 f e (f' e) wertet zuerst f aus
  • Von links nach rechts
 f e + f' e wertet zuerst f e aus
ToDo:
Schema überprüfen und vervollständigen.
Alle momentan zu editierenden Einträge werden hier gesammelt.

Es soll ein Ausdruck a ausgewertet werden: Schema

  • 1.) Ist der Typ von a eine Funktion?
    • Ja => gar nicht evaluieren
    • Nein => weiter
  • 2.) a ist nun von der Form 'f1 {Liste von Parametern}'. Betrachte die Definition von f1: Ist sie explizit (ohne Pattern matching)?
    • Ja => einsetzen. Weiter bei 2.
    • Nein => Weiter bei 3.
  • 3.) f1 ist mittels Pattern matching definiert. Gehe von oben nach unten durch die Liste der möglichen Patterns. Jeweils Match prüfen. Gibt es einen Match?
    • Ja => einsetzen. Weiter bei 2.
    • Nein => Fehler!

Beachte:

Guards ('|') sind eine Form von Pattern matching!

  • Match prüfen = Von links nach rechts ein Parameter nach dem anderen jeweils soweit evaluieren, bis Match oder Mismatch feststeht.


Eager Evaluation

  • Von innen nach aussen
 Beispiel
  • Von links nach rechts
 f e + f' e wertet zuerst f e aus

Funktionen

Funktionsdeklaration

Bemerkung: Die Art der Funktionsdeklaration hat Auswirkung auf die Reihenfolge, in welcher Ausdrücke ausgewertet werden!

Typdefinition

Es ist möglich die Typisierung der Funktion explizit anzugeben:

 xor :: Bool -> Bool -> Bool

Explizite Definition

 xor x y = (x || y) && not (x && y)

Definition mit Guards

 xor x y
   | x == True = not y
   | x == False = y

Definition mit Cases

 xor True True = False
 xor True False = True
 xor False True = True
 xor False False = False

Defintion mit Pattern

 xor True y = not y
 xor False y = y

Funktionsaufruf

Infix

 fun a b = a + b
 fun a b = a 'op' b

Prefix

 fun a b = (+) a b
 fun a b = op a b

Lambda-Calculus und Funktionen

Deklaration von Funktionen

Lambda Ausdrücke geben die Möglichkeit Funktionen "inline" zu definieren

Ein Parameter
\x -> x * 2
Zwei Parameter
\x -> \y -> x * y
Zwei Parameter (shorthand)
\x y -> x * y


Verkettung von Funktionen

(=function composition)

Mit dem "."-Operator können Funktionen verkettet werden

 Für Funktionen f :: b -> c und g :: a -> b
 (.) :: (b -> c) -> (a -> b) -> (a -> c)
 (.) f g = \x -> f (g x)

Beispiel

 map ((+10).(*100)) [1,2,3] = [110,210,310]

Funktionen aus der Vorlesung

Hier werden die standard Funktionen erklärt. Als standard verstehen sich solche Funktionen die während der Vorlesung für die einfache implementation benutzt wurden oder solche die im "Standard Prelude" beschrieben sind.

curry / uncurry

Uncurry nimmt eine Funktion f mit 2 Parameter und ein Pair x und berechnet daraus f (fst x) (fst y)

Curry wendet eine Funktion f (a,b) -> c auf zwei einzelne Parameter a, b an

Beispiel

 uncurry mod (5,4) = 1
 curry fst 2 3 = 2

foldr / foldl

 foldr :: (a -> b -> b) -> b -> [a] -> b
 foldl :: (b -> a -> b) -> b -> [a] -> b

foldr nimmt das zweite Argument und das letzte Item der Liste und wendet darauf die Funktion an. Dann nimmt es das letzte Item der Liste und das Resultat und wendet darauf die Funktion an, u.s.w


Mathematische Definitionen


Beispiel

 foldr (+) 5 [1,2,3,4] = 15
 foldr (/) 2 [8,12] = 1.333333
 foldr g 16 [2,4] where g x y = x
   = 2
 foldr g 16 [2,4] where g x y = y
   = 16
 foldl g 16 [2,4] where g x y = x
   = 16
 foldl g 16 [2,4] where g x y = y
   = 4

Implementation

 foldr f e (x:xs) = x ‘f‘ (foldr f e xs)
 foldl f e (x:xs) = foldl f (e ‘f‘ x) xs
 
 Alternative Schreibweise
 foldr f z [] = z
 foldr f z (x:xs) = f x (folder f z xs)
 
 foldl f z [] = z
 foldl f z (x:xs) = foldl f (f z x) xs

filter

  • Entfernt Elemente aus der Liste für welche die Funktion p nicht zu True auswertet
  • Behält nur Element der Liste für welche die Funktion p zu True auswertet
 filter :: (a -> Bool) -> [a] -> [a]
 filter p l

Beispiel

 filter even [1,2,3,4,5] = [2,4]
 even x =
   |(mod x 2) == 0 = True
   |otherwise = False

iter

Wendet die Funktion f n mal auf x an

 iter 0 f x = x
 iter n f x = f (iter (n-1) f x)


map

map wendet eine Funktion auf alle Elemente einer Liste an und gibt die veränderte Liste zurück.

 map :: (a -> b) -> [a] -> [b]


Beispiel

 map (*2) [1,2,3] = [2,4,6]

zip

 zip :: [a] -> [b] -> [(a,b)]

Beispiel

 zip [2,3,4] [5,6,7] = [(2,5), (3,6), (4,7)]
 zip [2,3,4] [5,6,7,8] = [(2,5), (3,6), (4,7)] Extra Elemente werden verworfen

zipWith

Beispiel

zipWith (*)  [1,2,3,4] [5,6,7,8] = [5,12,21,32]

Listen

Definition von Listen

 [] Leere Liste
 [3..6] = [3,4,5,6]
 [7,6..3] = [7,6,5,4,3]

Manipulationen auf Listen

Listen zusammenhängen

 [3,4,5] ++ [6] = [3,4,5,6]
 [2] ++ [3,4,5] = [2,3,4,5] ist äquivalent zu 2 : [3,4,5] = [2,3,4,5]

Element zu Liste hinzufügen

 2 : [3,4,5] = [2,3,4,5]
 [3,4,5] : 2 = ERROR

Erstes Element abspalten

 gethead [] = 0
 gethead (ersteselement:list) = ersteselement

Liste invertieren

Einfache Variante in O(n^2) Beachte: ++ ist O(n)!

 rev [] = []
 rev (a:x) = rev x ++ [a]

Beispiel

 rev [1,2,3,4,5] = [5,4,3,2,1]


Schnelle Variante in O(n)

 qrev x = aux (x, [])
 aux([], y) = y
 aux ((a:x),y) = aux (x, a:y) Element wird am Listenanfang angehängt

List comprehension

 [fun x | x <- [1..4], condition1 x, condition 2 x, ...]

Beispiel

 [xˆ2 | x <- [1..10], odd x] = [1,9,25,49,81]

Bemerkung

  • Funktioniert in gewissen Fällen auch mit unendlichen Listen

Unendliche Listen

Eine unendliche Liste wird zum Beispiel mit [1..] erzeugt

Man beachte, dass einige Funktionen auf unendlichen Listen nicht terminieren!

Beispiele

 head [1..] = 1
 tail [1..] terminiert nicht
 length [1..] terminiert nicht

Korrektheit

Ein Korrektheitsbeweis setzt sich aus folgenden Teilen zusammen:

  • Termination: Terminiert der Algorithmus für alle Eingaben?
  • Functional behavior: Erzeugt der Algorithmus korrekte Ausgaben?


Beweismethoden zu Termination

Beweis mittels Subfunktionen

Benutze die Funktion f ausschliesslich die Funktionen zur Berechnung des Resultates. Wenn alle Funktionen terminieren, dann terminiert auch f.


Beweis über eine "well-founded chain"

Diese Beweismethode ist besonders interessant bei rekursiven Funktionen

Definition

Eine Ordnung > auf einem Set S ist well-founded genau dann wenn es keine unendliche absteigende Folge

Beispiele

  • Für eine well-founded chain
    • In jedem Schritt wird n um 1 kleiner
    • Ist n = 0 bricht die Rekursion ab
    • Für Startwerte <0 bricht die Rekursion ab
 fac :: Int -> Int
 fac n
   |n == 0 = 1
   |n < 0 = 0
   |otherwise = n * fac (n-1)

Achtung: Dies gilt nur, wenn n vom Typ Integer ist!


  • Für eine nicht well-founded chain
    • Ist n = 0 oder n = 1 bricht die Rekursion ab
    • Das Problem ist allerdings, dass die Rekursion nur genau dann abbricht, wenn beide Funktionsaurufe g(n+1) + g(n-2) gleizeitig abbrechen. Dies ist in diesem Beispiel jedoch nicht nur nicht der Fall, sondern nicht einmal möglich! (Diverenz der Funktionsparameter 3, nur die 2 Abbruchfälle n= 0 und n= 1)
g :: Int -> Int
g n
  |n == 0 = 1
  |n == 1 = 1
  |otherwise = g(n+1) + g(n-2)

Beweismethoden zu Functional behavior

Korrektheitsbeweis über Fallunterscheidungen

Korrektheitsbeweis mittels Induktion

Korrektheitsbeweis mittels Induktion über Listen

 Base case: Beweise dass die Induktionshypothese für P([]) gilt
 Step case: Beweise dass die Induktionshypothese für P(a:x) und a::T gilt, unter der Annahme, dass P(x) für ein beliebiges x::[T] gilt.

Typing

Basic Types

 True           :: Bool
 'H'            :: Char
 "Hello World"  :: [Char]
 (==)           :: Eq a  => a -> a -> Bool
 (<)            :: Ord a => a -> a -> Bool
 (+)            :: Num a => a -> a -> a

Regeln für lambda-Calculus

Base Types

Axiom

Abstraction

mit

Application

Operations

ToDo:
{{{1}}}
Alle momentan zu editierenden Einträge werden hier gesammelt.

iszero

Tuples

ToDo:
{{{1}}}
Alle momentan zu editierenden Einträge werden hier gesammelt.

Enumeration types

 data Season = Spring | Summer | Fall | Winter

Syntax

  • Muss mit keyword data beginnen
  • Erster Buchstabe des Konstruktor muss ein Grossbuchstabe sein

Product types

 data People = Person String Int

Beispiel

 Person "Peter Muster" 3

Integration with classes

 data Season = Spring | Summer | Fall | Winter

Problem: Keine Gleichheit definiert

  • Lösung durch Implementation
 instance Eq Season where
   Spring == Spring = True
   Summer == Summer = True
   Fall == Fall = True
   Winter == Winter = True
   _ == _ = False


  • Lösung durch Vererbung
  data Season = Spring | Summer | Fall | Winter
     deriving (Eq, Ord, Enum, Show)

Advanced Beispiel

 data Set t = MkSet [t]  -- Deklaration eines Typ Set mit Elementen vom Typ t

 instance Show a => Show (Set a) where    -- Implementation der Show Funktion
    show (MkSet t1 )= show t1

Links

Haskell 98 Tutorial (PDF)

Haskell 98 Language Report (PDF)

Unter anderem Referenz zur Prelude