सामान्य रूप (सार पुनर्लेखन)

सार पुनर्लेखन में एक वस्तु सामान्य रूप में होती है यदि इसे आगे फिर से नहीं लिखा जा सकता है अर्थात यह अप्रासंगिक है। पुनर्लेखन प्रणाली के आधार पर एक वस्तु कई सामान्य रूपों में फिर से लिख सकती है या पूर्ण रूप से भी नहीं पुनर्लेखन प्रणालियों के कई गुण सामान्य रूपों से संबंधित हैं।

परिभाषाएँ

औपचारिक रूप से कहा गया है, यदि (A,→) एक अमूर्त पुनर्लेखन प्रणाली या परिभाषा है, x∈A 'सामान्य रूप' में है यदि कोई y∈A उपस्थित नहीं है जैसे कि x→y, यानी x एक अप्रासंगिक शब्द है।

एक वस्तु a 'अशक्त रूप से सामान्यीकरण' है यदि वहाँ से प्रारंभ होने वाले पुनर्लेखन का कम से कम एक विशेष क्रम उपस्थित है जो अंततः एक सामान्य रूप देता है। एक पुनर्लेखन प्रणाली में 'अशक्त सामान्यीकरण गुण' होता है या (अशक्त ) सामान्यीकरण (डब्ल्यू एन) होता है यदि प्रत्येक वस्तु अशक्त रूप से सामान्य हो रही हो। एक वस्तु a 'दृढ़ता से सामान्य' होती है यदि a से प्रारंभ होने वाले पुनर्लेखन का प्रत्येक क्रम अंततः सामान्य रूप से समाप्त हो जाता है। एक सार पुनर्लेखन प्रणाली जोरदार सामान्यीकरण समाप्ति नोथेरियन है, या '(शसक्त) सामान्यीकरण संपत्ति' (एसएन) है यदि इसकी प्रत्येक वस्तु दृढ़ता से सामान्य हो रही है।

एक पुनर्लेखन प्रणाली में सामान्य रूप गुण (एनएफ) होता है यदि सभी वस्तुओं के लिए a और सामान्य रूप b, b को पुनर्लेखन की एक श्रृंखला द्वारा a से पहुँचा जा सकता है और व्युत्क्रम पुनर्लेखन केवल तभी होता है जब a b तक कम हो जाता है। एक पुनर्लेखन प्रणाली में अद्वितीय सामान्य रूप गुण (यूएन) होता है यदि सभी सामान्य रूपों के लिए a, b ∈ S, a तक b से पुनर्लेखन की श्रृंखला द्वारा पहुँचा जा सकता है और व्युत्क्रम पुनर्लेखन केवल तभी होता है जब a, b के समान हो एक पुनर्लेखन प्रणाली में कमी के संबंध में विशिष्ट सामान्य रूप की संपत्ति होती है (UN^→) यदि प्रत्येक पद को सामान्य रूपों a और b में कम करने के लिए, a, b के समान है।

परिणाम

यह खंड कुछ प्रसिद्ध परिणाम प्रस्तुत करता है। सबसे पहले, SN का अर्थ WN है।

संगम (संक्षिप्त CR) का अर्थ है NF का अर्थ है UN का अर्थ है UN^→ उत्क्रम निहितार्थ सामान्यतः पकड़ में नहीं आते हैं। ^{{a→b,a→c,c→c,d→c,d→e} UN→ है किंतु UN नहीं क्योंकि b=e और b,e सामान्य रूप हैं।{a→b,a→c,b→b} UN है किंतु NF नहीं है क्योंकि b=c, c एक सामान्य रूप है, और बी सी को कम नहीं करता है। {a→b,a→c,b→b,c→c} NF है क्योंकि कोई सामान्य रूप नहीं है किंतु CR नहीं है क्योंकि b और c को कम करता है, और b,c में कोई सामान्य कमी नहीं है।WN और UN→ अर्थ संगम इसलिए CR, NF , UN और UN→ यदि WN धारण करता है तो मेल खाता है।}

उदाहरण

एक उदाहरण यह है कि अंकगणितीय व्यंजकों को सरल बनाने से एक संख्या उत्पन्न होती है - अंकगणित में सभी संख्याएँ सामान्य रूप होती हैं। एक उल्लेखनीय तथ्य यह है कि सभी अंकगणितीय अभिव्यक्तियों का एक अद्वितीय मान है इसलिए पुनर्लेखन प्रणाली दृढ़ता से सामान्यीकृत और संगम है:

(3 + 5) * (1 + 2) ⇒ 8 * (1 + 2) ⇒ 8 * 3 ⇒ 24

(3 + 5) * (1 + 2) ⇒ (3 + 5) * 3 ⇒ 3*3 + 5*3 ⇒ 9 + 5*3 ⇒ 9 + 15 ⇒ 24

