💻 computer science

Are Dependent Types in Set Theory Feasible?

यह शोध पत्र Lisa प्रूफ़ असिस्टेंट के भीतर टार्स्की-ग्रोथेंडिक सेट थ्योरी (Tarski-Grothendieck set theory) में डिपेंडेंट टाइप्स और यूनिवर्स के एक मेकेनाइज्ड एम्बेडिंग को प्रस्तुत करता है, जो एक सत्यापित, प्रूफ़-प्रोड्यूसिंग टाइप-चेकिंग टैक्टिक को सक्षम बनाता है जो स्वचालित तर्क के लिए मानक सेट-थ्योरेटिक समानता और प्रतिस्थापन नियमों का लाभ उठाता है।

मूल लेखक: Yunsong Yang, Simon Guilloud, Viktor Kunčak

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

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

CC BY 4.0

मूल लेखक: Yunsong Yang, Simon Guilloud, Viktor Kunčak

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

कल्पना कीजिए कि आप एक विशाल, जटिल पुस्तकालय बना रहे हैं। एक सदी से अधिक समय से, इस पुस्तकालय का मानक ब्लूप्रिंट सेट थ्योरी (विशेष रूप से ZFC) रहा है। इसमें, सब कुछ बस एक "डिब्बा" (एक सेट) है जिसमें अन्य डिब्बे रखे हैं। यह एक ठोस, समय-सिद्ध आधार है, लेकिन जब आप जटिल, स्व-संदर्भित (self-referential) संरचनाएं बनाना चाहते हैं, तो यह थोड़ा बोझिल हो सकता है।

हाल के दशकों में, एक नया, अधिक आधुनिक ब्लूप्रिंट जिसे डिपेंडेंट टाइप थ्योरी (Dependent Type Theory) कहा जाता है (जिसका उपयोग Lean और Rocq जैसे टूल्स में किया जाता है), सबका पसंदीदा बन गया है। यह एक ऐसे पुस्तकालय की तरह है जहाँ हर किताब पर एक ऐसा लेबल होता है जो उसके अंदर की सामग्री के आधार पर बदलता रहता है, जिससे अत्यंत सटीक संगठन संभव होता है। हालाँकि, इस ब्लूप्रिंट को बनाना और सत्यापित करना जटिल है। यदि आप इसके आधार में एक छोटी सी भी गलती करते हैं, तो पूरा पुस्तकालय असुरक्षित हो सकता है।

बड़ा सवाल: क्या हम "टाइप थ्योरी" के फैंसी, स्व-संगठित फीचर्स को "सेट थ्योरी" के मजबूत, पुराने ढर्रे वाले आधार के अंदर बना सकते हैं?

यह शोध पत्र कहता है हाँ, और उन्होंने इसे कैसे किया, यहाँ सरल उपमाओं (analogies) का उपयोग करके बताया गया है:

1. अनुवादक (The Embedding)

लेखकों ने एक अनुवादक बनाया जो दोनों भाषाओं को बोल सकता है।

समस्या: सेट थ्योरी स्वाभाविक रूप से "उन फंक्शन्स को नहीं समझती जो अपने इनपुट्स पर निर्भर करते हैं" (dependent types)। यह केवल मानक सेट्स को समझती है।
समाधान: उन्होंने एक डिक्शनरी बनाई जो "टाइप थ्योरी" की अवधारणाओं को "सेट थ्योरी" की अवधारणाओं में अनुवादित करती है।
- उपमा: कल्पना कीजिए कि आपके पास केक बनाने की एक रेसिपी है जो कहती है, "मैदा डालें यदि बैटर पीला है।" सेट थ्योरी नहीं जानती कि रेसिपी के संदर्भ में "यदि" का क्या अर्थ है। उन्होंने इसे एक सख्त नियम में अनुवादित किया: "सभी सामग्रियों के सेट में मैदा केवल तभी शामिल है जब बैटर पीला हो।"
- उन्होंने तर्क (logic) के एक विशेष विस्तार ( $\lambda$ FOL) का उपयोग किया जो इन "सशर्त रेसिपीज़" को मानक गणितीय सेट्स के रूप में लिखने की अनुमति देता है।

2. अनंत अलमारियाँ (Universes)

टाइप थ्योरी में, आपके पास "यूनिवर्स" होते हैं। इन्हें अलमारियों के रूप में सोचें। एक अलमारी किताबों (types) को रखती है, लेकिन उस अलमारी को खुद एक बड़ी अलमारी पर टिकना होता है।

