البرمجة الوظيفية الكاملة

البرمجة الوظيفية الكاملة (المعروفة أيضًا باسم البرمجة الوظيفية القوية ، ^{[ 1 ]} على عكس البرمجة الوظيفية العادية أو الضعيفة ) هي نموذج برمجي يقيد نطاق البرامج بتلك التي يمكن إثبات انتهائها . ^{[ 2 ]}

يُضمن إنهاء العقد بالقيود التالية:

1. شكل محدود من الاستدعاء الذاتي ، والذي يعمل فقط على أشكال "مختزلة" من وسائطه، مثل استدعاء والتر الذاتي ، أو الاستدعاء الذاتي البنيوي الفرعي ، أو "التطبيع القوي" كما هو مثبت من خلال التفسير المجرد للشيفرة. ^{[ 3 ]}
2. يجب أن تكون كل دالة دالة كلية (وليست جزئية ). أي يجب أن يكون لها تعريف لكل شيء داخل نطاقها.
   • توجد عدة طرق ممكنة لتوسيع نطاق الدوال الجزئية شائعة الاستخدام، مثل القسمة، لتصبح دوالًا كلية: اختيار نتيجة عشوائية للمدخلات التي تكون الدالة غير معرفة عليها عادةً (مثل${\displaystyle \forall x\in \mathbb {N} .x\div 0=0}$^{[ 2 ]} (للقسمة)؛ إضافة وسيطة أخرى لتحديد النتيجة لتلك المدخلات؛ أو استبعادها باستخدام ميزات نظام النوع مثل أنواع التحسين .

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

على سبيل المثال، ليس من السهل إثبات أن خوارزمية الفرز السريع تعتمد على التكرار البنيوي الفرعي، ولكنها لا تتكرر إلا إلى عمق أقصى يساوي طول المتجه (تعقيد زمني في أسوأ الحالات ^O ( n² ) ). ويمكن تطبيق خوارزمية الفرز السريع على القوائم (والتي سيرفضها مدقق التكرار البنيوي الفرعي) باستخدام لغة هاسكل .

استيراد Data.List ( القسم )qsort [] = [] qsort [ a ] = [ a ] qsort ( a : as ) = ​​let ( lesser , greater ) = partition ( < a ) as in qsort lesser ++ [ a ] ++ qsort greater

لجعلها تكرارية فرعية باستخدام طول المتجه كحد، يمكننا القيام بما يلي:

استيراد Data.List ( القسم )qsort x = qsortSub x x -- الحالة الدنيا qsortSub [] as = as -- يُظهر الإنهاء -- حالات qsort القياسية qsortSub ( l : ls ) [] = [] -- غير تكرارية، لذا مقبولة qsortSub ( l : ls ) [ a ] ​​= [ a ] ​​-- غير تكرارية، لذا مقبولة qsortSub ( l : ls ) ( a : as ) = let ( lesser , greater ) = partition ( < a ) as -- تكرارية، ولكنها تتكرر على ls، وهي بنية فرعية من -- مدخلها الأول. in qsortSub ls lesser ++ [ a ] ​​++ qsortSub ls greater

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

من النتائج الأخرى للبرمجة الوظيفية الكاملة أن كلاً من التقييم الصارم والتقييم الكسول يؤديان إلى نفس السلوك من حيث المبدأ؛ ومع ذلك، قد يكون أحدهما مفضلاً (أو حتى مطلوباً) لأسباب تتعلق بالأداء. ^{[ 4 ]}

في البرمجة الوظيفية الشاملة، يُفرَّق بين البيانات والبيانات المساعدة ؛ فالأولى محدودة ، بينما الثانية غير محدودة. تُستخدم هياكل البيانات غير المحدودة هذه في تطبيقات مثل الإدخال والإخراج . ويتطلب استخدام البيانات المساعدة عمليات مثل الاستدعاء الذاتي المشترك . مع ذلك، من الممكن إجراء عمليات الإدخال والإخراج في لغة برمجة وظيفية شاملة (مع أنواع تابعة ) حتى بدون استخدام البيانات المساعدة. ^{[ 5 ]}

يمكن اعتبار كل من Epigram و Charity لغتي برمجة وظيفية كاملة، على الرغم من أنهما لا تعملان بالطريقة التي حددها تيرنر في بحثه. وينطبق الأمر نفسه على البرمجة المباشرة في نظام F البسيط ، أو في نظرية مارتن-لوف للأنواع ، أو في حساب الإنشاءات .

• تحليل الإنهاء