2025-11-10T02:45:59.987115

Ground Stratification for a Logic of Definitions with Induction

Guermond, Nadathur
The logic underlying the Abella proof assistant includes mechanisms for interpreting atomic predicates through fixed point definitions that can additionally be treated inductively or co-inductively. However, the original formulation of the logic includes a strict stratification condition on definitions that is too restrictive for some applications such as those that use a logical relations based approach to semantic equivalence. Tiu has shown how this restriction can be eased by utilizing a weaker notion referred to as ground stratification. Tiu's results were limited to a version of the logic that does not treat inductive definitions. We show here that they can be extended to cover such definitions. While our results are obtained by using techniques that have been previously deployed in related ways in this context, their use is sensitive to the particular way in which we generalize the logic. In particular, although ground stratification may be used with arbitrary fixed-point definitions, we show that weakening stratification to this form for inductive definitions leads to inconsistency. The particular generalization we describe accords well with the way logical relations are used in practice. Our results are also a intermediate step to building a more flexible form for definitions into the full logic underlying Abella, which additionally includes co-induction, generic quantification, and a mechanism referred to as nominal abstraction for analyzing occurrences of objects in terms that are governed by generic quantifiers.
academic

परिभाषाओं के तर्क के लिए आधार स्तरीकरण और प्रेरण

मूल जानकारी

  • पेपर ID: 2510.12297
  • शीर्षक: Ground Stratification for a Logic of Definitions with Induction
  • लेखक: Nathan Guermond, Gopalan Nadathur (University of Minnesota Twin-Cities)
  • वर्गीकरण: cs.LO cs.PL
  • प्रकाशन सम्मेलन: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2025)
  • पेपर लिंक: https://arxiv.org/abs/2510.12297

सारांश

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

अनुसंधान पृष्ठभूमि और प्रेरणा

समस्या की पृष्ठभूमि

  1. Abella तर्क की प्रतिबंधात्मकता: Abella प्रमाण सहायक पर आधारित तर्क G में कठोर स्तरीकरण शर्त है, जिसमें विधेय स्थिरांक अपने परिभाषा सूत्र में शीर्ष-स्तरीय निहितार्थ प्रतीक के बाईं ओर प्रकट नहीं हो सकते
  2. व्यावहारिक अनुप्रयोग की आवश्यकता: तार्किक संबंध विधि प्रोग्रामिंग भाषा गुणों के अनुमान में व्यापक रूप से उपयोग की जाती है, जिसकी परिभाषाएं आमतौर पर प्रकार द्वारा अनुक्रमित होती हैं और स्वयं-परिभाषा मानती हैं (हालांकि संरचनात्मक रूप से छोटे प्रकारों के लिए)
  3. मौजूदा समाधान अपर्याप्त: Tiu की आधार स्तरीकरण विधि केवल प्रेरण परिभाषाओं को शामिल न करने वाले तर्क संस्करण पर लागू होती है

अनुसंधान का महत्व

  • सैद्धांतिक मूल्य: तार्किक परिभाषाओं की लचीलापन को विस्तारित करना, साथ ही संगतता सुनिश्चित करना
  • व्यावहारिक महत्व: अधिक प्रोग्रामिंग भाषा सत्यापन परिदृश्यों का समर्थन करना, विशेष रूप से तार्किक संबंधों पर आधारित विधियां
  • तकनीकी प्रगति: अधिक लचीले Abella तर्क के निर्माण के लिए आधार तैयार करना

मूल योगदान

  1. आधार स्तरीकरण सिद्धांत का विस्तार: Tiu के आधार स्तरीकरण परिणामों को प्रेरण परिभाषाओं को शामिल करने वाले तर्क तक विस्तारित करना
  2. प्रेरण परिभाषाओं की सीमाओं की पहचान: साबित करना कि स्तरीकरण शर्त को आधार स्तरीकरण रूप तक कमजोर करने से प्रेरण परिभाषाओं का तर्क असंगत हो जाता है
  3. मिश्रित स्तरीकरण रणनीति प्रस्तावित करना: प्रेरण विधेय कठोर स्तरीकरण का उपयोग करते हैं, निश्चित बिंदु विधेय आधार स्तरीकरण का उपयोग करते हैं
  4. संगतता प्रमाण प्रदान करना: आधार तर्क संस्करण में कमी के माध्यम से तर्क LDμ की संगतता साबित करना
  5. व्यावहारिक अनुप्रयोग प्रदर्शित करना: मजबूत सामान्यीकरण प्रमाण में कम करने योग्यता विधेय को कोडित करने का तरीका दिखाना

