2025-11-17T09:43:13.266953

Constructive validity of a generalized Kreisel-Putnam rule

Pezlar
In this paper, we propose a computational interpretation of the generalized Kreisel-Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry-Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for the intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding computational content of the typed Split rule. In other words, we want to find an appropriate selector function for the Split rule by considering its typed variant. Our investigation can also be reframed as an effort to answer the following questions: is the Split rule constructively valid in the sense of BHK semantics? Our answer is positive for the Split rule as well as for its newly proposed generalized version called the S rule.
academic

एक सामान्यीकृत Kreisel-Putnam नियम की रचनात्मक वैधता

मूल जानकारी

  • पेपर ID: 2311.15376
  • शीर्षक: एक सामान्यीकृत Kreisel-Putnam नियम की रचनात्मक वैधता
  • लेखक: Ivo Pezlar (चेक एकेडमी ऑफ साइंसेज, दर्शन संस्थान)
  • वर्गीकरण: cs.LO (कंप्यूटर विज्ञान - कंप्यूटर विज्ञान में तर्क), math.LO (गणित - तर्क)
  • प्रकाशन समय: 28 नवंबर 2023 (arXiv v2)
  • पेपर लिंक: https://arxiv.org/abs/2311.15376

सारांश

यह पेपर सामान्यीकृत Kreisel-Putnam नियम (जिसे सामान्यीकृत Harrop नियम या Split नियम भी कहा जाता है) की कम्प्यूटेशनल व्याख्या प्रस्तुत करता है, जो BHK शब्दार्थ शैली को अपनाता है। सूत्रों और प्रकारों के बीच Curry-Howard पत्राचार का उपयोग करके इसे प्राप्त किया जाता है। पहले Split नियम के अनुमान व्यवहार की जांच सहज ज्ञान युक्त प्रस्तावनात्मक तर्क की प्राकृतिक演नायक प्रणाली में की जाती है, जो टाइप किए गए Split नियम की संबंधित कम्प्यूटेशनल सामग्री को कैप्चर करने के लिए उपयुक्त प्रोग्राम तैयार करने का मार्गदर्शन करेगा। दूसरे शब्दों में, हम Split नियम के टाइप किए गए वेरिएंट पर विचार करके इसके लिए उपयुक्त चयनकर्ता फ़ंक्शन खोजना चाहते हैं। हमारे अनुसंधान को निम्नलिखित प्रश्न का उत्तर देने के रूप में भी पुनः तैयार किया जा सकता है: क्या Split नियम BHK शब्दार्थ के अर्थ में रचनात्मक रूप से वैध है? हमने Split नियम और इसके नए प्रस्तावित सामान्यीकृत संस्करण (S नियम कहा जाता है) दोनों के लिए एक सकारात्मक उत्तर दिया है।

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

मूल समस्या

इस पेपर द्वारा हल की जाने वाली मूल समस्या है: क्या Split नियम BHK शब्दार्थ के अर्थ में रचनात्मक रूप से वैध है? विशेष रूप से, एक रचनात्मक फ़ंक्शन खोजना है जो Split नियम के आधार के किसी भी प्रमाण को इसके निष्कर्ष के प्रमाण में परिवर्तित कर सके।

समस्या की महत्ता

  1. सैद्धांतिक महत्व: Kreisel-Putnam नियम सहज ज्ञान युक्त तर्क में एक स्वीकार्य लेकिन व्युत्पन्न नहीं नियम है, हालांकि Dummett-Prawitz शैली शब्दार्थ के वेरिएंट में प्रमाण-सैद्धांतिक रूप से वैध है।
  2. तार्किक प्रणाली विशेषताएं: जब Split नियम को सहज ज्ञान युक्त तर्क में जोड़ा जाता है, तो परिणामी प्रणाली (जैसे पूछताछ सहज ज्ञान युक्त तर्क) विच्छेदन गुण को बनाए रखता है और संरचनात्मक पूर्णता रखता है, जो शास्त्रीय तर्क की विशेषता है।
  3. व्यापक अनुप्रयोग: Split नियम कई क्षेत्रों में प्रकट होता है, जैसे डोमेन तर्क, इसकी मौलिक महत्ता को प्रदर्शित करता है।

