دلالات النموذج المستقر

📅 آخر تحديث: ٢٤ يوليو ٢٠٢٦
✍️ نُشر في: ٢٤ يوليو ٢٠٢٦
📷 يحتوي على 83 صور
الموسوعة الحرة

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

تحفيز

استُلهم البحث في الدلالات التصريحية للنفي في البرمجة المنطقية من حقيقة أن سلوك حل SLDNF - وهو تعميم لحل SLD الذي يستخدمه Prolog في وجود النفي في مجموعات القواعد - لا يتطابق تمامًا مع جداول الحقيقة المألوفة من منطق القضايا الكلاسيكي . لنأخذ على سبيل المثال البرنامج

ص{\displaystyle p}
ر←ص،q{\displaystyle r\leftarrow p,q}
s←ص،لا⁡q.{\displaystyle s\leftarrow p,\operatorname {not} q.}

بالنظر إلى هذا البرنامج، سينجح الاستعلام p ، لأن البرنامج يتضمن p كحقيقة؛ وسيفشل الاستعلام q ، لأنه لا يظهر في رأس أي من القواعد. وسيفشل الاستعلام r أيضًا، لأن القاعدة الوحيدة التي تحتوي على r في رأسها تتضمن الهدف الفرعي q في متنها؛ وكما رأينا، فإن هذا الهدف الفرعي يفشل. وأخيرًا، ينجح الاستعلام s ، لأن كل هدف فرعي من الأهداف الفرعية p ،لا⁡q{\displaystyle \operatorname {not} q}ينجح. (ينجح الأخير لأن الهدف الإيجابي المقابل q يفشل). باختصار، يمكن تمثيل سلوك حل SLDNF على البرنامج المعطى من خلال تعيين الحقيقة التالي:

صqرs
تيFFت .

من ناحية أخرى، يمكن اعتبار قواعد البرنامج المعطى بمثابة صيغ منطقية إذا اعتبرنا الفاصلة بمثابة حرف عطف.∧{\displaystyle \land }، الرمزلا{\displaystyle \operatorname {not} }مع النفي¬{\displaystyle \neg }، والموافقة على معاملةF←جي{\displaystyle F\leftarrow G}كدلالة ضمنيةجي→F{\displaystyle G\rightarrow F}مكتوبة بالمقلوب. على سبيل المثال، القاعدة الأخيرة من البرنامج المعطى، من وجهة النظر هذه، هي تدوين بديل للصيغة المنطقية.

ص∧¬q→s.{\displaystyle p\land \neg q\rightarrow s.}

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

صqرs
تيتيتيF.​

وبالتالي، فإن أحد نماذج البرنامج المذكور يتميز بكونه يمثل بدقة سلوك حل SLDNF. ما هي الخصائص الرياضية لهذا النموذج التي تجعله مميزًا؟ يُقدم تعريف النموذج المستقر إجابةً لهذا السؤال.

العلاقة بالمنطق غير الرتيب

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

يستخدم بناء الجملة في منطق المعرفة الذاتية عاملًا مشروطًا يسمح لنا بالتمييز بين ما هو صحيح وما هو معروف. اقترح مايكل جيلفوند [1987] أن يقرألا⁡ص{\displaystyle \operatorname {not} p}في صلب القاعدة كما يلي:ص{\displaystyle p}"غير معروف"، وفهم قاعدة مع النفي كصيغة مقابلة للمنطق المعرفي الذاتي. يمكن اعتبار دلالات النموذج المستقر، في شكلها الأساسي، إعادة صياغة لهذه الفكرة تتجنب الإشارات الصريحة إلى المنطق المعرفي الذاتي.

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

s←ص،لا⁡q{\displaystyle s\leftarrow p,\operatorname {not} q}

يمكن فهم ذلك على أنه الوضع الافتراضي الذي يسمح لنا بالاستنتاجs{\displaystyle s}منص{\displaystyle p}بافتراض أن¬q{\displaystyle \neg q}متسق. تستخدم دلالات النموذج المستقر نفس الفكرة، لكنها لا تشير صراحةً إلى المنطق الافتراضي.

