💻 computer science

Definitional Inversion, Without Normalisation

यह शोध पत्र एक नवीन डोमेन-सैद्धांतिक प्रमाण तकनीक प्रस्तुत करता है जो नॉर्मलाइजेशन पर निर्भर किए बिना डिपेंडेंट टाइप सिस्टम के लिए डेफिनिशनल इनवर्जन गुणों को स्थापित करता है, जिससे इड्रिस (Idris) और लीन (Lean) जैसे नॉन-नॉर्मलाइजिंग सिस्टम के साथ-साथ टाइप-इन-टाइप (type-in-type) वाले सिस्टम का मेटा-थ्योरिटिक विश्लेषण सक्षम होता है।

मूल लेखक: Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu, Meven Lennon-Bertrand, Paul-André Melliès, Stephanie Weirich

प्रकाशित 2026-07-16

📖 8 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu, Meven Lennon-Bertrand, Paul-André Melliès, Stephanie Weirich

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप एक विशाल, जादुई पुस्तकालय बना रहे हैं जहाँ हर किताब एक गणितीय प्रमाण (mathematical proof) है, और स्वयं अलमारियाँ तर्क (logic) से बनी हैं। यह डिपेंडेंट टाइप सिस्टम (dependent type systems) की दुनिया है, जो Lean और Idris जैसी आधुनिक प्रूफ़ असिस्टेंट्स और प्रोग्रामिंग भाषाओं के पीछे का गुप्त इंजन है। इस दुनिया में नियम अविश्वसनीय रूप से सख्त हैं: यदि आप "नंबरों" के लेबल वाली शेल्फ पर "बिल्ली" रखने की कोशिश करते हैं, तो पुस्तकालय का सुरक्षा तंत्र (टाइप चेकर) तुरंत चिल्लाएगा "त्रुटि!" (Error!) और आपको रोक देगा। यह सुरक्षा डेफिनिशनल इक्वैलिटी (definitional equality) की एक अवधारणा पर टिकी है, जो पुस्तकालय का यह तय करने का तरीका है कि क्या दो चीजें अनिवार्य रूप से एक ही हैं। उदाहरण के लिए, क्या एक "वर्ग" (square) केवल "समान भुजाओं वाला एक आयत" (rectangle with equal sides) है? यदि सिस्टम कहता है कि हाँ, तो वह उन्हें एक समान मानता है।

हालाँकि, इन नियमों की जाँच करना पेचीदा है। पारंपरिक रूप से, पुस्तकालय को सुरक्षित सिद्ध करने के लिए, गणितज्ञों को यह दिखाना पड़ता था कि प्रत्येक पुस्तक को उसके सबसे सरल, सबसे बुनियादी रूप में बदला जा सकता है (एक प्रक्रिया जिसे नॉर्मलाइजेशन (normalization) कहा जाता है)। लेकिन कई आधुनिक, शक्तिशाली पुस्तकालय ऐसे डिज़ाइन किए गए हैं जो अनंत या स्व-संदर्भित (self-referential) होते हैं, जिसका अर्थ है कि उन्हें एक अंतिम रूप में सरल नहीं किया जा सकता। यह एक फ्रैक्टल (fractal) को समतल करने की कोशिश करने जैसा है; आप बस अधिक विवरण पाते रहेंगे। लंबे समय तक, यदि कोई सिस्टम सरल नहीं हो सकता था, तो हम उसे सुरक्षित सिद्ध नहीं कर सकते थे। यह शोध पत्र एक नया तरीका पेश करता है जिससे फ्रैक्टल को पहले समतल किए बिना पुस्तकालय की सुरक्षा की जाँच की जा सकती है।

अनंत पहेली और जादुई दर्पण

एक डिपेंडेंट टाइप सिस्टम को एक विशाल, स्व-जाँचने वाली पहेली के रूप में सोचें। इसके टुकड़े 'टाइप्स' (जैसे "नंबर" या "फंक्शंस") हैं, और लक्ष्य यह सुनिश्चित करना है कि जब आप दो टुकड़ों को आपस में जोड़ते हैं, तो वे पूरी तरह फिट बैठते हैं। इस पहेली का सबसे महत्वपूर्ण नियम डेफिनिशनल इनवर्जन (definitional inversion) है। यह वह तर्क है जो कहता है: "यदि दो जटिल संरचनाएं एक जैसी दिखती हैं, तो उनके हिस्से भी समान होने चाहिए।" उदाहरण के लिए, यदि आपके पास दो फंक्शन टाइप हैं जो समान हैं, तो यह शोध पत्र सिद्ध करता है कि उनके इनपुट टाइप और आउटपुट टाइप भी समान होने चाहिए। यह महत्वपूर्ण है क्योंकि यह कंप्यूटर को जटिल कोड को बिना भ्रमित हुए छोटे टुकड़ों में सुरक्षित रूप से तोड़ने की अनुमति देता है।

