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

बस टाइप किया हुआ लैम्ब्डा कैलकुस ($\lambda ^{\to }$), एक प्रपत्र प्रकार सिद्धांत , केवल एक प्रकार के कंस्ट्रक्टर के साथ लैम्ब्डा कैलकुलस का टाइप किया हुआ लैम्ब्डा कैलकुलस है ($\to$) जो फ़ंक्शन प्रकार बनाता है। यह टाइप किए गए लैम्ब्डा कैलकुस का प्रामाणिक और सरल उदाहरण है। सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस को मूल रूप से अलोंजो चर्च द्वारा 1940 में अनटाइप्ड लैम्ब्डा कैलकुलस के विरोधाभासी उपयोग से बचने के प्रयास के रूप में पेश किया गया था।

शब्द सरल प्रकार का उपयोग केवल टाइप किए गए लैम्ब्डा गणना जैसे कार्टेशियन उत्पाद, सहउत्पाद या प्राकृतिक संख्या (डायलेक्टिका व्याख्या) या यहां तक ​​​​कि पूर्ण प्रत्यावर्तन (जैसे कंप्यूटेबल फ़ंक्शंस के लिए प्रोग्रामिंग भाषा) के एक्सटेंशन को संदर्भित करने के लिए भी किया जाता है। इसके विपरीत, सिस्टम जो पैरामीट्रिक बहुरूपता (जैसे सिस्टम एफ) या आश्रित प्रकार (जैसे एलएफ (तार्किक ढांचा)) पेश करते हैं, उन्हें केवल टाइप नहीं माना जाता है। सरल प्रकार, पूर्ण पुनरावर्तन को छोड़कर, अभी भी सरल माने जाते हैं क्योंकि ऐसी संरचनाओं के चर्च एन्कोडिंग केवल का उपयोग करके किया जा सकता है $\to$ और उपयुक्त प्रकार चर, जबकि बहुरूपता (जीव विज्ञान) और निर्भरता नहीं हो सकती।

सामान्य रूप से टाइप किया गया लैम्ब्डा कैलकुलस प्रपोजल अंतर्ज्ञानवादी तर्क के इम्प्लीकेशनल फ्रैगमेंट से निकटता से संबंधित है, यानी करी-हावर्ड आइसोमोर्फिज्म के माध्यम से न्यूनतम तर्क: शब्द प्राकृतिक कटौती में प्रमाणों के अनुरूप हैं, और आवास टाइप करें वास्तव में मिनिमम का टॉटोलॉजी (तर्क) है। तर्क।

सिंटेक्स

इस लेख में, प्रतीक $\sigma$ और $\tau$ प्रकार से अधिक श्रेणी के लिए उपयोग किया जाता है। अनौपचारिक रूप से, फ़ंक्शन प्रकार $\sigma \to \tau$ प्रकार के इनपुट को देखते हुए, प्रकार्यों के प्रकार को संदर्भित करता है $\sigma$, प्रकार का आउटपुट उत्पन्न करें $\tau$. रिवाज के सन्दर्भ मे, $\to$ दाईं ओर सहयोगी: $\sigma \to \tau \to \rho$ के रूप में पढ़ा जाता है $\sigma \to (\tau \to \rho )$.

प्रकारों को परिभाषित करने के लिए, आधार प्रकारों का एक सेट, $B$, पहले परिभाषित किया जाना चाहिए। इन्हें कभी-कभी परमाणु प्रकार या प्रकार स्थिरांक कहा जाता है। इस निश्चित के साथ, प्रकारों का सिंटैक्स है:

$\tau ::=\tau \to \tau \mid T\quad \mathrm {where} \quad T\in B$.

