💻 computer science

Fracterm Calculus for Partial Meadows

تقدم هذه الورقة حساب "فراكتيرم" (fracterm) للمروج الجزئية (partial meadows) باستخدام منطق الدائرة القصيرة ثلاثي القيم لتوفير صياغة صورية طبيعية للحقول ذات القسمة، مظهرةً أنه بينما لا يمكن للمنطق التعبير عن الطبيعة غير المعرفة للقسمة على صفر، فإن علاقة استتباعه هي شبه قابلة للحوسبة، وتؤدي توسيعات $\bot$ الخاصة به إلى مروج شائعة.

المؤلفون الأصليون: Jan A. Bergstra, Alban Ponse

نُشر 2026-05-14

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

CC BY 4.0

المؤلفون الأصليون: Jan A. Bergstra, Alban Ponse

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

تخيل أنك تحاول بناء حاسبة مثالية للكون. لقرون، عانى الرياضيون من خلل محدد: القسمة على صفر.

في الرياضيات القياسية، إذا حاولت قسمة 1 على 0، فإن الحاسبة تتعطل. تظهر رسالة "خطأ" (Error). في علوم الحاسوب، يُصنف هذا غالبًا كـ "دالة جزئية" (partial function)—وهي دالة تعمل في معظم الأوقات ولكنها ببساطة ترفض إعطاء إجابة لمدخلات معينة.

هذه الورقة البحثية، التي كتبها يان أ. بيرغسترا وألبان بونس، تقترح طريقة جديدة لكتابة "نظام التشغيل" لحاسبة كهذه. وقد أطلقوا عليها اسم حساب الكسور للمروج الجزئية (Fracterm Calculus for Partial Meadows). إليك تفصيل لأفكارهم باستخدام تشبيهات من الحياة اليومية.

1. المشكلة: الثقب الأسود "غير المعرّف"

في الرياضيات العادية، نفترض أن لكل رقم قيمة. لكن في "المروج الجزئية" (Partial Meadow)، يكون الرقم $\frac{1}{0}$ عبارة عن ثقب أسود؛ فهو غير موجود، وليس له قيمة.

يشير المؤلفان إلى مشكلة منطقية شائكة:

إذا سألت، "هل $\frac{1}{0}$ يساوي $\frac{1}{0}$ ؟"
في المنطق القياسي، ستقول "نعم، إنهما نفس الشيء غير المعرّف".
لكن في هذا النظام الجديد، بما أن $\frac{1}{0}$ ليس له قيمة، فإن السؤال "هل هو يساوي نفسه؟" هو أيضًا سؤال بلا معنى. إنه ليس صحيحًا ولا خاطئًا؛ بل هو غير معرّف (Undefined).

للتعامل مع هذا، قدم المؤلفان منطقًا ثلاثي القيم. فبدلاً من وجود "صحيح" و"خطأ" فقط، أضافا حالة ثالثة: غير معرّف (أو "لا توجد قيمة").

2. الحل: مفتاح "الدائرة القصيرة" (Short-Circuit)

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

التشبيه: مفتاح الضوء
تخيل ممرًا به مفتاحا ضوء متتاليان.

المفتاح أ: "هل الباب مفتوح؟"
المفتاح ب: "هل الضوء يعمل؟"

في نظام منطقي قياسي، تتحقق من كلا المفتاحين لتقرر ما إذا كانت عبارة "الباب مفتوح والضوء يعمل" صحيحة.

في منطق الدائرة القصيرة الخاص بالمؤلفين، أنت تتحقق منهما واحدًا تلو الآخر، من اليسار إلى اليمين.

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

لماذا يهم هذا في الرياضيات؟
تأمل الجملة التالية: "إذا كان $x$ لا يساوي صفرًا، فإن $\frac{x}{x} = 1$ ."

إذا كان $x = 0$ ، فإن الجزء الأول (" $x$ لا يساوي صفرًا") هو خاطئ.
وبسبب منطق "الدائرة القصيرة"، يتوقف النظام عند هذه النقطة. إنه لا يحاول أبدًا حساب $\frac{0}{0}$ .
تُعتبر الجملة تلقائيًا صحيحة (أو صالحة) لأن الشرط لم يتحقق، وبالتالي لم يتم المساس بالجزء الخطير.

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

3. "المروج الجزئية" (The Partial Meadow)

يعرف المؤلفان بنية تسمى المروج الجزئية.

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

4. "الخدعة السحرية": تحويل الثقوب إلى رقم جديد

