برمجة المنطق المقيد

برمجة المنطق المقيد هي شكل من أشكال برمجة القيود ، حيث يتم توسيع برمجة المنطق لتشمل مفاهيم من إرضاء القيود . برنامج المنطق المقيد هو برنامج منطقي يحتوي على قيود في متن بنوده. مثال على بند يتضمن قيدًا هو . في هذا البند، يمثل قيدًا؛ و و و هي قيم حرفية كما في برمجة المنطق العادية. يحدد هذا البند شرطًا واحدًا يتحقق بموجبه البيان : أن يكون أكبر من الصفر، وأن يكون كل من و صحيحًا.A(X,Y):-X+Y>0,B(X),C(Y)X+Y>0A(X,Y)B(X)C(Y)A(X,Y)X+YB(X)C(Y)

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

ملخص

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

B ( X , 1 ):- X < 0. B ( X , Y ):- X = 1 , Y > 0. A ( X , Y ):- X > 0 , B ( X , Y ).

كما هو الحال في البرمجة المنطقية التقليدية، يتطلب تقييم هدفٍ ما A(X,1)تقييمَ جسم العبارة الأخيرة باستخدام Y=1. وكما هو الحال في البرمجة المنطقية التقليدية، يتطلب هذا بدوره إثباتَ الهدف B(X,1). على عكس البرمجة المنطقية التقليدية، يتطلب هذا أيضًا استيفاءَ قيدٍ: ، وهو القيد الموجود في جسم العبارة الأخيرة. (في البرمجة المنطقية التقليدية، لا يمكن إثبات أن X>0 إلا إذا كانت X مرتبطةً بحدٍّ أساسيٍّX>0 كامل ، وسيفشل تنفيذ البرنامج إذا لم يكن الأمر كذلك).

لا يمكن دائمًا تحديد ما إذا كان القيد مُحققًا عند مواجهته. في هذه الحالة، على سبيل المثال، Xلا تُحدد قيمة عند تقييم البند الأخير. ونتيجةً لذلك، X>0لا يكون القيد مُحققًا ولا مُخالفًا في هذه المرحلة. بدلًا من المتابعة في تقييم B(X,1)ثم التحقق مما إذا كانت القيمة الناتجة لـ Xموجبة، يقوم المفسر بتخزين القيد X>0ثم المتابعة في تقييم B(X,1)؛ وبهذه الطريقة، يستطيع المفسر اكتشاف مخالفة القيد X>0أثناء تقييم والتراجع فورًا في هذه الحالة، بدلًا من انتظار انتهاء B(X,1)تقييم .B(X,1)