उदाहरण के लिए, $B=\{a,b\}$, से शुरू होने वाले प्रकारों का एक अनंत सेट उत्पन्न करता है $a,b,$$a\to a,$$a\to b,b\to b,$$b\to a,$$a\to (a\to a),\ldots ,$$(b\to a)\to (a\to b),\ldots$ आधार प्रकारों के लिए पद स्थिरांकों का एक समुच्चय भी निश्चित होता है। उदाहरण के लिए, यह माना जा सकता है कि आधार प्रकार nat, और पद स्थिरांक प्राकृत संख्याएँ हो सकती हैं। मूल प्रस्तुति में, चर्च ने केवल दो आधार प्रकारों का प्रयोग किया: $o$ प्रस्तावों के प्रकार के लिए और $\iota$ व्यक्तियों के प्रकार के लिए। प्ररूप $o$ कोई शब्द स्थिरांक नहीं है, जबकि $\iota$ एक पद स्थिर है। अक्सर केवल एक आधार प्रकार के साथ कलन, आमतौर पर $o$, माना जाता है।

बस टाइप किए गए लैम्ब्डा कैलकुलस का सिंटैक्स अनिवार्य रूप से लैम्ब्डा कैलकुलस का ही है। शब्द $x\mathbin {:} \tau$ दर्शाता है कि चर $x$ प्रकार का है $\tau$. बैकस-नौर रूप में सिंटैक्स शब्द तब है:

$e::=x\mid \lambda x\mathbin {:} \tau .e\mid e\,e\mid c$

कहाँ $c$ एक स्थिरांक है।

यही है, चर संदर्भ, अमूर्तता, अनुप्रयोग और स्थिरांक। एक चर संदर्भ $x$ बाध्य है अगर यह एक अमूर्त बंधन के अंदर है $x$. यदि कोई अनबाउंड चर नहीं हैं तो एक शब्द बंद हो जाता है।

इसकी तुलना में, अनटाइप्ड लैम्ब्डा कैलकुलस के सिंटैक्स में ऐसा कोई टाइपिंग या शब्द स्थिरांक नहीं है:

$e::=x\mid \lambda x.e\mid e\,e$

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

टाइपिंग नियम

किसी दिए गए प्रकार के अच्छी तरह से टाइप किए गए लैम्ब्डा शब्दों के सेट को परिभाषित करने के लिए, शब्दों और प्रकारों के बीच एक टाइपिंग संबंध को परिभाषित करता है। सबसे पहले, व्यक्ति टाइपिंग संदर्भों या टाइपिंग परिवेशों का परिचय देता है $\Gamma ,\Delta ,\dots$, जो टाइपिंग मान्यताओं के सेट हैं। एक टाइपिंग धारणा का रूप है $x\mathbin {:} \sigma$, अर्थ $x$ प्रकार है $\sigma$.

टाइपिंग संबंध $\Gamma \vdash e\mathbin {:} \sigma$ दर्शाता है कि $e$ प्रकार का शब्द है $\sigma$ संदर्भ में $\Gamma$. इस मामले में $e$ कहा जाता है कि अच्छी तरह से टाइप किया गया है (type $\sigma$). टंकण संबंध के उदाहरणों को टंकण निर्णय कहा जाता है। एक टाइपिंग निर्णय की वैधता एक टाइपिंग व्युत्पत्ति प्रदान करके दिखाई जाती है, जिसे टाइपिंग नियमों का उपयोग करके बनाया गया है (जिसमें लाइन के ऊपर का परिसर हमें लाइन के नीचे निष्कर्ष निकालने की अनुमति देता है)। सीधे शब्दों में टाइप किया गया लैम्ब्डा कैलकुलस इन नियमों का उपयोग करता है:

${\frac {x\mathbin {:} \sigma \in \Gamma }{\Gamma \vdash x\mathbin {:} \sigma }}$ (1)	${\frac {c{\text{ is a constant of type }}T}{\Gamma \vdash c\mathbin {:} T}}$ (2)
${\frac {\Gamma ,x\mathbin {:} \sigma \vdash e\mathbin {:} \tau }{\Gamma \vdash (\lambda x\mathbin {:} \sigma .~e)\mathbin {:} (\sigma \to \tau )}}$ (3)	${\frac {\Gamma \vdash e_{1}\mathbin {:} \sigma \to \tau \quad \Gamma \vdash e_{2}\mathbin {:} \sigma }{\Gamma \vdash e_{1}~e_{2}\mathbin {:} \tau }}$ (4)

