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

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

परिभाषाएँ <अवधि वर्ग = एंकर आईडी = परिभाषा>

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

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

परिणाम

यह खंड कुछ प्रसिद्ध परिणाम प्रस्तुत करता है। सबसे पहले, SN का अर्थ WN है। संगम (शब्द पुनर्लेखन) (संक्षिप्त सीआर) का अर्थ है 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} यूएन है लेकिन एनएफ नहीं है क्योंकि बी = सी, सी एक सामान्य रूप है, और बी सी को कम नहीं करता है। {a→b,a→c,b→b,c→c} एनएफ है क्योंकि कोई सामान्य रूप नहीं है, लेकिन सीआर नहीं है क्योंकि बी और सी को कम करता है, और बी, सी में कोई सामान्य कमी नहीं है।}

डब्ल्यूएन और यूएन^→ मतलब संगम। इसलिए सीआर, एनएफ, यूएन और यूएन^→ यदि 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 ⇒ ...) और लूप जैसे Collatz अनुमान के परिवर्तन समारोह (1 ⇒ 2 ⇒ 4 ⇒ 1 ⇒ ...) शामिल हैं। , अगर Collatz रूपांतरण के कोई अन्य लूप हैं तो यह एक खुली समस्या है)। एक अन्य उदाहरण एकल-नियम प्रणाली है { r(x,y) → r(y,x) }, जिसमें किसी भी शब्द से कोई सामान्य गुण नहीं है, उदा। r(4,2) एक एकल पुनर्लेखन क्रम शुरू होता है, अर्थात। r(4,2) → r(2,4) → r(4,2) → r(2,4) → ..., जो असीम रूप से लंबा है। यह मोडुलो क्रमविनिमेयता को फिर से लिखने के विचार की ओर ले जाता है जहां कोई नियम सामान्य रूप में होता है यदि कोई नियम नहीं है लेकिन कम्यूटेटिविटी लागू होती है।

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

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

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

शुद्ध अप्रकाशित लैम्ब्डा कैलकुलस मजबूत सामान्यीकरण संपत्ति को संतुष्ट नहीं करता है, और कमजोर सामान्यीकरण संपत्ति को भी नहीं। शब्द पर विचार करें $\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)$ दृढ़ता से सामान्यीकरण नहीं कर रहा है। और यह केवल कमी का क्रम है, इसलिए यह कमजोर रूप से सामान्यीकरण भी नहीं कर रहा है।

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

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

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

यह भी देखें

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