نماذج مستقرة

يستخدم تعريف النموذج المستقر أدناه، والمقتبس من [Gelfond and Lifschitz, 1988]، اصطلاحين. أولًا، تُعرَّف قيمة الصواب بأنها مجموعة الذرات التي تأخذ القيمة T. على سبيل المثال، قيمة الصواب

صqرs
تيFFت .

يتم تحديدها مع المجموعة{ص،s}{\displaystyle \{p,s\}}يُتيح لنا هذا الاصطلاح استخدام علاقة احتواء المجموعة لمقارنة قيم الصواب فيما بينها. أصغر قيمة من بين جميع قيم الصواب هي∅{\displaystyle \emptyset }هو الذي يجعل كل ذرة خاطئة؛ أما أكبر قيمة لتعيين الحقيقة فتجعل كل ذرة صحيحة.

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

حتى⁡(0){\displaystyle \operatorname {even} (0)}
حتى⁡(s(X))←لا⁡حتى⁡(X){\displaystyle \operatorname {even} (s(X))\leftarrow \operatorname {not} \operatorname {even} (X)}

يُفهم ذلك على أنه نتيجة استبدال X في هذا البرنامج بالحدود الأساسية

0،s(0)،s(s(0))،....{\displaystyle 0,s(0),s(s(0)),\dots .}

بكل الطرق الممكنة. والنتيجة هي برنامج الأرض اللانهائي

حتى⁡(0){\displaystyle \operatorname {even} (0)}
حتى⁡(s(0))←لا⁡حتى⁡(0){\displaystyle \operatorname {even} (s(0))\leftarrow \operatorname {not} \operatorname {even} (0)}
حتى⁡(s(s(0)))←لا⁡حتى⁡(s(0)){\displaystyle \operatorname {even} (s(s(0)))\leftarrow \operatorname {not} \operatorname {even} (s(0))}
...{\displaystyle \dots }

تعريف

ليكن P مجموعة من القواعد على الشكل التالي:

أ←ب1،...،بم،لا⁡ج1،...،لا⁡جن{\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}

أينأ،ب1،...،بم،ج1،...،جن{\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}هي ذرات أرضية. إذا لم تحتوي P على نفي (ن=0{\displaystyle n=0}في كل قاعدة من قواعد البرنامج)، فإن النموذج المستقر الوحيد لـ P ، بحسب التعريف، هو النموذج الأدنى بالنسبة لاحتواء المجموعة. [ 1 ] (أي برنامج بدون نفي له نموذج أدنى واحد فقط). لتوسيع هذا التعريف ليشمل حالة البرامج التي تحتوي على نفي، نحتاج إلى المفهوم المساعد للاختزال، المعرّف كما يلي.

بالنسبة لأي مجموعة I من الذرات الأساسية، فإن اختزال P بالنسبة إلى I هو مجموعة القواعد بدون نفي التي تم الحصول عليها من P عن طريق حذف كل قاعدة بحيث تكون إحدى الذرات على الأقلجأنا{\displaystyle C_{i}}في جسدها

ب1،...،بم،لا⁡ج1،...،لا⁡جن{\displaystyle B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}

ينتمي إلى أنا ، ثم إسقاط الأجزاءلا⁡ج1،...،لا⁡جن{\displaystyle \operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}من نصوص جميع القواعد المتبقية.

نقول إن I نموذج مستقر لـ P إذا كان I هو النموذج المستقر للاختزال الخاص بـ P بالنسبة إلى I. (بما أن الاختزال لا يحتوي على النفي، فقد تم تعريف نموذجه المستقر مسبقًا). وكما يوحي مصطلح "النموذج المستقر"، فإن كل نموذج مستقر لـ P هو نموذج لـ P.

مثال

ولتوضيح هذه التعريفات، دعونا نتحقق من ذلك.{ص،s}{\displaystyle \{p,s\}}هو نموذج مستقر للبرنامج

