Einführung
Eines Abends stießt du auf ein altes Notizbuch voller kryptischer Kritzeleien, als hätte jemand besessen einer Idee nachgejagt.
Auf einer Seite stach eine einzige Frage hervor: Findet jede Zahl ihren Weg zur 1?
Sie war mit etwas verbunden, das Collatz-Vermutung genannt wird: ein Rätsel, das Denkern seit Jahrzehnten Kopfzerbrechen bereitet.
Die Regeln waren trügerisch einfach.
Wähle eine beliebige positive Ganzzahl.
- Wenn sie gerade ist, teile sie durch 2.
- Wenn sie ungerade ist, multipliziere sie mit 3 und addiere 1.
Dann wiederholst du diese Schritte mit dem Ergebnis, und das immer weiter.
Aus Neugier nahmst du die Zahl 12 und begannst die Reise:
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
Von der zweiten Zahl (6) an gerechnet brauchte es 9 Schritte bis zur 1, und mit jeder Wiederholung der Regeln veränderte sich die Zahl weiter.
Zuerst schien die Folge unberechenbar: mal ging es hinauf, mal hinunter, mal kreuz und quer.
Doch die Vermutung besagt, dass wir, egal mit welcher Zahl wir starten, immer bei 1 landen.
Das war faszinierend, aber auch rätselhaft.
Warum scheint das immer zu funktionieren?
Könnte es eine Zahl geben, bei der der Prozess zusammenbricht, endlos kreist oder ins Unendliche entweicht?
Das Notizbuch legte nahe, dass die Lösung etwas Tiefgründiges offenbaren könnte, und wer seine Geheimnisse lüftet, wird mit Ruhm, Reichtum und einem Platz in der Geschichte belohnt.
Anleitung
Gib für eine positive Ganzzahl die Anzahl der Schritte zurück, die nötig sind, um nach den Regeln der Collatz-Vermutung die 1 zu erreichen.
Subtype
In dieser Übung wird ein Subtype namens Positive definiert, und zwar für alle natürlichen Zahlen größer als 0.
Einen Subtype kann man sich als Paar ⟨x, h⟩ vorstellen, wobei x der Wert und h der Beweis seiner Gültigkeit ist.
Auf den Wert innerhalb eines Subtype (hier x) greifst du mit .val zu, zum Beispiel mit x.val.
Auf seinen Beweis greifst du mit .property zu, zum Beispiel mit x.property.
Auf beide kannst du wie gewohnt auch per Pattern Matching zugreifen.
Um einen Wert für einen Subtype zu konstruieren, musst du seine Gültigkeit beweisen, in diesem Fall also, dass die Zahl größer als 0 ist.
In Lean gibt es eine Reihe von Lemmata und Theoremen, die als Ausgangspunkt für diesen Beweis dienen können.
Zum Beispiel ist Nat.zero_lt_succ ein Lemma, das besagt, dass für jede natürliche Zahl n gilt: 0 < n + 1.
Eine gute Referenz für das Beweisen von Theoremen in Lean findest du in der Kerndokumentation.
Beweis der Terminierung
In Lean müssen rekursive Funktionen ihre Terminierung beweisen.
Dieser Beweis ist manchmal unkompliziert und ergibt sich implizit aus der Struktur einer Funktion.
In anderen Fällen musst du ihn explizit angeben.
In dieser Übung ist die Terminierung der Funktion genau die collatz conjecture, ein offenes mathematisches Problem.
Ziehe eine der folgenden Möglichkeiten in Betracht:
- Wenn du das Schlüsselwort
partial vor die Deklaration einer Funktion setzt, wird die Terminierungsprüfung deaktiviert und (potenziell unsichere) rekursive Aufrufe werden möglich.
- Imperative Konstrukte, die in monadischem Code erlaubt sind, etwa
while, sind intern mit partieller Rekursion umgesetzt. Du kannst sie also immer dann verwenden, wenn die Terminierung nicht erzwungen wird.
Die Id-Monade ist eine bequeme Möglichkeit, diese Konstrukte in Code zu nutzen, der ansonsten rein aussieht, ohne zusätzliche Effekte einzuführen.
- Wenn du einen Helfer mit einem zusätzlichen Parameter für die maximale Anzahl rekursiver Aufrufe definierst, ist die Terminierung gesichert.
