How to play the Accordion: Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (extended version)

तकनीकी सारांश: "एकार्डियन कैसे बजाएं: $\lambda$-कैलकुलस के रैखिक सन्निकटन की एकरूपता और (गैर-)रूढ़िवादिता"

समस्या विवरण
यह शोध पत्र $\lambda$-कैलकुलस के रैखिक सन्निकटन (linear approximation) की रूढ़िवादिता (conservativity) की जांच करता है, विशेष रूप से एहरार्ड और रेनियर के डिफरेंशियल $\lambda$-कैलकुलस और रिसोर्स कैलकुलस के ढांचे के भीतर। जबकि यह स्थापित है कि एक $\lambda$-टर्म $M$ का टेलर विस्तार $T(M)$ $\beta$-रिडक्शन का अनुकरण करने की अनुमति देता है (अर्थात, यदि $M \to_\beta N$, तो $T(M) \twoheadrightarrow_r T(N)$), विपरीत प्रश्न अभी भी बना हुआ है: क्या रिसोर्स कैलकुलस में प्रत्येक रिडक्शन वास्तव में स्रोत $\lambda$-कैलकुलस में एक वास्तविक रिडक्शन द्वारा प्रेरित होता है?

औपचारिक रूप से, दिए गए रिडक्शन $T(M) \twoheadrightarrow_r T(N)$ के लिए (जो रिसोर्स टर्म्स के अनंत रैखिक संयोजनों पर कार्य करता है), क्या एक $\beta$-रिडक्शन अनुक्रम $M \to_\beta N$ मौजूद है? लेखक दो सेटिंग्स के बीच अंतर करते हैं:

1. परिमित (Finite) $\lambda$-कैलकुलस: टर्म्स परिमित हैं, और रिडक्शन परिमित अनुक्रम हैं।
2. अनंत (Infinitary) $\lambda$-कैलकुलस ($\lambda^{001}$): टर्म्स अनंत (को-इंडक्टिव) हो सकते हैं, और रिडक्शन अनंत अनुक्रम ($\to^{001}_\beta$) हो सकते हैं, बशर्ते रेडेक्स (redexes) को बढ़ती गहराई पर चलाया जाए।

केंद्रीय समस्या यह है कि क्या रैखिक सन्निकटन इन सेटिंग्स में स्रोत कैलकुलस का एक रूढ़िवादी विस्तार (conservative extension) है।

कार्यप्रणाली
लेखक रीराइटिंग थ्योरी (rewriting theory), को-इंडक्टिव परिभाषाओं और "मैशअप" तकनीक (स्रोत टर्म्स को उनके रिसोर्स एप्रोक्सिमेंट्स से जोड़ना) के संयोजन का उपयोग करते हैं।

1. परिमित मामला विश्लेषण: परिमित टर्म्स के लिए, लेखक केरीनैक और वॉक्स ऑकलैर द्वारा उपयोग की गई "मैशअप" प्रमाण तकनीक को अनुकूलित करते हैं। वे एक संबंध $\vdash$ को परिभाषित करते हैं जो एक $\lambda$-टर्म को उसके रिसोर्स एप्रोक्सिमेंट्स से जोड़ता है। यह सिद्ध करके कि यदि $T(M) \tworedrightarrow_r T(N)$, तो $M \vdash T(N)$, और इसके बाद कि $M \vdash T(N)$ का अर्थ $M \to^*_\beta N$ है, वे परिमित मामले के लिए रूढ़िवादिता स्थापित करते हैं।
2. अनंत काउंटरएग्जांपल (द एकार्डियन): अनंत मामले को संबोधित करने के लिए, लेखक एक विशिष्ट काउंटरए एग्जांपल, एकार्डियन (Accordion - $A$) का निर्माण करते हैं। यह टर्म एक अनंत संरचना को "खींचने" (stretch) और "संकुचित करने" (compress) का अनुकरण करने के लिए डिज़ाइन किया गया है।
   • टर्म $A$ एक अनुक्रम $A_n$ में रिड्यूस होता है जो एक अनंत टर्म $\bar{A} = (\langle T \rangle)(\langle F \rangle)\omega$ को एप्रोक्सिमेट करता है।
   • महत्वपूर्ण रूप से, जबकि $T(A) \twoheadrightarrow_r T(\bar{A})$ सत्य है, लेखक यह सिद्ध करते हैं कि कोई वैध अनंत $\beta$-रिडक्शन $A \to^{001}_\beta \bar{A}$ मौजूद नहीं है। $A$ के रिडक्शन पाथ्स को बद्ध गहराइयों (bounded depths) पर "ग्लोबल" स्टेप्स की आवश्यकता होती है जो अनंत $\beta$-रिडक्शन के लिए आवश्यक स्तरीकरण (stratification) की स्थिति का उल्लंघन करते हैं (लेम्मा 2.5)।
