💻 computer science

Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

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

المؤلفون الأصليون: Sohei Ito, Makoto Tatsuta

نُشر 2026-03-20

📖 5 دقيقة قراءة🧠 قراءة متعمّقة

CC BY 4.0

المؤلفون الأصليون: Sohei Ito, Makoto Tatsuta

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

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

المؤشر: وسيلة لقول "هذا الصندوق يحتوي على ذلك الرقم".
الصفر: الرقم 0.
زر "التالي": وسيلة لقول "الرقم الذي يلي هذا الرقم".

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

إليك قصة كيف استطاع مؤلفا الورقة، سوهي إيتو وماكوتو تاتسوتا، تنفيذ هذه الخدعة السحرية.

الإعداد: غرفة الذاكرة

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

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

ثم أضافوا الأرقام: 0 و التالي (الذي يحول 0 إلى 1، و1 إلى 2، وهكذا).

الخدعة: بناء "ورقة غش" في الغرفة

السؤال الكبير هو: كيف تقوم بعمليات حسابية مثل $2 + 2 = 4$ أو $5 \times 3 = 15$ إذا لم يكن لديك علامة زائد أو علامة ضرب؟

حل المؤلفين كان عبقرياً: لا تحسب الرياضيات؛ بل ابحث عنها.

تخيل أن لديك جداراً ضخماً من الصناديخ اللانهائية في غرفة الذاكرة الخاصة بك. قررت استخدام هذا الجدار كـ ورقة غش (أو جدول بحث).

إذا كنت تريد معرفة $2 + 3$ ، فأنت لا تجمعهما. بل تذهب إلى مكان محدد على الجدار مكتوب عليه "الجمع"، وتجد الصف الخاص بـ 2 و3، وتقرأ الإجابة المكتوبة هناك.
إذا كنت تريد معرفة ما إذا كان $5 \le 10$ ، تذهب إلى قسم "عدم التساوي" على الجدار وتتحقق مما إذا كانت الإجابة مكتوبة هناك.

أثبت المؤلفان أنه على الرغم من صغر حجم هذا المنطق، يمكنك إجبار "غرفة الذاكرة" على بناء ورقة الغش الكاملة هذه من أجلك. يمكن للمنطق أن يقول: "إذا كان الجدار يحتوي على صندوق يقول إن جمع 2 و3 يساوي 5، فإنني أقبل بأن 2+3=5".

من خلال بناء هذه الجداول داخل الذاكرة، يمكن لهذا المنطق الصغير محاكاة حساب بيانو (Peano Arithmetic) (الرياضيات القياسية التي نتعلمها في المدرسة).

النتيجة الكبيرة: لغز "غير قابل للتقرير"

في علوم الكمبيوتر، هناك مسألة شهيرة تسمى مسألة التوقف (Halting Problem). وهي تسأل: "هل يمكننا كتابة برنامج ينظر إلى أي برنامج آخر ويخبرنا ما إذا كان سيعمل للأبد أم سيتوقف؟". الإجابة هي لا. إنه أمر مستحيل التقرير.

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

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

المأخذ: الأمر يعمل في اتجاه واحد فقط

تشير الورقة أيضاً إلى قيد مضحك. خدعة "ورقة الغش" هذه تعمل بشكل مثالي للأسئلة التي تبدأ بـ "لكل الأرقام..." (مثل "لكل الأرقام، $x+0=x$ "). وهذا يسمى صيغة $\Pi^0_1$ .

ومع ذلك، إذا سألت سؤالاً يبدأ بـ "يوجد رقم..." (مثل "يوجد رقم $x$ بحيث $x+0 \neq x$ ")، فإن الخدعة تفشل.

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

استراتيجية "الإثبات المزدوج"

لم يعتمد المؤلفان على طريقة واحدة فقط. لقد استخدما طريقتين مختلفتين لإثبات وجهة نظرهما، مثل عرض خدعة سحرية من زاويتين مختلفتين:

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

لماذا يجب أن تهتم؟

هذه الورقة مهمة لسببين:

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

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

إليك ملخص تقني مفصل للورقة البحثية بعنوان "ترميز حساب بيانو في جزء أدنى من منطق الفصل" (Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic) للباحثين سوهي إيتو وماكوتو تاتسوتا.

1. بيان المشكلة

تتناول الورقة البحثية مسألة القرار (decidability) الجوهرية في منطق الفصل (Separation Logic - SL) عند توسيعه بالعمليات الحسابية. وبينما يُستخدم منطق الفصل على نطاق واسع للتحقق من البرامج التي تتعامل مع الذاكرة (heap)، يُفترض غالبًا أن الجمع بين منطق الفصل ونظريات حسابية (مثل حساب بريسر) يحافظ على خاصية القرار إذا كان الجزء الحسابي قابلًا للقرار.