दशकों तक, इन टुकड़ों के फिट होने को सिद्ध करने का एकमात्र तरीका कॉन्फ्लुएंस (confluence) (यह जाँचने के लिए कि क्या सरलीकरण के विभिन्न पथ एक ही परिणाम की ओर ले जाते हैं) या लॉजिकल रिलेशंस (logical relations) (यह देखने का एक जटिल तरीका कि टर्म्स कैसे व्यवहार करते हैं) का उपयोग करना था। लेकिन ये पुराने उपकरण विफल हो गए। कॉन्फ्लुएंस तब टूट जाता है जब आप कुछ "एक्सटेंशनल" नियम (जैसे $\eta$ -laws, जो कहते हैं कि एक फंक्शन पूरी तरह से इस बात से परिभाषित होता है कि वह क्या करता है, न कि इस बात से कि वह कैसे लिखा गया है) जोड़ते हैं। लॉजिकल रिलेशंस के लिए आमतौर पर सिस्टम का "नॉर्मलाइजिंग" (रुकने में सक्षम) होना आवश्यक है, जो उन कई वास्तविक-दुनिया के प्रोग्रामिंग भाषाओं को बाहर कर देता है जो अनंत लूप या स्व-संदर्भित प्रकारों की अनुमति देते हैं।

नया दृष्टिकोण: संभावनाओं का एक मानचित्र

लेखक, जो कंप्यूटर वैज्ञानिकों और गणितज्ञों की एक टीम है, डोमेन थ्योरी (domain theory) पर आधारित एक नई रणनीति प्रस्तावित करते हैं। पहेली के टुकड़ों को एक एकल अंतिम आकार में बदलने के बजाय, वे सभी संभावित व्यवहारों का एक मानचित्र बनाते हैं।

कल्पना कीजिए कि आप एक अंधेरे जंगल में एक रहस्यमय जीव की पहचान करने की कोशिश कर रहे हैं।

पुराना तरीका: आप जीव के रुकने और अपने वास्तविक, अंतिम रूप को प्रकट करने का इंतजार करते हैं। यदि जीव कभी नहीं रुकता (क्योंकि वह एक अनंत लूप है), तो आप उसे पहचान नहीं सकते, और जंगल असुरक्षित है।
नया तरीका: आप जीव के रुकने का इंतजार नहीं करते। इसके बजाय, आप उसके पदचिह्नों (footprints) का अवलोकन करते हैं। आप देखते हैं कि वह एक "बायां-पैर" का निशान छोड़ता है, फिर एक "दायां-पैर" का निशान, फिर फिर से एक "बायां-पैर" का निशान। भले ही जीव कभी चलना बंद न करे, फिर भी आप उसके कदमों के पैटर्न को देखकर उसके आकार का अनुमान लगा सकते हैं।

शोध पत्र की भाषा में, इन "पदचिह्नों" को कॉम्पैक्ट एलिमेंट्स (compact elements) या फाइनाइट ऑब्जर्वेशन (finite observations) कहा जाता है। लेखक एक "डोमेन" (एक संरचित स्थान) का निर्माण करते हैं जहाँ प्रत्येक टाइप को अंतिम उत्तर के रूप में नहीं, बल्कि उन सभी सीमित चीजों के सेट के रूप में दर्शाया जाता है जिन्हें हम उसके बारे में देख सकते हैं। वे इस डोमेन को प्रबंधनीय हिस्सों में काटने के लिए फिनिटरी प्रोजेक्टर्स (finitary projectors) नामक तकनीक का उपयोग करते हैं।

उन्होंने क्या पाया

इस "पदचिह्न" पद्धति का उपयोग करते हुए, टीम ने सफलतापूर्वक सिद्ध किया कि डेफिनिशनल इनवर्जन उन प्रणालियों में भी सत्य है जो:

कभी भी सरलीकरण नहीं रोकतीं (non-normalizing), जैसे कि वे जिनमें "टाइप-इन-टाइप" का नियम होता है (जहाँ एक टाइप स्वयं को समाहित कर सकता है)।
$\eta$ -laws को शामिल करती हैं, जो जटिल नियम हैं जो फंक्शन्स और पेयर्स को अधिक सहज बनाते हैं लेकिन पारंपरिक प्रमाण विधियों को तोड़ देते हैं।

