Nonlinear Arithmetic with SMTLIB Division is Undecidable

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

هذه الورقة البحثية تتحدث عن مجموعة محددة من القواعد تسمى الحساب الحقيقي غير الخطي (NRA). فكر في هذا كأنه لعبة تُلعَب باستخدام الأعداد الحقيقية (مثل 3.14، أو -5، أو 0.001) حيث يمكنك الجمع، والطرح، والضرب، والقسمة.

القاعدة "السحرية" التي تكسر اللعبة

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

ومع ذلك، اكتشف المؤلف، ديجان جوفانوفيتش (Dejan Jovanović)، فخاً مخفياً في كتاب القواعد الرسمي (معيار SMTLIB). هذا الفخ يكمن في كيفية تعامل القواعد مع القسمة على صفر.

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

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

كيف يجعل هذا اللعبة غير قابلة للحل

تجادل الورقة بأن قاعدة "أي شيء يذهب" هذه المتعلقة بالقسمة على صفر هي المفتاح الذي يفتح باباً للفوضى.

إليك المنطق، بشكل مبسط:

1. الهدف: يريد المؤلف إثبات أنه إذا كنت تملك هذه القاعدة السحرية للقسمة على صفر، يمكنك خداع الحاسوب لحل ألغاز الأعداد الصحيحة (ألغاز تستخدم الأعداد الكاملة مثل 1، 2، 3).
2. المشكلة: حل ألغاز الأعداد الصحيحة هو أمر مستحيل تقنياً للحواسيب في جميع الحالات (وهذا ما يُعرف بمسألة هيلبرت العاشرة). الأمر يشبه محاولة العثور على إبرة في كومة قش تنمو إلى ما لا نهاية.
3. الخدعة: يوضح المؤلف أنه باستخدام هذه القسمة السحرية على صفر، يمكنك بناء جسر رياضي. يمكنك أخذ لغز صعب للأعداد الصحيحة وترجمته إلى لغز أعداد حقيقية باستخدام خدعة القسمة هذه.
   • التشبيه: تخيل أن لديك شفرة سرية مكتوبة بلغة يفهمها البشر فقط (الأعداد الصحيحة). أنت تبني آلة (خدعة القسمة) تترجم هذه الشفرة إلى لغة تفهمها الحواسيب (الأعداد الحقيقية). ولأن لغة الحاسوب تحتوي على قاعدة "القسمة على صفر السحرية"، يمكن للحاسوب أن يحل بالخطأ الشفرة البشرية.
4. النتيجة: بما أننا نعلم أن الحواسيب لا يمكنها حل جميع ألغاز الأعداد الصحيحة، وبما أن هذه الخدعة تسمح لها بمحاولة حل ألغاز الأعداد الصحيحة باستخدام الأعداد الحقيقية، فهذا يعني أن الحاسوب لا يمكنه حل جميع ألغاز الأعداد الحقيقية أيضاً. تصبح اللعبة غير قابلة للتقرير (undecidable).

تشبيه دالة "الأرضية" (Floor Function)

لإثبات ذلك، يستخدم المؤلف خدعة ذكية. يوضح أنه إذا كان لديك هذه القسمة السحرية، يمكنك إجبار الحاسوب على التصرف مثل دالة الأرضية (الدالة التي تقرب الرقم لأسفل إلى أقرب عدد صحيح، مثل تحويل 3.9 إلى 3).

بمجرد أن يتمكن الحاسوب من تقريب الأرقام لأسفل، يمكنه البدء في عد الأعداد الصحيحة. وبمجرد أن يتمكن من عد الأعداد الصحيحة، يمكنه محاولة حل تلك الألغاز المستحيلة للأعداد الصحيحة. وبما أن هذه الألغاز مستحيلة الحل بشكل عام، فإن النظام بأكمله للحساب الحقيقي مع قاعدة القسمة هذه يصبح مستحيلاً للحل بشكل عام.

ماذا يعني هذا بالنسبة للعالم الحقيقي (وفقاً للورقة)

لا تتحدث الورقة عن استخدامات الذكاء الاصطناعي المستقبلي أو الاستخدامات الطبية. بل تركز على الحالة الراهنة لمعايير الحاسوب (المسائل الاختبارية):

• الفخ: العديد من المسائل الاختبارية الموجودة في مكتبة SMTLIB (وهي مجموعة ضخمة من الألغاز الرياضية المستخدمة لاختبار الحواسيب) تستخدم القسمة مع المتغيرات (مثل x / y). إذا كانت y تساوي صفراً، فإن هذه المسائل تقع في فخ "عدم القدرة على التقرير".
• الحل؟ يقترح المؤلف طريقتين لإصلاح كتاب القواعد:
  1. اختيار إجابة محددة: تحديد أن القسمة على صفر تساوي دائماً رقماً معيناً (مثل 0 أو 1)، تماماً كما تتعامل بعض أنظمة الحاسوب مع الأرقام الثنائية.
  2. تقسيم اللعبة: إنشاء فئة جديدة ومنفصلة للمسائل التي تقسم فيها على متغيرات، والاحتفاظ بالفئة "الآمنة" للمسائل التي تقسم فيها فقط على أرقام ثابتة معروفة.

الخلاصة

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