समस्या: मानक सेट थ्योरी में, आप "सभी सेट्स का सेट" नहीं बना सकते (इससे विरोधाभास पैदा होते हैं)। आप अलमारियों की एक अनंत सीढ़ी आसानी से नहीं बना सकते जहाँ प्रत्येक अलमारी नीचे वाली को संभालने के लिए पर्याप्त बड़ी हो।
समाधान: उन्होंने टार्स्की के एक्सिओम (Tarski's Axiom) नामक एक शक्तिशाली गणितीय नियम का उपयोग किया।
- उपमा: कल्पना कीजिए कि आप डिब्बों का एक टॉवर बनाने की कोशिश कर रहे हैं। मानक नियम कहते हैं, "आप एक डिब्बे को दूसरे बहुत बड़े डिब्बे के अंदर नहीं रख सकते।" टार्स्की का एक्सिओम एक जादुई नियम की तरह है जो कहता है, "आपके पास प्रत्येक डिब्बे के लिए, एक सुपर-बॉक्स मौजूद है जो उसे रखने के लिए पर्याप्त बड़ा है, और उस सुपर-बॉक्स को रखने के लिए एक सुपर-सुपर-बॉक्स भी मौजूद है, और यह सिलसिला हमेशा चलता रहेगा।"
- यह उन्हें सेट थ्योरी के भीतर "यूनिवर्स" (अलमारियों) का एक अनंत पदानुक्रम (hierarchy) बनाने की अनुमति देता है, ठीक वैसे ही जैसे टाइप थ्योरी को आवश्यकता होती है।

3. ऑटो-चेकर (Proof-Producing Tactic)

आमतौर पर, जब आप इन सिस्टमों में कोड या प्रमाण (proof) लिखते हैं, तो आपको कंप्यूटर को यह समझाने के लिए मैन्युअल रूप से प्रयास करना पड़ता है कि आपका तर्क सही है।

नवाचार: लेखकों ने एक स्वचालित प्रमाण जनरेटर (automatic proof generator) बनाया है।
- उपमा: कल्पना कीजिए कि आप एक कहानी लिख रहे हैं। आमतौर पर, आपको फुटनोट्स लिखने पड़ते हैं जो समझाते हैं कि आपकी हर पंक्ति का अर्थ क्यों सही है। यह नया टूल एक स्मार्ट संपादक की तरह है जो आपकी कहानी पढ़ता है, तर्क की जांच करता है, और स्वचालित रूप से आपके लिए फुटनोट्स लिख देता है जिसे पुस्तकालय का सुरक्षा गार्ड (सेट थ्योरी कर्नल) समझ सके।
- यदि आप कहते हैं, "यह फंक्शन एक नंबर लेता है और एक लिस्ट लौटाता है," तो टूल स्वचालित रूप से वह गणितीय प्रमाण तैयार करता है जो कहता है, "हाँ, संख्याओं का यह सेट वास्तव में सूचियों (lists) के सेट के भीतर है।"

4. "सबटाइपिंग" का कमाल (The "Subtyping" Trick)

उन्होंने सबटाइपिंग (Subtyping) नामक एक फीचर भी जोड़ा।

अवधारणा: प्रोग्रामिंग में, एक "कुत्ता" (Dog) एक "जानवर" (Animal) का प्रकार है। यदि किसी फंक्शन को एक "जानवर" की आवश्यकता है, तो आप उसे एक "कुत्ता" दे सकते हैं।
चुनौती: शुद्ध सेट थ्योरी में, यह कठिन है क्योंकि सेट्स हमेशा "इस प्रकार का है" (is a kind of) वाले संबंधों के साथ तालमेल नहीं बिठा पाते।
परिणाम: उन्होंने एक विशिष्ट नियम को सिद्ध किया जो इसे उनके सेट थ्योरी अनुवाद के भीतर सुरक्षित रूप से काम करने की अनुमति देता है, लेकिन इसमें कुछ सुरक्षा घेरे (guardrails) भी हैं ताकि "सभी फंक्शन्स का सेट" अस्तित्व में रहने के लिए बहुत बड़ा न हो जाए।

यह क्यों महत्वपूर्ण है?

मान लीजिए कि Lean और Rocq उच्च-तकनीकी, भविष्यवादी पुस्तकालय हैं जो उपयोग में अद्भुत हैं लेकिन उनके आधार जटिल और नाजुक हैं। मान लीजिए कि सेट थ्योरी एक ऐसा पुस्तकालय है जो चट्टानी आधार पर बना है—उबाऊ लेकिन अटूट।

यह शोध पत्र एक पुल बनाने जैसा है।

यह लोगों को उनकी फैंसी, आधुनिक कोड को "टाइप थ्योरी" के अंदाज में लिखने की अनुमति देता है।
यह पुल स्वचालित रूप से इसे "सेट थ्योरी" की भाषा में अनुवादित करता है।
सेट थ्योरी का आधार सत्यापित करता है कि यह 100% सही है।

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

यहाँ युनसोंग यांग, साइमन गिलौड और विक्टर कुन्चाक के शोध पत्र "Are Dependent Types in Set Theory Feasible?" का विस्तृत तकनीकी सारांश दिया गया है।

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

यह शोध पत्र इंटरैक्टिव थ्योरम प्रूविंग (जैसे Lean 4, Rocq) में डिपेंडेंट टाइप थ्योरी (DTT) के प्रभुत्व और ज़र्मेलो-फ्रेंकेल सेट थ्योरी विद चॉइस (ZFC) की मौलिक सरलता के बीच के तनाव को संबोधित करता है।

चुनौती: जबकि DTT बिल्ट-इन कंप्यूटेशन और अनुमानित टाइप चेकिंग जैसी व्यावहारिक सुविधाएँ प्रदान करता है, इसके लॉजिकल कर्नेल जटिल, सत्यापन में कठिन और कार्यान्वयन बगों के प्रति संवेदनशील होते हैं। इसके विपरीत, ZFC एक परिपक्व, अच्छी तरह से समझ में आने वाला आधार है, लेकिन इसमें आधुनिक प्रूफ असिस्टेंट्स के लिए आवश्यक डिपेंडेंट टाइप्स और "टाइप्स-एज़-सेट्स" प्रतिमान (paradigm) के लिए नेटिव सपोर्ट की कमी है।
लक्ष्य: लेखक यह निर्धारित करने का लक्ष्य रखते हैं कि क्या एक मौजूदा सेट-थ्योरेटिक फाउंडेशन (विशेष रूप से Lisa प्रूफ असिस्टेंट) के ऊपर डिपेंडेंट टाइप्स के लिए एक सॉफ्ट टाइप सिस्टम (soft type system) को लागू करना व्यवहार्य है। इसका उद्देश्य DTT की सिंटैक्स और ऑटोमेशन प्रदान करना है, जबकि यह सुनिश्चित करना है कि सभी तर्क (reasoning) सेट-थ्योरेटिक एक्सिओम्स और फर्स्ट-ऑर्डर लॉजिक (FOL) के डीडक्शन रूल्स द्वारा औपचारिक रूप से न्यायसंगत हों।

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

लेखक $\lambda$ FOL का उपयोग करते हुए, स्कीमैटिक फर्स्ट-ऑर्डर लॉजिक विद इक्वैलिटी में डिपेंडेंट फंक्शन टाइप्स और यूनिवर्स पदानुक्रम (universe hierarchy) के एक मेकेनाइज्ड एम्बेडिंग (mechanized embedding) का प्रस्ताव करते हैं, जिसे Lisa प्रूफ असिस्टेंट के माध्यम से कार्यान्वित किया गया है।

A. तार्किक आधार: $\lambda$ FOL

वेरिएबल बाइंडिंग (जो टाइप थ्योरी में $\lambda$ -एब्स्ट्रैक्शन के लिए आवश्यक है) को फर्स्ट-ऑर्डर फ्रेमवर्क के भीतर संभालने के लिए, लेखक $\lambda$ FOL का उपयोग करते हैं, जो Lisa में उपलब्ध FOL का एक विस्तार है।

विशेषताएँ: $\lambda$ FOL में $\lambda$ -टर्म्स और हिल्बर्ट का $\epsilon$ -ऑपरेटर शामिल है।
सरलता: सिस्टम $\beta$ -रिडक्शन और स्कीमैटिक सिंबल इंस्टेंशिएशन पर निर्भर करता है, जिससे हायर-ऑर्डर टर्म्स को शुद्ध फर्स्ट-ऑर्डर टर्म्स में अनफोल्ड किया जा सकता है, जिससे कर्नेल की "फर्स्ट-ऑर्डर भावना" बनी रहती है।

B. डिपेंडेंट टाइप्स का एम्बेडिंग (Embedding Dependent Types)

लेखक एक एम्बेडिंग फंक्शन को परिभाषित करते हैं जो टाइप-थ्योरेटिक टर्म्स को $\lambda$ FOL टर्म्स में मैप करता है:

एब्स्ट्रैक्शन ( $\lambda x:T. u$ ): इसे एक फंक्शनल रिलेशन को दर्शाने वाले जोड़ों के सेट के रूप में मैप किया जाता है: abs(T)(λx.u) := {⟨x, L(x)⟩ | x ∈ T}।
एप्लीकेशन ( $t u$ ): इसे फंक्शन सेट से एक वैल्यू चुनने के लिए $\epsilon$ -ऑपरेटर का उपयोग करके मैप किया जाता है: app(t)(u) := εy. (u, y) ∈ t।
डिपेंडेंट प्रोडक्ट ( $\Pi x:T_1. T_2$ ): इसे डोमेन और कोडोमेन बाधाओं को संतुष्ट करने वाले फंक्शनल रिलेशंस के सेट के रूप में मैप किया जाता है:
$\Pi(T_1)(L) := \{ f \in \mathcal{P}(T_1 \times \bigcup_{x \in T_1} L(x)) \mid \text{isFunc}(f) \land \forall x \in T_1. \text{app}(f)(x) \in L(x) \}$
प्रमुख प्रमेय: वे सिद्ध करते हैं कि ये परिभाषाएँ मानक DTT इन्फरेंस रूल्स को पुनः प्राप्त करती हैं, जिसमें $\beta$ -रिडक्शन, एब्स्ट्रैक्शन (Tabs), और एप्लीकेशन (Tapp) शामिल हैं, जो विशुद्ध रूप से सेट-थ्योरेटिक एक्सिओम्स से प्राप्त होते हैं।

C. यूनिवर्स मैनेजमेंट (Universe Management)

मानक ZFC में आंतरिक रूप से यूनिवर्स (ऐसे सेट जो सभी कंस्ट्रक्शंस के लिए बंद होते हैं) की अवधारणा का अभाव है। पॉलीमोर्फिज्म के लिए आवश्यक संचयी पदानुक्रम (cumulative hierarchy - $Type_i : Type_{i+1}$ ) को मॉडल करने के लिए:

टार्सकी-ग्रोथेंडिक एक्सिओम्स (Tarski-Grothendieck Axioms): लेखक टार्सकी के एक्सिओम को अपनाते हैं, जो अनंत ग्रोथेंडिक यूनिवर्स (Grothendieck universes) के अस्तित्व को प्रमाणित करता है।
परिभाषा: एक ग्रोथेंडिक यूनिवर्स एक ऐसा सेट है जो पेयरिंग, यूनियन, पावर सेट्स और रिप्लेसमेंट के लिए क्लोज्ड (closed) है।
कार्यान्वयन: वे एक प्रेडिकेट isUniverse और एक फंक्शन universeOf(x) ( $\epsilon$ -ऑपरेटर का उपयोग करके) को परिभाषित करते हैं जो दिए गए सेट को समाहित करने वाले यूनिवर्स का चयन करता है। यह डिपेंडेंट प्रोडक्ट फॉर्मेशन के लिए आवश्यक यूनिवर्स पदानुक्रम ($Typen$) के निर्माण की अनुमति देता है।

D. स्वचालित प्रमाण जनरेशन (Automated Proof Generation)

टाइपिंग जजमेंट्स के लिए मैनुअल प्रूफ कंस्ट्रक्शन से बचने के लिए, लेखकों ने Lisa के भीतर एक द्विदिश टाइप-चेकिंग टैक्टिक (bidirectional type-checking tactic) (Typecheck.prove) को लागू किया है।

मोड्स (Modes): टैक्टिक Check (एक अपेक्षित टाइप के विरुद्ध टर्म को सत्यापित करना), Infer (एक टर्म का टाइप कंप्यूट करना), और Subset (सबटाइपिंग को संभालना) मोड में कार्य करता है।
सबटाइपिंग: वे सबटाइपिंग के एक प्रतिबंधित रूप को लागू करते हैं। हालांकि पूर्ण कंट्रावेरिएंस (contravariance) सेट थ्योरी में साइज संबंधी समस्याओं के कारण समस्याग्रस्त है, वे डिपेंडेंट प्रोडक्ट्स ( $\Pi$ -subtyping) के लिए इनवेरिएंट डोमेन और कोवेरिएंट कोडोमेन के नियम को सिद्ध करते हैं।
आउटपुट: एक बूलियन रिटर्न करने के बजाय, टैक्टिक एक औपचारिक प्रमाण ऑब्जेक्ट (एक सेट-थ्योरेटिक प्रूफ) सिंथेसाइज़ करता है जिसे Lisa कर्नेल द्वारा सत्यापित किया जा सकता है।

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

DTT का सेट-थ्योरेटिक एम्बेडिंग: फर्स्ट-ऑर्डर सेट-थ्योरेटिक फ्रेमवर्क के भीतर डिपेंडेंट फंक्शन टाइप्स और यूनिवर्स पदानुक्रमों का एक औपचारिक कार्यान्वयन, जो यह सिद्ध करता है कि DTT कंस्ट्रक्ट्स को सेट मेंबरशिप और इक्वैलिटी में बदला जा सकता है।
प्रूफ-प्रोड्यूसिंग टाइप चेकर: एक ऐसे टैक्टिक का कार्यान्वयन जो टाइपिंग जजमेंट्स के लिए स्वचालित रूप से कर्नेल-वेरिफिएबल प्रूफ जेनरेट करता है, जो हाई-लेवल टाइप थ्योरी और लो-लेवल सेट थ्योरी के बीच के अंतर को पाटता है।
सबटाइपिंग सपोर्ट: सेट-थ्योरेटिक मॉडल के भीतर सबटाइपिंग (विशेष रूप से कोवेरिएंट फंक्शन टाइप्स) का एक प्रूफ-ऑफ-कॉन्सेप्ट कार्यान्वयन, जो इस दृष्टिकोण की लचीलापन प्रदर्शित करता है।
इंटरऑपरेबिलिटी पाथवे: DTT-आधारित सिस्टम्स (जैसे Lean 4 और Rocq) से प्रमाणों को सेट-थ्योरेटिक प्रूफ असिस्टेंट्स में अनुवादित करने की दिशा में एक कदम, जो प्रूफ ट्रांसफर और सिस्टम इंटरऑपरेबिलिटी को सुगम बनाता है।

4. परिणाम (Results)

सत्यापन (Verification): लेखकों ने Lisa में इस एम्बेडिंग को सफलतापूर्वक मेकेनाइज किया है। उन्होंने प्रदर्शित किया कि टाइपिंग जजमेंट्स (जैसे, पॉलीमोर्फिक आइडेंटिटी के साथ फंक्शन कंपोजिशन) को स्वचालित रूप से सत्यापित किया जा सकता है।
उदाहरण केस: उन्होंने एक पॉलीमोर्फिक कंपोजिशन उदाहरण (Function.comp और id) को सत्यापित किया, जो दिखाता है कि टैक्टिक इनपुट धारणाओं और यूनिवर्स लेवल्स के आधार पर कंपोज्ड फंक्शन के लिए सेट मेंबरशिप को सही ढंग से निकालता है।
सटीकता (Correctness): सिस्टम यह सुनिश्चित करता है कि सभी टाइप-चेकिंग निर्णय टार्सकी-ग्रोथेंडिक एक्सिओम्स और FOL डीडक्शन रूल्स द्वारा समर्थित हैं, जिससे एक जटिल, unverified टाइप-थ्योरेटिक कर्नेल की आवश्यकता समाप्त हो जाती है।

5. महत्व (Significance)

मौलिक मजबूती (Foundational Robustness): DTT को ZFC में स्थापित करके, यह दृष्टिकोण दशकों के गणितीय सर्वसम्मति का लाभ उठाता है और लॉजिकल कर्नेल को सरल बनाता है, जिससे जटिल DTT कर्नेल की तुलना में कार्यान्वयन बगों का जोखिम कम हो जाता है।
समुदायों को जोड़ना: यह कार्य DTT-प्रधान इकोसिस्टम (Lean, Rocq) और सेट-थ्योरेटिक सिस्टम (Mizar, Isabelle/ZF) के बीच प्रमाणों के हस्तांतरण को सुगम बनाता है, जो संभावित रूप से औपचारिक गणित को एकीकृत करता है।
व्यावहारिक ऑटोमेशन: यह दर्शाता है कि "सॉफ्ट टाइप सिस्टम" दृष्टिकोण सेट थ्योरी की मौलिक सरलता से समझौता किए बिना DTT की उपयोगिता और ऑटोमेशन प्रदान कर सकता है।
भविष्य की दिशाएं: लेखक इसे Lean 4 और Rocq के लिए एक पूर्ण ट्रांसलेशन लेयर की ओर पहला कदम मानते हैं, जो सुझाव देता है कि सेट-थ्योरेटिक फाउंडेशन डिपेंडेंट टाइप्स और सबटाइपिंग जैसे उन्नत टाइप-थ्योरेटिक फीचर्स को बिना किसी पैराडाइम शिफ्ट के सपोर्ट कर सकते हैं।