शब्दों में,

1. अगर $x$ प्रकार है $\sigma$ संदर्भ में, तब $x$ प्रकार है $\sigma$.
2. पद स्थिरांक के उपयुक्त आधार प्रकार होते हैं।
3. यदि, एक निश्चित संदर्भ में $x$ प्रकार होना $\sigma$, $e$ प्रकार है $\tau$, फिर, उसी संदर्भ में बिना $x$, $\lambda x\mathbin {:} \sigma .~e$ प्रकार है $\sigma \to \tau$.
4. अगर, एक निश्चित संदर्भ में, $e_{1}$ प्रकार है $\sigma \to \tau$, और $e_{2}$ प्रकार है $\sigma$, तब $e_{1}~e_{2}$ प्रकार है $\tau$.

बंद शर्तों के उदाहरण, यानी खाली संदर्भ में टाइप करने योग्य शब्द हैं:

• हर प्रकार के लिए $\tau$, अवधी $\lambda x\mathbin {:} \tau .x\mathbin {:} \tau \to \tau$ (पहचान समारोह / मैं-संयोजक),
• प्रकार के लिए $\sigma ,\tau$, अवधी $\lambda x\mathbin {:} \sigma .\lambda y\mathbin {:} \tau .x\mathbin {:} \sigma \to \tau \to \sigma$ (के-कॉम्बिनेटर), और
• प्रकार के लिए $\tau ,\tau ',\tau ''$, अवधी $\lambda x\mathbin {:} \tau \to \tau '\to \tau ''.\lambda y\mathbin {:} \tau \to \tau '.\lambda z\mathbin {:} \tau .xz(yz):(\tau \to \tau '\to \tau '')\to (\tau \to \tau ')\to \tau \to \tau ''$ (एस-कॉम्बिनेटर)।

ये संयोजन तर्क के बेसिक कॉम्बिनेटर्स के टाइप किए गए लैम्ब्डा कैलकुलस रिप्रेजेंटेशन हैं।

प्रत्येक प्रकार $\tau$ एक आदेश, एक संख्या सौंपी जाती है $o(\tau )$. आधार प्रकार के लिए $o(T)=0$; समारोह प्रकार के लिए, $o(\sigma \to \tau )={\mbox{max}}(o(\sigma )+1,o(\tau ))$. अर्थात्, एक प्रकार का क्रम सबसे बाएँ-नेस्टेड तीर की गहराई को मापता है। इस तरह:

$o(\iota \to \iota \to \iota )=1$

$o((\iota \to \iota )\to \iota )=2$

शब्दार्थ

आंतरिक बनाम बाहरी व्याख्या

मोटे तौर पर, सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस को अर्थ देने के दो अलग-अलग तरीके हैं, जैसे टाइप की गई भाषाओं के लिए, जिन्हें विभिन्न प्रकार से इंट्रिंसिक बनाम एक्सट्रिंसिक, ऑन्कोलॉजिकल बनाम सिमेंटिकल, या चर्च-शैली बनाम करी-शैली कहा जाता है। एक आंतरिक शब्दार्थ केवल अच्छी तरह से टाइप किए गए शब्दों को अर्थ प्रदान करता है, या अधिक सटीक रूप से, टाइपिंग व्युत्पत्तियों को सीधे अर्थ प्रदान करता है। इसका प्रभाव यह है कि केवल एनोटेशन के प्रकार से भिन्न होने वाले शब्दों को फिर भी अलग-अलग अर्थ दिए जा सकते हैं। उदाहरण के लिए, पहचान शब्द $\lambda x\mathbin {:} {\mathtt {int}}.~x$ पूर्णांक और पहचान शब्द पर $\lambda x\mathbin {:} {\mathtt {bool}}.~x$ बूलियन पर अलग-अलग चीजों का मतलब हो सकता है। (क्लासिक इरादा व्याख्याएं पूर्णांकों पर पहचान फलन और बूलियन मानों पर पहचान फलन हैं।) इसके विपरीत, एक बाहरी शब्दार्थ टाइपिंग की परवाह किए बिना शब्दों को अर्थ प्रदान करता है, क्योंकि उनकी व्याख्या एक अप्रकाशित भाषा में की जाएगी। इस दृश्य में, $\lambda x\mathbin {:} {\mathtt {int}}.~x$ और $\lambda x\mathbin {:} {\mathtt {bool}}.~x$ मतलब एक ही चीज़ (यानी, एक ही चीज़ के रूप में $\lambda x.~x$).

आंतरिक और बाह्य शब्दार्थ के बीच का अंतर कभी-कभी लैम्ब्डा सार पर एनोटेशन की उपस्थिति या अनुपस्थिति से जुड़ा होता है, लेकिन वास्तव में यह प्रयोग सटीक नहीं है। केवल प्रकारों को अनदेखा करके (अर्थात, प्रकार विलोपन के माध्यम से) एनोटेट शर्तों पर एक बाहरी शब्दार्थ को परिभाषित करना संभव है, क्योंकि यह संभव है कि जब संदर्भ से (यानी, प्रकार के माध्यम से) अनुमान लगाया जा सकता है, तो असंबद्ध शब्दों पर एक आंतरिक शब्दार्थ दिया जा सकता है। ). आंतरिक और बाह्य दृष्टिकोण के बीच आवश्यक अंतर यह है कि क्या टाइपिंग नियमों को भाषा को परिभाषित करने के रूप में देखा जाता है, या अधिक आदिम अंतर्निहित भाषा के गुणों को सत्यापित करने के लिए औपचारिकता के रूप में देखा जाता है। नीचे चर्चा की गई अधिकांश विभिन्न शब्दार्थ व्याख्याओं को आंतरिक या बाह्य परिप्रेक्ष्य के माध्यम से देखा जा सकता है।

