حساب التفاضل والتكامل الموضعي μ

في علم الحاسوب النظري ، يعتبر حساب μ الموجه ( Lμ ، Lμ _، أو حساب mu الافتراضي ^{[ 1 ]} ، وأحيانًا حساب μ فقط ، على الرغم من أن هذا يمكن أن يكون له معنى أكثر عمومية ) امتدادًا للمنطق الموجه الافتراضي (مع العديد من الوسائط ) عن طريق إضافة عامل النقطة الثابتة الأصغر μ وعامل النقطة الثابتة الأكبر ν، وبالتالي منطق النقطة الثابتة .

يعود أصل حساب μ (الافتراضي، الموجه) إلى دانا سكوت وجاكو دي باكر ، ^{[ 2 ]} وقد طوّره ديكستر كوزين ^{[ 3 ]} إلى النسخة الأكثر استخدامًا اليوم. يُستخدم هذا الحساب لوصف خصائص أنظمة الانتقال المُصنّفة وللتحقق من هذه الخصائص. يمكن ترميز العديد من المنطق الزمني في حساب μ، بما في ذلك CTL* وأجزائه واسعة الاستخدام - المنطق الزمني الخطي ومنطق الشجرة الحسابي . ^{[ 4 ]}

يتمثل المنظور الجبري في اعتباره جبرًا للدوال الرتيبة على شبكة كاملة ، مع مؤثرات تتألف من التركيب الوظيفي بالإضافة إلى مؤثرات النقطة الثابتة الصغرى والكبرى؛ ومن هذا المنظور، فإن حساب μ-النمطي يكون على شبكة جبر مجموعة القوى . ^{[ 5 ]} ترتبط دلالات اللعبة لحساب μ-النمطي بألعاب اللاعبين ذات المعلومات الكاملة ، ولا سيما ألعاب التكافؤ اللانهائي . ^{[ 6 ]}

ليكن P (القضايا) و A (الأفعال) مجموعتين منتهيتين من الرموز، وليكن Var مجموعة متغيرات قابلة للعد. تُعرَّف مجموعة صيغ حساب μ (القضايا، الموجه) كما يلي:

• كل اقتراح وكل متغير عبارة عن صيغة؛
• لو${\displaystyle \phi }$و${\displaystyle \psi }$إذا كانت صيغًا،${\displaystyle \phi \wedge \psi }$هي صيغة رياضية؛
• لو${\displaystyle \phi }$إذا كانت صيغة،${\displaystyle \neg \phi }$هي صيغة رياضية؛
• لو${\displaystyle \phi }$هي صيغة و${\displaystyle a}$إذا كان فعلًا،${\displaystyle [a]\phi }$هي صيغة رياضية؛ (تُنطق إما:${\displaystyle a}$صندوق${\displaystyle \phi }$أو خطة${\displaystyle a}$بالضرورة${\displaystyle \phi }$)
• لو${\displaystyle \phi }$هي صيغة و${\displaystyle Z}$متغير، إذن${\displaystyle \nu Z.\phi }$هي صيغة، بشرط أن يكون كل ظهور حر لـ${\displaystyle Z}$في${\displaystyle \phi }$يحدث بشكل إيجابي، أي ضمن نطاق عدد زوجي من النفي.