मौजूदा विधियों की सीमाएं

  1. कम्प्यूटेशनल व्याख्या की कमी: हालांकि Split नियम महत्वपूर्ण है, इसके प्रमाण-सैद्धांतिक अर्थ और कम्प्यूटेशनल सामग्री अधिकतर अन्वेषित नहीं हैं।
  2. रचनात्मक वैधता अस्पष्ट: Split नियम की कम्प्यूटेशनल सामग्री की व्याख्या के लिए कोई स्पष्ट रचनात्मक फ़ंक्शन नहीं है।

अनुसंधान प्रेरणा

Curry-Howard पत्राचार के माध्यम से, सूत्रों को प्रकार के रूप में मानते हुए, Split नियम की कम्प्यूटेशनल सामग्री को कैप्चर करने के लिए उपयुक्त चयनकर्ता फ़ंक्शन खोजना, जिससे इसकी रचनात्मक वैधता स्थापित की जा सके।

मुख्य योगदान

  1. S नियम प्रस्तावित किया: Split नियम को विच्छेदन-उन्मूलन नियम के सामान्यीकृत रूप के रूप में पुनः तैयार किया, जिसे S नियम कहा जाता है।
  2. रचनात्मक वैधता स्थापित की: S नियम के लिए एक प्रभावी चयनकर्ता फ़ंक्शन S खोजा, इसकी रचनात्मक वैधता को सिद्ध किया।
  3. कम्प्यूटेशनल व्याख्या प्रदान की: टाइप किए गए वेरिएंट और कम्प्यूटेशनल नियमों के माध्यम से, Split नियम की पूर्ण कम्प्यूटेशनल व्याख्या दी।
  4. सामान्यीकरण गुण सिद्ध किया: Martin-Löf निर्माणात्मक प्रकार सिद्धांत में टाइप किए गए S नियम को जोड़ने के बाद भी सामान्यीकरण को बनाए रखा।
  5. नियम समतुल्यता स्थापित की: Split नियम और S नियम की समतुल्यता को सिद्ध किया, और संबंधित कमी प्रक्रिया प्रदान की।

विधि विवरण

कार्य परिभाषा

इनपुट: Split नियम का आधार C → (A ∨ B), जहां C एक Harrop सूत्र है आउटपुट: Split नियम का निष्कर्ष (C → A) ∨ (C → B)बाधा: आधार से निष्कर्ष में रूपांतरण को लागू करने वाला रचनात्मक फ़ंक्शन खोजना

मुख्य विधि आर्किटेक्चर

1. नियम पुनः तैयारी

मूल Split नियम:

C → (A ∨ B)
─────────────── Split
(C → A) ∨ (C → B)

को S नियम (विच्छेदन-उन्मूलन) के रूप में पुनः तैयार किया:

[C]
 ⋮
A ∨ B    [C → A]    [C → B]
          ⋮           ⋮
          D           D
─────────────────────────── S
            D

2. टाइप किया गया S नियम

Martin-Löf निर्माणात्मक प्रकार सिद्धांत के ढांचे में, S नियम का टाइप किया गया रूप:

[z : C]
  ⋮
c(z) : A ∨ B    [x : C → A]    [y : C → B]
                   ⋮              ⋮
                d(x) : D        e(y) : D
────────────────────────────────────────── S
            S(c, d, e) : D

3. चयनकर्ता S के कम्प्यूटेशनल नियम

चयनकर्ता S का कम्प्यूटेशन पैटर्न मिलान और केस विश्लेषण पर आधारित है:

बाएं शाखा कम्प्यूटेशनल नियम:

S(inl(a(z)), d, e) = d(λz.a(z)) : D

दाएं शाखा कम्प्यूटेशनल नियम:

S(inr(b(z)), d, e) = e(λz.b(z)) : D

