منطق النقطة الثابتة

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

تمت دراسة منطق النقطة الثابتة الأدنى بشكل منهجي لأول مرة من قبل يانيس ن. موشوفاكيس في عام 1974، ^{[ 1 ]} وتم تقديمه لعلماء الحاسوب في عام 1979، عندما اقترح ألفريد أهو وجيفري أولمان منطق النقطة الثابتة كلغة استعلام معبرة لقواعد البيانات. ^{[ 2 ]}

بالنسبة للتوقيع العلائقي X ، فإن FO[PFP]( X ) هي مجموعة الصيغ المُشكَّلة من X باستخدام الروابط والمسندات من الدرجة الأولى ، والمتغيرات من الدرجة الثانية ، بالإضافة إلى عامل النقطة الثابتة الجزئية.${\displaystyle \operatorname {PFP} }$تُستخدم لتكوين صيغ من الشكل${\displaystyle [\operatorname {PFP} _{{\vec {x}},P}\varphi ]{\vec {t}}}$، أين${\displaystyle P}$متغير من الدرجة الثانية،${\displaystyle {\vec {x}}}$مجموعة من المتغيرات من الدرجة الأولى،${\displaystyle {\vec {t}}}$مجموعة من المصطلحات وأطوالها${\displaystyle {\vec {x}}}$و${\displaystyle {\vec {t}}}$يتزامن مع عدد${\displaystyle P}$.