بشكل عام، تتم عملية تقييم برنامج منطق القيود بنفس طريقة تقييم برنامج المنطق العادي. مع ذلك، تُوضع القيود التي تُصادف أثناء التقييم في مجموعة تُسمى مخزن القيود. على سبيل المثال، A(X,1)تتم عملية تقييم الهدف بتقييم جسم العبارة الأولى باستخدام Y=1`؛`، وهذا التقييم يُضيف X>0إلى مخزن القيود ويتطلب B(X,1)إثبات الهدف. أثناء محاولة إثبات هذا الهدف، تُطبق العبارة الأولى، لكن تقييمها يُضيف X<0إلى مخزن القيود. هذه الإضافة تجعل مخزن القيود غير قابل للإثبات. عندئذٍ، يتراجع المفسر، مُزيلًا الإضافة الأخيرة من مخزن القيود. يُضيف تقييم العبارة الثانية ``` X=1و``` Y>0إلى مخزن القيود. بما أن مخزن القيود قابل للإثبات، ولا توجد قيود حرفية أخرى متبقية للإثبات، يتوقف المفسر عند الحل ``` X=1, Y=1.

علم الدلالة

يمكن تعريف دلالات برامج منطق القيود من حيث مترجم افتراضي يحتفظ بزوججي،S{\displaystyle \langle G,S\rangle }أثناء التنفيذ. يُسمى العنصر الأول من هذا الزوج بالهدف الحالي؛ ويُسمى العنصر الثاني بمخزن القيود. يحتوي الهدف الحالي على القيم الحرفية التي يحاول المفسر إثباتها، وقد يحتوي أيضًا على بعض القيود التي يحاول تحقيقها؛ بينما يحتوي مخزن القيود على جميع القيود التي افترض المفسر أنها قابلة للتحقيق حتى الآن.

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

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

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

يثبت المفسر الهدف عندما يكون الهدف الحالي فارغًا ولا يتم اكتشاف عدم قابلية مخزن القيود للتنفيذ. نتيجة التنفيذ هي مجموعة القيود الحالية (المبسطة). قد تتضمن هذه المجموعة قيودًا مثل:X=2{\displaystyle X=2}التي تُجبر المتغيرات على قيمة محددة، ولكنها قد تتضمن أيضًا قيودًا مثلX>2{\displaystyle X>2}التي تربط المتغيرات فقط دون إعطائها قيمة محددة.

بشكل رسمي، تُعرَّف دلالات برمجة منطق القيود من حيث الاشتقاقات . الانتقال هو زوج من أزواج الهدف/المخزن، ويُشار إليه بـجي،Sجي،S{\displaystyle \langle G,S\rangle \rightarrow \langle G',S'\rangle }يُشير هذا الزوج إلى إمكانية الانتقال من الحالةجي،S{\displaystyle \langle G,S\rangle }للتصريحجي،S{\displaystyle \langle G',S'\rangle }هذا التحول ممكن في ثلاث حالات محتملة:

  • أحد عناصر المجموعة G هو قيد C ، ولديناجي=جي{ج}{\displaystyle G'=G\backslash \{C\}}وS=S{ج}{\displaystyle S'=S\cup \{C\}}بمعنى آخر، يمكن نقل القيد من الهدف إلى مخزن القيود
  • عنصر من G هو حرفيل(ت1،...،تن){\displaystyle L(t_{1},\ldots ,t_{n})}توجد عبارة، إذا أعيدت كتابتها باستخدام متغيرات جديدة، تصبحل(ت1،...،تن):-ب{\displaystyle L(t_{1}',\ldots ,t_{n}')\mathrel {{:}{-}} B}، المجموعةجي{\displaystyle G'}هل G معل(ت1،...،تن){\displaystyle L(t_{1},\ldots ,t_{n})}تم استبدالها بـت1=ت1،...،تن=تن،ب{\displaystyle t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B}، وS=S{\displaystyle S'=S}بمعنى آخر، يمكن استبدال القيمة الحرفية بجسم صيغة جديدة من جملة تحتوي على نفس المسند في رأسها، مع إضافة جسم الصيغة الجديدة ومساواة المصطلحات المذكورة أعلاه إلى الهدف.
  • رملS{\displaystyle S'}تكون متكافئة وفقًا لدلالات القيد المحددة

سلسلة من الانتقالات هي اشتقاق. يمكن إثبات الهدف G إذا وُجد اشتقاق منجي،{\displaystyle \langle G,\emptyset \rangle }ل،S{\displaystyle \langle \emptyset ,S\rangle }بالنسبة لمخزن قيود قابل للإرضاء S. تُضفي هذه الدلالة طابعًا رسميًا على التطورات الممكنة للمفسر الذي يختار بشكل تعسفي الحرف المراد معالجته في الهدف والبند المراد استبداله بالحرف. بعبارة أخرى، يُثبت الهدف وفقًا لهذه الدلالة إذا وُجد تسلسل من اختيارات الأحرف والبنود، من بين العديد من الاختيارات الممكنة، يؤدي إلى هدف فارغ ومخزن قابل للإرضاء.

تقوم المترجمات الفعلية بمعالجة عناصر الهدف بترتيب LIFO : تُضاف العناصر في البداية وتُعالج من البداية. كما أنها تختار بند القاعدة الثانية وفقًا لترتيب كتابتها، وتعيد كتابة مخزن القيود عند تعديله.

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

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

يُشار عادةً إلى المساواة الثنائية بين وسيطي متغيرين حرفيين بشكل مختصر بواسطةل(ت1،...،تن)=ل(ت1،...،تن){\displaystyle L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')}هذا اختصار للقيودت1=ت1،...،تن=تن{\displaystyle t_{1}=t_{1}',\ldots ,t_{n}=t_{n}'}يضيف أحد المتغيرات الشائعة لدلالات برمجة منطق القيودل(ت1،...،تن)=ل(ت1،...،تن){\displaystyle L(t_{1},\ldots ,t_{n})=L(t_{1}',\ldots ,t_{n}')}مباشرة إلى مخزن القيود بدلاً من الهدف.

الشروط والأحكام

تُستخدم تعريفات مختلفة للمصطلحات، مما يُنتج أنواعًا مختلفة من برمجة منطق القيود: على الأشجار، أو الأعداد الحقيقية، أو المجالات المحدودة. أحد أنواع القيود الموجودة دائمًا هو تساوي المصطلحات. هذه القيود ضرورية لأن المفسر يُضيف t1=t2إلى الهدف كلما P(...t1...)استُبدل حرفي بجسم عبارة جديدة رأسها P(...t2...).

مصطلحات الشجرة

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

يمكن تبسيط القيد t1=t2إذا كان كلا الحدين عبارة عن رموز دالة مطبقة على حدود أخرى. إذا كان رمزا الدالة متطابقين وكان عدد الحدود الفرعية متطابقًا أيضًا، فيمكن استبدال هذا القيد بمساواة الحدود الفرعية ثنائياً. أما إذا كانت الحدود مكونة من رموز دوال مختلفة أو من نفس الدالة ولكن على عدد مختلف من الحدود، فإن القيد غير قابل للتحقيق.

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

في هذا الشكل من أشكال إرضاء القيود، تكون قيم المتغيرات عبارة عن حدود.

ريال

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

بتعبير أدق، تُعرَّف الحدود بأنها تعابير تُعبِّر عن متغيرات وثوابت حقيقية. وتُعدّ المساواة بين الحدود نوعًا من القيود الموجودة دائمًا، إذ يُولِّد المفسِّر هذه المساواة أثناء التنفيذ. على سبيل المثال، إذا كان الحرف الأول للهدف الحالي هو ` A(X+1)x`، واختار المفسِّر عبارة `x` التي تُصبح A(Y-1):-Y=1بعد إعادة كتابة `x` متغيرات، فإن القيود المُضافة إلى الهدف الحالي هي `x` X+1=Y-1و`x`.Y=1{\displaystyle Y=1}من الواضح أن قواعد التبسيط المستخدمة لرموز الدوال لا تُستخدم: X+1=Y-1لا يمكن اعتبار التعبير غير قابل للتحقيق لمجرد أن التعبير الأول تم بناؤه باستخدام +والثاني باستخدام -.

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

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

المجالات المحدودة

النوع الثالث من القيود المستخدمة في برمجة منطق القيود هو نطاقات محدودة. في هذه الحالة، تُؤخذ قيم المتغيرات من نطاق محدود، غالبًا ما يكون نطاق الأعداد الصحيحة . لكل متغير، يمكن تحديد نطاق مختلف: X::[1..5]على سبيل المثال، يعني أن قيمة المتغير Xتقع بين 0 1و 51. يمكن أيضًا تحديد نطاق المتغير عن طريق تعداد جميع القيم التي يمكن أن يأخذها؛ لذلك، يمكن كتابة تعريف النطاق أعلاه على النحو التالي X::[1,2,3,4,5]: . تسمح هذه الطريقة الثانية لتحديد النطاق باستخدام نطاقات لا تتكون من أعداد صحيحة، مثل X::[george,mary,john]. إذا لم يتم تحديد نطاق المتغير، يُفترض أنه مجموعة الأعداد الصحيحة القابلة للتمثيل في اللغة. يمكن إعطاء مجموعة من المتغيرات نفس النطاق باستخدام تعريف مثل [X,Y,Z]::[1..5].

قد يتقلص نطاق المتغير أثناء التنفيذ. فعندما يُضيف المُفسِّر قيودًا إلى مخزن القيود، فإنه يُجري عملية نشر القيود لفرض شكل من أشكال الاتساق المحلي ، وقد تُقلِّل هذه العمليات نطاق المتغيرات. إذا أصبح نطاق المتغير فارغًا، يصبح مخزن القيود غير متسق، ويتراجع الخوارزمية. إذا أصبح نطاق المتغير عنصرًا فريدًا ، يُمكن إسناد القيمة الوحيدة في نطاقه إلى المتغير. تشمل أشكال الاتساق المُطبَّقة عادةً اتساق القوس ، واتساق القوس الفائق ، واتساق الحدود . يُمكن فحص النطاق الحالي للمتغير باستخدام قيم حرفية مُحدَّدة؛ على سبيل المثال، dom(X,D)لمعرفة النطاق الحالي Dللمتغير X.

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

متجر الخصومات

يحتوي مخزن القيود على القيود التي يُفترض حاليًا أنها قابلة للتحقيق. ويمكن اعتباره بمثابة الاستبدال الحالي للبرمجة المنطقية العادية. عندما يُسمح فقط باستخدام حدود الشجرة، يحتوي مخزن القيود على قيود من الشكل التالي t1=t2: ; يتم تبسيط هذه القيود عن طريق التوحيد، مما ينتج عنه قيود من الشكل التالي variable=term: ; هذه القيود مكافئة للاستبدال.

مع ذلك، قد يحتوي مخزن القيود أيضًا على قيود من الشكل t1!=t2، إذا كان الفرق !=بين الحدود مسموحًا به. وعندما تكون القيود على الأعداد الحقيقية أو المجالات المحدودة مسموحة، فقد يحتوي مخزن القيود أيضًا على قيود خاصة بالمجال مثل X+2=Y/2، إلخ.

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

قد تُضاف القيود الخاصة بالمجال إلى مخزن القيود من متن العبارات أو من خلال مساواة قيمة حرفية برأس عبارة: على سبيل المثال، إذا أعاد المفسر كتابة القيمة الحرفية A(X+2)بعبارة يكون رأسها المتغير الجديد هو A(Y/2)، فسيتم إضافة القيد X+2=Y/2إلى مخزن القيود. إذا ظهر متغير في تعبير مجال حقيقي أو مجال محدود، فلا يمكنه أن يأخذ إلا قيمة في الأعداد الحقيقية أو المجال المحدود. لا يمكن لمثل هذا المتغير أن يأخذ حدًا مكونًا من دالة مطبقة على حدود أخرى كقيمة. يكون مخزن القيود غير قابل للإرضاء إذا كان المتغير ملزمًا بأخذ كل من قيمة المجال المحدد ودالة مطبقة على الحدود.

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

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

وضع العلامات

تُستخدم رموز التسمية على المتغيرات في نطاقات محدودة للتحقق من إمكانية تحقيق قيود المخزن أو تحقيقها جزئيًا، ولإيجاد قيمة مُرضية. تأخذ رمز التسمية الشكل `<t>` labeling([variables])، حيث `<t>` هي قائمة بالمتغيرات في نطاقات محدودة. عندما يُقيّم المُفسِّر رمزًا كهذا، فإنه يُجري بحثًا في نطاقات متغيرات القائمة لإيجاد قيمة تُحقق جميع القيود ذات الصلة. عادةً ما يتم ذلك من خلال نوع من التراجع : تُقيّم المتغيرات بالتسلسل، مع تجربة جميع القيم الممكنة لكل منها، والتراجع عند اكتشاف أي تناقض.

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

يُستخدم رمز التسمية الثاني لتحديد تقييم المتغيرات الذي يُحقق شرط التخزين. فبدون رمز التسمية، تُسند قيم للمتغيرات فقط عندما يحتوي شرط التخزين على قيد من النوع المحدد، X=valueوعندما يُقلل الاتساق المحلي نطاق المتغير إلى قيمة واحدة. يُجبر رمز التسمية المُطبق على بعض المتغيرات على تقييم هذه المتغيرات. بعبارة أخرى، بعد تطبيق رمز التسمية، تُسند قيمة لجميع المتغيرات.

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

حل ( X ):- القيود ( X ) ، التسمية ( X ) القيود ( X ) :- ( جميع قيود CSP )

عندما يُقيّم المُفسّر الهدف solve(args)، فإنه يضع نص صيغة جديدة من الشرط الأول في الهدف الحالي. وبما أن الهدف الأول هو constraints(X')، يتم تقييم الشرط الثاني، وتُنقل هذه العملية جميع القيود في الهدف الحالي، وفي النهاية إلى مخزن القيود. labeling(X')ثم يتم تقييم الحرف ، مما يُجبر على البحث عن حل لمخزن القيود. وبما أن مخزن القيود يحتوي على قيود مسألة إرضاء القيود الأصلية نفسها، فإن هذه العملية تبحث عن حل للمسألة الأصلية.

إعادة صياغة البرامج

يمكن إعادة صياغة برنامج منطق القيود لتحسين كفاءته. القاعدة الأولى هي وضع المتغيرات الدلالية بعد تراكم أكبر قدر ممكن من القيود عليها في مخزن القيود. بينما يُعادل هذا نظريًا ، فإن البحث الذي يُجرى عند مصادفة المفسر للمتغير الدلالي يكون في مخزن قيود لا يحتوي على القيد . ونتيجة لذلك، قد يُولّد حلولًا، مثل ، والتي يُكتشف لاحقًا أنها لا تُحقق هذا القيد. من ناحية أخرى، في الصياغة الثانية، يُجرى البحث فقط عندما يكون القيد موجودًا بالفعل في مخزن القيود. وبالتالي، لا يُعيد البحث إلا الحلول المتوافقة معه، مستفيدًا من حقيقة أن القيود الإضافية تُقلل من مساحة البحث.A(X):-labeling(X),X>0A(X):-X>0,labeling(X)X>0X=-1

تتمثل إحدى طرق إعادة الصياغة التي تُحسّن الكفاءة في وضع القيود قبل القيم الحرفية في متن البنود. وهما متكافئان من حيث المبدأ. مع ذلك، قد تتطلب الطريقة الأولى حسابات أكثر. على سبيل المثال، إذا احتوى مخزن القيود على القيد ، فإن المفسر يُقيّم بشكل متكرر في الحالة الأولى؛ إذا نجح، فإنه يكتشف أن مخزن القيود غير متسق عند إضافة . في الحالة الثانية، عند تقييم هذا البند، يُضيف المفسر أولًا إلى مخزن القيود، ثم يُقيّم إن أمكن . بما أن مخزن القيود بعد إضافة يصبح غير متسق، فإن التقييم المتكرر لـ لا يُجرى على الإطلاق.A(X):-B(X),X>0A(X):-X>0,B(X)X<-2B(X)X>0X>0B(X)X>0B(X)

ثمة طريقة ثالثة لتحسين الكفاءة تتمثل في إضافة قيود زائدة. إذا كان المبرمج يعلم (بأي وسيلة كانت) أن حل مشكلة ما يُحقق قيدًا معينًا، فيمكنه تضمين هذا القيد لإحداث تناقض في مخزن القيود في أقرب وقت ممكن. على سبيل المثال، إذا كان معروفًا مسبقًا أن تقييم B(X)سينتج عنه قيمة موجبة لـ X، فيمكن للمبرمج إضافة X>0قبل أي ظهور لـ B(X). على سبيل المثال، A(X,Y):-B(X),C(X)سيفشل في الهدف A(-2,Z)، ولكن لا يُكتشف ذلك إلا أثناء تقييم الهدف الفرعي B(X). من ناحية أخرى، إذا استُبدلت العبارة السابقة بـ ، فإن المفسر يتراجع بمجرد إضافة القيد إلى مخزن القيود، وهو ما يحدث قبل بدء تقييم .A(X,Y):-X>0,A(X),B(X)X>0B(X)

قواعد التعامل مع القيود

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

A(X) <=> B(X) | C(X) A(X) ==> B(X) | C(X)

تنص القاعدة الأولى على أنه إذا B(X)كان الشرط مستنتجًا من المخزن، A(X)فيمكن إعادة كتابة القيد على النحو التالي C(X): . على سبيل المثال، N*X>0يمكن إعادة كتابة على النحو التالي: X>0إذا كان المخزن يستلزم أن N>0. يرمز الرمز <=>إلى التكافؤ في المنطق، ويشير إلى أن القيد الأول مكافئ للقيد الثاني. عمليًا، هذا يعني أنه يمكن استبدال القيد الأول بالقيد الثاني.

تنص القاعدة الثانية على أن القيد الأخير هو نتيجة للقيد الأول، إذا كان القيد الأوسط متضمنًا في مخزن القيود. ونتيجة لذلك، إذا A(X)كان القيد موجودًا في مخزن B(X)القيود ومتضمنًا فيه، C(X)فيمكن إضافة القيد الجديد إلى المخزن. وبخلاف حالة التكافؤ، تُعد هذه إضافة وليست استبدالًا: يُضاف القيد الجديد بينما يبقى القيد القديم.

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

يمكن استخدام عبارات البرمجة المنطقية بالتزامن مع قواعد معالجة القيود لتحديد طريقة إثبات قابلية إرضاء مخزن القيود. تُستخدم عبارات مختلفة لتنفيذ الخيارات المختلفة للطريقة؛ وتُستخدم قواعد معالجة القيود لإعادة كتابة مخزن القيود أثناء التنفيذ. على سبيل المثال، يمكن تنفيذ التراجع مع نشر الوحدة بهذه الطريقة. لنفترض holds(L)أن يمثل عبارة اقتراحية، حيث Lتكون القيم الحرفية في القائمة بنفس ترتيب تقييمها. يمكن تنفيذ الخوارزمية باستخدام عبارات لاختيار تعيين قيمة حرفية إلى صحيح أو خطأ، وقواعد معالجة القيود لتحديد النشر. تحدد هذه القواعد أنه holds([l|L])يمكن إزالة إذا l=trueكان يتبع من المخزن، ويمكن إعادة كتابته على النحو التالي holds(L)إذا l=falseكان يتبع من المخزن. وبالمثل، holds([l])يمكن استبدال بـ l=true. في هذا المثال، يتم تنفيذ اختيار قيمة لمتغير باستخدام عبارات البرمجة المنطقية؛ ومع ذلك، يمكن ترميزه في قواعد معالجة القيود باستخدام امتداد يسمى قواعد معالجة القيود الانفصالية أو CHR .

التقييم من الأسفل إلى الأعلى

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

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

A ( q ). B ( X ):- A ( X ).

تكون مجموعة النتائج فارغة في البداية. في الخطوة الأولى، A(q)تكون العبارة الوحيدة التي يمكن إثبات صحتها (لأنها فارغة)، A(q)ولذلك تُضاف إلى مجموعة النتائج الحالية. في الخطوة الثانية، بما أن A(q)العبارة قد ثبتت، يمكن استخدام العبارة الثانية B(q)وتُضاف إلى النتائج. ولأنه لا يمكن إثبات أي نتيجة أخرى من العبارة الأولى {A(q),B(q)}، ينتهي التنفيذ.

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

A ( q ). B ( X ):- A ( X ). A ( X ):- B ( X ).

على سبيل المثال، أثناء تقييم جميع الإجابات المتعلقة بالهدف A(X)، ستنتج استراتيجية التقييم من أعلى إلى أسفل النتائج التالية:

A ( q ) A ( q) ):- B ( q ), B ( q ) ):- A ( q ), A ( q ) A ( q ) ):- B ( q ), B ( q ) ):- A ( q ), A ( q ) ):- B ( q) , B ( q ) ):- A ( q ), A ( q )

بمعنى آخر، يتم التوصل إلى النتيجة الوحيدة A(q)أولاً، ثم يتكرر عمل الخوارزمية على الاشتقاقات التي لا تُنتج أي إجابة أخرى. وبشكل أعم، قد تتكرر استراتيجية التقييم من أعلى إلى أسفل على الاشتقاقات الممكنة، حتى في حال وجود اشتقاقات أخرى.

لا تعاني استراتيجية "من الأسفل إلى الأعلى" من نفس العيب، إذ لا يكون للنتائج المستنتجة مسبقًا أي تأثير. في البرنامج المذكور أعلاه، تبدأ استراتيجية "من الأسفل إلى الأعلى" بإضافة نتائج جديدة A(q)إلى مجموعة النتائج؛ في الخطوة الثانية، B(X):-A(X)تُستخدم النتائج لاستنتاج النتائج B(q)؛ في الخطوة الثالثة، تكون الحقائق الوحيدة التي يمكن استنتاجها من النتائج الحالية هي النتائج A(q)و B(q)، وهما موجودتان بالفعل ضمن مجموعة النتائج. ونتيجة لذلك، تتوقف الخوارزمية.

في المثال أعلاه، كانت الحقائق المستخدمة الوحيدة هي القيم الحرفية الأساسية. عمومًا، تُعتبر كل جملة تحتوي على قيود فقط في متنها حقيقة. على سبيل المثال، تُعتبر الجملة حقيقة أيضًا. وفقًا لهذا التعريف الموسع للحقائق، قد تكون بعض الحقائق متكافئة دون أن تكون متطابقة نحويًا. على سبيل المثال، تُكافئ الجملة الأولى، وكلاهما يُكافئ الجملة الثانية . لحل هذه المشكلة، تُترجم الحقائق إلى صيغة عادية يكون رأسها عبارة عن مجموعة من المتغيرات المختلفة؛ وتكون حقيقتان متكافئتين إذا كان متنهما متكافئًا بالنسبة لمتغيرات الرأس، أي أن مجموعات حلولهما متطابقة عند تقييدها بهذه المتغيرات.A(X):-X>0,X<10A(q)A(X):-X=qA(X):-X=Y,Y=q

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

أ ( 0 ). ا ( X ): - X > 0. ا ( X ): - X = Y + 1 , ا ( Y ).

تستنتج خوارزمية التقييم من الأسفل إلى الأعلى أولاً أن A(X)العبارة صحيحة لـ X=0و X>0. في الخطوة الثانية، تسمح الحقيقة الأولى مع الشرط الثالث باستنتاج A(1). في الخطوة الثالثة، A(2)يتم استنتاج ، وهكذا. مع ذلك، فإن هذه الحقائق مستنتجة بالفعل من حقيقة أن العبارة A(X)صحيحة لأي قيمة غير سالبة لـ X. يمكن التغلب على هذا العيب بالتحقق من حقائق الاستلزام التي ستُضاف إلى مجموعة النتائج الحالية. إذا كانت النتيجة الجديدة مستنتجة بالفعل من المجموعة، فلن تُضاف إليها. بما أن الحقائق تُخزن كشروط، ربما مع "متغيرات محلية"، فإن الاستلزام يقتصر على متغيرات رؤوسها.

برمجة منطق القيود المتزامنة

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

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

التطبيقات

تم تطبيق برمجة المنطق المقيد على عدد من المجالات، مثل الجدولة الآلية ، [ 1 ] واستنتاج النوع ، [ 2 ] والهندسة المدنية ، والهندسة الميكانيكية ، والتحقق من الدوائر الرقمية ، ومراقبة الحركة الجوية ، والتمويل، وغيرها.

تاريخ

طُوِّرت برمجة المنطق المقيد بواسطة جعفر ولاسيز عام ١٩٨٧. [ ٣ ] عمَّما الملاحظة القائلة بأن مصطلحي المعادلات واللا معادلات في لغة برولوج ٢ يمثلان شكلاً محدداً من القيود، وعمّما هذه الفكرة لتشمل لغات القيود المختلفة. وكانت أولى تطبيقات هذا المفهوم هي برولوج ٣ ، و CLP(R) ، و CHIP .

انظر أيضاً

مراجع

مراجع

  1. عبد الناظر، سليم، وهانز شلينكر. " جدولة الممرضة باستخدام برمجة منطق القيد ." AAAI /IAAI. 1999.
  2. ميخائيلوف، سبيرو، وفرانك بفينينغ . " برمجة المنطق من الرتبة العليا كبرمجة منطق القيود ". PPCP. المجلد 93. 1993.
  3. جعفر، جوكسان، و جيه إل. لاسيز. " برمجة المنطق المقيد ". وقائع الندوة الرابعة عشرة لجمعية ACM SIGPLAN-SIGACT حول مبادئ لغات البرمجة . ACM، 1987.