तकनीकी नवाचार बिंदु

1. Harrop सूत्रों का विशेष उपचार

  • मुख्य अंतर्दृष्टि: Harrop सूत्र कम्प्यूटेशनल रूप से अप्रासंगिक हैं, क्योंकि उनके पास कम्प्यूटेशनल सामग्री नहीं है
  • तकनीकी कार्यान्वयन: Smith (1993) के परिणाम का उपयोग करते हुए, मुक्त चर युक्त खुले प्रमाण वस्तुओं की कम्प्यूटेशन को सामान्य रूप में अनुमति देता है, बशर्ते ये चर Harrop सूत्रों तक सीमित हों।

2. अनुमान निर्णय का विशेषीकरण

विशेषीकृत अनुमान निर्णय रूप का परिचय:

z : C ⊢ b(z) : B(z)

जहां C को Harrop सूत्र तक सीमित किया गया है, इसका अर्थ व्याख्या: b(z) एक प्रोग्राम है जो कम्प्यूट करने के बाद प्रकार B(z) की एक सामान्य प्रमाण वस्तु उत्पन्न करता है।

3. कमी प्रक्रिया का डिजाइन

S नियम के लिए संबंधित कमी नियम प्रदान किए गए:

  • S-redL: बाएं विच्छेदन की कमी को संभालता है
  • S-redR: दाएं विच्छेदन की कमी को संभालता है

ये कमी नियम नियम की सामंजस्य और स्थानीय पूर्णता सुनिश्चित करते हैं।

प्रायोगिक सेटअप

सैद्धांतिक सत्यापन ढांचा

यह पेपर मुख्य रूप से प्रायोगिक सत्यापन के बजाय सैद्धांतिक विश्लेषण करता है, निम्नलिखित ढांचे को अपनाता है:

  1. आधार प्रणाली: सहज ज्ञान युक्त प्रस्तावनात्मक तर्क (IPC) की प्राकृतिक演नायक प्रणाली
  2. प्रकार सिद्धांत: Martin-Löf निर्माणात्मक प्रकार सिद्धांत
  3. शब्दार्थ ढांचा: BHK व्याख्या और Curry-Howard पत्राचार

सत्यापन विधि

  1. रचनात्मकता: स्पष्ट चयनकर्ता फ़ंक्शन के निर्माण के माध्यम से रचनात्मक वैधता को सिद्ध करना
  2. सामान्यीकरण: Smith (1993) के सामान्यीकरण प्रमाण को विस्तारित करके प्रणाली की सामंजस्य को सत्यापित करना
  3. समतुल्यता: पारस्परिक व्युत्पत्ति के माध्यम से Split नियम और S नियम की समतुल्यता को सिद्ध करना

प्रायोगिक परिणाम

मुख्य सैद्धांतिक परिणाम

1. रचनात्मक वैधता प्रमाण

प्रमेय: S नियम रचनात्मक रूप से वैध है। प्रमाण: स्पष्ट रूप से चयनकर्ता S का निर्माण करके, जो S नियम के आधार को निष्कर्ष में परिवर्तित कर सकता है।

2. सामान्यीकरण प्रमेय

प्रमेय: Martin-Löf निर्माणात्मक प्रकार सिद्धांत में टाइप किए गए S नियम को जोड़ने के बाद, प्रणाली सामान्यीकरण को बनाए रखती है। प्रमाण: Kleene-Aczel तिरछी प्राप्यता के प्रकार सिद्धांत अनुवाद को विस्तारित किया, S नियम युक्त प्रणाली सामान्यीकरण गुण को संतुष्ट करती है।

3. समतुल्यता परिणाम

प्रमेय: Split नियम और S नियम तार्किक रूप से समतुल्य हैं। प्रमाण:

  • S नियम से Split नियम को व्युत्पन्न किया जा सकता है
  • Split नियम से S नियम को व्युत्पन्न किया जा सकता है

विशिष्ट केस विश्लेषण

केस 1: परमाणु सूत्र स्थिति