विधि विवरण

तर्क LDμ की परिभाषा

वाक्य रचना संरचना

  • आधार: Church सरल प्रकार सिद्धांत पर आधारित अंतर्ज्ञानवादी प्रथम-क्रम तर्क
  • प्रकार प्रणाली: आधार प्रकार ι₁,...,ιₙ, फलन प्रकार α→β और प्रस्ताव प्रकार o शामिल
  • पद: सरल प्रकार λ कलन में सुप्रकार पद
  • सूत्र: प्रकार o के पद

परिभाषा तंत्र

तर्क दो प्रकार की परिभाषा खंड का समर्थन करता है:

  1. निश्चित बिंदु खंड: H ^∆= B, सामान्य निश्चित बिंदु परिभाषाओं के लिए
  2. प्रेरण खंड: H ^μ= B, प्रेरण परिभाषाओं के लिए (न्यूनतम निश्चित बिंदु)

स्तरीकरण शर्तें

आधार स्तरीकरण (Ground Stratification)

परिभाषा D के लिए आधार स्तरीकृत होने के लिए, यदि और केवल यदि आधार परमाणु सूत्रों के स्तर असाइनमेंट मौजूद हो, जैसे कि प्रत्येक खंड H ^∆= B ∈ D और प्रत्येक X-आधार प्रतिस्थापन ρ के लिए:

lvl(Hρ) ≥ lvl(Bρ)

स्तर फलन निम्नानुसार परिभाषित है:

  • lvl(⊥) := lvl(⊤) := 0
  • lvl(A∧B) := lvl(A∨B) := max(lvl(A), lvl(B))
  • lvl(A ⊃ B) := max(lvl(A)+1, lvl(B))
  • lvl(∀x:α.C) := lvl(∃x:α.C) := sup{lvl(Ct/x∅) | t ∈ ground(α)}

कठोर स्तरीकरण (Strict Stratification)

स्तर असाइनमेंट को केवल विधेय शीर्ष पर निर्भर करने की आवश्यकता है, अर्थात किसी भी आधार पद अनुक्रम t₁ और t₂ के लिए:

lvl(pt₁) = lvl(pt₂)

मिश्रित स्तरीकरण रणनीति

  • प्रेरण विधेय: कठोर स्तरीकरण शर्त को संतुष्ट करना चाहिए
  • निश्चित बिंदु विधेय: आधार स्तरीकरण शर्त का उपयोग कर सकते हैं

अनुमान नियम

परिभाषा नियम

{range(θ);Γθ,B' ⊢ Cθ | defn(H^∆=B,A,θ,B'), H^∆=B ∈ D}
―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――
                    Y;Γ,A ⊢ C                                    ∆L

                    Y;Γ ⊢ B'
                ――――――――――――――――――――――――  ∆R
                    Y;Γ ⊢ A

प्रेरण नियम

x;B Sx ⊢ Sx    X;Γ,St ⊢ C
―――――――――――――――――――――――――――――――――  μL
        X;Γ, pt ⊢ C

        X;Γ ⊢ B pt
        ――――――――――――――  μR  
         X;Γ ⊢ pt

सैद्धांतिक विश्लेषण

असंगतता प्रमाण

साबित किया कि यदि प्रेरण परिभाषाओं को आधार स्तरीकरण का उपयोग करने की अनुमति दी जाए, तो तर्क असंगत हो जाता है। मुख्य उदाहरण:

विषम संख्या विधेय परिभाषित करना:

odd (s X) ^μ= odd X ⊃ ⊥

