نظرية الأنواع

عمومًا، النتيجة المرجوة من البرهان في نظرية الأنواع هي إثبات وجود نوع محدد . ^{[ 17 ]} مشكلة تحديد وجود نوع محدد (يُشار إليها اختصارًا بـ${\displaystyle \exists t.\Gamma \vdash t:\tau$ ?} ⁠ ) هو:

بالنظر إلى السياق${\displaystyle \Gamma }$ونوع​​${\displaystyle \tau }$⁠ ، قرر ما إذا كان هناك مصطلح ⁠${\displaystyle t}$التي يمكن تعيين النوع لها${\displaystyle \tau }$في بيئة النوع${\displaystyle \Gamma }$⁠ .

تُظهر مفارقة جيرارد أن سكنى النوع ترتبط ارتباطًا وثيقًا باتساق نظام النوع مع تناظر كاري-هوارد. ولكي يكون هذا النظام سليمًا، يجب أن يحتوي على أنواع غير مسكونة.

تتضمن نظرية الأنواع عادةً عدة قواعد، بما في ذلك قواعد تتعلق بما يلي:

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

أيضًا، لكل نوع من أنواع "حسب القاعدة"، هناك 4 أنواع مختلفة من القواعد:

• تحدد قواعد "تكوين النوع" كيفية إنشاء النوع
• تحدد قواعد "إدخال المصطلحات" المصطلحات الأساسية ووظائف البناء، مثل "الزوج" و "S".
• تحدد قواعد "حذف المصطلحات" الوظائف الأخرى مثل "الأول" و"الثاني" و"R".
• تحدد قواعد "الحساب" كيفية إجراء الحساب باستخدام الدوال الخاصة بالنوع.

للاطلاع على أمثلة للقواعد، يمكن للقارئ المهتم الرجوع إلى الملحق أ.2 من كتاب نظرية النوع المتماثل ، ^{[ 15 ]} أو قراءة نظرية النوع الحدسية لمارتن-لوف. ^{[ 18 ]}

اقترح بير مارتن-لوف نظريته الحدسية للأنواع كأساس للرياضيات البنائية . ^{[ 14 ]} تتطلب الرياضيات البنائية عند إثبات "وجود"${\displaystyle x}$مع ملكية${\displaystyle P(x)}$" ، يجب على المرء أن يبني شيئاً معيناً${\displaystyle x}$وإثبات امتلاكها للعقارات${\displaystyle P}$في نظرية الأنواع، يتم تحقيق الوجود باستخدام نوع المنتج التابع، ويتطلب إثباته مصطلحًا من هذا النوع.

من أمثلة البرهان غير البنّاء البرهان بالتناقض . الخطوة الأولى هي افتراض أن${\displaystyle x}$غير موجود، ودحضه بالتناقض. والنتيجة من هذه الخطوة هي "ليس الأمر كذلك".${\displaystyle x}$"غير موجود". الخطوة الأخيرة هي، من خلال النفي المزدوج، استنتاج أن${\displaystyle x}$موجود. لا تسمح الرياضيات البنائية بالخطوة الأخيرة المتمثلة في إزالة النفي المزدوج للاستنتاج بأن${\displaystyle x}$موجود. ^{[ 19 ]}

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

تُجري العديد من البرامج التي تعمل بنظرية الأنواع (مثل برامج إثبات النظريات التفاعلية) استدلالًا للأنواع أيضًا. وهذا يُمكّنها من اختيار القواعد التي يقصدها المستخدم، مع تقليل الإجراءات التي يقوم بها المستخدم.

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

• تتوافق الفئات المغلقة الديكارتية مع حساب التفاضل والتكامل λ المكتوب ( لامبيك ، 1970)؛
• تتوافق C-monoids (الفئات التي تحتوي على منتجات وأسس وكائن واحد غير طرفي) مع حساب λ غير المصنف (الذي لاحظه لامبيك ودانا سكوت بشكل مستقل حوالي عام 1980)؛
• تتوافق الفئات المغلقة الديكارتية المحلية مع نظريات من نوع مارتن-لوف (سيلي، 1984).

