A simple formalization of alpha-equivalence

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

في حساب لامدا، تُعرَّف الدوال باستخدام أماكن محجوزة لمدخلاتها. على سبيل المثال، قد تُكتب دالة كالتالي: "خذ x وأرجع x زائد واحد". لكن الحرف "x" ليس سوى علامة (label). ستعمل الدالة بنفس الطريقة تماماً إذا أسمينا المكان المحجوز "y" أو "z". في عالم هذا النظام الرياضي، تُعتبر هاتان النسختان متطابقتين. تُسمى هذه الفكرة "التكافؤ ألفا" (alpha-equivalence). وهذا يعني أن الأسماء المحددة التي نعطيها للمتغيرات المحلية لا تهم، بل المهم هو بنية الدالة فقط. وبينما يبدو هذا بديهياً للقارئ البشري، إلا أنه من الصعب للغاية كتابته كقواعد صارمة ليتبعها الحاسوب. معظم الكتب الدراسية والأنظمة الرسمية تتعامل مع هذا الأمر إما بتجاهل المشكلة، أو بافتراض أن الأسماء ستكون دائماً مختلفة، أو باستخدام حيلة معقدة تجرد الأسماء تماماً وتستبدلها بأرقام. هذه الحلول البديلة غالباً ما تجعل الرياضيات أصعب في المتابعة للطلاب أو تتطلب طبقة ثقيلة من الترجمة التي تحجب المنطق الأصلي.

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

للقيام بذلك، بنى الباحثان طريقة جديدة للنظر في مصطلحات حساب لامدا. فبدلاً من مجرد مقارنة دالتين جنباً إلى جنب، قدما نظاماً يتتبع "السياق" (context) أو قائمة المتغيرات الموجودة حالياً في النطاق. تخيل الدالة كمجموعة من الصناديق المتداخلة. عندما تكون داخل صندوق، يمكنك الوصول إلى المتغيرات المعرفة في ذلك الصندوق وجميع الصناديق خارجه. أنشأ الباحثان مجموعة من القواعد تقول: إذا كان لديك دالتان، فهما متكافئتان إذا تطابقت بنيتاهما، وإذا كانت متغيراتهما تشير إلى نفس الموقع في قوائم متغيراتهما النشطة. على سبيل المثال، إذا كان المتغير هو الأحدث تعريفاً في كلتا الدالتين، فيُعتبران متماثلين، حتى لو كان أحدهما يسمى "x" والآخر "y". وإذا كان المتغير مُعرفاً في موقع أبعد في القائمة، فإن القواعد تتحقق مما إذا كان قد تم "حجبه" (shadowed) أو إخفاؤه بواسطة متغير جديد يحمل نفس الاسم. يسمح هذا النهج للنظام بالتمييز بين المتغير الذي هو بارامتر محلي وبين المتغير الذي هو ثابت عالمي، وذلك بمجرد النظر إلى موقعه في القائمة.

ثم أخذ الباحثان هذا التعريف واختبره بصرامة باستخدام أداة تسمى "رورك" (Rocq Prover)، وهي برمجية تتحقق من صحة البراهين الرياضية بشكل مطلق. لقد أثبتا أن تعريفهما الجديد يعمل تماماً كما ينبغي. فهو انعكاسي (reflexive)، بمعنى أن الدالة تكافئ نفسها؛ ومتماثل (symmetric)، بمعنى أنه إذا كانت الدالة A تكافئ B، فإن B تكافئ A؛ ومتعدٍ (transitive)، بمعنى أنه إذا كانت A تكافئ B وB تكافئ C، فإن A تكافئ C. كما أظهرا أن هذا التعريف يعمل بشكل مثالي مع العمليات الأخرى لحساب لامدا، مثل الاستبدال (substitution)، وهو عملية استبدال متغير بقيمة ما. في العديد من الأنظمة الأخرى، يكون الاستبدال حقل ألغام حيث يمكن للمتغيرات أن تُحتجز أو تختلط بالخطأ، لكن الباحثين أثبتا أن تعريفهما يتعامل مع هذه الحالات بوضوح وتوقع.

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

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

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

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