यह परिभाषा आधार स्तरीकरण के तहत वैध है, लेकिन विरोधाभास की ओर ले जाती है:

  1. किसी भी पद t के लिए साबित किया जा सकता है: X;odd t ⊢ ev t और X;odd t ⊢ ev t ⊃ ⊥
  2. इसलिए X;odd t ⊢ ⊥ सभी t के लिए सत्य है
  3. विशेष रूप से, ·;odd z ⊢ ⊥ और ·;odd (s z) ⊢ ⊥ दोनों व्युत्पन्न हो सकते हैं
  4. अंततः ·;· ⊢ ⊥ प्राप्त होता है

संगतता प्रमाण रणनीति

LDμ की संगतता साबित करने के लिए अप्रत्यक्ष विधि अपनाई गई:

  1. आधार तर्क LDμ∞: केवल आधार अनुक्रमों को संभालने वाले अनंत तर्क संस्करण को परिभाषित करना
  2. कट-उन्मूलन प्रमेय: LDμ∞ की कट-उन्मूलन संपत्ति साबित करना
  3. व्याख्या मानचित्र: LDμ से LDμ∞ तक व्याख्या स्थापित करना, संगतता को कम करना

कट-उन्मूलन

निम्नलिखित चरणों के माध्यम से साबित किया गया:

  1. कट-उन्मूलन कमी संबंध परिभाषित करना
  2. सामान्यीकृत व्युत्पत्ति अवधारणा प्रस्तुत करना
  3. सामान्यीकृत होना सामान्यीकरण को निहित करता है साबित करना
  4. सामान्यीकरण लेम्मा स्थापित करना

मुख्य विस्तार लेम्मा:

मान लीजिए p x ^μ= B p x प्रेरण परिभाषा का निश्चित बिंदु रूप है, किसी भी व्युत्पत्ति Ψ के लिए ∆ ⊢ D p, जहां p D में प्रकट नहीं होता है और केवल सकारात्मक रूप से D p में प्रकट होता है, व्युत्पत्ति μ(Ψ,ΠS) of ∆ ⊢ D S मौजूद है।

व्यावहारिक अनुप्रयोग

मजबूत सामान्यीकरण प्रमाण

Tait शैली के मजबूत सामान्यीकरण प्रमाण में सामान्यीकरण योग्यता विधेय को कोडित करने का तरीका दिखाता है:

red unit T ^∆= sn T
red (arrow A B) T ^∆= ∀u:tm.(red A u ⊃ red B (app T u))

यह परिभाषा कठोरता से स्तरीकृत नहीं की जा सकती (क्योंकि red इसके परिभाषा निकाय में नकारात्मक रूप से प्रकट होता है), लेकिन आधार स्तरीकृत हो सकती है, क्योंकि नकारात्मक रूप से प्रकट होने वाले उदाहरण red A u में, प्रकार पैरामीटर A शीर्ष प्रकार पैरामीटर (arrow A B) का उप-पद है।

तार्किक समतुल्यता संबंध

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

संबंधित कार्य

Tiu के कार्य के साथ संबंध

  • आधार: Tiu के आधार स्तरीकरण सिद्धांत पर निर्मित
  • विस्तार: परिणामों को प्रेरण परिभाषाओं को शामिल करने के लिए विस्तारित करना
  • सीमा: प्रेरण परिभाषाओं के लिए मजबूत शर्तों की आवश्यकता की खोज

μNJ के साथ तुलना

  • μNJ: Baelde और Nadathur द्वारा विकसित प्राकृतिक अनुमान कलन, पुनर्लेखन नियमों के माध्यम से लचीली परिभाषाएं
  • यह कार्य: स्तरीकरण शर्तों के माध्यम से, समीकरण शब्दार्थ को संशोधित करने से बचना
  • पूरकता: दोनों विधियों के अपने फायदे हैं, एक दूसरे से सीख सकते हैं

निष्कर्ष और चर्चा

