المنطق الفئوي
المنطق الفئوي هو فرع من الرياضيات يُطبَّق فيه أدوات ومفاهيم نظرية الفئات على دراسة المنطق الرياضي . ويُعرف أيضًا بارتباطه الوثيق بعلم الحاسوب النظري . [ 1 ] وبشكل عام، يُمثِّل المنطق الفئوي كلاً من بناء الجملة والدلالة بواسطة فئة ، والتفسير بواسطة دالة . يوفر الإطار الفئوي خلفية مفاهيمية ثرية للبنى المنطقية ونظرية الأنواع . وقد أصبح هذا الموضوع معروفًا بهذه المصطلحات منذ حوالي عام 1970.
ملخص
توجد ثلاثة مواضيع مهمة في المنهج التصنيفي للمنطق:
- الدلالات الفئوية
- يُقدّم المنطق الفئوي مفهوم البنية المُقَيَّمة في فئة C، مع ظهور المفهوم النظري الكلاسيكي للبنية في الحالة الخاصة التي تكون فيها C فئة المجموعات والدوال . وقد أثبت هذا المفهوم جدواه عندما يفتقر المفهوم النظري للمجموعات إلى العمومية و/أو يكون غير ملائم. ويُعدّ نمذجة RAG Seely لنظريات غير تنبؤية مختلفة ، مثل النظام F ، مثالًا على فائدة الدلالات الفئوية.
- وقد تبين أن الروابط المنطقية لما قبل التصنيف تُفهم بشكل أوضح باستخدام مفهوم الدالة المرافقة ، وأن الكميات تُفهم أيضاً بشكل أفضل باستخدام الدوال المرافقة. [ 2 ]
- اللغات الداخلية
- يمكن اعتبار هذا بمثابة صياغة رسمية وتعميم لأسلوب البرهان عن طريق تتبع المخططات . إذ يتم تعريف لغة داخلية مناسبة تُسمي المكونات ذات الصلة بفئة ما، ثم تُطبق الدلالات الفئوية لتحويل التأكيدات في منطق اللغة الداخلية إلى عبارات فئوية مقابلة. وقد حقق هذا نجاحًا كبيرًا في نظرية التوبوس ، حيث تُمكّن اللغة الداخلية للتوبوس، جنبًا إلى جنب مع دلالات المنطق الحدسي ذي الرتبة العليا في التوبوس، من التفكير في كائنات ومورفيزمات التوبوس كما لو كانت مجموعات ودوال. [ 3 ] وقد نجح هذا في التعامل مع التوبوس التي تحتوي على "مجموعات" ذات خصائص غير متوافقة مع المنطق الكلاسيكي . ومن الأمثلة البارزة على ذلك نموذج دانا سكوت لحساب لامدا غير المُنمذج من حيث الكائنات التي تتراجع إلى فضاء دوالها الخاص . ومثال آخر هو نموذج موجي -هايلاند للنظام F من خلال فئة فرعية كاملة داخلية للتوبوس الفعال لمارتن هايلاند .
- بناء نماذج المصطلحات
- في كثير من الحالات، توفر الدلالات الفئوية لمنطق ما أساسًا لإقامة تطابق بين النظريات في ذلك المنطق وحالات نوع مناسب من الفئات. ومن الأمثلة الكلاسيكية على ذلك التطابق بين نظريات منطق المعادلات βη على حساب لامدا ذي النوع البسيط والفئات المغلقة الديكارتية . ويمكن عادةً وصف الفئات الناشئة عن النظريات عبر بناء نماذج المصطلحات، وصولًا إلى التكافؤ ، بخاصية شاملة مناسبة . وقد مكّن هذا من إثبات خصائص ما وراء النظرية لبعض المنطق باستخدام جبر فئوي مناسب . فعلى سبيل المثال، قدّم فريد برهانًا على خاصيتي الفصل والوجود للمنطق الحدسي بهذه الطريقة.
هذه المواضيع الثلاثة مترابطة. تتكون الدلالات الفئوية للمنطق من وصف فئة من الفئات المهيكلة المرتبطة بفئة النظريات في ذلك المنطق عن طريق الاقتران، حيث يعطي العاملان في الاقتران اللغة الداخلية لفئة مهيكلة من جهة، ونموذج المصطلح لنظرية من جهة أخرى.
انظر أيضاً
ملحوظات
- ↑ جوجين، جوزيف؛ موساكوفسكي، تيل؛ دي بايفا، فاليريا؛ رابي، فلوريان؛ شرودر، لوتز (2007). "نظرة مؤسسية على المنطق الفئوي" (ملف PDF) . المجلة الدولية للبرمجيات والمعلوماتية . 1 (1): 129-152 . CiteSeerX 10.1.1.126.2361 .
- ↑ لوفير 1971 ، الكميات والحزم
- ↑ ألوفي 2009
مراجع
- الكتب
- أبرامسكي، سامسون؛ غاباي، دوف (2001). المنطق والأساليب الجبرية . دليل المنطق في علوم الحاسوب. المجلد 5. مطبعة جامعة أكسفورد. ISBN 0-19-853781-6.
- ألوفي، باولو (2009). الجبر: الفصل 0 ( الطبعة الأولى). الجمعية الأمريكية للرياضيات. الصفحات 18-20 . ISBN 978-1-4704-1168-8.
- جاباي، د.م.؛ كاناموري، أ.؛ وودز، ج.، محرران. (2012). المجموعات والامتدادات في القرن العشرين . دليل تاريخ المنطق. المجلد 6. نورث هولاند. ISBN 978-0-444-51621-3.
- كينت، ألين؛ ويليامز، جيمس ج. (1990). موسوعة علوم وتكنولوجيا الحاسوب . مارسيل ديكر. ISBN 0-8247-2272-8.
- بار، م.؛ ويلز ، س. (1996). نظرية الفئات لعلوم الحاسوب ( الطبعة الثانية). برنتيس هول. ISBN 978-0-13-323809-9.
- لامبيك، ج .؛ سكوت، ب. ج. (1988). مقدمة في المنطق الفئوي من الرتبة العليا . دراسات كامبريدج في الرياضيات المتقدمة. المجلد 7. مطبعة جامعة كامبريدج. ISBN 978-0-521-35653-4.
- لوفير، إف دبليو ؛ روزبروغ، آر. (2003). المجموعات في الرياضيات . مطبعة جامعة كامبريدج. ISBN 978-0-521-01060-3.
- لوفير، إف دبليو؛ شانيل، إس إتش (2009). الرياضيات المفاهيمية: مقدمة أولية للفئات ( الطبعة الثانية). مطبعة جامعة كامبريدج. ISBN 978-1-139-64396-2.
أوراق بحثية رائدة
- لوفير، ف. و. (نوفمبر 1963). "الدلالات الوظيفية للنظريات الجبرية" . وقائع الأكاديمية الوطنية للعلوم . 50 ( 5): 869-872 . Bibcode : 1963PNAS...50..869L . doi : 10.1073 / pnas.50.5.869 . JSTOR 71935. PMC 221940. PMID 16591125 .
- — (ديسمبر 1964). "النظرية الأولية لفئة المجموعات" . وقائع الأكاديمية الوطنية للعلوم . 52 (6 ) : 1506-1511 . Bibcode : 1964PNAS...52.1506L . doi : 10.1073 / pnas.52.6.1506 . JSTOR 72513. PMC 300477. PMID 16591243 .
- — (1971). “المحددات الكمية والحزم”. الأعمال : المؤتمر الدولي للرياضيات نيس 1-10 سبتمبر 1970. حانة. Sous La Direction Du Comite D'organisation Du Congres . غوتييه فيلارز. ص 1506 – 11. OCLC 217031451 . زبل 0261.18010 .
للمزيد من القراءة
- ماكاي، مايكل ؛ رييس، غونزالو إي. (1977). المنطق الفئوي من الدرجة الأولى . سلسلة محاضرات في الرياضيات. المجلد 611. سبرينغر. doi : 10.1007/BFb0066201 . ISBN 978-3-540-08439-6.
- لامبيك، ج.؛ سكوت، ب. ج. (1988). مقدمة في المنطق الفئوي من الرتبة العليا . دراسات كامبريدج في الرياضيات المتقدمة. المجلد 7. مطبعة جامعة كامبريدج. ISBN 978-0-521-35653-4.مقدمة سهلة الفهم إلى حد ما، ولكنها قديمة بعض الشيء. وقد تم تطوير المنهج التصنيفي للمنطق ذي الرتبة العليا على الأنواع متعددة الأشكال والتابعة إلى حد كبير بعد نشر هذا الكتاب.
- جاكوبس، بارت (1999). المنطق الفئوي ونظرية الأنواع . دراسات في المنطق وأسس الرياضيات. المجلد 141. نورث هولاند، إلسيفير. ISBN 0-444-50170-3.دراسة شاملة كتبها عالم حاسوب، تغطي منطق الرتبة الأولى ومنطق الرتب العليا، بالإضافة إلى الأنواع متعددة الأشكال والأنواع التابعة. ويركز الكتاب على الفئة الليفية كأداة شاملة في المنطق الفئوي، وهو أمر ضروري للتعامل مع الأنواع متعددة الأشكال والأنواع التابعة.
- بيل، جون لين (2001). "تطور المنطق الفئوي" . في: غاباي، د.م.؛ غوينتنر، فرانز (محرران). دليل المنطق الفلسفي . المجلد 12 ( الطبعة الثانية). سبرينغر. الصفحات 279-361 . ISBN 978-1-4020-3091-8.النسخة متاحة على الإنترنت في الصفحة الرئيسية لجون بيل.
- ماركيز، جان بيير؛ رييس، غونزالو إي. “تاريخ المنطق القاطع 1963-1977” . جاباي، كاناموري وودز 2012 . ص 689 – 800. نسخة أولية .
- أوودي، ستيف (12 يوليو 2024). "المنطق الفئوي" . ملاحظات المحاضرة .
- لوري، جاكوب . "المنطق الفئوي (278x)" . ملاحظات المحاضرة .
فئات :
- المنطق الفئوي
- أنظمة المنطق الصوري
- علوم الحاسوب النظرية