منطق قابلية الحوسبة

منطق الحوسبة ( CoL ) هو برنامج بحثي وإطار رياضي لإعادة تطوير المنطق كنظرية رسمية منهجية للحوسبة ، على عكس المنطق الكلاسيكي ، الذي هو نظرية رسمية للحقيقة . وقد تم تقديمه وتسميته بهذا الاسم من قبل جيورجي جاباريدزه في عام 2003. ^{[ 1 ]}

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

يُصاغ منطق الحوسبة (CoL) المشكلات الحسابية في معناها الأكثر عمومية - التفاعلي . يُعرّف CoL المشكلة الحسابية على أنها لعبة يلعبها جهاز ضد بيئته. تكون هذه المشكلة قابلة للحساب إذا وُجد جهاز يفوز باللعبة ضد كل سلوك مُحتمل للبيئة. يُعمم هذا الجهاز الذي يلعب اللعبة فرضية تشيرش-تورينج إلى المستوى التفاعلي. يتضح أن المفهوم الكلاسيكي للحقيقة هو حالة خاصة من قابلية الحساب، ذات درجة تفاعل صفرية. هذا يجعل المنطق الكلاسيكي جزءًا خاصًا من CoL. وبالتالي، يُعد CoL امتدادًا محافظًا للمنطق الكلاسيكي. يتميز منطق الحوسبة بأنه أكثر تعبيرًا وبنائيةً ودلالةً حسابيةً من المنطق الكلاسيكي. إلى جانب المنطق الكلاسيكي، يُعد منطق الاستقلال (IF) وبعض الامتدادات المناسبة للمنطق الخطي والمنطق الحدسي أجزاءً طبيعية من CoL. ^{[ 2 ] [ 3 ]} ومن ثم، يُمكن اشتقاق مفاهيم ذات دلالة مثل "الحقيقة الحدسية" و"حقيقة المنطق الخطي" و"حقيقة منطق الاستقلال" من دلالات CoL.

يجيب منطق الحساب (CoL) بشكل منهجي على السؤال الأساسي حول ما يمكن حسابه وكيف؛ ولذلك، فإن لمنطق الحساب تطبيقات عديدة، مثل النظريات التطبيقية البنّاءة، وأنظمة قواعد المعرفة ، وأنظمة التخطيط والتنفيذ. ومن بين هذه التطبيقات، لم يتم استكشاف سوى تطبيقات النظريات التطبيقية البنّاءة بشكل مكثف حتى الآن: فقد تم بناء سلسلة من نظريات الأعداد القائمة على منطق الحساب، والتي تُسمى "الحسابات الكلاسيكية"، ^{[ 4 ] [ 5 ]} كبدائل ذات مغزى حسابي ونظري من حيث التعقيد لحساب بيانو من الدرجة الأولى القائم على المنطق الكلاسيكي وتنوعاته مثل أنظمة الحساب المحدود .

لا تكفي أنظمة البرهان التقليدية، مثل الاستدلال الطبيعي وحساب المتتاليات ، لوضع بديهيات للأجزاء غير التافهة من نظرية القانون. وقد استدعى ذلك تطوير طرق برهان بديلة أكثر عمومية ومرونة، مثل حساب الدوائر . ^{[ 6 ] [ 7 ]}

تُوسّع لغة CoL الكاملة لغة منطق الرتبة الأولى الكلاسيكي . تحتوي مفرداتها المنطقية على أنواع عديدة من الروابط ، والفصل ، والمُكمِّمات ، والاستلزام ، والنفي ، وما يُسمى بعوامل التكرار. تشمل هذه المجموعة جميع الروابط والمُكمِّمات في المنطق الكلاسيكي. كما تحتوي اللغة على نوعين من الذرات غير المنطقية: الذرات الأولية والذرات العامة . الذرات الأولية، وهي ببساطة ذرات المنطق الكلاسيكي، تُمثل مسائل أولية ، أي ألعاب بدون حركات يفوز بها الجهاز تلقائيًا عندما تكون صحيحة ويخسرها عندما تكون خاطئة. أما الذرات العامة، فيمكن تفسيرها على أنها أي لعبة، أولية أو غير أولية. من الناحيتين الدلالية والنحوية، فإن المنطق الكلاسيكي ليس سوى جزء من CoL تم الحصول عليه من خلال منع الذرات العامة في لغته، ومنع جميع العوامل الأخرى غير ¬، ∧، ∨، →، ∀، ∃.

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

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

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