وقد كان التفاعل، المعروف باسم المنطق الفئوي ، موضوعًا للبحث النشط منذ ذلك الحين؛ انظر على سبيل المثال دراسة جاكوبس (1999).

تسعى نظرية النوع المتماثل إلى الجمع بين نظرية النوع ونظرية الفئات. وتركز على المساواة، لا سيما المساواة بين الأنواع. وتختلف نظرية النوع المتماثل عن نظرية النوع الحدسية بشكل رئيسي في طريقة تعاملها مع نوع المساواة. في عام 2016، طُرحت نظرية النوع المكعبة ، وهي نظرية نوع متماثل مع تطبيع. ^{[ 23 ] [ 24 ]}

تُسمى الأنواع الأساسية بالذرات، ويُعرف المصطلح الذي يكون نوعه ذرة بالمصطلح الذري. ومن المصطلحات الذرية الشائعة في نظريات الأنواع الأعداد الطبيعية ، والتي غالبًا ما يُرمز لها بالنوع ⁠${\displaystyle {\mathsf {nat}}}$قيم المنطق البولياني (​${\displaystyle {\texttt {true}}}$و​​${\displaystyle {\texttt {false}}}$) ، مُشار إليه بالنوع${\displaystyle {\mathsf {bool}}}$والمتغيرات الرسمية ،التي قد يختلف نوعها. ^{[ 17 ]} على سبيل المثال، قد تكون المصطلحات التالية مصطلحات ذرية.

• ${\displaystyle 42:{\mathsf {nat}}}$
• ${\displaystyle {\texttt {true}}:{\mathsf {bool}}}$
• ${\displaystyle x:{\mathsf {nat}}}$
• ${\displaystyle y:{\mathsf {bool}}}$

بالإضافة إلى المصطلحات الذرية، تسمح معظم نظريات الأنواع الحديثة أيضًا بالدوال . تُعرّف أنواع الدوال برمز السهم، وتُعرّف استقرائيًا : إذا${\displaystyle \sigma }$و${\displaystyle \tau }$إذا كانت أنواعًا، فإن الترميز${\displaystyle \sigma \to \tau }$هو نوع دالة تأخذ مُعاملًا من نوع${\displaystyle \sigma }$ويعيد مصطلحًا من النوع ⁠${\displaystyle \tau }$تُعرف أنواع هذا ^الشكل بالأنواع البسيطة . ^[ 17 ^]

قد يتم تعريف بعض المصطلحات مباشرةً على أنها ذات نوع بسيط، مثل المصطلح التالي، ⁠${\displaystyle \mathrm {add} }$، والتي تأخذ عددين طبيعيين بالتسلسل وتعيد عددًا طبيعيًا واحدًا.

${\displaystyle \mathrm {add}$ :{\mathsf {nat}}\to ({\mathsf {nat}}\to {\mathsf {nat}})}

بالمعنى الدقيق للكلمة، يسمح النوع البسيط بمدخل واحد ومخرج واحد فقط، لذا فإن القراءة الأكثر دقة للنوع المذكور أعلاه هي كالتالي:${\displaystyle \mathrm {add} }$هي دالة تأخذ عددًا طبيعيًا كمدخل وتعيد دالة على الشكل التالي :${\displaystyle {\mathsf {nat}}\to {\mathsf {nat}}}$توضح الأقواس أن${\displaystyle \mathrm {add} }$لا يمتلك النوع ⁠${\displaystyle ({\mathsf {nat}}\to {\mathsf {nat}})\to {\mathsf {nat}}}$، وهي دالة تأخذ دالة من الأعداد الطبيعية وتعيد عددًا طبيعيًا. الاصطلاح هو أن السهم يكون تجميعيًا من اليمين ، لذا يمكن حذف الأقواس من ⁠${\displaystyle \mathrm {add} }$نوع ⁠ . ^{[ 17 ]}

