النوع الاستقرائي

تُعدّ أنواع W أنواعًا راسخة في نظرية الأنواع الحدسية (ITT). ^{[ 1 ]} وهي تُعمّم الأعداد الطبيعية، والقوائم، والأشجار الثنائية، وأنواع البيانات الأخرى "ذات الشكل الشجري". ليكن U فضاءً من الأنواع . بفرض وجود نوع A  : U وعائلة تابعة B  : A → U ، يُمكن تكوين نوع W.${\displaystyle {\mathsf {W}}_{a:A}B(a)}$يمكن اعتبار النوع A بمثابة "علامات" للمنشئات (التي قد يكون عددها لانهائيًا) للنوع الاستقرائي المُعرَّف، بينما يشير B إلى عدد معاملات كل منشئ (الذي قد يكون لانهائيًا) . كما يمكن فهم أنواع W (أو أنواع M) على أنها أشجار ذات أساس متين (أو غير ذات أساس متين) ذات عقد مُصنَّفة بالعناصر a  : A ، حيث تحتوي العقدة المُصنَّفة بـ a على B ( a ) من الأشجار الفرعية. ^{[ 2 ]} كل نوع W متماثل مع الجبر الأولي لما يُسمى بالدالة متعددة الحدود .

لنفترض أن 0 ، 1 ، 2 ، إلخ، هي أنواع منتهية ذات عناصر 1 _:  1 ، 1: ₂ ، ₂ : 2 ، إلخ. يمكن تعريف الأعداد الطبيعية على أنها من النوع W. $${\displaystyle \mathbb {N}$$ :={\mathsf {W}}_{x:\mathbf {2} }f(x)} مع f  : 2 → U يتم تعريفها بواسطة f (1 ₂ ) = 0 (تمثل الدالة البانية للصفر، والتي لا تأخذ أي وسيطات)، و f (2 ₂ ) = 1 (تمثل دالة الخلف، والتي تأخذ وسيطًا واحدًا).

يمكن تعريف القوائم على نوع A  : U على النحو التالي:${\displaystyle \operatorname {List} (A):={\mathsf {W}}_{(x:\mathbf {1} +A)}f(x)}$أين $${\displaystyle {\begin{aligned}f(\operatorname {inl} (1_{\mathbf {1} }))&=\mathbf {0} \\f(\operatorname {inr} (a))&=\mathbf {1} \end{aligned}}}$$ و1 _هو الساكن الوحيد في 1. قيمة${\displaystyle f(\operatorname {inl} (1_{\mathbf {1} }))}$يتوافق مع مُنشئ القائمة الفارغة، بينما قيمة${\displaystyle f(\operatorname {inr} (a))}$يتوافق مع الدالة البانية التي تضيف عنصرًا إلى بداية قائمة أخرى.

المُنشئ لعناصر النوع W العام${\displaystyle {\mathsf {W}}_{x:A}B(x)}$له نوع $${\displaystyle {\mathsf {sup}}:\prod _{a:A}{\Big (}B(a)\to {\mathsf {W}}_{x:A}B(x){\Big )}\to {\mathsf {W}}_{x:A}B(x).}$$ يمكننا أيضاً كتابة هذه القاعدة بأسلوب برهان الاستنتاج الطبيعي ، $${\displaystyle {\frac {a:A\qquad f:B(a)\to {\mathsf {W}}_{x:A}B(x)}{{\mathsf {sup}}(a,f):{\mathsf {W}}_{x:A}B(x)}}.}$$

تعمل قاعدة الحذف لأنواع W بشكل مشابه للاستقراء البنيوي على الأشجار. إذا، كلما كانت الخاصية (وفقًا لتفسير القضايا كأنواع )${\displaystyle C:{\mathsf {W}}_{x:A}B(x)\to U}$ينطبق هذا على جميع الأشجار الفرعية لشجرة معينة، وينطبق أيضاً على تلك الشجرة، ثم ينطبق على جميع الأشجار.

$${\displaystyle {\frac {w:{\mathsf {W}}_{a:A}B(a)\qquad a:A,\;f:B(a)\to {\mathsf {W}}_{x:A}B(x),\;c:\prod _{b:B(a)}C(f(b))\;\vdash \;h(a,f,c):C({\mathsf {sup}}(a,f))}{{\mathsf {elim}}(w,h):C(w)}}}$$

في نظريات الأنواع الامتدادية، يمكن تعريف أنواع W (أو أنواع M) حتى التشاكل كجبر ابتدائي (أو جبر مشترك نهائي) للدوال متعددة الحدود . في هذه الحالة، تتوافق خاصية الابتدائي (أو النهائي) مباشرةً مع مبدأ الاستقراء المناسب. ^{[ 3 ]} في نظريات الأنواع القصدية مع بديهية التكافؤ الأحادي ، يظل هذا التوافق قائمًا حتى التماثل (المساواة الافتراضية). ^{[ 4 ] [ 5 ] [ 6 ]}

تُعتبر أنواع M ثنائية لأنواع W، وتمثل بيانات استقرائية مشتركة (قد تكون لانهائية) مثل التدفقات . ^{[ 7 ]} ويمكن اشتقاق أنواع M من أنواع W. ^{[ 8 ]}

تتيح هذه التقنية تعريف بعض الأنواع المتعددة التي تعتمد على بعضها البعض. على سبيل المثال، تعريف مسندين للتكافؤ على الأعداد الطبيعية باستخدام نوعين استقرائيين متبادلين في لغة روك:

Inductive even : nat -> Prop := | zero_is_even : even O | S_of_odd_is_even : ( forall n : nat , odd n -> even ( S n )) with odd : nat -> Prop := | S_of_even_is_odd : ( forall n : nat , even n -> odd ( S n )).

بدأ الاستقراء التكراري كدراسة لحدود نظرية الأنواع الاستقرائية. وبمجرد تحديد هذه الحدود، تم تحويلها إلى قواعد تسمح بتعريف أنواع استقرائية جديدة. يمكن لهذه الأنواع أن تعتمد على دالة، ويمكن لهذه الدالة أن تعتمد على النوع، طالما تم تعريف كليهما في آن واحد.

يمكن تعريف أنواع الكون باستخدام الاستقراء والتكرار.

يسمح الاستقراء-الاستقراء بتعريف نوع ومجموعة من الأنواع في الوقت نفسه. لذا، نوع A ومجموعة من الأنواع${\displaystyle B:A\to Type}$.

يُعدّ هذا مجالًا بحثيًا راهنًا في نظرية أنواع التماثل (HoTT). ويختلف هذا عن نظرية أنواع الاستقراء (ITT) في نوع الهوية (المساواة). تُعرّف الأنواع الاستقرائية العليا نوعًا جديدًا بثوابت ووظائف تُنشئ عناصر من هذا النوع، وحالات جديدة من نوع الهوية تربط بينها.

ومن الأمثلة البسيطة على ذلك نوع الدائرة ، والذي يتم تعريفه باستخدام منشئين، ونقطة أساس؛

القاعدة  : دائرة

وحلقة؛

حلقة  : القاعدة = القاعدة .

إن وجود مُنشئ جديد لنوع الهوية يجعل الدائرة نوعًا استقرائيًا أعلى.