Οδηγίες
Προσδιόρισε αν ένας αριθμός είναι τέλειος, υπερτέλειος ή ελλιπής, με βάση το σύστημα ταξινόμησης του Nicomachus (60 - 120 μ.Χ.) για τους θετικούς ακέραιους.
Ο Έλληνας μαθηματικός Nicomachus επινόησε ένα σύστημα ταξινόμησης των θετικών ακεραίων, στο οποίο κάθε αριθμός ανήκει σε μία και μόνο κατηγορία: στους τέλειους, τους υπερτέλειους ή τους ελλιπείς αριθμούς, με βάση το άθροισμα γνησίων διαιρετών του.
Το άθροισμα γνησίων διαιρετών ορίζεται ως το άθροισμα των διαιρετών ενός αριθμού, χωρίς να συμπεριλαμβάνεται ο ίδιος ο αριθμός.
Για παράδειγμα, το άθροισμα γνησίων διαιρετών του 15 είναι 1 + 3 + 5 = 9.
Τέλειος αριθμός
Ένας αριθμός είναι τέλειος όταν ισούται με το άθροισμα γνησίων διαιρετών του.
Για παράδειγμα:
- Ο
6 είναι τέλειος αριθμός, γιατί 1 + 2 + 3 = 6
- Ο
28 είναι τέλειος αριθμός, γιατί 1 + 2 + 4 + 7 + 14 = 28
Υπερτέλειος αριθμός
Ένας αριθμός είναι υπερτέλειος όταν είναι μικρότερος από το άθροισμα γνησίων διαιρετών του.
Για παράδειγμα:
- Ο
12 είναι υπερτέλειος αριθμός, γιατί 1 + 2 + 3 + 4 + 6 = 16
- Ο
24 είναι υπερτέλειος αριθμός, γιατί 1 + 2 + 3 + 4 + 6 + 8 + 12 = 36
Ελλιπής αριθμός
Ένας αριθμός είναι ελλιπής όταν είναι μεγαλύτερος από το άθροισμα γνησίων διαιρετών του.
Για παράδειγμα:
- Ο
8 είναι ελλιπής αριθμός, γιατί 1 + 2 + 4 = 7
- Οι πρώτοι αριθμοί είναι ελλιπείς
Εργασία
Υλοποίησε έναν τρόπο να προσδιορίζεις αν ένας δεδομένος αριθμός είναι τέλειος.
Ανάλογα με τη γλώσσα προγραμματισμού που χρησιμοποιείς, μπορεί επίσης να χρειαστεί να υλοποιήσεις έναν τρόπο να προσδιορίζεις αν ένας δεδομένος αριθμός είναι υπερτέλειος ή ελλιπής.
Ορισμός ενός επαγωγικού τύπου
Αυτή η άσκηση περιμένει η τιμή επιστροφής να είναι ένας επαγωγικός τύπος Classification που πρέπει να ορίσεις.
Αυτός ο τύπος πρέπει να έχει ένα στιγμιότυπο BEq, δηλαδή να επιδέχεται έλεγχο ισότητας Boolean, και ένα στιγμιότυπο Repr, δηλαδή οι τιμές του τύπου να μπορούν να μορφοποιηθούν για εμφάνιση.
Μπορείς να ανατρέξεις σε αυτή τη σελίδα για τις δηλώσεις στιγμιότυπων.
Το Lean μπορεί να δημιουργήσει αυτόματα στιγμιότυπα για πολλές κλάσεις.
Υποτύποι
Το όρισμα της συνάρτησης classify είναι ένας υποτύπος που ονομάζεται Positive:
def Positive := { x : Nat // x > 0 }
Οι υποτύποι αναπαριστούν στοιχεία ενός συγκεκριμένου τύπου που ικανοποιούν ένα κατηγόρημα.
Ο Positive αναπαριστά στοιχεία του Nat που είναι μεγαλύτερα από το 0.
Κάθε στοιχείο ενός υποτύπου μπορεί να θεωρηθεί ως ένα ζεύγος που αποτελείται από μια τιμή του υποκείμενου τύπου και μια απόδειξη, με τη μαθηματική έννοια, ότι αυτή η τιμή ικανοποιεί το αντίστοιχο κατηγόρημα.
Οι υποτύποι επιβάλλουν αναλλοίωτα σε επίπεδο τύπου, διασφαλίζοντας ότι δεν μπορούν να κατασκευαστούν κακοσχηματισμένες τιμές.