يمكن إنشاء حدود دالة جديدة باستخدام تعابير لامدا ، وتُسمى حدود لامدا. تُعرَّف هذه الحدود أيضًا استقرائيًا: حد لامدا له الشكل التالي :${\displaystyle (\lambda v.t)}$، حيث${\displaystyle v}$هو متغير رسمي و${\displaystyle t}$هو مصطلح، ونوعه مُشار إليه${\displaystyle \sigma \to \tau }$، حيث${\displaystyle \sigma }$هو نوع من${\displaystyle v}$، و${\displaystyle \tau }$هو نوع من${\displaystyle t}$⁠ . ^{[ 17 ]} يمثل مصطلح lambda التالي دالة تقوم بمضاعفة عدد طبيعي مدخل.

${\displaystyle (\lambda x.\mathrm {add} \,x\,x):{\mathsf {nat}}\to {\mathsf {nat}}}$

المتغير هو${\displaystyle x}$ويجب أن يكون لها نوع (ضمنياً من نوع مصطلح لامدا)${\displaystyle {\mathsf {nat}}}$. المصطلح${\displaystyle \mathrm {add} \,x\,x}$لديه نوع ⁠${\displaystyle {\mathsf {nat}}}$، وهو ما يتضح من خلال تطبيق قاعدة استدلال تطبيق الدالة مرتين. وبالتالي، فإن مصطلح لامدا من النوع${\displaystyle {\mathsf {nat}}\to {\mathsf {nat}}}$وهذا يعني أنها دالة تأخذ عددًا طبيعيًا كوسيط وتعيد عددًا طبيعيًا.

مصطلح لامدا هو دالة مجهولة ^{[ d ]} لأنه لا يحمل اسمًا. يظهر مفهوم الدوال المجهولة في العديد من لغات البرمجة.

تكمن قوة نظريات الأنواع في تحديد كيفية دمج المصطلحات عن طريق قواعد الاستدلال . ^{[ 5 ]} كما أن نظريات الأنواع التي تتضمن دوالًا تتضمن أيضًا قاعدة الاستدلال الخاصة بتطبيق الدالة : إذا${\displaystyle t}$هو مصطلح من النوع ⁠${\displaystyle \sigma \to \tau }$، و${\displaystyle s}$هو مصطلح من النوع ⁠${\displaystyle \sigma }$ثم تطبيق${\displaystyle t}$إلى​${\displaystyle s}$⁠ ، غالباً ما تُكتب ⁠${\displaystyle (t\,s)}$، من النوع${\displaystyle \tau }$على سبيل المثال ، إذا كان المرء يعرف رموز الأنواع${\displaystyle 0:{\textsf {nat}}}$،​​${\displaystyle 1:{\textsf {nat}}}$، و​${\displaystyle 2:{\textsf {nat}}}$⁠ ، ثم يمكن استنتاج رموز الأنواع التاليةمن تطبيق الدالة. ^{[ 17 ]}

• ${\displaystyle (\mathrm {add} \,1):{\textsf {nat}}\to {\textsf {nat}}}$
• ${\displaystyle ((\mathrm {add} \,2)\,0):{\textsf {nat}}}$
• ${\displaystyle ((\mathrm {add} \,1)((\mathrm {add} \,2)\,0)):{\textsf {nat}}}$

تشير الأقواس إلى ترتيب العمليات ؛ ومع ذلك، جرت العادة على أن يكون تطبيق الدوال تجميعيًا من اليسار ، لذا يمكن حذف الأقواس عند الاقتضاء. ^{[ 17 ]} في حالة الأمثلة الثلاثة أعلاه، يمكن حذف جميع الأقواس من المثالين الأولين، ويمكن تبسيط المثال الثالث إلى ⁠${\displaystyle \mathrm {add} \,1\,(\mathrm {add} \,2\,0):{\textsf {nat}}}$⁠ .

