8 · Listenverarbeitung
8.3
�
Induktion über Listen · 8.3
Induktion über Listen
Dank referenzieller Transparenz kann man Behauptungen wie
rev ≡ reverse
relativ einfach beweisen.
�
Beweise über listenverarbeitende Funktionen können häufig mittels
Induktion über Listen, analog zu Induktionsbeweisen für Behauptungen
über Elemente aus N, geführt werden:
1. Induktionsanfang (aka. Induktionsverankerung).
�
Beweise die Aussage mit der leeren Liste [].
2. Induktionsschritt von xs zu x : xs.
�
Übung
Dabei wird die Induktionshypothese (die Aussage mit einer beliebigen, festen
Liste xs) verwendet, um die Aussage mit x : xs für alle x zu zeigen.
Für alle Listen xs gilt xs ++ [ ] ≡ xs.
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
226
8 · Listenverarbeitung
Beispiel
�
Induktion über Listen · 8.3
Beweisen rev xs ≡ reverse xs für alle Listen xs.
Da rev xs � shunt [ ] xs (cf. Seite 224), genügt es, die allgemeinere
Behauptung zu zeigen:
shunt ys xs
≡
reverse xs ++ ys
, für alle xs, ys :: [α]
Induktionsverankerung Sei xs = [ ], und ys :: [α] beliebig.
shunt ys [ ]
Stefan Klinger · DBIS
≡
≡
≡
ys
[ ] ++ ys
reverse [ ] ++ ys
Informatik 2 · Sommer 2016
(shunt.1)
(++.1)
(reverse.1)
227
8 · Listenverarbeitung
Induktion über Listen · 8.3
Induktionshypothese Für ein beliebiges, festes xs :: [α], und für alle ys :: [α]
gelte:
shunt ys xs ≡ reverse xs ++ ys
Induktionsschritt Von xs zu x : xs. Seien x :: α, und ys :: [α].
Mit dem xs aus der Induktionshypothese gilt:
shunt ys (x : xs)
≡
≡
≡
≡
≡
≡
shunt (x : ys) xs
reverse xs ++ (x : ys)
reverse xs ++ (x : ([ ] ++ ys))
reverse xs ++ ([x] ++ ys)
(reverse xs ++ [x]) ++ ys
reverse (x : xs) ++ ys
(shunt.2)
(Hypothese)
(++.1 rückw.)
(++.2 rückw.)
(++ assoziativ)
(reverse.2)
Übung Die hier verwendete Annahme über die Assoziativität von ++ müssen wir
ebenfalls noch beweisen: xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs. Auch hier führt
Listeninduktion über den Parameter zum Ziel, über den die Rekursion der betrachteten
Funktion ++ formuliert ist, also xs.
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
228
8 · Listenverarbeitung
8.4
Programm-Synthese · 8.4
Programm-Synthese
Bei der Beweisführung über Programme werden Eigenschaften eines
gegebenen Programms Schritt für Schritt nachvollzogen und dadurch
bewiesen (s. rev und reverse).
Programm-Synthese kehrt dieses Prinzip um:
�
Gegeben ist eine formale Spezifikation eines Problems,
�
gesucht ist ein problemlösendes Programm, das durch schrittweise
Umformung der Spezifikation gewonnen (synthetisiert) wird.
Wenn die Transformationen diszipliniert vorgenommen werden, kann die
Synthese als Beweis dafür gelesen werden, dass das Programm die
Spezifikation erfüllt (der Traum aller Software-Ingenieure).
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
229
8 · Listenverarbeitung
Programm-Synthese · 8.4
Beispiel Die Funktion init der standard prelude bestimmt das initiale
Segment ihres Listenargumentes, also etwa
init [1..10] � [1, 2, 3, 4, 5, 6, 7, 8, 9].
�
Damit wäre eine naheliegende Spezifikation für init die folgende:
init xs = take (length xs - 1) xs
wobei xs endlich und nicht leer
“Nimm alle Elemente von xs, aber nicht das letzte Element”
�
Die Synthese versucht eine effizientere Variante von init abzuleiten
(die Spezifikation wäre ja prinzipiell schon ausführbar, traversiert xs zur
Berechnung des Ergebnisses aber zweimal).
Für die Synthese instantiieren wir xs
1. mit [x] und
2. mit x1 : x2 : xs.
Jede nichtleere Liste besitzt die eine oder die andere Form.
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
230
8 · Listenverarbeitung
Programm-Synthese · 8.4
Fall 1 [x]
init [x]
=
=
— Instanziierung
Spezifikation
take (length [x] − 1) [x]
length, Arithmetik
take 0 [x]
=
take.1
[]
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
231
8 · Listenverarbeitung
Programm-Synthese · 8.4
Fall 2 x1 : x2 : xs
init (x1 : x2 : xs)
=
=
— Instanziierung
Spezifikation
take (length (x1 : x2 : xs) − 1) (x1 : x2 : xs)
length, Arithmetik
take (length xs + 1) (x1 : x2 : xs)
=
take.3
x1 : take (length xs) (x2 : xs)
=
=
length.2, Arithmetik
x1 : take (length (x2 : xs) − 1) (x2 : xs)
x1 : init (x2 : xs)
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
232
8 · Listenverarbeitung
Programm-Synthese · 8.4
Zusammenfassen der beiden so erhaltenen Gleichungen ergibt
1
2
3
init :: [a] -> [a]
init [x]
= []
init (x1:x2:xs) = x1 : init (x2:xs)
Weitere Verbesserungen
1
2
3
4
�
Das wiederholte Zerlegen und Zusammensetzen der Liste x2 : xs kann
man sich sparen.
�
Für die leere Liste geben wir einen brauchbaren Fehler aus.
init
init
init
init
:: [a] -> [a]
[x]
= []
(x:xs) = x : init xs
[]
= error "init: empty list"
Übung Versuchen Sie Ihren Haskell-Code durch simple
Äquivalenzumformungen zu verbessern. Manchmal gewinnt man dabei
überraschende Einsichten.
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
233
8 · Listenverarbeitung
8.5
List Comprehensions · 8.5
List Comprehensions
List Comprehensions sind vor allem in modernen FPLs als eine alternative
Notation für Operationen auf Listen verbreitet30 .
�
Die Notation mittels Set Comprehension31 ist aus der Mathematik
(Mengenlehre) bekannt. Die Idee dabei:
�
�
�
Term � Prädikat+
• Beschreibt eine Menge, deren Elemente jeweils von Term beschrieben werden,
• unter den durch die Prädikate bestimmten Bedingungen.
�
List Comprehensions erweitern die Ausdruckskraft der Sprache nicht,
erlauben aber oft eine kompakte, leicht lesbare und elegante Notation
von Listenoperationen.
Wir werden eine Abbildung auf den Haskell-Kern besprechen.
30 Miranda™ (Dave Turner, 1976) sah als erste FPL List Comprehensions syntaktisch
31 aka. “set-builder notation”. Einen deutschen Begriff scheint’s nicht zu geben.
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
vor.
234
8 · Listenverarbeitung
List Comprehensions · 8.5
Beispiel Die Menge aller natürlichen geraden Zahlen kann durch eine
set comprehension kompakt notiert werden:
{n | n ∈ N, n mod 2 = 0}
Eine entsprechende List Comprehension (die unendliche Liste aller geraden
Zahlen) wird syntaktisch ganz ähnlich notiert:
[ n | n <- [0 .. ], n ‘mod‘ 2 == 0 ]
Beispiel Die Standardfunktionen map und filter sind mittels List
Comprehensions ohne die sonst notwendige Rekursion formulierbar:
1
2
map :: (α -> β) -> [α] -> [β]
map f xs = [ f x | x <- xs ]
Stefan Klinger · DBIS
1
2
filter :: (α -> Bool) -> [α] -> [α]
filter p xs = [ x | x <- xs, p x ]
Informatik 2 · Sommer 2016
235
8 · Listenverarbeitung
List Comprehensions · 8.5
Syntax der List Comprehension
Die allgemeine Form einer List Comprehension ist
[ e | q1 , q2 , ..., qn ]
wobei
�
der Kopf e ein beliebiger Ausdruck ist, und
�
die Qualifier qi (mit n ≥ 1), eine von drei Formen besitzen:
Generator pi <- ei , wobei ei :: [αi ], und pi ein Pattern für Werte des Typs
αi ist — schreiben salopp pi :: αi .
Prädikat qi :: Bool.
lokale Bindung let { pi1 = ei1 ; pi2 = ei2 ... }. Dabei sind die eij beliebige
Ausdrücke, und die pij entsprechende Patterns.
Beispiel von vorhin: [ n | n <- [0 .. ], n ‘mod‘ 2 == 0 ] .
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
236
8 · Listenverarbeitung
ListComp
Qual
List Comprehensions · 8.5
→
→
|
|
[ Expr | Qual (, Qual)∗ ]
— Zusammenfassung
Pattern <- Expr
— Pattern :: α, Expr :: [α]
Expr
— Expr :: Bool
let { Pattern = Expr (; Pattern = Expr)∗ }
— cf. Seite 167
Semantik der List Comprehension — in Worten
�
Ein Generator qi = pi <- ei versucht das Pattern pi der Reihe nach
gegen die Elemente der Liste ei zu matchen.
• Für jeden erfolgreichen Match werden die nachfolgenden Qualifier
qi+1 , ..., qn ausgewertet.
• Die durch den Match gebundenen Variablen des Patterns pi sind in den
nachfolgenden Qualifiern sichtbar und an entsprechende Werte gebunden.
�
Eine lokale Bindung (let) kann ebenfalls Variablen an Werte binden.
�
Jede Bindung wird solange nach rechts propagiert, bis ein Prädikat
unter ihr zu False evaluiert wird.
�
Der Kopf e wird für alle Bindungen ausgewertet, die alle Prädikate
passieren konnten.
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
237
8 · Listenverarbeitung
List Comprehensions · 8.5
Entsprechend dieser Semantik wird also in [ e | p1 <- e1 , p2 <- e2 ]
�
zuerst über die Domain e1 des Generators p1 <- e1 iteriert, und dann
�
für jeden Match von p1 über die Domain e2 des Generators p2 <- e2 .
Dies trifft die Intuition der aus der Mengenlehre bekannten Set
Comprehension:
�
Stefan Klinger · DBIS
[ (x,y) | x <- [x1 , x2 ], y <- [y1 , y2 ] ]
[(x1 ,y1 ), (x1 ,y2 ), (x2 ,y1 ), (x2 ,y2 )]
Informatik 2 · Sommer 2016
238
8 · Listenverarbeitung
Beispiel
1
2
3
4
5
List Comprehensions · 8.5
Elegante (aber ineffiziente) Variante von Quicksort als 2-Zeiler
qsort :: (α -> α -> Bool) -> [α] -> [α]
qsort _
[]
= []
qsort (<) (x:xs) = qsort (<) [ y | y <- xs, y < x ]
++ [x] ++
qsort (<) [ y | y <- xs, not (y < x) ]
Beachte: In der split-Phase dieser Implementation wird die Liste xs jeweils
(unnötigerweise) zweimal durchlaufen.
Beispiel Matrix über Typ α als Liste von Zeilenvektoren (wiederum
Listen). Bestimme ersten Spaltenvektor:
1
2
firstcol :: [[α]] -> [α]
firstcol m = [ e | (e:_) <- m ]
firstcol nutzt die Möglichkeit, in Generatoren Patterns zu spezifizieren.
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
239
8 · Listenverarbeitung
Beispiel
List Comprehensions · 8.5
Alle Permutationen einer Liste xs
1. Die leere Liste [ ] hat sich selbst als einzige Permutation.
2. Wenn xs nicht leer ist, wähle ein Element a aus xs und stelle a den
Permutationen der Liste xs ohne a voran.
3. Führe 2. für jedes Element der Liste xs aus.
1
2
3
perms :: [Integer] -> [[Integer]]
perms [] = [[]]
perms xs = [ a:p | a <- xs, p <- perms $ xs \\ [a] ]
4
5
6
> perms [2, 3]
[[2, 3], [3, 2]]
�
�
Dabei entfernt die Listendifferenz xs \\ ys alle Elemente von ys aus der
Liste xs, etwa: [1, 2, 1, 2, 3] \\ [2, 5] � [1, 1, 3].
Wie könnte man \\ implementieren?
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
240
8 · Listenverarbeitung
Beispiel
1
List Comprehensions · 8.5
Berechne alle Pythagoräischen Dreiecke mit Seitenlänge ≤ n
pyth n = [ (a,b,c) | c <- [1..n], a <- [1..c], b <- [1..a], a^2 + b^2 == c^2 ]
2
3
4
> pyth 20
[(4,3,5),(8,6,10),(12,5,13),(12,9,15),(15,8,17),(16,12,20)]
Beispiel
1
Was berechnet die folgende Funktion bar? Wie lautet ihr Typ?
bar xs = [ x | [x] <- xs ]
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
241
8 · Listenverarbeitung
Beispiel
1
2
List Comprehensions · 8.5
“Join” zwischen zwei Listen bzgl. eines Prädikates p
join :: (α -> β -> γ) -> (α -> β -> Bool) -> [α] -> [β] -> [γ]
join f p xs ys = [ f x y | x <- xs, y <- ys, p x y ]
Den “klassischen relationalen Join” R1 �fst=fst R2 auf binären Relationen
Ri , erhält man dann durch
1
2
3
4
5
foo = join
(\x y -> (fst x, snd x, snd y))
(\x y -> fst x == fst y)
[(1, "John"), (2, "Jack"), (3, "Bonnie")]
[(2, "Ripper"), (1, "Doe"), (3, "Parker"), (2, "Dalton"), (1, "Cleese")]
6
7
8
9
Prelude> foo
[ (1, "John", "Doe"), (1, "John", "Cleese"), (2, "Jack", "Ripper")
, (2, "Jack", "Dalton"), (3, "Bonnie", "Parker")]
Stefan Klinger · DBIS
Informatik 2 · Sommer 2016
242
© Copyright 2024 ExpyDoc
