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

साधारणतः टाइप किया हुआ लैम्ब्डा कैलकुस ($\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$ संदर्भ में $\Gamma$ $\sigma$ टाइप का शब्द है। इस स्थिति में $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$-समानता) कार्तीय बंद श्रेणियों (सीसीसी) की आंतरिक भाषा है। जैसा कि पहली बार जोआचिम लैम्बेक द्वारा देखा गया था। किसी भी विशिष्ट सीसीसी को देखते हुए, संबंधित लैम्ब्डा कैलकुस के मूल टाइप केवल वस्तु (श्रेणी सिद्धांत) हैं, और नियम रूपवाद हैं। इसके विपरीत, प्रत्येक सामान्य रूप से टाइप किया गया लैम्ब्डा कैलकुलस सीसीसी देता है। जिसकी वस्तुएँ टाइप होती हैं, और रूपवाद शब्दों के तुल्यता वर्ग होते हैं।

पत्राचार को श्रेणीबद्ध करने के लिए, कार्टेशियन उत्पाद के लिए एक टाइप का निर्माता सामान्यतः ऊपर जोड़ा जाता है। उत्पाद (श्रेणी सिद्धांत) को संरक्षित करने के लिए, युग्मन, प्रक्षेपण और इकाई शब्द के लिए टाइपिंग नियम जोड़े जाते हैं। दो नियम $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$) और t शब्द है (टाइप का $\tau$), इसमें (वैकल्पिक रूप से) x को छोड़कर कोई मुक्त चर नहीं है। सदैव की तरह करीने और लगाने से क्लोजर प्राप्त होता है।

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

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

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

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

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

ऊपर दी गई प्रस्तुति केवल टाइप किए गए लैम्ब्डा कैलकुस के सिंटैक्स को परिभाषित करने का एकमात्र विधि नहीं है। विकल्प यह है कि टाइप एनोटेशन को पूरी तरह से हटा दिया जाए (जिससे सिंटैक्स अनटाइप्ड लैम्ब्डा कैलकुलस के समान हो), यह सुनिश्चित करते हुए कि हिंडले-मिलनर टाइप के अनुमान के माध्यम से शब्द अच्छी तरह से टाइप किए गए हैं। अनुमान एल्गोरिथम समाप्ति, ध्वनि और पूर्ण है। जब भी कोई शब्द टाइप करने योग्य होता है, एल्गोरिथम उसके टाइप की गणना करता है। अधिक श्रेणीबद्ध रूप से, यह शब्द के प्रमुख टाइप की गणना करता है। क्योंकि अधिकांशतः अघोषित शब्द (जैसे $\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] की व्याख्या इस टाइप करते हैं |

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

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

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

मानक शब्दार्थ को देखते हुए, सामान्य रूप से टाइप किया गया लैम्ब्डा कैलकुलस नॉर्मलाइज़ेशन प्रॉपर्टी (लैम्ब्डा-कैलकुलस) है: अर्थात, अच्छी तरह से टाइप किए गए शब्द सदैव एक मान को कम करते हैं अर्थात, ए $\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