مشكلة الإطار

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

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

في المثال المبسط للباب والضوء، يمكن صياغة الحجب رسميًا بواسطة مسندين${\displaystyle \mathrm {occludeopen} (t)}$و${\displaystyle \mathrm {occludeon} (t)}$والسبب في ذلك هو أن الشرط لا يمكن أن تتغير قيمته إلا إذا كان شرط الحجب المقابل صحيحًا في النقطة الزمنية التالية. وبدوره، يكون شرط الحجب صحيحًا فقط عند تنفيذ إجراء يؤثر على الشرط.

${\displaystyle \neg \mathrm {مفتوح} (0)}$

${\displaystyle \neg \mathrm {on} (0)}$

${\displaystyle \mathrm {open} (1)\wedge \mathrm {occludeopen} (1)}$

${\displaystyle \forall t.\neg \mathrm {occludeopen} (t)\implies (\mathrm {open} (t-1)\iff \mathrm {open} (t))}$

${\displaystyle \forall t.\neg \mathrm {occludeon} (t)\implies (\mathrm {on} (t-1)\iff \mathrm {on} (t))}$

بشكل عام، كل فعل يجعل شرطاً ما صحيحاً أو خاطئاً يجعل أيضاً مسند الحجب المقابل صحيحاً. في هذه الحالة،${\displaystyle \mathrm {occludeopen} (1)}$صحيح، مما يجعل الشرط السابق للصيغة الرابعة أعلاه خاطئًا بالنسبة لـ${\displaystyle t=1}$لذلك، فإن القيد هو${\displaystyle \mathrm {open} (t-1)\iff \mathrm {open} (t)}$لا ينطبق ذلك على${\displaystyle t=1}$. لذلك،${\displaystyle \mathrm {مفتوح} }$يمكن أن تتغير القيمة، وهذا ما يتم فرضه أيضًا بواسطة الصيغة الثالثة.

لكي يتحقق هذا الشرط، يجب أن تكون مسندات الحجب صحيحة فقط عندما تصبح صحيحة كنتيجة لفعل ما. ويمكن تحقيق ذلك إما عن طريق التحديد أو عن طريق إكمال المسند. ومن الجدير بالذكر أن الحجب لا يستلزم بالضرورة تغييرًا: على سبيل المثال، تنفيذ فعل فتح الباب عندما يكون مفتوحًا بالفعل (في الصيغة أعلاه) يجعل المسند${\displaystyle \mathrm {occludeopen} }$صحيح ويجعل${\displaystyle \mathrm {مفتوح} }$صحيح؛ ومع ذلك،${\displaystyle \mathrm {مفتوح} }$لم تتغير قيمتها، لأنها كانت صحيحة بالفعل.

يشبه هذا الترميز حل الحجب السلس، لكن المسندات الإضافية تدل على التغيير، وليس على الإذن بالتغيير. على سبيل المثال،${\displaystyle \mathrm {changeopen} (t)}$يمثل حقيقة أن المسند${\displaystyle \mathrm {مفتوح} }$سيتغير من وقت لآخر${\displaystyle t}$ل${\displaystyle t+1}$وبالتالي، يتغير الشرط إذا وفقط إذا كان الشرط المقابل له صحيحًا. ويؤدي أي فعل إلى تغيير إذا وفقط إذا جعل شرطًا كان خاطئًا سابقًا صحيحًا أو العكس.

${\displaystyle \neg \mathrm {مفتوح} (0)}$

${\displaystyle \neg \mathrm {on} (0)}$

${\displaystyle \neg \mathrm {open} (0)\ضمني \mathrm {changeopen} (0)}$

${\displaystyle \forall t.\mathrm {changeopen} (t)\iff (\neg \mathrm {open} (t)\iff \mathrm {open} (t+1))}$

${\displaystyle \forall t.\mathrm {changeon} (t)\iff (\neg \mathrm {on} (t)\iff \mathrm {on} (t+1))}$

الصيغة الثالثة هي طريقة أخرى للتعبير عن أن فتح الباب يؤدي إلى فتحه. تحديدًا، تنص على أن فتح الباب يغير حالته إذا كان مغلقًا سابقًا. أما الشرطان الأخيران فينصان على أن قيمة شرط ما تتغير في وقت معين.${\displaystyle t}$إذا وفقط إذا كان شرط التغيير المقابل صحيحًا في وقت${\displaystyle t}$لإكمال الحل، يجب أن تكون نقاط الوقت التي تكون فيها مسندات التغيير صحيحة أقل ما يمكن، ويمكن القيام بذلك عن طريق تطبيق إكمال المسند على القواعد التي تحدد آثار الإجراءات.

يمكن تحديد قيمة الشرط بعد تنفيذ إجراء ما من خلال حقيقة أن الشرط يكون صحيحًا إذا وفقط إذا:

1. الفعل يجعل الشرط صحيحاً؛ أو
2. كان الشرط صحيحاً في السابق، والفعل لا يجعله خاطئاً.