समीकरण सिद्धांत

सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस में βη-तुल्यता का समान समीकरण सिद्धांत है, जैसा कि अनटाइप्ड लैम्ब्डा कैलकुलस # रिडक्शन है, लेकिन टाइप प्रतिबंधों के अधीन है। बीटा कमी के लिए समीकरण

$(\lambda x\mathbin {:} \sigma .~t)\,u=_{\beta }t[x:=u]$

संदर्भ में रखता है $\Gamma$ जब कभी भी $\Gamma ,x\mathbin {:} \sigma \vdash t\mathbin {:} \tau$ और $\Gamma \vdash u\mathbin {:} \sigma$, जबकि ईटीए कमी के लिए समीकरण

$\lambda x\mathbin {:} \sigma .~t\,x=_{\eta }t$

जब भी रखता है $\Gamma \vdash t\!:\sigma \to \tau$ और $x$ में मुक्त नहीं दिखता $t$.

परिचालन शब्दार्थ

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

स्पष्ट शब्दार्थ

बस टाइप किया हुआ लैम्ब्डा कैलकुलस (साथ $\beta \eta$-equivalence) कार्तीय बंद श्रेणियों (CCCs) की आंतरिक भाषा है, जैसा कि पहली बार जोआचिम लैम्बेक द्वारा देखा गया था। किसी भी विशिष्ट सीसीसी को देखते हुए, संबंधित लैम्ब्डा कैलकुस के मूल प्रकार केवल वस्तु (श्रेणी सिद्धांत) हैं, और शर्तें morphisms हैं। इसके विपरीत, प्रत्येक सामान्य रूप से टाइप किया गया लैम्ब्डा कैलकुलस एक CCC देता है जिसकी वस्तुएँ प्रकार होती हैं, और morphisms शब्दों के तुल्यता वर्ग होते हैं।

