الرابط العميق مساواة البراهين الرياضية وبرامج الكمبيوتر | مجلة كوانتا

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

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

ببساطة، تفترض مراسلات كاري-هاوارد أن مفهومين من علوم الكمبيوتر (الأنواع والبرامج) متساويان، على التوالي، للافتراضات والبراهين – مفاهيم من المنطق.

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

تم تسمية المراسلات على اسم الباحثين اللذين اكتشفاها بشكل مستقل. في عام 1934، لاحظ عالم الرياضيات والمنطق هاسكل كاري تشابهًا بين الوظائف في الرياضيات وعلاقة التضمين في المنطق، والتي تأخذ شكل عبارات "إذا-ثم" بين افتراضين.

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

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

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

ولتجنب هذه المفارقة، أوضح راسل أنه يمكننا استخدام "الأنواع". بشكل تقريبي، هذه هي الفئات التي تسمى قيمها المحددة بالكائنات. على سبيل المثال، إذا كان هناك نوع يسمى "Nat"، أي الأعداد الطبيعية، فإن كائناته هي 1، 2، 3، وهكذا. يستخدم الباحثون عادة النقطتين للإشارة إلى نوع الكائن. يمكن كتابة الرقم 7، من النوع الصحيح، بالشكل "7: عدد صحيح". يمكن أن يكون لديك دالة تأخذ كائنًا من النوع A وتنتج كائنًا من النوع B، أو دالة تجمع بين زوج من الكائنات التي كانت من النوع A والنوع B في نوع جديد يسمى "A × B".

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

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

أظهر كاري وهوارد أن الأنواع تعادل بشكل أساسي الافتراضات المنطقية. عندما "تسكن" دالة نوعًا ما - أي عندما تتمكن من تحديد دالة تمثل كائنًا من هذا النوع بنجاح - فإنك تُظهر بشكل فعال أن الاقتراح المقابل صحيح. لذا فإن الوظائف التي تأخذ مدخلات من النوع A وتعطي مخرجات من النوع B، المشار إليه بالنوع A → B، يجب أن تتوافق مع المعنى الضمني: "إذا كان A، إذن B". على سبيل المثال، خذ الاقتراح "إذا هطل المطر، فالأرض رطبة". في نظرية النوع، سيتم صياغة هذا الاقتراح من خلال دالة من النوع "Raining → GroundIsWet". إن الصيغ ذات المظهر المختلف هي في الواقع نفسها من الناحية الرياضية.

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

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

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

وقال: "ما حدث في القرن منذ رؤية كاري هو أننا نستمر في اكتشاف المزيد والمزيد من الحالات التي يتوافق فيها النظام المنطقي X مع النظام الحسابي Y". مايكل كلاركسون، عالم الكمبيوتر في جامعة كورنيل. لقد ربط الباحثون بالفعل البرمجة بأنواع أخرى من المنطق مثل المنطق الخطي، والذي يتضمن مفهوم “الموارد”، والمنطق النموذجي، الذي يتعامل مع مفاهيم الإمكانية والضرورة.

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