إن بديهية الحالة اللاحقة هي صياغة منطقية لهاتين الحقيقتين. على سبيل المثال، إذا${\displaystyle \mathrm {opendoor} (t)}$و${\displaystyle \mathrm {closedoor} (t)}$هناك شرطان يستخدمان للدلالة على أن الإجراء الذي تم تنفيذه في وقت${\displaystyle t}$كان الهدف هو فتح الباب أو إغلاقه، على التوالي، ويتم ترميز المثال الجاري على النحو التالي.

${\displaystyle \neg \mathrm {مفتوح} (0)}$

${\displaystyle \neg \mathrm {on} (0)}$

${\displaystyle \mathrm {مفتوح} (0)}$

${\displaystyle \forall t.\mathrm {open} (t+1)\iff \mathrm {opendoor} (t)\vee (\mathrm {open} (t)\wedge \neg \mathrm { Closedoor} (t))}$

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

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

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

في حساب التفاضل والتكامل السلس، يُمثَّل كل حالة ممكنة بمصطلح مُشتق من تركيب مصطلحات أخرى، يُمثل كل منها الشروط الصحيحة في تلك الحالة. على سبيل المثال، تُمثَّل الحالة التي يكون فيها الباب مفتوحًا والضوء مُضاءً بالمصطلح${\displaystyle \mathrm {open} \circ \mathrm {on} }$من المهم ملاحظة أن المصطلح ليس صحيحًا أو خاطئًا في حد ذاته، لأنه موضوع وليس شرطًا. بعبارة أخرى، المصطلح${\displaystyle \mathrm {open} \circ \mathrm {on} }$يمثل هذا حالة محتملة، ولا يعني بالضرورة أنها الحالة الحالية. يمكن تحديد شرط منفصل لتوضيح أن هذه هي الحالة الفعلية في وقت معين، على سبيل المثال،${\displaystyle \mathrm {state} (\mathrm {open} \circ \mathrm {on} ,10)}$هذا يعني أن هذه هي الحالة في ذلك الوقت${\displaystyle 10}$.

يكمن حل مشكلة الإطار المذكورة في حساب التفاضل والتكامل السلس في تحديد آثار الأفعال من خلال بيان كيفية تغير مصطلح يمثل الحالة عند تنفيذ الفعل. على سبيل المثال، يُعبَّر عن فعل فتح الباب عند الزمن صفر بالصيغة التالية:

${\displaystyle \mathrm {state} (s\circ \mathrm {open} ,1)\iff \mathrm {state} (s,0)}$

يتم تمثيل فعل إغلاق الباب، الذي يجعل الشرط خاطئاً بدلاً من أن يكون صحيحاً، بطريقة مختلفة قليلاً:

${\displaystyle \mathrm {state} (s,1)\iff \mathrm {state} (s\circ \mathrm {open} ,0)}$

تنجح هذه الصيغة بشرط تحديد البديهيات المناسبة بشأنها.${\displaystyle \mathrm {state} }$و${\displaystyle \circ }$على سبيل المثال، لا يُعدّ المصطلح الذي يحتوي على الشرط نفسه مرتين حالةً صالحة (على سبيل المثال،${\displaystyle \mathrm {state} (\mathrm {open} \circ s\circ \mathrm {open} ,t)}$هذا خطأ دائماً بالنسبة لكل${\displaystyle s}$و${\displaystyle t}$).

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

${\displaystyle {\mathit {holdsAt}}(F,T2)\leftarrow }$