पत्राचार को स्पष्ट करने के लिए, कार्टेशियन उत्पाद के लिए एक प्रकार का निर्माता आमतौर पर ऊपर जोड़ा जाता है। उत्पाद (श्रेणी सिद्धांत) को संरक्षित करने के लिए, युग्मन, प्रक्षेपण और एक इकाई शब्द के लिए टाइपिंग नियम जोड़े जाते हैं। दो शर्तें दी गई हैं $s\mathbin {:} \sigma$ और $t\mathbin {:} \tau$, शब्द $(s,t)$ प्रकार है $\sigma \times \tau$. इसी तरह, अगर किसी का कार्यकाल है $u\mathbin {:} \tau _{1}\times \tau _{2}$, तो शर्तें हैं $\pi _{1}(u)\mathbin {:} \tau _{1}$ और $\pi _{2}(u)\mathbin {:} \tau _{2}$ जहां $\pi _{i}$ कार्टेशियन उत्पाद के अनुमानों के अनुरूप। प्रकार 1 का इकाई शब्द इस प्रकार लिखा जाता है $()$ और 'शून्य' के रूप में मुखरित, अंतिम वस्तु है। समान सिद्धांत को इसी तरह विस्तारित किया जाता है, ताकि किसी के पास हो

$\pi _{1}(s\mathbin {:} \sigma ,t\mathbin {:} \tau )=s\mathbin {:} \sigma$

$\pi _{2}(s\mathbin {:} \sigma ,t\mathbin {:} \tau )=t\mathbin {:} \tau$

$(\pi _{1}(u\mathbin {:} \sigma \times \tau ),\pi _{2}(u\mathbin {:} \sigma \times \tau ))=u\mathbin {:} \sigma \times \tau$ :$t\mathbin {:} 1=()$

इस अंतिम को ऐसे पढ़ा जाता है जैसे कि t में टाइप 1 है, तो यह शून्य हो जाता है।

उपरोक्त प्रकारों को ऑब्जेक्ट (श्रेणी सिद्धांत) के रूप में ले कर एक श्रेणी में बदल दिया जा सकता है। रूपवाद $\sigma \to \tau$ जोड़े के समकक्ष वर्ग हैं $(x\mathbin {:} \sigma ,t\mathbin {:} \tau )$ जहाँ x एक चर है (प्रकार का $\sigma$) और टी एक शब्द है (प्रकार का $\tau$), इसमें (वैकल्पिक रूप से) x को छोड़कर कोई मुक्त चर नहीं है। हमेशा की तरह करीने और लगाने से क्लोजर प्राप्त होता है।

अधिक सटीक रूप से, कार्टेशियन बंद श्रेणियों की श्रेणी और सरल रूप से टाइप किए गए लैम्ब्डा सिद्धांतों की श्रेणी के बीच ऑपरेटर मौजूद हैं।

एक रेखीय प्रकार की प्रणाली का उपयोग करके इस मामले को बंद मोनोइडल श्रेणी में विस्तारित करना आम है। इसका कारण यह है कि CCC बंद सममित मोनोइडल श्रेणी का एक विशेष मामला है, जिसे आमतौर पर सेट की श्रेणी के रूप में लिया जाता है। समुच्चय सिद्धान्त की नींव रखने के लिए यह ठीक है, लेकिन अधिक सामान्य topos एक बेहतर नींव प्रदान करते हैं।

प्रमाण-सैद्धांतिक शब्दार्थ

सामान्य रूप से टाइप किया गया लैम्ब्डा कैलकुलस प्रपोजल अंतर्ज्ञानवादी तर्क के इम्प्लीकेशनल फ्रैगमेंट से निकटता से संबंधित है, यानी करी-हावर्ड आइसोमोर्फिज्म के माध्यम से न्यूनतम तर्क: शब्द प्राकृतिक कटौती में प्रमाणों के अनुरूप हैं, और आवास टाइप करें वास्तव में मिनिमम का टॉटोलॉजी (तर्क) है। तर्क।

वैकल्पिक सिंटैक्स

