الاستقراء والتكرار

في نظرية الأنواع الحدسية (ITT)، وهي فرع من فروع المنطق الرياضي ، يُعد الاستقراء التكراري ميزةً لتعريف نوع ودالة عليه في آنٍ واحد. يُتيح ذلك إنشاء أنواع أكبر من الأنواع الاستقرائية ، مثل الأكوان . وتظل الأنواع المُنشأة قابلةً للتنبؤ ضمن نظرية الأنواع الحدسية.

يُعطى التعريف الاستقرائي من خلال قواعد توليد عناصر نوعٍ ما. ويمكن بعد ذلك تعريف الدوال من هذا النوع بالاستقراء على طريقة توليد عناصره. يُعمم الاستقراء-الاستدعاء الذاتي هذا الوضع، إذ يُمكن تعريف النوع والدالة في آنٍ واحد ، لأن قواعد توليد عناصر النوع يُسمح لها بالإشارة إلى الدالة. ^{[ 1 ]}

يمكن استخدام الاستقراء التكراري لتعريف أنواع كبيرة تشمل مختلف بنيات الكون. وهو يزيد بشكل كبير من قوة نظرية البرهان لنظرية الأنواع. ومع ذلك، لا تزال التعريفات الاستقرائية التكرارية تُعتبر تنبؤية .

نشأت نظرية الاستقراء التكراري من دراساتٍ لقواعد نظرية مارتن-لوف الحدسية للأنواع . تحتوي هذه النظرية على عددٍ من "مُكوِّنات الأنواع" وأربعة أنواع من القواعد لكلٍّ منها. وقد أشار مارتن-لوف إلى أن قواعد كل مُكوِّن نوع تتبع نمطًا يحافظ على خصائص نظرية الأنواع (مثل التطبيع القوي ، والتنبؤ ). بدأ الباحثون بالبحث عن الوصف الأكثر عمومية لهذا النمط، لأنه سيُحدد أنواع مُكوِّنات الأنواع التي يُمكن إضافتها (أو عدم إضافتها!) لتوسيع نظرية الأنواع.

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

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

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

• لا تشير إلى النوع الذي يتم تعريفه
• أن يكون بالضبط من النوع الذي يتم تحديده، أو
• أن تكون دالة تُرجع النوع الذي يتم تعريفه.

في الأنواع الاستقرائية، يمكن أن يعتمد نوع المعامل على معاملات سابقة، لكن لا يمكن أن يشير إلى معاملات من النوع المُعرَّف. أما الأنواع الاستقرائية التكرارية فتتجاوز ذلك: إذ يمكن لأنواع المعاملات أن تشير إلى معاملات سابقة تستخدم النوع المُعرَّف. ويجب أن تكون هذه المعاملات "شبه موجبة".

• تكون دالة تعتمد على مُعامل سابق إذا كان هذا المُعامل مُغلفًا في الدالة التي يتم تعريفها.

لذا، إذا${\displaystyle D}$هو النوع الذي يتم تعريفه و${\displaystyle f}$إذا تم تعريف الدالة (في نفس الوقت)، فإن تعريفات هذه المعاملات تكون موجبة:

• ${\displaystyle a:A}$
• ${\displaystyle d:D}$
• ${\displaystyle g:A\to {\mathsf {Type}}}$
• ${\displaystyle h:A\to D}$
• ${\displaystyle i:A\to B\to D}$
• ${\displaystyle j:g\ a}$ (يعتمد على المعلمات السابقة، والتي لا يوجد أي منها من النوع)${\displaystyle D}$.)

هذا إيجابي جزئياً:

• ${\displaystyle k:(f\ d)\to D}$ (يعتمد على المعامل)${\displaystyle d}$من النوع${\displaystyle D}$ولكن فقط من خلال الاتصال بـ${\displaystyle f}$.)

هذه ليست نتائج إيجابية ولا نتائج إيجابية جزئية:

• ${\displaystyle k:D\to A}$ (${\displaystyle D}$(وهو أحد مُعاملات الدالة.)
• ${\displaystyle l:(A\to D)\to A}$ (يأخذ المعامل دالة تُرجع${\displaystyle D}$لكنه يعود${\displaystyle A}$نفسها.)
• ${\displaystyle m:z\ d}$ (يعتمد على)${\displaystyle d}$من النوع${\displaystyle D}$ولكن ليس من خلال الوظيفة${\displaystyle f}$.)

ومن الأمثلة الشائعة والبسيطة على ذلك مُكوِّن النوع الخاص بكون على غرار تارسكي. وهو يتكون من نوع${\displaystyle U}$ووظيفة${\displaystyle T:U\to {\mathsf {Type}}}$بحيث يكون هناك عنصر من${\displaystyle U}$لكل نوع في نظرية الأنواع (باستثناء${\displaystyle U}$(نفسها!)، والوظيفة${\displaystyle T}$خرائط عناصر${\displaystyle U}$إلى النوع المرتبط.

النوع${\displaystyle U}$يحتوي كل مُنشئ نوع في نظرية الأنواع على دالة إنشاء (أو قاعدة إدخال). أما دالة إنشاء الدوال التابعة فهي كالتالي:

${\displaystyle {\mathsf {constructor}}_{\Pi }(u:U)(u':T(u)\to U):U}$

أي أنه يأخذ عنصرًا${\displaystyle u}$من النوع${\displaystyle U}$سيتم ربط ذلك بنوع المعامل، ودالة.${\displaystyle u'}$بحيث يكون ذلك لجميع القيم${\displaystyle x:T(u)}$،${\displaystyle u'(x)}$يُشير إلى نوع القيمة المُعادة من الدالة (والذي يعتمد على قيمة المُعامل،${\displaystyle x}$). (النهائي${\displaystyle :U}$يشير إلى أن نتيجة المُنشئ هي عنصر من النوع${\displaystyle U}$.)

تنص قاعدة الاختزال (أو قاعدة الحساب) على ما يلي:${\displaystyle T({\mathsf {constructor}}_{\Pi }(u,u'))}$يتقلص إلى${\displaystyle \prod _{x:T(u)}T(u'(x))}$.

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

تم تطبيق الاستقراء والتكرار في Agda و Idris . ^{[ 3 ]}

• الاستقراء-الاستقراء - عمل إضافي يُعرّف نوعًا ومجموعة من الأنواع في الوقت نفسه

• قائمة بمؤلفات بيتر دايبير حول الاستقراء والاستقراء التكراري
• شرائح عرض تتناول الاستقراء التكراري ومشتقاته