نظرية النوع المتماثل

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

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

قام ستيف أوودي وطالبه مايكل وارن ببناء أول نماذج متعددة الأبعاد لنظرية النوع القصدي عام ٢٠٠٥ باستخدام فئات نموذج كويلين . عُرضت هذه النتائج لأول مرة علنًا في مؤتمر FMCS ٢٠٠٦ ^{[ ٥ ] ، حيث ألقى وارن محاضرة بعنوان "نماذج التماثل لنظرية النوع القصدي"، والتي كانت أيضًا بمثابة ملخص أطروحته (ضمت لجنة مناقشة الأطروحة أوودي ونيكولا جامبينو وأليكس سيمبسون). يتضمن ملخص أطروحة وارن [ ٦ ]} ملخصًا لهذه النتائج.

في ورشة عمل لاحقة حول أنواع الهوية في جامعة أوبسالا عام ٢٠٠٦ ^{[ ٧ ]} ، قُدِّمَت محاضرتان حول العلاقة بين نظرية الأنواع القصدية وأنظمة التحليل: الأولى لريتشارد غارنر بعنوان "أنظمة التحليل لنظرية الأنواع" ^{[ ٨ ]} ، والثانية لمايكل وارن بعنوان "فئات النموذج وأنواع الهوية القصدية". ونُوقِشَت أفكارٌ ذات صلة في محاضرات ستيف أوودي بعنوان "نظرية الأنواع للفئات ذات الأبعاد الأعلى"، وتوماس سترايشر بعنوان "أنواع الهوية مقابل الزمر الأوميغا الضعيفة: بعض الأفكار، وبعض المشكلات". وفي المؤتمر نفسه، ألقى بينو فان دن بيرغ محاضرة بعنوان "الأنواع كفئات أوميغا ضعيفة"، حيث عرض فيها الأفكار التي أصبحت فيما بعد موضوع ورقة بحثية مشتركة مع ريتشارد غارنر.

واجهت جميع البنى المبكرة للنماذج ذات الأبعاد الأعلى مشكلة التماسك التي تميز نماذج نظرية الأنواع التابعة، وطُورت حلول متنوعة. أحد هذه الحلول قدمه فويفودسكي عام 2009، وآخر قدمه فان دن بيرغ وغارنر عام 2010. ^{[ 9 ]} وفي النهاية، قدم لومسدين ووارن حلاً عاماً، استناداً إلى بناء فويفودسكي، عام 2014. ^{[ 10 ]}

في مؤتمر PSSL86 عام 2007 ^{[ 11 ]،} ألقى أوودي محاضرة بعنوان "نظرية نوع التماثل" (وكان هذا أول استخدام علني لهذا المصطلح، الذي صاغه أوودي ^{[ 12 ]} ). وقد لخص أوودي ووارن نتائج بحثهما في ورقة بحثية بعنوان "نماذج نظرية التماثل لأنواع الهوية"، والتي نُشرت على خادم ما قبل الطباعة ArXiv عام 2007 ^{[ 13 ]} ونُشرت عام 2009؛ وظهرت نسخة أكثر تفصيلاً في أطروحة وارن بعنوان "الجوانب النظرية للتماثل لنظرية النوع البنائية" عام 2008.

في نفس الفترة تقريبًا، كان فلاديمير فويفودسكي يُجري بحثًا مستقلًا في نظرية الأنواع في سياق البحث عن لغة لصياغة الرياضيات بشكل عملي. في سبتمبر 2006، نشر على قائمة بريد Types مقالًا بعنوان "ملاحظة قصيرة جدًا حول حساب التفاضل والتكامل اللامدا للتماثل "، ^{[ 14 ]} والذي رسم فيه الخطوط العريضة لنظرية أنواع تتضمن منتجات ومجاميع وعوالم تابعة، ونموذجًا لهذه النظرية في مجموعات كان التبسيطية . بدأت المذكرة بالقول: "إن حساب لامدا للتماثل هو نظام أنواع افتراضي (في الوقت الحالي)"، وانتهت بالقول: "في الوقت الحالي، لا يزال الكثير مما ذكرته أعلاه مجرد تخمينات. حتى تعريف نموذج TS في فئة التماثل ليس بالأمر البسيط"، في إشارة إلى قضايا التماسك المعقدة التي لم تُحل حتى عام 2009. تضمنت هذه المذكرة تعريفًا نحويًا لـ"أنواع المساواة" التي زُعم أنها تُفسر في النموذج بواسطة فضاءات المسار، لكنها لم تأخذ في الاعتبار قواعد بير مارتن-لوف لأنواع الهوية. كما صنفت المذكرة العوالم حسب بُعد التماثل بالإضافة إلى الحجم، وهي فكرة تم التخلي عنها لاحقًا في الغالب.