تتضمن نظريات الأنواع التي تسمح باستخدام مصطلحات لامدا أيضًا قواعد استدلال تُعرف باسم${\displaystyle \beta }$-التخفيض و${\displaystyle \eta }$الاختزال. وهي تعمم مفهوم تطبيق الدالة على حدود لامدا. وتُكتب رمزياً على النحو التالي:

• ${\displaystyle (\lambda v.t)\,s\rightarrow t[v\colon =s]}$( ⁠${\displaystyle \beta }$( -الاختزال).
• ${\displaystyle (\lambda v.t\,v)\rightarrow t}$، لو${\displaystyle v}$ليس متغيرًا حرًا في${\displaystyle t}$( ⁠${\displaystyle \eta }$( -الاختزال).

يصف الاختزال الأول كيفية تقييم مصطلح لامدا: إذا كان تعبير لامدا${\displaystyle (\lambda v.t)}$يتم تطبيقه على مصطلح ⁠${\displaystyle s}$، يتم استبدال كل ظهور لـ${\displaystyle v}$في${\displaystyle t}$مع​${\displaystyle s}$⁠ . يوضح الاختزال الثاني العلاقة بين تعابير لامدا وأنواع الدوال: إذا${\displaystyle (\lambda v.t\,v)}$إذا كان مصطلحًا لامدا، فلا بد أن يكون كذلك.${\displaystyle t}$هو مصطلح دالة لأنه يتم تطبيقه على${\displaystyle v}$لذلك ، فإن تعبير لامدا يكافئ ببساطة${\displaystyle t}$، حيث يأخذ كلاهما في الاعتبار حجة واحدة ويطبقانها${\displaystyle t}$^{[ 5 ]}​

على سبيل المثال، قد يكون المصطلح التالي${\displaystyle \beta }$-مخفض.

${\displaystyle (\lambda x.\mathrm {add} \,x\,x)\,2\rightarrow \mathrm {add} \,2\,2}$

في نظريات الأنواع التي تُرسّخ أيضًا مفاهيم المساواة بين الأنواع والمصطلحات، توجد قواعد استدلال مقابلة لـ${\displaystyle \beta }$-المساواة و${\displaystyle \eta }$المساواة. ^{[ 17 ]}

النوع الفارغ ليس له حدود. عادةً ما يُكتب النوع${\displaystyle \bot }$أو​${\displaystyle \mathbb {0} }$يُستخدم النوع الفارغ في إثباتات سكن النوع . إذا كان لنوع ما${\displaystyle a}$، من المتسق اشتقاق دالة من النوع${\displaystyle a\to \bot }$ثم​${\displaystyle a}$غير مأهولة بالسكان ، أي أنها لا تملك أي شروط.

يحتوي نوع الوحدة على مصطلح أساسي واحد فقط. يُكتب النوع${\displaystyle \top }$أو${\displaystyle \mathbb {1} }$ويكتب المصطلح المتعارف عليه الوحيد ⁠${\displaystyle \ast }$يُستخدم نوع الوحدة أيضًا في إثباتات سكن النوع. إذا كان لنوع ما${\displaystyle a}$، من المتسق اشتقاق دالة من النوع${\displaystyle \top \to a}$ثم​${\displaystyle a}$مأهولة ، أي يجب أن يكون لها مصطلح واحد أو أكثر .

يحتوي النوع المنطقي على مصطلحين أساسيين فقط. وعادةً ما يُكتب هذا النوع على النحو التالي:${\displaystyle {\textsf {bool}}}$أو${\displaystyle \mathbb {B} }$أو​${\displaystyle \mathbb {2} }$. المصطلحات المتعارف عليها عادة${\displaystyle \mathrm {true} }$و​${\displaystyle \mathrm {false} }$⁠ .

تُطبَّق الأعداد الطبيعية عادةً بأسلوب حساب بيانو . وهناك مصطلح متعارف عليه.${\displaystyle 0:{\mathsf {nat}}}$بالنسبة للصفر. تستخدم القيم الأساسية الأكبر من الصفر تطبيقات متكررة لدالة لاحقة .${\displaystyle \mathrm {S}$ :{\mathsf {nat}}\to {\mathsf {nat}}} ⁠ .

نوع المنتج، ⁠${\displaystyle \times }$يعتمد على نوعين، وعادةً ما تُكتب حدوده على شكل أزواج مرتبة .${\displaystyle (s,t)}$الزوج​${\displaystyle (s,t)}$يحتوي على نوع المنتج ⁠${\displaystyle \sigma \times \tau }$، حيث${\displaystyle \sigma }$هو نوع من${\displaystyle s}$و${\displaystyle \tau }$هو نوع من${\displaystyle t}$. عادةً ما يتم تعريف كل نوع من أنواع المنتجات باستخدام دوال الحذف${\displaystyle \mathrm {first}$ } و ⁠${\displaystyle \mathrm {second}$ :\sigma \times \tau \to \tau } ⁠ .

• ${\displaystyle \mathrm {first} \,(s,t)}$الإرجاع​${\displaystyle s}$، و
• ${\displaystyle \mathrm {second} \,(s,t)}$الإرجاع​${\displaystyle t}$⁠ .

إلى جانب الأزواج المرتبة، يُستخدم هذا النوع لمفهومي الاقتران المنطقي والتقاطع .

يُكتب نوع المجموع إما${\displaystyle +}$أو​${\displaystyle \sqcup }$في لغات البرمجة ، قد يُشار إلى أنواع الجمع باسم الاتحادات الموسومة . كل نوع${\displaystyle \sigma \sqcup \tau }$يتم تعريفها عادةً باستخدام الدوال البانية${\displaystyle \mathrm {left}$ :\sigma \to (\sigma \sqcup \tau )} و ⁠${\displaystyle \mathrm {right}$ :\tau \to (\sigma \sqcup \tau )} ⁠ ، وهيدوال أحادية، ودالة حذف${\displaystyle \mathrm {match}$ :(\sigma \to \rho )\to (\tau \to \rho )\to (\sigma \sqcup \tau )\to \rho } بحيث

• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {left} \,x)}$الإرجاع​${\displaystyle f\,x}$، و
• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {right} \,y)}$الإرجاع​${\displaystyle g\,y}$⁠ .