تُفهم العمليات المنطقية في نظرية الألعاب على أنها عمليات على الألعاب. هنا نستعرض بعضًا من هذه العمليات بشكل غير رسمي. ولتبسيط الأمر، نفترض أن مجال الخطاب هو دائمًا مجموعة جميع الأعداد الطبيعية: {0، 1، 2، ...}.

تُبدّل عملية النفي ("ليس") أدوار اللاعبين، فتحوّل تحركات وانتصارات الآلة إلى تلك التي يحققها النظام، والعكس صحيح. على سبيل المثال، إذا كانت لعبة الشطرنج هي لعبة الشطرنج (مع استبعاد التعادلات) من منظور اللاعب الأبيض، فإن لعبة الشطرنج "ليس" هي نفسها من منظور اللاعب الأسود.

يجمع العطف المتوازي ∧ ("pand") والفصل المتوازي ∨ ("por") الألعاب بطريقة متوازية. سلسلة A ∧ B أو A ∨ B هي لعب متزامن في كلا العطفين. يفوز الجهاز في A ∧ B إذا فاز في كليهما. ويفوز في A ∨ B إذا فاز في أحدهما على الأقل. على سبيل المثال، الشطرنج ∨¬ الشطرنج لعبة على رقعتين، إحداهما بالأبيض والأخرى بالأسود، ومهمة الجهاز هي الفوز على رقعة واحدة على الأقل. يمكن الفوز بهذه اللعبة بسهولة بغض النظر عن هوية الخصم، وذلك بنسخ حركاته من رقعة إلى أخرى.

يُعرَّف عامل الاستلزام المتوازي → ("pimplication") بالعلاقة A → B = ¬ A ∨ B. والمعنى البديهي لهذه العملية هو اختزال B إلى A ، أي حل A طالما أن الخصم قادر على حل B.

يمكن تعريف المُكمِّمات المتوازية ∧ ("pall") و ∨ ("pexists") كما يلي: ∧ xA ( x ) = A ( 0 ) ∧ A ( 1) ∧ A (2) ∧ ... و ∨ xA ( x ) = A (0) ∨ A (1) ∨ A (2) ∨ ... وبالتالي، تُمثل هذه عمليات لعب متزامنة للبطاقات A (0) و A (1) و A (2) ...، كلٌّ منها على لوحة منفصلة. تربح الآلة ∧ xA ( x ) إذا ربحت جميع هذه الألعاب، و ∨ xA ( x ) إذا ربحت بعضها.

من ناحية أخرى، تُولّد المُكمِّمات العمياء ∀ ("blall") و∃ ("blexists") ألعابًا على لوحة واحدة. تُعتبر سلسلة ∀ xA ( x ) أو ∃ xA ( x ) سلسلة واحدة من A. يفوز الجهاز في ∀ xA ( x ) (أو ∃ xA ( x )) إذا كانت هذه السلسلة سلسلة فائزة من A ( x ) لجميع (أو قيمة واحدة على الأقل) القيم الممكنة لـ x ، ويفوز في ∃ xA ( x ) إذا كان هذا صحيحًا لقيمة واحدة على الأقل.

جميع المؤثرات التي تم توصيفها حتى الآن تتصرف تمامًا مثل نظيراتها الكلاسيكية عند تطبيقها على الألعاب الأولية (التي لا تتضمن حركة)، وتؤكد صحة المبادئ نفسها. لهذا السبب، يستخدم منطق CoL الرموز نفسها لهذه المؤثرات كما في المنطق الكلاسيكي. مع ذلك، عند تطبيق هذه المؤثرات على الألعاب غير الأولية، فإن سلوكها لا يعود كلاسيكيًا. على سبيل المثال، إذا كانت p ذرة أولية و P ذرة عامة، فإن p → p ∧ p صحيحة بينما P → P ∧ P غير صحيحة. ومع ذلك، يبقى مبدأ الوسط المرفوع P ∨ ¬P صحيحًا. هذا المبدأ نفسه غير صحيح مع الأنواع الثلاثة الأخرى من الفصل (الاختيار، والتسلسل، والتبديل).