3. एकरूपता (Uniformity) और सुसंगति (Coherence): अनंत मामले में रूढ़िवादिता को पुनः प्राप्त करने के लिए, लेखक एकरूपता पेश करते हैं, जो एहरार्ड और रेनियर के कार्य में मूल रूप से केंद्रीय थी। वे रिसोर्स टर्म्स पर एक सुसंगति संबंध ($\bowtie$) परिभाषित करते हैं और रिडक्शन संबंध को यूनिफॉर्म सम्स (uniform sums) (ऐसे योग जहाँ सभी तत्व युग्मवार सुसंगत/pairwise coherent हैं) तक सीमित करते हैं।
   • वे एक यूनिफॉर्म रिसोर्स रिडक्शन ($\to^{\curvearrowright}_r$) और उसके अनंत विस्तार ($\to^{\curvearrowright \infty}_r$) को परिभाषित करते हैं।
   • यह प्रतिबंध सुनिश्चित करता है कि रिसोर्स कैलकुलस में रिडक्शन सख्ती से स्रोत कैलकुलस में होने वाले रिडक्शन के अनुरूप होते हैं, जिससे ऐसे "गैर-यूनिफॉर्म" पथों को हटाया जा सके जो वास्तविक $\beta$-रिडक्शन के अनुरूप नहीं हैं।
4. $\beta_\perp$ तक विस्तार: लेखक इन परिणामों को $\beta_\perp$-रिडक्शन (जो अनसुलने योग्य टर्म्स को $\bot$ में ढहा देता है) तक विस्तारित करते हैं, यह दिखाते हुए कि एकरूपता $\bot$-रिडक्शन शामिल होने पर भी रूढ़िवादिता को बनाए रखती है।

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

1. परिमित टर्म्स के लिए रूढ़िवादिता: शोध पत्र यह प्रमाण प्रदान करता है कि रैखिक सन्निकटन परिमित $\lambda$-कैलकुलस के संबंध में रूढ़िवादी है (प्रमेय 3.1)।
2. अनंत टर्म्स के लिए गैर-रूढ़िवादिता: लेखक एक विशिष्ट काउंटरए एग्जांपल, एकार्डियन का निर्माण करके यह प्रदर्शित करते हैं कि मानक पॉइंटवाइज रिसोर्स रिडक्शन ($\twoheadrightarrow_r$) अनंत $\lambda$-कैलकुलस के संबंध में गैर-रूढ़िवादी है (प्रमेय 4.4)। यह सिद्ध करता है कि $T(A) \twoheadrightarrow_r T(\bar{A})$ होने पर भी $A \to^{001}_\beta \bar{A}$ नहीं होता है।
3. एकरूपता के माध्यम से बहाली: लेखक एकरूपता को उस लुप्त कड़ी के रूप में पहचानते हैं जो अनंत $\lambda$-कैलकुलस के लिए रूढ़िवादिता को बहाल करने के लिए आवश्यक है। रिसोर्स कैलकुलस को यूनिफॉर्म रिडक्शन ($\to^{\curvearrowright \infty}_r$) तक सीमित करके, वे सिद्ध करते हैं कि रैखिक सन्निकटन अनंत $\lambda$-कैलकुलस का एक रूढ़िवादी विस्तार बन जाता है (प्रमेय 5.10)।
4. $\beta_\perp$ तक विस्तार: परिणामों को $\beta_\perp$-रिडक्शन में सामान्यीकृत किया गया है, यह दिखाते हुए कि यूनिफॉर्म दृष्टिकोण $\bot$-रिडक्शन शामिल होने पर भी रूढ़िवादिता को सही ढंग से सिम्युलेट और संरक्षित करता है (प्रमेय 5.18 और 5.19)।

