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

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

बीटा कमी

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

$(\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$

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

यह भी देखें

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