${\displaystyle [{\mathit {happensAt}}(E1,T1)\wedge {\mathit {initiates}}(E1,F,T1)\wedge (T1<T2)\wedge }$

${\displaystyle \neg \exists E2,T[{\mathit {happensAt}}(E2,T)\wedge {\mathit {terminates}}(E2,F,T)\wedge (T1\leq T<T2)]}$

تنص البديهية على أن الشخص الطليق${\displaystyle F}$يحجز في وقت واحد${\displaystyle T2}$، إذا حدث${\displaystyle E1}$يحدث ويبدأ${\displaystyle F}$في وقت سابق${\displaystyle T1}$ولا يوجد حدث${\displaystyle E2}$ يحدث ذلك وينتهي${\displaystyle F}$ بعد أو في نفس الوقت${\displaystyle T1}$وقبل ذلك${\displaystyle T2}$.

لتطبيق حساب الأحداث على مجال مشكلة معين، من الضروري تحديد${\displaystyle initiates}$و${\displaystyle terminates}$المسندات الخاصة بهذا المجال. على سبيل المثال:

${\displaystyle {\mathit {initiates}}(opendoor,open,T).}$

${\displaystyle {\mathit {terminates}}(opendoor,closed,T).}$

${\displaystyle {\mathit {initiates}}(closedoor,closed,T).}$

${\displaystyle {\mathit {terminates}}(closeddoor,open,T).}$

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

${\displaystyle {\mathit {happensAt}}(opendoor,0)}$.

${\displaystyle {\mathit {happensAt}}(closedoor,3)}$.

لحل مشكلة، مثل ما هي الطاقات التي تسري في الوقت 5؟، من الضروري طرح المشكلة كهدف، مثل:

${\displaystyle \exists Fluent[{\mathit {holdsAt(Fluent,5)}}].}$

في هذه الحالة، الحصول على الحل الفريد:

${\displaystyle Fluent=closed.}$

يحل حساب الأحداث مشكلة الإطار، ويزيل الحلول غير المرغوب فيها، باستخدام منطق غير رتيب ، مثل منطق الرتبة الأولى مع التقييد ^{[ 3 ]} أو عن طريق التعامل مع حساب الأحداث كبرنامج منطقي باستخدام النفي كفشل .

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

${\displaystyle {\frac {R(x,s)\;:\ R(x,\mathrm {do} (a,s))}{R(x,\mathrm {do} (a,s))}}}$

(لو${\displaystyle R(x)}$هذا صحيح في هذه الحالة${\displaystyle s}$ويمكن افتراض ^{[ 4 ]} أن${\displaystyle R(x)}$يظل هذا صحيحًا بعد تنفيذ الإجراء${\displaystyle a}$إذن يمكننا أن نستنتج أن${\displaystyle R(x)}$(يبقى صحيحاً).

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

إن نظير الحل المنطقي الافتراضي في لغة برمجة مجموعات الإجابات هو قاعدة ذات نفي قوي :

${\displaystyle r(X,T+1)\leftarrow r(X,T),\ {\hbox{not }}\sim r(X,T+1)}$

(لو${\displaystyle r(X)}$صحيح في بعض الأحيان${\displaystyle T}$ويمكن افتراض أن${\displaystyle r(X)}$يظل هذا صحيحًا في وقت${\displaystyle T+1}$إذن يمكننا أن نستنتج أن${\displaystyle r(X)}$(يبقى صحيحاً).

منطق الفصل هو أسلوب رسمي للاستدلال حول برامج الحاسوب باستخدام مواصفات ما قبل/ما بعد على النحو التالي:${\displaystyle \{\mathrm {precondition} \}\ \mathrm {code} \ \{\mathrm {postcondition} \}}$منطق الفصل هو امتداد لمنطق هوار، وهو موجه للاستدلال حول هياكل البيانات القابلة للتغيير في ذاكرة الحاسوب والموارد الديناميكية الأخرى، ويحتوي على رابط خاص (*)، يُنطق "و بشكل منفصل"، لدعم الاستدلال المستقل حول مناطق الذاكرة المنفصلة. ^{[ 5 ] [ 6 ]}

تعتمد منطق الفصل على تفسير دقيق لمواصفات ما قبل وما بعد التنفيذ، والتي تنص على أن الكود لا يمكنه الوصول إلا إلى مواقع الذاكرة التي يضمن وجودها الشرط المسبق. ^{[ 7 ]} وهذا ما يُعزز سلامة أهم قاعدة استدلال في هذا المنطق، وهي قاعدة الإطار.

${\displaystyle {\frac {\{\mathrm {precondition} \}\ \mathrm {code} \ \{\mathrm {postcondition} \}}{\{\mathrm {precondition} \ast \mathrm {frame} \}\ \mathrm {code} \ \{\mathrm {postcondition} \ast \mathrm {frame} \}}}}$

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

${\displaystyle {\frac {\{\operatorname {list} (x)\}\ \mathrm {code} \ \{\operatorname {sortedlist} (x)\}}{\{\operatorname {list} (x)\ast \operatorname {sortedlist} (y)\}\ \mathrm {code} \ \{\operatorname {sortedlist} (x)\ast \operatorname {sortedlist} (y)\}}}}$

يلتقط هذا الكود الذي يقوم بفرز القائمة x لا يقوم بإلغاء فرز قائمة منفصلة y، ويفعل ذلك دون ذكر y على الإطلاق في المواصفات الأولية أعلى السطر.

أدى أتمتة قاعدة الإطار إلى زيادات كبيرة في قابلية التوسع لتقنيات الاستدلال الآلي للبرمجيات، ^{[ 8 ]} والتي تم نشرها في نهاية المطاف على نطاق صناعي لقواعد بيانات برمجية تحتوي على عشرات الملايين من الأسطر. ^{[ 9 ]}

يبدو أن هناك بعض التشابه بين حل منطق الفصل لمشكلة الإطار وحل حساب التفاضل والتكامل السلس المذكور أعلاه.

تتجنب لغات وصف الأفعال مشكلة الإطار بدلاً من حلها. لغة وصف الأفعال هي لغة رسمية ذات بنية نحوية محددة لوصف المواقف والأفعال. على سبيل المثال، أن الفعل${\displaystyle \mathrm {opendoor} }$يُعبَّر عن فتح الباب إذا لم يكن مغلقًا بما يلي:

${\displaystyle \mathrm {opendoor} }$الأسباب${\displaystyle \mathrm {open} }$لو${\displaystyle \neg \mathrm {locked} }$

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

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