💻 computer science

A Diagrammatic Basis for Computer Programming

تقدم هذه الورقة فئات "كليين-كارتيزيان" الصارمة (Kleene-Cartesian rig categories) ومخططات الشريط (tape diagrams) المرتبطة بها بوصفها تدوينًا رسوميًا قادرًا على تمثيل البرامج الأمرية ومختلف منطقيات البرامج بشكل ملائم.

المؤلفون الأصليون: Filippo Bonchi, Alessandro Di Giorgio, Elena Di Lavore

نُشر 2026-04-22

📖 4 دقيقة قراءة☕ قراءة في استراحة قهوة

CC BY 4.0

المؤلفون الأصليون: Filippo Bonchi, Alessandro Di Giorgio, Elena Di Lavore

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

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

تقدم هذه الورقة البحثية هذا المفهوم بالضبط: طريقة جديدة لرسم البرامج تسمى مخططات الشريط (Tape Diagrams)، والمبنية على أساس رياضي يسمى فئات كليين-كارتيزيان ريج (Kleene-Cartesian Rig Categories).

إليك تفصيل للموضوع بأسلوب مبسط، باستخدام التشبيهات.

1. المشكلتان الكبيرتان: البيانات مقابل التحكم

فكر في برنامج الكمبيوتر كأنه مصنع.

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

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

2. الحل: فئة الـ "Rig" (الأداة المزدوجة)

يقدم المؤلفون مفهومًا يسمى فئة الـ Rig.

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

السحر في هذه الورقة البحثية هو إظهار كيف يمكن لهاتين الأداتين العمل معًا بشكل مثالي دون كسر قواعد المنطق. ويطلقون على هذا اسم فئة كليين-كارتيزيان ريج (Kleene-Cartesian Rig Category).

3. اللغة البصرية: مخططات الشريط (Tape Diagrams)

كيف ترسم هذا؟ يستخدم المؤلفون مخططات الشريط.

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

الأمر يشبه النظر إلى خريطة مترو الأنفاق (تدفق التحكم) حيث تحتوي كل محطة على مخطط تفصيلي لمحطة القطار من الداخل (تدفق البيانات).

4. لماذا يهم هذا؟ ("لغة التجميع" للمنطق)

تزعم الورقة أن هذه المخططات تعمل كـ "لغة تجميع" (Assembly Language) لمنطق البرامج.

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

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

5. أمثلة من الواقع في الورقة البحثية

يظهر المؤلفون أن هذا يعمل مع:

الأعداد الطبيعية: يمكنهم رسم بديهيات بيانو (قواعد العد 0، 1، 2...) باستخدام هذه الأشرطة.
البرامج الأمرية (Imperative Programs): يمكنهم ترجمة الكود القياسي (مثل x = x + 1 أو if x > 0 then...) إلى هذه المخططات.
المنطق العلاقاتي: يمكنهم إثبات أن برنامجين مختلفين يقومان بنفس الشيء تمامًا بمجرد النظر إلى ما إذا كان بإمكان تحويل مخططاتهما إلى بعضهما البعض.

الملخص

هذه الورقة البحثية تشبه ابتكار قواعد لغوية عالمية لبرامج الكمبيوتر.

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

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

إليك ملخص تقني مفصل للورقة البحثية بعنوان "أساس رسومي لبرمجة الحاسوب" (A Diagrammatic Basis for Computer Programming) من تأليف فيليبو بونتشي، وأليساندرو دي جيورجيو، وإيلينا دي لافوري.

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

تتناول الورقة البحثية الحاجة إلى أساس جبري منهجي لـ منطقيات البرامج (مثل منطق هوار، ومنطق عدم الصحة، ومنطق هوار العلاقاتي). وبينما قدمت الحسابات العلاقاتية ونظرية الفئات تاريخياً أسساً للمنطق (على سبيل المثال، دلالات الدوال لـ Lawvere للحسابات التساوُلية)، إلا أن الأطر الحالية تعاني في توحيد تدفق البيانات (Data Flow) وتدفق التحكم (Control Flow) ضمن إطار واحد معبر ورسومي.

تحديداً، حدد المؤلفون فجوة في نمذجة البرامج الأمرية (Imperative Programs) حيث:

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

2. المنهجية

يستخدم المؤلفون الجبر الفئوي (Categorical Algebra) والاستدلال الرسومي (Diagrammatic Reasoning) لبناء إطار عمل موحد. تتضمن منهجيتهم ثلاث خطوات رئيسية:

أ. تعريف فئات "كليين-كارتيزيان ريج" (kc-rig)

قدموا بنية فئوية جديدة تسمى فئة كليين-كارتيزيان ريج (Kleene-Cartesian rig category). تمتلك فئة "الريج" (أو فئة نصف الحلقات) بنيتين مونويديتين:

$(\otimes, 1)$ (الديكارتية): تنمذج تدفق البيانات. هذه البنية هي فئة ثنائية ديكارتية (Cartesian bicategory)، حيث يكون المنتج المونويدي هو الضرب الديكارتي للمجموعات. وهي تدعم نسخ البيانات والتخلص منها (الدوال).
$(\oplus, 0)$ (الكليين): تنمذج تدفق التحكم. هذه البنية هي فئة كليين ثنائية (Kleene bicategory)، حيث يكون المنتج المونويدي هو الجمع المنفصل (Biproduct). وهي تدعم عدم الحتمية، والاختيار، والتكرار عبر تتبع منتظم (Uniform trace).

يتم ضبط التفاعل بين هاتين البنيتين عبر قوانين التوزيع، مما يضمن تحقق بنية "الريج" (الشبيهة بنصف الحلقة).

ب. تقديم مخططات الشريط (Tape Diagrams)

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