उन्होंने इसे MLTT $\eta$ (ए- $\eta$ -लॉज़ के साथ मार्टिन-लॉफ टाइप थ्योरी) नामक टाइप थ्योरी के एक छोटे, कोर संस्करण पर प्रदर्शित किया। उन्होंने दिखाया कि भले ही यह अराजक, संभावित रूप से अनंत प्रणाली हो, यदि दो टाइप समान हैं, तो उनके निर्माण खंड (building blocks) भी समान होने चाहिए। यह एक बड़ी बात है क्योंकि यह सिद्ध करता है कि टाइप सिस्टम का "सुरक्षा जाल" तब भी काम करता है जब सिस्टम को अव्यवस्थित और अनंत होने की अनुमति दी जाती है।

यह क्यों मायने रखता है

लेखकों ने केवल एक छोटे खिलौना सिस्टम के लिए पहेली हल नहीं की; उन्होंने दिखाया कि उनका तरीका मजबूत (robust) है। उन्होंने अपने प्रमाण को निम्नलिखित को शामिल करने के लिए विस्तारित किया:

डिपेंडेंट सम्स (dependent sums) (डेटा के जोड़े)।
यूनिट टाइप्स (unit types) (एक टाइप जिसमें केवल एक मान होता है)।
फिक्स्ड-पॉइंट कॉम्बिनेटर्स (fixed-point combinators) (ऐसे उपकरण जो अनंत पुनरावृत्ति की अनुमति देते हैं)।
पैटर्न मैचिंग के साथ नेचुरल नंबर्स (natural numbers)।
आइडेंटिटी टाइप्स (identity types) (यह सिद्ध करना कि दो चीजें एक ही हैं)।
प्रूफ-इररेलिवेंट प्रोपोजिशन्स (proof-irrelevant propositions) (जहाँ प्रमाण की सामग्री मायने नहीं रखती, केवल उसका अस्तित्व मायने रखता है)।

उन्होंने "स्ट्रिक्ट प्रोपोजिशन्स के ब्रह्मांड" के लिए एक मॉडल भी बनाया, जो दर्शाता है कि उनकी तकनीक Lean, Agoda, और Rocq जैसे वास्तविक-दुनिया के उपकरणों में पाए जाने वाले जटिल फीचर्स को संभाल सकती है।

सीमाएं और भविष्य

शोध पत्र बहुत स्पष्ट है कि यह क्या नहीं करता है। यह यह सिद्ध नहीं करता है कि ये सिस्टम "नॉर्मलाइजिंग" (कि वे हमेशा रुकते हैं) हैं। वास्तव में, यह स्पष्ट रूप से उन सिस्टमों के लिए काम करता है जो नहीं रुकते। यह "न्यूट्रल्स" (वे चर जो अभी भरे नहीं गए हैं) की समस्या को उसी तरह हल नहीं करता जैसे यह क्लोज्ड टर्म्स के लिए करता है, हालांकि यह संकेत देता है कि भविष्य में इसे कैसे किया जा सकता है।

लेखकों ने पहले ही अपने गणितीय प्रमाणों को कोड में बदल दिया है, और तीन अलग-अलग प्रूफ़ असिस्टेंट्स (Agda, Lean, और Rocq) में तीन बार सत्यापित किया है। यह सुझाव देता है कि उनकी विधि केवल एक सैद्धांतिक विचार नहीं है बल्कि एक व्यावहारिक उपकरण है।

निष्कर्ष

यह शोध पत्र ऐसा है जैसे जादुई पुस्तकालय के निर्माताओं को एक नया चश्मा थमाना। पहले, वे पुस्तकालय की सुरक्षा तभी जाँच सकते थे जब किताबें स्थिर और पूर्ण होती थीं। अब, वे उन किताबों की सुरक्षा की जाँच कर सकते हैं जो अभी भी लिखी जा रही हैं, या वे किताबें जो स्वयं को अनंत काल तक संदर्भित करती हैं। अंतिम गंतव्य (रुकना) के बजाय अवलोकनीय व्यवहार (पदचिह्न) पर ध्यान केंद्रित करके, उन्होंने सबसे शक्तिशाली, जटिल और संभावित रूप से अनंत टाइप सिस्टमों को सत्यापित करने का द्वार खोल दिया है। यह "Lean4Lean" और "MetaRocq" जैसे प्रोजेक्ट्स के लिए मार्ग प्रशस्त करता है—ऐसे प्रोजेक्ट्स जहाँ प्रूफ़ असिस्टेंट्स अपने स्वयं के कोड को सत्यापित करते हैं, जिससे गणित और सॉफ्टवेयर बनाने के लिए उपयोग किए जाने वाले उपकरण और भी अधिक विश्वसनीय बन जाते हैं।