ऊपर दी गई प्रस्तुति केवल टाइप किए गए लैम्ब्डा कैलकुस के सिंटैक्स को परिभाषित करने का एकमात्र तरीका नहीं है। एक विकल्प यह है कि टाइप एनोटेशन को पूरी तरह से हटा दिया जाए (ताकि सिंटैक्स अनटाइप्ड लैम्ब्डा कैलकुलस के समान हो), यह सुनिश्चित करते हुए कि हिंडले-मिलनर प्रकार के अनुमान के माध्यम से शब्द अच्छी तरह से टाइप किए गए हैं। अनुमान एल्गोरिथम समाप्ति, ध्वनि और पूर्ण है: जब भी कोई शब्द टाइप करने योग्य होता है, एल्गोरिथम उसके प्रकार की गणना करता है। अधिक सटीक रूप से, यह शब्द के प्रमुख प्रकार की गणना करता है, क्योंकि अक्सर एक अघोषित शब्द (जैसे $\lambda x.~x$) के एक से अधिक प्रकार हो सकते हैं (${\mathtt {int}}\to {\mathtt {int}}$, ${\mathtt {bool}}\to {\mathtt {bool}}$, आदि, जो मुख्य प्रकार के सभी उदाहरण हैं $\alpha \to \alpha$).

सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस की एक अन्य वैकल्पिक प्रस्तुति द्विदिश प्रकार की जाँच पर आधारित है, जिसके लिए हिंडले-मिलनर अनुमान की तुलना में अधिक प्रकार के एनोटेशन की आवश्यकता होती है लेकिन वर्णन करना आसान है। प्रकार प्रणाली को दो निर्णयों में विभाजित किया गया है, जो लिखित 'जाँच' और 'संश्लेषण' दोनों का प्रतिनिधित्व करते हैं $\Gamma \vdash e\Leftarrow \tau$ और $\Gamma \vdash e\Rightarrow \tau$ क्रमश। परिचालन रूप से, तीन घटक $\Gamma$, $e$, और $\tau$ जाँच निर्णय के सभी इनपुट हैं $\Gamma \vdash e\Leftarrow \tau$, जबकि संश्लेषण निर्णय $\Gamma \vdash e\Rightarrow \tau$ ही लेता है $\Gamma$ और $e$ इनपुट के रूप में, प्रकार का उत्पादन $\tau$ आउटपुट के रूप में। ये निर्णय निम्नलिखित नियमों के माध्यम से प्राप्त किए गए हैं:

${\frac {x\mathbin {:} \sigma \in \Gamma }{\Gamma \vdash x\Rightarrow \sigma }}$ [1]	${\frac {c{\text{ is a constant of type }}T}{\Gamma \vdash c\Rightarrow T}}$ [2]
${\frac {\Gamma ,x\mathbin {:} \sigma \vdash e\Leftarrow \tau }{\Gamma \vdash \lambda x.~e\Leftarrow \sigma \to \tau }}$ [3]	${\frac {\Gamma \vdash e_{1}\Rightarrow \sigma \to \tau \quad \Gamma \vdash e_{2}\Leftarrow \sigma }{\Gamma \vdash e_{1}~e_{2}\Rightarrow \tau }}$ [4]
${\frac {\Gamma \vdash e\Rightarrow \tau }{\Gamma \vdash e\Leftarrow \tau }}$ [5]	${\frac {\Gamma \vdash e\Leftarrow \tau }{\Gamma \vdash (e\mathbin {:} \tau )\Rightarrow \tau }}$ [6]

निरीक्षण करें कि नियम [1]-[4] उपरोक्त नियमों (1)-(4) के लगभग समान हैं, जांच या संश्लेषण निर्णयों के सावधानीपूर्वक चयन को छोड़कर। इन विकल्पों को इस प्रकार समझाया जा सकता है:

1. अगर $x\mathbin {:} \sigma$ संदर्भ में है, हम प्रकार को संश्लेषित कर सकते हैं $\sigma$ के लिए $x$.
2. शब्द स्थिरांक के प्रकार निश्चित होते हैं और इन्हें संश्लेषित किया जा सकता है।
3. इसकी जांच के लिए $\lambda x.~e$ प्रकार है $\sigma \to \tau$ किसी संदर्भ में, हम संदर्भ का विस्तार करते हैं $x\mathbin {:} \sigma$ और इसे जांचें $e$ प्रकार है $\tau$.
4. अगर $e_{1}$ प्रकार संश्लेषित करता है $\sigma \to \tau$ (किसी संदर्भ में), और $e_{2}$ प्रकार के विरुद्ध जाँच करता है $\sigma$ (उसी संदर्भ में), तब $e_{1}~e_{2}$ प्रकार संश्लेषित करता है $\tau$.