المفهوم: مخططات الشريط هي "رسوم تخطيطية سلسة لرسوم تخطيطية سلسة".
الطبقة الداخلية (الدوائر): تمثل البنية الديكارتية ( $\otimes$ )، وتنمذج تدفق البيانات (النسخ، التخلص من البيانات، تطبيق الدوال).
الطبقة الخارجية (الأشرطة): تمثل بنية كليين ( $\oplus$ )، وتنمذج تدفق التحكم (التفرع، الحلقات، الاختيار غير الحتمي).
النحو (Syntax): تسمح المخططات بتداخل الدوائر داخل الأشرطة، مما يوفر تمثيلاً ثنائي الأبعاد للتفاعل بين البيانات والتحكم.

ج. الدلالات الدوالية (Functorial Semantics)

اتباعاً لمنهج لوفير (Lawvere)، عرف المؤلفون نظريات كليين-كارتيزيان كأزواج من "التوقيع" (Signature) ومجموعة من البديهيات (عدم التساوي بين الأشرطة). وتكون نماذج هذه النظريات عبارة عن دوال من الفئة المولدة بحرية لمخططات الشريط إلى فئة مستهدفة (غالباً ما تكون Rel، فئة المجموعات والعلاقات).

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

1. فئات كليين الثنائية وجبر كليين النوعي

صاغ المؤلفون فئات كليين الثنائية كفئات مونويدية متتبعة (Traced Monoidal Categories) غنية بالترتيب الجزئي (Poset-enriched) مع منتجات ثنائية. وأثبتوا أن هذه الفئات تكافئ جبر كليين النوعي (Typed Kleene Algebras) (امتداد بديهيات كوزين لتشمل أنواعاً متعددة). وهذا يثبت أن التتبع الفئوي على المنتجات الثنائية يجسد تماماً الخصائص الجبرية لنجمة كليين ( $*$ )، التي تمثل التكرار.

2. حساب مخططات الشريط

قدموا حساباً رسومياً كاملاً لفئات kc-rig.

مبرهنة 7.1: فئة مخططات الشريط ( $KCT_\Sigma$ ) هي فئة كليين-كارتيزيان ريج حرة من نوع sesquistrict ناتجة عن توقيع معين.
يتضمن الحساب بديهيات محددة للتفاعل بين المنتجين المونويديين، بما في ذلك شروط الانتظام (Uniformity conditions) للتتبع، وهي ضرورية لاشتقاق ثوابت الحلقات ومبادئ الاستقراء.

3. ترميز البرامج الأمرية

توضح الورقة كيفية ترميز بنى البرمجة الأمرية القياسية في مخططات الشريط:

المتغيرات/الحالة: تمثلها الأسلاك في الطبقة الديكارتية.
الإسنادات (Assignments): تُنمذج باستخدام بنية النسخ/التخلص من البيانات في الفئات الديكارتية الثنائية.
الجمل الشرطية: تُنمذج باستخدام بنية المنتج الثنائي ( $\oplus$ ) والمنعكسات الأساسية (Coreflexives/Predicates).
الحلقات: تُنمذج باستخدام نجمة كليين ( $*$ ) وعملية التتبع.

4. اشتقاق منطقيات البرامج

النتيجة الرئيسية هي أن منطقيات البرامج القياسية ليست قواعد عشوائية، بل هي نتائج للقوانين الجبرية لفئات kc-rig.

منطق هوار (Hoare Logic): أثبت المؤلفون أن قواعد الاستدلال لمنطق هوار (الصحة الجزئية) تتبع مباشرة من بديهيات فئات kc-rig (القسم 9.7).
منطق هوار العلاقاتي (RHL): أظهروا أن RHL (الذي يستدل على برنامجين في آن واحد) يمكن التعبير عنه بشكل طبيعي باستخدام منتج $\otimes$ للأشرطة، مما يسمح ببناء "برامج منتجة" وإثبات خصائص مثل عدم التداخل والأمن.
المنطقيات الأخرى: يستوعب الإطار أيضاً "منطق عدم الصحة"، و"منطق عدم الصحة الكافي"، و"المنطق الضروري" بمجرد تغيير اتجاه عدم التساوي في التفسير الدلالي.

5. حساب بيانو (Peano Arithmetic)

قدم المؤلفون نظرية كليين-كارتيزيان لبديهيات بيانو للأعداد الطبيعية. وأظهروا أن مبدأ الاستقراء الرياضي هو نتيجة مباشرة لـ الانتظام المرتبي (Posetal uniformity) للتتبع في بنية فئة كليين الثنائية.

4. النتائج

اكتمال الترميز: ترميز البرامج الأمرية في مخططات الشريط هو ترميز سليم (Sound). إذا تساوى برنامجان في حساب الشريط، فهما متكافئان دلالياً (لهما نفس الدلالات العلاقاتية).
اشتقاق القواعد: تقدم الورقة اشتقاقات رسومية صريحة توضح أن:
- ثلاثيات هوار $\{P\}C\{Q\}$ تقابل عدم التساوي $E(P)^\dagger ; E(C) \leq E(Q)^\dagger$ .
- قاعدة حلقات while مشتقة من بديهية الانتظام للتتبع.
- قاعدة الإطار (Frame Rule) في منطق هوار العلاقاتي مشتقة من التفاعل بين المنتج الديكارتي والتتبع.
القدرة التعبيرية: أثبتت الورقة أن الإطار أكثر قدرة تعبيرية من "جبر كليين مع الاختبارات" (KAT) القياسي، لأنه ينمذج صراحةً تدفق البيانات وتبعية المتغيرات، مما يسمح بإثبات التكافؤات التي لا يستطيع KAT اشتقاقها دون بديهيات إضافية (مثل تبادلية الإسنادات على متغيرات منفصلة).

5. الأهمية

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

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