ভূমিকা
এক সন্ধ্যায় হঠাৎ আপনার হাতে পড়ে গেল একটি পুরোনো নোটবুক, রহস্যময় আঁকিবুঁকিতে ভরা, যেন কেউ এক নেশায় কোনো একটি ভাবনার পেছনে ছুটে চলছিল।
একটি পাতায় স্পষ্ট হয়ে উঠল একটি প্রশ্ন: প্রতিটি সংখ্যা কি নিজের পথ খুঁজে ১-এ পৌঁছাতে পারে?
প্রশ্নটি জড়িয়ে ছিল কোলাটজ অনুমান নামের একটি ধাঁধার সঙ্গে, যা কয়েক দশক ধরে চিন্তাবিদদের হতবাক করে রেখেছে।
নিয়মগুলো ছিল আপাতদৃষ্টিতে সহজ।
যেকোনো একটি ধনাত্মক ইন্টিজার বেছে নিন।
- এটি জোড় হলে, এটিকে ২ দিয়ে ভাগ করুন।
- এটি বিজোড় হলে, এটিকে ৩ দিয়ে গুণ করুন এবং ১ যোগ করুন।
এরপর ফলাফলটি নিয়ে একই ধাপগুলো আবার করুন, এভাবে অনির্দিষ্টকাল চলতে থাকুক।
কৌতূহলী হয়ে আপনি পরীক্ষা করার জন্য ১২ নম্বরটি বেছে নিয়ে যাত্রা শুরু করলেন:
১২ ➜ ৬ ➜ ৩ ➜ ১০ ➜ ৫ ➜ ১৬ ➜ ৮ ➜ ৪ ➜ ২ ➜ ১
দ্বিতীয় সংখ্যা (৬) থেকে গুনতে শুরু করলে ১-এ পৌঁছাতে লেগেছিল ৯টি ধাপ, আর নিয়মগুলো প্রতিবার পুনরাবৃত্তি হওয়ার সঙ্গে সঙ্গে সংখ্যাটি বদলাতেই থাকল।
শুরুতে ক্রমটি অনুমানযোগ্য মনে হচ্ছিল না, এদিক-ওদিক, ওপর-নিচ, সর্বত্র লাফিয়ে চলছিল।
তবুও অনুমানটি দাবি করে, শুরুর সংখ্যা যা-ই হোক, শেষে আমরা সবসময় ১-এ পৌঁছাব।
এটা ছিল মুগ্ধকর, আবার একইসঙ্গে রহস্যজনক।
কেন এটা সবসময় কাজ করে বলে মনে হয়?
হতে পারে এমন কোনো সংখ্যা আছে, যেখানে প্রক্রিয়াটি ভেঙে পড়ে, চিরকালের জন্য লুপ করে ঘোরে, বা অসীমের দিকে পালিয়ে যায়?
নোটবুকটি ইঙ্গিত দিচ্ছিল, এটি সমাধান করলে হয়তো গভীর কোনো কিছু প্রকাশ পাবে, আর এর রহস্য উন্মোচন করতে পারলেই আপনার জন্য অপেক্ষা করছে খ্যাতি, ভাগ্য আর ইতিহাসে এক স্থান।
নির্দেশনা
একটি ধনাত্মক ইন্টিজার দেওয়া হলে, 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 মোনাড ব্যবহার করা হলো এমন একটি সুবিধাজনক উপায়, যা নাহলে বিশুদ্ধ দেখতে কোডে অতিরিক্ত এফেক্ট আনা ছাড়াই এই কনস্ট্রাক্টগুলো চালু করে।
- সর্বোচ্চ কতবার রিকার্সিভ কল হবে তা বোঝানোর জন্য একটি বাড়তি প্যারামিটারসহ একটি হেল্পার ডিফাইন করলে টার্মিনেশন নিশ্চিত হয়।