तकनीकी सारांश: परिभाषात्मक व्युत्क्रमण (Definitional Inversion), सामान्यीकरण के बिना

समस्या
डिपेंडेंट टाइप सिस्टम्स (Dependent type systems) महत्वपूर्ण प्रूफ़ असिस्टेंट्स (Agda, Lean, Rocq) और प्रोग्रामिंग भाषाओं (Idris, dependent Haskell) का आधार हैं। उनके मेटा-थ्योरेटिक गुणों, विशेष रूप से परिभाषात्मक व्युत्क्रमण सिद्धांतों (injectivity और no-confusion of type constructors) को स्थापित करना, साउंडनेस (soundness), प्रकारों की विशिष्टता (uniqueness of types), और कर्नेल सत्यापन (kernel verification) को सिद्ध करने के लिए आवश्यक है। हालाँकि, मौजूदा मेटा-थ्योरेटिक उपकरण गंभीर सीमाओं का सामना करते हैं:

कन्फ्लुएंस-आधारित दृष्टिकोण (Confluence-based approaches): ये आधुनिक विशेषताओं जैसे $\eta$ -laws के साथ संघर्ष करते हैं। जबकि कन्फ्लुएंस $\beta$ -reduction के लिए काम करता है, $\eta$ -laws (जैसे कि फंक्शन्स या पेयर्स के लिए) और टाइप्ड कन्वर्जन के साथ मिश्रण अक्सर गैर-कन्फ्लुएंट सिस्टम्स या जटिल, गैर-मानक प्रस्तुतियों की आवश्यकता पैदा करता है।
नॉर्मलाइजेशन-आधारित दृष्टिकोण (Logical Relations): पारंपरिक लॉजिकल रिलेशंस नॉर्मल फॉर्म्स के अस्तित्व पर निर्भर करते हैं। वे गैर-नॉर्मलाइजिंग टाइप थ्योरीज (जो व्यवहार में आम हैं, जैसे Type:Type या फिक्स्ड-पॉइंट कॉम्बिनेटर्स का उपयोग करने वाली थ्योरीज) के लिए विफल हो जाते हैं। इसके अलावा, नॉर्मलाइजेशन को सिद्ध करने के लिए एक परिवेशी तर्क (ambient logic) की आवश्यकता होती है जो ऑब्जेक्ट लॉजिक से अधिक शक्तिशाली हो (अक्सर इंडक्शन-रिकर्सन या इम्प्रेडिकेटिविटी की आवश्यकता होती है), जिससे स्वयं के भीतर (जैसे कि Lean4Lean, MetaRocq) प्रूफ असिस्टेंट्स की मेटा-थ्योरी का अध्ययन करना असंभव हो जाता है।

यह शोध पत्र MLTT $\eta$ के विशिष्ट मामले को संबोधित करता है, जो मार्टिन-लॉफ की टाइप थ्योरी का एक रूपांतर है जिसमें डिपेंडेंट प्रोडक्ट्स, $\beta$ और $\eta$ इक्वेशन्स, और एक Type:Type यूनिवर्स शामिल है। यह सिस्टम $\eta$ के कारण कन्फ्लुएंस को विफल करता है और Type:Type के कारण नॉर्मलाइजेशन को विफल करता है, जिससे इसके परिभाषात्मक व्युत्क्रमण गुण अप्राप्त रह जाते हैं।

कार्यप्रणाली (Methodology)
लेखक डोमेन थ्योरी पर आधारित एक नई प्रमाण तकनीक प्रस्तावित करते हैं, विशेष रूप से फिनिटरी प्रोजेक्शन मॉडल्स (finitary projection models) का उपयोग करते हुए। मुख्य अंतर्दृष्टि यह है कि प्रकारों (types) की व्याख्या उनके नॉर्मल फॉर्म्स द्वारा नहीं (जो मौजूद नहीं हो सकते), बल्कि एक स्कॉट डोमेन (Scott domain) में कॉम्पैक्ट एलिमेंट्स के माध्यम से उनके "अवलोकनीय व्यवहार" (observable behavior) द्वारा की जाती है।

