الخلاصة

  • كانت الأداة التكتيكية في Edinburgh LCF تقترح أهدافاً فرعية وتعيد دالة validation. ولا يصبح الناتج نظرية إلا حين تركّب هذه الدالة نظريات الأهداف الفرعية بواسطة قواعد الاستدلال البدائية المحمية.
  • قلّص النوع المجرّد thm مساحة الشيفرة التي تملك سلطة مباشرة لبناء النظريات، لكنه لم يثبت اتساق المنطق أو مطابقة المواصفات للواقع أو خلو المترجم وبيئة التشغيل والعتاد من العيوب.
  • الإنجاز جماعي: قدّم Dana Scott المنطق الأساسي، وسبق Stanford LCF نظام Edinburgh، وأسهم Michael Gordon وChristopher Wadsworth وLockwood Morris وMalcolm Newey وباحثون آخرون في LCF وML.

انتهاء البحث لا يعني قبول النظرية

يعمل البرهان التفاعلي غالباً من الهدف إلى الخلف. تقسّم الأداة التكتيكية الهدف، وتجرب إعادة الكتابة، وتختار بين بدائل، ثم تتراجع عند الفشل. قد يبدو السجل الطويل مقنعاً، لكنه لا يجيب وحده عن سؤال LCF الحاسم: هل تستطيع الواجهة المحمية بناء النظرية المطلوبة؟

تعيد الأداة مع الأهداف الفرعية دالة validation. تأخذ هذه الدالة قيم النظريات التي تثبت الأهداف الفرعية، ثم يجب أن تنتج منها نظرية الهدف الأصلي. وهكذا يُسوّى البحث إلى الخلف لاحقاً باستدلال إلى الأمام. إذا عجزت validation عن الوفاء بوعدها، فلا تتحول رسالة النجاح إلى برهان مقبول.

عالج هذا الفصل توتراً عملياً بين القابلية للتوسعة والثقة. يحتاج المستخدمون إلى كتابة طرق إثبات جديدة، ومن الطبيعي أن تخطئ تلك الشيفرة. لو استطاع كل امتداد إنشاء نظرية مباشرة، لاتسعت مساحة الثقة مع كل تكتيك. لذلك وضع Edinburgh LCF النظريات خلف نوع مجرّد يسمى عادة thm، وجعل البديهيات وقواعد الاستدلال البدائية العمليات المسموح لها بإرجاع قيم من ذلك النوع.

لم تصبح التكتيكات معصومة. يمكن أن تدور بلا نهاية، أو تختار أهدافاً سيئة، أو تطلق استثناءً، أو تعيد validation غير صالحة. الضمان المعماري أضيق: الخطأ خارج الواجهة لا يفتح مُنشئاً بديلاً. النتيجة المعتادة هي عدم الحصول على النظرية المطلوبة.

من Stanford إلى Edinburgh: عمل فريق

وصف Robin Milner عام 1972 مدققاً منفذاً لمنطق Logic for Computable Functions الذي وضعه Dana Scott. أظهر Stanford LCF إمكان الدعم الآلي، كما كشف كلفة البراهين الطويلة منخفضة المستوى. بعد انتقال Robin Milner إلى Edinburgh عام 1973، اتجه المشروع إلى بيئة أكثر قابلية للبرمجة.

يحمل كتاب Edinburgh LCF الصادر عام 1979 أسماء Michael J. C. Gordon وRobin Milner وChristopher P. Wadsworth. وتضم ورقة اللغة الوصفية لعام 1978 أيضاً Lockwood Morris وMalcolm Newey. تربط مراجعات Larry Paulson وMichael Gordon بين Stanford LCF وEdinburgh LCF ثم Cambridge LCF وHOL وIsabelle. مركزية فكرة Robin Milner لا تجعل ML أو التكتيكات أو البرهان التفاعلي عملاً فردياً.

نشأت ML بوصفها Meta Language لكتابة إجراءات البرهان. ثم أصبحت منظومة الأنواع متعددة الأشكال إنجازاً مستقلاً؛ عرض بحث Robin Milner عام 1978 نتائج للسلامة الدلالية والتركيبية وشرح خوارزمية استدلال مستخدمة بالفعل في Edinburgh LCF. وقد كرمت A. M. Turing Award لعام 1991 أعماله في LCF وML وCCS، من دون أن تلغي الإسهام الجماعي.

تعمل قواعد الاستدلال إلى الأمام من نظريات موجودة إلى نظرية جديدة. وتعمل التكتيكات إلى الخلف من الهدف إلى أهداف فرعية. تصل validation الاتجاهين. أما tacticals فتنظم التسلسل والتكرار والاختيار بين التكتيكات؛ توسع التحكم في البحث ولا تضيف بديهيات جديدة.

ما الذي يشتريه النوع المجرّد؟

يخفي النوع المجرّد تمثيله الداخلي ولا يكشف سوى عمليات مختارة. تستطيع الشيفرة العادية حمل قيمة thm وتمريرها إلى القواعد، لكنها لا تعدّل بنيتها السرية لتزوّر قيمة أخرى. تحرس منظومة الأنواع هذا الحد.

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

غير أن «النواة الصغيرة» لا تعني غياب الثقة. يجب أن تكون القواعد البدائية سليمة بالنسبة إلى المنطق المختار. ويجب أن تحافظ بنية ML والمترجم وبيئة التشغيل على التجريد. قد تكسره وظائف غير آمنة أو أخطاء العتاد. كما يمكن للمحلل أو العارض أن يبيّن للمستخدم عبارة غير التي خُزنت فعلاً. تضيق قاعدة الثقة ولا تختفي.

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

validation التزام مؤجل

عندما تقترح الأداة التكتيكية أهدافاً فرعية فهي تعد بأن نظرياتها تكفي للهدف الأصلي. وعلى validation أن تفي بهذا الوعد لاحقاً بواسطة القواعد المقبولة. إزالة الهدف من الشاشة ليست برهاناً.

وعندما تركب tacticals عمليات بحث متعددة، فإنها تركب دوال validation أيضاً. قد تصبح طبقة التحكم كبيرة، لكن سلسلة القبول تظل عائدة إلى العمليات البدائية. يشرح السجل والبرنامج والإشارة الخضراء النشاط؛ ولا يملكون سلطة القيمة المقبولة.

ورث HOL وIsabelle جوانب من الفكرة، لكنهما ليسا نسخاً متطابقة. يوضح Paulson أن Isabelle يمثل القواعد وحالات البرهان على أسس تختلف عن LCF الكلاسيكي. أنظمة أخرى تحتفظ بمصطلحات البرهان أو تصدر شهادات لفحص مستقل. كما ترسم أنظمة نظرية الأنواع مثل Coq حدوداً مختلفة. وجود التكتيكات وحده لا يكفي لوصف نظام بأنه LCF.

المصادر وحدود الاستنتاج

هذا بحث تاريخي ومعماري، لا تدقيق أمني لمبرهن حديث ولا قياس لحجم نواته. الربط بين قاعدة مشتركة دنيا قابلة للتحقق محلياً وحرية الأساليب المستقبلية قراءة تحريرية مستلهمة من مبدأ المواصفة الأولية الدنيا لدى Lu Heng، وليس موقفاً مؤسسياً منسوباً إلى Robin Milner.