बीटा सामान्य रूप

लैम्ब्डा कैलकुलस में, यदि कोई लैम्ब्डा कैलकुलस#β-रिडक्शन संभव नहीं है, तो एक शब्द बीटा सामान्य रूप में होता है। एक शब्द बीटा-एटा सामान्य रूप में होता है यदि न तो बीटा कमी और न ही लैम्ब्डा कैलकुलस#η-कमी संभव है। यदि हेड पोजीशन में बीटा-रेडेक्स नहीं है तो एक शब्द हेड सामान्य रूप में होता है। किसी शब्द का सामान्य रूप, यदि कोई मौजूद है, अद्वितीय है (चर्च-रोसेर प्रमेय के परिणाम के रूप में)। हालाँकि, एक शब्द के एक से अधिक शीर्ष सामान्य रूप हो सकते हैं।

बीटा कमी

लैम्ब्डा कैलकुलस में, बीटा रिडेक्स फॉर्म का एक शब्द है:

$(\mathbf {\lambda } x.A)M$.

एक रेडेक्स $r$ एक पद में शीर्ष स्थान पर है $t$, अगर $t$ इसका आकार निम्नलिखित है (ध्यान दें कि अनुप्रयोग की प्राथमिकता अमूर्तता से अधिक है, और नीचे दिए गए सूत्र का अर्थ लैम्ब्डा-अमूर्त होना है, अनुप्रयोग नहीं):

$\lambda x_{1}\ldots \lambda x_{n}.\underbrace {(\lambda x.A)M_{1}} _{{\text{the redex }}r}M_{2}\ldots M_{m}$, कहाँ $n\geq 0$ और $m\geq 1$.

बीटा कमी एक शब्द में निहित बीटा रिडेक्स के लिए निम्नलिखित पुनर्लेखन नियम का एक अनुप्रयोग है:

$(\mathbf {\lambda } x.A)M\longrightarrow A[x:=M]$

कहाँ $A[x:=M]$ शब्द को प्रतिस्थापित करने का परिणाम है $M$ चर के लिए $x$ अवधि में $A$.

हेड बीटा रिडक्शन एक बीटा रिडक्शन है जिसे हेड पोजीशन में लागू किया जाता है, जो कि निम्नलिखित रूप में होता है:

$\lambda x_{1}\ldots \lambda x_{n}.(\lambda x.A)M_{1}M_{2}\ldots M_{m}\longrightarrow \lambda x_{1}\ldots \lambda x_{n}.A[x:=M_{1}]M_{2}\ldots M_{m}$, कहाँ $n\geq 0$ और $m\geq 1$.

कोई भी अन्य कमी आंतरिक बीटा कमी है।

'सामान्य रूप' एक ऐसा शब्द है जिसमें कोई बीटा रेडेक्स नहीं होता है, यानी उसे और कम नहीं किया जा सकता. 'हेड नॉर्मल फॉर्म' एक ऐसा शब्द है जिसमें हेड पोजीशन में बीटा रिडेक्स शामिल नहीं होता है, यानी इसे हेड रिडक्शन द्वारा और कम नहीं किया जा सकता है। सरल लैम्ब्डा कैलकुलस पर विचार करते समय (अर्थात स्थिरांक या फ़ंक्शन प्रतीकों को जोड़े बिना, जिसका अर्थ अतिरिक्त डेल्टा नियम द्वारा कम किया जाना है), शीर्ष सामान्य रूप निम्नलिखित आकार के शब्द हैं:

$\lambda x_{1}\ldots \lambda x_{n}.xM_{1}M_{2}\ldots M_{m}$, कहाँ $x$ एक परिवर्तनशील है, $n\geq 0$ और $m\geq 0$.

सिर का सामान्य रूप हमेशा सामान्य रूप नहीं होता,क्योंकि लागू तर्क $M_{j}$ सामान्य होने की आवश्यकता नहीं है. हालाँकि, इसका उलटा सच है: कोई भी सामान्य रूप भी एक प्रमुख सामान्य रूप है।वास्तव में, सामान्य रूप बिल्कुल शीर्ष सामान्य रूप होते हैं जिनमें उपपद होते हैं $M_{j}$ स्वयं सामान्य रूप हैं। यह सामान्य रूपों का आगमनात्मक वाक्यविन्यास विवरण देता है।

कमजोर शीर्ष सामान्य रूप की भी धारणा है: कमजोर शीर्ष सामान्य रूप में एक शब्द या तो सिर सामान्य रूप में एक शब्द है या एक लैम्ब्डा अमूर्त है। इसका मतलब है कि लैम्ब्डा बॉडी के अंदर एक रेडेक्स दिखाई दे सकता है।

कमी की रणनीतियाँ

सामान्य तौर पर, किसी दिए गए शब्द में कई रिडेक्स शामिल हो सकते हैं, इसलिए कई अलग-अलग बीटा कटौती लागू की जा सकती हैं। हम किस रिडेक्स को कम करना है यह चुनने के लिए एक कटौती रणनीति (लैम्ब्डा कैलकुलस) निर्दिष्ट कर सकते हैं।

• सामान्य-क्रम कटौती वह रणनीति है जिसमें व्यक्ति सिर की स्थिति में बीटा कमी के नियम को लगातार लागू करता है जब तक कि ऐसी और कटौती संभव न हो जाए। उस बिंदु पर, परिणामी पद सामान्य रूप में होता है। फिर कोई उपशर्तों में हेड रिडक्शन लागू करना जारी रखता है $M_{j}$, बाएं से दाएं। अन्यथा कहा गया है, सामान्य-क्रम कटौती वह रणनीति है जो हमेशा सबसे पहले बाएं-सबसे बाहरी-सबसे रिडेक्स को कम करती है।
• इसके विपरीत, एप्लिकेटिव ऑर्डर कटौती में, कोई पहले आंतरिक कटौती लागू करता है, और उसके बाद केवल हेड कटौती लागू करता है जब कोई और आंतरिक कटौती संभव नहीं होती है।

सामान्य-क्रम में कमी इस अर्थ में पूर्ण है कि यदि किसी पद का शीर्ष सामान्य रूप है, तो सामान्य-क्रम में कमी अंततः उस तक पहुंच जाएगी। उपरोक्त सामान्य रूपों के वाक्यविन्यास विवरण के अनुसार, इसमें "पूरी तरह से" सामान्य रूप के लिए एक ही कथन शामिल है (यह मानकीकरण प्रमेय है)। इसके विपरीत, लागू आदेश में कमी समाप्त नहीं हो सकती है, भले ही शब्द का सामान्य रूप हो। उदाहरण के लिए, एप्लिकेटिव ऑर्डर कटौती का उपयोग करते हुए, कटौती का निम्नलिखित क्रम संभव है:

${\begin{aligned}&(\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\&\ldots \end{aligned}}$

लेकिन सामान्य क्रम में कमी का उपयोग करते हुए, वही प्रारंभिक बिंदु जल्दी से सामान्य रूप में कम हो जाता है:

$(\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))$

$\rightarrow z$

सिनोट के निर्देशक स्ट्रिंग ्स एक ऐसी विधि है जिसके द्वारा बीटा कमी की कम्प्यूटेशनल जटिलता को अनुकूलित किया जा सकता है।

यह भी देखें

• लैम्ब्डा कैलकुलस
• सामान्य रूप (बहुविकल्पी)