A Machine-checked Proof of Consistency for Impredicative Pure Type Systems

तकनीकी सारांश: इम्प्रेडिकेटिव प्योर टाइप सिस्टम्स के लिए एक मशीन-चेक्ड कंसिस्टेंसी प्रूफ

समस्या और संदर्भ
यह शोध पत्र टाइप थ्योरी के मशीनीकरण की चुनौतियों को संबोधित करता है, जो विशेष रूप से प्योर टाइप सिस्टम्स (PTS) के मेटा-थ्योरिटिकल गुणों पर केंद्रित है। टाइपिंग को औपचारिक बनाने में एक केंद्रीय कठिनाई सब्स्टीट्यूशन (substitution) और $\beta$-रिडक्शन को हैंडल करने में निहित है, जो नाम कैप्चर (name capture) को रोकने के लिए वेरिएबल रीनेमिंग (variable renaming) पर ध्यान केंद्रित करती है। पारंपरिक परिभाषाएँ (जैसे करी-फेज़) टर्म की लंबाई पर वेल-फाउंडेड इंडक्शन (well-founded induction) की मांग करती हैं क्योंकि रीनेमिंग स्टेप्स नॉन-प्रिमिटिव रिकर्सिव होते हैं, जिससे मशीनीकरण कठिन हो जाता है। वैकल्पिक दृष्टिकोण जैसे कि डी ब्रुइन इंडिसेस (dBI), लोकली नेमलेस सिंटैक्स (locally nameless syntax), और हायर-ऑर्डर एब्स्ट्रैक्ट सिंटैक्स (HOAS) समाधान प्रदान करते हैं, लेकिन वे अपने स्वयं के दोष भी लाते हैं: dBI मानव पठनीयता के लिए बोझिल है; लोकली नेमलेस सिंटैक्स ऐसे वेल-फॉर्मडनेस प्रेडिकेट्स की आवश्यकता रखता है जो मेटा-थ्योरिटिकल परिणामों को "दूषित" कर देते हैं; और HOAS अक्सर निष्पादन योग्य कोड (executable code) के निर्माण या डैसिडेबिलिटी (decidability) प्रश्नों के निर्धारण को रोकता है।