ص{\displaystyle p}
ر←ص،q{\displaystyle r\leftarrow p,q}
s←ص،لا⁡q.{\displaystyle s\leftarrow p,\operatorname {not} q.}

تقليص هذا البرنامج بالنسبة إلى{ص،s}{\displaystyle \{p,s\}}يكون

ص{\displaystyle p}
ر←ص،q{\displaystyle r\leftarrow p,q}
s←ص.{\displaystyle s\leftarrow p.}

(في الواقع، منذq∉{ص،s}{\displaystyle q\not \in \{p,s\}}يتم الحصول على الاختزال من البرنامج عن طريق حذف الجزءلا⁡q.{\displaystyle \operatorname {not} q.}النموذج المستقر للاختزال هو{ص،s}{\displaystyle \{p,s\}}(في الواقع، تُحقق هذه المجموعة من الذرات جميع قواعد الاختزال، وليس لها مجموعات جزئية فعلية لها نفس الخاصية). وهكذا، بعد حساب النموذج المستقر للاختزال، توصلنا إلى نفس المجموعة.{ص،s}{\displaystyle \{p,s\}}التي بدأنا بها. وبالتالي، فإن هذه المجموعة هي نموذج مستقر.

وبنفس الطريقة يتم فحص المجموعات الـ 15 الأخرى المكونة من الذراتص،q،ر،s{\displaystyle p,q,r,s}يُظهر ذلك أن هذا البرنامج لا يملك نماذج مستقرة أخرى. على سبيل المثال، اختزال البرنامج بالنسبة إلى{ص،q،ر}{\displaystyle \{p,q,r\}}يكون

ص{\displaystyle p}
ر←ص،q.{\displaystyle r\leftarrow p,q.}

النموذج المستقر للاختزال هو{ص}{\displaystyle \{p\}}وهو يختلف عن المجموعة{ص،q،ر}{\displaystyle \{p,q,r\}}التي بدأنا بها.

البرامج التي لا تمتلك نموذجًا ثابتًا فريدًا

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

ص←لا⁡q{\displaystyle p\leftarrow \operatorname {not} q}
q←لا⁡ص{\displaystyle q\leftarrow \operatorname {not} p}

يحتوي على نموذجين مستقرين{ص}{\displaystyle \{p\}}،{q}{\displaystyle \{q\}}برنامج القاعدة الواحدة

ص←لا⁡ص{\displaystyle p\leftarrow \operatorname {not} p}

لا توجد نماذج مستقرة.

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

لكن استخدام النماذج المستقرة في برمجة مجموعات الإجابات يُقدّم منظورًا مختلفًا لهذه البرامج. في هذا النموذج البرمجي ، تُمثَّل مسألة البحث ببرنامج منطقي، بحيث تُقابل النماذج المستقرة للبرنامج الحلول. بالتالي، تُقابل البرامج التي تحتوي على العديد من النماذج المستقرة مسائل ذات حلول متعددة، بينما تُقابل البرامج التي لا تحتوي على نماذج مستقرة مسائل غير قابلة للحل. على سبيل المثال، لغز الملكات الثماني له 92 حلاً؛ لحله باستخدام برمجة مجموعات الإجابات، نُشفّره ببرنامج منطقي يحتوي على 92 نموذجًا مستقرًا. من هذا المنظور، تُعدّ البرامج المنطقية التي تحتوي على نموذج مستقر واحد فقط مميزة في برمجة مجموعات الإجابات، تمامًا مثل كثيرات الحدود التي لها جذر واحد فقط في الجبر.

خصائص دلالات النموذج المستقر

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

أ←ب1،...،بم،لا⁡ج1،...،لا⁡جن{\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}

أينأ،ب1،...،بم،ج1،...،جن{\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}هي ذرات أرضية.

ذرات الرأس
إذا كانت الذرة A تنتمي إلى نموذج مستقر لبرنامج منطقي P فإن A هي رأس إحدى قواعد P.
الحد الأدنى
أي نموذج مستقر لبرنامج منطقي P يكون أصغر نموذج من بين نماذج P بالنسبة إلى احتواء المجموعة.
خاصية السلسلة المضادة
إذا كان I و J نموذجين مستقرين لنفس البرنامج المنطقي، فإن I ليس مجموعة جزئية فعلية من J. بعبارة أخرى، مجموعة النماذج المستقرة لبرنامج ما هي سلسلة مضادة .
اكتمال NP
اختبار ما إذا كان لبرنامج منطق أرضي محدود نموذج مستقر هو مسألة NP-كاملة .

العلاقة بنظريات أخرى للنفي باعتباره فشلاً

إتمام البرنامج

إن أي نموذج مستقر لبرنامج أرضي محدود ليس مجرد نموذج للبرنامج نفسه، بل هو أيضًا نموذج لإتمامه [ ماريك وسوبرامانيان، 1989]. إلا أن العكس ليس صحيحًا. على سبيل المثال، إتمام برنامج القاعدة الواحدة

ص←ص{\displaystyle p\leftarrow p}

هل هذا تكرار؟ص↔ص{\displaystyle p\leftrightarrow p}النموذج∅{\displaystyle \emptyset }يُعد هذا التكرار نموذجًا مستقرًا لـص←ص{\displaystyle p\leftarrow p}لكن نموذجها الآخر{ص}{\displaystyle \{p\}}ليس كذلك. فقد وجد فرانسوا فاج [1994] شرطًا نحويًا على البرامج المنطقية يقضي على هذه الأمثلة المضادة ويضمن استقرار كل نموذج لإتمام البرنامج. تُسمى البرامج التي تُحقق شرطه بالبرامج المحكمة .

أوضح فانغزين لين ويوتينغ تشاو [2004] كيفية تحسين عملية إكمال برنامج غير محكم بحيث يتم التخلص من جميع نماذجه غير المستقرة. وتُسمى الصيغ الإضافية التي أضافوها إلى عملية الإكمال بصيغ الحلقات .

دلالات راسخة

يقسم النموذج المتين لبرنامج منطقي جميع الذرات الأساسية إلى ثلاث مجموعات: صحيحة، خاطئة، وغير معروفة. إذا كانت الذرة صحيحة في النموذج المتين لـP{\displaystyle P}إذن فهو ينتمي إلى كل نموذج مستقر منP{\displaystyle P}أما العكس، فلا ينطبق عموماً. على سبيل المثال، البرنامج

ص←لا⁡q{\displaystyle p\leftarrow \operatorname {not} q}
q←لا⁡ص{\displaystyle q\leftarrow \operatorname {not} p}
ر←ص{\displaystyle r\leftarrow p}
ر←q{\displaystyle r\leftarrow q}

يحتوي على نموذجين مستقرين،{ص،ر}{\displaystyle \{p,r\}}و{q،ر}{\displaystyle \{q,r\}}. بالرغم منر{\displaystyle r}ينتمي إلى كليهما، وقيمته في النموذج الراسخ غير معروفة .

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

نفي قوي

تمثيل معلومات غير كاملة

من منظور تمثيل المعرفة ، يمكن اعتبار مجموعة من الذرات الأساسية وصفًا لحالة معرفية كاملة: فالذرات التي تنتمي إلى المجموعة معروفة بصحتها، والذرات التي لا تنتمي إليها معروفة بخطئها. ويمكن وصف حالة معرفية قد تكون غير كاملة باستخدام مجموعة متسقة ولكنها قد تكون غير كاملة من المتغيرات؛ فإذا كانت ذرةص{\displaystyle p}إذا لم ينتمي إلى المجموعة، ونفيه لا ينتمي إلى المجموعة أيضًا، فإنه من غير المعروف ما إذا كانص{\displaystyle p}صحيح أم خطأ؟

في سياق البرمجة المنطقية، تؤدي هذه الفكرة إلى ضرورة التمييز بين نوعين من النفي: النفي كفشل ، الذي نوقش أعلاه، والنفي القوي ، الذي يُشار إليه هنا بـ∼{\displaystyle \sim }[ ٢ ] المثال التالي، الذي يوضح الفرق بين نوعي النفي، من تأليف جون مكارثي . يجوز لحافلة مدرسية عبور خط السكة الحديد بشرط عدم وجود قطار قادم. إذا لم نكن متأكدين بالضرورة من اقتراب قطار، فإن القاعدة التي تستخدم النفي كدليل على الفشل لا تنطبق .

يعبر←لا تتدرب{\displaystyle {\hbox{Cross}}\leftarrow {\hbox{not Train}}}

لا يُمثّل هذا المثال الفكرة تمثيلاً كافياً: فهو يُجيز العبور في حال عدم وجود معلومات عن قطار قادم. القاعدة الأضعف، التي تستخدم نفياً قوياً في متن الجملة، هي الأفضل.

يعبر←∼يدرب.{\displaystyle {\hbox{Cross}}\leftarrow \,\sim {\hbox{Train}}.}

يقول النص إنه لا بأس بالعبور إذا كنا نعلم أنه لا يوجد قطار قادم.

نماذج مستقرة متماسكة

لإدراج النفي القوي في نظرية النماذج المستقرة، سمح جيلفوند وليفشيتز [1991] بكل تعبير من التعبيراتأ{\displaystyle A}،بأنا{\displaystyle B_{i}}،جأنا{\displaystyle C_{i}}في قاعدة

أ←ب1،...،بم،لا⁡ج1،...،لا⁡جن{\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}

أن تكون إما ذرة أو ذرة مسبوقة برمز النفي القوي. وبدلاً من النماذج المستقرة، يستخدم هذا التعميم مجموعات الإجابات ، والتي قد تشمل كلاً من الذرات والذرات المسبوقة برمز النفي القوي.

يُعالج نهج بديل [Ferraris and Lifschitz, 2005] النفي القوي كجزء من الذرة، ولا يتطلب أي تغييرات في تعريف النموذج المستقر. في هذه النظرية للنفي القوي، نميز بين نوعين من الذرات، موجبة وسالبة ، ونفترض أن كل ذرة سالبة هي تعبير من الشكل التالي :∼أ{\displaystyle {\sim }A}، أينأ{\displaystyle A}هي ذرة موجبة. تُسمى مجموعة الذرات متماسكة إذا لم تحتوي على أزواج من الذرات "المتكاملة".أ،∼أ{\displaystyle A,{\sim }A}. النماذج المتماسكة والمستقرة للبرنامج هي نفسها مجموعات الإجابات المتسقة الخاصة به بمعنى [Gelfond and Lifschitz, 1991].

على سبيل المثال، البرنامج

ص←لا⁡q{\displaystyle p\leftarrow \operatorname {not} q}
q←لا⁡ص{\displaystyle q\leftarrow \operatorname {not} p}
ر{\displaystyle r}
∼ر←لا⁡ص{\displaystyle {\sim }r\leftarrow \operatorname {not} p}

يحتوي على نموذجين مستقرين،{ص،ر}{\displaystyle \{p,r\}}و{q،ر،∼ر}{\displaystyle \{q,r,{\sim }r\}}النموذج الأول متماسك؛ أما الثاني فليس كذلك، لأنه يحتوي على كل من الذرةر{\displaystyle r}والذرة∼ر{\displaystyle {\sim }r}.

افتراض العالم المغلق

وفقًا لـ [جيلفوند وليفشيتز، 1991]، فإن افتراض العالم المغلق للمسندص{\displaystyle p}يمكن التعبير عنها بالقاعدة

∼ص(X1،...،Xن)←لا⁡ص(X1،...،Xن){\displaystyle \sim p(X_{1},\dots ,X_{n})\leftarrow \operatorname {not} p(X_{1},\dots ,X_{n})}

(العلاقة)ص{\displaystyle p}لا ينطبق هذا على المجموعة المرتبةX1،...،Xن{\displaystyle X_{1},\dots ,X_{n}}(إذا لم يكن هناك دليل على ذلك). على سبيل المثال، النموذج المستقر للبرنامج

ص(أ،ب){\displaystyle p(a,b)}
ص(ج،د){\displaystyle p(c,d)}
∼ص(X،Y)←لا⁡ص(X،Y){\displaystyle \sim p(X,Y)\leftarrow \operatorname {not} p(X,Y)}

يتكون من ذرتين موجبتين

ص(أ،ب)،ص(ج،د){\displaystyle p(a,b),p(c,d)}

و14 ذرة سالبة

∼ص(أ،أ)،∼ص(أ،ج)،...{\displaystyle \sim p(a,a),{\sim }p(a,c),\dots }

أي، النفي القوي لجميع الذرات الأرضية الموجبة الأخرى المتكونة منص،أ،ب،ج،د{\displaystyle p,a,b,c,d}.

يمكن لبرنامج منطقي ذي نفي قوي أن يتضمن قواعد افتراض العالم المغلق لبعض مسنداته ويترك المسندات الأخرى في نطاق افتراض العالم المفتوح .

برامج ذات قيود

تم تعميم دلالات النموذج المستقر لتشمل أنواعًا عديدة من البرامج المنطقية بخلاف مجموعات القواعد "التقليدية" التي نوقشت أعلاه - قواعد من الشكل

أ←ب1،...،بم،لا⁡ج1،...،لا⁡جن{\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}

أينأ،ب1،...،بم،ج1،...،جن{\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}هي ذرات. يسمح أحد التوسعات البسيطة للبرامج باحتواء قيود - قواعد ذات رأس فارغ:

←ب1،...،بم،لا⁡ج1،...،لا⁡جن.{\displaystyle \leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}.}