الفصل الاختياري ⊔ ("chor") للعبتين A و B ، ويُكتب A ⊔ B ، هو لعبة يتعين على الآلة فيها، للفوز، اختيار أحد الخيارين المنفصلين ثم الفوز في المكون المختار. يبدأ الفصل التسلسلي ("sor") A ∩ B كـ A ؛ وينتهي أيضًا كـ A ما لم تقم الآلة بحركة "تبديل"، وفي هذه الحالة يتم التخلي عن A وتُعاد اللعبة وتستمر كـ B. في الفصل التبديلي ("tor") A ⩛ B ، يمكن للآلة التبديل بين A و B عددًا محدودًا من المرات. لكل عامل فصل اقتران ثنائي، يتم الحصول عليه عن طريق تبديل أدوار اللاعبين. يمكن تعريف الكميات المقابلة على أنها اقترانات أو فواصل لا نهائية بنفس طريقة تعريف الكميات المتوازية. يُنتج كل نوع من أنواع الفصل أيضًا عملية استلزام مقابلة بنفس طريقة الاستلزام المتوازي →. على سبيل المثال، يتم تعريف استلزام الاختيار ("chimplication") A ⊐ B على أنه ¬ A ⊔ B.

يمكن تعريف التكرار المتوازي ("التكرار المسبق") لـ A على أنه الاقتران المتوازي اللانهائي A ∧A∧A∧... ويمكن تعريف أنواع التكرار التسلسلي ("التكرار") والتبديل ("التكرار") بشكل مماثل.

يمكن تعريف عوامل التكرار الأساسي على أنها عمليات فصل لا نهائية. التكرار المتفرع ( "التكرار المتفرع") ⫰ ، وهو أقوى أنواع التكرار، لا يملك اقترانًا مقابلًا. ⫰ A هي لعبة تبدأ وتستمر على النحو A. ومع ذلك، يُسمح للبيئة في أي وقت بإجراء حركة "تكرارية"، مما يُنشئ نسختين من الموضع الحالي لـ A ، وبالتالي يقسم اللعب إلى مسارين متوازيين لهما ماضٍ مشترك ولكن قد تختلف تطوراتهما المستقبلية. وبنفس الطريقة، يمكن للبيئة تكرار أي من مواضع أي مسار، مما يُنشئ المزيد والمزيد من مسارات A. تُلعب هذه المسارات بالتوازي، ويحتاج الجهاز إلى الفوز بـ A في جميع المسارات ليكون الفائز في ⫰ A. يُعرَّف التكرار الأساسي المتفرع ( " التكرار المتفرع") ⫯ بشكل متناظر عن طريق تبديل "الجهاز" و"البيئة".

يُنتج كل نوع من أنواع التكرار نسخة ضعيفة مقابلة من الاستلزام ونسخة ضعيفة من النفي. يُطلق على الأولى اسم " استلزام جزئي "، وعلى الثانية اسم " نفي" . الاستلزام الجزئي المتفرع ("brimplication") A ⟜ B ليس سوى ⫰ A → B ، والنفي المتفرع ("brefutation") لـ A هو A ⟜ ⊥، حيث ⊥ هي اللعبة الأولية الخاسرة دائمًا. وينطبق الأمر نفسه على جميع أنواع الاستلزام الجزئي والنفي الأخرى.

توفر لغة CoL طريقة منهجية لتحديد عدد لا حصر له من المسائل الحسابية، سواء كانت لها أسماء محددة في المراجع العلمية أم لا. فيما يلي بعض الأمثلة.

لتكن f دالة أحادية . تُكتب مسألة حساب f على الصورة ⊓ x ⊔ y( y = f ( x )). وفقًا لدلالات CoL، هذه لعبة حيث تكون الخطوة الأولى ("المدخلات") من قِبل البيئة، التي يجب أن تختار قيمة m لـ x . بديهيًا، هذا يعني مطالبة الآلة بتحديد قيمة f ( m ). تستمر اللعبة على الصورة ⊔ y( y = f ( m )). الآن، يُتوقع من الآلة القيام بخطوة ("المخرجات")، والتي يجب أن تختار قيمة n لـ y . هذا يعني أن n هي قيمة f ( m ). تُختزل اللعبة الآن إلى المعادلة الأولية n = f ( m )، والتي تفوز بها الآلة إذا وفقط إذا كانت n هي بالفعل قيمة f ( m ).

