مقدمه
یک شب، چشمتان به دفترچهی قدیمیای افتاد که پر از خطخطیهای رمزآلود بود، انگار کسی وسواسگونه دنبال یک ایده افتاده بود.
در یکی از صفحهها، پرسشی بود که خودنمایی میکرد: آیا هر عددی میتواند راهش را به ۱ پیدا کند؟
این پرسش به چیزی به اسم حدس کولاتز گره خورده بود، معمایی که دههها ذهن اندیشمندان را به خود مشغول کرده است.
قواعد بهشکلی فریبنده ساده به نظر میرسیدند.
هر عدد صحیح مثبتی را انتخاب کنید.
- اگر زوج باشد، آن را بر ۲ تقسیم کنید.
- اگر فرد باشد، آن را در ۳ ضرب کنید و ۱ را به آن اضافه کنید.
سپس این مراحل را با نتیجه تکرار کنید و همینطور تا بینهایت ادامه دهید.
از روی کنجکاوی، عدد ۱۲ را برای آزمایش انتخاب کردید و سفر را آغاز کردید:
۱۲ ➜ ۶ ➜ ۳ ➜ ۱۰ ➜ ۵ ➜ ۱۶ ➜ ۸ ➜ ۴ ➜ ۲ ➜ ۱
اگر از عدد دوم (۶) شروع به شمردن کنیم، ۹ گام طول کشید تا به ۱ برسیم و هر بار که قواعد تکرار میشد، عدد مدام تغییر میکرد.
در ابتدا، دنباله غیرقابلپیشبینی به نظر میرسید، طوری که بالا و پایین و به هر طرف میپرید.
با این حال، این حدس ادعا میکند که هر عددی که شروع کنیم، همیشه به ۱ میرسیم.
این هم جذاب بود و هم گیجکننده.
چرا این کار همیشه جواب میدهد؟
آیا ممکن است عددی وجود داشته باشد که فرایند در آن بشکند و تا ابد در حلقهای بیفتد یا به بینهایت بگریزد؟
دفترچه اشاره میکرد که حل این مسئله میتواند موضوعی عمیق را آشکار کند و همراه با آن، شهرت، ثروت و جایگاهی در تاریخ در انتظار کسی است که بتواند رازهایش را بگشاید.
دستورالعملها
یک عدد صحیح مثبت به شما داده میشود؛ تعداد گامهایی را که برای رسیدن به ۱ بر اساس قواعد حدس کولاتز لازم است، برگردانید.
زیرنوع
این تمرین یک زیرنوع به نام Positive تعریف میکند که همهی اعداد طبیعی بزرگتر از ۰ را در بر میگیرد. زیرنوع را میتوان جفتی مانند ⟨x, h⟩ در نظر گرفت که x مقدار و h اثبات درستی آن است.
مقدار درون یک زیرنوع (در اینجا x) را میتوان با استفاده از .val به دست آورد، برای مثال x.val. اثبات آن را هم میتوان با استفاده از .property به دست آورد، برای مثال x.property. هر دو را نیز مانند همیشه میتوان با تطبیق الگو به دست آورد.
برای ساختن یک مقدار برای یک زیرنوع، باید درستی آن را اثبات کنید، در اینجا اینکه عدد بزرگتر از ۰ است.
در Lean چند لم و قضیه وجود دارد که میتواند نقطهی شروعی برای این اثبات باشد. برای مثال، Nat.zero_lt_succ لمی است که بیان میکند برای هر عدد طبیعی n: 0 < n + 1.
مرجع خوبی برای اثبات قضیه در Lean را میتوانید در مستندات اصلی پیدا کنید.
اثبات خاتمه
در Lean، توابع بازگشتی باید خاتمهی خود را اثبات کنند. این اثبات گاهی ساده است و بهطور ضمنی از ساختار تابع نتیجه میشود. در موارد دیگر باید آن را صریح بیان کرد.
در این تمرین، خاتمهی تابع دقیقاً همان collatz conjecture است که یک مسئلهی باز ریاضی به شمار میرود.
بهتر است یکی از این گزینهها را در نظر بگیرید:
- افزودن کلیدواژهی
partial پیش از اعلان یک تابع، بررسی خاتمه را غیرفعال میکند و فراخوانیهای بازگشتی (احتمالاً ناایمن) را ممکن میسازد.
- ساختارهای امری که در کد مونادی مجاز هستند، مانند
while، در پشت صحنه با بازگشت جزئی پیادهسازی میشوند، بنابراین هر جا که خاتمه اجباری نباشد میتوان از آنها استفاده کرد.
استفاده از موناد Id روش راحتی است برای فعال کردن این ساختارها در کدی که در ظاهر خالص به نظر میرسد، بدون افزودن اثرهای اضافی.
- تعریف یک تابع کمکی با یک پارامتر اضافی برای بیشترین تعداد فراخوانیهای بازگشتی، خاتمه را تضمین میکند.
