Anleitung
Bestimme anhand des Klassifikationsschemas von Nicomachus (60 - 120 n. Chr.) für positive Ganzzahlen, ob eine Zahl perfect, abundant oder deficient ist.
Der griechische Mathematiker Nicomachus entwickelte ein Klassifikationsschema für positive Ganzzahlen. Es ordnet jede Zahl anhand ihrer Aliquotsumme eindeutig einer der Kategorien perfect, abundant oder deficient zu.
Die Aliquotsumme ist definiert als die Summe der Teiler einer Zahl, wobei die Zahl selbst nicht mitgezählt wird.
Zum Beispiel ist die Aliquotsumme von 15 gleich 1 + 3 + 5 = 9.
Perfect
Eine Zahl ist perfect, wenn sie gleich ihrer Aliquotsumme ist.
Zum Beispiel:
-
6 ist perfect, weil 1 + 2 + 3 = 6
-
28 ist perfect, weil 1 + 2 + 4 + 7 + 14 = 28
Abundant
Eine Zahl ist abundant, wenn sie kleiner als ihre Aliquotsumme ist.
Zum Beispiel:
-
12 ist abundant, weil 1 + 2 + 3 + 4 + 6 = 16
-
24 ist abundant, weil 1 + 2 + 3 + 4 + 6 + 8 + 12 = 36
Deficient
Eine Zahl ist deficient, wenn sie größer als ihre Aliquotsumme ist.
Zum Beispiel:
-
8 ist deficient, weil 1 + 2 + 4 = 7
- Primzahlen sind deficient
Aufgabe
Implementiere eine Möglichkeit, festzustellen, ob eine gegebene Zahl perfect ist.
Je nach deinem Sprach-Track musst du vielleicht auch eine Möglichkeit implementieren, festzustellen, ob eine gegebene Zahl abundant oder deficient ist.
Einen induktiven Typ definieren
Diese Übung erwartet als Rückgabewert einen induktiven Typ Classification, den du selbst definieren musst.
Dieser Typ muss eine BEq-Instanz haben, also einen booleschen Gleichheitstest zulassen, und eine Repr-Instanz, das heißt, Werte des Typs lassen sich für die Ausgabe formatieren.
Wie du Instanzen deklarierst, erfährst du auf dieser Seite.
Lean kann für viele Klassen automatisch Instanzen generieren.
Untertypen
Das Argument der Funktion classify ist ein Untertyp namens Positive:
def Positive := { x : Nat // x > 0 }
Untertypen repräsentieren Elemente eines bestimmten Typs, die ein Prädikat erfüllen.
Positive repräsentiert die Elemente von Nat, die größer als 0 sind.
Jedes Element eines Untertyps kann man sich als Paar vorstellen, das aus einem Wert des zugrunde liegenden Typs und einem Beweis im mathematischen Sinn besteht, dass dieser Wert das entsprechende Prädikat erfüllt.
Untertypen erzwingen Invarianten auf Typebene und stellen so sicher, dass sich fehlerhaft gebildete Werte nicht konstruieren lassen.
