kapitel 4: beweis und herleitung von programmen · ’funktionale programmierung (ws2005/2006) 4/7...
TRANSCRIPT
Funktionale Programmierung (WS2005/2006) 4/1'
&
$
%
Kapitel 4: Beweis und Herleitung von Programmen
Lernziele dieses Kapitels
1. Bedeutung der referenziellen Transparenz und des Gleichungsbeweisens
2. Strukturelle Induktion: Naturliche Zahlen, Listen, Baume
3. Listengesetze: Dekomposition, Dualitat, Fusion, Homomorphie
4. Homomorphismen zur Herleitung von Algorithmen: Mergesort, Fibonacci
5. Programmtransformationen zur Erhohung der Effizienz:Maximale Segmentsumme
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/2'
&
$
%
Referenzielle Transparenz (1)Def.: ein Ausdruck E heisst referenziell transparent, wenn jeder beliebigeTeilausdruck T durch einen Ausdruck T’ gleichen Wertes ersetzt werden kann,ohne dass sich dabei der Wert von E andert.
Bei referenzieller Transparenz gilt die Leibniz-Regel: T=T ′E[x:=T ]=E[x:=T ′]
Beispiel:
f x + f x = {nicht-striktes let}let y = f x in f x + f x = {Leibniz}let y = f x in y + f x = {Leibniz} kritische Stelle
let y = f x in y + y = {Arithmetik auf Integer-Variablen}let y = f x in 2 * y = {Leibniz}let y = f x in 2 * f x = {nicht-striktes let}2 * f x
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/3'
&
$
%
Referenzielle Transparenz (2)• Sprache mit Seiteneffekten: referenzielle Transparenz nicht gegeben
dann z.B.: f x + f x 6= 2 * f x, vgl. Kap. 1
• funktionale Sprachen mit referenzieller Transparenz: rein funktional
• Haskell erlaubt Ein-/Ausgabe mit referenzieller Transparenz:Wert von I/O-Operationen ist nicht Ruckgabewert der Operation, sondern dieOperation selbst:
Haskell OCaml
let outOp = putStr "ha"
in do outOp
outOp
let outOp = printf "ha"
in outOp;
outOp
Ausgabe: haha Ausgabe: ha
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/4'
&
$
%
Beweis von Programmen
• gegeben
1. Spezifikation, d.h. Ein-/Ausgaberelation
2. Programm
• gesucht: Beweis, dass Programm die Spezifikation erfullt
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/5'
&
$
%
Beweis imperativer Programme
etablierte Methode: Hoare-Kalkul (Methode der Zusicherungen)
• Spezifikation: Vor- und Nachbedingung an Programm
• Aussagen uber den Zustand der Belegung der Variablen
• Vorbedingung und Nachbedingung an jeden Programmteil
– Invarianten fur Schleifen
– Substitutionsregel fur Statements
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/6'
&
$
%
Beweis funktionaler Programme
etablierte Methode: Equational Reasoning (Gleichheitsbeweise)
Spezifikation: Ein-/Ausgaberelation, was bleibt zu tun?
1. Spezifikation muss nicht ausfuhrbar sein, z.B.
• Gleichungen sind keine zulassigen Funktionsdefinitionen
• nicht-integrierte Zusatzbedingungen
2. Spezifikation ist ausfuhrbar, aber extrem ineffizient
• Programm hat gleiche Semantik, aber effizienteren Berechnungsweg
Gleichheitsbeweis: schrittweise Uberfuhrung der Spezifikation in dasEndprogramm durch Anwendung von Regeln (z.B. Leibniz)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/7'
&
$
%
Prinzip des Gleichheitsbeweisens
• Gleichungskette zwischen zwei Ausdrucken
• jede Gleichung gerechtfertigt durch Anwendung einer Regel
Regelanwendung, um Gleichheit P = Q zu rechtfertigen:
1. gib einen Kontext E mit einer Variablen v an, sodass es Ausdrucke L’ und R’gibt, mit denen gilt: E[v:=L′] = P und E[v:=R′] = Q
2. wahle geeignete Regel L = R (oder R = L) aus Regelbasis aus
3. gib eine Substitution(*) ϕ an, so dass L′ = ϕL und R′ = ϕ R
(*) Substitution ϕT rein syntaktisch und simultan: fur jede freie Variable x in T
ersetze jedes freie Vorkommen von x in T durch einen bestimmten Ausdruck (ϕx)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/8'
&
$
%
Beispiel einer Regelanwendunggegeben
• P = f (x * (y + g z)) - 1
• Q = f (x * y + x * g z) - 1.
• Regelbasis enthalt: (a * (b + c)) = a * b + a * c (Distributivgesetz)
zu zeigen: P = Q
1. gib einen Kontext E mit einer Variablen v an, sodass es Ausdrucke L’ und R’gibt, mit denen gilt: E[v:=L′] = P und E[v:=R′] = Q
E = f v - 1, L′ = x * (y + g z), R′ = x * y + x * g z
2. wahle geeignete Regel L = R (oder R = L) aus Regelbasis aus
wahle Distributivgesetz: L = a * (b + c), R = a * b + a * c
3. gib eine Substitution ϕ an, so dass L′ = ϕL und R′ = ϕR
ϕ = [a:=x, b:=y, c:=g z]
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/9'
&
$
%
Beweis-Skizzenur der Name der Regel wird angegeben oder eine intuitive Bezeichnung
fac 0 = 1 -- fac.1
fac n | n>0 = n * fac (n-1) -- fac.2
Beispiel (Beweis-Skizze):
fac 2 = {fac.2}2 * fac (2-1) = {Arithmetik}2 * fac 1 = {fac.2}2 * (1 * fac (1-1)) = {Arithmetik}2 * (1 * fac 0) = {fac.1}2 * (1 * 1) = {Arithmetik}2 * 1 = {Arithmetik}2
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/10'
&
$
%
Korrektheit des Gleichungsbeweisens
Haskell hat wichtige Eigenschaften
1. referenzielle Transparenzjede Gleichung erhalt die partielle Korrektheit
2. Nicht-Striktheit der Funktionsanwendung (Laziness):Terminationsverhalten bleibt unverandert bei
• Verwendung einer Funktionsgleichung als Regel (z.B. fac.2)
• Anderung von Ersetzungsreihenfolgen
3. statisches Typsystemjeder Ausdruck hat eine definierte Semantik
• soetwas wie (/2).(*2) = id = (’div’ 2).(*2) gibt es nicht
• Regeln sind typabhangig: + assoziativ fur Rational, aber nicht fur Float
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/11'
&
$
%
Unterschiedliche Ersetzungsreihenfolgen (1)bridge :: (Float,Float) -> Float -> Float -> Float
bridge (x0,y0) x y = if x==x0 then y0 else y -- bridge
f :: Float -> Float
f x = bridge (0,1) x (sin x / x) -- f
zuerst Argumentauswertung
f 0 = {f}bridge (0,1) 0 (sin 0 / 0) = {Arithmetik}bridge (0,1) 0 (0 / 0) = {Arithmetik}bridge (0,1) 0 ⊥ = {bridge}if 0==0 then 1 else ⊥ = {==}if True then 1 else ⊥ = {if-then-else}1
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/12'
&
$
%
Unterschiedliche Ersetzungsreihenfolgen (2)bridge :: (Float,Float) -> Float -> Float -> Float
bridge (x0,y0) x y = if x==x0 then y0 else y -- bridge
f :: Float -> Float
f x = bridge (0,1) x (sin x / x) -- f
zuerst Anwendung der Funktionsgleichung
f 0 = {f}bridge (0,1) 0 (sin 0 / 0) = {bridge}if 0==0 then 1 else (sin 0 / 0) = {==}if True then 1 else (sin 0 / 0) = {if-then-else}1
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/13'
&
$
%
Strukturelle Induktion
hier: endliche Strukturen, keine Betrachtung von Laziness
Die naturlichen Zahlen als (strukturell) induktiv definierte Menge:
data Nat = Zero Null
| Succ Nat Nachfolger
deriving (Eq,Ord,Show)
Wir verwenden Z und S als Abkurzung fur Zero bzw. Succ.
Elemente von Nat: Z (0), S Z (1), S (S Z) (2), S (S (S Z)) (3) ...
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/14'
&
$
%
Addition auf Nat
Definition von Funktionen auf induktiv definierten Typendurch Angabe der Gleichung fur jeden Datenkonstruktor
add :: Nat -> Nat -> Nat
add x Z = x -- add.1
add x (S y) = S (add x y) -- add.2
add’ :: Integer -> Integer -> Integer
add’ x 0 = x -- add’.1
add’ x y | y>0 = 1 + add’ x (y-1) -- add’.2
add (S Z) (S Z) Ã S (S Z)
add’ 1 1 Ã 2
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/15'
&
$
%
Multiplikation auf Nat
mul :: Nat -> Nat -> Nat
mul x Z = Z -- mul.1
mul x (S y) = add x (mul x y) -- mul.2
mul’ :: Integer -> Integer -> Integer
mul’ x 0 = 0 -- mul’.1
mul’ x y | y>0 = x + mul’ x (y-1) -- mul’.2
mul (S (S Z)) (S (S (S Z))) Ã S (S (S (S (S (S Z)))))
mul’ 2 3 Ã 6
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/16'
&
$
%
Schrittweise Berechnungmul (S (S Z)) (S (S (S Z)))
{mul.2}→ add (S (S Z)) (mul (S (S Z)) (S (S Z)))
{mul.2}→ add (S (S Z)) (add (S (S Z)) (mul (S (S Z)) (S Z)))
{mul.2}→ add (S (S Z)) (add (S (S Z))
(add (S (S Z)) (mul (S (S Z)) Z)))
{mul.1}→ add (S (S Z)) (add (S (S Z)) (add (S (S Z)) Z))
{add.1}→ add (S (S Z)) (add (S (S Z)) (S (S Z)))
{add.2}→ add (S (S Z)) (S (add (S (S Z)) (S Z)))
{add.2}→ S (add (S (S Z)) (add (S (S Z)) (S Z)))
{add.2}→ S (add (S (S Z)) (S (add (S (S Z)) Z)))
{add.2}→ S (S (add (S (S Z)) (add (S (S Z)) Z)))
{add.1}→ S (S (add (S (S Z)) (S (S Z))))
{add.2}→ S (S (S (add (S (S Z)) (S Z))))
{add.2}→ S (S (S (S (add (S (S Z)) Z))))
{add.1}→ S (S (S (S (S (S Z)))))
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/17'
&
$
%
Der induktive Datentyp Liste
data List a = Nil leere Liste
| C a (List a) cons
In Haskell (keine legale Quellprogrammsyntax)
-- data [a] = []
-- | a : [a] deriving (Eq, Ord)
Elemente: Nil []
C x Nil x:[]
C y (C x Nil) y:x:[]
C z (C y (C x Nil)) z:y:x:[]
...
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/18'
&
$
%
Die Langenfunktion auf Listen
len :: List a -> Nat
len Nil = Z -- len.1
len (C _ xs) = S (len xs) -- len.2
len’ :: [a] -> Int --Integer nicht notig, weil Speicher <= Adressraum
len’ [] = 0 -- len’.1
len’ (_:xs) = 1 + len’ xs -- len’.2
len (C z (C y (C x Nil))) Ã S (S (S Z))
len’ (z:y:x:[]) Ã 3
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/19'
&
$
%
Die Summenfunktion auf Listen
su :: List Nat -> Nat
su Nil = Z -- su.1
su (C x xs) = add x (su xs) -- su.2
su’ :: Num a => [a] -> a
su’ [] = 0 -- su’.1
su’ (x:xs) = x + su’ xs -- su’.2
su (C (S Z) (C (S (S Z)) (C (S Z) Nil))) Ã S (S (S (S Z)))
su’ (1:2:1:[]) Ã 4
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/20'
&
$
%
Induktive Definition der append-Funktion
append (++) verkettet zwei Listen
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys -- (++).1
(x:xs) ++ ys = x : (xs ++ ys) -- (++).2
(1:2:3:[]) ++ (4:5:6:7:8:9:[])
{(++).2}→ 1:((2:3:[]) ++ (4:5:6:7:8:9:[]))
{(++).2}→ 1:2:((3:[]) ++ (4:5:6:7:8:9:[]))
{(++).2}→ 1:2:3:([] ++ (4:5:6:7:8:9:[]))
{(++).1}→ 1:2:3:4:5:6:7:8:9:[]
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/21'
&
$
%
Induktive Definition des map-Kombinatorsmap :: (a->b) -> [a] -> [b]
map f [] = [] -- map.1
map f (x:xs) = f x : map f xs -- map.2
map (^2) (1:2:3:4:[])
{map.2}→ (^2) 1 : map (^2) (2:3:4:[])
{(^2) }→ 1 : map (^2) (2:3:4:[])
{map.2}→ 1 : (^2) 2 : map (^2) (3:4:[])
{(^2) }→ 1 : 4 : map (^2) (3:4:[])
{map.2}→ 1 : 4 : (^2) 3 : map (^2) (4:[])
{(^2) }→ 1 : 4 : 9 : map (^2) (4:[])
{map.2}→ 1 : 4 : 9 : (^2) 4 : map (^2) []
{(^2) }→ 1 : 4 : 9 : 16 : map (^2) []
{map.1}→ 1 : 4 : 9 : 16 : []
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/22'
&
$
%
Struktureller Induktionsbeweis (informell)• Induktionsaxiom: (zum Beweis einer Aussage P )
fur jeden Datenkonstruktor C eines induktiv definierten Typs S:
1. sei x ein beliebiges Element von S mit Wurzelsymbol C
2. Induktionsannahme: P (xi) gelte fur jede echte Teilstruktur xi von x
3. man zeige, dass P (x) gilt
⇒ dann gilt die Aussage P fur alle endlichen Elemente von S
• Basisfall, gdw. kein xi enthalt Element vom Typ S
• Induktionsfall, gdw. mindestens ein xi enthalt Element vom Typ S
• Problem: Wahl der Induktionsvariablen x in P (x)
• Spezialfalle
– Vollstandige Induktion: Konstruktoren Zero (0) und Succ (x → x+1)
– Listeninduktion: Konstruktoren [] (nil) und (:) (cons)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/23'
&
$
%
Strukturelles Induktionsaxiom (halbformal)• sei S ein algebraischer Datentyp mit Konstruktoren { Cj | j ∈ N ∧ 0 ≤ j < n }• #j die Anzahl der Argumente von Konstruktor Cj
• P ein zu beweisendes Pradikat
• Induktionsaxiom
∀j : 0 ≤ j < n ::
∀xj,0, . . . , xj,#j−1 ::
(∀i : (0≤ i<#j ∧ xj,i ∈ S) : P (xj,i)) =⇒ P (Cj xj,0...xj,#j−1)
∀x : x ∈ S ∧ x endlich : P (x)
• Vollstandige Induktion als Spezialfall
P (Zero) ∧ (∀x : x ∈ Nat : P (x) =⇒ P (Succ x))∀x : x ∈ Nat ∧ x endlich : P (x)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/24'
&
$
%
Beweis: map f xs ++ map f ys == map f (xs++ys) {Fall.1}
Induktionsvariable: xs
{Fall.1}: xs==[]map f xs ++ map f ys
{Fall.1}== map f [] ++ map f ys
{ map.1}== [] ++ map f ys
{(++).1}== map f ys
{(++).1}== map f ([]++ys)
{Fall.1}== map f (xs++ys)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/25'
&
$
%
Beweis: map f xs ++ map f ys == map f (xs++ys) {Fall.2}
Induktionsvariable: xs
{Fall.2}: xs==(z:zs)map f xs ++ map f ys
{Fall.2}== map f (z:zs) ++ map f ys
{ map.2}== (f z : map f zs) ++ map f ys
{(++).2}== f z : (map f zs ++ map f ys)
{Ind-A.}== f z : (map f (zs++ys))
{ map.2}== map f (z:(zs++ys))
{(++).2}== map f ((z:zs)++ys)
{Fall.2}== map f (xs++ys)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/26'
&
$
%
Beweis: (map f . map g) xs == map (f . g) xs {Fall.1}
(q . p) x = q (p x) -- compose
Induktionsvariable: xs
{Fall.1}: xs==[](map f . map g) xs
{Fall.1 }== (map f . map g) []
{compose}== map f (map g [])
{ map.1 }== map f []
{ map.1 }== []
{ map.1 }== map (f . g) []
{Fall.1 }== map (f . g) xs
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/27'
&
$
%
Beweis: (map f . map g) xs == map (f . g) xs {Fall.2}
Induktionsvariable: xs
{Fall.2}: xs==(z:zs)(map f . map g) xs
{Fall.2 }== (map f . map g) (z:zs)
{compose}== map f (map g (z:zs))
{ map.2 }== map f (g z : map g zs)
{ map.2 }== f (g z) : map f (map g zs)
{compose}== (f . g) z : map f (map g zs)
{compose}== (f . g) z : (map f . map g) zs
{Ind-A. }== (f . g) z : map (f . g) zs
{ map.2 }== map (f . g) (z:zs)
{Fall.2 }== map (f . g) xs
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/28'
&
$
%
Verwendung der vordefinierten Arithmetik
• Konstruktor-basierte Berechnung: langsam und inflexibel
• besser: eingebaute Arithmetik verwenden
• Bsp.: Fakultatsfunktion
fac :: Integer -> Integer
fac 0 = 1
fac n | n>0 = n * fac (n-1)
• Vorsicht: Wertebereich berucksichtigen (Termination)
• Induktionsbeweise analog mit 0 statt Zero und (+1) statt Succ
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/29'
&
$
%
Baume als induktive Datentypendata BinTree1 a
= Empty1
| Fork1 { elem1::a, left1, right1 :: BinTree1 a }
data BinTree2 a
= Leaf2 { elem2::a }| Fork2 { left2, right2 :: BinTree2 a }
data BinTree3 a
= Leaf3 { elem3::a }| Fork3 { elem3::a, left3, right3 :: BinTree3 a }
data RoseTree a
= Fork4 { elem4::a, children::[RoseTree a] }
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/30'
&
$
%
Summenfunktion sumT auf BinTree2
sumT :: Num a => BinTree2 a -> a
sumT (Leaf2 elem) = elem -- sumT.1
sumT (Fork2 left right) = sumT left + sumT right -- sumT.2
sumT (Fork2 (Fork2 (Leaf2 1) (Leaf2 2)) (Leaf2 1))
{sumT.2}→ sumT (Fork2 (Leaf2 1) (Leaf2 2)) + sumT (Leaf2 1)
{sumT.2}→ sumT (Leaf2 1) + sumT (Leaf2 2) + sumT (Leaf2 1)
{sumT.1}→ 1 + sumT (Leaf2 2) + sumT (Leaf2 1)
{sumT.1}→ 1 + 2 + sumT (Leaf2 1)
{ + }→ 3 + sumT (Leaf2 1)
{sumT.1}→ 3 + 1
{ + }→ 4
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/31'
&
$
%
Beweis: leaves t == forks t + 1
data BinTree2 a = Leaf2 a
| Fork2 (BinTree2 a) (BinTree2 a)
leaves, forks :: BinTree2 a -> Integer
leaves (Leaf2 ) = 1 -- leaves.1
leaves (Fork2 l r) = leaves l + leaves r -- leaves.2
forks (Leaf2 ) = 0 -- forks.1
forks (Fork2 l r) = 1 + forks l + forks r -- forks.2
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/32'
&
$
%
Beweis: leaves t == forks t + 1 {Fall.1}
Induktionsvariable: t
{Fall.1}: t == Leaf2
leaves t
{ Fall.1 }== leaves (Leaf2 )
{ leaves.1 }== 1
{Arithmetik}== 0 + 1
{ forks.1 }== forks (Leaf2 ) + 1
{ Fall.1 }== forks t + 1
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/33'
&
$
%
Beweis: leaves t == forks t + 1 {Fall.2}
Induktionsvariable: t
{Fall.2}: t == Fork2 l r
leaves t
{ Fall.2 }== leaves (Fork2 l r)
{leaves.2}== leaves l + leaves r
{ Ind.A. }== forks l + 1 + leaves r
{ Kommut.}== 1 + forks l + leaves r
{ Ind.A. }== 1 + forks l + forks r + 1
{ forks.2}== forks (Fork2 l r) + 1
{ Fall.2 }== forks t + 1
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/34'
&
$
%
Ungleichungs-Beweis: sumT t <= leaves t * maxT t
Kette von <= und == statt Kette von ==
leaves (Leaf2 ) = 1 -- leaves.1
leaves (Fork2 l r) = leaves l + leaves r -- leaves.2
sumT (Leaf2 x) = x -- sumT.1
sumT (Fork2 l r) = sumT l + sumT r -- sumT.2
maxT (Leaf2 x) = x -- maxT.1
maxT (Fork2 l r) = max (maxT l) (maxT r) -- maxT.2
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/35'
&
$
%
Ungleichungs-Beweis: sumT t <= leaves t * maxT t {Fall.1}
Induktionsvariable: t
{Fall.1}: t == Leaf2 x
sumT t
{ Fall.1 }== sumT (Leaf2 x)
{ sumT.1 }== x
{Neutr. *}== 1 * x
{leaves.1}== leaves (Leaf2 x) * x
{ maxT.1 }== leaves (Leaf2 x) * maxT (Leaf2 x)
{ Fall.1 }== leaves t * maxT (Leaf2 x)
{ Fall.1 }== leaves t * maxT t
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/36'
&
$
%
Ungleichungs-Beweis: sumT t <= leaves t * maxT t {Fall.2}Induktionsvariable: t
{Fall.2}: t == Fork2 l r
sumT t
{ Fall.2 }== sumT (Fork2 l r)
{ sumT.2 }== sumT l + sumT r
{ Ind.A. }<= leaves l * maxT l + sumT r
{ Ind.A. }<= leaves l * maxT l + leaves r * maxT r
{ max }<= leaves l * (max (maxT l) (maxT r)) + leaves r * maxT r
{ max }<= leaves l * (max (maxT l) (maxT r))
+ leaves r * (max (maxT l) (maxT r))
{ Distr. }== (leaves l + leaves r) * max (maxT l) (maxT r)
{leaves.2}== leaves (Fork2 l r) * max (maxT l) (maxT r)
{ maxT.2 }== leaves (Fork2 l r) * maxT (Fork2 l r)
{ Fall.2 }== leaves t * maxT (Fork2 l r)
{ Fall.2 }== leaves t * maxT t
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/37'
&
$
%
Beobachtungen
• mehrmalige Anwendung der Induktionsannahme kann notig oder nutzlich sein
– bei Strukturen mit mehr als einer rekursiven Teilstruktur (z.B. Baume)
– bei mehrmaligem Auftreten der Induktionsvariablen
• oft kann man schnell die Gleichungskette finden, wenn man
1. von oben abwarts zur Mitte bzw.
2. von unten aufwarts zur Mitte
Funktionsdefinitionen einsetzt (Unfolding) und vereinfacht
• bei Strukturen mit einem Basisfall und einem Induktionsfall werden oft die{.1}-Regeln beim Beweis des Basisfalles und die {.2}-Regeln beim Beweis desInduktionsfalles gebraucht.
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/38'
&
$
%
Listengesetze und Fold
Achtung: Einschrankung auf endliche Listen ohne explizite Erwahnung
• Dekompositionssatze: zerlegen einer Liste
• Dualitatssatze: Beziehung zwischen foldl und foldr
• Fusionssatze: verschmelzen einer Berechnung nach einem fold mit dem fold
• Homomorphiesatze: wann ist eine Funktion ein Listenhomomorphismus?
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/39'
&
$
%
Definitionen
foldl f e [] = e -- foldl.1
foldl f e (x:xs) = foldl f (f e x) xs -- foldl.2
foldr f e [] = e -- foldr.1
foldr f e (x:xs) = f x (foldr f e xs) -- foldr.2
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/40'
&
$
%
Fold-Dekompositionssatze
• (foldl-dec.):foldl f a (xs++ys) = foldl f (foldl f a xs) ys
• (foldr-dec.):foldr f a (xs++ys) = foldr f (foldr f a ys) xs
falls f assoziativ mit neutralem Element e:
• (foldl-ass.):foldl f e (xs++ys) = f (foldl f e xs) (foldl f e ys)
• (foldr-ass.):foldr f e (xs++ys) = f (foldr f e xs) (foldr f e ys)
Beweise: zum uben
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/41'
&
$
%
Erster Dualitatssatz (1)
Sei f assoziativ mit neutralem Element e.Dann gilt fur jede endliche Liste xs: foldr f e xs = foldl f e xs
Beweis durch Induktion uber die Struktur von xs
{Fall.1}: xs == []
foldr f e xs
{ Fall.1 }== foldr f e []
{foldr.1 }== e
{foldl.1 }== foldl f e []
{ Fall.1 }== foldl f e xs
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/42'
&
$
%
Erster Dualitatssatz (2)
{Fall.2}: xs == (y:ys)
foldr f e xs
{ Fall.2 }== foldr f e (y:ys)
{ foldr.2 }== f y (foldr f e ys)
{ Ind.Ann.}== f y (foldl f e ys)
{Hilfsbew.}== foldl f (f y e) ys
{Neut. e } == foldl f y ys
{Neut. e } == foldl f (f e y) ys
{ foldl.2 }== foldl f e (y:ys)
{ Fall.2 }== foldl f e xs
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/43'
&
$
%
Erster Dualitatssatz, Hilfsbeweis (1) Fehlversuch!
zu zeigen: f y (foldl f e ys) = foldl f (f y e) ys
{Fall.1}: ys == []
f y (foldl f e ys)
{ Fall.1 }== f y (foldl f e [])
{ foldl.1 }== f y e
{ foldl.1 }== foldl f (f y e) []
{ Fall.1 }== foldl f (f y e) ys
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/44'
&
$
%
Erster Dualitatssatz, Hilfsbeweis (2) Fehlversuch!
zu zeigen: f y (foldl f e ys) = foldl f (f y e) ys
{Fall.2}: ys == (z:zs)
f y (foldl f e ys)
{ Fall.2 }== f y (foldl f e (z:zs))
{ foldl.2 }== f y (foldl f (f e z) zs)
{ Neut.e. }== f y (foldl f z zs)
{ ? }== foldl f (f y z) zs
{ foldl.2 }== foldl f y (z:zs)
{ Neut. e }== foldl f (f y e) (z:zs)
{ Fall.2 }== foldl f (f y e) ys
z ist i.a. nicht gleich dem neutralen Element.Induktionsannahme muss verallgemeinert werden!
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/45'
&
$
%
Erster Dualitatssatz, Hilfsbeweis (1) richtig
zu zeigen: f y (foldl f x ys) = foldl f (f y x) ys
{Fall.1}: ys == []
f y (foldl f x ys)
{ Fall.1 }== f y (foldl f x [])
{ foldl.1 }== f y x
{ foldl.1 }== foldl f (f y x) []
{ Fall.1 }== foldl f (f y x) ys
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/46'
&
$
%
Erster Dualitatssatz, Hilfsbeweis (2) richtig
zu zeigen: f y (foldl f x ys) = foldl f (f y x) ys
{Fall.2}: ys == (z:zs)
f y (foldl f x ys)
{ Fall.2 }== f y (foldl f x (z:zs))
{ foldl.2 }== f y (foldl f (f x z) zs)
{ Ind.Ann.}== foldl f (f y (f x z)) zs
{ Ass. f }== foldl f (f (f y x) z) zs
{ foldl.2 }== foldl f (f y x) (z:zs)
{ Fall.2 }== foldl f (f y x) ys
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/47'
&
$
%
Zweiter Dualitatssatz (1)
foldr f x xs = foldl (flip f) x (reverse xs)
Beweis durch Induktion uber die Struktur von xs
{Fall.1}: xs == []
foldr f x xs
{Fall.1 }== foldr f x []
{foldr.1}== x
{foldl.1}== foldl (flip f) x []
{ rev.1 }== foldl (flip f) x (reverse [])
{Fall.1 }== foldl (flip f) x (reverse xs)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/48'
&
$
%
Zweiter Dualitatssatz (2)
{Fall.2}: xs == y:ys
foldr f x xs
{ Fall.2 }== foldr f x (y:ys)
{ foldr.2 }== f y (foldr f x ys)
{ flip }== flip f (foldr f x ys) y
{ foldl.1 }== foldl (flip f) (flip f (foldr f x ys) y) []
{ foldl.2 }== foldl (flip f) (foldr f x ys) [y]
{ Ind.Ann. }== foldl (flip f) (foldl (flip f) x (reverse ys)) [y]
{foldl-dec.}== foldl (flip f) x (reverse ys ++ [y])
{reverse.2 }== foldl (flip f) x (reverse (y:ys))
{ Fall.2 }== foldl (flip f) x (reverse xs)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/49'
&
$
%
Anwendung des zweiten Dualitatssatzes
Herleitung einer effizienten Implementierung von reverse
reverse xs Spezifikation, s.u.
{ id }== id (reverse xs)
{foldr/id}== foldr (:) [] (reverse xs)
{ 2.Dual }== foldl (flip (:)) [] (reverse (reverse xs))
{rev/rev }== foldl (flip (:)) [] xs Implementierung linearer Zeit
2. Dualitatssatz verwendet Spezifikation von reverse mit quadratischer Zeit!
reverse [] = [] -- reverse.1
reverse (x:xs) = reverse xs ++ [x] -- reverse.2
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/50'
&
$
%
Fusionssatze (1: foldr-Fusion)
Sei f strikt und gelte f (g x y) = h x (f y).Dann gilt: f . foldr g a = foldr h (f a)
g ah
x
f
x’
h ah
x x’
f
g g
x x’
afy
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/51'
&
$
%
Fusionssatze (2: foldl-Fusion)
Sei f strikt und gelte f (g x y) = h (f x) y.Dann gilt: f . foldl g a = foldl h (f a)
hg fa
yy’
h hfa
yy’
g g
y’
xa
y
f
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/52'
&
$
%
Spezialfalle der Fusionssatze
• fold/map-Fusionfoldr f a . map g = foldr (f . g) a
• bookkeeping-law: sei f assoziativ mit neutralem Element e; dann gilt:foldr f e . concat = foldr f e . map (foldr f e)
Anwendung Buchfuhrung (f=(+),e=0):sum . concat = sum . map sum
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/53'
&
$
%
Monoid
Monoid: Halbgruppe mit neutralem Element, Notation (M,⊕, e)
• M Menge
• (⊕): M → M → M eine totale Funktion, ⊕ assoziativ
• e ist neutrales Element bzgl. ⊕
Haskell-Beispiele:
• (Integer,+,0), naturliche Zahlen mit Addition
• ([a],++,[]), (endliche) Listen mit append
• (a->a, . ,id), Funktionen mit Komposition
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/54'
&
$
%
Monoidhomomorphismus
• seien M1 = (M1,⊕1, e1) und M2 = (M2,⊕2, e2) Monoide
• Monoidhomomorphismus: Abbildung h : M1 → M2 mit den Eigenschaften
1. h(e1) = e2
2. ∀m,m′ ∈ M1 : h(m⊕1 m′) = h(m)⊕2 h(m′)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/55'
&
$
%
Listenhomomorphismen
Beispiele fur Homomorphismen von M1 = ([a], ++, []) nach M2 = (Integer, +, 0):
• length
• sum
• sum . map f
es gibt viele Homomorphismen von M1 nach M2
Unterscheidung: durch Erzeugendensystem
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/56'
&
$
%
Erzeugendensystem• sei M = (M,⊕, e) ein Monoid
• Erzeugendensystem: Teilmenge A ⊆ M , sodass jedes m ∈ M durchwiederholte Anwendung von ⊕ aus Elementen von A und e konstruiertwerden kann.
• sei M1 = ([a], ++, [])
• Satz: die einelementigen Listen bilden ein Erzeugendensystem fur M1
(Beweis: siehe Thiemann-Buch (6.1))
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/57'
&
$
%
Beispiele fur Listenhomomorphismen
Beispiele fur Homomorphismen von M1 = ([a], ++, []) nach M2 = (M2,⊕, e):
Name h [x] e (⊕)
id [x] [] (++)
map f [f x] [] (++)
reverse [x] [] (flip (++))
length 1 0 (+)
sum x 0 (+)
product x 1 (*)
sum . map f f x 0 (+)
foldr g e . map f (*) f x e g
(*) g ist assoziativ mit neutralem Element e
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/58'
&
$
%
Erster HomomorphiesatzOriginal: Bird, 1988
eine Funktion h::[a]->b ist ein Homomorphismus
⇐⇒
es gibt
• eine assoziative Funktion g mit neutralem Element e und
• eine Funktion f mit der Eigenschaft f x = h [x],
sodass h sich schreiben lasst als: h = foldr g e . map f
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/59'
&
$
%
Definitionen
Eine Listenfunktion h heisst
• ⊕-linksgerichtet fur einen binaren Operator ⊕ gdw., fur alle Elemente a undListen y gilt: h ([a] ++y) = a⊕ h y
• ⊗-rechtsgerichtet fur einen binaren Operator ⊗ gdw., fur alle Listen x undElemente a gilt: h (x ++[a]) = hx⊗ a
Anm.: es wird nicht gefordert, dass ⊕ bzw. ⊗ assoziativ sind.
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/60'
&
$
%
Zweiter Homomorphiesatz (Spezialisierungssatz)Original: Bird, 1987
Jeder Listenhomomorphismus lasst sich sowohl als eine linksgerichtete als auch alseine rechtsgerichtete Listenfunktion ausdrucken, d.h.
• sei h von ([α],++,[ ]) nach (β,~,e) ein Homomorphismus
• dann gibt es
1. einen Operator ⊕ mit a⊕ y = f a ~ y, sodass h = foldr (⊕) e
2. einen Operator ⊗ mit x⊗ b = x ~ f b, sodass h = foldl (⊗) e
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/61'
&
$
%
Dritter HomomorphiesatzBeweis und Beispiel nach Gibbons, 1995
Wenn h linksgerichtet und rechtsgerichtet ist,dann ist h ein Homomorphismus.
Zu zeigen: wenn h links- und rechtsgerichtet ist, dann gibt es einen Operator ¯,so dass h (x ++ y) = hx¯ h y. ¯ assoziativ weil ++ assoziativ.Wir suchen eine explizite Definition fur ¯, d.h., eine Funktion g mit
1. t¯ u = h (g t ++ g u)
2. h ◦ g ◦ h = h
Idee: g liefert zu x und y aquivalente Reprasentanten im Definitionsbereich von h.
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/62'
&
$
%
Hilfslemma 1 zum Beweis des dritten Homomorphiesatzes
Hilfslemma 1.Fur jede berechenbare Funktion h mit aufzahlbarem Definitionsbereich gibt eseine berechenbare (mglw. nicht totale) Funktion g, so dass gilt: h ◦ g ◦ h = h.
Beweis. Um g t zu berechnen, kann man den Definitionsbereich von h aufzahlen,und das erste x zuruckgeben, fur das gilt: hx = t. Falls t im Wertebereich von h
liegt, terminiert dieses Verfahren.
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/63'
&
$
%
Hilfslemma 2 zum Beweis des dritten Homomorphiesatzes
Hilfslemma 2:Die Listenfunktion h ist ein Homomorphismus gdw. fur alle Listen v, w, x und y
gilt: h v = h x ∧ h w = h y =⇒ h (v ++w) = h (x ++y) .
Beweis:
• h-Homomorphismus ⇒ ∃⊕ :: h(v ++w) = h v ⊕ hw = hx⊕ h y = h(x ++y)
• gelte h v = hx ∧ hw = h y =⇒ h (v ++ w) = h (x ++ y) (*)
– wahle g, sodass h ◦ g ◦ h = h (Hilfslemma 1)
– definiere ¯ durch t¯ u = h (g t ++g u)
hx¯ h y = {Definition ¯}h (g (hx) ++ g (h y)) = { setze v = g (hx) und w = g (h y) }h (v ++w) = { h v = hx ∧ hw = h y ∧ (∗) }h (x ++y)
also: h ist Homomorphismus mit Operator ¯ (neutrales Element: h [ ]).
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/64'
&
$
%
Beweis des dritten Homomorphiesatzes
zu zeigen: h ist links- und rechtsgerichtet =⇒ h Homomorphismus
• gelte: h ist links- und rechtsgerichtet: h = foldr (⊕) e = foldl (⊗) e
• zu zeigen: h Homomorphismus
• zeige aquivalente Aussage nach Hilfslemma 2:h v = hx ∧ h w = h y =⇒ h(v ++ w) = h(x ++y)
– gelte h v = h x ∧ h w = h y
– zu zeigen: h (v ++ w) = h (x ++ y) [nachste Folie]
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/65'
&
$
%
Beweis:
h (v ++ w)= { h ist linksgerichtet }foldr (⊕) e (v ++ w)= { foldr -Dekomposition }foldr (⊕) (foldr (⊕) e w) v= { hw = h y }foldr (⊕) (foldr (⊕) e y) v= { foldr -Dekomposition }foldr (⊕) e (v ++ y)= { h ist linksgerichtet }h (v ++ y)= { h ist rechtsgerichtet }foldl (⊗) e (v ++ y)= { foldl -Dekomposition }foldl (⊗) (foldl (⊗) e v) y= { h v = hx }foldl (⊗) (foldl (⊗) e x) y= { foldl -Dekomposition }foldl (⊗) e (x ++ y)= { h ist rechtsgerichtet }h (x ++ y)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/66'
&
$
%
Anwendung: Herleitung eines Sortierverfahrens
Einfugen in eine sortierte Liste: ins
ins a [] = [a]
ins a (b:x) | a<=b = a : b : x
| a>b = b : ins a x
ins’ = flip ins
Sortieren basieren auf einfugen:
• linksgerichtet: sort’ = foldr ins []
• rechtsgerichtet: sort = foldl ins’ []
Folge aus dem dritten Homomorphiesatz: sort ist ein Homomorphismus.
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/67'
&
$
%
Herleitung eines Sortierverfahrens
• sowohl linksgerichtetes als auch rechtsgerichtetes Einfugesortieren brauchtZeit θ(n2) fur Liste der Lange n
• gesucht: Losung, bei der die Liste in zwei etwa gleich große Teile geteilt wird,um Zeit θ(n · log n) zu erreichen.
• Plan: Herleitung eines Sortierverfahrens, das
– Teilung der unsortierten Liste in zwei beliebige Teile ungleich [ ] zulasst
– links- und rechtsgerichtetes Einfugesortieren als Spezialfalle enthalt
• bestimme Implementierung des Operators ¯, so dass gilt:sort u ¯ sort v == sort (u ++ v).
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/68'
&
$
%
Herleitung eines Sortierverfahrensu ¯ v{ u, v sortiert } =sort u ¯ sort v{ sort ist Homomorphismus } =sort (u ++ v){ sort } =foldl ins’ [] (u ++ v){ foldl-Dekomposition } =foldl ins’ (foldl ins’ [] u) v{ sort } =foldl ins’ (sort u) v{ u sortiert } =foldl ins’ u v{ setze mergeQ = foldl ins’ (*) } =mergeQ u v
(*) Name mergeQ wegen Eigenschaft von foldl ins’:
mergeQ u [] == foldl ins’ u [] == u
mergeQ u (b:v) == foldl ins’ u (b:v)
== foldl ins’ (ins’ u b) v == mergeQ (ins’ u b) v
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/69'
&
$
%
Herleitung eines Sortierverfahrens
u ¯ v = mergeQ u v
mergeQ u [] = u
mergeQ u (b:v) = mergeQ (ins’ u b) v
• mergeQ verwendet Eigenschaft, dass u sortiert ist
• mergeQ verwendet nicht, dass v sortiert ist⇒ immer noch quadratische Laufzeit!
Verbesserung von mergeQ zu merge:Umschreiben unter Ausnutzung der Sortiertheit von v
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/70'
&
$
%
Verbesserung von mergeQ zu merge
Abkurzung: sei a ein Element und v eine Liste:a ≤ v heisst: fur alle b in v gilt a ≤ b
Hilfslemma:a ≤ x ∧ a ≤ y ⇒ (foldl ins’ (a:x) y) = (a : foldl ins’ x y)
Beweis: durch Induktion
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/71'
&
$
%
Verbesserung von mergeQ zu merge
• zweite Liste ist leer
merge u []{ merge == mergeQ } =
mergeQ u []{ mergeQ.1 } =
u
• erste Liste ist leer
merge [] v{ merge == mergeQ } =
mergeQ [] v{ Abk. mergeQ } =
foldl ins’ [] v{ sort } =sort v{ v ist sortiert } =v
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/72'
&
$
%
Verbesserung von mergeQ zu merge
• beide Listen sind nicht leer
merge (a:u) (b:v){ merge == mergeQ } =
mergeQ (a:u) (b:v){ Abk. mergeQ } =
foldl ins’ (a:u) (b:v){ foldl.2 } =foldl ins’ (ins’ (a:u) b) v=. . .
weiter mit Fallunterscheidung a < b und a ≥ b
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/73'
&
$
%
Verbesserung von mergeQ zu merge (a < b)
Annahme: (a:u) und (b:v) sortiert und a< b
also gilt: a≤ u, a≤ v und a≤ (ins’ u b)
merge (a:u) (b:v){ Schritte von letzter Folie } =
foldl ins’ (ins’ (a:u) b) v{ ins’ ∧ a<b } =foldl ins’ (a : ins’ u b) v{ Hilfslemma } =a : foldl ins’ (ins’ u b) v{ foldl.2 } =a : foldl ins’ u (b:v){ Abk. mergeQ } =a : mergeQ u (b:v)
{ merge == mergeQ } =a : merge u (b:v)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/74'
&
$
%
Verbesserung von mergeQ zu merge (a ≥ b)
Annahme: (a:u) und (b:v) sortiert und a≥ b
also gilt: b≤ (a:u) und b≤ v
merge (a:u) (b:v){ Schritte von vorletzter Folie } =
foldl ins’ (ins’ (a:u) b) v{ ins’ ∧ a≥b } =foldl ins’ (b:a:u) v{ Hilfslemma } =b : foldl ins’ (a:u) v{ Abk. mergeQ } =b : mergeQ (a:u) v
{ merge == mergeQ } =b : merge (a:u) v
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/75'
&
$
%
Verbesserung von mergeQ zu merge, Fazit
damit ergibt sich fur merge . . .
merge [] v = v
merge u [] = u
merge (a:u) (b:v) | a<b = a : merge u (b:v)
| a>=b = b : merge (a:u) v
. . . und die Einfugefunktionen sind Spezialfalle davon:
ins a xs == merge [a] xs
ins’ xs a == merge xs [a]
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/76'
&
$
%
Resultierendes Sortierverfahren: mergesort
mergesort :: Ord a => [a] -> [a]
mergesort [] = [] -- neutrales Element
mergesort [x] = [x] -- Erzeugendensystem
mergesort xs = let (ys,zs) = splitAt (length xs ‘div‘ 2) xs
u = mergesort ys
v = mergesort zs
in merge u v -- Operator im Wertebereich
-- des Homomorphismus
merge :: Ord a => [a] -> [a] -> [a]
merge [] v = v
merge u [] = u
merge (a:u) (b:v) | a<b = a : merge u (b:v)
| a>=b = b : merge (a:u) v
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/77'
&
$
%
Programmtransformationen
gehen zuruck auf Burstall/Darlington (1977): “A transformation system fordeveloping recursive programs”
Anwendung: transformiere ineffizientes in effizientes Programm
Arten von Transformationsschritten
• unfold: ersetzen eines Funktionsnamens durch den Funktionsrumpf
• fold: Umkehrung von unfold
• def: einfuhren lokaler Definitionen (let/where)
• spec: Spezialisierung
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/78'
&
$
%
Beispiel: Fibonacci-Funktion
Ausgangspunkt: sehr ineffizientes Programm
fib 0 = 0 -- fib.0
fib 1 = 1 -- fib.1
fib n | n>1 = fib (n-2) + fib (n-1)
fib (n+2) = fib n + fib (n+1) -- fib.2
Performance-steigernde Transformationen
(1) einfugen einer lokalen Definition:
fib (n+2) = z1 + z2 where (z1,z2) = (fib n, fib (n+1))
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/79'
&
$
%
(2) Definiere eine Hilfsfunktion fur die rechte Seite von fib (n+2)
fib2 n = (fib n, fib (n+1)) -- fib2
(3) Anwendung von (spec)
(a) fib2 0 = (fib 0, fib 1) = (0,1)
(b)fib2 (n+1){ Def. fib2 } =(fib (n+1), fib (n+2))
{ unfold } =(fib (n+1), fib (n+1) + fib n)
{ where } =(z2,z2+z1) where (z1,z2) = fib2 n
Damit:fib n{ fib.2 } =z1 where (z1,z2) = fib2 n
{ fst } == fst (fib2 n)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/80'
&
$
%
fib2 :: Integer -> (Integer,Integer)
fib2 0 = (0,1)
fib2 n | n>0 = (z2,z2+z1) where (z1,z2) = fib2 (n-1)
fib :: Integer -> Integer
fib n = fst (fib2 n)
oder, Rekursion ersetzt durch foldl
fib :: Integer -> Integer
fib n = let f (z1,z2) = const (z2,z2+z1)
in fst (foldl f (0,1) [1..n])
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/81'
&
$
%
Homomorphieeigenschaften bei fib
• Ziel: Optimierung der foldl-Berechnung
• reprasentieren n durch Liste von () der Lange n
• Homomorphismus h : ([()], ++, []) → (N2 → N2, ◦, id)
fib :: Integer -> Integer
fib n = fst (fibHom [ () | _ <- [1..n] ] (0,1))
fibHom :: [()] -> ((Integer,Integer)->(Integer,Integer))
fibHom xs = let f (z1,z2) = (z2,z2+z1)
in foldr (.) id (map (const f) xs)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/82'
&
$
%
Weitere Verbesserungen
• explizite Funktionskomposition ist speicherplatzaufwandig
• suchen nach algebraischen Moglichkeiten zur Kompaktifizierung derKomposition
wir wissen:
• f ist eine lineare Abbildung f(z1, z2) = (z2, z2 + z1) = ( ( 0 11 1 ) ( z1
z2 ) )T
• Komposition linearer Abbildungen (g ◦ f) entspricht Matrixmultiplikation
nachster Schritt: Umstellung des foldr-Operators auf Matrixmultiplikation
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/83'
&
$
%
Einfuhrung eines Typs von 2x2-Matrizen
data M2 a = M2 {upperLeft,upperRight,lowerLeft,lowerRight::a}deriving (Eq,Show)
unitMat, fibMat :: M2 Integer
unitMat = M2 1 0
0 1 -- (z1,z2) -> (z1,z2)
fibMat = M2 0 1
1 1 -- (z1,z2) -> (z2,z1+z2)
instance Num a => Num (M2 a) where
(M2 a b
c d) *
(M2 e f
g h) = M2 (a*e+b*g) (a*f+b*h)
(c*e+d*g) (c*f+d*h)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/84'
&
$
%
Fibonacci-Berechnung mittels Matrixmultiplikation
fib :: Integer -> Integer
fib n = lowerLeft (fibHom’ [ () | _ <- [1..n] ])
fibHom’ :: [()] -> M2 Integer
fibHom’ xs = foldr (*) unitMat (map (const fibMat) xs)
-- war: foldr (.) id (map (const f ) xs)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/85'
&
$
%
weitere Optimierung: effiziente Potenzierung
fibOpt :: Integer -> Integer
fibOpt n = lowerLeft $ fibMat^n
Laufzeitvergleiche (Zeiten mit ghci in Sekunden, ohne Ausgabe)
n binar rekursiv linear rekursiv foldr (.) foldr (*) fibOpt
30 5.38 – – – –
31 8.70 – – – –
1000 – 0.01 0.00 0.01 0.00
10000 – 0.12 0.10 0.42 0.00
100000 – 12.19 11.62 87.28 0.01
1000000 – – – – 0.26
10000000 – – – – 8.39
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/86'
&
$
%
Problem der maximalen Segmentsummegesucht: Maximum der Summen aller Segmente einer Liste ganzer Zahlen
Bsp.: [-3,4,-7,2,4,-5,2,3,7,-2,-1,9,3,-15,6,-2,9,-7] → 22
imperative Problemlosungen (beschrieben in: Jon Bentley: Programming Pearls)
• Test aller Segmente: Θ(n3)
• inkrementelles Update von Teilsummen: Θ(n2)
• Divide-and-Conquer Losung: Θ(n · log n)
• Scan-Algorithmus: Θ(n)
Im folgenden: formale Herleitungen
• funktionaler Scan-Algorithmus Θ(n)
• paralleler D&C-Algorithms Θ(log n)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/87'
&
$
%
Problem der maximalen SegmentsummeSpezifikation:
mss :: [Integer] -> Integer
mss = let segs = concat . map inits . tails
in maximum . map sum . segs
• tails: finale Segmente, Bsp.: tails [1,2,3] Ã [[1,2,3],[2,3],[3],[]]
• inits: initiale Segmente, Bsp.: map inits (tails [1,2,3]) Ã[[[],[1],[1,2],[1,2,3]], [[],[2],[2,3]], [[],[3]], [[]]]
• segs: alle SegmenteBsp.: segs [1,2,3] Ã[[],[1],[1,2],[1,2,3],[],[2],[2,3],[],[3],[]]]
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/88'
&
$
%
Reduktion der Komplexitat von Θ(n3) auf Θ(n)
mss{Definition mss} =maximum . map sum . concat . map inits . tails
{concat/map} =maximum . concat . map (map sum) . map inits . tails
{map/.} =maximum . concat . map (map sum . inits) . tails
{ bookkeeping } =maximum . map maximum . map (map sum . inits) . tails
{map/.} =maximum . map (maximum . map sum . inits) . tails
{map/sum} =maximum . map (maximum . scanl (+) 0) . tails
{ Def. maximum } =maximum . map (foldr1 max . scanl (+) 0) . tails
{ foldr Fusion } =maximum . map (foldr (¯) 0) . tails
where x¯y = max 0 (x+y){ map/foldr } =
maximum . scanr (¯) 0 where x¯y = max 0 (x+y)
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/89'
&
$
%
Akkumulierung der Zwischenergebnisse
Def.: x ¯ y = max 0 (x+y)
mss{ vorige Folie } =maximum . scanr (¯) 0{ Def. maximum } =foldr1 max . scanr (¯) 0{ Tupling } =snd . foldr (⊗) (0,0)
max max max max
0
4
−8 5 −2 4
0 7 2 4
0477
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/90'
&
$
%
Akkumulierung der Zwischenergebnisse
mss = snd . foldr (⊗) (0,0)
max max max max
0
4
−8 5 −2 4
0 7 2 4
0477
x ⊗ (acc,res) = let acc’ = max 0 (x+acc) -- x ¯ acc
in (acc’, max res acc’)
Interpretation des Akkumulatorinhalts: Wert des maximalen initialen Segments
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/91'
&
$
%
Anwendung von Homomorphieeigenschaften
1. segs = concat . map inits . tails:mss = let x ⊗ (acc,res) = let acc’ = max 0 (x+acc)
in (acc’, max acc’ res)
in snd . foldr (⊗) (0,0)
Akkumulator: Wert des maximalen initialen Segments (mis)
2. segs = concat . map tails . inits:mss = let (acc,res) ⊕ x = let acc’ = max 0 (acc+x)
in (acc’, max acc’ res)
in snd . foldl (⊕) (0,0)
Akkumulator: Wert des maximalen finalen Segments (mfs):
mss ist eine Projektion einer linksgerichteten und rechtsgerichteten Listenfunktion.
Dritter Homomorphiesatz: mss ist Projektion eines Homomorphismus h.
Suche nach dem Kombinationsoperator ~: h (x++y) == h x ~ h y
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/92'
&
$
%
Suche nach dem Kombinationsoperator ~Der Homomorphismus muss enthalten:
1. maximale Segmentsumme mss
2. Summe des maximalen initialen Segments mis
3. Summe des maximalen finalen Segments mfs
Problem: wie erhalt man aus x und y die Werte fur x ~ y?
1. mssx~y = max (max mssx mssy) (mfsx + misy)
2. misx~y = max misx (sumx + misy)
3. mfsx~y = max mfsy (sumy + mfsx)
zusatzliches Tupling mit der Summe aller Werte notig:
4. sumx~y = sumx + sumy
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/93'
&
$
%
mss als Projektion eines Homomorphismus
mss :: [Integer] -> Integer
mss = prj1aus4 . foldr g e . map f
where e = (0,0,0,0)
g (mssX,misX,mfsX,sumX)
(mssY,misY,mfsY,sumY) = (max (max mssX mssY)
(mfsX + misY),
max misX (sumX + misY),
max mfsY (sumY + mfsX),
sumX + sumY)
f x = let xnn = max 0 x
in (xnn,xnn,xnn,x)
prj1aus4 (a,b,c,d) = a
Ubungsaufgabe: Erweiterung, so dass auch Segmentgrenzen geliefert werden
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/94'
&
$
%
mss als Divide-and-Conquer
mss :: [Integer] -> Integer
mss [] = 0
mss xs = prj1aus4 (dc pred basic divide combine xs) where
pred xs = length xs == 1
basic [x] = let xnn = max 0 x
in (xnn,xnn,xnn,x)
divide xs = let (ys,zs) = splitAt (length xs ‘div‘ 2) xs
in [ys,zs]
combine _ [(mssX,misX,mfsX,sumX),
(mssY,misY,mfsY,sumY)] = (max (max mssX mssY)
(mfsX + misY),
max misX (sumX + misY),
max mfsY (sumY + mfsX),
sumX + sumY)
prj1aus4 (a,b,c,d) = a
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.
Funktionale Programmierung (WS2005/2006) 4/95'
&
$
%
Beobachtungen fur mss
• Laufzeitreduktion von Θ(n3) (Spezifikation)
– sequenziell: auf Θ(n)
– parallel: durch D&C auf Θ(log n)
• wichtige Gesetze/Techniken
– bookkeeping: vermeidet temporare Listen
– fold-Fusion und map-Komposition: vermeidet Mehrfachdurchgange
– Tupling: erhoht die Flexibilitat der verknupfenden Operatoren∗ Zwischenergebnisse fur Fold-Fusion∗ Assoziativitat fur Homomorphismen
Dr. Christoph Herrmann c©Universitat Passau, Lehrstuhl Prof. Lengauer, Ph.D.