يُستخدم نوع المجموع لمفهومي الفصل المنطقي والاتحاد .

مع تعدد الأشكال، يمكن تعريف دوال الحذف بشكل عام لجميع أنواع المنتجات على النحو التالي:${\displaystyle \mathrm {first}$ :\forall \,\sigma \,\tau .\sigma \times \tau \to \sigma } and ⁠${\displaystyle \mathrm {second}$ :\forall \,\sigma \,\tau .\sigma \times \tau \to \tau } ⁠ .

• ${\displaystyle \mathrm {first} \,(s,t)}$الإرجاع​${\displaystyle s}$، و
• ${\displaystyle \mathrm {second} \,(s,t)}$الإرجاع​${\displaystyle t}$⁠ .

وبالمثل، يمكن تعريف مُنشئات نوع المجموع لجميع الأنواع الصالحة لأعضاء المجموع على النحو التالي:${\displaystyle \mathrm {left}$ :\forall \,\sigma \,\tau .\sigma \to (\sigma \sqcup \tau )} and ⁠${\displaystyle \mathrm {right}$ :\forall \,\sigma \,\tau .\tau \to (\sigma \sqcup \tau )} ⁠ ، وهيدوال أحادية، ويمكن التعبير عن دالة الحذف كما يلي:${\displaystyle \mathrm {match}$ لكل σ τ ρ .(σ → ρ) → (τ → ρ) → (σ ∪ τ) → ρ بحيث

• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {left} \,x)}$الإرجاع​${\displaystyle f\,x}$، و
• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {right} \,y)}$الإرجاع​${\displaystyle g\,y}$⁠ .

