9 Daten beliebiger Größe
Die Datentypen, die wir bisher gesehen haben, repräsentieren grundsätzlich Daten, die aus einer festen Anzahl von atomaren Daten bestehen. Dies liegt daran, dass jede Datendefinition nur andere Datendefinitionen verwenden darf, die vorher bereits definiert wurden. Betrachten wir zum Beispiel
(define-struct gcircle (center radius)) ; A GCircle is (make-gcircle Posn Number) ; interp. the geometrical representation of a circle
so wissen wir, dass eine Posn aus zwei und eine Number aus einem atomaren Datum (jeweils Zahlen) besteht und damit ein GCircle aus genau drei atomaren Daten.
In vielen Situationen wissen wir jedoch nicht zum Zeitpunkt des Programmierens, aus wievielen atomaren Daten ein zusammengesetztes Datum besteht. In diesem Kapitel befassen wir uns damit, wie wir Daten beliebiger (und zum Zeitpunkt des Programmierens unbekannter) Größe repräsentieren und Funktionen, die solche Daten verarbeiten, programmieren können.
9.1 Rekursive Datentypen
Betrachten wir als Beispiel ein Programm, mit dem Stammbäume von Personen verwaltet werden können. Jede Person im Stammbaum hat einen Vater und eine Mutter; manchmal sind Vater oder Mutter einer Person auch unbekannt.
Mit den bisherigen Mitteln könnten wir zum Beispiel so vorgehen, um die Vorfahren einer Person zu repräsentieren:
(define-struct parent (name grandfather grandmother)) ; A Parent is: (make-parent String String String) ; interp. the name of a person with the names of his/her grandparents (define-struct person (name father mother)) ; A Person is: (make-person String Parent Parent) ; interp. the name of a person with his/her parents
Allerdings können wir so nur die Vorfahren bis zu genau den Großeltern repräsentieren. Natürlich könnten wir noch weitere Definitionen für die Urgroßeltern usw. hinzufügen, aber stets hätten wir eine beim Programmieren festgelegte Größe. Außerdem verstoßen wir gegen das DRY Prinzip, denn die Datendefinitionen sehen für jede Vorgängergeneration sehr ähnlich aus.
Was können wir machen um mit diesem Problem umzugehen? Betrachten wir etwas genauer, was für Daten wir hier eigentlich modellieren wollen. Die Erkenntnis, die wir hier benötigen, ist, dass ein Stammbaum eine rekursive Struktur hat: Der Stammbaum einer Person besteht aus dem Namen der Person und dem Stammbaum seiner Mutter und dem Stammbaum seiner Eltern. Ein Stammbaum hat also eine Eigenschaft, die man auch Selbstähnlichkeit nennt: Ein Teil eines Ganzen hat die gleiche Struktur wie das Ganze.
Dies bedeutet, dass wir die Restriktion fallen lassen müssen, dass in einer Datendefinition nur die Namen bereits vorher definierter Datentypen auftauchen dürfen. In unserem Beispiel schreiben wir:
(define-struct person (name father mother)) ; A FamilyTree is: (make-person String FamilyTree FamilyTree) ; interp. the name of a person and the tree of his/her parents.
Die Definition von FamilyTree benutzt also selber wieder FamilyTree. Erstmal ist nicht ganz klar, was das bedeuten soll. Vor allen Dingen ist aber auch nicht klar, wie wir einen Stammbaum erzeugen sollen. Wenn wir versuchen, einen zu erzeugen, bekommen wir ein Problem:
(make-person "Bob" (make-person "Horst" (make-person "Joe" ...)))
Wir können überhaupt gar keinen Stammbaum erzeugen, weil wir zur Erzeugung bereits einen Stammbaum haben müssen. Ein Ausdruck, der einen Stammbaum erzeugt, wäre also unendlich groß.
Bei genauer Überlegung sind Stammbäume aber niemals unendlich groß, sondern sie enden bei irgendeiner Generation - zum Beispiel weil die Vorfahren unbekannt oder nicht von Interesse sind.
Diesem Tatbestand können wir dadurch Rechnung tragen, dass wir aus FamilyTree einen Summentyp machen, und zwar wie folgt:
(define-struct person (name father mother)) ; A FamilyTree is either: ; - (make-person String FamilyTree FamilyTree) ; - #false ; interp. either the name of a person and the tree of its parents, ; or #false if the person is not known/relevant.
Dieser neue, nicht-rekursive Basisfall erlaubt es uns nun, Werte dieses Typen zu erzeugen. Hier ist ein Beispiel:
(define Bob (make-person "Bob" (make-person "Alice" #false #false) (make-person "Horst" (make-person "Joe" #false (make-person "Rita" #false #false)) #false)))
Was bedeutet also so eine rekursive Datendefinition? Wir haben bisher Datentypen immer als Mengen von Werten aus dem Datenuniversum interpretiert, und dies ist auch weiterhin möglich, nur die Konstruktion der Menge, die der Typ repräsentiert, ist nun etwas aufwendiger:
Sei ft_0 die leere Menge, ft_1 die Menge \{ \mathtt{\# false} \}, ft_2 die Vereinigung aus \{ \mathtt{\# false} \} und der Menge der (make-person name #false #false) für alle Strings name. Im Allgemeinen sei fti+1 die Vereinigung aus \{ \mathtt{\# false} \} und der Menge der (make-person name p1 p2) für alle Strings name sowie für alle p1 und alle p2 aus fti. Beispielsweise ist Bob ein Element von ft5 (und damit auch ft6, ft7 usw.) aber nicht von ft4.
Dann ist die Bedeutung von FamilyTree, \mathit{ft}, die Vereinigung aller dieser Mengen, also ft0 vereinigt mit ft_1 vereinigt mit ft_2 vereinigt mit ft_3 vereinigt mit ... .
In mathematischer Schreibweise können wir die Konstruktion so zusammenfassen:
\begin{aligned} \mathit{ft}_0 & = \emptyset \\ \mathit{ft}_{i+1} & = \{ \mathtt{\# false} \} \cup \{ \mathtt{(make-person}\ \mathit{n}\ \mathit{p}_1\ \mathit{p}_2 \mathtt{)} \ | \mathit{n} \in \mathit{String}, \mathit{p}_1 \in \mathit{ft}_{i}, \mathit{p}_2 \in \mathit{ft}_{i} \} \\ \mathit{ft} & = \bigcup_{i \in \mathbb{N}}{\mathit{ft}_i} \end{aligned}
Es ist nicht schwer zu sehen, dass stets \mathit{ft}_i \subseteq \mathit{ft}_{i+1}; die nächste Menge umfasst also stets die vorherige.
Aus dieser Mengenkonstruktion wird klar, wieso rekursive Datentypen es ermöglichen, Daten beliebiger Größe zu repräsentieren: Jede Menge fti enthält die Werte, deren maximale Tiefe in Baumdarstellung i ist. Da wir alle fti miteinander vereinigen, ist die Tiefe (und damit auch die Größe) unbegrenzt.
Diese Mengenkonstruktion kann für jeden rekursiven Datentyp definiert werden. Falls es mehrere rekursive Alternativen gibt, so ist die i-te Menge die Vereinigung der i-ten Mengen für jede Alternative. Gäbe es also beispielsweise noch eine zusätzliche FamilyTree Alternative (make-celebrity String Number FamilyTree FamilyTree) bei der neben dem Namen auch noch das Vermögen angegeben wird, so wäre
\begin{aligned} \mathit{ft}_{i+1} & = \{ \mathtt{\# false} \} \cup \{ \mathtt{(make-person}\ \mathit{n}\ \mathit{p}_1\ \mathit{p}_2 \mathtt{)} \ | \mathit{n} \in \mathit{String}, \mathit{p}_1 \in \mathit{ft}_{i}, \mathit{p}_2 \in \mathit{ft}_{i} \} \\ & \cup \{ \mathtt{(make-celebrity}\ \mathit{n}\ \mathit{w}\ \mathit{p}_1\ \mathit{p}_2 \mathtt{)} \ | \mathit{n} \in \mathit{String}, \mathit{w} \in \mathit{Number}, \mathit{p}_1 \in \mathit{ft}_{i}, \mathit{p}_2 \in \mathit{ft}_{i} \} \end{aligned}
9.2 Programmieren mit rekursiven Datentypen
Im letzten Abschnitt haben wir gesehen, wie man rekursive Datentypen definiert, was sie bedeuten, und wie man Instanzen dieser Datentypen erzeugt. Nun wollen wir überlegen, wie man Funktionen programmieren kann, die Instanzen solcher Typen als Argumente haben oder als Resultat produzieren.
Betrachten Sie dazu folgende Aufgabe: Programmieren sie eine Funktion, die herausfindet, ob es im Stammbaum einer Person einen Vorfahren mit einem bestimmten Namen gibt.
Eine Signatur, Aufgabenbeschreibung und Tests sind dazu schnell definiert:
; FamilyTree String -> Boolean ; determines whether person p has an ancestor a (check-expect (person-has-ancestor Bob "Joe") #true) (check-expect (person-has-ancestor Bob "Emil") #false) (define (person-has-ancestor p a) ...)
Da FamilyTree ein Summentyp ist, sagt unser Entwurfsrezept, dass wir eine Fallunterscheidung machen. In jedem Zweig der Fallunterscheidung können wir die Selektoren für die Felder eintragen. In unserem Beispiel ergibt sich:
(define (person-has-ancestor p a) (cond [(person? p) ...(person-name p) ... ...(person-father p)... ...(person-mother p) ...] [else ...]))
Wir interpretieren das Wort "Vorfahr" so, dass eine Person ihr eigener Vorfahr ist. Wie müsste das Programm aussehen, um die nicht-reflexive Interpretation des Worts "Vorfahr" zu realisieren?
Unser Entwurfsrezept schlägt für Fälle, in denen Felder einer Strukur selber einen komplexen Summen-/Produkttyp haben, vor, eigene Hilfsfunktionen zu definieren. Dies können wir wie folgt andeuten:
(define (person-has-ancestor p a) (cond [(person? p) ... (person-name p) ... ... (father-has-ancestor (person-father p) ...)... ... (mother-has-ancestor (person-mother p) ...)...] [else ...]))
Wenn wir uns jedoch etwas genauer überlegen, was father-has-ancestor und mother-has-ancestor tun sollen, stellen wir fest, dass sie die gleiche Signatur und Aufgabenbeschreibung haben wie person-has-ancestor! Das bedeutet, dass die Templates für diese Funktionen wiederum jeweils zwei neue Hilfsfunktionen erfordern. Da wir nicht wissen, wie tief der Stammbaum ist, können wir auf diese Weise das Programm also gar nicht realisieren.
Zum Glück haben wir aber bereits eine Funktion, deren Aufgabe identisch mit der von father-has-ancestor und mother-has-ancestor ist, nämlich person-has-ancestor selbst. Dies motiviert das folgende Template:
(define (person-has-ancestor p a) (cond [(person? p) ... (person-name p) ... ... (person-has-ancestor (person-father p) ...)... ... (person-has-ancestor (person-mother p) ...)...] [else ...]))
Die Struktur der Daten diktiert also die Struktur der Funktionen. Dort wo die Daten rekursiv sind, sind auch die Funktionen, die solche Daten verarbeiten, rekursiv.
Die Vervollständigung des Templates ist nun eifach:
(define (person-has-ancestor p a) (cond [(person? p) (or (string=? (person-name p) a) (person-has-ancestor (person-father p) a) (person-has-ancestor (person-mother p) a))] [else #false]))
Die erfolgreich ablaufenden Tests illustrieren, dass diese Funktion anscheinend das tut, was sie soll, aber wieso?
Vergleichen wir die Funktion mit einem anderen Ansatz, der nicht so erfolgreich ist. Betrachten wir nochmal den Anfang der Programmierung der Funktion, diesmal mit anderem Namen:
; FamilyTree String -> Boolean ; determines whether person p has an ancestor a (check-expect (person-has-ancestor-stupid Bob "Joe") #true) (check-expect (person-has-ancestor-stupid Bob "Emil") #false) (define (person-has-ancestor-stupid p a) ...)
Wenn wir schon eine Funktion hätten, die bestimmen kann, ob eine Person einen bestimmten Vorfahren hat, könnten wir einfach diese Funktion aufrufen. Aber zum Glück sind wir ja schon gerade dabei, diese Funktion zu programmieren. Also rufen wir doch einfach diese Funktion auf:
; FamilyTree -> Boolean ; determines whether person p has an ancestor a (check-expect (person-has-ancestor-stupid Bob "Joe") #true) (check-expect (person-has-ancestor-stupid Bob "Emil") #false) (define (person-has-ancestor-stupid p a) (person-has-ancestor-stupid p a))
Irgendwie scheint diese Lösung zu einfach zu sein. Ein Ausführen der Tests bestätigt den Verdacht. Allerdings schlagen die Tests nicht fehl, sondern die Ausführung der Tests terminiert nicht und wir müssen sie durch Drücken auf die "Stop" Taste abbrechen.
Wieso funktioniert person-has-ancestor aber nicht person-has-ancestor-stupid?
Zunächst einmal können wir die Programme operationell miteinander vergleichen. Wenn wir den Ausdruck (person-has-ancestor-stupid Bob "Joe") betrachten, so sagt unsere Reduktionssemantik:
(person-has-ancestor-stupid Bob "Joe") → (person-has-ancestor-stupid Bob "Joe")
Es gibt also keinerlei Fortschritt bei der Auswertung. Dies erklärt, wieso die Ausführung nicht stoppt.
Dies ist anders bei (person-has-ancestor Bob "Joe"). Die rekursiven Aufrufe rufen person-has-ancestor stets auf Vorfahren der Person auf. Da der Stammbaum nur eine endliche Tiefe hat, muss irgendwann (person-has-ancestor #false "Joe") aufgerufen werden, und wir landen im zweiten Fall des konditionalen Ausdrucks, der keine rekursiven Ausdrücke mehr enthält.
Wir können das Programm auch aus Sicht der Bedeutung der rekursiven Datentypdefinition betrachten.
Für jede Eingabe p gibt es ein minimales i so dass p in fti ist.
Für Bob ist dieses i=5. Da die Werte der mother und father Felder von p damit
in ft_{i-1} sind, ist klar, dass der p Parameter bei allen rekursiven Aufrufe in ft_{i-1} ist.
Da das Programm offensichtlich für Werte aus ft_0 (im Beispiel die Menge {#false}) terminiert, ist
klar, dass dann auch alle Aufrufe mit Werten aus ft_1 terminieren müssen, damit dann aber auch
die Aufrufe mit Werten aus ft_2 und so weiter. Damit haben wir gezeigt, dass die Funktion
für alle Werte aus ft_i für ein beliebiges i wohldefiniert ist —
Dieses informell vorgetragene Argument aus dem vorherigen Absatz ist mathematisch gesehen ein Induktionsbeweis.
Bei person-has-ancestor-stupid ist die Lage anders, da im rekursiven Aufruf das Argument eben nicht aus ft_{i-1} ist.
Die Schlussfolgerung aus diesen Überlegungen ist, dass Rekursion in Funktionen unproblematisch und wohldefiniert ist, solange sie der Struktur der Daten folgt. Da Werte rekursiver Datentypen eine unbestimmte aber endliche Größe haben, ist diese sogenannte strukturelle Rekursion stets wohldefiniert. Unser Entwurfsrezept schlägt vor, dass immer dort wo Datentypen rekursiv sind, auch die Funktionen, die darauf operieren, (strukturell) rekursiv sein sollen.
Bevor wir uns das angepasste Entwurfsrezept im Detail anschauen, wollen wir erst noch überlegen, wie Funktionen aussehen, die Exemplare rekursiver Datentypen produzieren.
Als Beispiel betrachten wir eine Funktion, die sehr nützlich ist, um den eigenen Stammbaum etwas eindrucksvoller aussehen zu lassen, nämlich eine, mit der der Name aller Vorfahren um einen Titel ergänzt werden kann.
Hier ist die Signatur, Aufgabenbeschreibung und ein Test für diese Funktion:
; FamilyTree -> FamilyTree ; prefixes all members of a family tree p with title t (check-expect (promote Bob "Dr. ") (make-person "Dr. Bob" (make-person "Dr. Alice" #false #false) (make-person "Dr. Horst" (make-person "Dr. Joe" #false (make-person "Dr. Rita" #false #false)) #false))) (define (promote p t) ...)
Die Funktion konsumiert und produziert also gleichzeitig einen Wert vom Typ FamilyTree. Das Template für solche Funktionen unterscheidet sich nicht von dem für person-has-ancestor. Auch hier wenden wir wieder dort Rekursion an, wo auch der Datentyp rekursiv ist:
(define (promote p t) (cond [(person? p) ...(person-name p)... ...(promote (person-father p) ...)... ...(promote (person-mother p) ...)...] [else ...]))
Nun ist es recht einfach, die Funktion zu vervollständigen. Um Werte vom Typ FamilyTree zu produzieren, bauen wir die Resultate der rekursiven Aufrufe in einen Aufruf des make-person Konstruktors ein:
(define (promote p t) (cond [(person? p) (make-person (string-append t (person-name p)) (promote (person-father p) t) (promote (person-mother p) t))] [else p]))
9.3 Formale Signaturen für rekursive Datentypen
Wir können formale Signaturen auch für rekursive Datentypen verwenden. Den äußeren Summentyp können wir über den Signaturkonstruktur mixed abbilden. Wichtig an der formalen Signatur FamilyTree ist, dass die Definition selber rekursiv ist.
(define-struct person (name father mother)) (define FamilyTree (signature (mixed False (PersonOf String FamilyTree FamilyTree))))
Dieser Datentyp kann nun wie gewohnt in Signaturen verwendet werden, beispielsweise:
(: Bob FamilyTree) (: person-has-ancestor (FamilyTree String -> Boolean)) (define (person-has-ancestor p a) ...)
9.4 Listen
Die FamilyTree Datendefinition von oben steht für eine Menge von Bäumen, in denen
jeder Knoten genau zwei ausgehende Kanten hat. Selbstverständlich können wir auch auf die
gleiche Weise Bäume repräsentieren, die drei oder fünf ausgehende Kanten haben —
Ein besonders wichtiger Spezialfall ist der, wo jeder Knoten genau eine ausgehende Kante hat. Diese degenerierten Bäume nennt man auch Listen.
9.4.1 Listen, hausgemacht
Hier ist eine mögliche Definition für Listen von Zahlen:
(define-struct lst (first rest)) ; A List-of-Numbers is either: ; - (make-lst Number List-Of-Numbers) ; - #false ; interp. the head and rest of a list, or the empty list
Hier ist ein Beispiel, wie wir eine Liste mit den Zahlen 1 bis 3 erzeugen können:
(make-lst 1 (make-lst 2 (make-lst 3 #false)))
Der Entwurf von Funktionen auf Listen funktioniert genau wie der Entwurf von Funktionen auf allen anderen Bäumen. Betrachten wir als Beispiel eine Funktion, die alle Zahlen in einer Liste aufaddiert.
Hier ist die Spezifikation dieser Funktion:
; List-Of-Numbers -> Number ; adds up all numbers in a list (check-expect (sum (make-lst 1 (make-lst 2 (make-lst 3 #false)))) 6) (define (sum l) ...)
Für das Template schlägt das Entwurfsrezept vor, die verschiedenen Alternativen zu unterscheiden und in den rekursiven Alternativen rekursive Funktionsaufrufe einzubauen:
(define (sum l) (cond [(lst? l) ... (lst-first l) ... (sum (lst-rest l)) ...] [else ...]))
Auf Basis dieses Templates ist die Vervollständigung nun einfach:
(define (sum l) (cond [(lst? l) (+ (lst-first l) (sum (lst-rest l)))] [else 0]))
9.4.2 Listen aus der Konserve
Weil Listen so ein häufig vorkommender Datentyp sind, gibt es in BSL vordefinierte Funktionen für Listen. Wie List-of-Numbers zeigt, benötigen wir diese vordefinierten Funktionen eigentlich nicht, weil wir Listen einfach als degenerierte Bäume repräsentieren können. Dennoch machen die eingebauten Listenfunktionen das Programmieren mit Listen etwas komfortabler und sicherer.
Die eingebaute Konstruktorfunktion für Listen in BSL heißt cons; die leere Liste wird nicht durch #false sondern durch die spezielle Konstante empty repräsentiert.
Es ist sinnvoll, die leere Liste durch einen neuen Wert zu repräsentieren, der für nichts anderes steht, denn dann kann es niemals zu Verwechslungen kommen. Wenn wir etwas analoges in unserer selbstgebauten Datenstruktur für Listen machen wollten, könnten wir dies so erreichen, indem wir eine neue Struktur ohne Felder definieren und ihren einzigen Wert als Variable definieren:
(define-struct empty-lst ()) (define EMPTYLIST (make-empty-lst))
Dementsprechend würde die Beispielliste von oben nun so konstruiert:
(make-lst 1 (make-lst 2 (make-lst 3 EMPTYLIST)))
Die cons Operation entspricht unserem make-lst von oben, allerdings mit einem wichtigen Unterschied: Sie überprüft zusätzlich, dass das zweite Argument auch eine Liste ist:
> (cons 1 2) cons: second argument must be a list, but received 1 and 2
Man kann sich cons also so vorstellen wie diese selbstgebaute Variante von cons auf Basis von List-Of-Numbers:
(define (our-cons x l) (if (or (empty-lst? l) (lst? l)) (make-lst x l) (error "second argument of our-cons must be a list")))
Die wichtigsten eingebauten Listenfunktionen sind:
empty, empty?, cons, first, rest und cons?.
Sie entsprechen in unserem selbstgebauten Listentyp:
EMPTYLIST, empty-lst?, our-cons, lst-first, lst-rest und lst?.
Die Funktion, die make-lst entspricht, wird von BSL versteckt, um sicherzustellen, dass alle Listen stets mit cons konstruiert werden und dementsprechend die Invariante forciert wird, dass das zweite Feld der Struktur auch wirklich eine Liste ist. Mit unseren bisherigen Mitteln können wir dieses "Verstecken" von Funktionen nicht nachbauen; dazu kommen wir später, wenn wir über Module reden.
Unser Beispiel von oben sieht bei Nutzung der eingebauten Listenfunktionen also so aus:
; A List-of-Numbers is one of: ; - (cons Number List-Of-Numbers) ; - empty ; List-Of-Numbers -> Number ; adds up all numbers in a list (check-expect (sum (cons 1 (cons 2 (cons 3 empty)))) 6) (define (sum l) (cond [(cons? l) (+ (first l) (sum (rest l)))] [else 0]))
9.4.3 Die list Funktion
Es stellt sich schnell als etwas mühselig heraus, Listen mit Hilfe von cons und empty zu konstruieren. Aus diesem Grund gibt es etwas syntaktischen Zucker, um Listen komfortabler zu erzeugen: Die list Funktion.
Mit der list Funktion können wir die Liste (cons 1 (cons 2 (cons 3 empty))) so erzeugen:
(list 1 2 3)
Die list Funktion ist jedoch nur etwas syntaktischer Zucker, der wie folgt definiert ist:
steht für n verschachtelte cons Ausdrücke:
Es ist wichtig, zu verstehen, dass dies wirklich nur eine abkürzende Schreibweise ist. Auch wenn Sie mittels list leichter Listen definieren können, ist es wichtig, stets im Kopf zu behalten, dass dies nur eine Kurzschreibweise für die Benutzung von cons und empty ist, denn nur so ist das Entwurfsrezept für rekursive Datentypen auch auf Listen anwendbar.
9.4.4 Datentypdefinitionen für Listen
Wir haben oben eine Datendefinition List-of-Numbers gesehen. Sollen wir auch für List-of-Strings oder List-of-Booleans eigene Datendefinitionen schreiben? Sollen diese die gleiche Struktur benutzen, oder sollen wir separate Strukturen für jeden dieser Datentypen haben?
Es ist sinnvoll, dass alle diese Datentypen die gleiche Struktur benutzen, nämlich in Form der eingebauten Listenfunktionen. Hierfür gibt es zwei Gründe: Erstens wären all diese Strukturen sehr ähnlich und wir würden damit gegen das DRY Prinzip verstoßen. Zweitens gibt es eine ganze Reihe von Funktionen, die auf beliebigen Listen arbeiten, zum Beispiel eine Funktion second, die das zweite Listenelement einer Liste zurückgibt:
(define (second l) (if (or (empty? l) (empty? (rest l))) (error "need at least two list elements") (first (rest l))))
Diese Funktion (die übrigens schon vordefiniert ist, genau wie third, fourth und so weiter) funktioniert für beliebige Listen, unabhängig von der Art der gespeicherten Daten. Solche Funktionen könnten wir nicht schreiben, wenn wir je nach Typ der Listenelemente andere Strukturen verwenden würden.
Der häufigste Anwendungsfall von Listen ist der, dass die Listen homogen sind. Das bedeutet, dass alle Listenelemente einen gemeinsamen Typ haben. Dies ist keine sehr große Einschränkung, denn dieser gemeinsame Typ kann beispielsweise auch ein Summentyp mit vielen Alternativen sein. Für diesen Fall verwenden wir Datendefinitionen mit Typparametern, und zwar so:
; A (List-of X) is one of: ; - (cons X (List-of X) ; - empty
Diese Datendefinitionen benutzen wir, indem wir einen Typ für den Typparameter angeben. Hierzu verwenden wir die Syntax für Funktionsanwendung; wir schreiben also (List-of String), (List-of Boolean), (List-of (List-of String)) oder (List-of FamilyTree) und meinen damit implizit die oben angeführte Datendefinition.
Was aber ist ein geeigneter Datentyp für die Signatur von second oben, also im Allgemeinen für Funktionen, die auf beliebigen Listen funktionieren?
Um deutlich zu machen, dass die Funktionen für Listen mit beliebigem Elementtyp funktionieren, sagen wir dies in der Signatur explizit. Im Beispiel der Funktion second sieht das so aus:
Allerdings werden wir im Moment nur im Ausnahmefall Funktionen wie second selber programmieren. Die meisten Funktionen, die wir im Moment programmieren wollen, verarbeiten Listen mit einem konkreten Elementtyp. Auf sogenannte polymorphe Funktionen wie second werden wir später noch zurückkommen.
9.4.5 Aber sind Listen wirklich rekursive Datenstrukturen?
Wenn man sich Listen aus der realen Welt anschaut (auf einem Blatt Papier, in einer Tabellenkalkulation etc.), so suggerieren diese häufig keine rekursive, verschachtelte Struktur sondern sehen "flach" aus. Ist es also "natürlich", Listen so wie wir es getan haben, über einen rekursiven Datentyp - als degenerierten Baum - zu definieren?
In vielen (vor allem älteren) Programmiersprachen gibt es eine direktere Unterstützung für Listen. Listen sind in diesen Programmiersprachen fest eingebaut. Listen sind in diesen Sprachen nicht rekursiv; stattdessen wird häufig über einen Index auf die Elemente der Liste zugegriffen. Um die Programmierung mit Listen zu unterstützen, gibt es einen ganzen Satz von Programmiersprachenkonstrukten (wie z.B. verschiedenen Schleifen- und Iterationskonstrukten), die der Unterstützung dieser fest eingebauten Listen dienen.
Es gibt allerdings auch durchaus Situationen, in denen rekursiv aufgebaute Listen effizienter sind. Mehr dazu später.
Der Reiz der rekursiven Formulierung liegt darin, dass man keinerlei zusätzliche Unterstützung für Listen in der Programmiersprache benötigt. Wir haben ja oben gesehen, dass wir uns die Art von Listen, die von BSL direkt unterstützt werden, auch selber programmieren können. Es ist einfach "yet another recursive datatype", und alle Konstrukte, Entwurfsrezepte und so weiter funktionieren nahtlos auch für Listen. Wir brauchen keine speziellen Schleifen oder andere Spezialkonstrukte um Listen zu verarbeiten, sondern machen einfach das, was wir auch bei jedem anderen rekursiven Datentyp machen. Das ist bei fest eingebauten Index-basierten Listen anders; es gibt viele Beispiele für Sprachkonstrukte, die für "normale Werte" funktionieren, aber nicht für Listen, und umgekehrt.
BSL und Racket stehen in der Tradition der Programmiersprache Scheme. Die Philosophie, die im ersten Satz der Sprachspezifikation von Scheme (http://www.r6rs.org) zu finden ist, ist damit auch für BSL und Racket gültig:
Programming languages should be designed not by piling feature on top of feature, but by removing the weaknesses and restrictions that make additional features appear necessary. Scheme demonstrates that a very small number of rules for forming expressions, with no restrictions on how they are composed, suffice to form a practical and efficient programming language that is flexible enough to support most of the major programming paradigms in use today.
Die Behandlung von Listen als rekursive Datentypen ist ein Beispiel für diese Philosophie.
Manche Programmieranfänger finden es nicht intuitiv, Listen und Funktionen darauf rekursiv zu formulieren. Aber ist es nicht besser, ein Universalwerkzeug zu verwenden, welches in sehr vielen Situationen verwendbar ist, als ein Spezialwerkzeug, das in nichts besser ist als das Universalwerkzeug und nur in einer Situation anwendbar ist?
9.4.6 Natürliche Zahlen als rekursive Datenstruktur
Es gibt in BSL nicht nur Funktionen, die Listen konsumieren, sondern auch solche, die Listen produzieren. Eine davon ist make-list. Hier ein Beispiel:
> (make-list 4 "abc") ("abc" "abc" "abc" "abc")
Die make-list Funktion konsumiert also eine natürliche Zahl n und einen Wert und produziert eine Liste mit n Wiederholungen des Werts. Obwohl diese Funktion also nur atomare Daten konsumiert, produziert sie ein beliebig großes Resultat. Wie ist das möglich?
Auch in der Mathematik werden natürliche Zahlen ähnlich rekursiv definiert. Recherchieren sie, was die Peano-Axiome sind.
; A Nat (Natural Number) is one of: ; – 0 ; – (add1 Nat)
Beispielsweise können wir die Zahl 3 repräsentieren als (add1 (add1 (add1 0))). Die add1 Funktion hat also eine Rolle ähnlich zu den Konstruktorfunktionen bei Strukturen. Die Rolle der Selektorfunktion wird durch die Funktion sub1 übernommen. Das Prädikat für die erste Alternative von Nat ist zero?; das Prädikat für die zweite Alternative heißt positive?.
Mit dieser Sichtweise sind wir nun in der Lage, mit unserem Standard-Entwurfsrezept Funktionen wie make-list selber zu definieren. Nennen wir unsere Variante von make-list iterate-value. Hier ist die Spezifikation:
; [X] Nat X -> (List-of X) ; creates a list with n occurences of x (check-expect (iterate-value 3 "abc") (list "abc" "abc" "abc")) (define (iterate-value n x) ...)
Gemäß unseres Entwurfsrezepts für rekursive Datentypen erhalten wir folgendes Template:
(define (iterate-value n x) (cond [(zero? n) ...] [(positive? n) ... (iterate-value (sub1 n) ...)...]))
Dieses Template zu vervollständigen ist nun nur noch ein kleiner Schritt:
(define (iterate-value n x) (cond [(zero? n) empty] [(positive? n) (cons x (iterate-value (sub1 n) x))]))
9.5 Mehrere rekursive Datentypen gleichzeitig
Ein schwierigerer Fall ist es, wenn mehrere Parameter einer Funktion einen rekursiven Datentyp haben. In diesem Fall ist es meist sinnvoll, einen dieser Parameter zu bevorzugen und zu ignorieren, dass andere Parameter ebenfalls rekursiv sind. Welcher Parameter bevorzugt werden sollte, ergibt sich aus der Fragestellung, wie Sie die Eingabe der Funktion am sinnvollsten zerlegen können, so dass Sie aus dem Ergebnis des rekursiven Aufrufs und den anderen Parametern am einfachsten das Gesamtergebnis berechnen können.
; [X] (list-of X) (list-of X) -> (list-of X) ; concatenates l1 and l2 (check-expect (lst-append (list 1 2) (list 3 4)) (list 1 2 3 4)) (define (lst-append l1 l2) (cond [(empty? l1) ...l2...] [(cons? l1) ... (first l1) ... (lst-append (rest l1) ...)]))
Tatsächlich ist es in diesem Fall leicht, das Template zu vervollständigen. Wenn wir das Ergebnis von (lst-append (rest l1) l2) haben, so müssen wir nur noch (first l1) vorne anhängen:
(define (lst-append l1 l2) (cond [(empty? l1) l2] [(cons? l1) (cons (first l1) (lst-append (rest l1) l2))]))
(define (lst-append l1 l2) (cond [(empty? l2) ...l1...] [(cons? l2) ... (first l2) ... (lst-append .. (rest l2))]))
9.6 Entwurfsrezept für Funktionen mit rekursiven Datentypen
Wir haben gesehen, wie wir mit Hilfe eines Entwurfsrezepts einfache Funktionen (Entwurfsrezept zur Funktionsdefinition), Funktionen mit Summentypen (Entwurf mit Summentypen), Funktionen mit Produkttypen (Erweiterung des Entwurfsrezepts) und Funktionen mit algebraischen Datentypen (Programmentwurf mit ADTs) entwerfen.
An dieser Stelle fassen wir zusammen, wie wir das Entwurfsrezept erweitern, um mit Daten beliebiger Größe umzugehen.
Wenn es in der Problemdomäne Informationen unbegrenzter Größe gibt, benötigen Sie eine selbstreferenzierende Datendefinition. Damit eine selbstreferenzierende Datendefinition gültig ist, muss sie drei Bedingungen erfüllen: 1) Der Datentyp ist ein Summentyp. 2) Es muss mindestens zwei Alternativen geben. 3) Mindestens eine der Alternativen referenziert nicht den gerade definierten Datentyp, ist also nicht rekursiv.
Sie sollten für rekursive Datentypen Datenbeispiele angeben, um zu validieren, dass Ihre Definition sinnvoll ist. Wenn es nicht offensichtlich ist, wie Sie ihre Datenbeispiele beliebig groß machen, stimmt vermutlich etwas nicht.
Beim zweiten Schritt ändert sich nichts: Sie benötigen wie immer eine Signatur, eine Aufgabenbeschreibung und eine Dummy-Implementierung.
Bei selbstreferenzierenden Datentypen ist es nicht mehr möglich, für jede Alternative einen Testfall anzugeben (weil es, wenn man in die Tiefe geht, unendlich viele Alternativen gibt). Die Testfälle sollten auf jeden Fall alle Teile der Funktion abdecken. Versuchen Sie weiterhin, kritische Grenzfälle zu identifizieren und zu testen.
Rekursive Datentypen sind algebraische Datentypen, daher kann für den Entwurf des Templates die Methodik aus Programmentwurf mit ADTs angewendet werden. Die wichtigste Ergänzung zu dem Entwurfsrezept betrifft den Fall, dass eine Alternative implementiert werden muss, die selbstreferenzierend ist. Statt wie sonst eine neue Hilfsfunktion im Template zu verwenden, wird in diesem Fall ein rekursiver Aufruf der Funktion, die Sie gerade implementieren, ins Template aufgenommen. Als Argument des rekursiven Aufrufs wird der Aufruf des Selektors, der den zur Datenrekursion gehörigen Wert extrahiert, ins Template mit aufgenommen. Wenn Sie beispielsweise eine Funktion (define (f a-list-of-strings ...) ...) auf Listen definieren, so sollte im cons? Fall der Funktion der Aufruf (f (rest a-list-of-strings) ...) stehen.
Beim Entwurf des Funktionsbodies starten wir mit den Fällen der Funktion, die nicht rekursiv sind. Diese Fälle nennt man auch die Basisfälle, in Analogie zu Basisfällen bei Beweisen per Induktion. Die nicht-rekursiven Fälle sind typischerweise einfach und sollten sich direkt aus den Testfällen ergeben.
In den rekursiven Fällen müssen wir uns überlegen, was der rekursive Aufruf bedeutet. Hierzu nehmen wir an, dass der rekursive Aufruf die Funktion korrekt berechnet, so wie wir es in der Aufgabenbeschreibung in Schritt 2 festgelegt haben. Mit diesem Wissen müssen wir nun nur noch die zur Verfügung stehenden Werte zur Lösung zusammenbauen.
Testen Sie wie üblich, ob ihre Funktion wie gewünscht funktioniert und prüfen Sie, ob die Tests alle interessanten Fälle abdecken.
Für Programme mit rekursiven Datentypen gibt es einige neue Refactorings, die möglicherweise sinnvoll sind. Überprüfen Sie, ob ihr Programm Datentypen enthält, die nicht rekursiv sind, aber die durch einen rekursiven Datentyp vereinfacht werden könnten. Enthält ihr Programm beispielsweise separate Datentypen für Angestellter, Gruppenleiter, Abteilungsleiter, Bereichsleiter und so weiter, so könnte dies durch einen rekursiven Datentyp, mit dem beliebig tiefe Managementhierarchien modelliert werden können, vereinfacht werden.
9.7 Refactoring von rekursiven Datentypen
Bezüglich der Datentyp-Refactorings aus Refactoring von algebraischen Datentypen ergeben sich neue Typisomorphien durch "inlining" bzw. Expansion von rekursiven Datendefinitionen. Beispielsweise ist in folgendem Beispiel list-of-number isomorph zu list-of-number2, denn letztere Definition ergibt sich aus der ersten indem man die Rekursion einmal expandiert.
; A list-of-number is either: ; - empty ; - (cons Number list-of-number) (define-struct Number-and-Number-List (num numlist)) ; A list-of-number2 is either: ; - empty ; - (make-Number-and-Number-List Number list-of-number)
Wenn wir die Notation aus Refactoring von algebraischen Datentypen verwenden, so können wir rekursive Datentypen als Funktionen modellieren, wobei der Funktionsparameter das rekursive Vorkommen des Datentyps modelliert. Beispielsweise kann der Datentyp der Listen von Zahlen durch die Funktion F (X) = (+ Empty (* Number X)) modelliert werdenSolche Funktionen nennt man auch Funktoren und sie sind in der universellen Algebra als F-Algebras von wichtiger Bedeutung.. Das schöne an dieser Notation ist, dass man sehr leicht definieren kann, wann rekursive Datentypen isormoph sind. Die Expansion eines rekursiven Datentyps ergibt sich daraus, den Funktionsparameter X durch die rechte Seite der Definition zu ersetzen, also in dem Beispiel F (X) = (+ Empty (* Number (+ Empty (* Number X)))). Inlining ist die umgekehrte Operation. Die Rechtfertigung für diese Operationen ergibt sich daraus, dass man rekursive Datentypen als kleinsten Fixpunkt solcher Funktoren verstehen kann. Beispielsweise ist der kleinste Fixpunkt von F (X) = (+ Empty (* Number X)) die unendliche Summe (+ Empty (* Number Empty) (* Number Number Empty) (* Number Number Number Empty) ...). Der kleinste Fixpunkt ändert sich durch Expansion oder Inlining nicht, daher sind solche Datentypen isomorph.
9.8 Programmäquivalenz und Induktionsbeweise
Betrachten Sie die folgenden beiden Funktionen:
; FamilyTree -> Number ; computes the number of known ancestors of p (check-expect (numKnownAncestors Bob) 5) (define (numKnownAncestors p) (cond [(person? p) (+ 1 (numKnownAncestors (person-father p)) (numKnownAncestors (person-mother p)))] [else 0])) ; FamilyTree -> Number ; computes the number of unknown ancestors of p (check-expect (numUnknownAncestors Bob) 6) (define (numUnknownAncestors p) (cond [(person? p) (+ (numUnknownAncestors (person-father p)) (numUnknownAncestors (person-mother p)))] [else 1]))
Die Tests suggerieren, dass für alle Personen p folgende Äquivalenz gilt: (+ (numKnownAncestors p) 1) ≡ (numUnknownAncestors p). Aber wie können wir zeigen, dass diese Eigenschaft tatsächlich stimmt?
Das Schliessen durch Gleichungen, wie wir es in Refactoring von Ausdrücken und Schliessen durch Gleichungen kennengelernt haben, reicht hierzu alleine nicht aus. Dadurch, dass die Funktionen rekursiv sind, können wir durch EFUN immer größere Terme erzeugen, aber wir kommen niemals von numKnownAncestors zu numUnknownAncestors.
Bei strukturell rekursiven Funktionen auf rekursiven Datentypen können wir jedoch ein weiteres, sehr mächtiges Beweisprinzip verwenden, nämlich das Prinzip der Induktion. Betrachten Sie nochmal die Mengenkonstruktion der fti aus Rekursive Datentypen. Wir wissen, dass der Typ FamilyTree die Vereinigung aller fti ist. Desweiteren wissen wir, dass, wenn p in fti+1 ist, dann ist (person-father p) und (person-mother p) in fti. Dies rechtfertigt die Verwendung des Beweisprinzips der Induktion: Wir zeigen die gewünschte Äquivalenz für den Basisfall i = 1, also p = #false. Dann zeigen wir die Äquivalenz für den Fall i = n+1, unter der Annahme, dass die Äquivalenz bereits für i = n gilt. Anders ausgedrückt zeigen wir für die Äquivalenz für den Fall p = (make-person n p1 p2) unter der Annahme, dass die Äquivalenz für p1 und p2 gilt.
Typischerweise läßt man bei dieser Art von Induktionsbeweisen die Mengenkonstruktion mit ihren Indizes weg und "übersetzt" die Indizes direkt in die Datentyp-Notation. Dies bedeutet, dass man die gewünschte Aussage zunächst für die nicht-rekursiven Fälle des Datentyps zeigt, und dann im Induktionsschritt die Aussage für die rekursiven Fälle zeigt unter der Annahme, dass die Aussage für die Unterkomponenten des Datentyps bereits gilt. Diese Art des Induktionsbeweises nennt man auch strukturelle Induktion.
Wir wollen beweisen: (+ (numKnownAncestors p) 1) ≡ (numUnknownAncestors p) für alle Personen p. Betrachten wir zunächst den Basisfall p = #false.
Dann können wir schliessen:
(+ (numKnownAncestors #false) 1)
≡ (gemäß EFUN und EKONG)
(+ (cond [(person? #false) ...] [else 0]) 1)
≡ (gemäß STRUCT-predfalse und EKONG)
(+ (cond [#false ...] [else 0]) 1)
≡ (gemäß COND-False und EKONG)
≡ (gemäß COND-True und EKONG)
(+ 0 1)
≡ (gemäß PRIM)
1
Unter Nutzung von ETRANS können wir damit (+ (numKnownAncestors #false) 1) ≡ 1 schliessen. Auf die gleiche Weise können wir schliessen: (numUnknownAncestors #false) ≡ 1. Damit haben wir den Basisfall gezeigt.
Für den Induktionsschritt müssen wir die Äquivalenz für p = (make-person n p1 p2) zeigen und dürfen hierbei verwenden, dass die Aussage für p1 und p2 gilt, also (+ (numKnownAncestors p1) 1) ≡ (numUnknownAncestors p1) und (+ (numKnownAncestors p2) 1) ≡ (numUnknownAncestors p2).
Wir können nun wie folgt schliessen:
(+ (numKnownAncestors (make-person n p1 p2)) 1)
≡ (gemäß EFUN und EKONG)
(+ (cond [(person? (make-person n p1 p2)) (+ 1 (numKnownAncestors (person-father (make-person n p1 p2))) (numKnownAncestors (person-mother (make-person n p1 p2))))] [else 0]) 1)
≡ (gemäß STRUCT-predtrue und EKONG)
(+ (cond [#true (+ 1 (numKnownAncestors (person-father (make-person n p1 p2))) (numKnownAncestors (person-mother (make-person n p1 p2))))] [else 0]) 1)
≡ (gemäß COND-True und EKONG)
(+ (+ 1 (numKnownAncestors (person-father (make-person n p1 p2))) (numKnownAncestors (person-mother (make-person n p1 p2)))) 1)
≡ (gemäß STRUCT-select und EKONG)
(+ (+ 1 (numKnownAncestors p1) (numKnownAncestors p2)) 1)
≡ (gemäß EPRIM)
(+ (+ (numKnownAncestors p1) 1) (+ (numKnownAncestors p2) 1))
≡ (gemäß Induktionsannahme und EKONG)
(+ (numUnknownAncestors p1) (numUnknownAncestors p2))
≡ (gemäß STRUCT-select und EKOMM und EKONG)
(+ (numUnknownAncestors (person-father (make-person n p1 p2))) (numUnknownAncestors (person-mother (make-person n p1 p2))))
≡ (gemäß EFUN und EKOMM)
(numUnknownAncestors (make-person n p1 p2))
Damit haben wir (unter Nutzung von ETRANS) die Äquivalenz bewiesen. Dieser Beweis ist sehr ausführlich und kleinschrittig. Wenn Sie geübter im Nutzen von Programmäquivalenzen sind, werden ihre Beweise großschrittiger und damit auch kompakter.
Die gleiche Beweismethodik lässt sich für alle rekursiven Datentypen anwenden. Insbesondere lässt sie sich auch für Listen anwenden.