Constructing (Co)inductive Types via Large Sizes

यहाँ बास्टियन लारकर, डेनिएल ओटन और बेनो वैन डेन बर्ग के शोध पत्र "Constructing (Co)inductive Types via Large Sizes" का विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण (Problem Statement)

प्रूफ असिस्टेंट्स (जैसे Agda, Lean, Rocq) निर्भर प्रकार सिद्धांत (dependent type theory) पर निर्भर करते हैं ताकि निरंतरता (consistency) और निर्णयक्षमता (decidability) सुनिश्चित की जा सके। एक महत्वपूर्ण आवश्यकता यह है कि सभी रिकर्सिव फलन (recursive functions) पूर्ण (समाप्त होने वाले/total) होने चाहिए और सभी को-रिकर्सिव फलन (corecursive functions) उत्पादक (productive) होने चाहिए।

• वर्तमान सीमाएँ: अधिकांश प्रणालियाँ सिंटैक्टिक जाँच (जैसे structural recursion या size-change termination) के माध्यम से पूर्णता को लागू करती हैं। ये जाँचें अक्सर प्रतिबंधात्मक, गैर-मॉड्यूलर और कोड रिफैक्टरिंग के प्रति संवेदनशील होती हैं।
• आकारित प्रकार (Sized Types): आकार-आधारित विकल्प "आकारों" (ordinals) का उपयोग करता है जो प्रकारों को एनोटेट करते हैं, जिससे आकार पर वेल्ड-फाउंडेड इंडक्शन (well-founded induction) के माध्यम से समाप्ति सिद्ध की जा सकती है।
• Agda की विसंगति (The Agda Inconsistency): Agda 'sized types' को लागू करता है लेकिन $\infty$ के रूप में एक सबसे बड़े आकार (largest size) को पेश करता है ताकि $\infty$ पर इसके सन्निकटन (approximation) के रूप में पूर्ण इंडक्टिव/को-इंडक्टिव प्रकार को परिभाषित किया जा सके। यह एक तार्किक विसंगति पैदा करता है: सिस्टम $\infty < \infty$ सिद्ध करता है, जो स्ट्रिक्ट वेल-ऑर्डर्स की इरैफ्लेक्सिविटी (irreflexivity) का उल्लंघन करता है।
• पूर्ववर्ती सैद्धांतिक कार्य: पैरामेट्रिक क्वांटिफायर (existential $\exists$ इंडक्टिव के लिए, universal $\forall$ को-इंडक्टिव के लिए) का उपयोग करके इसे ठीक करने के पिछले प्रयास सीमित थे। विशेष रूप से, वे केवल फिनिटली-ब्रांचिंग (finitely-branching) इंडक्टिव प्रकार ही बना सकते थे क्योंकि आकार का प्रकार प्राकृतिक संख्याओं ($\mathbb{N}$) के रूप में व्याख्यायित किया गया था, जिसमें अनंत रूप से ब्रांचिंग करने वाली संरचनाओं के लिए आवश्यक लिमिट ऑर्डिनल्स (limit ordinals) का अभाव था।

लक्ष्य: एक सुसंगत टाइप थ्योरी का निर्माण करना जो सबसे बड़े आकार ($\infty$) पर निर्भर रहने के बजाय, आकारित प्रकारों (sized types) और पैरामेट्रिक क्वांटिफायर का उपयोग करके सभी (को-)इंडक्टिव प्रकारों (अनंत रूप से ब्रांचिंग वाले भी) का समर्थन करती है।

2. कार्यप्रणाली (Methodology)

लेखक इस निर्माण को प्राप्त करने और एक रियलाइज़ेबिलिटी मॉडल (realizability model) के माध्यम से इसकी निरंतरता सिद्ध करने के लिए विशिष्ट विशेषताओं के साथ मार्टिन-लोफ़ टाइप थ्योरी (MLTT) का विस्तार करते हैं।

A. विस्तारित टाइप थ्योरी (The Extended Type Theory)

इसमें मानक MLTT विशेषताएं (universes, $\Sigma$, $\Pi$, identity types) शामिल हैं, साथ ही:

1. आकारों का एक प्रकार (Size):
   • शून्य ($0$) और सक्सेसर ($\uparrow i$) के साथ सुसज्जित।
   • एक प्री-ऑर्डर ($\leq$) द्वारा क्रमबद्ध, जिसे एक 'मेयर प्रोपोजिशन' (mere proposition) के रूप में एनकोड किया गया है।
   • महत्वपूर्ण रूप से: Size एक लार्ज टाइप (large type) है (यूनिवर्स $U$ में नहीं), लेकिन इस पर क्वांटिफिकेशन से छोटे प्रकार प्राप्त किए जा सकते हैं।