يسمح نوعان شائعان من التبعيات النوعية ، وهما نوع الضرب التابع ونوع المجموع التابع، لنظرية BHK بترميز المنطق الحدسي من خلال العمل كمكافئات للتكميم الكلي والوجودي ؛ ويتم إضفاء الطابع الرسمي على ذلك من خلال تناظر كاري-هوارد . ^{[ 26 ]} ولأنها ترتبط أيضًا بالضرب والجمع في نظرية المجموعات ، فغالبًا ما تُكتب بالرموز .${\displaystyle \Pi }$و​${\displaystyle \Sigma }$، على التوالي.

تُرى أنواع الجمع في أزواج تابعة ، حيث يعتمد النوع الثاني على قيمة الحد الأول. ينشأ هذا بشكل طبيعي في علوم الحاسوب حيث قد تُرجع الدوال أنواعًا مختلفة من المخرجات بناءً على المدخلات. على سبيل المثال، يُعرَّف النوع المنطقي عادةً باستخدام دالة حذف .${\displaystyle \mathrm {if} }$، والتي تأخذ ثلاثة وسائط وتتصرف على النحو التالي.

• ${\displaystyle \mathrm {if} \,{\texttt {true}}\,x\,y}$الإرجاع​${\displaystyle x}$، و
• ${\displaystyle \mathrm {if} \,{\texttt {false}}\,x\,y}$الإرجاع​${\displaystyle y}$⁠ .

التعريفات العادية لـ${\displaystyle \mathrm {if} }$يتطلب${\displaystyle x}$و${\displaystyle y}$أن يكون لهما نفس النوع. إذا سمحت نظرية الأنواع بالأنواع التابعة، فمن الممكن تعريف نوع تابع.${\displaystyle x:{\mathsf {bool}}\,\vdash \,\mathrm {TF} \,x:U\to U\to U}$بحيث

• ${\displaystyle \mathrm {TF} \,{\texttt {true}}\,\sigma \,\tau }$الإرجاع​${\displaystyle \sigma }$، و
• ${\displaystyle \mathrm {TF} \,{\texttt {false}}\,\sigma \,\tau }$الإرجاع​${\displaystyle \tau }$⁠ .

نوع${\displaystyle \mathrm {if} }$ويمكن كتابتها على النحو التالي :${\displaystyle \forall \,\sigma \,\tau .\Pi _{x:{\mathsf {bool}}}.\sigma \to \tau \to \mathrm {TF} \,x\,\sigma \,\tau }$⁠ .

وبناءً على مفهوم تطابق كاري-هوارد، فإن نوع الهوية هو نوع تم تقديمه ليعكس التكافؤ الافتراضي ، على عكس التكافؤ الحكمي (النحوي) الذي توفره نظرية النوع بالفعل.

يتطلب نوع الهوية مصطلحين من نفس النوع، ويكتب بالرمز ⁠${\displaystyle =}$على سبيل المثال، إذا${\displaystyle x+1}$و${\displaystyle 1+x}$إذن، هذه هي الشروط${\displaystyle x+1=1+x}$يُعد نوعًا ممكنًا. تُنشأ المصطلحات الأساسية باستخدام دالة انعكاسية ،${\displaystyle \mathrm {refl} }$. لمصطلح ⁠${\displaystyle t}$، المكالمة${\displaystyle \mathrm {refl} \,t}$يُعيد المصطلح المتعارف عليه الذي ينتمي إلى النوع ⁠${\displaystyle t=t}$⁠ .

إن تعقيدات المساواة في نظرية الأنواع تجعلها موضوع بحث نشط؛ ونظرية نوع التماثل هي مجال بحث بارز يتعامل بشكل أساسي مع المساواة في نظرية الأنواع.

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

تعتمد بعض برامج المساعدة في البرهان ، مثل Rocq (المعروف سابقًا باسم Coq ) و Lean ، على حساب التفاضل والتكامل للإنشاءات الاستقرائية، وهو حساب التفاضل والتكامل للإنشاءات ذات الأنواع الاستقرائية.