लैम्ब्डा कैलकुस में, यदि किसी शब्द का सामान्य रूप है, तो सामान्य आदेश कमी रणनीति हमेशा इसका उत्पादन करेगी।लैम्ब्डा कैलकुस, सामान्य ऑर्डर, सामान्य फॉर्म,
मुझे आश्चर्य है कि उपरोक्त प्रस्ताव को सख्ती से कैसे साबित करना है?
परिणाम जिसका आप उल्लेख करते हैं, तथाकथित मानकीकरण प्रमेय का एक सारांश है, यह बताते हुए कि किसी भी कमी अनुक्रम एम-> एन के लिए एक ही "मानक" एक ही शब्द एम और एन के बीच है, जहां आप बाईं ओर बाहरी में लाल रंग निष्पादित करते हैं आदेश। सबूत इतना छोटा नहीं है, और साहित्य में कई अलग-अलग दृष्टिकोण हैं। मैं नीचे एक छोटी ग्रंथसूची जोड़ता हूं।
काशीमा 5 द्वारा हालिया सबूत (1 पर भी देखें) अवशिष्ट की धारणा का उपयोग न करने और पूरी तरह से अपरिवर्तनीय तकनीकों के आधार पर होने का लाभ नहीं है। यह औपचारिकरण 2 के लिए भी अच्छा है, लेकिन जब तक कि आप इस विषय से पहले से ही आत्मविश्वास नहीं रखते हैं, यह विशेष रूप से निर्देशक नहीं है।
मानकीकरण के पीछे सामान्य विचार निम्नलिखित है। दो redexes आर और एस, जहां एस आर के संबंध में वाम-पंथी सबसे बाहरी स्थिति में है, और निम्न कमी पर विचार करने के मान लीजिए: आप एस फायरिंग, बजाय शुरू कर सकते हैं, तो फिर
R S
M -> P -> N
, लेकिन इस तरह से आप संभवतया रेडएक्स आर को डुप्लिकेट (या मिटाना) कर सकते हैं। ये रेडियक्स, जो अनिवार्य रूप से एस को फायरिंग के बाद आर के बने रहते हैं, को अवशिष्ट कहा जाता है, और आमतौर पर आर/एस (पढ़ा जाता है: एस के बाद आर के अवशेष) के रूप में इंगित किया जाता है। तो, बुनियादी लेम्मा कि
R S = S (R/S)
आदेश मानकीकरण के लिए इसका इस्तेमाल करने के लिए, हम एक मनमाना अनुक्रम ρ (है कि हम सबसे बाईं ओर के सबसे बाहरी स्थिति wrt में कोई redex साथ, मानक होने के लिए मान सकते हैं करने के लिए आर सामान्यीकरण करने की जरूरत है एस)। यह अभी भी सच है कि
(*) ρS = S (ρ/S)
लेकिन क्या इतना स्पष्ट नहीं है (ρ/एस) के मानकीकरण है। इस उद्देश्य के लिए, हमें देखते हैं कि एसआर = सी [\ xM एन] को फायर करने से पहले ρ किया गया था, अनिवार्य रूप से तीन डिस्कनेक्टेड क्षेत्रों में शब्द को विभाजित करता है: संदर्भ सी, एम, और एन यह ρ की पुनरावृत्ति को प्रेरित करता है लगातार तीन दृश्यों में:
ρ1 inside M
ρ2 inside N
ρ3 inside C
(याद रखें कि कोई redex वाम-पंथी सबसे बाहरी स्थिति wrt एस में था)। डुप्लीकेट (या मिटाया जा सकता है) का एकमात्र हिस्सा ρ2 है, और शेष ρ2-0 ... ρ2-k को आसानी से की विभिन्न स्थितियों के अनुसार आदेश दिया गया है जो एस की गोलीबारी द्वारा बनाई गई एन की प्रतियां हैं। तो
S ρ1 ρ2-0 ... ρ2-k ρ_3
(*) का मानक संस्करण है।
मूल ग्रंथसूची।
1 एएस्पेर्टी, जेजे। लेवी। The cost of usage in the lambda-calculus। एलआईसीएस 2013.
3 एच पी बारेन्ड्रेग। लैम्ब्डा कैलकुलस, नॉर्थ-हॉलैंड (1 9 84)।
4 जी। गोंथियर, जेजे। लेवी, पीए। Mellies। An abstract standardisation theorem। एलआईसीएस 9 2 9।
2 एफ। गुइडी। Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover। औपचारिक तर्क का जर्नल 5 (1): 1-25, 2012.
5 आर। कशिमा। A proof of the standardization theorem in lambda-calculus। तकनीकी रिपोर्ट सी-145, टोक्यो इंस्टीट्यूट ऑफ टेक्नोलॉजी, 2000.
[6] जेडब्ल्यू। Klop। कॉम्बिनेटरी कमी प्रणाली। पीएचडी थीसिस, सीडब्ल्यूआई, एम्स्टर्डम, 1 9 80।
[7] जी। मिट्स्के। लैम्ब्डा-कैलकुस के लिए मानकीकरण प्रमेय। जेड मैथ। लॉजिक। Grundlag। गणित, 25: 2 9 -31, 1 9 7 9
[8] एम। ताकाहाशी। लैम्ब्डा-कैलकुस में समानांतर कमी। सूचना और गणना 118, पीपी.120-127, 1 99 5।
[9] एच। Xi, Upper bounds for standardizations and an application। जर्नल ऑफ़ सिंबलोक लॉजिक 64, पीपी.2 9 1-303, 1 999।
मुझे लगता है कि आपका मतलब चर्च रस्सी "प्रमेय" – nicolas