منطق متعدد الأنواع

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

توجد طرقٌ عديدةٌ لصياغة النية المذكورة أعلاه؛ والمنطق متعدد الأنواع هو أي حزمة معلومات تُحققها. وفي معظم الحالات، تُقدَّم المعلومات التالية:

• مجموعة من الأنواع، S
• تعميم مناسب لمفهوم التوقيع ليكون قادراً على التعامل مع المعلومات الإضافية التي تأتي مع أنواع التوقيع.

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

عند التفكير في الكائنات الحية، من المفيد التمييز بين نوعين:${\displaystyle \mathrm {نبات} }$و${\displaystyle \mathrm {حيوان} }$بينما دالة${\displaystyle \mathrm {الأم} \colon \mathrm {حيوان} \to \mathrm {حيوان} }$هذا منطقي، وظيفة مماثلة${\displaystyle \mathrm {mother} \colon \mathrm {plant} \to \mathrm {plant} }$لا يحدث ذلك عادةً. يسمح منطق التصنيف المتعدد بوجود مصطلحات مثل${\displaystyle \mathrm {mother} (\mathrm {lassie} )}$لكن التخلص من مصطلحات مثل${\displaystyle \mathrm {mother} (\mathrm {my\_favorite\_oak} )}$باعتبارها غير سليمة نحوياً.

تم شرح عملية تحويل المنطق متعدد الأنواع إلى جبري في مقال بقلم كاليرو وجونسالفيس، ^{[ 1 ]} والذي يعمم المنطق الجبري المجرد إلى الحالة متعددة الأنواع، ولكن يمكن استخدامه أيضًا كمادة تمهيدية.

بينما يتطلب منطق التصنيف المتعدد وجود نوعين متميزين لمجموعات كون منفصلة، ​​يسمح منطق التصنيف المرتب بنوع واحد فقط.${\displaystyle s_{1}}$أن يُعلن أنه نوع فرعي من نوع آخر${\displaystyle s_{2}}$وعادةً عن طريق الكتابة${\displaystyle s_{1}\subseteq s_{2}}$أو صيغة مشابهة. في مثال علم الأحياء المذكور أعلاه ، يُفضّل التصريح بـ

${\displaystyle {\text{dog}}\subseteq {\text{carnivore}}}$،

${\displaystyle {\text{dog}}\subseteq {\text{mammal}}}$،

${\displaystyle {\text{carnivore}}\subseteq {\text{animal}}}$،

${\displaystyle {\text{mammal}}\subseteq {\text{animal}}}$،

${\displaystyle {\text{animal}}\subseteq {\text{organism}}}$،

${\displaystyle {\text{plant}}\subseteq {\text{organism}}}$،

وهكذا دواليك؛ انظر الصورة.

أينما ورد مصطلح من نوع ما${\displaystyle s}$مطلوب، مصطلح من أي نوع فرعي من${\displaystyle s}$يمكن توفير بديل ( مبدأ استبدال ليسكوف ). على سبيل المثال، بافتراض تعريف دالة${\displaystyle {\text{الأم}}:{\text{الحيوان}}\longrightarrow {\text{الحيوان}}}$وإعلان ثابت${\displaystyle {\text{لاسي}}:{\text{كلب}}}$، على المدى ${\displaystyle {\text{الأم}}({\text{الفتاة}})}$صحيح تمامًا وله نفس النوع${\displaystyle {\text{حيوان}}}$ولتقديم المعلومة بأن أم الكلب هي كلبة بدورها، يلزم إعلان آخر ${\displaystyle {\text{الأم}}:{\text{الكلب}}\longrightarrow {\text{الكلب}}}$قد يتم إصدارها؛ وهذا ما يسمى تحميل الوظائف الزائد ، وهو مشابه للتحميل الزائد في لغات البرمجة .

