Εισαγωγή
Ένα βράδυ, σκόνταψες πάνω σε ένα παλιό σημειωματάριο γεμάτο αινιγματικά μουτζουρώματα, λες και κάποιος κυνηγούσε ιδεοληπτικά μια ιδέα.
Σε μια σελίδα, ξεχώριζε μια μόνο ερώτηση: Μπορεί κάθε αριθμός να βρει τον δρόμο του προς το 1;
Ήταν συνδεδεμένη με κάτι που ονομάζεται Εικασία Collatz, ένα παζλ που μπερδεύει τους στοχαστές εδώ και δεκαετίες.
Οι κανόνες ήταν παραπλανητικά απλοί.
Διάλεξε οποιονδήποτε θετικό ακέραιο.
- Αν είναι άρτιος, διαίρεσέ τον με το 2.
- Αν είναι περιττός, πολλαπλασίασέ τον επί 3 και πρόσθεσε 1.
Στη συνέχεια, επανάλαβε αυτά τα βήματα με το αποτέλεσμα, συνεχίζοντας επ' άπειρον.
Από περιέργεια, διάλεξες τον αριθμό 12 για να τον δοκιμάσεις και ξεκίνησες το ταξίδι:
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
Μετρώντας από τον δεύτερο αριθμό (6), χρειάστηκαν 9 βήματα για να φτάσει στο 1, και κάθε φορά που επαναλαμβάνονταν οι κανόνες, ο αριθμός άλλαζε συνεχώς.
Στην αρχή, η ακολουθία φαινόταν απρόβλεπτη: πηδούσε πάνω, κάτω και από εδώ και από εκεί.
Ωστόσο, η εικασία ισχυρίζεται ότι, ανεξάρτητα από τον αρχικό αριθμό, πάντα θα καταλήγουμε στο 1.
Ήταν συναρπαστικό, αλλά και αινιγματικό.
Γιατί αυτό φαίνεται να λειτουργεί πάντα;
Θα μπορούσε να υπάρχει ένας αριθμός όπου η διαδικασία καταρρέει, παγιδεύεται σε ατέρμονο βρόχο ή ξεφεύγει στο άπειρο;
Το σημειωματάριο άφηνε να εννοηθεί ότι η επίλυσή της θα μπορούσε να αποκαλύψει κάτι βαθύ, και μαζί με αυτό, φήμη, πλούτο και μια θέση στην ιστορία περιμένουν όποιον καταφέρει να ξεκλειδώσει τα μυστικά της.
Οδηγίες
Δεδομένου ενός θετικού ακέραιου, επέστρεψε τον αριθμό των βημάτων που χρειάζονται για να φτάσεις στο 1, σύμφωνα με τους κανόνες της Εικασίας Collatz.
Subtypes
Αυτή η άσκηση ορίζει ένα Subtype με το όνομα Positive, για όλους τους φυσικούς αριθμούς που είναι μεγαλύτεροι του 0.
Ένα Subtype μπορεί να ιδωθεί ως ένα ζεύγος ⟨x, h⟩, όπου το x είναι η τιμή και το h είναι η απόδειξη της εγκυρότητάς του.
Η τιμή μέσα σε ένα Subtype (το x, στην περίπτωση αυτή) είναι προσβάσιμη με το .val, για παράδειγμα x.val.
Η απόδειξή του είναι προσβάσιμη με το .property, για παράδειγμα x.property.
Και τα δύο είναι επίσης προσβάσιμα μέσω αντιστοίχισης προτύπων, όπως συνήθως.
Για να κατασκευάσεις μια τιμή για ένα Subtype, είναι απαραίτητο να αποδείξεις την εγκυρότητά της, στην περίπτωση αυτή, ότι ο αριθμός είναι μεγαλύτερος του 0.
Υπάρχουν αρκετά λήμματα και θεωρήματα στο Lean που μπορούν να χρησιμεύσουν ως αφετηρία για αυτή την απόδειξη.
Για παράδειγμα, το Nat.zero_lt_succ είναι ένα λήμμα που δηλώνει ότι για κάθε φυσικό αριθμό n: 0 < n + 1.
Μια καλή πηγή αναφοράς για την απόδειξη θεωρημάτων στο Lean βρίσκεται στην βασική τεκμηρίωση.
Απόδειξη τερματισμού
Στο Lean, οι αναδρομικές συναρτήσεις πρέπει να αποδεικνύουν τον τερματισμό τους.
Αυτή η απόδειξη μερικές φορές είναι απλή και προκύπτει σιωπηρά από τη δομή μιας συνάρτησης.
Σε άλλες περιπτώσεις, πρέπει να γίνει ρητή.
Σε αυτή την άσκηση, ο τερματισμός της συνάρτησης είναι ακριβώς η collatz conjecture, που αποτελεί ένα ανοιχτό μαθηματικό πρόβλημα.
Σκέψου να χρησιμοποιήσεις μία από τις παρακάτω επιλογές:
- Η προσθήκη της λέξης-κλειδί
partial πριν από τη δήλωση μιας συνάρτησης απενεργοποιεί τον έλεγχο τερματισμού και επιτρέπει (δυνητικά μη ασφαλείς) αναδρομικές κλήσεις.
- Οι προστακτικές δομές που επιτρέπονται σε κώδικα με μονάδες, όπως ο
while, υλοποιούνται με μερική αναδρομή στο παρασκήνιο, οπότε μπορούν να χρησιμοποιηθούν όποτε ο τερματισμός δεν επιβάλλεται.
Η χρήση της μονάδας Id είναι ένας βολικός τρόπος να ενεργοποιήσεις αυτές τις δομές σε κώδικα που κατά τα άλλα φαίνεται καθαρός, χωρίς να εισαγάγεις πρόσθετες παρενέργειες.
- Ο ορισμός μιας βοηθητικής συνάρτησης με μια επιπλέον παράμετρο για τον μέγιστο αριθμό αναδρομικών κλήσεων εξασφαλίζει τον τερματισμό.
