परिचय
एक शाम आपके हाथ एक पुरानी नोटबुक लगी, जिसमें समझ न आने वाली घसीट भरी थी, मानो कोई जुनून की हद तक किसी विचार का पीछा कर रहा हो।
एक पेज पर एक ही सवाल सबसे अलग चमक रहा था: क्या हर संख्या 1 तक पहुँचने का रास्ता खोज ही लेती है?
यह किसी कोलाट्ज़ अनुमान नाम की चीज़ से जुड़ा था, ऐसी पहेली जिसने दशकों से विचारकों को उलझाए रखा है।
नियम ऊपर से बहुत आसान लगते थे।
कोई भी धनात्मक पूर्णांक चुनिए।
- अगर संख्या सम है, तो उसे 2 से भाग दीजिए।
- अगर संख्या विषम है, तो उसे 3 से गुणा कीजिए और 1 जोड़िए।
फिर इन्हीं चरणों को नतीजे पर दोहराइए, और यह क्रम इसी तरह अनंत तक चलता रहता है।
उत्सुक होकर आपने परखने के लिए संख्या 12 चुनी और यात्रा शुरू की:
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
दूसरी संख्या (6) से गिनें तो 1 तक पहुँचने में 9 चरण लगे, और जितनी बार ये नियम दोहराए गए, संख्या बदलती चली गई।
शुरू में यह क्रम अनुमान से परे लगा। कभी ऊपर उछलता, कभी नीचे, कभी इधर-उधर।
फिर भी यह अनुमान कहता है कि शुरुआती संख्या कोई भी हो, हम हमेशा 1 पर ही पहुँचेंगे।
यह बहुत दिलचस्प था, पर साथ ही हैरान करने वाला भी।
यह हर बार काम क्यों करता दिखता है?
क्या कोई ऐसी संख्या हो सकती है जहाँ यह प्रक्रिया टूट जाए, जो हमेशा के लिए लूप में फँस जाए या अनंत में निकल जाए?
नोटबुक में लिखा था कि शायद इसे सुलझाने से कोई बहुत गहरी बात सामने आए, और जो भी इसके राज़ खोल सकेगा, उसके लिए प्रसिद्धि, धन और इतिहास में एक जगह इंतज़ार कर रहे हैं।
निर्देश
एक धनात्मक पूर्णांक दिया गया हो, तो Collatz Conjecture के नियमों के अनुसार 1 तक पहुँचने में लगने वाले चरणों की संख्या लौटाइए।
सबटाइप
यह अभ्यास Positive नाम का एक सबटाइप परिभाषित करता है, जो 0 से बड़ी सभी प्राकृत संख्याओं के लिए है।
किसी सबटाइप को एक जोड़ी ⟨x, h⟩ के रूप में समझा जा सकता है, जहाँ x वैल्यू है और h उसकी वैधता का प्रमाण है।
सबटाइप के अंदर की वैल्यू (यहाँ x) तक .val इस्तेमाल करके पहुँचा जा सकता है, जैसे x.val.
उसका प्रमाण .property इस्तेमाल करके निकाला जा सकता है, जैसे x.property.
दोनों तक पैटर्न मैचिंग से भी पहुँचा जा सकता है, जैसा आम तौर पर होता है।
किसी सबटाइप के लिए वैल्यू बनाने के लिए उसकी वैधता सिद्ध करना ज़रूरी है, इस मामले में यह कि संख्या 0 से बड़ी है।
Lean में कई लेम्मा और प्रमेय हैं जो इस प्रमाण की शुरुआत के लिए काम आ सकते हैं।
उदाहरण के लिए, Nat.zero_lt_succ एक लेम्मा है जो बताता है कि किसी भी प्राकृत संख्या n के लिए: 0 < n + 1.
Lean में प्रमेय सिद्ध करने के लिए एक अच्छा संदर्भ मुख्य डॉक्यूमेंटेशन में मिलता है।
समापन का प्रमाण
Lean में रिकर्सिव फंक्शन को अपना समापन सिद्ध करना पड़ता है।
यह प्रमाण कभी-कभी सीधा होता है, जो फंक्शन की बनावट से अपने आप निकल आता है।
दूसरे मामलों में इसे साफ़-साफ़ लिखना पड़ता है।
इस अभ्यास में फंक्शन का समापन ठीक-ठीक collatz conjecture ही है, जो एक अनसुलझी गणितीय समस्या है।
इनमें से कोई एक विकल्प अपनाने पर विचार कीजिए:
- फंक्शन की घोषणा से पहले
partial कीवर्ड जोड़ना समापन की जाँच बंद कर देता है और (संभवतः असुरक्षित) रिकर्सिव कॉल की इजाज़त देता है।
- मोनैडिक कोड में इजाज़त वाले इम्परेटिव कंस्ट्रक्ट, जैसे
while, अंदर ही अंदर पार्शियल रिकर्सन से लागू किए जाते हैं, इसलिए जहाँ समापन अनिवार्य नहीं है वहाँ इनका इस्तेमाल किया जा सकता है।
Id मोनैड इस्तेमाल करना इन कंस्ट्रक्ट को बाकी शुद्ध दिखने वाले कोड में चालू करने का आसान तरीका है, बिना कोई अतिरिक्त इफेक्ट जोड़े।
- ज़्यादा से ज़्यादा कितनी रिकर्सिव कॉल हो सकती हैं, उसके लिए एक अतिरिक्त पैरामीटर वाला हेल्पर बनाने से समापन सुनिश्चित होता है।