يمكن ترجمة المنطق المرتب إلى منطق غير مرتب، باستخدام مسند أحادي.${\displaystyle p_{i}(x)}$لكل نوع${\displaystyle s_{i}}$، وبديهية${\displaystyle \forall x(p_{i}(x)\rightarrow p_{j}(x))}$لكل إعلان فرز فرعي${\displaystyle s_{i}\subseteq s_{j}}$. وقد نجح النهج العكسي في إثبات النظريات الآلي : ففي عام 1985، تمكن كريستوف والتر من حل مشكلة كانت تُعتبر معيارًا في ذلك الوقت عن طريق ترجمتها إلى منطق مرتب ومصنف، مما أدى إلى تبسيطها بمقدار عشرة أضعاف، حيث تحولت العديد من المسندات الأحادية إلى أنواع. ^{[ 2 ]}

لدمج منطق الترتيب في مُثبت نظريات آلي قائم على البنود، يلزم وجود خوارزمية توحيد مُرتبة مُقابلة ، والتي تتطلب لأي نوعين مُعلنين${\displaystyle s_{1},s_{2}}$تقاطعهم${\displaystyle s_{1}\cap s_{2}}$سيتم الإعلان عنه أيضًا: إذا${\displaystyle x_{1}}$و${\displaystyle x_{2}}$هي متغيرات من نوع ما${\displaystyle s_{1}}$و${\displaystyle s_{2}}$، على التوالي، المعادلة${\displaystyle x_{1}{\stackrel {?}{=}}\,x_{2}}$لديه الحل${\displaystyle \{x_{1}=x,\;x_{2}=x\}}$، أين${\displaystyle x:s_{1}\cap s_{2}}$.

عمّم سمولكا منطق الترتيب المرتب للسماح بتعدد الأشكال البارامتري . ^{[ 3 ] [ 4 ]} في إطاره، تُعمّم تعريفات الفرز الفرعي إلى تعبيرات الأنواع المعقدة. كمثال برمجي، الفرز البارامتري${\displaystyle {\text{list}}(X)}$يجوز الإعلان (مع${\displaystyle X}$(باعتباره مُعامل نوع كما في قالب C++ )، ومن تعريف فرز فرعي${\displaystyle {\text{int}}\subseteq {\text{float}}}$العلاقة${\displaystyle {\text{list}}({\text{int}})\subseteq {\text{list}}({\text{float}})}$يتم استنتاج ذلك تلقائيًا، مما يعني أن كل قائمة من الأعداد الصحيحة هي أيضًا قائمة من الأعداد العشرية.

عمّم شميدت-شاوس منطق الترتيب المصنف للسماح بتصريحات المصطلحات. ^{[ 5 ]} على سبيل المثال، بافتراض تصريحات الفرز الفرعي${\displaystyle {\text{even}}\subseteq {\text{int}}}$و${\displaystyle {\text{odd}}\subseteq {\text{int}}}$إعلان مصطلح مثل${\displaystyle \forall i:{\text{int}}.\;(i+i):{\text{even}}}$يسمح هذا بتعريف خاصية جمع الأعداد الصحيحة التي لا يمكن التعبير عنها عن طريق التحميل الزائد العادي.

• المنطق الفئوي
• منطق الرتبة الأولى §  منطق متعدد الأنواع

تتضمن الأوراق البحثية المبكرة حول منطق الأنواع المتعددة ما يلي:

• وانغ، هاو (1952). "منطق النظريات متعددة الأنواع". مجلة المنطق الرمزي . 17 (2): 105-116 . doi : 10.2307/2266241 . JSTOR 2266241 . ، تم جمعها في كتاب المؤلف " الحوسبة، المنطق، الفلسفة: مجموعة من المقالات" ، بكين: دار النشر العلمية؛ دوردريخت: كلوير الأكاديمية، 1990.
• جيلمور، بي سي (1958). "إضافة إلى "منطق النظريات المتعددة الأنواع"" (PDF) . تكوين الرياضيات . 13 : 277-281 .
• أ. أوبرشيلب (1962). "Unter suchungen zur mehrsortigen Quantorenlogik" . الرياضيات أنالن . 145 (4): 297-333 . دوى : 10.1007 / bf01396685 . S2CID 123363080 . مؤرشف من الأصل بتاريخ 2015-02-20 . تم الاسترجاع 2013/09/11 . 
• إف. جيفري بيليتييه (1972). "التصنيف الكمي والتصنيف الكمي المقيد" (ملف PDF) . دراسات فلسفية . 23 (6): 400-404 . doi : 10.1007/bf00355532 . S2CID 170303654 . 

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