من الناحية التركيبية، افترض بينو فان دن بيرغ في عام 2006 أن سلسلة أنواع الهوية لنوع ما في نظرية الأنواع القصدية يجب أن تتخذ بنية فئة ω، بل وشبه زمرة ω، بالمعنى "الكوني الجبري" لمايكل باتانين. وقد أثبت فان دن بيرغ وغارنر هذا لاحقًا بشكل مستقل في ورقة بحثية بعنوان "الأنواع هي شبه زمر أوميغا ضعيفة" (نُشرت عام 2008)، ^{[ 15 ]} وبيتر لومسدين في ورقة بحثية بعنوان "فئات ω ضعيفة من نظرية الأنواع القصدية" (نُشرت عام 2009) وكجزء من أطروحته للدكتوراه عام 2010 بعنوان "الفئات العليا من نظريات الأنواع". ^{[ 16 ]}

قدّم فويفودسكي مفهوم التليف الأحادي في أوائل عام 2006. ^{[ 17 ]} ومع ذلك، ونظرًا لإصرار جميع عروض نظرية مارتن-لوف على خاصية أن أنواع الهوية، في السياق الفارغ، قد تحتوي فقط على خاصية الانعكاسية، لم يدرك فويفودسكي حتى عام 2009 إمكانية استخدام أنواع الهوية هذه بالتزامن مع الأكوان الأحادية. وعلى وجه الخصوص، لم تظهر فكرة إمكانية إدخال الأحادية ببساطة عن طريق إضافة بديهية إلى نظرية مارتن-لوف القائمة إلا في عام 2009. ^{[ أ ] [ ب ]}

في عام ٢٠٠٩ أيضًا، وضع فويفودسكي مزيدًا من التفاصيل حول نموذج لنظرية الأنواع في مجمعات كان ، ولاحظ أن وجود تليف كان شامل يمكن استخدامه لحل مشكلات التماسك في النماذج الفئوية لنظرية الأنواع. كما أثبت، باستخدام فكرة أ. ك. بوسفيلد، أن هذا التليف الشامل أحادي القيمة: فالتليف المرتبط بتكافؤات التماثل الزوجية بين الألياف يكافئ تليف فضاء المسارات للقاعدة.

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

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

كان الحدث المحوري التالي ورشة عمل مصغرة في معهد البحوث الرياضية في أوبرولفاخ في مارس 2011، نظمها ستيف أوودي، وريتشارد غارنر، وبير مارتن-لوف، وفلاديمير فويفودسكي، بعنوان "التفسير الهوموتوبي لنظرية الأنواع البنائية". ^{[ 20 ]} وكجزء من برنامج تعليمي لـ Coq لهذه الورشة، كتب أندريه باور مكتبة Coq صغيرة ^{[ 21 ]} استنادًا إلى أفكار فويفودسكي (ولكن دون استخدام أي من شفرته البرمجية)؛ وأصبحت هذه المكتبة فيما بعد نواة الإصدار الأول من مكتبة "HoTT" Coq ^{[ 22 ]} (يشير أول تعديل لها ^{[ 23 ]} من قِبل مايكل شولمان إلى "التطوير استنادًا إلى ملفات أندريه باور، مع استلهام العديد من الأفكار من ملفات فلاديمير فويفودسكي"). ومن أهم ما انبثق عن اجتماع أوبرولفاخ الفكرة الأساسية للأنواع الاستقرائية العليا، والتي تعود إلى لومسدين، وشولمان، وباور، ووارن. كما قام المشاركون بصياغة قائمة بالأسئلة المفتوحة المهمة، مثل ما إذا كانت بديهية التكافؤ الواحد تحقق المعيارية (لا تزال مفتوحة، على الرغم من حل بعض الحالات الخاصة بشكل إيجابي ^{[ 24 ] [ 25 ]} )، وما إذا كانت بديهية التكافؤ الواحد تحتوي على نماذج غير قياسية (أجاب عليها شولمان بالإيجاب منذ ذلك الحين)، وكيفية تعريف الأنواع (شبه) البسيطة (لا تزال مفتوحة في MLTT، على الرغم من أنه يمكن القيام بذلك في نظام نوع التماثل لفويفودسكي (HTS)، وهي نظرية نوع تحتوي على نوعين متساويين).

