لغة البرمجة الوظيفية للمنطق الجبري

تجمع لغة البرمجة الجبرية المنطقية الوظيفية ( ALF ) بين تقنيات البرمجة الوظيفية والمنطقية . وتعتمد أساساً على منطق بنود هورن مع المساواة، والذي يتكون من المسندات وبنود هورن للبرمجة المنطقية، والدوال والمعادلات للبرمجة الوظيفية.

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

صُمم نظام ALF ليكون تطبيقًا فعالًا لدمج عمليات التحليل والتضييق وإعادة الكتابة والرفض. تُترجم برامج ALF إلى تعليمات لآلة مجردة ، تستند إلى آلة وارن المجردة (WAM) مع عدة إضافات لتنفيذ التضييق وإعادة الكتابة. في تطبيق ALF الحالي ، تُنفذ برامج هذه الآلة المجردة بواسطة محاكي مكتوب بلغة C.

في مستودع الذكاء الاصطناعي بجامعة كارنيجي ميلون ، ^{[ 1 ]} تُدرج لغة ALF كلغة برمجة للذكاء الاصطناعي، وتحديدًا كلغة برمجة وظيفية/منطقية تُطبّق لغة برولوج. ^{[ 2 ]} يتوفر دليل مستخدم ^{[ 3 ]} يشرح اللغة وكيفية استخدام النظام. يعمل نظام ALF ^{[ 4 ]} على نظام يونكس ، وهو متاح بموجب ترخيص برمجيات خاص يمنح الحق في استخدامه لأغراض "التقييم والبحث والتدريس"، ولكنه لا يسمح باستخدامه لأغراض تجارية أو عسكرية. ^{[ 5 ]}

• منشورات مايكل هانوس ، بما في ذلك العديد من المقالات ذات الصلة بتصميم ونظرية ALF
• معلومات حول الحصول على نظام ALF وتثبيته