गैर-सामान्यीकृत प्रणालियों के उदाहरणों (अशक्त या दृढ़ता से नहीं) में अनंत तक गिनती (1 ⇒ 2 ⇒ 3 ⇒ ...) और लूप जैसे कोलात्ज़ अनुमान के परिवर्तन कार्य (1 ⇒ 2 ⇒ 4 ⇒ 1 ⇒ ...) सम्मिलित हैं। यदि कोलात्ज़ रूपांतरण के कोई अन्य लूप हैं तो यह एक विवर्त समस्या है)। एक अन्य उदाहरण एकल-नियम प्रणाली है { { r(x,y) → r(y,x) }, जिसमें किसी भी शब्द से कोई सामान्य गुण नहीं है, उदा। r(4,2) एक एकल पुनर्लेखन क्रम प्रारंभ होता है, अर्थात r(4,2) → r(2,4) → r(4,2) → r(2,4) → ..., जो असीम रूप से लंबा है। यह मोडुलो क्रमविनिमेयता को फिर से लिखने के विचार की ओर ले जाता है जहां कोई नियम सामान्य रूप में होता है यदि कोई नियम नहीं है किंतु कम्यूटेटिविटी प्रयुक्त होती है।

अशक्त किंतु दृढ़ता से पुनर्लेखन प्रणाली को सामान्य नहीं कर रहा है

प्रणाली {b → a, b → c, c → b, c → d} (चित्रित) अशक्त सामान्यीकरण का एक उदाहरण है, किंतु दृढ़ता से सामान्यीकरण प्रणाली नहीं है। a और d सामान्य रूप हैं, और b और c को a या d में घटाया जा सकता है, किंतु अनंत कमी b → c → b → c → ... का अर्थ है कि न तो b और न ही c दृढ़ता से सामान्यीकरण कर रहा है।

अनटाइप्ड लैम्ब्डा कैलकुलस

शुद्ध अप्रकाशित लैम्ब्डा कैलकुलस शसक्त सामान्यीकरण संपत्ति को संतुष्ट नहीं करता है, और अशक्त सामान्यीकरण संपत्ति को भी नहीं शब्द $\lambda x.xxx$ पर विचार करें। (अनुप्रयोग बाएं साहचर्य है) इसका निम्नलिखित पुनर्लेखन नियम है: किसी भी पद $t$ के लिए,

$(\mathbf {\lambda } x.xxx)t\rightarrow ttt$

किंतु विचार करें कि जब हम $\lambda x.xxx$ प्रयुक्त करते हैं तो क्या होता है खुद के लिए:

${\begin{aligned}(\mathbf {\lambda } x.xxx)(\lambda x.xxx)&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow \ \cdots \,\end{aligned}}$

इसलिए शब्द $(\lambda x.xxx)(\lambda x.xxx)$ दृढ़ता से सामान्यीकरण नहीं कर रहा है। और यह केवल कमी का क्रम है इसलिए यह अशक्त रूप से सामान्यीकरण भी नहीं कर रहा है।

लैम्ब्डा कैलकुलस टाइप किया

टाइप किए गए लैम्ब्डा कैलकुलस की विभिन्न प्रणालियाँ जिनमें सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस जीन-यवेस गिरार्ड के प्रणाली एफ और थिएरी कोक्वांड के निर्माण के कैलकुलस सम्मिलित हैं दृढ़ता से सामान्यीकरण कर रहे हैं।

सामान्यीकरण संपत्ति के साथ एक लैम्ब्डा कैलकुलस प्रणाली को एक प्रोग्रामिंग भाषा के रूप में देखा जा सकता है, जिसमें संपत्ति का प्रत्येक कार्यक्रम समाप्ति विश्लेषण होता है। चूँकि यह एक बहुत ही उपयोगी संपत्ति है इसमें एक खामी है: सामान्यीकरण संपत्ति के साथ एक प्रोग्रामिंग भाषा ट्यूरिंग पूर्ण नहीं हो सकती है, अन्यथा कोई प्रोग्राम के प्रकार की जांच करके हॉल्टिंग समस्या को हल कर सकता है। इसका अर्थ यह है कि ऐसे संगणनीय कार्य हैं जिन्हें केवल टाइप किए गए लैम्ब्डा कैलकुलस में परिभाषित नहीं किया जा सकता है, और इसी तरह निर्माण और प्रणाली एफ के कैलकुलस के लिए एक विशिष्ट उदाहरण कुल प्रोग्रामिंग भाषा में एक स्व-दुभाषिया का है।

यह भी देखें

• कानूनी फॉर्म
• टाइप लैम्ब्डा कैलकुस
• पुनर्लेखन
• कुल कार्यात्मक प्रोग्रामिंग
• बारेन्ड्रेगट-गेवर-क्लॉप अनुमान
• न्यूमैन की लेम्मा
• मूल्यांकन द्वारा सामान्यीकरण