डोमेन निर्माण (Domain Construction): लेखक डोमेन $D$ $D$ का निर्माण टाइप कंस्ट्रक्टर्स ( $\Pi$ $Π$ , $\mathcal{U}$ $U$ , आदि) का प्रतिनिधित्व करने वाले रिकर्सिव डोमेन इक्वेशन के समाधान के रूप में करते हैं। डोमेन को कॉम्पैक्ट एलिमेंट्स ( $C_n$ $C_{n}$ ) के एक बढ़ते क्रम के लिमिट के रूप में बनाया गया है।
- महत्वपूर्ण रूप से, मॉडल $\eta$ -laws को संतुष्ट करने के लिए $\bot$ को $\lambda x.\bot$ के रूप में पहचानता है, जबकि $\Pi$ -constructors को $\mathcal{U}$ से अलग रखता है ताकि विच्छेदता (disjointness) सुनिश्चित हो सके।
सिमेंटिक टाइपिंग (Semantic Typing): डोमेन के कॉम्पैक्ट एलिमेंट्स पर एक सिमेंटिक टाइपिंग संबंध परिभाषित किया गया है। यह संबंध फिनिटरी प्रोजेक्टर्स (एक निरंतर मैप $p: D \to D$ जहाँ $p(\alpha) \le \alpha$ और $p(p(\alpha)) = p(\alpha)$ ) का उपयोग करके तैयार किया गया है। एक प्रकार की व्याख्या एक फिनिटरी प्रोजेक्टर के रूप में की जाती है, और एक टर्म को एक प्रकार से संबंधित माना जाता है यदि उसका डेनोटेशन उस प्रोजेक्टर का फिक्स्ड पॉइंट है।
लॉजिकल रिलेशन (Logical Relation): सिंटैक्टिक टर्म्स और सिमेंटिक विटनेस (कॉम्पैक्ट एलिमेंट्स) के ऊपर एक लॉजिकल रिलेशन परिभाषित किया गया है। पारंपरिक लॉजिकल रिलेशंस के विपरीत, जो टाइप नॉर्मल फॉर्म्स पर रिकर्स करते हैं, यह संबंध कॉम्पैक्ट एलिमेंट्स के स्टेज $n$ $n$ और सिमेंटिक विटनेस की संरचना पर रिकर्स करता है।
- यह संबंध ओपन टर्म्स को संभालता है, जहाँ न्यूट्रल टर्म्स को $\bot$ के रूप में व्याख्यायित किया जाता है, जिससे क्रिप्के-शैली (Kripke-style) के क्वांटिफिकेशन की जटिलता से बचा जा सके और ओपन कॉन्टेक्स्ट में भी इनवर्जन का समर्थन किया जा सके।
- इसे हेड रिडक्शन (head reduction) तक परिभाषित किया गया है, जिसमें $\beta$ और $\eta$ नियमों को सीधे लॉजिकल रिलेशन की संरचना में शामिल किया गया है।
एडेक्वसी (Adequacy): लेखक एक एडेक्वसी थ्योरम सिद्ध करते हैं: यदि दो टर्म्स सिंटैक्स में परिभाषात्मक रूप से समान हैं, तो वे लॉजिकल रिलेशन में संबंधित हैं। यह सिंटैक्टिक गुणों (जैसे कि इंजेक्टिविटी) को डोमेन एलिमेंट्स की विच्छेदता (disjointness) से प्राप्त करने की अनुमति देता है।

प्रमुख योगदान