सूत्र (p → (q ∨ r)) → ((p → q) ∨ (p → r)) के लिए, जहां p एक परमाणु सूत्र है (इसलिए एक Harrop सूत्र), S नियम का उपयोग करके सफलतापूर्वक सिद्ध किया जा सकता है।

केस 2: गैर-Harrop सूत्र स्थिति

सूत्र ((s ∨ t) → (q ∨ r)) → (((s ∨ t) → q) ∨ ((s ∨ t) → r)) के लिए, चूंकि (s ∨ t) एक Harrop सूत्र नहीं है, S नियम को लागू नहीं किया जा सकता, नियम की सीमा को प्रदर्शित करता है।

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

मुख्य संबंधित अनुसंधान

  1. Kreisel-Putnam तर्क: मूल रूप से Kreisel और Putnam (1957) द्वारा प्रस्तावित, सहज ज्ञान युक्त तर्क से अधिक मजबूत लेकिन विच्छेदन गुण को बनाए रखने वाली तार्किक प्रणाली।
  2. पूछताछ सहज ज्ञान युक्त तर्क: Punčochář (2016) और Ciardelli आदि (2020) का कार्य, Split नियम को सहज ज्ञान युक्त तर्क में जोड़कर प्राप्त प्रणाली।
  3. प्रमाण-सैद्धांतिक शब्दार्थ: Prawitz (1971, 1973) की Dummett-Prawitz शैली शब्दार्थ और इसके वेरिएंट।

इस पेपर का संबंधित कार्य से संबंध

  1. Condoluci और Manighetti (2018) के साथ तुलना: उन्होंने संबंधित Harrop नियम के कम्प्यूटेशनल दृष्टिकोण का अध्ययन किया, लेकिन ऊपर-से-नीचे दृष्टिकोण अपनाया, जबकि यह पेपर नीचे-से-ऊपर दृष्टिकोण अपनाता है।
  2. Smith (1993) के साथ संबंध: यह पेपर Kleene-Aczel तिरछी प्राप्यता के प्रकार सिद्धांत पर Smith के कार्य को विस्तारित करता है, विशेष रूप से खुले प्रमाण वस्तुओं की कम्प्यूटेशन के बारे में।

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

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

  1. Split नियम रचनात्मक रूप से वैध है: S नियम के माध्यम से, Split नियम BHK शब्दार्थ के अर्थ में रचनात्मक रूप से वैध है।
  2. S नियम एक प्राकृतिक सामान्यीकरण प्रदान करता है: S नियम एक विच्छेदन-उन्मूलन नियम के रूप में, Split नियम के लिए एक अधिक प्राकृतिक अभिव्यक्ति प्रदान करता है।
  3. प्रणाली अच्छे गुण बनाए रखती है: S नियम को जोड़ने के बाद प्रकार प्रणाली सामान्यीकरण जैसे महत्वपूर्ण गुणों को बनाए रखती है।

सीमाएं

  1. Harrop सूत्रों तक सीमित: S नियम केवल तब लागू किया जा सकता है जब आधार में C एक Harrop सूत्र हो, प्रणाली सुसंगत प्रतिस्थापन के तहत बंद नहीं है।
  2. जटिलता: चयनकर्ता S की कम्प्यूटेशन खुले प्रमाण वस्तुओं के उपचार को शामिल करती है, सैद्धांतिक जटिलता को बढ़ाती है।
  3. व्यावहारिकता: सैद्धांतिक परिणामों का व्यावहारिक अनुप्रयोग मूल्य आगे की खोज की आवश्यकता है।

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

  1. अन्य सामान्यीकरण: Split नियम को निहितार्थ-उन्मूलन नियम के रूप में देखने के एक अन्य सामान्यीकरण की खोज करना।
  2. विस्तारित अनुप्रयोग: अन्य तार्किक प्रणालियों और कम्प्यूटेशनल ढांचे में S नियम के अनुप्रयोग का अनुसंधान करना।
  3. कार्यान्वयन सत्यापन: विशिष्ट प्रमाण सहायकों में इन सैद्धांतिक परिणामों को कार्यान्वित और सत्यापित करना।

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