2. पैरामेट्रिक क्वांटिफायर (Parametric Quantifiers):
   • $\exists i. A(i)$ (Existential): सन्निकटन के यूनियन (union) का प्रतिनिधित्व करता है। टर्म्स जोड़े $\langle s, a \rangle$ हैं, लेकिन आकार $s$ को एब्स्ट्रैक्ट (abstracted) रखा गया है (इसका पैटर्न-मैच नहीं किया जा सकता)। एलिमिनेशन को छोटे प्रकारों तक सीमित किया गया है।
   • $\forall i. A(i)$ (Universal): सन्निकटन के इंटरसेक्शन (intersection) का प्रतिनिधित्व करता है। फलन किसी भी आकार पर समान रूप से कार्य करते हैं।
   • पैरामेट्रिसिटी एक्सिओम्स (Parametricity Axioms): इसमें ऐसे एक्सिओम शामिल हैं जो यह बताते हैं कि ये क्वांटिफायर टाइप कंस्ट्रक्टर्स के साथ कम्यूट करते हैं (जैसे $\Pi x:A. \exists i. B(x,i) \simeq \exists i. \Pi x:A. \exists j < i. B(x,j)$)। यह इस विचार को आंतरिक बनाता है कि आकारों के साथ समान व्यवहार किया जाता है।
3. वेल्ड-फाउंडेड इंडक्शन (fix):
   • एक फिक्स्पॉइंट ऑपरेटर जो आकारों पर इंडक्शन द्वारा परिभाषा की अनुमति देता है: $fix\ f : \forall i. A(i)$ यदि $f : \forall i. ((\forall j < i. A(j)) \to A(i))$।
   • टाइप चेकिंग की निर्णयक्षमता बनाए रखने के लिए $\beta$-नियम प्रोपोजिशनल (propositional) है (डिफिनिशनल नहीं)।

B. (को-)इंडक्टिव प्रकारों का निर्माण ((Co)inductive Types Construction)

लेखक पॉलीनोमियल एंडोफंक्टर्स ($F$) के लिए इनिशियल अल्जेब्रा और फाइनल को-अल्जेब्रा के रूप में (को-)इंडक्टिव प्रकारों को एनकोड करते हैं।

1. ऑर्डिनल एप्रोक्सिमेशन (Ordinal Approximations): वे आकार-इंडेक्स्ड फंक्टर्स $F[\exists -]$ और $F[\forall -]$ को परिभाषित करते हैं। fix ऑपरेटर का उपयोग करके, वे इन आकार-इंडेक्स्ड फंक्टर्स के लिए इनिशियल अल्जेब्रा ($\mu_3 F$) और फाइनल को-अल्जेब्रा ($\nu_2 F$) का निर्माण करते हैं। ये एक विशिष्ट आकार पर ट्रंकेटेड (truncated) प्रकार का प्रतिनिधित्व करते हैं।
2. क्वांटिफिकेशन के माध्यम से पूर्ण प्रकार (Full Types via Quantification):
   • इंडक्टिव प्रकार: $\mu F := \exists i. (\mu_3 F) i$ के रूप में परिभाषित हैं। अस्तित्वपरक क्वांटिफायर (existential quantifier) उन सभी टर्म्स को एकत्र करता है जो किसी आकार द्वारा सीमित हैं।
   • को-इंडक्टिव प्रकार: $\nu F := \forall i. (\nu_2 F) i$ के रूप में परिभाषित हैं। सार्वभौमिक क्वांटिफायर (universal quantifier) यह सुनिश्चित करता है कि टर्म्स किसी भी गहराई पर अवलोकन योग्य (observable) हों।
3. अनंत रूप से ब्रांचिंग प्रकारों को संभालना (Handling Infinitely-Branching Types): मुख्य नवाचार यह दिखाना है कि पॉलीनोमियल फंक्टर्स अस्तित्वपरक क्वांटिफायर के साथ वीकली कम्यूट (weakly commute) करते हैं। इसके लिए आकारों के अनुक्रमों के सुप्रीमा (suprema/limit ordinals) के अस्तित्व की आवश्यकता होती, जो कि यदि आकार केवल $\mathbb{N}$ हों तो असंभव है।

C. निरंतरता प्रमाण: रियलाइज़ेबिलिटी मॉडल (Consistency Proof: Realizability Model)

सिद्धांत की निरंतरता सिद्ध करने के लिए, लेखक हाइलैंड के इफेक्टिव टोपोस (Effective Topos) पर आधारित एक रियलाइज़ेबिलिटी मॉडल का निर्माण करते हैं।

• प्रकारों की व्याख्या (Interpretation of Types):
  • छोटे प्रकार (Small Types): प्राकृतिक संख्याओं पर पार्शियल इक्विवेलेंस रिलेशंस (PERs) के रूप में व्याख्यायित।
  • बड़े प्रकार (Large Types): असेंबलीज़ (assemblies - सेट विद कंप्यूटेबिलिटी रिलेशंस) के रूप में व्याख्यायित।
• Size की व्याख्या:
  • Size को $\nabla \omega_1$ के रूप में व्याख्यायित किया गया है, जहाँ $\omega_1$ प्रथम अनकाउंटेबल ऑर्डिनल (सभी गणनीय ऑर्डिनल्स का सेट) है।
  • इसे "फुल" रियलाइज़ेबिलिटी रिलेशन दिया गया है, जिसका अर्थ है कि मॉर्फिज्म को सभी आकारों के साथ समान रूप से (पैरामेट्रिक रूप से) व्यवहार करना चाहिए।
