الجانب المنطقي لحساب لامدا (دراسة تحليلية)

يناقش هذا البحث حساب لامدا الذي قدمه المنطقي "ألونزو تشيرش Alonzo Church*"(1903-1995)[1]"، واعتبر من أساسيات لغات برمجة الحاسوب، إلا أنني أتناول فيه الجانب النسقي الصوري له کجزءٍ من المنطق الرياضي، فتناولت بالتعريف حساب لامدا، الذي يشار إليه بالمصطلح الرمزي λ، مبيناً أنه يتعلق بالأسس الشائعة لبرمجة الدالة، مبيناً أنه عبارة عن لغةٍ صوريةٍ ذات قواعد اختزال محددة، تؤدي إلى نتائجٍ في المنطق الصوري، ونظرية الدالات العودية" التکرارية"، ولغة البرمجة، مبيناً أن حساب لامدا يعرف قوانين صياغة الحساب، وتحويل التعبيرات داخل النسق.
     يتعامل حساب لامدا مع نظرية النمط الحر، التي تطبق على تطابق الدالة الذي قدمه "کيوري" تحت عنوان منطق التحليل، وقدمه "تشيرش" بعد ذلک، في محاولةٍ منه لتقديم المنطق في صورة دالات بدلاً من نظرية الفئات. تطابق نموذج حساب لامدا "لکيوري وتشيرش" مع نموذج "ميلنر"، الذي يسمى بالنمط الضمني، ومن ثم يعتبر حساب لامدا غامضاً من أول وهلة، لکن يعتبر آداةً للتسمية، ويعامل حساب لامدا کنسقٍ جبري صوري للتفکير حول الحساب، هذا الحساب يزودنا بنموذٍج کليٍ للحساب، قدمه "تشيرش"، و أوضحه فيما بعد "آلان تورنج"، کما اعتبر نسقاً صورياً له بديهيات وقواعد استدلال، تساعد بنفسها في تحليل استخدام اللغة وأدوات المنطق الرياضي، وفيه يُلاحظ حساب لامدا باعتباره استنباطاً إرشادياً في هذا النسق الصوري.
      وحساب –λ حسابٌ اقتصادي في الدالات، لکنه يخفي المدى الذي ينبع من أصوله هذا الحساب في المنطق الرياضي، ويکتب التعبير في حساب–λ في شکل تصدير محدد، ولهذا لايوجد مجالٌ لإقحام أو إزالة الثوابت، علاوة على أن الدالة والبرهان يکتبان ببساطة بجوار بعضهما البعض دون أقواس حول البرهان، لذلک بينما يکتب عالم الرياضيات ومبرمج الحاسب الآلي جيب الدالة Sin جا (س)، نکتب جا (س) في حساب –λ بطريقةٍ أبسط من ذلک، إذا أخذت الدالة أکثر من برهان؛ فإنها حينئذٍ تصطف ببساطة بعد الدالة، ومن ثم "س + 3" تصبح "+ س 3"، وتصبح "س²"  "س س"، وتستخدم الأقواس فقط لفرض تنظيمٍ خاص على المجموعات.
     هناک أکثر من استخدام لحساب-λ صاغها کلٌ من "تشيرش" عام 1930، و"کلين*[2]Stephen Cole Kleene (1909-1994)" عام 1936 الذي أوضح في بحثٍ له کيفية تمثيل بعض الأعداد الترتيبية بحدود –λ.



*"ألونزو تشيرش "Alonzo Church: ولد في 14 يونيه عام 1903 بواشنطن، تخرج في جامعة برينستون عام 1924، حصل على درجة الدکتوراه عام 1927، في موضوع يفترض أن الأنساق التي تقوم على بديهية الاختيار ربما تکون کاذبة، قضى عامان في الزمالة البحثية الوطنية أولهما في هارفارد، والآخر في جوتينجن وأمستردام ، عاد بعدهما إلى برينستون ليکون سبباً في رفع مکانة الکلية في شعبة الرياضيات. ( انظر  Seldin. P . Jonathan : The Logic of Curry and Church)وترجع أهميته ليس فقط للحلول التي قدمها لبعض المشکلات التقنية الصعبة، بل أيضاً لمساهمته الفعالة في نشر المنطق الرياضي من خلال وظيفته کأستاذ في جامعة برينستون وبنشره "مجلة المنطق الرمزي" The Journal of Symbolic Logic التي تعتبر وثيقة هامة في هذا المجال،وهي مجلة ربع سنوية ويقوم على نشرها کل من تشيرش وناجل Nagel E . وهي تهتم بنشر الأبحاث الجديدة في المنطق الرياضي فضلاً عن نشر التعليقات النقدية على کل المؤلفات التي تظهر في مجال المنطق.
انظر:   ديمتريو: تاريخ المنطق" قراءات حول التطور المعاصر للمنطق" ج4، ترجمة د: إسماعيل عبد العزيز، دار الثقافة للنشر والتوزيع، القاهرة، 1997، ص114.


* کلينStephen Cole Kleene:ولد في 5يناير عام 1909، وتوفي في 25 يناير عام 1994، عمل أستاذ بجامعة ويسکونسن، ويدين له المنطق الرياضي بإسهامات هامة على صعيد الإبداع  الشخصي والأبحاث التفسيرية على حدٍ سواء، حيث أنه عمل منذ 1940 في برنامج للأبحاث في الرياضيات الحدسية والدوال الراجعة، والتي شرح بواسطتها بعض أفکار الحدسيين. کما أنشأ نسقاً صورياً جديداً للتحليل الحدسي، والذي يختلف عن النسق الذي قدمه هايتنج Heyting (1930)، ولکنه يتوافق مع نسق التحليل الکلاسيکي.مما أدى بالتالي إلى سهولة المقارنة بين النسق الحدسي والأنساق الکلاسيکية. کما استخدم کلين الدوال الراجعة لدراسة النسق الحدسي من وجهة نظر سيمانطيقية.
انظر: ديمتريو: مرجع سابق، ص120.
** فيبوناتشي Fibonacci: عالم رياضيات إيطالي شهير في العصور الوسطى اشتهر باسم ليوناردو أو ليوناردو بيزا (نسبة إلى مولده في مدينة بيزا الإيطالية) ولد عام 1175 ميلادية.