تستكشف الورقة أيضًا خدعة ذكية لجعل النظام أسهل في الدراسة. لقد قدموا رمزًا نائبًا خاصًا، وهو $\perp$ (يُنطق "أسفل" أو "العنصر الامتصاصي").

التحويل: يأخذون "المروج الجزئية" (ذات الثقوب) ويملأون كل ثقب بهذا الرمز الجديد $\perp$ .
النتيجة: الآن، بدلاً من وجود دالة "لا تعمل"، أصبح لديك دالة تعمل دائمًا، ولكنها أحيانًا تعيد الإجابة الخاصة $\perp$ .
التشبيه: تخيل آلة بيع ذاتي.
- الطريقة القد قديمًا: إذا وضعت عملة مكسورة، ستتعطل الآلة (غير معرّف).
- الطريقة الجديدة: إذا وضعت عملة مكسورة، ستخرج لك الآلة رمز "عملة مكسورة". الآلة لا تتعطل أبدًا؛ بل تعطيك فقط رمزًا محددًا للخطأ.

يثبت المؤلفان أن نسخة "العملة المكسورة" هذه (والتي يسمونها المروج المشتركة أو Common Meadow) مكافئة رياضيًا لنسخة "الثقوب". وهذا أمر قوي لأنه يسمًاح لهم باستخدام أدوات الرياضيات القياسية والمعروفة جيدًا لدراسة هذه الأنظمة الغريبة المليئة بالثقوب.

5. ما يدّعونه فعليًا

تقدم الورقة ثلاثة ادعاءات محددة وملموسة:

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

الملخص

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

ملخص تقني: حساب الكسور (Fracterm Calculus) للمروج الجزئية (Partial Meadows)

بيان المشكلة
تتناول الورقة البحثية الصياغة الرسمية للحساب الأولي الذي يتضمن القسمة، وتحديداً عندما تُعامل القسمة كدالة جزئية (غير معرفة عندما يكون المقام صفراً). غالباً ما تلجأ المقاربات التقليدية إلى جعل القسمة دالة كلية (تعيين قيمة لـ $x/0$ ) أو الاعتماد على المنطق الكلاسيكي ثنائي القيم، وهو ما يواجه صعوبة في التعامل مع تعبيرات مثل $1/0 = 1/0$ دون تعيين قيم حقيقية اصطناعية. يرى المؤلفون أن النهج الجبري الجزئي، حيث يُعتبر $1/0$ مصطلحاً تركيبياً صالحاً ("fracterm") ولكنه يفتقر إلى قيمة، يتطلب إطاراً منطقياً محدداً. وقد اعتُبر منطق "كلي القوة" (strong Kleene) القياسي غير كافٍ لأنه يفتقر إلى خصائص التقييم المتسلسل اللازمة لمنع تقييم التعبيرات الجزئية غير المعرفة (مثل تقييم $3/0$ في التخيير $3/0 = 2 \lor 3 = 3$ ).

المنهجية
يستخدم المؤلفون منطق رتبة أولى ثلاثي القيم، ذو خاصية "التخطي" (short-circuit)، يُرمز له بـ $L_{sfol}(\Sigma)$ ، استناداً إلى المنطق الشرطي ذي التخطي (C $\ell$ SCL). يستخدم هذا المنطق روابط متسلسلة ( $\land_{rb}$ , $\lor_{rb}$ , $\to_{b}$ ) تقوم بتقييم المعاملات من اليسار إلى اليمين، مع تخطي عملية التقييم إذا تم تحديد نتيجة المعامل الأول.

تتقدم المنهجية عبر ثلاث مراحل رئيسية:

التأسيس المنطقي: تُعرف الورقة دلالات هذا المنطق باستخدام دلالات "تارسكي" الاستقرائية للجبر الجزئي. وهي تقدم "المساواة الجزئية" ( $=_{p}$ )، والتي تكون غير معرفة إذا كان أي من الطرفين غير معرف، و"عدم المساواة بالإنكار" ( $\neq_{p}$ ).
الأكسيوماتية (FTC $_{pm}$ ): يقترح المؤلفون "حساب الكسور للمروج الجزئية" (FTC $_{pm}$ )، وهو توصيف للمروج الجزئية (حقول مع عامل قسمة جزئي) باستخدام المنطق المحدد. تشمل الأكسيومات (البديهيات) أكسيومات الحلقات القياسية، وقواعد محددة للمساواة الجزئية (الاستبدال الضعيف)، وأكسيومات القسمة المشروطة بأن يكون المقام غير صفري عبر الاستلزام ذي التخطي.
الترجمة الدلالية (توسعة $\perp$ ): لتحليل القابلية للحوسبة والخصائص النظرية لإثبات هذا المنطق الجزئي، يقدم المؤلفون ترجمة إلى المنطق القياسي للأجزاء الموسعة بـ $\perp$ . حيث تُعرف "توسعة $\perp$ " لجبر جزئي بإضافة عنصر امتصاصي $\perp$ (يمثل "لا قيمة") إلى المجال. وتقوم دالة تحويل $\psi_{true}$ برسم الخرائط من الصيغ المنطقية للمنطق الجزئي إلى صيغ المنطق القياسي فوق التوقيع الموسع.