नई प्रमाण तकनीक: नॉर्मलाइजेशन या कन्फ्लुएंस पर निर्भर किए बिना परिभाषात्मक व्युत्क्रमण (इंजेक्टिविटी और नो-कन्फ्यूजन) को सिद्ध करने के लिए एक डोमेन-थ्योरेटिक विधि।
$\eta$ और नॉन-नॉर्मलाइजेशन को संभालना: यह तकनीक $\eta$ -laws और Type:Type (या फिक्स्ड-पॉइंट कॉम्बिनेटर्स) वाले सिस्टम्स के लिए इंजेक्टिविटी को सफलतापूर्वक सिद्ध करती है, जो मानक विधियों के लिए पहले कठिन था।
कमजोर परिवेशी तर्क (Weak Ambient Logic): यह प्रमाण केवल प्राकृतिक संख्याओं पर बुनियादी इंडक्शन पर निर्भर करता है, जिससे उन मजबूत तार्किक सिद्धांतों (जैसे इंडक्शन-रिकर्सन) की आवश्यकता नहीं होती जो नॉर्मलाइजेशन प्रमाणों के लिए आवश्यक हैं। यह इसे स्व-सत्यापन परियोजनाओं (जैसे Lean के भीतर Lean की विशेषताओं को सिद्ध करना) के लिए उपयुक्त बनाता है।
विस्तारशीलता (Extensibility): इस तकनीक को MLTT $\eta$ पर प्रदर्शित किया गया है और इसे निम्नलिखित समृद्ध सिद्धांतों तक विस्तारित किया गया है:
- $\eta$ -laws के साथ डिपेंडेंट सम्स ( $\Sigma$ ) और यूनिट टाइप ($1$)।
- फिक्स्ड-पॉइंट कॉम्बिनेटर ( $Y$ ) के माध्यम से जनरल रिकर्सन।
- पैटर्न मैचिंग के साथ नेचुरल नंबर्स ( $\mathbb{N}$ )।
- ट्रांसपोर्ट के साथ प्रूफ-रिलिवेंट आइडेंटिटी टाइप्स ($Id$)।
- डेफिनिशनल प्रूफ इररेलेवेंस के साथ स्ट्रिक्ट प्रोपोज़िशन्स ( $\text{Prop}$ ) का यूनिवर्स।
मैकेनाइजेशन (Mechanisation): उपरोक्त विभिन्न विस्तारों को कवर करते हुए, परिणाम Agda, Lean, और Rocq में मैकेनाइज किए गए हैं।

परिणाम

$\Pi$ की इंजेक्टिविटी: पेपर सिद्ध करता है कि यदि $\Pi x:A.B \equiv \Pi x:A'.B'$ है, तो $A \equiv A'$ और $B \equiv B'$ ।
विच्छेदता (Disjointness): टाइप कंस्ट्रक्टर्स विच्छेदित हैं (उदाहरण के लिए, $\Pi x:A.B \not\equiv \mathcal{U}$ )।
सबजेक्ट रिडक्शन और प्रोग्रेस: इन इनवर्जन सिद्धांतों के परिणाम के रूप में, लेखक प्रोग्रेस और प्रिजर्वेशन थ्योरम्स को प्राप्त करते हैं, जो एक प्रोग्रामिंग भाषा के रूप में भाषा की साउंडनेस स्थापित करते हैं।
UIP की विफलता: मॉडल यह प्रदर्शित करता है कि इस सिस्टम में यूनिकनेस ऑफ आइडेंटिटी प्रूफ (UIP/K-rule) व्युत्पन्न नहीं किया जा सकता है, क्योंकि डोमेन मॉडल आइडेंटिटी के विभिन्न प्रमाणों के बीच अंतर करता है।

महत्व
यह पेपर दावा करता है कि यह डिपेंडेंट टाइप सिस्टम्स की मेटा-थ्योरी में एक "ब्लाइंड स्पॉट" को भरता है। नॉर्मलाइजेशन से परिभाषात्मक व्युत्क्रमण को अलग करके, यह तकनीक गैर-नॉर्मलाइजिंग सिस्टम्स और समृद्ध इक्वेशनल थ्योरीज (जैसे $\eta$ ) वाले सिस्टम्स के गहन अध्ययन को सक्षम बनाती है, जो आधुनिक प्रूफ असिस्टेंट्स और प्रोग्रामिंग भाषाओं में प्रचलित हैं।

लेखक इस कार्य को Lean4Lean और MetaRocq जैसी परियोजनाओं के लिए एक आधारभूत कदम के रूप में देखते हैं, जिनका लक्ष्य स्वयं के भीतर प्रूफ असिस्टेंट्स की मेटा-थ्योरी को सत्यापित करना है। चूंकि ये परियोजनाएं गोडेल के दूसरे अपूर्णता प्रमेय (Gödel's second incompleteness theorem) के कारण ऑब्जेक्ट लॉजिक के नॉर्मलाइजेशन को मान नहीं सकतीं, इसलिए यह डोमेन-थ्योरेटिक दृष्टिकोण एक व्यवहार्य पथ प्रदान करता है। लेखक इस तकनीक के संभावित अनुप्रयोग उन डिपेंडेंटली टाइप्ड प्रोग्रामिंग भाषाओं के लिए भी सुझाते हैं जो नॉन-टर्मिनेटिंग फीचर्स या ग्रेडुअल टाइपिंग का उपयोग करती हैं, जहाँ पारंपरिक टर्मिनेशन-आधारित मेटा-थ्योरी विफल हो जाती है।