परिणाम

• परिमित सेटिंग: रिसोर्स रिडक्शन द्वारा $\beta$-रिडक्शन का अनुकरण रूढ़िवादी है।
• अनंत सेटिंग (मानक): मानक पॉइंटवाइज रिसोर्स रिडक्शन द्वारा अनंत $\beta$-रिडक्शन का अनुकरण गैर-रूढ़िवादी है। एकार्डियन टर्म $A$, $\bar{A}$ में रिड्यूस होता है लेकिन $\lambda$-कैलकुलस में नहीं।
• अनंत सेटिंग (यूनिफॉर्म): यूनिफॉर्म रिसोर्स रिडक्शन द्वारा अनंत $\beta$-रिडक्शन का अनुकरण रूढ़िवादी है।
• $\beta_\perp$ सेटिंग: मानक रिडक्शन की गैर-रूढ़िवादिता $\beta_\perp$-रिडक्शन तक विस्तृत होती है, जबकि यूनिफॉर्म रिडक्शन $\beta_\perp$ के लिए भी रूढ़िवादी रहता है।

महत्व
यह शोध पत्र स्पष्ट करता है कि किन सटीक शर्तों के तहत रैखिक सन्निकटन $\lambda$-कैलकुलस की गतिशीलता का एक निष्ठावान मॉडल (faithful model) के रूप में कार्य करता है। यह पहले लेखक के पीएचडी थीसिस से जुड़े एक अनुमान को हल करता है कि अनंत सेटिंग में मात्रात्मक (quantitative) रैखिक सन्निकटन गैर-रूढ़िवादी है।

प्राथमिक महत्व इस बात की पहचान में है कि एकरूपता (uniformity) केवल टेलर एक्सपेंशन के एक सिमेंटिक गुण के रूप में ही नहीं, बल्कि स्वयं रिडक्शन संबंध पर एक आवश्यक सिंथैक्टिक बाधा के रूप में भी है, ताकि रूढ़िवादिता सुनिश्चित की जा सके। इस प्रतिबंध के बिना, रिसोर्स कैलकुलस ऐसे "घोस्ट" (ghost) रिडक्शन की अनुमति देता है जिनका स्रोत कैलकुलस में कोई समकक्ष नहीं है, विशेष रूप से अनंत टर्म्स की उपस्थिति में। यह कार्य "कम्यूटेशन थ्योरम" (नॉर्मलाइजेशन, एप्रोक्सिमेशन के साथ कम्यूट करता है) के सूक्ष्म अंतर को स्पष्ट करता है, यह दिखाते हुए कि जबकि अनुकरण (simulation) सामान्य रूप से मान्य है, रूढ़िवादिता (conservativity) के लिए सख्त यूनिफॉर्म ढांचे की आवश्यकता होती।

लेखक स्पष्ट रूप से बताते हैं कि उनका कार्य पूर्ण प्रमाण प्रदान करके और $\beta_\perp$-रिडक्शन तक विश्लेषण का विस्तार करके पिछले कॉन्फ्रेंस संस्करणों में सुधार करता है, जो बोम ट्रीज़ (Böhm trees) से टर्म्स को जोड़ने के लिए अत्यंत महत्वपूर्ण हैं।