Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda
تقدم هذه الورقة صياغة لبناء أعداد كوشي الحقيقية القائم على نظرية النوع النوعية المتجانسة (Homotopy Type Theory) في لغة Cubical Agda، مظهرةً أن هذا النهج يتجنب مشكلات الاختيار القابل للعد، والأعباء الإضافية للـ setoid، وتتبع مستويات الكون المتأصلة في التعريفات البنائية الأخرى، مع القدرة على التحقق من صحة النوع دون الحاجة إلى مسلمات.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك تحاول بناء مسطرة مثالية، لانهائية، لقياس كل شيء في الكون. في عالم الرياضيات الكلاسيكية، وصف هذه المسطرة أمر سهل: ما عليك سوى أخذ جميع "القياسات التقريبية" الممكنة (مثل 3.1، 3.14، 3.141، إلخ) ثم تقول: "إذا اقتربت سلسلتان من القياسات من بعضهما البعض، فهما تمثلان نفس النقطة على المسطرة".
ومع ذلك، في الرياضيات التأسيسية (Constructive Mathematics) — وهو أسلوب رياضي يصر على أنه يجب أن تكون قادراً على بناء أو حساب الشيء الذي تتحدث عنه فعلياً — يصطدم هذا النهذا البسيط بحائط مسدود. لإثبات أن مسطرتك كاملة، يتعين عليك اتخاذ قرار سحري: يجب أن تختار قياساً واحداً محدداً من قائمة لانهائية من الخيارات لتمثيل النقطة النهائية. تقول الرياضيات التأسيسية: "لا يُسمح بالسحر هنا. إذا لم تستطع أن تريني كيف اخترت ذلك، فأنت لم تبنِ المسطرة بعد".
لعقود من الزمن، اضطر الرياضيون إلى تقديم تنازلات. فإما استخدموا حيل "التدقيق الحسابي" التي جعلت كل عملية حسابية معقدة، أو بنوا المسطرة بطريقة تتطلب تتبع "مستويات كونية" معقدة (مثل تتبع حجم الصناديق التي تضع فيها الأشياء).
المخطط الجديد (الأعداد الحقيقية في كتاب HoTT)
تقدم هذه الأطروحة مخططاً جديداً لبناء المسطرة، مأخوذاً من كتاب نظرية النوع الطوبولوجي (Homotopy Type Theory - HoTT) الشهير. بدلاً من بناء المسطرة عن طريق لصق القطع معاً ثم محاولة تنعيمها، تقوم هذه الطريقة ببناء المسطرة وقواعد "النعومة" في آن واحد.
تخيل أنك تبني منزلاً حيث يتم رسم الجدران والمخطط في اللحظة ذاتها:
- اللبنات: تبدأ بأرقام بسيطة ومعروفة (مثل الكسور).
- الغراء: تضيف قاعدة خاصة تقول: "إذا كانت نقطتان قريبتين بما يكفي، فهما في الواقع نفس النقطة".
- السحر: لأن قاعدة "القرب" مدمجة في تعريف المنزل نفسه، فلن تحتاج إلى اتخاذ تلك الاختيارات السحرية لاحقاً. يكون منزلك مكتملاً بمجرد انتهائك من وضع اللبنات.
التحدي: المترجم الحاسوبي
قام المؤلف، جاكسون بروف، بأخذ هذا المخطط النظري وحاول ترجمته إلى لغة يمكن للحاسوب فهمها والتحقق منها: Cubical Agda.
تخيل أنك تحاول شرح رقصة معقدة لروبوت لا يفهم إلا تعليمات صارمة وحرفية.
- المشكلة: فشلت المحاولات السابقة لترجمة هذا المخطط لأن لغة الحاسوب لم تكن تمتلك "الحركات" الصحيحة (تحديداً، لم تكن قادرة على التعامل مع التعريف المتزامن للمسطرة وقواعد القرب). كان على المترجمين أن يقولوا: "افترض أن هذه الحركة موجودة"، وهذا يعتبر غشاً في الرياضيات.
- الحل: لغة Cubical Agda هي روبوت أحدث وأذكى يفهم هذه الحركات المعقدة بشكل أصيل. فهي تسمح للمؤلف بكتابة المخطط تماماً كما صُمم، دون غش.
ماذا حدث أثناء الترجمة؟
هذه الأطروحة ليست مجرد كتابة كود برمجي؛ بل تتعلق بما حدث عندما حاول المؤلف جعل الحاسوب يفهم الرياضيات. لقد أجبرت صرامة الحاسوب المؤلف على اكتشاف فجوات خفية في الشرح الأصلي:
- الخريطة "البديلة": وصف الكتاب الأصلي كيفية التحقق مما إذا كانت نقطتان قريبتين. ولكن عندما حاول المؤلف كتابة الكود، أدرك أن طريقة الكتاب كانت مثل "شارع باتجاه واحد". يمكنك إثبات أن النقاط قريبة، لكن لا يمكنك بسهولة العودة للوراء لمعرفة لماذا. اضطر المؤلف لبناء خريطة ثانية "حسابية" (تسمى علاقة بديلة) تعمل مثل ناقل الحركة الخلفي، مما يسمح للحاسوب فعلياً بحساب الإجابة.
- المكون المفقود: وصف الكتاب قاعدة لبناء الدوال (مثل الضرب) كما لو كان بإمكان الحاسوب "تذكر" قائمة التقريبات الأصلية. نسخة الكود الأولى التي كتبها المؤلف نسيت هذه الذاكرة، فرفضها الحاسوب. اضطر المؤلف لإعادة كتابة القاعدة لتنقل الذاكرة معها بشكل صريح، مدركاً أن النص الأصلي كان غامضاً جداً بالنسبة لآلة.
- لغز المتغيرات المتعددة: ألمح الكتاب إلى أن القواعد الخاصة بالأرقام المفردة يمكن تطبيقها بسهولة على أزواج أو ثلاثيات من الأرقام. لم يكن الحاسوب مقتنعاً. اضطر المؤلف لإثبات "لمة" (Lemma) جديدة ومحددة تظهر أنه إذا كانت القاعدة تعمل لمتغير واحد، فإنها تعمل لمتغيرين، بشرداً أن يتم التحقق منهما واحداً تلو الآخر.
النتيجة
المنتج النهائي هو مكتبة ضخمة من الكود مفتوح المصدر (أكثر من 13,000 سطر) تثبت أن الأعداد الحقيقية في كتاب HoTT تعمل بشكل مثالي.
- تثبت أن هذه الأعداد تشكل حقلاً مرتباً كاملاً (يمكنك الجمع، الطرح، الضرب، القسمة، والمقارنة).
- تثبت أن المسطرة "أرخميدسية" (بمعنى أنه مهما كان الفراغ صغيراً، يمكنك دائماً إيجاد كسر يتسع بداخله).
- والأهم من ذلك، أنها تفعل كل هذا دون غش. لقد تحقق الحاسوب من كل خطوة، ويعمل الكود دون أي "افتراضات سحرية".
باختصار
هذه الأطروحة هي قصة أخذ فكرة رياضية رفيعة المستوى وجميلة، وإجبارها على النجاة في العالم الصارم والحرفي للتحقق الحاسوبي. ومن خلال القيام بذلك، لم يبنِ المؤلف مسطرة رقمية فحسب، بل قام بصقل المخطط نفسه، كاشفاً عن تفاصيل خفية وجعل النظرية أقوى وأكثر دقة مما كانت عليه. الكود متاح الآن لأي شخص لاستخدامه كأساس متين للاكتشافات الرياضية المستقبلية.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.