ध्यान दें कि संश्लेषण के नियम ऊपर से नीचे तक पढ़े जाते हैं, जबकि जाँच के नियम नीचे से ऊपर तक पढ़े जाते हैं। विशेष रूप से ध्यान दें कि हमें नियम [3] में लैम्ब्डा अमूर्तता पर किसी एनोटेशन की आवश्यकता नहीं है, क्योंकि बाउंड वेरिएबल के प्रकार को उस प्रकार से घटाया जा सकता है जिस पर हम फ़ंक्शन की जांच करते हैं। अंत में, हम नियम [5] और [6] की व्याख्या इस प्रकार करते हैं: <ओल प्रारंभ = 5>

उसकी जांच करने के लिए $e$ प्रकार है $\tau$, यह प्रकार को संश्लेषित करने के लिए पर्याप्त है $\tau$।</ली>

अगर $e$ प्रकार के विरुद्ध जाँच करता है $\tau$, फिर स्पष्ट रूप से एनोटेट किया गया शब्द $(e\mathbin {:} \tau )$ संश्लेषित $\tau$. </ली> </ओल> इन अंतिम दो नियमों के कारण संश्लेषण और जाँच के बीच ज़बरदस्ती, यह देखना आसान है कि किसी भी अच्छी तरह से टाइप किए गए लेकिन बिना टिप्पणी वाले शब्द को द्विदिश प्रणाली में जाँचा जा सकता है, जब तक हम पर्याप्त प्रकार के एनोटेशन सम्मिलित करते हैं। और वास्तव में, एनोटेशन की आवश्यकता केवल β-redexes पर होती है।

सामान्य अवलोकन

मानक शब्दार्थ को देखते हुए, सामान्य रूप से टाइप किया गया लैम्ब्डा कैलकुलस नॉर्मलाइज़ेशन प्रॉपर्टी (लैम्ब्डा-कैलकुलस) है: यानी, अच्छी तरह से टाइप किए गए शब्द हमेशा एक मान को कम करते हैं, यानी, ए $\lambda$ अमूर्त। ऐसा इसलिए है क्योंकि टाइपिंग नियमों द्वारा रिकर्सन की अनुमति नहीं है: फिक्स्ड-पॉइंट कॉम्बिनेटर और लूपिंग टर्म के लिए प्रकार खोजना असंभव है $\Omega =(\lambda x.~x~x)(\lambda x.~x~x)$. रिकर्सन को या तो एक विशेष ऑपरेटर के द्वारा भाषा में जोड़ा जा सकता है ${\mathtt {fix}}_{\alpha }$प्रकार का $(\alpha \to \alpha )\to \alpha$ या सामान्य पुनरावर्ती प्रकार जोड़ना, हालांकि दोनों मजबूत सामान्यीकरण को समाप्त करते हैं।

चूंकि यह दृढ़ता से सामान्यीकरण कर रहा है, यह निर्णायकता (तर्क) है कि क्या केवल टाइप किया गया लैम्ब्डा कैलकुलस प्रोग्राम रुकता है या नहीं: वास्तव में, यह हमेशा रुकता है। इसलिए हम यह निष्कर्ष निकाल सकते हैं कि भाषा ट्यूरिंग पूर्ण नहीं है।

महत्वपूर्ण परिणाम

