مقدمة
في إحدى الأمسيات، عثرت على دفتر قديم مليء بخربشات غامضة، وكأن أحدهم كان يطارد فكرة بلا هوادة.
في إحدى الصفحات، برز سؤال واحد: هل يستطيع كل عدد أن يجد طريقه إلى 1؟
وكان مرتبطًا بشيء يُسمى حدسية كولاتز، وهي أحجية حيّرت المفكرين لعقود.
كانت القواعد بسيطة ظاهريًا.
اختر أي عدد صحيح موجب.
- إذا كان زوجيًا، اقسمه على 2.
- إذا كان فرديًا، اضربه في 3 ثم أضف 1.
ثم كرّر هذه الخطوات على الناتج، واستمر بلا نهاية.
وبدافع الفضول، اخترت العدد 12 لتجربته وبدأت الرحلة:
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
وبالعدّ من العدد الثاني (6)، استغرقت تسع خطوات للوصول إلى 1، وفي كل مرة كانت القواعد تتكرر، كان العدد يتغير باستمرار.
في البداية، بدا التسلسل غير متوقع، يقفز صعودًا وهبوطًا وفي كل اتجاه.
ومع ذلك، تؤكد الحدسية أنه مهما كان عدد البداية، فسننتهي دائمًا عند 1.
كان الأمر مذهلًا، لكنه محيّر أيضًا.
لماذا يبدو هذا ناجحًا دائمًا؟
هل يمكن أن يوجد عدد تتعطل عنده العملية، فيدور في حلقة لا نهاية لها أو يهرب إلى ما لا نهاية؟
أشار الدفتر إلى أن حل هذه المسألة قد يكشف شيئًا عميقًا، ومعه ينتظر الشهرة والثروة ومكانة في التاريخ كل من يستطيع فك ألغازها.
التعليمات
بالنظر إلى عدد صحيح موجب، أرجِع عدد الخطوات اللازمة للوصول إلى 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 وسيلة ملائمة لتمكين هذه التراكيب في كود يبدو نقيًا فيما عدا ذلك، دون إدخال تأثيرات إضافية.
- تعريف دالة مساعدة بمعامل إضافي يمثّل الحد الأقصى لعدد الاستدعاءات العودية يضمن الإنهاء.