• वैलिडेशन (Validation):
  • क्योंकि $\omega_1$ में लिमिट ऑर्डिनल्स शामिल हैं, मॉडल उन पैरामेट्रिसिटी एक्सिओम्स को मान्य करता है जो अनंत रूप से ब्रांचिंग इंडक्टिव प्रकारों के लिए आवश्यक हैं।
  • मॉडल इम्प्रेडिकेटिविटी (impredicativity - बड़े प्रकारों पर क्वांटिफाई करना छोटे प्रकार देता है) और यूनिकनेस ऑफ आइडेंटिटी प्रूफ (UIP) को मान्य करता है, भले ही सिंटैक्स इन्हें मान न रखता हो। यह दर्शाता है कि सिंटैक्स अधिक शक्तिशाली सिद्धांतों (जैसे HoTT) के साथ संगत है।

3. मुख्य योगदान (Key Contributions)

1. (को-)इंडक्टिव प्रकारों का सामान्य निर्माण: पिछले पैरामेट्रिक दृष्टिकोणों के विपरीत, जो फिनिटली-ब्रांचिंग प्रकारों तक सीमित थे, यह कार्य सभी (को-)इंडक्टिव प्रकारों (जैसे ब्रौवर ऑर्डिनल्स, कंस्ट्रक्टिव सेट थ्योरी मॉडल्स) का निर्माण करता है।
2. Agda की विसंगति का समाधान: सबसे बड़े आकार ($\infty$) को पैरामेट्रिक क्वांटिफायर के माध्यम से बदलकर, लेखक एक सुसंगत विकल्प प्रदान करते हैं।
3. पैरामेट्रिक क्वांटिफायर एक तंत्र के रूप में: वे यह प्रदर्शित करते हैं कि आकारों पर $\exists$ और $\forall$ के माध्यम से पैरामेट्रिसिटी को आंतरिक बनाना, गैर-समाप्ति व्यवहार और तार्किक विसंगतियों को रोकने के लिए आवश्यक एब्स्ट्रैक्शन को प्रभावी ढंग से लागू करता है।
4. मजबूत रियलाइज़ेबिलिटी मॉडल: एक ऐसा मॉडल जहाँ Size की व्याख्या $\omega_1$ के रूप में की गई है, वह इस सिद्धांत के लिए एक कठोर सेमेंटिक औचित्य प्रदान करता है, जो यह सिद्ध करता है कि पैरामेट्रिसिटी एक्सिओम्स सुसंगत हैं।

4. परिणाम (Results)

• सैद्धांतिक सुदृढ़ता (Theoretical Soundness): पेपर सिद्ध करता है कि किसी भी पॉलीनोमियल एंडोफंक्टर के लिए इनिशियल अल्जेब्रा और फाइनल को-अल्जेब्रा विस्तारित सिद्धांत के भीतर मौजूद हैं।
• निरंतरता (Consistency): रियलाइज़ेबिलिटी मॉडल पुष्टि करता है कि सिद्धांत सुसंगत है। यह दिखाता है कि पैरामेट्रिसिटी एक्सिओम्स तब मान्य होते हैं जब आकारों को अनकाउंटेबल ऑर्डिनल के रूप में व्याख्यायित किया जाता है।
• संगतता (Compatibility): निर्माणات UIP या इम्प्रेडिकेटिविटी पर निर्भर नहीं हैं, जिससे परिणाम होमोटॉपी टाइप थ्योरी (HoTT) के साथ संगत हो जाते हैं।

5. महत्व और भविष्य का कार्य (Significance and Future Work)

• प्रूफ असिस्टेंट्स पर प्रभाव: यह कार्य Agda जैसे प्रूफ असिस्टेंट्स में वर्तमान विसंगति के बिना साइज़्ड टाइप्स को लागू करने का मार्ग प्रशस्त करता है।
• कंप्यूटेशनल व्यवहार: लेखक स्वीकार करते हैं कि यद्यपि सिद्धांत सुसंगत है, वर्तमान सिंटैक्स में पैरामेट्रिसिटी एक्सिओम्स के लिए कंप्यूटेशनल व्यवहार (reduction rules के रूप में नहीं, बल्कि केवल एक्सिओम के रूप में) का अभाव है। भविष्य के कार्य को इसे ब्रिज टाइप्स या क्यूबिकल टाइप थ्योरी के माध्यम से जोड़ना होगा।
• असमानता की निर्णयक्षमता (Decidability of Inequality): मॉडल यह संकेत देता है कि आकारों पर असमानता सामान्यतः निर्णय योग्य नहीं है। लेखक व्यावहारिक कार्यान्वयन के लिए हाइब्रिड दृष्टिकोण का सुझाव देते हैं।
• सामान्यीकरण (Generalization): मॉडल को अन्य पार्शियल कॉम्बिनेटरी अल्जेब्रा तक विस्तारित किया जा सकता है या इफेक्ट्स और यूनिवैलेंस के साथ एकीकृत किया जा सकता है।