المساهمات والنتائج الرئيسية

المسوغ للمنطق ذي التخطي: تثبت الورقة أن المنطق ذي التخطي هو النموذج الأكثر طبيعية للمروج الجزئية. وتوضح أن المنطق البديل (مثل منطق كلي القوة) يفشل في منع تقييم المصطلحات غير المعرفة في التخييرات، بينما يتعامل منطق التخطي بشكل طبيعي مع تأكيدات مثل $x \neq_{p} 0 \to_{b} x/x =_{p} 1$ دون محاولة تقييم $0/0$ .
الأكسيوماتية الكاملة (FTC $_{pm}$ ): يقدم المؤلفون أكسيومات كاملة (FTC $_{pm}$ ) لفئة المروج الجزئية. ويثبتون سلامة واكتمال هذه الأكسيومات بالنسبة لفئة المروج الجزئية. وتتمثل إحدى النتائج الرئيسية في "تسطيح الكسور المشروط"، والذي يوضح أنه يمكن تحويل أي مصطلح إلى "مصطلح كسر مسطح" (fracterm flat) (قسمة واحدة لمصطلحين خاليين من القسمة) تحت شرط أن يكون المقام معرفاً.
محدودية التعبير: تثبت الورقة نتيجة سلبية هامة: لا يمكن للمنطق التعبير عن أن القسمة على صفر هي "غير معرفة". وبينما ينمذج المنطق الجزئية، فإنه لا يستطيع تمييز المروج الجزئية عن النسخة الكلية منها (مثلاً حيث $x/0 = 0$ ) تركيبياً، لأن المنطق يعامل المصطلحات غير المعرفة كأنها تفتقر إلى قيمة كلاسيكية، مما يجعلها غير قابلة للتمييز عن المصطلحات الكلية في سياقات معينة.
الحوسبة ونظرية الإثبات: من خلال تفسير المنطق ذي التخطي في جبر $\perp$ -الموسع في المنطق من الرتبة الأولى، يوضح المؤلفون أن علاقة الاستلزام للمنطق الجزئي هي شبه قابلة للحوسبة. يوفر هذا التفسير فعلياً نظام إثبات للمجبر الجزئية.
الارتباط بالمروج الشائعة: تؤسس الورقة جسراً بين المروج الجزئية و"المروج الشائعة" (حقول ذات عامل قسمة كلي حيث $x/0 = \perp$ ). وتظهر أن توسعة $\perp$ لمروج جزئية هي مروج شائعة. علاوة على ذلك، فإن تطبيق تحويل $\psi_{true}$ على أكسيومات FTC $_{pm}$ ينتج أكسيومات المروج الشائعة (FTC $_{cm}$ )، مما يثبت أن أكسيومات المروج الجزئية قوية بما يكفي لتوليد نظرية المروج الشائعة.

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

توفير إطار منطقي صارم (منطق التخطي) للاستدلال حول أنواع البيانات الجزئية حيث يكون عدم التعريف سمة هيكلية وليس حالة خطأ يجب تجنبها.
تقديم أكسيومات كاملة (FTC $_{pm}$ ) تسمح باشتقاق الخصائص الحسابية القياسية مع التعامل بشكل صحيح مع المصطلحات غير المعرفة.
إثبات أن النموذج الدلالي للمروج الجزئية يمكن اختزاله إلى النموذج الدلالي للمروج الشائعة عبر توسعة $\perp$ ، مما يربط بين المقاربات الجبرية الجزئية والكلية.
إثبات أن علاقة الاستلزام لهذا المنطق هي شبه قابلة للحوسبة، مما يشير إلى أن نظرية الإثبات للمجبر الجزئية هي أمر ممكن.

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