💻 computer science

Fully Evaluated Left-Sequential Logics

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

المؤلفون الأصليون: Alban Ponse, Daan J. C. Staudt

نُشر 2026-05-14

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

CC BY 4.0

المؤلفون الأصليون: Alban Ponse, Daan J. C. Staudt

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

تخيل أنك طاهٍ يحضر طبقاً معقداً. في عالم المنطق الحاسوبي، "المكونات" هي حقائق (صحيحة أو خاطئة)، و"الوصفات" هي تعليمات حول كيفية دمج هذه المكونات. تقدم هذه الورقة عائلة من أساليب الطهي تسمى المنطقيات كاملة التقييم والمتسلسلة من اليسار (Fully Evaluated Left-Sequential Logics - FELs).

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

إليك تفصيل لـ "أساليب الطهي" (المنطقيات) المختلفة التي يستعرضها المؤلفون، باستخدام تشبيهات من الحياة اليومية.

1. القاعدة الأساسية: "التسلسل من اليسار"

في هذه المنطقيات، الترتيب مهم. إذا كانت لديك وصفة A ثم B ، فإنه يجب عليك تذوق A أولاً.

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

2. المستويات الأربعة لـ "أساليب الطهي"

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

المستوى 1: FEL الحر (FFEL) – "المتذوق الفوضوي"

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

المستوى 2: FEL الذاكر (MFEL) – "الطاهي مدون الملاحظات"

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

المستوى 3: FEL الشرطي (CℓFEL) – "الفريق المرن"