تذكر أن القاعدة التقليدية يمكن اعتبارها تدوينًا بديلًا لصيغة منطقية إذا اعتبرنا الفاصلة بمثابة حرف عطف.∧{\displaystyle \land }، الرمزلا{\displaystyle \operatorname {not} }مع النفي¬{\displaystyle \neg }، والموافقة على معاملةF←جي{\displaystyle F\leftarrow G}كدلالة ضمنيةجي→F{\displaystyle G\rightarrow F}مكتوبة بالعكس. ولتوسيع هذا الاصطلاح ليشمل القيود، نحدد القيد بنفي الصيغة المقابلة لجسمه:

¬(ب1∧⋯∧بم∧¬ج1∧⋯∧¬جن).{\displaystyle \neg (B_{1}\land \cdots \land B_{m}\land \neg C_{1}\land \cdots \land \neg C_{n}).}

يمكننا الآن توسيع تعريف النموذج المستقر ليشمل البرامج ذات القيود. وكما هو الحال في البرامج التقليدية، نبدأ لتعريف النماذج المستقرة بالبرامج التي لا تحتوي على نفي. قد يكون هذا البرنامج غير متسق؛ وعندها نقول إنه لا يملك نماذج مستقرة. إذا كان هذا البرنامجP{\displaystyle P}إذا كان متسقًاP{\displaystyle P}يمتلك نموذجًا أدنى فريدًا، ويُعتبر هذا النموذج النموذج المستقر الوحيد لـP{\displaystyle P}.