بعد ورشة عمل أوبرولفاخ بفترة وجيزة، تم إنشاء موقع ومدونة نظرية أنواع التماثل ^{[ 26 ]} ، وبدأ الموضوع ينتشر تحت هذا الاسم. ويمكن استخلاص فكرة عن بعض التطورات المهمة خلال هذه الفترة من تاريخ المدونة. ^{[ 27 ]}

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

المفهوم الأساسي لنظرية نوع التماثل هو المسار . في نظرية نوع التماثل، النوع${\displaystyle a=b}$هو نوع جميع المسارات من النقطة${\displaystyle a}$مباشرة إلى النقطة${\displaystyle b}$(لذلك، فإن البرهان على نقطة ما هو${\displaystyle a}$يساوي نقطة${\displaystyle b}$هو نفسه المسار من النقطة${\displaystyle a}$مباشرة إلى النقطة${\displaystyle b}$.) لأي نقطة${\displaystyle a}$يوجد مسار من النوع${\displaystyle a=a}$، بما يتوافق مع خاصية الانعكاس للمساواة. مسار من النوع${\displaystyle a=b}$يمكن عكسها، مما يشكل مسارًا من النوع${\displaystyle b=a}$، بما يتوافق مع خاصية التناظر للمساواة. مساران من النوع${\displaystyle a=b}$على التوالي.${\displaystyle b=c}$يمكن دمجها، لتشكيل مسار من النوع${\displaystyle a=c}$وهذا يتوافق مع خاصية التعدي للمساواة.

