Justification Logic of the Lambda Calculus

تخيل عالماً حيث كل فكرة تراودك هي أيضاً قطعة من الكود البرمجي، وكل قطعة كود هي برهان يثبت أن فكرتك منطقية. هذا هو التقاطع الغريب والجميل بين علوم الحاسوب والمنطق المعروف باسم "تناظر كوري-هوارد" (Curry-Howard correspondence). فكر في الأمر كأنه قاموس سحري حيث كلمتا "برهان" و"برنامج" هما في الواقع مترادفتان. إذا استطعت كتابة برنامج حاسوبي يعمل دون أن يتوقف عن العمل (crash)، فقد أثبتت رياضياً صحة عبارة ما. لعقود من الزمن، استخدم العلماء هذه الفكرة لبناء أنظمة يمكن للحواسيب من خلالها التحقق من عملها الخاص، مما يضمن أن المنطق الكامن وراء تحديث برمجيات ما هو بصلابة نظرية رياضية. ولكن هناك عقبة: عادةً ما تعامل هذه الأنظمة "البرهان" (المنطق) و"البرنامج" (الحوسبة) كلغتين مختلفتين تصادف أنهما تبدوان متشابهتين. إنهما يشبهان شخصين يتحدثان لهجتين مختلفتين من نفس اللغة؛ يفهم كل منهما الآخر، لكنهما ليسا الشخص نفسه تماماً.

هنا تصبح القصة مثيرة للاهتمام. ماذا لو لم نكتفِ بالترجمة بين الاثنين، بل دمجناهما فعلياً في لغة واحدة فائقة القوة؟ ماذا لو لم يكن "البرهان" مجرد ملصق مرفق بالبرنامج، بل كان هو البرنامج نفسه؟ هذا هو السؤال الكبير الذي يتناوله سيلفيا غيليزان وباراس باديار في ورقته البحثية الجديدة. إنهما يتساءلان: هل يمكننا بناء نظام منطقي يكون فيه فعل الحوسبة هو نفسه فعل الإثبات؟ هما لا يقترحان فقط أن هذه فكرة رائعة؛ بل قاما ببناء المخطط الفعلي، وكتابة القواعد، وإثبات أن النظام يعمل دون أن ينهار. لقد أطلقا على هذا النظام الجديد اسم "Jλ" (يُنطق "جي-لامدا")، وهو مصمم للسماح للحاسوب بالتفكير في حساباته في الوقت الفعلي، مما يمحو الخط الفاصل بين "التفكير" و"الفعل" حتى يصبحا شيئاً واحداً.

المنطق الجديد لـ "الفعل"

يقدم المؤلفان نوعاً جديداً من المنطق يسمى منطق التبرير لحساب لامدا (Justification Logic of the Lambda Calculus - Jλ). لفهم ما يجعل هذا النظام مميزاً، تخيل أنك محقق يحاول حل لغز. في المنطق القياسي، قد يكون لديك ملف مكتوب عليه "برهان الجريمة". وبداخله، تجد ملاحظة تقول: "لقد أثبتُّ ذلك بسبب س، ص، وع". الملف هو البرهان، لكن الملاحظة بداخله هي مجرد وصف. في الأنظمة القديمة (مثل منطق البراهين، أو LP)، يكون "البرهان" جسماً ثابتاً، مثل شهادة.

لكن نظام Jλ الذي طوره غيليزان وباديار يغير قواعد اللعبة. في نظامهم، ليس "البرهان" شهادة؛ بل هو الفعل نفسه. تخيل بدلاً من وجود ملف، أن لديك بثاً فيديوياً مباشراً للمحقق وهو يحل الجريمة. الفيديو هو البرهان. إذا قام المحقق بحركة ما، يتحدث البرهان فوراً. في Jλ، "مصطلحات البرهان" هي بالضبط ذاتها البرامج الحاسوبية (المسماة $\lambda$-terms) التي تقوم بالعمل. عندما يقول النظام "أنا أعلم أن A صحيحة"، فهو لا يكتفي برفع لافتة تقول ذلك؛ بل يمسك بالكود الفعلي الذي يحسب A. وهذا يعني أن المنطق يمكنه التفكير في حساباته الخاصة في آن واحد. إنه يشبه روبوتاً يمكنه التفكير في كيفية تفكيره أثناء قيامه بعملية التفكير.

بناء الآلة: قواعد اللعبة

لا تكتفي الورقة البحثية باقتراح هذه الفكرة فحسب؛ بل تبني المحرك بأكمله من الصفر. يبدأ المؤلفان بكتابة البديهيات (axioms)، وهي القواعد الأساسية للعبة. يأخذان القواعد القياسية للمنطق الحدسي (نوع من المنطق المستخدم في علوم الحاسوب يتطلب منك بناء برهان فعلي لتقول إن شيئاً ما صحيح) ويضيفان عامل "صندوق" خاص. في المنطق العادي، قد يقول الصندوق "من الضروري أن A". في Jλ، يتم استبدال هذا الصندوق بقطعة كود محددة، تُكتب كـ $[t]A$، والتي تعني "الكود $t$ هو برهان على أن A صحيحة".