بعد ذلك، يتم تعريف النماذج المستقرة للبرامج العشوائية ذات القيود باستخدام الاختزالات، التي يتم تشكيلها بنفس الطريقة كما في حالة البرامج التقليدية (انظر تعريف النموذج المستقر أعلاه). مجموعةأنا{\displaystyle I}يُعد نموذج الذرات نموذجًا مستقرًا للبرنامجP{\displaystyle P}مع مراعاة القيود إذا كان التخفيضP{\displaystyle P}بالنسبة إلىأنا{\displaystyle I}يمتلك نموذجًا مستقرًا، وهذا النموذج المستقر يساويأنا{\displaystyle I}.

تنطبق خصائص دلالات النموذج المستقر المذكورة أعلاه للبرامج التقليدية في وجود القيود أيضًا.

تلعب القيود دورًا مهمًا في برمجة مجموعات الإجابات، لأن إضافة قيد إلى برنامج منطقيP{\displaystyle P}يؤثر على مجموعة النماذج المستقرة لـP{\displaystyle P}ببساطة شديدة: فهي تزيل النماذج المستقرة التي تنتهك القيد. بعبارة أخرى، لأي برنامجP{\displaystyle P}مع مراعاة القيود وأي قيود أخرىج{\displaystyle C}النماذج المستقرة لـP∪{ج}{\displaystyle P\cup \{C\}}يمكن وصفها بأنها نماذج مستقرة لـP{\displaystyle P}ذلك يرضيج{\displaystyle C}.

