سؤال حول المنطق ومراسلات الكاري هوارد

Question

هل يمكن أن تشرح لي ما هي العلاقة الأساسية بين أساسيات البرمجة المنطقية وظاهرة التشابه النحوي بين أنظمة النوع والمنطق التقليدي؟

Answer 1

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

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

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

بعض النقاط الأخرى:

1. من الممكن بناء البرمجة المنطقية على منطق أكثر تطوراً من شروط القرن ؛ على سبيل المثال ، يعتمد Lambda-Prolog على المنطق الحدسي ، مع آلية حساب مختلفة عن الدقة.
2. وصف ديل ميلر النموذج النظري للمثليف وراء البرمجة المنطقية البحث عن البرمجة كبرمجة الاستعارة ، على النقيض من البراهين كبرامج الاستعارة التي هي مصطلح آخر يستخدم لمراسلات الكاري هارد.

Answer 2

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

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

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