منطق من الدرجة الثانية أحادي

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

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

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

المنطق الأحادي من الدرجة الثانية مكافئ تعبيريًا للمنطق الجمعي .

المتغيرات

يأتي منطق الرتبة الثانية الأحادي في شكلين. في الشكل الذي يُدرس على هياكل مثل الرسوم البيانية وفي نظرية كورسيل، قد تتضمن الصيغة ثوابت مسند غير أحادية (في هذه الحالة مسند الحافة الثنائي).هـ(x،y){\displaystyle E(x,y)})، لكن التحديد الكمي يقتصر على متغيرات المسند الأحادي فقط. في الصيغة التي تم تناولها في نظرية الأوتوماتا ونظرية بوشي-إلجوت-تراختنبروت، يجب أن تكون جميع المسندات، الثابتة أو المتغيرة، أحادية، باستثناء المساواة (={\displaystyle =}) والترتيب (<{\displaystyle <}العلاقات.

التعقيد الحسابي للتقييم

المنطق الوجودي الأحادي من الرتبة الثانية (EMSO) هو جزء من المنطق الأحادي من الرتبة الأولى (MSO) حيث يجب أن تكون جميع المُكمِّمات على المجموعات مُكمِّمات وجودية ، خارج أي جزء آخر من الصيغة. أما المُكمِّمات من الرتبة الأولى فهي غير مقيدة. أي، يمكن القول "يوجد x بحيث..." و"لكل x ، لدينا..." حيث x حد، ولكن لا يمكن القول إلا "يوجد محمول أحادي P بحيث..." وليس "لكل محمول أحادي P ، لدينا...".

تنص نظرية فاجين على أن منطق الرتبة الثانية الوجودي (ESO) يجسد بدقة التعقيد الوصفي لفئة التعقيد NP . وبالمثل، تُسمى فئة المسائل التي يمكن التعبير عنها في منطق الرتبة الثانية الوجودي الأحادي NP الأحادي . بعبارة أخرى، يجسد منطق الرتبة الثانية الوجودي الأحادي (EMSO) بدقة التعقيد الوصفي لفئة NP الأحادي (MNP).

في منطق الرسوم البيانية ، يندرج اختبار ما إذا كان الرسم البياني منفصلاً ضمن فئة MNP، حيث يمكن تمثيل الاختبار بصيغة تصف وجود مجموعة جزئية فعلية من الرؤوس لا تربطها أي حواف ببقية الرسم البياني. أما المسألة المكملة، وهي اختبار ما إذا كان الرسم البياني متصلاً، فلا تنتمي إلى فئة NP الأحادية. أي أنها مسألة في co -MNP \ MNP. وبالتناظر، يندرج اختبار فصل الرسم البياني ضمن فئة MNP \ co-MNP، مما يدل على أن أيًا من فئتي التعقيد لا تحتوي الأخرى. [ 2 ] [ 3 ] إن إضافة كلمة "أحادية" تُسهّل المسألة. أما السؤال المماثل، وهو ما إذا كانت NP = co-NP ، فهو سؤال مفتوح في مجال التعقيد الحسابي.

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

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

قابلية الحسم وتعقيد الإرضاء

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

تُعتبر نظرية الرتبة الثانية الأحادية للشجرة الثنائية الكاملة اللانهائية ، والتي تُسمى S2S ، قابلة للتقرير . [ 9 ] ونتيجةً لهذه النتيجة، فإن النظريات التالية قابلة للتقرير:

  • نظرية الأشجار من الدرجة الثانية الأحادية.
  • S1S، نظرية الرتبة الثانية الأحادية ذات التابع الواحد (أي، منشمال{\displaystyle \mathbb {N} })
  • WS2S و WS1S، اللذان يقيدان التحديد الكمي إلى مجموعات فرعية محدودة (منطق أحادي ضعيف من الدرجة الثانية).
    • من خلال ترميز الأعداد الطبيعية ثنائياً كمجموعات جزئية محدودة، يمكن تعريف عملية الجمع حتى في نظام WS1S.

بالنسبة لكل من هذه النظريات (S2S، S1S، WS2S، WS1S)، فإن تعقيد مسألة القرار غير أولي . [ 5 ] [ 6 ] ويمكن الحصول عليها عن طريق اختزال مسألة الفراغ للغات الخالية من النجوم إلى WS1S. [ 10 ] ومن المعروف أن WS1S تحديدًا هي مسألة كاملة من نوع TOWER . [ 11 ]

استخدام قابلية إرضاء MSO على الأشجار في التحقق

تُستخدم منطق الأشجار من الدرجة الثانية الأحادية في التحقق الرسمي . وقد استُخدمت إجراءات القرار الخاصة بإمكانية إرضاء منطق الأشجار من الدرجة الثانية الأحادية [ 12 ] [ 13 ] [ 14 ] لإثبات خصائص البرامج التي تتعامل مع هياكل البيانات المرتبطة ، [ 15 ] كشكل من أشكال تحليل الشكل ، وللاستدلال الرمزي في التحقق من الأجهزة . [ 16 ]

انظر أيضاً

مراجع

  1. ↑ كورسيل، برونو ؛ إنجلفريت، جوست (2012-01-01). بنية الرسم البياني ومنطق الرتبة الثانية الأحادي: مدخل نظري لغوي . مطبعة جامعة كامبريدج. ISBN 978-0521898331تم الاطلاع عليه بتاريخ 15-09-2016 .
  2. ^ فاجين، رونالد (1975)، “الأطياف المعممة الأحادية”، Zeitschrift für Mathematische Logik und Grundlagen der Mathematik ، 21 : 89–96 ، دوى : 10.1002/malq.19750210112 ، السيد 0371623 .
  3. ↑ فاجين، ر.؛ ستوكمير ، ل .؛ فاردي، م.ي. (1993)، "حول NP أحادي مقابل co-NP أحادي"، وقائع المؤتمر السنوي الثامن حول البنية في نظرية التعقيد ، معهد مهندسي الكهرباء والإلكترونيات، doi : 10.1109/sct.1993.336544 ، S2CID 32740047 .
  4. ↑ ثاتشر، جيه دبليو؛ رايت، جيه بي (1968-03-01). "نظرية الأوتوماتا المحدودة المعممة مع تطبيق على مسألة قرار في منطق الرتبة الثانية". نظرية الأنظمة الرياضية . 2 (1): 57-81 . doi : 10.1007/BF01691346 . ISSN 1433-0490 . S2CID 31513761 .  
  5. 1 2 ماير، ألبرت ر. (1975). باريك، روهيت (محرر). "نظرية الرتبة الثانية الأحادية الضعيفة للخلف ليست ابتدائية-استدعائية". ندوة المنطق . محاضرات في الرياضيات. سبرينغر برلين هايدلبرغ: 132-154 . doi : 10.1007/bfb0064872 . ISBN 9783540374831.
  6. 1 2 ستوكمير، لاري؛ ماير، ألبرت ر. (2002-11-01). "الحد الأدنى الكوني لتعقيد الدائرة لمسألة صغيرة في المنطق" . مجلة ACM . 49 (6): 753-784 . doi : 10.1145/602220.602223 . ISSN 0004-5411 . S2CID 15515064 .  
  7. ↑ باغان، غيوم (2006). إسيك، زولتان (محرر). "استعلامات MSO على الهياكل القابلة للتحليل الشجري قابلة للحساب بتأخير خطي". منطق علوم الحاسوب . محاضرات في علوم الحاسوب. 4207. سبرينغر برلين هايدلبرغ: 167-181 . doi : 10.1007/11874683_11 . ISBN 9783540454595.
  8. ^ ارنبورج ، ستيفان. لاجرجرين، ينس؛ انظر ديتليف (1991/06/01). “مشاكل سهلة للرسوم البيانية القابلة للتحلل”. مجلة الخوارزميات . 12 (2): 308–340 . دوى : 10.1016/0196-6774(91)90006-K . ردمك 0196-6774 . 
  9. ↑ رابين، مايكل أو. (1969). "قابلية الحسم لنظريات الرتبة الثانية والآلات على الأشجار اللانهائية" . معاملات الجمعية الرياضية الأمريكية . 141 : 1-35 . doi : 10.2307/1995086 . ISSN 0002-9947 . JSTOR 1995086 .  
  10. ↑ ستوكمير، لاري جوزيف (1974). تعقيد مشاكل القرار في نظرية الأتمتة والمنطق (أطروحة دكتوراه). معهد ماساتشوستس للتكنولوجيا.
  11. ↑ شميتز، سيلفان (2016-02-03). "تسلسلات التعقيد ما وراء المستوى الابتدائي" . معاملات ACM في نظرية الحوسبة . 8 (1): 1-36 . arXiv : 1312.5686 . doi : 10.1145/2858784 . ISSN 1942-3454 . 
  12. ^ هنريكسن، جيسبر جي. جنسن، جاكوب؛ يورجنسن، مايكل. كلارلوند، نيلز. بيج، روبرت؛ راوهي، ثيس؛ ساندهولم، أندرس (1995). برينكسما، إي. كليفلاند، WR؛ لارسن، كغ؛ مارغريا، ت . ستيفن، ب. (محرران). "منى: المنطق الأحادي من الدرجة الثانية في الممارسة العملية" . أدوات وخوارزميات لبناء وتحليل الأنظمة . ملاحظات محاضرة في علوم الكمبيوتر. 1019 . برلين، هايدلبرغ: سبرينغر: 89-110 . دوى : 10.1007 / 3-540-60630-0_5 . رقم ISBN 978-3-540-48509-4.
  13. ^ فيدور، توماس. هوليك، لوكاس؛ لينجال، أوندريج؛ فوينار ، توماس (2019-04-01). "مضادات السلاسل المتداخلة لـ WS1S" . اكتا إنفورماتيكا . 56 (3): 205-228 . دوى : 10.1007 / s00236-018-0331-z . ردمك 1432-0525 . S2CID 57189727 .  
  14. ↑ ترايتل، ديمتري؛ نيبكو، توبياس (25-09-2013). "إجراءات قرار مُدققة لـ MSO على الكلمات بناءً على مشتقات التعبيرات النمطية" . ACM SIGPLAN Notices . 48 (9): 3–f12. doi : 10.1145/2544174.2500612 . hdl : 20.500.11850/106053 . ISSN 0362-1340 . 
  15. ↑ مولر، أندرس؛ شوارتزباخ، مايكل آي. (1 مايو 2001). "محرك منطق تأكيد المؤشر" . وقائع مؤتمر ACM SIGPLAN 2001 حول تصميم لغات البرمجة وتنفيذها . PLDI '01. سنوبيرد، يوتا، الولايات المتحدة الأمريكية: رابطة آلات الحوسبة. الصفحات 221-231 . doi : 10.1145/378795.378851 . ISBN  978-1-58113-414-8. S2CID 11476928 . 
  16. ↑ باسين، ديفيد؛ كلارلوند، نيلز (1998-11-01). "الاستدلال الرمزي القائم على الأوتوماتا في التحقق من الأجهزة" . الأساليب الرسمية في تصميم الأنظمة . 13 (3): 255-288 . doi : 10.1023/A:1008644009416 . ISSN 0925-9856 .