يبحث المؤلفان في جزء أدنى من منطق الفصل مع الأعداد (SLN)، والذي يتم تعريفه كالتالي:

المكون المكاني: فقط مسند "الإشارة إلى" الحدسي ( $t_1 \to t_2$ )، والذي يمثل خلية ذاكرة واحدة.
المكون الحسابي: فقط الثابت $0$ ودالة التابع (successor) $s$ .
الاستثناءات: يستبعد هذا الجزء صراحةً عملية "الاقتران الفاصل" ( $*$ )، و"العصا السحرية" ( $-\ast$ )، ومسندات "الإشارة إلى" متعددة الحقول.

تتمثل المشكلة الأساسية في تحديد القدرة التعبيرية لهذا الجزء الضعيف للغاية. وتحديدًا، يتساءل المؤلفان: هل يمكن لهذا الجزء الأدنى ترميز صيغ $\Pi^0_1$ غير القابلة للقرار في حساب بيانو (PA)؟

2. المنهجية

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

أ. جداول العمليات القائمة على الذاكرة (Heap-Based Operation Tables)

الابتكار الأساسي هو ترميز العمليات الحسابية (الجمع، الضرب، وعدم المساواة) مباشرة في بنية الذاكرة (heap). فبدلاً من وجود معاملات حسابية مدمجة، يقوم المنطق بمحاكاة هذه العمليات باستخدام جداول عمليات مخزنة في خلايا ذاكرة مرتبطة.

مخطط الترميز: تخزن الذاكرة المدخلات في شكل خلايا متتالية.
- الجمع: موسوم بالرمز 0. يتم تخزين مدخل لـ $x + y = z$ كسلسلة من الخلايا تبدأ من العنوان $a$ : $(0, x+3, y+3, z+3)$ . الإزاحة $+3$ تمنع التصادم مع الوسوم (tags).
- الضرب: موسوم بالرمز 1. المدخل: $(1, x+3, y+3, z+3)$ .
- عدم المساواة: موسوم بالرمز 2. المدخل: $(2, x+3, y+3)$ .
قيود الاتساق: يتم بناء صيغة محددة $H$ (شرط جدول الذاكرة) لفرض أنه إذا كانت الذاكرة تحتوي على مدخل لعملية ما، فإن الخلايا اللاحقة يجب أن تحتوي على النتيجة الصحيحة بناءً على التعريفات الاستقرائية (على سبيل المثال، $s(x) + y = s(x+y)$ ).

ب. ترجمة صيغ $\Pi^0_1$

يعرّف المؤلفان عملية ترجمة $(\cdot)^\circ$ من الصيغ المحدودة في حساب بيانو (PA) إلى SLN.

الشكل الطبيعي: يقومون أولاً بتحويل صيغ PA إلى "شكل طبيعي" حيث تظهر العمليات الحسابية ( $+, \times$ ) فقط ضمن المكممات الوجودية من الشكل $\exists(x = t + u)$ .
منطق الترجمة:
- تُستبدل الحدود الحسابية بمراجع لجداول العمليات (على سبيل المثال، $x + y = z$ تصبح $\forall a ((a \to 0, [x], [y]) \to s^3(a) \to [z])$ ).
- التعامل مع الذاكرات المحدودة: التحدي الحرج هو أن الذاكرة محدودة وقد لا تحتوي على مدخلات للأرقام الكبيرة. تعالج الترجمة ذلك باستخدام الاستلزامات: إذا كانت الذاكرة "صغيرة جدًا" بحيث لا تحتوي على مدخل الجدول المطلوب، فإن الاستلزام يكون صحيحًا بالضرورة (vacuously true). يضمن هذا أن الصلاحية في SLN (التي تتطلب الصدق لجميع حالات الذاكرة) تتوافق مع الصلاحية في PA (النموذج القياسي).
- وتحديدًا، بالنسبة للمكممات المحدودة $\exists x \le t$ ، تتضمن الترجمة انفصالًا (disjunction): إما أن تكون الذاكرة صغيرة جدًا للتحقق من الحد، أو أن الذاكرة تحتوي على مدخلات الجدول اللازمة للتحقق من الحد.

ج. تحليل التعقيد

لتحديد فئة التعقيد بدقة، يثبت المؤلفان اتجاهين:

الحد الأدنى ( $\Pi^0_1$ -hard): من خلال إظهار أن الترجمة تحافظ على الصلاحية لصيغ $\Pi^0_1$ .
الحد الأعلى ( $\Pi^0_1$ ): من خلال إثبات أن مشكلة التحقق من النموذج (model-checking problem) لـ SLN هي مسألة قابلة للقرار. حيث يوضحون أن المتغيرات في مسند "الإشارة إلى" يمكن حصرها بحجم الذاكرة، مما يقلل المشكلة إلى التحقق من جزء قابل للقرار من حساب التابع (وهو جزء فرعي من حساب بريسر).