البرامج المنفصلة

في قاعدة الفصل ، قد يكون الرأس عبارة عن فصل لعدة ذرات:

أ1؛...؛أك←ب1،...،بم،لا⁡ج1،...،لا⁡جن{\displaystyle A_{1};\dots ;A_{k}\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}

(تُعتبر الفاصلة المنقوطة بمثابة تدوين بديل للفصل)∨{\displaystyle \lor }). تتوافق القواعد التقليدية معك=1{\displaystyle k=1}والقيود المفروضة علىك=0{\displaystyle k=0}لتوسيع دلالات النموذج المستقر لتشمل البرامج الانفصالية [Gelfond and Lifschitz, 1991]، نُعرّف أولاً أنه في غياب النفي (ن=0{\displaystyle n=0}في كل قاعدة، تكون النماذج المستقرة للبرنامج هي نماذجه الدنيا. ويبقى تعريف الاختزال للبرامج الانفصالية كما هو من قبل . مجموعةأنا{\displaystyle I}يُعد نموذج الذرات نموذجًا مستقرًا لـP{\displaystyle P}لوأنا{\displaystyle I}هو نموذج مستقر لاختزالP{\displaystyle P}بالنسبة إلىأنا{\displaystyle I}.

على سبيل المثال، المجموعة{ص،ر}{\displaystyle \{p,r\}}هو نموذج مستقر للبرنامج الانفصالي

ص؛q{\displaystyle p;q}
ر←لا⁡q{\displaystyle r\leftarrow \operatorname {not} q}

لأنه أحد النموذجين الأدنى للاختزال

ص؛q{\displaystyle p;q}
ر.{\displaystyle r.}

يحتوي البرنامج المذكور أعلاه على نموذج أكثر استقرارًا،{q}{\displaystyle \{q\}}.

كما هو الحال في البرامج التقليدية، فإن كل عنصر من عناصر أي نموذج مستقر لبرنامج منفصلP{\displaystyle P}هي ذرة رأسية منP{\displaystyle P}، بمعنى أنه يظهر في رأس إحدى قواعدP{\displaystyle P}كما هو الحال في الحالة التقليدية، تكون النماذج المستقرة لبرنامج انفصالي هي نماذج دنيا وتشكل سلسلة مضادة. اختبار ما إذا كان لبرنامج انفصالي محدود نموذج مستقر هوΣ2P{\displaystyle \Sigma _{2}^{\rm {P}}}-كامل [ إيتر وجوتلوب، 1993].

نماذج مستقرة لمجموعة من الصيغ المنطقية

تتميز القواعد، حتى القواعد الانفصالية ، ببنية نحوية خاصة مقارنةً بالصيغ المنطقية العادية . فكل قاعدة انفصالية هي في جوهرها استلزام، حيث يكون مقدمها (جسم القاعدة) عبارة عن اقتران بين متغيرات حرفية ، بينما تكون نتيجتها (رأس القاعدة) عبارة عن فصل بين عناصر منطقية. وقد بيّن ديفيد بيرس [1997] وباولو فيراريس [2005] كيفية توسيع تعريف النموذج المستقر ليشمل مجموعات من الصيغ المنطقية العادية. ولهذا التعميم تطبيقات في برمجة مجموعات الإجابات .

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

التعريف العام للنموذج المستقر

وفقًا لـ [Ferraris, 2005]، فإن اختزال الصيغة المنطقيةF{\displaystyle F}بالنسبة لمجموعةأنا{\displaystyle I}الصيغة المشتقة من الذراتF{\displaystyle F}عن طريق استبدال كل صيغة فرعية قصوى غير مستوفاة بـأنا{\displaystyle I}مع الثابت المنطقي⊥{\displaystyle \bot }(خطأ). اختزال مجموعةP{\displaystyle P}من الصيغ المنطقية المتعلقة بـأنا{\displaystyle I}يتكون من اختزالات جميع الصيغ منP{\displaystyle P}بالنسبة إلىأنا{\displaystyle I}كما هو الحال في البرامج الانفصالية، نقول إن مجموعةأنا{\displaystyle I}يُعد نموذج الذرات نموذجًا مستقرًا لـP{\displaystyle P}لوأنا{\displaystyle I}يُعدّ هذا النموذج (فيما يتعلق باحتواء المجموعة) الأدنى بين نماذج اختزالP{\displaystyle P}بالنسبة إلىأنا{\displaystyle I}.

على سبيل المثال، اختزال المجموعة

{ص،ص∧q→ر،ص∧¬q→s}{\displaystyle \{p,p\land q\rightarrow r,p\land \neg q\rightarrow s\}}

بالنسبة إلى{ص،s}{\displaystyle \{p,s\}}يكون

{ص،⊥→⊥،ص∧¬⊥→s}.{\displaystyle \{p,\bot \rightarrow \bot ,p\land \neg \bot \rightarrow s\}.}

منذ{ص،s}{\displaystyle \{p,s\}}هو نموذج للاختزال، والمجموعات الفرعية المناسبة لتلك المجموعة ليست نماذج للاختزال.{ص،s}{\displaystyle \{p,s\}}هو نموذج مستقر لمجموعة الصيغ المعطاة.

لقد رأينا ذلك{ص،s}{\displaystyle \{p,s\}}يُعدّ هذا أيضًا نموذجًا مستقرًا لنفس الصيغة، مكتوبًا بلغة البرمجة المنطقية، بالمعنى المقصود في التعريف الأصلي . وهذا مثال على حقيقة عامة: عند تطبيقها على مجموعة من (الصيغ المقابلة لـ) القواعد التقليدية، فإن تعريف النموذج المستقر وفقًا لفيراريس يُكافئ التعريف الأصلي. وينطبق الأمر نفسه، بشكل أعم، على البرامج ذات القيود والبرامج الانفصالية .

خصائص دلالات النموذج المستقر العام

تنص النظرية على أن جميع عناصر أي نموذج مستقر لبرنامجP{\displaystyle P}هي ذرات الرأس منP{\displaystyle P}يمكن توسيع ذلك ليشمل مجموعات من الصيغ المنطقية، إذا عرّفنا الذرات الرئيسية على النحو التالي. ذرةأ{\displaystyle A}هي ذرة رأسية لمجموعةP{\displaystyle P}من الصيغ المنطقية إذا كان هناك ظهور واحد على الأقل لـأ{\displaystyle A}في صيغة منP{\displaystyle P}لا يقع ضمن نطاق النفي ولا ضمن مقدمة الاستلزام. (نفترض هنا أن التكافؤ يُعامل كاختصار، وليس كرابط أساسي).

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

ص∨¬ص{\displaystyle p\lor \neg p}

يحتوي على نموذجين مستقرين،∅{\displaystyle \emptyset }و{ص}{\displaystyle \{p\}}. الأخير ليس أدنى، وهو مجموعة شاملة مناسبة للأول.

اختبار ما إذا كانت مجموعة محدودة من الصيغ الافتراضية تمتلك نموذجًا مستقرًا هوΣ2P{\displaystyle \Sigma _{2}^{\rm {P}}}-كاملة ، كما هو الحال في البرامج الانفصالية .

انظر أيضاً

ملحوظات

  1. ↑ يعود هذا النهج في دلالات البرامج المنطقية بدون نفي إلى مارتن فان إمدن وروبرت كوالسكي - فان إمدن وكوالسكي 1976 .
  2. ↑ يُطلق جيلفوند وليفشيتز (1991) على النفي الثاني اسم "كلاسيكي" ويرمزان إليه بـ¬{\displaystyle \neg }.

مراجع