• टैट ने 1967 में दिखाया कि $\beta$-रिडक्शन नॉर्मलाइज़ेशन प्रॉपर्टी (लैम्ब्डा-कैलकुलस) है।एक परिणाम के रूप में $\beta \eta$-समानता निर्णायकता (तर्क) है। स्टेटमैन ने 1979 में दिखाया कि सामान्यीकरण समस्या प्राथमिक पुनरावर्ती नहीं है,एक प्रमाण जिसे बाद में मैरसन ने सरल बनाया।समस्या सेट में होने के लिए जानी जाती है ${\mathcal {E}}^{4}$ ग्रेज़गोर्स्की पदानुक्रम का। 1991 में बर्जर और श्विटेनबर्ग द्वारा एक विशुद्ध रूप से सिमेंटिक सामान्यीकरण प्रमाण (मूल्यांकन द्वारा सामान्यीकरण देखें) दिया गया था।* एकीकरण (कंप्यूटिंग) समस्या के लिए $\beta \eta$-तुल्यता अनिर्णीत है। ह्यूएट ने 1973 में दिखाया कि तीसरे क्रम का एकीकरण अनिर्णीत हैऔर 1978 में बैक्सटर द्वारा इसमें सुधार किया गयाफिर 1981 में गोल्डफार्ब द्वारायह दिखाते हुए कि दूसरा क्रम एकीकरण पहले से ही अनिर्णीत है। 2006 में कॉलिन स्टर्लिंग द्वारा एक प्रमाण की घोषणा की गई थी कि उच्च क्रम मिलान (एकीकरण जहां केवल एक शब्द में अस्तित्वगत चर शामिल हैं) निर्णायक है, और 2009 में एक पूर्ण प्रमाण प्रकाशित किया गया था।
• हम प्रकार के संदर्भ में प्राकृतिक संख्याओं को सांकेतिक शब्दों में बदल सकते हैं $(o\to o)\to (o\to o)$ (चर्च अंक)। श्विटेनबर्ग ने 1975 में दिखाया कि में $\lambda ^{\to }$ बिल्कुल विस्तारित बहुपद चर्च अंकों पर कार्यों के रूप में प्रतिनिधित्व योग्य हैं;ये मोटे तौर पर सशर्त संकारक के अंतर्गत बंद किए गए बहुपद हैं।
• का एक पूर्ण मॉडल $\lambda ^{\to }$ सेट-सैद्धांतिक समारोह स्थान द्वारा सेट (गणित) और फ़ंक्शन प्रकारों के रूप में आधार प्रकारों की व्याख्या करके दिया जाता है। फ्रीडमैन ने 1975 में दिखाया कि यह व्याख्या पूर्णता (तर्क) के लिए है $\beta \eta$-समानता, यदि आधार प्रकार की व्याख्या अनंत सेटों द्वारा की जाती है।स्टेटमैन ने 1983 में दिखाया था कि $\beta \eta$-समतुल्यता अधिकतम तुल्यता है जो आम तौर पर अस्पष्ट है, यानी प्रकार प्रतिस्थापन (स्टेटमैन की विशिष्ट अस्पष्टता प्रमेय) के तहत बंद है।इसका एक परिणाम यह है कि परिमित मॉडल संपत्ति धारण करती है, अर्थात परिमित सेट उन शब्दों को अलग करने के लिए पर्याप्त हैं जिन्हें इसके द्वारा पहचाना नहीं जाता है $\beta \eta$-तुल्यता।
• प्लॉटकिन ने 1973 में एक मॉडल के तत्वों की विशेषता के लिए तार्किक संबंधों की शुरुआत की, जो लैम्ब्डा शर्तों द्वारा परिभाषित हैं।1993 में जंग और ट्यूरिन ने दिखाया कि तार्किक संबंध का एक सामान्य रूप (क्रिपके तार्किक संबंध अलग-अलग एरिटी के साथ) वास्तव में लैम्ब्डा निश्चितता की विशेषता है।प्लॉटकिन और स्टेटमैन ने अनुमान लगाया कि यह निश्चित है कि परिमित सेट से उत्पन्न मॉडल का दिया गया तत्व लैम्ब्डा शब्द (प्लॉटकिन-स्टेटमैन अनुमान) द्वारा निश्चित है या नहीं। 2001 में लोडर द्वारा अनुमान को झूठा दिखाया गया था।

टिप्पणियाँ

संदर्भ

• H. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1993. ISBN 0-19-853761-1.

बाहरी संबंध

• Loader, Ralph (February 1998). "Notes on Simply Typed Lambda Calculus".
• "Church's Type Theory" entry in the Stanford Encyclopedia of Philosophy