3. المساهمات الرئيسية

عدم قابلية القرار لـ SLN الأدنى: تثبت الورقة أن الصلاحية في SLN غير قابلة للقرار. وهذا أمر مفاجئ لأن الجزء يحتوي فقط على أبسط مسند مكاني وأضعف حساب (التابع فقط)، ومع ذلك فهو قوي بما يكفي لمحاكاة حساب بيانو الكامل لصيغ $\Pi^0_1$ .
مبرهنة التمثيل: تم تقديم ترجمة دقيقة تظهر أن صيغة $\Pi^0_1$ (المسماة $A$ ) تكون صالحة في PA إذا وفقط إذا كانت ترجمتها $A^\circ$ صالحة في SLN.
الاكتمال لـ $\Pi^0_1$ : يثبت المؤلفون أن مشكلة الصلاحية لـ SLN هي $\Pi^0_1$ -complete. وهذه نتيجة هامة لأنها تحدد موقع تعقيد المنطق بدقة ضمن التسلسل الحسابي.
القصور في $\Sigma^0_1$ : توضح الورقة أن الترجمة لا تحافظ على الصلاحية لصيغ $\Sigma^0_1$ . تم تقديم مثال مضاد ( $\exists x (x + 0 \neq x)$ )، يوضح أنه بينما تكون الصيغة خاطئة في PA، فإن ترجمتها تكون صالحة في SLN لأن الذاكرات "الصغيرة" يمكنها استيفاء الشرط تلقائيًا بسبب افتقارها لمدخلات الجدول اللازمة.
برهان بديل: تم تقديم برهان بديل لعدم قابلية القرار عبر الاختزال من مشكلة الصلاحية في نظرية النماذج المحدودة (مبرهنة تراكنبروت)، من خلال ترميز البنى المحدودة في الذاكرات.

4. النتائج

المبرهنة الرئيسية: صلاحية صيغ $\Pi^0_1$ في حساب بيانو تكافئ صلاحية ترجماتها في الجزء الأدنى من SLN.
النتيجة المترتبة: مشكلة الصلاحية لـ SLN غير قابلة للقرار.
التعقيد: مشكلة الصلاحية هي $\Pi^0_1$ $Π_{1}^{0}$ -complete.
- الشدة (Hardness): مستمدة من ترميز PA.
- العضوية (Membership): مستمدة من قابلية قرار مشكلة التحقق من النموذج (المتغيرات في الذرات المكانية محدودة بحجم الذاكرة؛ والمنطق المتبقي هو حساب تابع قابل للقرار).

5. الأهمية

الحدود النظرية: تعيد هذه النتائج تعريف الحدود بين الأجزاء القابلة للقرار وغير القابلة للقرار لمنطق الفصل. فهي تظهر أن إضافة أبسط العمليات الحسابية (0 والتابع) إلى جزء مكاني أدنى كافٍ لكسر قابلية القرار، بشرط أن يسمح المنطق بالتكميم فوق الذاكرات.
الآثار على التحقق: بالنسبة للتحقق من البرامج، يعني هذا أن أدوات الاستدلال الآلي لمنطق الفصل مع الأعداد يجب أن تكون حذرة. فحتى لو كان الجزء المكاني مقتصرًا على مؤشرات الخلية الواحدة، فإن الجمع مع الحساب يمكن أن يؤدي إلى عدم قابلية القرار، مما يستلزم استخدام الاستدلالات التجريبية (heuristics) أو أجزاء مقيدة (مثل الذاكرات الرمزية ذات التعريفات الاستقرائية المحددة) للأدوات العملية.
القدرة التعبيرية: تسلط الورقة الضوء على أن الطبيعة "الحدسية" لمسند "الإشارة إلى" (التي تسمح بوجود ذاكرات جزئية) مع القيود الحسابية كافية لترميز عمليات حسابية معقدة، مما يتحدى الاعتقاد بأن الاقتران الفاصل ( $*$ ) ضروري للقدرة التعبيرية العالية في SL.

باختصار، يثبت إيتو وتاتسوتا أن البساطة التركيبية لا تضمن قابلية القرار في منطق الفصل. فالجزء الذي يحتوي فقط على مسند مكاني واحد وحساب أساسي كافٍ لترميز خصائص الاتساق والإنهاء للأنظمة المنطقية، مما يضع مشكلة الصلاحية عند مستوى $\Pi^0_1$ -completeness.