ثم يوضحان كيف يمكن لهذا النظام أن يستوعب داخلياً (internalize) استنتاجاته الخاصة. هذه طريقة منمقة للقول إن النظام يمكنه النظر إلى خطواته الخاصة والقول: "مهلاً، لقد قمت بهذه الخطوة للتو، وإليك الكود الذي يثبت أنني قمت بها بشكل صحيح". وهما يثبتان أنه إذا استطاع النظام استنباط نظرية، فإنه يمكنه تلقائياً توليد الكود المحدد (مصطلح البرهان) الذي يبرر تلك النظرية. إنه يشبه سيارة ذاتية القيادة لا تكتفي بالقيادة إلى المتجر فحسب، بل تكتب أيضاً سجلاً مفصلاً لكل منعطف اتخذته، مما يثبت أنها اتبعت القواعد طوال الوقت.

جولة الخطوات الثلاث: من القواعد إلى الواقع

للتأكد من أن منطقهم الجديد ليس مجرد خيال، يأخذ المؤلفان القارئ في "جولة" عبر ثلاث طرق مختلفة للنظر إلى النظام، مما يثبت أن جميعها تؤدي إلى نفس النتيجة.

1. كتاب القواعد (النظام البديهي): أولاً، يكتبون القواعد مثل الدستور. يظهرون أنه إذا اتبعت هذه القواعد، يمكنك استنباط نظريات. ويثبتون أن النظام "يستوعب ذاتياً"، مما يعني أنه يمكنه دائماً توليد كود البرهان لأي شيء يدعي صحته.
2. الورشة (الاستنباط الطبيعي): بعد ذلك، يبنون نظام "استنباط طبيعي". فكر في هذا كورشة عمل تقوم فيها ببناء البراهين خطوة بخطوة، مثل تجميع الأثاث. يقدمون نسخة "مُنمّطة" (typed) من هذه الورشة (تسمى $\lambda J\lambda$) حيث يكون لكل قطعة خشب (كل مصطلح) تسمية (نوع) محددة. ويظهرون أن "البراهين" التي تبنيها هنا تتطابق تماماً مع "مصطلحات البرهان" من كتاب القواعد. إنه يشبه إظهار أن التعليمات الموجودة في الدليل تطابق القطع الموجودة في الصندوق بالفعل.
3. المصنع (حساب المتتاليات): أخيراً، ينشئون "حساب متتاليات" (sequent calculus)، وهو يشبه خط تجميع سريع في مصنع للبراهن. يثبتون خاصية حاسمة تسمى حذف القطع (cut-elimination). بعبارات بسيطة، "القطع" يشبه أخذ طريق مختصر في البرهان—استخدام نتيجة من مكان آخر دون إظهار كيفية الوصول إليها. "حذف القطع" يعني أنه يمكنك دائماً إزالة هذه الاختصارات وإعادة كتابة البرهان لإظهار كل خطوة من البداية. يثبت المؤلفون أن نظامهم يمكنه دائماً القيام بذلك، مما يضمن أن النظام "قابل للتطبيع" (normalizable). وهذا يعني أن البراهن ستستقر في النهاية دائماً في شكل نظيف ومعياري دون أن تتعثر في حلقات مفرغة لا نهائية.

لماذا يهم هذا (وما لا يفعله)

يفرق المؤلفون بعناية بين عملهم والمحاولات السابقة. في الماضي، حاول الباحثون ربط المنطق بالحوسبة، لكنهم غالباً ما اصطدموا بحائط: كان المنطق بسيطاً جداً بحيث لا يمكنه التعامل مع الحيل المعقدة التي يمكن للبرامج الحاسوبية القيام بها. يشير المؤلفون إلى أن نظامهم متميز لأن بنيته قائمة مباشرة على حساب لامدا ($\lambda$-calculus) (أساس البرمجة الوظيفية). هم لا يحاولون فرض شكل مربع في ثقب مستدير؛ فالمنطق والكود مصنوعان من المادة نفسها.

كما يوضحون ما لا يفعله نظامهم. هم لا يحاولون استبدال كل الرياضيات أو حل كل مشكلة في علوم الحاسوب. بدلاً من ذلك، يركزون تحديداً على "الجزء السلبي" من المنطق (التعامل مع "و" و "يقتضي"). ويثبتون أنه ضمن هذا النطاق المحدد، يعمل نظامهم بشكل مثالي. يظهرون أنه يمكنك أخذ برهان من نظامهم وترجمته للعودة إلى برنامج حاسوبي قياسي، والعكس صحيح، دون فقدان أي معلومات.

الخلاصة

لقًد نجح غيليزان وباديار في بناء إطار منطقي جديد حيث يختفي الحد الفاصل بين "إثبات حقيقة" و"تشغيل برنامج". لقد قدموا البديهيات، وقواعد الاستنباط الطبيعي، وحساب المتتاليات، وأثبتوا بصرامة أن هذه الرؤى المختلفة متسقة مع بعضها البعض. لقد أظهروا أن هذا النظام يمكنه التفكير في حساباته الخاصة، وتوليد مصطلحات برهان لا يمكن تمييزها عن البرامج نفسها. ورغم أنهم لا يدعون أنهم حلوا كل لغز في المنطق، إلا أنهم قدموا نموذجاً عملياً صلباً حيث يمكن للحاسوب حقاً فهم الكود الخاص به كبرهان رياضي، مما يفتح الباب أمام أنظمة برمجية أكثر قوة وذاتية التحقق في المستقبل.