लेखक एक ऐसे दृष्टिकोण की व्यवहार्यता का आकलन करने का लक्ष्य रखते हैं जो क्लासिकल सिंटैक्स (नामित वेरिएबल्स का उपयोग करके) को बनाए रखते हुए स्टौटन के सिमल्टेनियस सब्स्टीट्यूशन (Stoughton's simultaneous substitutions) का उपयोग करता है। यह विधि एक सिंगल स्ट्रक्चरल रिकर्सन के माध्यम से बाउंड वेरिएबल्स की रीनेमिंग को सब्स्टीट्यूशन के साथ समवर्ती रूप से करती है, जिससे अधिकांश प्रमाणों के लिए टर्म की लंबाई पर वेल-फाउंडेड इंडक्शन की आवश्यकता नहीं रहती।

कार्यप्रणाली (Methodology)
यह विकास पूरी तरह से Agda (v2.6.2.2) और स्टैंडर्ड लाइब्रेरी का उपयोग करके मशीन-चेक्ड है। कार्यप्रणाली निम्नलिखित मुख्य घटकों पर निर्भर करती है:

1. स्टौटन के सिमल्टेनियस सब्स्टीट्यूशन: सब्स्टीट्यूशन को वेरिएबल्स से $\lambda$-टर्म्स तक के फंक्शन के रूप में परिभाषित किया गया है ($Sub = V \to \Lambda$)। ऑपरेशन $M \bullet \sigma$ को स्ट्रक्चरल रिकर्सन द्वारा परिभाषित किया गया है। $\lambda$-एब्स्ट्रैक्शन और $\Pi$-टाइप्स के लिए, बाउंड वेरिएबल को एक फ्रेश नाम $y$ में रीनेम किया जाता है जिसे एक फंक्शन $X$ द्वारा चुना जाता है, और सब्स्टीट्यूशन को पुराने बाउंड वेरिएबल को इस नए नाम से मैप करने के लिए अपडेट किया जाता है। यह सुनिश्चित करता है कि प्रत्येक एब्स्ट्रैक्शन के लिए केवल एक ही रिकर्सिव कॉल की आवश्यकता होती है, जिससे प्रिमिटिव रिकर्सिवनेस बनी रहती है।
2. $\alpha$-कम्यूटेटिव संबंध: लेखक एक ऐसे संबंधों का सिद्धांत विकसित करते हैं जो $\alpha$-कन्वर्जन के साथ कम्यूट करते हैं। एक संबंध $S$ $\alpha$-कम्यूटिव है यदि $M \sim_\alpha N$ और $N S P$ होने पर एक $Q$ का अस्तित्व होता है ताकि $M S Q$ और $Q \sim_\alpha P$ हो। यह ढांचा लेखकों को $\alpha$-कन्वर्जन तक कन्फ्लुएंस (confluence) को स्पष्ट रूप से संभालने की अनुमति देता है, जिससे उन डुप्लीकेट लेम्माओं से बचा जा सके जो अन्य औपचारिकताओं में देखे जाते हैं।
3. कन्फ्लुएंस प्रूफ के लिए ताकाहाशी का संशोधन: मूल टैट और मार्टिन-लॉफ प्रूफ के बजाय, यह शोध पत्र पैरेलल रिडक्शन ($\Rightarrow$) का उपयोग करते हुए ताकाहाशी के संशोधन को अपनाता है। लेखक $\alpha$-कन्वर्जन नियमों के बिना पैरेलल रिडक्शन को परिभाषित करते हैं, और कन्फ्लुएंस सिद्ध करने के लिए पेंटागन प्रॉपर्टी (pentagon property - जो $\alpha$-कन्वर्जन तक डायमंड प्रॉपर्टी का सामान्यीकरण है) पर भरोसा करते हैं।
4. नॉर्मलाइजेशन धारणा (Normalization Assumption): कंसिस्टेंसी का प्रमाण इस धारणा पर आधारित है कि विचार किया जा रहा विशिष्ट PTS नॉर्मलाइजिंग है (प्रत्येक वेल-टाइप्ड टर्म वीकली नॉर्मलाइजिंग है)। लेखक नोट करते हैं कि इम्प्रेडिकेटिव सिस्टम्स के लिए नॉर्मलाइजेशन को Agda के भीतर सिद्ध करना संभवतः असंभव है क्योंकि Agda में मेटा-लैंग्वेज में इम्प्रेडिकेटिविटी का अभाव है।

प्रमुख योगदान
शोध पत्र तीन प्रमुख मेटा-थ्योरिटिकल गुणों के लिए औपचारिक प्रमाण प्रस्तुत करता है:

1. $\beta$-रिडक्शन का कन्फ्लुएंस: लेखक PTS के अंतर्निहित सिंटैक्स के लिए चर्च-रोसर (Church-Rosser) प्रमेय को सिद्ध करते हैं। $\alpha$-कम्यूटिव संबंधों के सिद्धांत और ताकाहाशी के पैरेलल रिडक्शन का उपयोग करते हुए, वे स्थापित करते हैं कि पैरेलल रिडक्शन का स्टार क्लोजर, मेनी-स्टेप $\beta$-रिडक्शन के साथ मेल खाता है और पेंटागन प्रॉपर्टी को संतुष्ट करता है।
2. सब्जेक्ट रिडक्शन (SR): शोध पत्र रिडक्शन के तहत टाइपिंग के संरक्षण को औपचारिक बनाता है। मैककिना और पोलक के विचारों का अनुसरण करते हुए, लेखक कॉन्टेक्स्ट्स तक रिडक्शन का विस्तार करते हैं और विषयों (subjects) के लिए कॉन्टेक्स्ट्स की वैधता और टाइपिंग के संरक्षण के संबंध में एक समवर्ती प्रमेय सिद्ध करते हैं। इसमें प्रोडक्ट इनजेक्टिविटी को सिद्ध करना शामिल है, जो इन्वर्जन के लिए एक महत्वपूर्ण लेम्मा है।
3. इम्प्रेडिकेटिव PTS के लिए कंसिस्टेंसी: लेखक इम्प्रेडिकेटिव PTS के एक विशिष्ट उपवर्ग (उन विशिष्ट एक्सिओम्स और रूल्स वाले जो $(\ast, \square) \in \mathcal{A}$ और $(\square, \ast, \ast) \in \mathcal{R}$ को संतुष्ट करते हैं) के लिए सिद्ध करते हैं कि टाइप $\Pi[x : s]x$ (जो करी-हावर्ड के तहत असत्यता का प्रतिनिधित्व करता है) खाली कॉन्टेक्स्ट में अनहैबिटेड (uninhabited) है। यह प्रमाण कोक्वैंड के पेन-एंड-पेपर प्रूफ (Calculus of Constructions के लिए) का विस्तार है। यह इंडक्टिवली डिफाइंड नॉर्मल और न्यूट्रल फॉर्म्स, इन्वर्जन लेम्माज, और अनुमानित नॉर्मलाइजेशन प्रॉपर्टी पर निर्भर करता है।

परिणाम और मूल्यांकन

• औपचारिक आकार (Formalization Size): संपूर्ण विकास लगभग 4,300 लाइन्स ऑफ कोड (LoC) का है, जिसमें 3,000 LoC स्टौटन के सब्स्टीट्यूशन और PTS सिंटैक्स के पिछले कार्य से है।
• तुलना: लेखक अपने कार्य की तुलना डी ब्रुइन इंडिसेस (बैरस और वर्नर, ~2,900 LoC) और लोकली नेमलेस सिंटैक्स (अडेमिर एट अल., ~4,800 LoC) का उपयोग करने वाले औपचारिकताओं से करते हैं। वे तर्क देते हैं कि उनका दृष्टिकोण आकार में तुलनीय है लेकिन उपयोग किए गए सिंटैक्स के संबंध में बेहतर पारदर्शिता प्रदान करता है, क्योंकि यह शास्त्रीय प्रस्तुति (जैसे कि वीकनिंग लेम्मा शास्त्रीय नोटेशन के लगभग समान दिखता है) के बहुत करीब है।
• व्यवहार्यता (Feasibility): परिणाम सुझाव देते हैं कि क्लासिकल सिंटैक्स और सिमल्टेनियस सब्स्टीट्यूशन का उपयोग करने वाला दृष्टिकोण डिपेंडेंट टाइप थ्योरी के लिए व्यवहार्य है। लेखक नोट करते हैं कि केवल कुछ ही लेम्माज को वेल-फाउंडेड इंडक्शन की आवश्यकता थी, और कोड का आकार "विस्फोटित" नहीं हुआ।

महत्ता और दावे
शोध पत्र का दावा है कि स्टौटन के सब्स्टीट्यूशन का उपयोग करने वाला दृष्टिकोण, विशेष रूप से $\alpha$-कन्वर्जन को संभालने के संबंध में, मेटा-थ्योरिटिकल समस्याओं के लिए "स्पष्ट प्रस्तुति और उपचार" प्रदान करता है। लेखक का कहना है कि उनका समाधान मानव पाठकों के लिए अधिक पारदर्शी है, क्योंकि यह ओपनिंग टर्म्स और फ्रेश पैरामीटर्स को मैन्युअल रूप से प्रबंधित करने के "नोटेशनल क्लटर" से बचता है।

इस कार्य का महत्व यह प्रदर्शित करने में है कि क्लासिकल सिंटैक्स को छोड़े बिना, यदि नॉर्मलाइजेशन को माना जाए, तो इम्प्रेडिकेटिव सिस्टम्स के लिए कंसिस्टेंसी का मशीन-चेक्ड प्रमाण प्राप्त करना संभव है। लेखक विनम्रतापूर्वक स्वीकार करते हैं कि इम्प्रेडिकेटिव थ्योरीज के लिए पूर्ण नॉर्मलाइजेशन का मशीनीकरण गोडेल के अपूर्णता प्रमेय (Gödel's incompleteness theorem) के प्रभावों के कारण Agda में संभवतः असंभव है, लेकिन कंसिस्टेंसी प्रूफ स्वयं ऐसे सिस्टम्स के लिए करेक्ट-बाय-कंस्ट्रक्शन टाइप-चेकिंग एल्गोरिदम की दिशा में एक महत्वपूर्ण कदम है। यह कार्य डिपेंडेंट टाइप थ्योरी के भविष्य के औपचारिककरण के लिए इस ढांचे की उपयोगिता के सत्यापन के रूप में कार्य करता है।