(تبقى مفاهيم المتغيرات الحرة والمقيدة كما هي، حيث${\displaystyle \nu }$(هو عامل الربط الوحيد.)

بناءً على التعريفات المذكورة أعلاه، يمكننا إثراء الصيغة بما يلي:

• ${\displaystyle \phi \lor \psi }$معنى${\displaystyle \neg (\neg \phi \land \neg \psi )}$
• ${\displaystyle \langle a\rangle \phi }$(يُنطق إما:${\displaystyle a}$الماس${\displaystyle \phi }$أو خطة${\displaystyle a}$ربما${\displaystyle \phi }$) معنى${\displaystyle \neg [a]\neg \phi }$
• ${\displaystyle \mu Z.\phi }$وسائل${\displaystyle \neg \nu Z.\neg \phi [Z:=\neg Z]}$، أين${\displaystyle \phi [Z:=\neg Z]}$يعني الاستبدال${\displaystyle \neg Z}$ل${\displaystyle Z}$في جميع الحالات المجانية لـ${\displaystyle Z}$في${\displaystyle \phi }$.

الصيغتان الأوليان هما الصيغتان المألوفتان من حساب القضايا الكلاسيكي والمنطق متعدد الوسائط الأدنى K على التوالي .

الترميز${\displaystyle \mu Z.\phi }$(ومكافئها) مستوحاة من حساب التفاضل والتكامل لامدا ؛ والهدف هو الإشارة إلى أصغر (وأكبر) نقطة ثابتة للتعبير${\displaystyle \phi }$حيث يكون "التقليل" (و"التعظيم" على التوالي) في المتغير${\displaystyle Z}$يشبه إلى حد كبير حساب التفاضل والتكامل لامدا${\displaystyle \lambda Z.\phi }$هي دالة ذات صيغة${\displaystyle \phi }$متغير مقيد${\displaystyle Z}$; ^{[ 7 ]} انظر إلى الدلالات الدلالية أدناه لمزيد من التفاصيل.

تُقدَّم نماذج حساب التفاضل والتكامل (الافتراضي) μ كأنظمة انتقال مُصنَّفة${\displaystyle (S,R,V)}$أين:

• ${\displaystyle S}$هي مجموعة من الحالات؛
• ${\displaystyle R}$خريطة لكل تسمية${\displaystyle a}$علاقة ثنائية على${\displaystyle S}$؛
• ${\displaystyle V:P\to 2^{S}}$، يرسم كل اقتراح${\displaystyle p\in P}$إلى مجموعة الحالات التي تكون فيها القضية صحيحة.

بالنظر إلى نظام انتقالي مصنف${\displaystyle (S,R,V)}$وتفسير${\displaystyle i}$من المتغيرات${\displaystyle Z}$التابع${\displaystyle \mu }$- حساب التفاضل والتكامل،${\displaystyle [\![\cdot ]\!]_{i}:\phi \to 2^{S}}$، هي الدالة المحددة بالقواعد التالية:

• ${\displaystyle [\![p]\!]_{i}=V(p)}$؛
• ${\displaystyle [\![Z]\!]_{i}=i(Z)}$؛
• ${\displaystyle [\![\phi \wedge \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cap [\![\psi ]\!]_{i}}$؛
• ${\displaystyle [\![\neg \phi ]\!]_{i}=S\smallsetminus [\![\phi ]\!]_{i}}$؛
• ${\displaystyle [\![[a]\phi ]\!]_{i}=\{s\in S\mid \forall t\in S,(s,t)\in R_{a}\rightarrow t\in [\![\phi ]\!]_{i}\}}$؛
• ${\displaystyle [\![\nu Z.\phi ]\!]_{i}=\bigcup \{T\subseteq S\mid T\subseteq [\![\phi ]\!]_{i[Z:=T]}\}}$، أين${\displaystyle i[Z:=T]}$خرائط${\displaystyle Z}$ل${\displaystyle T}$مع الحفاظ على خرائط${\displaystyle i}$في كل مكان آخر.

وبموجب مبدأ الازدواجية، يكون تفسير الصيغ الأساسية الأخرى كما يلي:

• ${\displaystyle [\![\phi \vee \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cup [\![\psi ]\!]_{i}}$؛
• ${\displaystyle [\![\langle a\rangle \phi ]\!]_{i}=\{s\in S\mid \exists t\in S,(s,t)\in R_{a}\wedge t\in [\![\phi ]\!]_{i}\}}$؛
• ${\displaystyle [\![\mu Z.\phi ]\!]_{i}=\bigcap \{T\subseteq S\mid [\![\phi ]\!]_{i[Z:=T]}\subseteq T\}}$

بصورة أقل رسمية، هذا يعني أنه بالنسبة لنظام انتقال معين${\displaystyle (S,R,V)}$:

• ${\displaystyle p}$ينطبق في مجموعة الولايات${\displaystyle V(p)}$؛
• ${\displaystyle \phi \wedge \psi }$يسري هذا في كل ولاية حيث${\displaystyle \phi }$و${\displaystyle \psi }$كلاهما صحيح؛
• ${\displaystyle \neg \phi }$يسري هذا في كل ولاية حيث${\displaystyle \phi }$هذا غير صحيح.
• ${\displaystyle [a]\phi }$يُعقد في ولاية${\displaystyle s}$إذا كان كل${\displaystyle a}$- الانتقال المؤدي إلى الخروج من${\displaystyle s}$يؤدي إلى حالة حيث${\displaystyle \phi }$يحجز.
• ${\displaystyle \langle a\rangle \phi }$يُعقد في ولاية${\displaystyle s}$إذا كان هناك${\displaystyle a}$- الانتقال المؤدي إلى الخروج من${\displaystyle s}$وهذا يؤدي إلى حالة حيث${\displaystyle \phi }$يحجز.
• ${\displaystyle \nu Z.\phi }$ينطبق في أي حالة في أي مجموعة${\displaystyle T}$بحيث عندما يكون المتغير${\displaystyle Z}$تم ضبطه على${\displaystyle T}$، ثم${\displaystyle \phi }$يحجز للجميع${\displaystyle T}$(يستنتج من نظرية كناستر-تارسكي ما يلي:${\displaystyle [\![\nu Z.\phi ]\!]_{i}}$هي أكبر نقطة ثابتة لـ${\displaystyle T\mapsto [\![\phi ]\!]_{i[Z:=T]}}$، و${\displaystyle [\![\mu Z.\phi ]\!]_{i}}$(أدنى نقطة ثابتة لها .)

تفسيرات${\displaystyle [a]\phi }$و ${\displaystyle \langle a\rangle \phi }$هي في الواقع تلك "الكلاسيكية" من المنطق الديناميكي . بالإضافة إلى ذلك، فإن العامل${\displaystyle \mu }$يمكن تفسيرها على أنها حيوية ("سيحدث شيء جيد في النهاية") و${\displaystyle \nu }$باعتبارها أمانًا ("لا يحدث شيء سيء على الإطلاق") في تصنيف ليزلي لامبورت غير الرسمي. ^{[ 8 ]}

تُعدّ مسألة إمكانية إرضاء صيغة حساب التفاضل والتكامل المشروط (μ-calculus) مسألة كاملة من فئة EXPTIME . ^{[ 11 ]} وكما هو الحال في المنطق الزمني الخطي، ^{[ 12 ]} فإنّ مسائل التحقق من النموذج ، وإمكانية الإرضاء، والصحة في حساب التفاضل والتكامل المشروط الخطي تُعدّ مسائل كاملة من فئة PSPACE . ^{[ 13 ]}

في الواقع، فإن تعقيد مسألة قابلية الإرضاء في حساب التفاضل والتكامل الموجه المتدرج هو أيضًا مسألة كاملة من حيث الوقت، حتى لو كُتب العدد في الوسائط بالنظام الثنائي (حساب التفاضل والتكامل الموجه المتدرج هو امتداد لحساب التفاضل والتكامل الموجه القياسي مع الوسائط "يوجد على الأقل k من الخلفاء بحيث ..."). ^{[ 14 ]}

تذكر أن المنطق الموجه يمكن ترجمته إلى منطق الرتبة الأولى (FO) عبر الترجمة القياسية المشار إليها بـ${\displaystyle ST}$ويتم فهرستها بواسطة متغير من الدرجة الأولى${\displaystyle x}$للدلالة على الحالة الحالية:

${\displaystyle {\begin{aligned}ST_{x}(p)&:=p(x)\\ST_{x}(\lnot \phi )&:=\lnot ST_{x}(\phi )\\ST_{x}(\phi \land \psi )&:=ST_{x}(\phi )\land ST_{y}(\psi )\\ST_{x}([a]\phi )&:=\forall y,xR_{a}y\rightarrow ST_{y}(\phi )\end{aligned}}}$

تذكر أن منطق الرتبة الثانية الأحادي (MSO) يوسع منطق الرتبة الأولى (FO) ليشمل التكميمات من الرتبة الثانية على المجموعات الجزئية. ويمكن ترجمته إلى حساب التفاضل والتكامل (μ-calculus) الذي يمكن ترجمته إلى منطق الرتبة الثانية الأحادي بإضافة قواعد الترجمة التالية لمعاملات النقطة الثابتة ^{[ 15 ]} :

${\displaystyle {\begin{aligned}ST_{x}(\mu X.\phi )&:=\forall X,(\forall y,ST_{y}(\phi )\rightarrow y\in X)\rightarrow x\in X)\\ST_{x}(\nu X.\phi )&:=\exists X,(\forall y,y\in X\rightarrow ST_{y}(\phi ))\land x\in X)\end{aligned}}}$

أثبت جانين ووالوكيفيتش في عام 1996 أن أي صيغة من الدرجة الثانية الأحادية التي تكون ثابتة بواسطة التماثل الثنائي تعادل صيغة حسابية مو ^{[ 1 ]} .

• نظرية النموذج المحدود
• حساب التفاضل والتكامل الموضعي الخالي من التناوب

• كلارك، إدموند م. الابن؛ أورنا غرومبيرغ؛ دورون أ. بيليد (1999). التحقق من النماذج . كامبريدج، ماساتشوستس، الولايات المتحدة الأمريكية: مطبعة معهد ماساتشوستس للتكنولوجيا. ISBN 0-262-03270-8.، الفصل 7، التحقق من النموذج لحساب التفاضل والتكامل μ، الصفحات  97-108
• ستيرلينغ، كولين. (2001). الخصائص النمطية والزمنية للعمليات . نيويورك، برلين، هايدلبرغ: سبرينغر فيرلاغ. ISBN 0-387-98717-7.، الفصل 5، حساب التفاضل والتكامل المشروط، الصفحات من  103 إلى 128
• أندريه أرنولد؛ داميان نيوينسكي (2001). أساسيات μ-حساب التفاضل والتكامل . إلسفير. رقم ISBN 978-0-444-50620-7. يتناول الفصل السادس، بعنوان "حساب التفاضل والتكامل μ على جبر مجموعات القوى"، الصفحات 141-153، حساب التفاضل والتكامل μ الموجه.
• محاضرات يدي فينيما (2008) حول حساب التفاضل والتكامل الموجه μ ؛ عُرضت في المدرسة الصيفية الأوروبية الثامنة عشرة في المنطق واللغة والمعلومات
• برادفيلد، جوليان وستيرلينغ، كولين (2006). "حسابات ميو المشروطة" . في: ب. بلاكبيرن؛ ج. فان بنثام و ف. وولتر (محررون). دليل المنطق المشروط . إلسيفير . ص 721-756 . 
• إيمرسون، إي. ألين (1996). "التحقق من النموذج وحساب ميو". التعقيد الوصفي والنماذج المحدودة . الجمعية الرياضية الأمريكية . ص 185-214 . ISBN  0-8218-0517-7.
• كوزين، ديكستر (1983). "نتائج حول حساب μ الافتراضي". علوم الحاسوب النظرية . 27 (3): 333-354 . doi : 10.1016/0304-3975(82)90125-6 .

• صوفي بينشينات، تسجيل فيديو لمحاضرة في مدرسة ANU الصيفية للمنطق 2009، بعنوان " المنطق، الأوتوماتا، والألعاب".