मुख्य निष्कर्ष

  1. सैद्धांतिक योगदान: प्रेरण परिभाषाओं को शामिल करने वाले तर्क तक आधार स्तरीकरण को सफलतापूर्वक विस्तारित करना
  2. व्यावहारिक मार्गदर्शन: आधार स्तरीकरण के सुरक्षित उपयोग की सीमा शर्तें निर्धारित करना
  3. तकनीकी पथ: अधिक लचीले Abella तर्क के निर्माण के लिए मध्यवर्ती चरण प्रदान करना

सीमाएं

  1. प्रेरण परिभाषा प्रतिबंध: प्रेरण परिभाषाओं को अभी भी कठोर स्तरीकरण को संतुष्ट करना चाहिए
  2. कट-उन्मूलन प्रमाण: पूर्ण तर्क के कट-उन्मूलन को सीधे साबित नहीं किया जा सकता
  3. विशेषता की कमी: अभी तक सह-प्रेरण, सामान्य परिमाणीकरण और नाममात्र अमूर्तता शामिल नहीं है

भविष्य की दिशाएं

  1. प्रेरण प्रक्रिया का विस्तार: प्रेरण खंडों में विधेय को गैर-वास्तविक नकारात्मक स्थितियों में प्रकट होने की अनुमति देना
  2. प्रत्यक्ष कट-उन्मूलन प्रमाण: ऐसी गैर-आधार कलन विकसित करना जो कट-उन्मूलन को सीधे साबित कर सके
  3. उच्च-क्रम परिमाणीकरण: मॉड्यूलरिटा बढ़ाने के लिए उच्च-क्रम परिमाणीकरण क्षमता जोड़ना
  4. पूर्ण विशेषता एकीकरण: सह-प्रेरण, सामान्य परिमाणीकरण आदि को एकीकृत करना

गहन मूल्यांकन

लाभ

  1. सैद्धांतिक कठोरता: पूर्ण संगतता प्रमाण प्रदान करता है, तकनीकी प्रक्रिया सूक्ष्म है
  2. व्यावहारिक प्रासंगिकता: तार्किक संबंधों जैसे महत्वपूर्ण अनुप्रयोग परिदृश्यों की आवश्यकता को हल करता है
  3. संतुलित डिजाइन: लचीलापन और सुरक्षा के बीच उपयुक्त संतुलन खोजता है
  4. स्पष्ट अभिव्यक्ति: पेपर संरचना स्पष्ट है, तकनीकी विवरण सटीक रूप से व्यक्त किए गए हैं

कमियां

  1. अनुप्रयोग सीमा: प्रेरण परिभाषा प्रतिबंध कुछ उन्नत अनुप्रयोगों को प्रभावित कर सकते हैं
  2. प्रमाण जटिलता: अप्रत्यक्ष संगतता प्रमाण सैद्धांतिक जटिलता बढ़ाता है
  3. कार्यान्वयन अंतराल: वास्तविक Abella प्रणाली के साथ एकीकरण अभी भी कार्य की आवश्यकता है

प्रभाव

  1. सैद्धांतिक योगदान: तार्किक परिभाषा सिद्धांत के लिए महत्वपूर्ण विस्तार प्रदान करता है
  2. व्यावहारिक मूल्य: अधिक औपचारिक सत्यापन परिदृश्यों का समर्थन करता है
  3. तकनीकी प्रभाव: समान तर्क प्रणाली डिजाइन के लिए संदर्भ प्रदान करता है

लागू परिदृश्य

  • लचीली परिभाषा तंत्र की आवश्यकता वाली औपचारिक सत्यापन
  • तार्किक संबंधों पर आधारित प्रोग्राम गुण प्रमाण
  • प्रोग्रामिंग भाषा शब्दार्थ का औपचारिक अनुसंधान
  • प्रकार प्रणाली और मजबूत सामान्यीकरण प्रमाण

संदर्भ

पेपर 17 संबंधित संदर्भों का हवाला देता है, जो तार्किक परिभाषा, प्रेरण अनुमान, कट-उन्मूलन आदि मूल क्षेत्रों के महत्वपूर्ण कार्यों को कवर करता है, विशेष रूप से McDowell & Miller (2000) का अग्रणी कार्य और Tiu (2012) का आधार स्तरीकरण सिद्धांत।