والأهم من ذلك، بالنظر إلى المسار${\displaystyle p:a=b}$وإثبات لبعض الممتلكات${\displaystyle P(a)}$، يمكن "نقل" البرهان على طول المسار${\displaystyle p}$لتقديم دليل على الملكية${\displaystyle P(b)}$(بمعنى آخر، كائن من نوع${\displaystyle P(a)}$يمكن تحويله إلى كائن من نوع${\displaystyle P(b)}$يتوافق هذا مع خاصية الاستبدال للمساواة . وهنا يبرز فرقٌ هام بين نظرية التكافؤ والرياضيات الكلاسيكية. ففي الرياضيات الكلاسيكية، بمجرد تساوي قيمتين، يصبح التكافؤ متحققًا.${\displaystyle a}$و${\displaystyle b}$تم تأسيسها،${\displaystyle a}$و${\displaystyle b}$يمكن استخدام المصطلحين بشكل متبادل بعد ذلك، دون مراعاة أي تمييز بينهما. ومع ذلك، في نظرية نوع التماثل، قد توجد مسارات متعددة مختلفة.${\displaystyle a=b}$ونقل جسم ما عبر مسارين مختلفين سيؤدي إلى نتيجتين مختلفتين. لذلك، في نظرية التماثل، عند تطبيق خاصية الاستبدال، من الضروري تحديد المسار المستخدم.

بشكل عام، يمكن أن يكون للقضية الواحدة عدة براهين مختلفة. (على سبيل المثال، نوع جميع الأعداد الطبيعية، عند اعتباره قضية، يكون لكل عدد طبيعي برهان عليه). حتى لو كان للقضية برهان واحد فقط${\displaystyle a}$فضاء المسارات${\displaystyle a=a}$قد يكون الأمر غير تافه بطريقة ما. "الاقتراح المجرد" هو أي نوع إما أن يكون فارغًا، أو يحتوي على نقطة واحدة فقط ذات مسار تافه .

لاحظ أن الناس يكتبون${\displaystyle a=b}$ل${\displaystyle Id_{A}(a,b)}$وبالتالي ترك النوع${\displaystyle A}$ل${\displaystyle a,b}$ضمني. لا تخلط بينه وبين${\displaystyle id_{A}:A\to A}$، للدلالة على دالة التطابق على${\displaystyle A}$[ ^{ج ]​}

وظيفتان${\displaystyle f,g:A\rightarrow B}$هي عمليات تماثلية عن طريق التحديد النقطي: ^{[ 29 ] : 2.4.1}

${\displaystyle f\sim g:\equiv \prod _{x:A}f(x)=g(x)}$

أوجه التكافؤ بين نوعين${\displaystyle A}$و${\displaystyle B}$ينتمي إلى كون ما${\displaystyle U}$يتم تعريفها بواسطة الدوال${\displaystyle f:A\rightarrow B}$بالإضافة إلى إثبات وجود عمليات التراجع والمقاطع فيما يتعلق بالتماثلات: ^{[ 29 ] : 2.4.11، 2.4.10}

${\displaystyle A\simeq B:\equiv \sum _{f:A\rightarrow B}{\text{isequiv}}(f)}$، أين

${\displaystyle {\text{isequiv}}(f):\equiv \left(\sum _{g:B\rightarrow A}(f\circ g)\sim id_{B}\right)\times \left(\sum _{h:B\rightarrow A}(h\circ f)\sim id_{A}\right)}$

بالإضافة إلى بديهية التكافؤ الواحدية أدناه، يحصل المرء على "غير دائري"${\displaystyle \infty }$تم توسيع مفهوم "التماثل" ليشمل الهوية. ^{[ 37 ]}

${\displaystyle A\simeq B:\equiv {\text{هناك}}\ f:A\leftrightarrows B:g\ {\text{مع}}\ g\circ f\simeq id_{A}\ {\text{و}}\ f\circ g\simeq id_{B}}$

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

${\displaystyle (A=B)\to (A\simeq B),}$

وهو ما يعبر عن أن الأنواع${\displaystyle A,B}$الأشياء المتساوية، على وجه الخصوص، متكافئة أيضاً.

تنص بديهية التكافؤ الأحادي على أن هذه الدالة هي نفسها تكافؤ. ^{[ 29 ] : 115 [ 18 ] : 4-6} لذلك، لدينا

${\displaystyle (A=B)\simeq (A\simeq B)}$

وبعبارة أخرى، الهوية تعادل التكافؤ. وعلى وجه الخصوص، يمكن القول إن "الأنواع المتكافئة متطابقة". ^{[ 29 ] : 4}

أثبت مارتن هوتزل إسكاردو أن خاصية التكافؤ مستقلة عن نظرية مارتن-لوف للأنواع (MLTT). ^{[ 18 ] : 6 [ د ]} وذلك لأن تكافؤ الأنواع متوافق مع جميع بنيات نظرية الأنواع ^{[ 29 ] : 2.6-2.15} .

يزعم المؤيدون أن تقنية HoTT تُسهّل ترجمة البراهين الرياضية إلى لغة برمجة حاسوبية ، مما يُمكّن برامج البراهين الحاسوبية من التحقق من البراهين المعقدة بسهولة أكبر من ذي قبل. ويجادلون بأن هذا النهج يزيد من قدرة الحواسيب على التحقق من البراهين المعقدة. ^{[ 38 ]} مع ذلك، لا تحظى هذه المزاعم بقبول عالمي، ولا تعتمد العديد من الجهود البحثية وبرامج البراهين على تقنية HoTT.

تعتمد نظرية التماثل (HoTT) على بديهية التكافؤ الأحادي، التي تربط تساوي القضايا المنطقية الرياضية بنظرية التماثل. معادلة مثل${\displaystyle a=b}$هي عبارة رياضية يكون فيها لرمزين مختلفين القيمة نفسها. في نظرية التماثل، يُفهم من ذلك أن الشكلين اللذين يمثلان قيم الرموز متكافئان طوبولوجيًا. ^{[ 38 ]}

يرى جيوفاني فيلدر ، مدير معهد الدراسات النظرية في جامعة ETH زيورخ ، أن علاقات التكافؤ هذه يُمكن صياغتها بشكل أفضل في نظرية التماثل لأنها أكثر شمولية: إذ لا تُفسر نظرية التماثل سبب كون "أ يساوي ب" فحسب، بل تُفسر أيضًا كيفية استنتاج ذلك. أما في نظرية المجموعات، فيجب تعريف هذه المعلومات بشكل إضافي، وهو ما يُصعّب، بحسب مؤيدي نظرية التماثل، ترجمة القضايا الرياضية إلى لغات البرمجة. ^{[ 38 ]}

اعتبارًا من عام 2015، كان العمل البحثي المكثف جاريًا لنمذجة وتحليل السلوك الحسابي لبديهية التكافؤ في نظرية نوع التماثل بشكل رسمي. ^{[ 39 ]}

تُعد نظرية النوع المكعبي إحدى المحاولات لإضفاء محتوى حسابي على نظرية نوع التماثل.

مع ذلك، يُعتقد أن بعض الكائنات، مثل الأنواع شبه التبسيطية، لا يمكن بناؤها دون الرجوع إلى مفهوم ما للمساواة التامة. لذا، طُوِّرت نظريات أنواع ثنائية المستوى تُقسِّم أنواعها إلى أنواع ليفية، تحترم المسارات، وأنواع غير ليفية، لا تحترمها. تُعد نظرية الأنواع الحسابية المكعبة الديكارتية أول نظرية أنواع ثنائية المستوى تُقدِّم تفسيرًا حسابيًا كاملًا لنظرية أنواع التماثل. ^{[ 40 ]}