λProlog هي لغة برمجة منطقية تتميز بالكتابة باللامبدا (Lambda Prolog)، وهي تقنية مشتقة من لغة الـ Prolog الشهيرة. تم ظهور λProlog لأول مرة في عام 1986، وهي معروفة بميزاتها القوية مثل النوع البوليمورفي (Polymorphic typing)، والبرمجة النمطية (Modular programming)، والبرمجة من الدرجة الأعلى (Higher-order programming). تعتمد تلك التمديدات على صيغ Harrop الأعلى وراثيًا، والتي تستخدم لتبرير أسس λProlog. وتتمثل تلك التمديدات في الكمون الأعلى للترميز (Higher-order quantification)، والترميزات المبسطة للألفا-لامبدا (Simply typed λ-terms)، وتوحيد الكمون الأعلى (Higher-order unification)، والتي تمنح λProlog الدعم الأساسي اللازم لالتقاط نهج ترميز الشجرة λ للصيغة البنية الأعلى، وهو نهج لتمثيل الصيغة البنائية يقوم برسم تعليقات على مستوى الكائنات لربط اللغات البرمجية. تسمح لغة λProlog للمبرمجين بالتعامل مع الأسماء المتغيرة المرتبطة بمستويات مختلفة بدلاً من التعامل مع الأسماء المتغيرة المحددة: بدلاً من ذلك، يتوفر مجموعة متنوعة من الأدوات الإعلامية للتعامل مع نطاقات الملزمة وتطبيقاتها. ومنذ عام 1986، حصلت λProlog على العديد من التنفيذات، وحتى عام 2013، ما زالت اللغة وتنفيذاتها قيد التطوير النشط. تم تصميم مبرهنة Abella لتوفير بيئة تفاعلية لإثبات النظريات حول النواة الإعلامية لـ λProlog.
0
