ما هي "البرمجة الوظيفية الشاملة"؟

Question

ويكيبيديا لديه هذا ليقول:

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

و

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

هناك أيضًا Lambda The Ultimate Post حول ورقة بحثية إجمالي البرمجة الوظيفية.

لم أجد ذلك حتى الأسبوع الماضي في القائمة البريدية.

هل هناك المزيد من الموارد أو المراجع أو أي أمثلة للتطبيقات التي تعرفها؟

Answer 1

إذا فهمت ذلك بشكل صحيح، فإن البرمجة الوظيفية الإجمالية تعني ما يلي:البرمجة مع الوظائف الشاملة.إذا كنت أتذكر دورات الرياضيات الخاصة بي بشكل صحيح، فإن الدالة الإجمالية هي دالة تم تعريفها في مجالها بالكامل، والدالة الجزئية هي التي بها "ثغرات" في تعريفها.

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

لا تسمح لك البرمجة الوظيفية الإجمالية بكتابة مثل هذه الوظيفة.تُرجع جميع الوظائف دائمًا نتيجة لجميع المدخلات الممكنة؛ويتأكد مدقق النوع من أن هذا هو الحال.

أعتقد أن هذا يبسط إلى حد كبير معالجة الأخطاء:لا يوجد أي.

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

Answer 2

رغم أن هذا سؤال قديم، إلا أنني أعتقد أن أياً من الإجابات حتى الآن لم تذكر الحقيقة تحفيز لإجمالي البرمجة الوظيفية، وهو ما يلي:

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

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

ومن الجدير بالملاحظة أيضًا أن معظم مساعدي الإثبات يعملون بناءً على هذا المبدأ، Coq، على سبيل المثال.

Answer 3

الصدقة هي لغة أخرى تضمن إنهاء الخدمة:
http://pll.cpsc.ucalgary.ca/charity1/www/home.html

هيوم هي لغة ذات 4 مستويات.المستوى الخارجي هو تورينج كامل والطبقة الداخلية تضمن الإنهاء:
http://www-fp.cs.st-andrews.ac.uk/hume/report/