ليكن k عددًا صحيحًا،${\displaystyle x,y}$لتكن x و P متجهات من k متغيرات، وليكن P متغيرًا من الرتبة الثانية من الرتبة k ، ولتكن φ دالة من الرتبة FO(PFP,X) تستخدم x و P كمتغيرات. يمكننا تعريفها بشكل تكراري${\displaystyle (P_{i})_{i\in N}}$بحيث${\displaystyle P_{0}(x)=خطأ}$و${\displaystyle P_{i}(x)=\varphi (P_{i-1},x)}$(بمعنى φ مع${\displaystyle P_{i-1}}$(باستبدالها بالمتغير من الدرجة الثانية P ). عندئذٍ، إما أن تكون هناك نقطة ثابتة، أو قائمة من${\displaystyle (P_{i})}$s دورية. ^{[ 3 ]}

${\displaystyle [\operatorname {PFP} _{{\vec {x}},P}\varphi ]{\vec {t}}}$يُعرَّف بأنه قيمة النقطة الثابتة لـ${\displaystyle (P_{i})}$على${\displaystyle {\vec {t}}}$إذا كانت هناك نقطة ثابتة، وإلا فهي خاطئة. ^{[ 4 ]} بما أن P هي خصائص من الرتبة k ، فإن عددها على الأكثر${\displaystyle 2^{n^{k}}}$قيم لـ${\displaystyle P_{i}}$لذلك، باستخدام عداد في فضاء متعدد الحدود، يمكننا التحقق مما إذا كانت هناك حلقة تكرارية أم لا. ^{[ 5 ]}

لقد ثبت أنه في الهياكل المحدودة المرتبة، يمكن التعبير عن خاصية ما في FO(PFP, X ) إذا وفقط إذا كانت تقع في PSPACE . ^{[ 6 ]}

بما أن المسندات المتكررة المستخدمة في حساب النقطة الثابتة الجزئية ليست رتيبة بشكل عام، فقد لا توجد النقطة الثابتة دائمًا. FO(LFP,X)، أي منطق النقطة الثابتة الصغرى ، هي مجموعة الصيغ في FO(PFP,X) حيث تُؤخذ النقطة الثابتة الجزئية فقط على الصيغ φ التي تحتوي فقط على ظهورات موجبة لـ P (أي الظهورات التي تسبقها عدد زوجي من النفي). هذا يضمن رتابة بناء النقطة الثابتة (أي، إذا كان المتغير من الرتبة الثانية هو P ، فإن${\displaystyle P_{i}(x)}$يشير دائماً إلى${\displaystyle P_{i+1}(x)}$).

بسبب خاصية الرتابة، نضيف فقط متجهات إلى جدول الحقيقة لـ P ، وبما أنه لا يوجد سوى${\displaystyle n^{k}}$سنجد دائمًا نقطة ثابتة قبل المتجهات الممكنة${\displaystyle n^{k}}$التكرارات. تُظهر نظرية إيمرمان-فاردي، التي تم إثباتها بشكل مستقل بواسطة إيمرمان ^{[ 7 ]} وفاردي [ ^{8 ]} ، أن FO(LFP, X ⁾ تميز P على جميع الهياكل المرتبة.

تتطابق قدرة التعبير لمنطق النقطة الثابتة الصغرى تمامًا مع قدرة التعبير للغة استعلام قواعد البيانات Datalog ، مما يدل على أنه على الهياكل المرتبة، يمكن لـ Datalog التعبير بدقة عن تلك الاستعلامات القابلة للتنفيذ في وقت متعدد الحدود. ^{[ 9 ]}

هناك طريقة أخرى لضمان رتابة بناء النقطة الثابتة، وهي إضافة مجموعات جديدة فقط إلى${\displaystyle P}$في كل مرحلة من مراحل التكرار، دون إزالة الصفوف التي${\displaystyle P}$لم يعد هذا صحيحًا. رسميًا، نُعرّف${\displaystyle \operatorname {IFP} (\phi _{P,x})}$مثل${\displaystyle \operatorname {PFP} (\psi _{P,x})}$أين${\displaystyle \psi (P,x)=\phi (P,x)\vee P(x)}$.

تتفق هذه النقطة الثابتة التضخمية مع النقطة الثابتة الصغرى عند تعريف الأخيرة. مع أن منطق النقطة الثابتة التضخمية قد يبدو للوهلة الأولى أكثر تعبيرًا من منطق النقطة الثابتة الصغرى نظرًا لدعمه نطاقًا أوسع من حجج النقطة الثابتة، إلا أن كل صيغة من صيغ FO[IFP]( X ) تُكافئ في الواقع صيغة من صيغ FO[LFP]( X ). ^{[ 10 ]}

بينما اقتصرت جميع عوامل النقطة الثابتة المُقدَّمة حتى الآن على تعريف مُسند واحد فقط، يُنظر إلى العديد من برامج الحاسوب بشكل طبيعي على أنها تُكرِّر على عدة مُسندات في آنٍ واحد. إما بزيادة عدد عوامل النقطة الثابتة أو بتداخلها، يُمكن في الواقع التعبير عن كل نقطة ثابتة صغرى أو تضخمية أو جزئية متزامنة باستخدام بنيات التكرار الفردي المُناظرة التي نوقشت أعلاه. ^{[ 11 ]}

بدلاً من السماح بالاستقراء على المسندات التعسفية، فإن منطق الإغلاق المتعدي يسمح فقط بالتعبير عن الإغلاقات المتعدية بشكل مباشر.

FO[TC]( X ) هي مجموعة الصيغ المُشكَّلة من X باستخدام الروابط والمسندات من الدرجة الأولى، والمتغيرات من الدرجة الثانية، بالإضافة إلى عامل الإغلاق المتعدي.${\displaystyle \operatorname {TC} }$تُستخدم لتكوين صيغ من الشكل${\displaystyle [\operatorname {TC} _{{\vec {x}},{\vec {y}}}\varphi ]{\vec {s}}{\vec {t}}}$، أين${\displaystyle {\vec {x}}}$و${\displaystyle {\vec {y}}}$هي عبارة عن مجموعات من متغيرات من الدرجة الأولى متميزة ثنائياً،${\displaystyle {\vec {t}}}$و${\displaystyle {\vec {s}}}$مجموعات من المصطلحات وأطوالها${\displaystyle {\vec {x}}}$،${\displaystyle {\vec {y}}}$،${\displaystyle {\vec {s}}}$و${\displaystyle {\vec {t}}}$يتزامن.

يُعرَّف TC على النحو التالي: ليكن k عددًا صحيحًا موجبًا و${\displaystyle u,v,x,y}$لتكن متجهات من k متغيرات. إذن${\displaystyle {\mathsf {TC}}(\varphi _{u,v})(x,y)}$تكون العبارة صحيحة إذا وُجدت n متجهات من المتغيرات${\displaystyle (z_{i})}$بحيث${\displaystyle z_{1}=x,z_{n}=y}$ولجميع${\displaystyle i<n}$،${\displaystyle \varphi (z_{i},z_{i+1})}$هذا صحيح. هنا، φ هي صيغة مكتوبة بلغة FO(TC) و${\displaystyle \varphi (x,y)}$يعني ذلك استبدال المتغيرين u و v بالمتغيرين x و y .

في البنى المرتبة، تُميّز FO[TC] فئة التعقيد NL . ^{[ 12 ]} يُعدّ هذا التمييز جزءًا أساسيًا من برهان إيمرمان على أن NL مغلقة تحت المكمل (NL = co-NL). ^{[ 13 ]}

يُعرَّف FO[DTC]( X ) على أنه FO(TC,X) حيث يكون عامل الإغلاق المتعدي حتميًا. هذا يعني أنه عند تطبيق${\displaystyle \operatorname {DTC} (\phi _{u,v})}$نعلم أنه لكل قيمة لـ u ، يوجد على الأكثر قيمة واحدة لـ v بحيث${\displaystyle \phi (u,v)}$.

يمكننا أن نفترض أن${\displaystyle \operatorname {DTC} (\phi _{u,v})}$هو اختصار لفظي لـ${\displaystyle \operatorname {TC} (\psi _{u,v})}$أين${\displaystyle \psi (u,v)=\phi (u,v)\wedge \forall x(x=v\vee \neg \phi (u,x))}$.

^{على الهياكل المرتبة ،} FO[DTC] تميز فئة التعقيد L. [ ^{12 ]}

حدد رأسًا${\displaystyle x}$أن يكون ضعيفاً إذا، باستثناء واحد على الأكثر${\displaystyle y}$كل جيرانها${\displaystyle z}$ضعيف، وفقًا لصيغة النقطة الثابتة${\displaystyle W(x)\leftarrow \exists y\forall z{\bigl (}x\sim z\Rightarrow (y=z\vee W(z)){\bigr )}}$. تشكل الرؤوس المتبقية النواة الثنائية للرسم البياني.

تنص الصيغة التالية المكتوبة بلغة منطق النقطة الثابتة الصغرى على أن النواة الثنائية للرسم البياني ليست فارغة: $${\displaystyle \exists t[\operatorname {LFP} _{x,P}\exists y\forall z{\bigl (}x\sim z\Rightarrow (y=z\vee P(z)){\bigr )}]t}$$

تكون الشبكة متصلة إذا وُجد مسار بين كل زوج من الرؤوس. وجود مسار بين رأسين هو الإغلاق المتعدي لعلاقة التجاور. لذا، تنص الصيغة التالية المكتوبة بمنطق الإغلاق المتعدي على أن الشبكة متصلة: $${\displaystyle \forall s\forall t[\operatorname {TC} _{x,y}x\sim y]st}$$

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

سنعرّف الرتبة الأولى باستخدام التكرار،${\displaystyle {\mathsf {FO}}[t(n)]}$؛ هنا${\displaystyle t(n)}$هي (فئة من) الدوال من الأعداد الصحيحة إلى الأعداد الصحيحة، ولفئات مختلفة من الدوال${\displaystyle t(n)}$سنحصل على فئات تعقيد مختلفة${\displaystyle {\mathsf {FO}}[t(n)]}$.

سنكتب في هذا القسم ${\displaystyle (\forall xP)Q}$بمعنى${\displaystyle (\forall x(P\Rightarrow Q))}$و${\displaystyle (\exists xP)Q}$بمعنى${\displaystyle (\exists x(P\wedge Q))}$نحتاج أولاً إلى تعريف كتل المُكمِّمات (QB)، وكتلة المُكمِّمات هي قائمة${\displaystyle (Q_{1}x_{1},\phi _{1})...(Q_{k}x_{k},\phi _{k})}$حيث${\displaystyle \phi _{i}}$s هي صيغ FO خالية من المحددات الكمية و${\displaystyle Q_{i}}$إما أن تكون s${\displaystyle \forall }$أو${\displaystyle \exists }$إذا كانت Q عبارة عن كتلة مُكمِّمات، فسنسميها${\displaystyle [Q]^{t(n)}}$عامل التكرار، والذي يُعرَّف على أنه Q مكتوب${\displaystyle t(n)}$الوقت. ينبغي على المرء أن ينتبه إلى أن هناك هنا${\displaystyle k*t(n)}$المحددات الكمية في القائمة، ولكن يتم استخدام k متغير فقط، ويتم استخدام كل متغير من هذه المتغيرات.${\displaystyle t(n)}$مرات. ^{[ 14 ]}

يمكننا الآن تحديد${\displaystyle {\mathsf {FO}}[t(n)]}$أن تكون صيغ FO مع عامل تكرار يكون أسه في الفئة${\displaystyle t(n)}$ونحصل على المعادلات التالية:

• ${\displaystyle {\mathsf {FO}}[(\log n)^{i}]}$يساوي AC ⁱ المنتظم من الدرجة الأولى ، وفي الواقع${\displaystyle {\mathsf {FO}}[t(n)]}$هو تيار متردد منتظم من العمق${\displaystyle t(n)}$[ ^{15 ]​}
• ${\displaystyle {\mathsf {FO}}[(\log n)^{O(1)}]}$يساوي NC. ^{[ 16 ]}
• ${\displaystyle {\mathsf {FO}}[n^{O(1)}]}$يساوي PTIME . وهو أيضاً طريقة أخرى لكتابة FO(IFP). ^{[ 17 ]}
• ${\displaystyle {\mathsf {FO}}[2^{n^{O(1)}}]}$يساوي PSPACE . وهي أيضًا طريقة أخرى لكتابة FO(PFP). ^{[ 18 ]}

• إبنجهاوس، هاينز ديتر؛ فلوم، يورغ (1999). نظرية النموذج المحدود . وجهات نظر في المنطق الرياضي (2  ed.). سبرينغر. دوى : 10.1007/978-3-662-03182-7 . رقم ISBN 978-3-662-03184-1.
• نيل، إيمرمان (1999). التعقيد الوصفي . سبرينغر. ISBN 0-387-98600-6. OCLC 901297152 .