ليكن p محمولًا أحاديًا . عندئذٍ، يعبر ⊓ x ( p ( x )⊔¬ p ( x )) عن مشكلة تحديد p ، ويعبر ⊓ x ( p ( x )& ᐁ ¬ p ( x )) عن مشكلة التحديد الجزئي لـ p ، ويعبر ⊓ x ( p ( x )⩛¬ p ( x )) عن مشكلة التقريب التكراري لـ p .

ليكن p و q دالتين أحاديتين. عندئذٍ، يُعبّر التعبير ⊓ x ( p ( x )⊔¬ p ( x )) ⟜ ⊓ x ( q ( x )⊔¬ q ( x )) عن مسألة اختزال q إلى p باستخدام آلة تورينج (بمعنى أن q قابلة للاختزال إلى p باستخدام تورينج إذا وفقط إذا كانت المسألة التفاعلية ⊓ x ( p ( x )⊔¬ p ( x )) ⟜ ⊓ x ( q ( x )⊔¬ q ( x )) قابلة للحساب). ويُحقق التعبير ⊓ x ( p ( x )⊔¬ p ( x )) → ⊓ x ( q ( x )⊔¬ q ( x )) نفس الغرض، ولكن لنسخة أقوى من اختزال تورينج حيث لا يُمكن الاستعلام عن مرجع p إلا مرة واحدة. يُحقق التعبير ⊓ x ⊔ y ( q ( x )↔ p ( y )) نفس الغرض في مسألة اختزال q إلى p في حالة وجود عدد كبير من العناصر. وباستخدام تعابير أكثر تعقيدًا، يُمكن استخلاص أنواعٍ عديدة من العلاقات والعمليات غير المُسماة، ولكنها ذات دلالة محتملة، في المسائل الحسابية، مثل "اختزال مسألة شبه القرار r إلى مسألة اختزال q إلى p في حالة وجود عدد كبير من العناصر". وبفرض قيود زمنية أو مكانية على عمل الآلة، يُمكن الحصول على نظائر نظرية التعقيد لهذه العلاقات والعمليات.

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

من أمثلة النظريات التطبيقية القائمة على منطق الاستدلال ما يُعرف باسم "علم الحساب اللفظي" . وهي نظريات عددية مبنية على منطق الاستدلال بنفس معنى أن حساب بيانو من الرتبة الأولى مبني على المنطق الكلاسيكي. عادةً ما يكون هذا النظام امتدادًا محافظًا لحساب بيانو، إذ يتضمن جميع بديهيات بيانو، ويضيف إليها بديهية أو بديهيتين إضافيتين، مثل ⊓ x ⊔ y ( حيث y = x' ) للتعبير عن قابلية حساب دالة الخلف. كما يحتوي عادةً على قاعدة أو قاعدتين غير منطقيتين للاستدلال، مثل النسخ البنائية للاستقراء أو الفهم . ومن خلال تعديلات روتينية على هذه القواعد، يمكن الحصول على أنظمة سليمة وكاملة تُميز فئة أو أخرى من فئات التعقيد الحسابي التفاعلي C. بمعنى أن المسألة تنتمي إلى C إذا وفقط إذا كان لها برهان في النظرية. لذا، يمكن استخدام هذه النظرية لإيجاد حلول خوارزمية، بالإضافة إلى حلول فعّالة عند الطلب، مثل الحلول التي تعمل في وقت متعدد الحدود أو مساحة لوغاريتمية . تجدر الإشارة إلى أن جميع النظريات الحسابية تشترك في نفس المسلمات المنطقية، وتختلف مسلماتها غير المنطقية فقط باختلاف فئة التعقيد المستهدفة. وتكمن ميزتها البارزة عن المناهج الأخرى ذات الأهداف المماثلة (مثل الحساب المحدود ) في أنها تُوسّع نظرية الأتمتة المنطقية بدلاً من إضعافها، مما يحافظ على كامل قوتها الاستنتاجية وسهولة استخدامها.

• دلالات اللعبة
• الحوسبة التفاعلية
• منطق
• منطق الحوسبة

• الصفحة الرئيسية لمنطق الحوسبة: دراسة شاملة للموضوع.
• جيورجي جاباريدزه
• دلالات الألعاب أم المنطق الخطي؟
• محاضرة في منطق الحوسبة
• محاضرة فيديو حول دلالات الموارد المجردة ومنطق الحوسبة  من تقديم ن. فيريشاجين.
• دراسة استقصائية لمنطق الحوسبة (ملف PDF) نسخة قابلة للتنزيل من الصفحة الرئيسية المذكورة أعلاه.