الأجواء: هذا الفريق يمكنه تبادل الأماكن.
القاعدة: يشبه MFEL (أنت تتذكر ما تذوقته)، ولكن يمكنك الآن تبديل ترتيب المكونات إذا كانت مختلفة. A ثم B تُعامل بنفس طريقة B ثم A.
التشبيه: تخيل مجموعة من الأصدقاء يقررون أين يأكلون. إذا كان أليس وبوب يقرران بين البيتزا والسوشي، فلا يهم من يتحدث أولاً؛ القرار النهائي هو نفسه.
الميزة الرئيسية: هذا المنطق يكافئ منطقاً شهيراً ثلاثي القيم يسمى منطق بوخفار (Bochvar's Logic). وهو يتعامل مع المكونات "غير المعرفة" (مثل بيضة مكسورة) من خلال اعتبار الطبق بأكمله "مكسوراً" (غير معرف) فوراً.

المستوى 4: FEL الساكن (SFEL) – "المحاسب الصارم"

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

3. المكون "غير المعرف" (U)

يستكشف المؤلفون أيضاً ما يحدث إذا كان المكون غير معرف (U).

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

4. "أشجار" المنطق

لإثبات أن قواعدهم تعمل، يستخدم المؤلفون أشجار التقييم.

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

ملخص إنجاز الورقة

لم يكتفِ المؤلفون بوصف أساليب الطهي هذه؛ بل كتبوا كتب القواعد (Axioms) لكل منها.

حددوا بدقة كيفية دمج المكونات (المعادلات).
أثبتوا أن كتب القواعد هذه كاملة (تغطي كل السيناريوهات الممكنة) ومستقلة (لا توجد قاعدة زائدة؛ لا يمكنك إزالة أي منها دون كسر النظام).
استخدموا أدوات حاسوبية (Prover9 و Mace4) للتحقق من حساباتهم، لضمان عدم تسلل أي خطأ بشري.

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

ملخص تقني: المنطقيات المتسلسلة يسارياً ذات التقييم الكامل

بيان المشكلة
تتناول هذه الورقة صياغة وتأصيل "المنطقيات المتسلسلة يسارياً ذات التقييم الكامل" (Fully Evaluated Left-Sequential Logics - FELs). وخلافاً لمنطقيات التخطي (Short-Circuit Logics - SCLs)، حيث يتوقف التقييم بمجرد تحديد نتيجة تعبير مركب، تفرض منطقيات FEL استراتيجية "تقييم كامل" أو "صارم": حيث يتم تقييم كل قضية ذرية داخل المصطلح بغض النظر عما إذا كانت قيمتها ضرورية تماماً للنتيجة النهائية أم لا. تُعزى هذه الاستراتيجية إلى سياقات البرمجة حيث يجب ضمان حدوث الآثار الجانبية (مثل تغييرات الحالة) لجميع الذرات في التعبير. يهدف المؤلفون إلى تعريف تسلسل هرمي لهذه المنطقيات، يتراوح من الأضعف (Free FEL)، وهو محصن ضد الآثار الجانبية للذرات، إلى الأقوى (Static FEL)، والذي يسلك سلوك النسخة المتسلسلة من المنطق القضايا الكلاسيكي. علاوة على ذلك، توسع الورقة هذه المنطقيات لتشمل إطاراً ثلاثي القيم للتعامل مع "عدم التعريف" ( $U$ )، وهي سمة شائعة في البرمجة والمنطق (مثل القسمة على صفر).

المنهجية
يستخدم المؤلفون إطاراً دلالياً يعتمد على أشجار التقييم (Evaluation Trees)، وهو مفهوم قدموه في عملهم السابق [19].

الدلالات: أشجار التقييم هي أشجار ثنائية حيث تمثل العقد الداخلية الذرات، وتمثل الأوراق قيم الحقيقة ( $T$ $T$ ، $F$ $F$ ، أو $U$ $U$ ). ويمثل المسار من الجذر إلى الورقة تسلسل التقييم.
- في Free FEL (FFEL)، يحافظ هيكل الشجرة بدقة على ترتيب التقييم ويسمح بالتكرار المتعدد لنفس الذرة، مما ينمذج الآثار الجانبية المحتملة.
- في Memorising FEL (MFEL)، يتم تنقيح الدلالات بحيث لا يحتوي أي مسار في الشجرة على تكرارات متعددة لنفس الذرة؛ حيث يتم "تذكر" تقييم الذرة إذا تمت مواجهتها مرة أخرى.
- في Conditional FEL (CℓFEL)، تدمج المنطق خاصية التبادلية للذرات، مما يعني فعلياً أن ترتيب الذرات المستقلة غير ذي صلة.
- في Static FEL (SFEL)، ينهار المنطق إلى نسخة متسلسلة من المنطق القضايا حيث تسري قوانين الامتصاص.
التوسيع ثلاثي القيم: بالنسبة لجميع المنطقيات باستثناء SFEL، يقدم المؤلفون ثابتاً هو $U$ (غير معرف). يتم توسيع الدلالات لتشمل أشجاراً بأوراق في $\{T, F, U\}$ ، حيث يعمل $U$ كعنصر امتصاص (على سبيل المثال $U \land_r x = U$ ).
التأصيل (Axiomatization): المساهمة المنهجية الرئيسية هي اشتقاق تأصيلات متساوية كاملة لكل منطق. يحدد المؤلفون أشكالاً طبيعية (مثل FEL Normal Form، و $\sigma$ -normal forms) لإثبات الاكتمال. كما استخدموا مبرهن النصوص الآلي Prover9 للتحقق من الاشتقاقات، وMace4 لتوليد نماذج مضادة منتهية لإثبات استقلال البديهيات.

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

التسلسل الهرمي لمنطقيات FEL ثنائية القيم:
- Free FEL (FFEL): أضعف منطق، تم تأصيله بواسطة المجموعة $EqFFEL$ . هو ينفي التكرار ( $x \land_r x \neq x$ ) ولكنه يحقق التجميعية. وهو منطق التقييم الكامل دون قيود على الآثار الجانبية.
- Memorising FEL (MFEL): تم تأصيله بإضافة بديهية واحدة إلى FFEL (تحديداً $(x \lor_r y) \land_r z = (\neg x \land_r (y \land_r z)) \lor_r (x \land_r z)$ ). وهو يفرض أن تُعامل الذرات المتكررة كأنها متطابقة، مما يلغي الآثار الجانبية.
- Conditional FEL (CℓFEL $_2$ ): تم تأصيله بإضافة التبادلية ( $x \land_r y = y \land_r x$ ) إلى MFEL. هذا المنطق مكافئ للفرع ثنائي القيم من المنطق الشرطي (Guzmán و Squier [12]).
- Static FEL (SFEL): أقوى منطق، يتم الحصول عليه بإضافة $x \land_r F = F$ إلى CℓFEL $_2$ . وهو مكافئ لمنطق التخطي الساكن (SSCL) والمنطق القضايا القياسي تحت التقييم المتسلسل.
التوسيعات ثلاثية القيم (FELU):
- يعرّف المؤلفون نسخاً ثلاثية القيم (FFELU، MFELU، CℓFEL) عن طريق إضافة البديهيات $\neg U = U$ و $U \land_r x = U$ .
- ثبت أن CℓFEL (المنطق الشرطي ثلاثي القيم) مكافئ لـ منطق بوخفار الصارم (Bochvar's strict logic) [8].
- لا يمكن توسيع SFEL باستخدام $U$ لأن قانون الامتصاص $F = U \land_r F = U$ يؤدي إلى انهيار قيم الحقيقة.
الاكتمال والاستقلال:
- تم تقديم تأصيلات متساوية كاملة لجميع المنطقيات المعرفة.
- يقدم المؤلفون مجموعات بديلة وأكثر إيجازاً من البديهيات المستقلة لكل منطق (مثل المجموعة $MF$ لـ MFEL)، والتي تم التحقق منها باستخدام أدوات آلية.
- تم بناء أشكال طبيعية لإثبات أن التساوي النحوي للأشكال الطبيعية يتوافق مع التساوي الدلالي لأشجار التقييم.

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

القدرة على التنبؤ: يجادل المؤلفون بأن منطقيات FEL توفر قدرة أكبر على التنبؤ بحالة البيئة (الآثار الجانبية) بعد التقييم مقارنة بمنطقيات SCL، حيث يتم ضمان تقييم جميع الذرات.
القدرة التعبيرية: توضح الورقة أنه بينما لا يستطيع FFEL التعبير عن بعض أشجار التقييم الموحدة (مثل الأشجار التي تظهر فيها ذرة في فروع مختلفة بنتائج مختلفة)، فإن MFEL والمنطقيات الأقوى يمكنها التعبير عن ذلك، مما يزيد من القدرة التعبيرية للمنطق.
العلاقة بالعمل القائم: تضع الورقة CℓFEL ضمن التسلسل الهرمي للمنطقيات، مبينة أنه مكافئ لمنطق بوخفار وفرع من المنطق الشرطي. كما توضح العلاقة بين FELs ومنطقيات التخطي (SCLs)، مشيرة إلى أنه يمكن تعريف روابط FEL ضمن أطر SCL (والعكس صحيح تحت شروط معينة)، رغم أن FELs تفرض انضباطاً أكثر صرامة في التقييم.

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