शक्तियां

  1. सैद्धांतिक गहराई: Split नियम की गहन प्रमाण-सैद्धांतिक विश्लेषण और रचनात्मक व्याख्या प्रदान करता है।
  2. विधि नवाचार: Split नियम को S नियम के रूप में पुनः तैयार करके, एक नया सैद्धांतिक दृष्टिकोण प्रदान करता है।
  3. तकनीकी कठोरता: Martin-Löf प्रकार सिद्धांत के ढांचे में कठोर औपचारिकीकरण किया गया है।
  4. पूर्णता: न केवल रचनात्मक वैधता को सिद्ध किया, बल्कि सामान्यीकरण जैसे महत्वपूर्ण गुणों को भी सत्यापित किया।

कमजोरियां

  1. सीमित अनुप्रयोग सीमा: Harrop सूत्रों तक सीमा व्यावहारिक अनुप्रयोग को प्रभावित कर सकती है।
  2. उच्च जटिलता: खुले प्रमाण वस्तुओं की कम्प्यूटेशन समझ और कार्यान्वयन की कठिनाई को बढ़ाती है।
  3. प्रायोगिक सत्यापन की कमी: विशिष्ट प्रणालियों में कार्यान्वयन और सत्यापन की कमी है।

प्रभाव

  1. सैद्धांतिक योगदान: प्रमाण-सैद्धांतिक शब्दार्थ और निर्माणात्मक प्रकार सिद्धांत के अंतःक्षेत्र में महत्वपूर्ण योगदान।
  2. पद्धति मूल्य: अन्य तार्किक नियमों की रचनात्मक वैधता का अध्ययन करने के लिए विधि टेम्पलेट प्रदान करता है।
  3. मौलिक अनुसंधान: सहज ज्ञान युक्त तर्क की कम्प्यूटेशनल सामग्री को समझने के लिए नई अंतर्दृष्टि प्रदान करता है।

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

  1. प्रमाण-सैद्धांतिक अनुसंधान: तार्किक नियमों के प्रमाण-सैद्धांतिक गुणों और कम्प्यूटेशनल व्याख्या का अध्ययन करने के लिए लागू।
  2. प्रकार सिद्धांत विकास: निर्माणात्मक प्रकार सिद्धांत के सैद्धांतिक आधार को विस्तारित और समृद्ध करने के लिए उपयोग किया जा सकता है।
  3. तार्किक प्रोग्रामिंग: तार्किक प्रोग्रामिंग भाषाओं के लिए नया सैद्धांतिक समर्थन प्रदान कर सकता है।

संदर्भ

यह पेपर समृद्ध संबंधित साहित्य का हवाला देता है, मुख्य रूप से:

  • Kreisel और Putnam (1957) की Kreisel-Putnam तर्क पर अग्रणी कार्य
  • Smith (1993) की Kleene-Aczel तिरछी प्राप्यता के प्रकार सिद्धांत व्याख्या
  • Martin-Löf (1984) का निर्माणात्मक प्रकार सिद्धांत आधार
  • Prawitz (1965, 1971, 1973) का प्रमाण सिद्धांत और शब्दार्थ कार्य
  • पूछताछ तर्क पर हाल के अनुसंधान (Punčochář 2016, Ciardelli आदि 2020)

यह तर्क और प्रकार सिद्धांत के अंतःक्षेत्र में एक उच्च गुणवत्ता वाला सैद्धांतिक अनुसंधान पेपर है, जो Split नियम की रचनात्मक सामग्री को समझने के लिए महत्वपूर्ण सैद्धांतिक योगदान प्रदान करता है। हालांकि इसमें एक निश्चित तकनीकी जटिलता और अनुप्रयोग सीमाएं हैं, इसकी कठोर सैद्धांतिक विश्लेषण और नवीन पद्धति संबंधित क्षेत्रों के विकास के लिए महत्वपूर्ण मूल्य रखती है।