हिंडले-मिलनर टाइप सिस्टम: Difference between revisions

	Expressions
	Types
	Context and Typing
	Free Type Variables

Revision as of 15:41, 18 July 2023

हिंडले-मिलनर (एचएम) टाइप प्रणाली प्राचलिक बहुरूपता के साथ लैम्ब्डा कलन के लिए चिरसम्मत टाइप की प्रणाली है। इसे दमास-मिलनर या दमास-हिंडले-मिलनर के नाम से भी जाना जाता है। इसका वर्णन सबसे पहले जे। रोजर हिंडले ने किया था^[1] और बाद में रॉबिन मिलनर द्वारा पुनः खोजा गया था।^[2] लुइस दामास ने अपनी पीएचडी थीसिस में विधि का सीमित औपचारिक विश्लेषण और प्रमाण दिया था।^[3]^[4]

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

परिचय

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

मूल सरल रूप से टाइप लैम्ब्डा कलन के लिए टाइप इन्फेरेंस कलन विधि है जिसे 1958 में हास्केल करी और रॉबर्ट फेयस द्वारा तैयार किया गया था। 1969 में, जे। रोजर हिंडले ने इस काम को आगे बढ़ाया और साबित किया कि उनका कलन विधि हमेशा सबसे सामान्य टाइप इन्फेरेंस लगाता है। 1978 में, रॉबिन मिलनर,^[5] हिंडले के काम से स्वतंत्र, समतुल्य कलन विधि डब्ल्यू प्रदान किया गया। 1982 में, लुई दामास^[4]अंततः साबित हुआ कि मिलनर का कलन विधि पूर्ण है और इसे बहुरूपी संदर्भों वाले प्रणाली का समर्थन करने के लिए विस्तारित किया गया है।

एकरूपता बनाम बहुरूपता

सरलता से टाइप किए गए लैम्ब्डा कलन में, टाइप $T$ या तो परमाणु टाइप के स्थिरांक हैं या फंक्शन टाइप के रूप हैं $T\rightarrow T$ , ऐसे टाइप एकरूप होते हैं। विशिष्ट उदाहरण अंकगणितीय मानों में प्रयुक्त टाइप हैं:

 3       : Number
 add 3 4 : Number
 add     : Number -> Number -> Number

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

id ≡ λ x ।x

जो जिस भी मान पर लागू होता है, उसे वापस लौटा देता है। अल्प तुच्छ उदाहरणों में सूची (कंप्यूटर विज्ञान) जैसे प्राचलिक टाइप शामिल हैं।

जबकि सामान्य तौर पर बहुरूपता का अर्थ है कि ऑपरेशन एक से अधिक टाइप के मानnको स्वीकार करते हैं, यहां प्रयुक्त बहुरूपता प्राचलिक है। साहित्य में टाइप की योजनाओं का उल्लेख भी मिलता है, जो बहुरूपता की प्राचलिक प्रकृति पर जोर देता है। इसके अतिरिक्त, स्थिरांक को (मात्राबद्ध) टाइप के चर के साथ टाइप किया जा सकता है। जैसे:

 cons : forall a । a -> List a -> List a
 nil  : forall a । List a
 id   : forall a । a -> a

बहुरूपी टाइप अपने चरों के लगातार प्रतिस्थापन से एकरूप बन सकते हैं। एकरूप उदाहरणों के उदाहरण हैं:

id'  : String -> String
nil' : List Number

अधिक आम तौर पर, टाइप बहुरूपी होते हैं जब उनमें टाइप चर होते हैं, जबकि उनके बिना टाइप एकरूप होते हैं।

उदाहरण के लिए पास्कल (प्रोग्रामिंग लैंग्वेज) (1970) या सी (प्रोग्रामिंग लैंग्वेज) (1972) में प्रयुक्त टाइप प्रणालियों के विपरीत, जो केवल एकरूप टाइप का समर्थन करते हैं, एचएम को प्राचलिक बहुरूपता पर जोर देने के साथ डिजाइन किया गया है। उल्लिखित लैंग्वेज के उत्तराधिकारी, जैसे C++ (1985), विभिन्न टाइप के बहुरूपता पर ध्यान केंद्रित करते हैं, अर्थात् बहुरूपता (कंप्यूटर विज्ञान) ऑब्जेक्ट ओरिएंटेड प्रोग्रामिंग और ओवरलोडिंग के संबंध में उपटाइपिंग हैं। जबकि उपटाइपिंग एचएम के साथ असंगत है, हास्केल के एचएम-आधारित टाइप प्रणाली में व्यवस्थित ओवरलोडिंग का एक टाइप उपलब्ध है।

लेट-पॉलीमोर्फिज्म

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

  (λ id ।  ।।। (id 3) ।।। (id "text") ।।। ) (λ x । x)

दुर्भाग्य से, बहुरूपी लैम्ब्डा कैलकुलस में टाइप इन्फेरेंस निर्णय योग्य नहीं है।^[6] इसके बजाय, एचएम फॉर्म का लेट-पॉलीमोर्फिज्म प्रदान करता है

 let id = λ x । x
  in ।।। (id 3) ।।। (id "text") ।।।

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

सिंहावलोकन

इस लेख का शेष भाग इस टाइप है:

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

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

हिंडले-मिलनर टाइप प्रणाली

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

सिंटेक्स

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

टाइप को वाक्यात्मक रूप से दो समूहों, मोनोटाइप्स और पॉलीटाइप्स में विभाजित किया गया है।^{[note 2]}

मोनोटाइप्स

मोनोटाइप हमेशा एक विशेष टाइप को निर्दिष्ट करते हैं। मोनोटाइप्स $\tau$ वाक्यात्मक रूप से टर्म (तर्क) के रूप में दर्शाया जाता है।

मोनोटाइप के उदाहरणों में टाइप स्थिरांक शामिल हैं ${\mathtt {int}}$ या ${\mathtt {string}}$ , और प्राचलिक टाइप जैसे ${\mathtt {Map\ (Set\ string)\ int}}$ । बाद वाले टाइप टाइप के फंक्शन के अनुप्रयोगों के उदाहरण हैं, उदाहरण के लिए, सेट से $\{{\mathtt {Map^{2},\ Set^{1},\ string^{0},\ int^{0}}},\ \rightarrow ^{2}\}$ , जहां सुपरस्क्रिप्ट टाइप के मापदंडों की संख्या को इंगित करता है। टाइप के फंक्शन का पूरा सेट $C$ एचएम में यादृच्छिक है,^{[note 3]} सिवाय इसके कि इसमें न्यूनतम $\rightarrow ^{2}$ , फंक्शन का टाइप शामिल होना चाहिए। सुविधा के लिए इसे अक्सर मध्यप्रत्यय संकेतन में लिखा जाता है। उदाहरण के लिए, पूर्णांकों को स्ट्रिंग्स से मैप करने वाले फ़ंक्शन का टाइप ${\mathtt {int}}\rightarrow {\mathtt {string}}$ होता है, फिर से, कोष्ठक का उपयोग किसी टाइप की अभिव्यक्ति को स्पष्ट करने के लिए किया जा सकता है। अनुप्रयोग मध्यप्रत्यय एरो की तुलना में अधिक मजबूती से सीमित होता है, जो राइट-सीमित है।

टाइप चर को मोनोटाइप के रूप में स्वीकार किया जाता है। मोनोटाइप्स को एकरूप टाइप के साथ भ्रमित नहीं किया जाना चाहिए, जो चर को छोड़कर केवल जमीनी शब्दों की अनुमति देते हैं।

दो मोनोटाइप समान हैं यदि उनके अभिव्यक्ति समान हैं।

पॉलीटाइप्स (बहुप्रकार)

पॉलीटाइप्स (या टाइप स्कीम) वे टाइप हैं जिनमें सभी परिमाणकों के लिए शून्य या अधिक से सीमित चर होते हैं, उदाहरण के लिए $\forall \alpha .\alpha \rightarrow \alpha$ ।

पॉलीटाइप वाला फ़ंक्शन $\forall \alpha .\alpha \rightarrow \alpha$ एक ही टाइप के किसी भी मान को स्वयं में मैप कर सकता है, और तत्समक फ़ंक्शन इस टाइप के लिए मान है।

एक अन्य उदाहरण के रूप में, $\forall \alpha .({\mathtt {Set}}\ \alpha )\rightarrow {\mathtt {int}}$ फ़ंक्शन का टाइप है जो सभी परिमित सेटों को पूर्णांकों में मैप करता है। फ़ंक्शन जो किसी सेट की प्रमुखता लौटाता है वह इस टाइप का मान होगा।

परिमाण केवल शीर्ष स्तर के दिखाई दे सकते हैं। उदाहरण के लिए, टाइप $\forall \alpha .\alpha \rightarrow \forall \alpha .\alpha$ टाइप के सिंटैक्स द्वारा बाहर रखा गया है। इसके अलावा पॉलीटाइप्स में मोनोटाइप भी शामिल होते हैं, एक टाइप का सामान्य रूप होता है $\forall \alpha _{1}\dots \forall \alpha _{n}.\tau ,n\geq 0$ , जहाँ $\tau$ मोनोटाइप है।

पॉलीटाइप्स की समानता परिमाणीकरण को पुन: व्यवस्थित करने और परिमाणित चरों ( $\alpha$ -रूपांतरण) का नाम बदलने तक है इसके अलावा, मोनोटाइप में नहीं आने वाले परिमाणित चर को हटाया जा सकता है।

प्रसंग और टाइपिंग

अभी भी असंबद्ध भागों (सिंटेक्स अभिव्यक्ति और टाइप) को सार्थक रूप से एक साथ लाने के लिए तीसरे भाग की आवश्यकता है: संदर्भ वाक्यात्मक रूप से, संदर्भ युग्म की सूची है $x:\sigma$ , जिसे असाइनमेंट (गणितीय तर्क), धारणा या सीमित कहा जाता है, प्रत्येक युग्म उस मान चर $x_{i}$ को बताती है टाइप है $\sigma _{i}.$ तीनों भाग मिलकर फॉर्म का टाइपिंग निर्णय देते हैं $\Gamma \ \vdash \ e:\sigma$ , यह बताते हुए कि धारणाओं के तहत $\Gamma$ , अभिव्यक्ति $e$ , $\sigma$ टाइप है।

मुक्त टाइप के चर

टाइप में $\forall \alpha _{1}\dots \forall \alpha _{n}.\tau$ , मोनोटाइप में $\tau$ प्रतीक $\forall$ टाइप चर $\alpha _{i}$ सीमित वाला परिमाण है। चर $\alpha _{i}$ परिमाणित कहलाते हैं और परिमाणित टाइप के चर $\tau$ की कोई भी घटना को सीमित कहा जाता है और सभी अनबाउंड टाइप के चर $\tau$ मुक्त कहलाते हैं। परिमाणीकरण के अतिरिक्त $\forall$ पॉलीटाइप्स में, टाइप चर को संदर्भ में घटित होने से भी बाध्य किया जा सकता है, लेकिन दाईं ओर विपरीत प्रभाव के साथ $\vdash$ किया जा सकता है। ऐसे चर तब वहां टाइप स्थिरांक की तरह व्यवहार करते हैं। अंत में, एक टाइप का चर वैध रूप से टाइपिंग में अनबाउंड हो सकता है, जिस स्थिति में वे अंतर्निहित रूप से सभी-मात्राबद्ध होते हैं।

प्रोग्रामिंग लैंग्वेज में सीमित और अनबाउंड दोनों टाइप के चर की उपस्थिति थोड़ी असामान्य है। अक्सर, सभी टाइप के चरों को अंतर्निहित रूप से सर्व-मात्राबद्ध माना जाता है। उदाहरण के लिए, प्रोलॉग में मुक्त चर वाले खंड नहीं हैं। इसी तरह हास्केल में, ^{[note 4]} जहां सभी टाइप के चर अंतर्निहित रूप से मात्राबद्ध होते हैं, यानी हास्केल टाइप a -> a यहाँ $\forall \alpha .\alpha \rightarrow \alpha$ हैं। दाहिने हाथ की ओर $\sigma$ असाइनमेंट का बंधनकारी प्रभाव संबंधित और बहुत ही असामान्य भी है।

आमतौर पर, बाध्य और अनबाउंड दोनों टाइप के चर का मिश्रण एक अभिव्यक्ति में मुक्त चर के उपयोग से उत्पन्न होता है। स्थिरांक फंक्शन K = $\lambda x.\lambda y.x$ उदाहरण प्रदान करता है, इसका मोनोटाइप $\alpha \rightarrow \beta \rightarrow \alpha$ है कोई व्यक्ति बहुरूपता को बलपूर्वक लागू कर सकता है $\mathbf {let} \ k=\lambda x.(\mathbf {let} \ f=\lambda y.x\ \mathbf {in} \ f)\ \mathbf {in} \ k$ , यहाँ, $f$ , $\forall \gamma .\gamma \rightarrow \alpha$ टाइप है मुक्त मोनोटाइप चर $\alpha$ चर $x$ के टाइप से उत्पन्न होता है आसपास के दायरे में बंधा हुआ $k$ $\forall \alpha \forall \beta .\alpha \rightarrow \beta \rightarrow \alpha$ टाइप है, कोई मुक्त टाइप चर $\alpha$ , $f$ से सीमित रहें $\forall \alpha$ के टाइप में $k$ की कल्पना कर सकत है। लेकिन ऐसी गुंजाइश एचएम में व्यक्त नहीं की जा सकती। बल्कि संदर्भ से सीमित का एहसास होता है।

टाइप ऑर्डर

बहुरूपता का अर्थ है कि एक ही अभिव्यक्ति के (संभवतः अनंत रूप से) कई टाइप हो सकते हैं। लेकिन इस टाइप की प्रणाली में, ये टाइप पूरी तरह से असंबंधित नहीं हैं, बल्कि प्राचलिक बहुरूपता द्वारा व्यवस्थित हैं।

उदाहरण के तौर पर, तत्समक $\lambda x.x$ , $\forall \alpha .\alpha \rightarrow \alpha$ इसके टाइप के रूप में भी ${\texttt {string}}\rightarrow {\texttt {string}}$ या ${\texttt {int}}\rightarrow {\texttt {int}}$ और कई अन्य हो सकता है, लेकिन नहीं ${\texttt {int}}\rightarrow {\texttt {string}}$ हो सकता है, इस फ़ंक्शन के लिए सबसे सामान्य टाइप है $\forall \alpha .\alpha \rightarrow \alpha$ , जब अन्य अधिक विशिष्ट हैं और उन्हें सामान्य से लगातार प्राप्त किया जा सकता है टाइप मापदण्ड के लिए किसी अन्य टाइप को प्रतिस्थापित करना, यानी परिमाणितचर $\alpha$ है। प्रति-उदाहरण विफल हो जाता है क्योंकि प्रतिस्थापन सुसंगत नहीं है।

एकीकरण (कंप्यूटर विज्ञान) प्रतिस्थापन लागू करके लगातार प्रतिस्थापन $S=\left\{\ a_{i}\mapsto \tau _{i},\ \dots \ \right\}$ को औपचारिक बनाया जा सकता है, टाइप की अवधि के लिए $\tau$ , $S\tau$ लिखा हुआ। जैसा कि उदाहरण से पता चलता है, प्रतिस्थापन न केवल ऑर्डर से दृढ़ता से संबंधित है, जो व्यक्त करता है कि टाइप अल्प या ज्यादा विशेष है, बल्कि सभी-परिमाणीकरण के साथ भी है जो प्रतिस्थापन को लागू करने की अनुमति देता है।

औपचारिक रूप से, एचएम में, टाइप $\sigma '$ , $\sigma$ से अधिक सामान्य है, औपचारिक रूप से $\sigma '\sqsubseteq \sigma$ , यदि कुछ परिमाणित चर में $\sigma '$ लगातार इस टाइप प्रतिस्थापित किया जाता है कि लाभ $\sigma$ हो जैसा कि साइड बार में दिखाया गया है। यह ऑर्डर टाइप प्रणाली की टाइप परिभाषा का हिस्सा है।

हमारे पिछले उदाहरण में, प्रतिस्थापन $S=\left\{\alpha \mapsto {\texttt {string}}\right\}$ लागू करना $\forall \alpha .\alpha \rightarrow \alpha \sqsubseteq {\texttt {string}}\rightarrow {\texttt {string}}$ परिणाम होगा।

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

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

संबंध $\sqsubseteq$ आंशिक ऑर्डर है और $\forall \alpha .\alpha$ इसका सबसे छोटा तत्व है।

मूल टाइप

जबकि टाइप की योजना का विशेषज्ञता ऑर्डर का उपयोग है, यह टाइप प्रणाली में महत्वपूर्ण दूसरी भूमिका निभाता है। बहुरूपता के साथ टाइप इन्फेरेंस अभिव्यक्ति के सभी संभावित प्रकारों को सारांशित करने की चुनौती का सामना करता है। ऑर्डर गारंटी देता है कि ऐसा सारांश अभिव्यक्ति के सबसे सामान्य टाइप के रूप में मौजूद है।

टाइपिंग में प्रतिस्थापन

ऊपर परिभाषित टाइप ऑर्डर को टाइपिंग तक बढ़ाया जा सकता है क्योंकि टाइपिंग की अंतर्निहित सभी-मात्रा लगातार प्रतिस्थापन को सक्षम बनाती है:

\Gamma \vdash e:\sigma \quad \Longrightarrow \quad S\Gamma \vdash e:S\sigma

विशेषज्ञता नियम के विपरीत, यह परिभाषा का हिस्सा नहीं है, बल्कि अंतर्निहित सभी-परिमाणीकरण की तरह है, बल्कि आगे परिभाषित टाइप के नियमों का परिणाम है। टाइपिंग में मुक्त टाइप चर संभावित शोधन के लिए प्लेसहोल्डर के रूप में काम करते हैं। दाहिनी ओर मुक्त टाइप के चर के लिए पर्यावरण का बाध्यकारी प्रभाव $\vdash$ जो विशेषज्ञता नियम में उनके प्रतिस्थापन को फिर से प्रतिबंधित करता है, वह फिर से यह है कि प्रतिस्थापन को सुसंगत होना चाहिए और इसमें संपूर्ण टाइपिंग को शामिल करने की आवश्यकता होगी।

यह आलेख चार अलग-अलग नियम सेटों पर चर्चा करेगा:

$\vdash _{D}$ घोषणात्मक प्रणाली
$\vdash _{S}$ वाक्यात्मक प्रणाली
$\vdash _{J}$ कलन विधि J
$\vdash _{W}$ कलन विधि W

निगमनात्मक प्रणाली

निर्णयों (गणितीय तर्क) के रूप में टाइपिंग का उपयोग करके, एचएम के सिंटैक्स को अनुमान नियमों के सिंटैक्स तक आगे बढ़ाया जाता है जो औपचारिक प्रणाली का मुख्य भाग बनाता है। प्रत्येक नियम परिभाषित करता है कि किस आधार से क्या निष्कर्ष निकाला जा सकता है। निर्णयों के अतिरिक्त, ऊपर प्रस्तुत कुछ अतिरिक्त शर्तों को भी परिसर के रूप में उपयोग किया जा सकता है।

नियमों का उपयोग करने वाला प्रमाण निर्णयों का ऑर्डर है जैसे कि निष्कर्ष से पहले सभी परिसरों को सूचीबद्ध किया जाता है। नीचे दिए गए उदाहरण प्रमाणों का संभावित प्रारूप दिखाते हैं। बाएँ से दाएँ, प्रत्येक पंक्ति निष्कर्ष दर्शाती है $[{\mathtt {Name}}]$ या विधेय को स्पष्ट करके, या तो पहले की पंक्ति (संख्या) का संदर्भ देकर लागू नियम और परिसर का, यदि आधार निर्णय है।

टाइपिंग नियम

Declarative Rule System
${\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma }{\Gamma \vdash _{D}x:\sigma }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e_{0}:\tau \rightarrow \tau '\quad \quad \Gamma \vdash _{D}e_{1}:\tau }{\Gamma \vdash _{D}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\Gamma ,\;x:\tau \vdash _{D}e:\tau '}{\Gamma \vdash _{D}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e_{0}:\sigma \quad \quad \Gamma ,\,x:\sigma \vdash _{D}e_{1}:\tau }{\Gamma \vdash _{D}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau }}&[{\mathtt {Let}}]\\\\\\\displaystyle {\frac {\Gamma \vdash _{D}e:\sigma '\quad \sigma '\sqsubseteq \sigma }{\Gamma \vdash _{D}e:\sigma }}&[{\mathtt {Inst}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e:\sigma \quad \alpha \notin {\text{free}}(\Gamma )}{\Gamma \vdash _{D}e:\forall \ \alpha \ .\ \sigma }}&[{\mathtt {Gen}}]\\\\\end{array}}$

साइड बॉक्स एचएम टाइप प्रणाली के निगमन नियमों को दर्शाता है। नियमों को मोटे तौर पर दो समूहों में विभाजित किया जा सकता है:

पहले चार नियम $[{\mathtt {Var}}]$ (चर या फ़ंक्शन एक्सेस), $[{\mathtt {App}}]$ (अनुप्रयोग, यानी मापदण्ड के साथ फ़ंक्शन कॉल), $[{\mathtt {Abs}}]$ (अमूर्त, यानी फ़ंक्शन घोषणा) और $[{\mathtt {Let}}]$ (परिवर्तनीय घोषणा) सिंटेक्स पर केंद्रित हैं, प्रत्येक अभिव्यक्ति रूप के लिए नियम प्रस्तुत करते हैं। उनका अर्थ पहली नज़र में स्पष्ट है, क्योंकि वे प्रत्येक अभिव्यक्ति को विघटित करते हैं, उनकी उप-अभिव्यक्तियों को सिद्ध करते हैं और अंततः परिसर में पाए जाने वाले व्यक्तिगत टाइप को निष्कर्ष में दिए गए टाइप से जोड़ते हैं।

शेष दो नियमों $[{\mathtt {Inst}}]$ और $[{\mathtt {Gen}}]$ से दूसरा समूह बनता है। वे टाइप की विशेषज्ञता और सामान्यीकरण को संभालते हैं। जबकि नियम $[{\mathtt {Inst}}]$ उपरोक्त विशेषज्ञता वाले अनुभाग से स्पष्ट होना चाहिए, $[{\mathtt {Gen}}]$ विपरीत दिशा में काम करते हुए पहले का पूरक है। यह सामान्यीकरण की अनुमति देता है, यानी संदर्भ में सीमित हुए मोनोटाइप चर की मात्रा निर्धारित करने की अनुमति नहीं देता है।

निम्नलिखित दो उदाहरण क्रियान्वित नियम प्रणाली का प्रयोग करते हैं। चूँकि अभिव्यक्ति और टाइप दोनों दिए गए हैं, वे नियमों का टाइप-जाँच उपयोग हैं।

उदाहरण: के लिए प्रमाण $\Gamma \vdash _{D}id(n):int$ जहाँ $\Gamma =id:\forall \alpha .\alpha \rightarrow \alpha ,\ n:int$ ,लिखा जा सकता है

{\begin{array}{llll}1:&\Gamma \vdash _{D}id:\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Var}}]&(id:\forall \alpha .\alpha \rightarrow \alpha \in \Gamma )\\2:&\Gamma \vdash _{D}id:int\rightarrow int&[{\mathtt {Inst}}]&(1),\ (\forall \alpha .\alpha \rightarrow \alpha \sqsubseteq int\rightarrow int)\\3:&\Gamma \vdash _{D}n:int&[{\mathtt {Var}}]&(n:int\in \Gamma )\\4:&\Gamma \vdash _{D}id(n):int&[{\mathtt {App}}]&(2),\ (3)\\\end{array}}

उदाहरण: सामान्यीकरण प्रदर्शित करने के लिए, $\vdash _{D}\ {\textbf {let}}\,id=\lambda x.x\ {\textbf {in}}\ id\,:\,\forall \alpha .\alpha \rightarrow \alpha$ नीचे दिखाया गया है:

{\begin{array}{llll}1:&x:\alpha \vdash _{D}x:\alpha &[{\mathtt {Var}}]&(x:\alpha \in \left\{x:\alpha \right\})\\2:&\vdash _{D}\lambda x.x:\alpha \rightarrow \alpha &[{\mathtt {Abs}}]&(1)\\3:&\vdash _{D}\lambda x.x:\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Gen}}]&(2),\ (\alpha \not \in free(\epsilon ))\\4:&id:\forall \alpha .\alpha \rightarrow \alpha \vdash _{D}id:\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Var}}]&(id:\forall \alpha .\alpha \rightarrow \alpha \in \left\{id:\forall \alpha .\alpha \rightarrow \alpha \right\})\\5:&\vdash _{D}{\textbf {let}}\,id=\lambda x.x\ {\textbf {in}}\ id\,:\,\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Let}}]&(3),\ (4)\\\end{array}}

लेट-बहुरूपता

तुरंत दिखाई नहीं देता है, नियम सेट विनियमन को एन्कोड करता है जिसके तहत नियमों $[{\mathtt {Abs}}]$ और $[{\mathtt {Let}}]$ में मोनो- और पॉलीटाइप के थोड़े अलग उपयोग से किसी टाइप को सामान्यीकृत किया जा सकता है या नहीं किया जा सकता है। उसे याद रखो $\sigma$ और $\tau$ क्रमशः पॉली- और मोनोटाइप्स को निरूपित करें।

नियम में $[{\mathtt {Abs}}]$ , फ़ंक्शन के मापदण्ड का मान चर $\lambda x.e$ आधार के माध्यम से एकरूप टाइप के साथ संदर्भ में जोड़ा जाता है $\Gamma ,\ x:\tau \vdash _{D}e:\tau '$ , जबकि नियम $[{\mathtt {Let}}]$ में है चर पर्यावरण में बहुरूपी रूप $\Gamma ,\ x:\sigma \vdash _{D}e_{1}:\tau$ में प्रवेश करता है। हालाँकि दोनों ही मामलों में की उपस्थिति $x$ संदर्भ में असाइनमेंट में किसी भी मुक्त चर के लिए सामान्यीकरण नियम के उपयोग को रोकता है, यह विनियमन मापदण्ड $x$ के टाइप को बाध्य करता है $\lambda$ -अभिव्यक्ति एकरूप बनी रहेगी, जबकि लेट-एक्सप्रेशन में, चर को बहुरूपी पेश किया जा सकता है, जिससे विशेषज्ञता संभव हो सकेगी।

इस विनियमन के परिणामस्वरूप, $\lambda f.(f\,{\textrm {true}},f\,{\textrm {0}})$ टाइप नहीं किया जा सकता, मापदण्ड के बाद से $f$ एकरूप स्थिति में है, जबकि ${\textbf {let}}\ f=\lambda x.x\,{\textbf {in}}\,(f\,{\textrm {true}},f\,{\textrm {0}})$ टाइप $(bool,int)$ है, क्योंकि $f$ लेट-एक्सप्रेशन में पेश किया गया है और इसलिए इसे बहुरूपी माना जाता है।

सामान्यीकरण नियम

सामान्यीकरण नियम भी करीब से देखने लायक है। यहां, आधार $\Gamma \vdash e:\sigma$ में निहित सभी-परिमाणीकरण को निष्कर्ष में $\vdash _{D}$ के दाहिनी ओर ले जाया गया है। यह तब से संभव है $\alpha$ संदर्भ में मुक्त नहीं होता है। फिर, जबकि यह सामान्यीकरण नियम को प्रशंसनीय बनाता है, यह वास्तव में कोई परिणाम नहीं है। इसके विपरीत, सामान्यीकरण नियम एचएम की टाइप प्रणाली की परिभाषा का हिस्सा है और अंतर्निहित सभी-परिमाणीकरण एक परिणाम है।

अनुमान कलन विधि

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

नियमों को चुनने की स्वतंत्रता की डिग्री

प्रमाण में उन बिंदुओं को अलग करना, जहां कोई निर्णय संभव ही नहीं है, वाक्य-विन्यास पर केन्द्रित नियमों का पहला समूह तब से कोई विकल्प नहीं छोड़ता है प्रत्येक वाक्यात्मक नियम के अनुरूप एक अद्वितीय टाइपिंग नियम होता है, जो निर्धारित करता है प्रमाण का एक भाग, जबकि निष्कर्ष और इनके परिसर के बीच के निश्चित भागों की शृंखलाएँ $[{\mathtt {Inst}}]$ और $[{\mathtt {Gen}}]$ घटित हो सकता है। ऐसी श्रृंखला के निष्कर्ष के बीच भी मौजूद हो सकती है सर्वोच्च अभिव्यक्ति के लिए प्रमाण और नियम। सभी सबूत होने चाहिए इतना रेखांकित आकार।

क्योंकि नियम चयन के संबंध में प्रमाण में एकमात्र विकल्प हैं $[{\mathtt {Inst}}]$ और $[{\mathtt {Gen}}]$ जंजीरें, प्रमाण का स्वरूप यह प्रश्न सुझाता है कि क्या इसे और अधिक सटीक बनाया जा सकता है, जहां इन जंजीरों की आवश्यकता नहीं हो सकती है। यह वास्तव में संभव है और एक की ओर ले जाता है नियम प्रणाली का एक टाइप जिसमें ऐसे कोई नियम नहीं हैं।

सिंटैक्स-निर्देशित नियम प्रणाली

Syntactical Rule System
${\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \sigma \sqsubseteq \tau }{\Gamma \vdash _{S}x:\tau }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{S}e_{0}:\tau \rightarrow \tau '\quad \quad \Gamma \vdash _{S}e_{1}:\tau }{\Gamma \vdash _{S}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\Gamma ,\;x:\tau \vdash _{S}e:\tau '}{\Gamma \vdash _{S}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{S}e_{0}:\tau \quad \quad \Gamma ,\,x:{\bar {\Gamma }}(\tau )\vdash _{S}e_{1}:\tau '}{\Gamma \vdash _{S}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau '}}&[{\mathtt {Let}}]\end{array}}$
Generalization
${\bar {\Gamma }}(\tau )=\forall \ {\hat {\alpha }}\ .\ \tau \quad \quad {\hat {\alpha }}={\textrm {free}}(\tau )-{\textrm {free}}(\Gamma )$

एचएम का एक समकालीन उपचार विशुद्ध रूप से सिंटेक्स-निर्देशित नियम प्रणाली का उपयोग करता है मेहरबान^[7] एक मध्यवर्ती कदम के रूप में। इस प्रणाली में, विशेषज्ञता सीधे मूल के बाद स्थित होती है $[{\mathtt {Var}}]$ नियम और इसमें विलीन हो जाता है, जबकि सामान्यीकरण इसका हिस्सा बन जाता है $[{\mathtt {Let}}]$ नियम। वहां सामान्यीकरण है फ़ंक्शन को प्रस्तुत करके हमेशा सबसे सामान्य टाइप का उत्पादन करने के लिए भी निर्धारित किया गया है ${\bar {\Gamma }}(\tau )$ , जो मात्रा निर्धारित करता है सभी मोनोटाइप चर बाध्य नहीं हैं $\Gamma$ ।

औपचारिक रूप से, इस नई नियम प्रणाली को मान्य करने के लिए $\vdash _{S}$ मूल के समतुल्य है $\vdash _{D}$ , किसी के पास उसे दिखाने के लिए $\Gamma \vdash _{D}\ e:\sigma \Leftrightarrow \Gamma \vdash _{S}\ e:\sigma$ , जो दो उप-प्रमाणों में विघटित हो जाता है:

$\Gamma \vdash _{D}\ e:\sigma \Leftarrow \Gamma \vdash _{S}\ e:\sigma$ (गाढ़ापन)
$\Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\sigma$ (पूर्णता (तर्क))

जबकि नियमों को विघटित करके एकरूपता देखी जा सकती है $[{\mathtt {Let}}]$ और $[{\mathtt {Var}}]$ का $\vdash _{S}$ सबूतों में $\vdash _{D}$ , संभावना यही दिख रही है $\vdash _{S}$ अधूरा है, जैसे कोई दिखा नहीं सकता $\lambda \ x.x:\forall \alpha .\alpha \rightarrow \alpha$ में $\vdash _{S}$ , उदाहरण के लिए, लेकिन केवल $\lambda \ x.x:\alpha \rightarrow \alpha$ । पूर्णता का केवल थोड़ा कमजोर संस्करण ही सिद्ध किया जा सकता है ^[8] हालाँकि, अर्थात्

$\Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\tau \wedge {\bar {\Gamma }}(\tau )\sqsubseteq \sigma$

तात्पर्य यह है कि, कोई किसी अभिव्यक्ति के लिए मुख्य टाइप प्राप्त कर सकता है $\vdash _{S}$ हमें अंत में प्रमाण को सामान्यीकृत करने की अनुमति देता है।

की तुलना $\vdash _{D}$ और $\vdash _{S}$ , अब सभी नियमों के निर्णयों में केवल मोनोटाइप ही दिखाई देते हैं। इसके अतिरिक्त, निगमन प्रणाली के साथ किसी भी संभावित प्रमाण का आकार अब अभिव्यक्ति के आकार के समान है (दोनों को टर्म (तर्क)#औपचारिक परिभाषा के रूप में देखा जाता है)। इस टाइप अभिव्यक्ति पूरी तरह से प्रमाण के आकार को निर्धारित करती है। में $\vdash _{D}$ आकार संभवतः सभी नियमों को छोड़कर अन्य नियमों के अनुसार निर्धारित किया जाएगा $[{\mathtt {Inst}}]$ और $[{\mathtt {Gen}}]$ , जो अन्य नोड्स के बीच मनमाने ढंग से लंबी शाखाएं (चेन) बनाने की अनुमति देता है।

नियमों को लागू करने वाली स्वतंत्रता की डिग्री

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

यहां, प्रतिस्थापन (विशेषज्ञता) ऑर्डर चलन में आता है। हालाँकि पहली नज़र में कोई भी स्थानीय रूप से टाइप को निर्धारित नहीं कर सकता है, आशा है कि प्रमाण वृक्ष को पार करते समय ऑर्डर की सहायता से उन्हें परिष्कृत करना संभव है, इसके अतिरिक्त यह मानते हुए, क्योंकि परिणामी कलन विधि एक अनुमान विधि बनना है, कि किसी भी परिसर का टाइप सर्वोत्तम संभव के रूप में निर्धारित किया जाएगा। और वास्तव में, कोई भी, के नियमों को देखते हुए, ऐसा कर सकता है $\vdash _{S}$ सुझाव:

$[Abs]$ : महत्वपूर्ण विकल्प है $τ$ । फिलहाल इस बारे में कुछ पता नहीं चल पाया है $τ$ , इसलिए कोई केवल सबसे सामान्य टाइप ही मान सकता है, जो कि है $\forall \alpha .\alpha$ । योजना यह है कि यदि आवश्यक हो तो टाइप को विशेषज्ञ बनाया जाए। दुर्भाग्य से, इस स्थान पर पॉलीटाइप की अनुमति नहीं है, इसलिए कुछ $α$ फिलहाल करना होगा। अवांछित कैप्चर से बचने के लिए, एक टाइप का चर जो अभी तक प्रूफ़ में नहीं है, एक सुरक्षित विकल्प है। इसके अतिरिक्त, किसी को यह ध्यान में रखना होगा कि यह मोनोटाइप अभी तक तय नहीं हुआ है, लेकिन इसे और परिष्कृत किया जा सकता है।
$[Var]$ : चुनाव यह है कि कैसे परिष्कृत किया जाए $σ$ । क्योंकि किसी भी टाइप का कोई भी विकल्प $τ$ यहां चर के उपयोग पर निर्भर करता है, जो स्थानीय रूप से ज्ञात नहीं है, सबसे सुरक्षित दांव सबसे सामान्य है। ऊपर दी गई समान विधि का उपयोग करके सभी मात्रात्मक चर को तुरंत चालू किया जा सकता है $σ$ नए चर मोनोटाइप चर के साथ, उन्हें फिर से आगे के शोधन के लिए विवृत रखा गया है।
$[Let]$ : नियम कोई विकल्प नहीं छोड़ता। पूर्ण।
[App]: केवल अनुप्रयोग नियम ही अब तक खोले गए चर को परिष्कृत करने के लिए बाध्य कर सकता है, जैसा कि दोनों परिसरों द्वारा आवश्यक है।
1. पहला आधार अनुमान के परिणाम को प्रपत्र का होने के लिए बाध्य करता है $\tau \rightarrow \tau '$ $\tau \rightarrow \tau '$ ।
  - अगर ऐसा है तो ठीक है। कोई भी बाद में इसे चुन सकता है $τ'$ परिणाम के लिए।
  - यदि नहीं, तो यह एक विवृत चर हो सकता है। फिर इसे पहले की तरह दो नए चर के साथ आवश्यक रूप में परिष्कृत किया जा सकता है।
  - अन्यथा, टाइप की जाँच विफल हो जाती है क्योंकि पहले आधार से एक ऐसे टाइप इन्फेरेंस लगाया गया है जो फ़ंक्शन टाइप में नहीं है और न ही बनाया जा सकता है।
2. दूसरे आधार के लिए आवश्यक है कि अनुमानित टाइप बराबर हो $τ$ पहले परिसर का। अब संभवतः दो अलग-अलग टाइप हैं, शायद खुले टाइप के चर के साथ, तुलना करने के लिए और यदि संभव हो तो बराबर करने के लिए। यदि ऐसा है, तो एक शोधन पाया जाता है, और यदि नहीं, तो एक टाइप की त्रुटि फिर से पाई जाती है। प्रतिस्थापन द्वारा दो शब्दों को समान बनाने के लिए एक प्रभावी विधि ज्ञात है, तथाकथित असंयुक्त-सेट डेटा संरचना के साथ संयोजन में जॉन एलन रॉबिन्सन | रॉबिन्सन का एकीकरण (कंप्यूटिंग) | संयोजन-फाइंड कलन विधि।

संघ-खोज कलन विधि को संक्षेप में संक्षेप में प्रस्तुत करने के लिए, एक प्रमाण में सभी टाइप के सेट को देखते हुए, यह किसी को एक के माध्यम से उन्हें समतुल्य वर्गों में समूहित करने की अनुमति देता है। union प्रक्रिया और ऐसे प्रत्येक वर्ग के लिए एक प्रतिनिधि चुनना find प्रक्रिया। साइड इफेक्ट (कंप्यूटर विज्ञान) के अर्थ में प्रक्रिया (कंप्यूटर विज्ञान) शब्द पर जोर देते हुए, हम एक प्रभावी कलन विधि तैयार करने के लिए स्पष्ट रूप से तर्क के दायरे को छोड़ रहे हैं। ए के प्रतिनिधि ${\mathtt {union}}(a,b)$ इस टाइप निर्धारित किया जाता है कि, यदि दोनों $a$ और $b$ टाइप के चर हैं तो प्रतिनिधि मनमाने ढंग से उनमें से एक है, लेकिन एक चर और एक अभिव्यक्ति को एकजुट करते समय, अभिव्यक्ति प्रतिनिधि बन जाता है। संयोजन-फाइंड के कार्यान्वयन को हाथ में लेते हुए, कोई दो मोनोटाइप्स के एकीकरण को निम्नानुसार तैयार कर सकता है:

एकजुट(ta, tb):
    टा = खोजें(टा)
    टीबी = खोजें(टीबी)
    यदि दोनों ta,tb समान D,n के साथ D p1।।pn रूप के अभिव्यक्ति हैं
        प्रत्येक संगत iवें मापदण्ड के लिए unify(ta[i], tb[i])।
    अन्य
    यदि ta,tb में से न्यूनतम एक एक टाइप का चर है
        संघ(टीए, टीबी)
    अन्य
        त्रुटि 'टाइप मेल नहीं खाते'

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

कलन विधि एक्स

Algorithm J
${\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \tau ={\mathit {inst}}(\sigma )}{\Gamma \vdash _{J}x:\tau }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{J}e_{0}:\tau _{0}\quad \Gamma \vdash _{J}e_{1}:\tau _{1}\quad \tau '={\mathit {newvar}}\quad {\mathit {unify}}(\tau _{0},\ \tau _{1}\rightarrow \tau ')}{\Gamma \vdash _{J}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\tau ={\mathit {newvar}}\quad \Gamma ,\;x:\tau \vdash _{J}e:\tau '}{\Gamma \vdash _{J}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{J}e_{0}:\tau \quad \quad \Gamma ,\,x:{\bar {\Gamma }}(\tau )\vdash _{J}e_{1}:\tau '}{\Gamma \vdash _{J}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau '}}&[{\mathtt {Let}}]\end{array}}$

कलन विधि जे की प्रस्तुति तार्किक नियमों के अंकन का दुरुपयोग है, क्योंकि इसमें दुष्प्रभाव शामिल हैं लेकिन इसके साथ सीधी तुलना की अनुमति मिलती है $\vdash _{S}$ साथ ही एक कुशल कार्यान्वयन को व्यक्त करते हुए। नियम अब मापदंडों के साथ एक प्रक्रिया निर्दिष्ट करते हैं $\Gamma ,e$ उपज $\tau$ निष्कर्ष में जहां परिसर का निष्पादन बाएं से दाएं की ओर बढ़ता है।

प्रक्रिया $inst(\sigma )$ पॉलीटाइप में विशेषज्ञता रखता है $\sigma$ शब्द की प्रतिलिपि बनाकर और बाध्य टाइप चर को लगातार नए मोनोटाइप चर द्वारा प्रतिस्थापित करके। ' $newvar$ ' एक नया मोनोटाइप चर उत्पन्न करता है। संभावित, ${\bar {\Gamma }}(\tau )$ अवांछित कैप्चर से बचने के लिए परिमाणीकरण के लिए नए चर पेश करने वाले टाइप की प्रतिलिपि बनाना होगा। कुल मिलाकर, कलन विधि अब विशेषज्ञता को एकीकरण पर छोड़कर हमेशा सबसे सामान्य विकल्प चुनकर आगे बढ़ता है, जो स्वयं सबसे सामान्य परिणाम उत्पन्न करता है। जैसा कि उल्लेख किया गया है #सिंटैक्स संचालित नियम प्रणाली, अंतिम परिणाम $\tau$ को सामान्यीकृत करना होगा ${\bar {\Gamma }}(\tau )$ अंत में, किसी दिए गए अभिव्यक्ति के लिए सबसे सामान्य टाइप प्राप्त करने के लिए।

चूँकि कलन विधि में उपयोग की जाने वाली प्रक्रियाओं की लागत लगभग O(1) होती है, कलन विधि की कुल लागत उस अभिव्यक्ति के आकार में रैखिक के करीब होती है जिसके लिए एक टाइप इन्फेरेंस लगाया जाना है। यह टाइप अनुमान कलन विधि प्राप्त करने के कई अन्य प्रयासों के बिल्कुल विपरीत है, जो अक्सर समाप्ति के संबंध में अनिर्णीत समस्या होने पर भी एनपी कठिन के रूप में सामने आता है। इस टाइप एचएम सबसे अच्छा पूर्णतः सूचित टाइप-चेकिंग कलन विधि का प्रदर्शन कर सकता है। यहां टाइप-चेकिंग का मतलब है कि कलन विधि को कोई प्रमाण ढूंढना नहीं है, बल्कि केवल किसी दिए गए प्रमाण को मान्य करना है।

दक्षता थोड़ी अल्प हो गई है क्योंकि गणना की अनुमति देने के लिए संदर्भ में टाइप चर के सीमित को बनाए रखना पड़ता है ${\bar {\Gamma }}(\tau )$ और पुनरावर्ती टाइप के निर्माण को रोकने के लिए एक घटित जाँच को सक्षम करें $union(\alpha ,\tau )$ । ऐसे ही एक मामले का उदाहरण है $\lambda \ x.(x\ x)$ , जिसके लिए एचएम का उपयोग करके कोई टाइप प्राप्त नहीं किया जा सकता है। व्यावहारिक रूप से, टाइप केवल छोटे शब्द हैं और विस्तारित संरचनाओं का निर्माण नहीं करते हैं। इस टाइप, जटिलता विश्लेषण में, कोई उनकी तुलना O(1) लागत को बनाए रखते हुए एक स्थिर मान के रूप में कर सकता है।

कलन विधि साबित करना

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

उपरोक्त तर्क में सबसे महत्वपूर्ण बिंदु मोनोटाइप का परिशोधन है संदर्भ से सीमित चर। उदाहरण के लिए, कलन विधि साहसपूर्वक बदलता है उदाहरण के लिए अनुमान लगाते समय संदर्भ $\lambda f.(f\ 1)$ , क्योंकि मोनोटाइप चर को मापदण्ड के संदर्भ में जोड़ा गया है $f$ बाद में परिष्कृत करने की आवश्यकता है को $int\rightarrow \beta$ अनुप्रयोग को संभालते समय। समस्या यह है कि निगमन नियम ऐसे परिशोधन की अनुमति नहीं देते हैं। तर्क देते हुए कहा कि इसके स्थान पर पहले भी परिष्कृत टाइप जोड़ा जा सकता था मोनोटाइप चर सर्वोत्तम रूप से समीचीन है।

औपचारिक रूप से संतोषजनक तर्क तक पहुंचने की कुंजी उचित रूप से शामिल करना है परिशोधन के अंतर्गत संदर्भ। औपचारिक रूप से, टाइपिंग मुक्त टाइप चर के प्रतिस्थापन के साथ संगत है।

\Gamma \vdash _{S}e:\tau \quad \Longrightarrow \quad S\Gamma \vdash _{S}e:S\tau

इस टाइप मुक्त चरों को परिष्कृत करने का अर्थ है संपूर्ण टाइपिंग को परिष्कृत करना।

कलन विधि Ω

Algorithm W
$\begin{array}{cl} x : σ \in Γ τ = i n s t (σ) Γ ⊢_{W} x : τ, \emptyset [V a r] & \frac{\begin{array}{ll} Γ ⊢_{W} e_{0} : τ_{0}, S_{0} & S_{0} Γ ⊢_{W} e_{1} : τ_{1}, S_{1} \\ τ^{'} = n e w v a r & S_{2} = m g u (S_{1} τ_{0}, τ_{1} \to τ^{'}) \end{array}}{Γ ⊢_{W} e_{0} e_{1} : S_{2} τ^{'}, S_{2} S_{1} S_{0}} & [A p p] & \frac{τ = n e w v a r Γ, x : τ ⊢_{W} e : τ^{'}, S}{Γ ⊢_{W} λ x . e : S τ \to τ^{'}, S} & [A b s] & Γ ⊢_{W} e_{0} : τ, S_{0} S_{0} Γ, x : \bar{S_{0} Γ} (τ) ⊢_{W} e_{1} \end{array}$

वहां से, कलन विधि J का प्रमाण कलन विधि W की ओर ले जाता है, जो केवल बनाता है प्रक्रिया द्वारा लगाए गए दुष्प्रभाव

{\textit {union}}

द्वारा स्पष्ट प्रतिस्थापनों के माध्यम से इसकी क्रमिक संरचना को व्यक्त करना

S_{i}

। साइडबार में कलन विधि डब्ल्यू की प्रस्तुति अभी भी साइड इफेक्ट्स का उपयोग करती है इटैलिक में सेट किए गए ऑपरेशनों में, लेकिन ये अब जनरेटिंग तक ही सीमित हैं ताजा प्रतीक। निर्णय का स्वरूप है

\Gamma \vdash e:\tau ,S

, एक फ़ंक्शन को संदर्भ और अभिव्यक्ति के साथ मापदण्ड के रूप में निरूपित करना एक साथ एक मोनोटाइप का निर्माण करता है एक प्रतिस्थापन।

{\textsf {mgu}}

एक दुष्प्रभाव मुक्त संस्करण है का

{\textit {union}}

एक प्रतिस्थापन का निर्माण जो प्रथम-ऑर्डर शब्दों का एकीकरण (कंप्यूटर विज्ञान)#वाक्यात्मक एकीकरण है।

जबकि कलन विधि W को सामान्यतः HM कलन विधि माना जाता है और है प्रायः साहित्य में नियम व्यवस्था के बाद सीधे प्रस्तुत किया जाता है, इसका उद्देश्य है मिलनर द्वारा वर्णित^[2]पी। 369 पर इस टाइप है:

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

जबकि उन्होंने डब्ल्यू को अधिक जटिल और अल्प कुशल माना, उन्होंने इसे प्रस्तुत किया जे से पहले अपने प्रकाशन में। जब दुष्प्रभाव अनुपलब्ध या अवांछित होते हैं तो इसके अपने गुण होते हैं। पूर्णता साबित करने के लिए डब्ल्यू की भी आवश्यकता होती है, जिसे उसके द्वारा सुदृढ़ता प्रमाण में शामिल किया जाता है।

प्रमाण दायित्व

प्रमाण दायित्वों को तैयार करने से पहले, नियम प्रणाली डी और एस और प्रस्तुत कलन विधि के बीच विचलन पर जोर दिया जाना चाहिए।

जबकि उपरोक्त विकास ने "ओपन" प्रमाण चर के रूप में मोनोटाइप्स का दुरुपयोग किया था, इस संभावना को कि उचित मोनोटाइप चर को नुकसान पहुंचाया जा सकता था, नए चर पेश करके और सर्वोत्तम की उम्मीद करके दरकिनार कर दिया गया था। लेकिन इसमें परेशानी है: किए गए वादों में से एक यह था कि इन नए बदलावों को इसी तरह ध्यान में रखा जाएगा। यह वादा कलन विधि द्वारा पूरा नहीं किया गया है।

एक प्रसंग होना $1:int,\ f:\alpha$ , अभिव्यक्ति $f\ 1$ टाइप $\vdash _{D}$ या $\vdash _{S}$ भी नहीं किया जा सकता, लेकिन कलन विधि साथ प्ररूप $\beta$ आते हैं, जहां W अतिरिक्त रूप से प्रतिस्थापन प्रदान करता है $\left\{\alpha \mapsto int\rightarrow \beta \right\}$ , इसका मतलब है कि कलन विधि सभी टाइप की त्रुटियों का पता लगाने में विफल रहता है। इस चूक को अधिक सावधानी से अलग किए गए प्रमाण चर और मोनोटाइप चर द्वारा आसानी से ठीक किया जा सकता है।

लेखक समस्या से अच्छी तरह परिचित थे लेकिन उन्होंने इसे ठीक न करने का निर्णय लिया। इसके पीछे कोई व्यावहारिक कारण मान सकता है। जबकि टाइप इन्फेरेंस को अधिक उचित ढंग से लागू करने से कलन विधि अमूर्त मोनोटाइप से निपटने में सक्षम हो जाता, इच्छित अनुप्रयोग के लिए उनकी आवश्यकता नहीं थी, जहां पहले से मौजूद संदर्भ में कोई भी आइटम मुफ़्त नहीं है चर। इस प्रकाश में, एक सरल कलन विधि के पक्ष में अनावश्यक जटिलता को हटा दिया गया। शेष नकारात्मक पक्ष यह है कि नियम प्रणाली के संबंध में कलन विधि का प्रमाण अल्प सामान्य है और इसे केवल बनाया जा सकता है के साथ संदर्भों के लिए $free(\Gamma )=\emptyset$ एक पार्श्व शर्त के रूप में।

${\begin{array}{lll}{\text{(Correctness)}}&\Gamma \vdash _{W}e:\tau ,S&\quad \Longrightarrow \quad \Gamma \vdash _{S}e:\tau \\{\text{(Completeness)}}&\Gamma \vdash _{S}e:\tau &\quad \Longrightarrow \quad \Gamma \vdash _{W}e:\tau ',S\quad \quad {\text{forall}}\ \tau \ {\text{where}}\ {\overline {\emptyset }}(\tau ')\sqsubseteq \tau \end{array}}$ पूर्णता दायित्व में साइड कंडीशन यह बताती है कि कैसे निगमन कई टाइप दे सकती है, जबकि कलन विधि हमेशा एक उत्पन्न करता है। साथ ही, साइड कंडीशन की मांग है कि अनुमानित टाइप वास्तव में सबसे सामान्य है।

दायित्वों को ठीक से साबित करने के लिए पहले उन्हें मजबूत करने की आवश्यकता है ताकि प्रतिस्थापन लेम्मा को सक्रिय करने की अनुमति मिल सके जो प्रतिस्थापन को फैलाता है $S$ द्वारा $\vdash _{S}$ और $\vdash _{W}$ । वहां से, प्रमाण अभिव्यक्ति पर प्रेरण द्वारा होते हैं।

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

एक्सटेंशन

पुनरावर्ती परिभाषाएँ

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

टाइपिंग नियम

मूल कागज^[4]दिखाता है कि रिकर्सन को कॉम्बिनेटर द्वारा सिद्ध किया जा सकता है ${\mathit {fix}}:\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha$ । संभावित पुनरावर्ती परिभाषा इस टाइप तैयार की जा सकती है ${\mathtt {rec}}\ v=e_{1}\ {\mathtt {in}}\ e_{2}\ ::={\mathtt {let}}\ v={\mathit {fix}}(\lambda v.e_{1})\ {\mathtt {in}}\ e_{2}$ ।

वैकल्पिक रूप से अभिव्यक्ति सिंटैक्स का विस्तार और अतिरिक्त टाइपिंग नियम संभव है:

\displaystyle {\frac {\Gamma ,\Gamma '\vdash e_{1}:\tau _{1}\quad \dots \quad \Gamma ,\Gamma '\vdash e_{n}:\tau _{n}\quad \Gamma ,\Gamma ''\vdash e:\tau }{\Gamma \ \vdash \ {\mathtt {rec}}\ v_{1}=e_{1}\ {\mathtt {and}}\ \dots \ {\mathtt {and}}\ v_{n}=e_{n}\ {\mathtt {in}}\ e:\tau }}\quad [{\mathtt {Rec}}]

जहाँ

$\Gamma '=v_{1}:\tau _{1},\ \dots ,\ v_{n}:\tau _{n}$
$\Gamma ''=v_{1}:{\bar {\Gamma }}(\ \tau _{1}\ ),\ \dots ,\ v_{n}:{\bar {\Gamma }}(\ \tau _{n}\ )$

मूलतः विलय मोनोटाइप स्थितियों में पुनरावर्ती रूप से परिभाषित चर को शामिल करते हुए $[{\mathtt {Abs}}]$ और $[{\mathtt {Let}}]$ को विलय करना जहां वे ${\mathtt {in}}$ के बाईं ओर होते हैं लेकिन इसके दाईं ओर पॉलीटाइप के रूप में होते हैं।

परिणाम

हालाँकि उपरोक्त सीधा है, इसकी कीमत चुकानी पड़ती है।

टाइप सिद्धांत लैम्ब्डा कलन को गणना और तर्क से जोड़ती है। उपरोक्त आसान संशोधन का दोनों पर प्रभाव पड़ता है:

सामान्यीकरण गुण (सार पुनर्लेखन) अमान्य है, क्योंकि गैर-समाप्ति शर्तों को तैयार किया जा सकता है।
तर्क संगति हो जाता है क्योंकि टाइप $\forall a.a$ सयात्रिक बन जाता है।

ओवरलोडिंग

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

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

quickSort :: Ord a => [a] -> [a]

यहाँ, टाइप a न केवल बहुरूपी है, बल्कि कुछ टाइप के वर्ग Ord का उदाहरण होने तक भी सीमित हैऑर्डर विधेय प्रदान < और >= करता है फ़ंक्शंस बॉडी में उपयोग किया जाता है। इन विधेयों के उचित कार्यान्वयन को अतिरिक्त मापदंडों के रूप में क्विकॉर्ट्स को पास कर दिया जाता है, जैसे ही क्विकॉर्ट का उपयोग अधिक ठोस टाइप पर किया जाता है जो ओवरलोडेड फ़ंक्शन क्विकसॉर्ट का एकल कार्यान्वयन प्रदान करता है।

क्योंकि "वर्ग" केवल एक ही टाइप को अपने तर्क के रूप में अनुमति देती हैं, परिणामी टाइप प्रणाली अभी भी अनुमान प्रदान कर सकती है। इसके अतिरिक्त, टाइप की वर्ग को किसी टाइप के ओवरलोडिंग ऑर्डर से सुसज्जित किया जा सकता है, जिससे वर्ग को जाली (ऑर्डर) के रूप में व्यवस्थित किया जा सकता है।

उच्च-ऑर्डर टाइप

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

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

अतिरिक्त स्तर के हिस्सों को को हास्केल नाम के टाइप (टाइप सिद्धांत) में पेश किया गया है, जहां इसका उपयोग मोनाड (अभिलक्षकी प्रोग्रामिंग) टाइप करने में मदद के लिए किया जाता है। विस्तारित टाइप प्रणाली के आंतरिक यांत्रिकी में पर्दे के पीछे काम करते हुए, टाइप को अंतर्निहित छोड़ दिया जाता है।

उपटाइपिंग

उपटाइपिंग और टाइप इन्फेरेंस को संयोजित करने के प्रयासों से काफी निराशा हुई है।उपटाइपिंग व्यवरोध को जमा करना और प्रचारित करना (टाइप समानता व्यवरोध के विपरीत) सरल है, जिससे परिणामी व्यवरोध को अनुमानित टाइपिंग योजनाओं का हिस्सा बना दिया जाता है, उदाहरण के लिए $\forall \alpha .\ (\alpha \leq T)\Rightarrow \alpha \rightarrow \alpha$ , जहाँ $\alpha \leq T$ टाइप चर $\alpha$ पर व्यवरोध है। हालाँकि, क्योंकि टाइप चर अब इस दृष्टिकोण में उत्सुकता से एकीकृत नहीं हैं, यह कई सामान्य टाइप चर और व्यवरोध से युक्त बड़ी और बोझिल टाइपिंग योजनाएं उत्पन्न करता है, जिससे उन्हें पढ़ना और समझना कठिन हो जाता है। इसलिए, ऐसी टाइपिंग योजनाओं और उनकी व्यवरोध को सरल बनाने में काफी प्रयास किए गए, गैर-नियतात्मक परिमित स्वचल प्ररूप (एनएफए) सरलीकरण के समान तकनीकों का उपयोग करना है (अनुमानित पुनरावर्ती टाइप की उपस्थिति में उपयोगी)।^[9] अभी हाल ही में, डोलन और माइक्रॉफ्ट^[10]टाइपिंग योजना सरलीकरण और एनएफए सरलीकरण के बीच संबंध को औपचारिक रूप दिया गया और दिखाया कि उपटाइपिंग की औपचारिकता पर बीजगणितीय टेक ने एमएल जैसी लैंग्वेज (जिसे एमएलसब कहा जाता है) के लिए कॉम्पैक्ट प्रिंसिपल टाइपिंग योजनाएं तैयार करने की अनुमति दी। विशेष रूप से, उनकी प्रस्तावित टाइपिंग योजना में स्पष्ट व्यवरोध के बजाय संघ और प्रतिच्छेदन टाइप के प्रतिबंधित रूप का उपयोग किया गया था। पार्रेक्स ने बाद में दावा किया^[11] यह बीजगणितीय सूत्रीकरण कलन विधि डब्ल्यू से मिलते-जुलते अपेक्षाकृत सरल कलन विधि के बराबर था, और यह कि संयोजन और प्रतिच्छेदन टाइप का उपयोग आवश्यक नहीं था।

दूसरी ओर, ऑब्जेक्ट-ओरिएंटेड प्रोग्रामिंग लैंग्वेज के संदर्भ में टाइप इन्फेरेंस अधिक कठिन साबित हुआ है, क्योंकि ऑब्जेक्ट विधियों को प्रणाली एफ की शैली में प्रथम श्रेणी बहुरूपता की आवश्यकता होती है (जहां टाइप इन्फेरेंस अनिर्दिष्ट है) और एफ-बद्ध बहुरूपता सुविधाओं के कारण होती है, नतीजतन, ऑब्जेक्ट-ओरिएंटेड प्रोग्रामिंग को सक्षम करने वाले सबटाइपिंग वाले टाइप प्रणाली, जैसे लुका कार्डेली का प्रणाली एफ-उप $F_{<:}$ ,^[12] एचएम-शैली टाइप के अनुमान का समर्थन न करें।

पंक्ति बहुरूपता का उपयोग संरचनात्मक रिकॉर्ड जैसी लैंग्वेज सुविधाओं का समर्थन करने के लिए उपटाइपिंग के विकल्प के रूप में किया जा सकता है।^[13]हालाँकि बहुरूपता की यह शैली कुछ मायनों में उपटाइपिंग की तुलना में अल्प नम्य है, विशेष रूप से टाइप की व्यवरोध में दिशात्मकता की कमी से निपटने के लिए कड़ाई से आवश्यकता से अधिक बहुरूपता की आवश्यकता होती है, इसका लाभ यह है कि इसे मानक एचएम कलन विधि के साथ काफी आसानी से एकीकृत किया जा सकता है।

↑ Hindley–Milner type inference is DEXPTIME-complete. In fact, merely deciding whether an ML program is typeable (without having to infer a type) is itself DEXPTIME-complete. Non-linear behaviour does manifest itself, yet mostly on pathological inputs. Thus the complexity theoretic proofs by Mairson (1990) and Kfoury, Tiuryn & Urzyczyn (1990) came as a surprise to the research community.
↑ Polytypes are called "type schemes" in the original article.
↑ The parametric types $C\ \tau \dots \tau$ were not present in the original paper on HM and are not needed to present the method. None of the inference rules below will take care or even note them. The same holds for the non-parametric "primitive types" in said paper. All the machinery for polymorphic type inference can be defined without them. They have been included here for sake of examples but also because the nature of HM is all about parametric types. This comes from the function type $\tau \rightarrow \tau$ , hard-wired in the inference rules, below, which already has two parameters and has been presented here as only a special case.
↑ Haskell provides the ScopedTypeVariables language extension allowing to bring all-quantified type variables into scope.

संदर्भ

↑ Hindley, J. Roger (1969). "संयोजन तर्क में किसी वस्तु की प्रमुख प्रकार-योजना". Transactions of the American Mathematical Society. 146: 29–60. doi:10.2307/1995158. JSTOR 1995158.
↑ ^2.0 ^2.1 ^2.2 Milner, Robin (1978). "प्रोग्रामिंग में टाइप पालीमॉर्फिज़्म का एक सिद्धांत". Journal of Computer and System Sciences. 17 (3): 348–374. CiteSeerX 10.1.1.67.5276. doi:10.1016/0022-0000(78)90014-4. S2CID 388583.
↑ Damas, Luis (1985). प्रोग्रामिंग भाषाओं में असाइनमेंट टाइप करें (PhD thesis). University of Edinburgh. hdl:1842/13555. CST-33-85.
↑ ^4.0 ^4.1 ^4.2 Damas, Luis; Milner, Robin (1982). कार्यात्मक कार्यक्रमों के लिए प्रमुख प्रकार-योजनाएँ (PDF). 9th Symposium on Principles of programming languages (POPL'82). ACM. pp. 207–212. doi:10.1145/582153.582176. ISBN 978-0-89791-065-1.
↑ Milner, Robin (1978), "A Theory of Type Polymorphism in Programming", Journal of Computer and System Sciences, 17 (3): 348–375, doi:10.1016/0022-0000(78)90014-4
↑ Wells, J.B. (1994). "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable". Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 176–185. doi:10.1109/LICS.1994.316068. ISBN 0-8186-6310-3. S2CID 15078292.
↑ Clement (1986). A Simple Applicative Language: Mini-ML. LFP'86. ACM. doi:10.1145/319838.319847. ISBN 978-0-89791-200-6.
↑ Vaughan, Jeff (July 23, 2008) [May 5, 2005]. "A proof of correctness for the Hindley–Milner type inference algorithm" (PDF). Archived from the original (PDF) on 2012-03-24. {{cite journal}}: Cite journal requires |journal= (help)
↑ Pottier, François (1998). Type Inference in the Presence of Subtyping: from Theory to Practice (Thesis). Retrieved 2021-08-10.
↑ Dolan, Stephen; Mycroft, Alan (2017). "Polymorphism, subtyping, and type inference in MLsub". POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. doi:10.1145/3009837.3009882.
↑ Parreaux, Lionel (2020). "The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy". 25th ACM SIGPLAN International Conference on Functional Programming - ICFP 2020, [Online event], August 24-26, 2020. doi:10.1145/3409006.
↑ Cardelli, Luca; Martini, Simone; Mitchell, John C.; Scedrov, Andre (1994). "An extension of system F with subtyping". Information and Computation, vol. 9. North Holland, Amsterdam. pp. 4–56. doi:10.1006/inco.1994.1013.
↑ Daan Leijen, Extensible records with scoped labels, Institute of Information and Computing Sciences, Utrecht University, Draft, Revision: 76, July 23, 2005

Mairson, Harry G. (1990). "Deciding ML typability is complete for deterministic exponential time". Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '90. pp. 382–401. doi:10.1145/96709.96748. ISBN 978-0-89791-343-0. S2CID 75336. {{cite book}}: |journal= ignored (help)
Kfoury, A. J.; Tiuryn, J.; Urzyczyn, P. (1990). ML typability is dexptime-complete. pp. 206–220. doi:10.1007/3-540-52590-4_50. ISBN 978-3-540-52590-5. {{cite book}}: |journal= ignored (help)

बाहरी संबंध

A literate Haskell implementation of Algorithm W along with its source code on GitHub।
A simple implementation of Hindley-Milner algorithm in Python।

[5] Hindley–Milner type inference is DEXPTIME-complete. In fact, merely deciding whether an ML program is typeable (without having to infer a type) is itself DEXPTIME-complete. Non-linear behaviour does manifest itself, yet mostly on pathological inputs. Thus the complexity theoretic proofs by Mairson (1990) and Kfoury, Tiuryn & Urzyczyn (1990) came as a surprise to the research community.

[8] Polytypes are called "type schemes" in the original article.

[9] The parametric types $C\ \tau \dots \tau$ were not present in the original paper on HM and are not needed to present the method. None of the inference rules below will take care or even note them. The same holds for the non-parametric "primitive types" in said paper. All the machinery for polymorphic type inference can be defined without them. They have been included here for sake of examples but also because the nature of HM is all about parametric types. This comes from the function type $\tau \rightarrow \tau$ , hard-wired in the inference rules, below, which already has two parameters and has been presented here as only a special case.

[10] Haskell provides the ScopedTypeVariables language extension allowing to bring all-quantified type variables into scope.

[1] Hindley, J. Roger (1969). "संयोजन तर्क में किसी वस्तु की प्रमुख प्रकार-योजना". Transactions of the American Mathematical Society. 146: 29–60. doi:10.2307/1995158. JSTOR 1995158.

[Milner-2] 2.0 ^2.1 ^2.2 Milner, Robin (1978). "प्रोग्रामिंग में टाइप पालीमॉर्फिज़्म का एक सिद्धांत". Journal of Computer and System Sciences. 17 (3): 348–374. CiteSeerX 10.1.1.67.5276. doi:10.1016/0022-0000(78)90014-4. S2CID 388583.

[3] Damas, Luis (1985). प्रोग्रामिंग भाषाओं में असाइनमेंट टाइप करें (PhD thesis). University of Edinburgh. hdl:1842/13555. CST-33-85.

[Damas-4] 4.0 ^4.1 ^4.2 Damas, Luis; Milner, Robin (1982). कार्यात्मक कार्यक्रमों के लिए प्रमुख प्रकार-योजनाएँ (PDF). 9th Symposium on Principles of programming languages (POPL'82). ACM. pp. 207–212. doi:10.1145/582153.582176. ISBN 978-0-89791-065-1.

[6] Milner, Robin (1978), "A Theory of Type Polymorphism in Programming", Journal of Computer and System Sciences, 17 (3): 348–375, doi:10.1016/0022-0000(78)90014-4

[7] Wells, J.B. (1994). "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable". Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 176–185. doi:10.1109/LICS.1994.316068. ISBN 0-8186-6310-3. S2CID 15078292.

[11] Clement (1986). A Simple Applicative Language: Mini-ML. LFP'86. ACM. doi:10.1145/319838.319847. ISBN 978-0-89791-200-6.

[x-12] Vaughan, Jeff (July 23, 2008) [May 5, 2005]. "A proof of correctness for the Hindley–Milner type inference algorithm" (PDF). Archived from the original (PDF) on 2012-03-24. {{cite journal}}: Cite journal requires |journal= (help)

[13] Pottier, François (1998). Type Inference in the Presence of Subtyping: from Theory to Practice (Thesis). Retrieved 2021-08-10.

[14] Dolan, Stephen; Mycroft, Alan (2017). "Polymorphism, subtyping, and type inference in MLsub". POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. doi:10.1145/3009837.3009882.

[15] Parreaux, Lionel (2020). "The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy". 25th ACM SIGPLAN International Conference on Functional Programming - ICFP 2020, [Online event], August 24-26, 2020. doi:10.1145/3409006.

[16] Cardelli, Luca; Martini, Simone; Mitchell, John C.; Scedrov, Andre (1994). "An extension of system F with subtyping". Information and Computation, vol. 9. North Holland, Amsterdam. pp. 4–56. doi:10.1006/inco.1994.1013.

[17] Daan Leijen, Extensible records with scoped labels, Institute of Information and Computing Sciences, Utrecht University, Draft, Revision: 76, July 23, 2005

[1]

[2]

[3]

[4]

[note 1]

[5]

[6]

[note 2]

[note 3]

[note 4]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

@@ Line 473: / Line 473: @@
 प्रमाण दायित्वों को तैयार करने से पहले, नियम प्रणाली डी और एस और प्रस्तुत कलन विधि के बीच विचलन पर जोर दिया जाना चाहिए।
-जबकि उपरोक्त विकास ने ओपन प्रूफ चर के रूप में मोनोटाइप्स का दुरुपयोग किया था, इस संभावना को कि उचित मोनोटाइप चर को नुकसान पहुंचाया जा सकता था, नए चर पेश करके और सर्वोत्तम की उम्मीद करके दरकिनार कर दिया गया था। लेकिन इसमें एक दिक्कत है: किए गए वादों में से एक यह था कि इन नए बदलावों को इसी तरह ध्यान में रखा जाएगा। यह वादा कलन विधि द्वारा पूरा नहीं किया गया है।
+जबकि उपरोक्त विकास ने "ओपन" प्रमाण चर के रूप में मोनोटाइप्स का दुरुपयोग किया था, इस संभावना को कि उचित मोनोटाइप चर को नुकसान पहुंचाया जा सकता था, नए चर पेश करके और सर्वोत्तम की उम्मीद करके दरकिनार कर दिया गया था। लेकिन इसमें परेशानी है: किए गए वादों में से एक यह था कि इन नए बदलावों को इसी तरह ध्यान में रखा जाएगा। यह वादा कलन विधि द्वारा पूरा नहीं किया गया है।
-एक प्रसंग होना <math>1 : int,\ f : \alpha</math>, अभिव्यक्ति <math>f\ 1</math>
+एक प्रसंग होना <math>1 : int,\ f : \alpha</math>, अभिव्यक्ति <math>f\ 1</math> टाइप <math>\vdash_D</math> या <math>\vdash_S</math> भी नहीं किया जा सकता, लेकिन कलन विधि साथ प्ररूप <math>\beta</math> आते हैं, जहां W अतिरिक्त रूप से प्रतिस्थापन प्रदान करता है <math>\left\{\alpha \mapsto int \rightarrow \beta\right\}</math>, इसका मतलब है कि कलन विधि सभी टाइप की त्रुटियों का पता लगाने में विफल रहता है। इस चूक को अधिक सावधानी से अलग किए गए प्रमाण चर और मोनोटाइप चर द्वारा आसानी से ठीक किया जा सकता है।
-टाइप भी नहीं किया जा सकता <math>\vdash_D</math> या <math>\vdash_S</math>, लेकिन कलन विधि साथ आते हैं
-प्ररूप <math>\beta</math>, जहां W अतिरिक्त रूप से प्रतिस्थापन प्रदान करता है <math>\left\{\alpha \mapsto int \rightarrow \beta\right\}</math>,
-इसका मतलब है कि कलन विधि सभी टाइप की त्रुटियों का पता लगाने में विफल रहता है। इस चूक को अधिक सावधानी से अलग किए गए प्रमाण द्वारा आसानी से ठीक किया जा सकता है
-चर और मोनोटाइप चर।
-लेखक समस्या से अच्छी तरह परिचित थे लेकिन उन्होंने इसे ठीक न करने का निर्णय लिया। इसके पीछे कोई व्यावहारिक कारण मान सकता है।
+'''लेखक समस्या से अच्छी तरह परिचित थे लेकिन उन्होंने इसे ठीक न करने का निर्णय लिया। इसके पीछे कोई व्यावहारिक कारण मान सकता है।
 जबकि टाइप इन्फेरेंस  को अधिक उचित ढंग से लागू करने से कलन विधि अमूर्त मोनोटाइप से निपटने में सक्षम हो जाता,
-इच्छित अनुप्रयोग के लिए उनकी आवश्यकता नहीं थी, जहां पहले से मौजूद संदर्भ में कोई भी आइटम मुफ़्त नहीं है
+इच्छित अनुप्रयोग के लिए उनकी आवश्यकता नहीं थी, जहां पहले से मौजूद संदर्भ में कोई भी आइटम मुफ़्त नहीं''' है
 चर। इस प्रकाश में, एक सरल कलन विधि के पक्ष में अनावश्यक जटिलता को हटा दिया गया।
 शेष नकारात्मक पक्ष यह है कि नियम प्रणाली के संबंध में कलन विधि का प्रमाण अल्प सामान्य है और इसे केवल बनाया जा सकता है
@@ Line 504: / Line 500: @@
 === पुनरावर्ती परिभाषाएँ ===
-ट्यूरिंग को पूर्णता प्रदान करने के लिए पुनरावर्ती फंक्शन की आवश्यकता होती है।
+प्रोग्रामिंग को व्यावहारिक बनाने के लिए पुनरावर्ती फंक्शन की आवश्यकता होती है। लैम्ब्डा कलन की केंद्रीय गुण यह है कि पुनरावर्ती परिभाषाएँ सीधे उपलब्ध नहीं हैं, बल्कि इन्हें एक [[निश्चित बिंदु संयोजक]] के साथ व्यक्त किया जा सकता है। लेकिन दुर्भाग्य से, फिक्सपॉइंट कॉम्बिनेटर को लैम्ब्डा कैलकुलस के टाइप किए गए संस्करण में सिस्टम पर विनाशकारी प्रभाव डाले बिना तैयार नहीं किया जा सकता है जैसा कि नीचे बताया गया है।
-लैम्ब्डा कलन की एक केंद्रीय संपत्ति पुनरावर्ती परिभाषाएँ है
-सीधे उपलब्ध नहीं हैं, बल्कि इन्हें एक [[निश्चित बिंदु संयोजक]] के साथ व्यक्त किया जा सकता है।
-लेकिन दुर्भाग्य से, फिक्सपॉइंट कॉम्बिनेटर को टाइप किए गए संस्करण में तैयार नहीं किया जा सकता है
-लैम्ब्डा कलन का प्रणाली पर विनाशकारी प्रभाव पड़े बिना जैसा कि बताया गया है
-नीचे।
 ==== टाइपिंग नियम ====
-मूल कागज<ref name="Damas"/>दिखाता है कि रिकर्सन को कॉम्बिनेटर द्वारा महसूस किया जा सकता है
+मूल कागज<ref name="Damas"/>दिखाता है कि रिकर्सन को कॉम्बिनेटर द्वारा सिद्ध किया जा सकता है<math>\mathit{fix}:\forall\alpha.(\alpha\rightarrow\alpha)\rightarrow\alpha</math>। संभावित पुनरावर्ती परिभाषा इस टाइप तैयार की जा सकती है <math>\mathtt{rec}\ v = e_1\ \mathtt{in}\ e_2\ ::=\mathtt{let}\ v = \mathit{fix}(\lambda v.e_1)\ \mathtt{in}\ e_2</math>।
-<math>\mathit{fix}:\forall\alpha.(\alpha\rightarrow\alpha)\rightarrow\alpha</math>। इस टाइप एक संभावित पुनरावर्ती परिभाषा इस टाइप तैयार की जा सकती है
-<math>\mathtt{rec}\ v = e_1\ \mathtt{in}\ e_2\ ::=\mathtt{let}\ v = \mathit{fix}(\lambda v.e_1)\ \mathtt{in}\ e_2</math>।
-वैकल्पिक रूप से अभिव्यक्ति सिंटैक्स का विस्तार और एक अतिरिक्त टाइपिंग नियम संभव है:
+वैकल्पिक रूप से अभिव्यक्ति सिंटैक्स का विस्तार और अतिरिक्त टाइपिंग नियम संभव है:
 : <math>\displaystyle\frac{
@@ Line 527: / Line 516: @@
 * <math>\Gamma' = v_1:\tau_1,\ \dots,\ v_n:\tau_n</math>
 * <math>\Gamma'' = v_1:\bar\Gamma(\ \tau_1\ ),\ \dots,\ v_n:\bar\Gamma(\ \tau_n\ )</math>
-मूलतः विलय <math>[\mathtt{Abs}]</math> और <math>[\mathtt{Let}]</math> जबकि पुनरावर्ती रूप से परिभाषित शामिल है
+मूलतः विलय मोनोटाइप स्थितियों में पुनरावर्ती रूप से परिभाषित चर को शामिल करते हुए <math>[\mathtt{Abs}]</math> और <math>[\mathtt{Let}]</math> को विलय करना जहां वे <math>\mathtt{in}</math> के बाईं ओर होते हैं लेकिन इसके दाईं ओर पॉलीटाइप के रूप में होते हैं।
-मोनोटाइप स्थितियों में चर जहां वे बाईं ओर होते हैं <math>\mathtt{in}</math> लेकिन इसके दाईं ओर बहुप्रकार के रूप में।
 ==== परिणाम ====
@@ Line 534: / Line 522: @@
 हालाँकि उपरोक्त सीधा है, इसकी कीमत चुकानी पड़ती है।
-[[ प्रकार सिद्धांत | टाइप सिद्धांत]] लैम्ब्डा कलन को गणना और तर्क से जोड़ती है।
+[[ प्रकार सिद्धांत | टाइप सिद्धांत]] लैम्ब्डा कलन को गणना और तर्क से जोड़ती है। उपरोक्त आसान संशोधन का दोनों पर प्रभाव पड़ता है:
-उपरोक्त आसान संशोधन का दोनों पर प्रभाव पड़ता है:
-* [[सामान्यीकरण संपत्ति (सार पुनर्लेखन)]] अमान्य है, क्योंकि गैर-समाप्ति शर्तों को तैयार किया जा सकता है।
+* [[सामान्यीकरण संपत्ति (सार पुनर्लेखन)|सामान्यीकरण गुण (सार पुनर्लेखन)]] अमान्य है, क्योंकि गैर-समाप्ति शर्तों को तैयार किया जा सकता है।
-* तर्क संगति क्योंकि टाइप <math>\forall a. a</math> [[निवास प्रकार|निवास टाइप]] बन जाता है।
+* तर्क संगति हो जाता है क्योंकि टाइप <math>\forall a. a</math> सयात्रिक बन जाता है।
 === ओवरलोडिंग ===

Expressions
${\begin{array}{lrll}\\e&=&x&{\textrm {variable}}\\&\vert &e_{1}\ e_{2}&{\textrm {application}}\\&\vert &\lambda \ x\ .\ e&{\textrm {abstraction}}\\&\vert &{\mathtt {let}}\ x=e_{1}\ {\mathtt {in}}\ e_{2}&\\\\\end{array}}$
Types
${\begin{array}{llrll}\\{\textrm {mono}}&\tau &=&\alpha &\ {\textrm {variable}}\\&&\vert &C\ \tau \dots \tau &\ {\textrm {application}}\\{\textrm {poly}}&\sigma &=&\tau \\&&\vert &\forall \ \alpha \ .\ \sigma &\ {\textrm {quantifier}}\\\\\end{array}}$
Context and Typing
${\begin{array}{llrl}\\{\text{Context}}&\Gamma &=&\epsilon \ {\mathtt {(empty)}}\\&&\vert &\Gamma ,\ x:\sigma \\{\text{Typing}}&&=&\Gamma \vdash e:\sigma \\\\\end{array}}$
Free Type Variables
${\begin{array}{ll}\\{\text{free}}(\ \alpha \ )&=\ \left\{\alpha \right\}\\{\text{free}}(\ C\ \tau _{1}\dots \tau _{n}\ )&=\ \bigcup \limits _{i=1}^{n}{{\text{free}}(\ \tau _{i}\ )}\\{\text{free}}(\ \Gamma \ )&=\ \bigcup \limits _{x:\sigma \in \Gamma }{\text{free}}(\ \sigma \ )\\\\{\text{free}}(\ \forall \ \alpha \ .\ \sigma \ )&=\ {\text{free}}(\ \sigma \ )\ -\ \left\{\alpha \right\}\\{\text{free}}(\ \Gamma \vdash e:\sigma \ )&=\ {\text{free}}(\ \sigma \ )\ -\ {\text{free}}(\ \Gamma \ )\\\\\end{array}}$

The Syntax of Rules
${\begin{array}{lrl}{\text{Predicate}}&=&\sigma \sqsubseteq \sigma '\\&\vert \ &\alpha \not \in free(\Gamma )\\&\vert \ &x:\alpha \in \Gamma \\\\{\text{Judgment}}&=&{\text{Typing}}\\{\text{Premise}}&=&{\text{Judgment}}\ \vert \ {\text{Predicate}}\\{\text{Conclusion}}&=&{\text{Judgment}}\\\\{\text{Rule}}&=&\displaystyle {\frac {{\textrm {Premise}}\ \dots }{\textrm {Conclusion}}}\quad [{\mathtt {Name}}]\end{array}}$

Anonymous

Search

हिंडले-मिलनर टाइप सिस्टम: Difference between revisions

Revision as of 15:41, 18 July 2023

परिचय

एकरूपता बनाम बहुरूपता

लेट-पॉलीमोर्फिज्म

सिंहावलोकन

हिंडले-मिलनर टाइप प्रणाली

सिंटेक्स

मोनोटाइप्स

पॉलीटाइप्स (बहुप्रकार)

प्रसंग और टाइपिंग

मुक्त टाइप के चर

टाइप ऑर्डर

मूल टाइप

टाइपिंग में प्रतिस्थापन

निगमनात्मक प्रणाली

टाइपिंग नियम

लेट-बहुरूपता

सामान्यीकरण नियम

अनुमान कलन विधि

नियमों को चुनने की स्वतंत्रता की डिग्री

सिंटैक्स-निर्देशित नियम प्रणाली

नियमों को लागू करने वाली स्वतंत्रता की डिग्री

कलन विधि एक्स

कलन विधि साबित करना

कलन विधि Ω

प्रमाण दायित्व

एक्सटेंशन

पुनरावर्ती परिभाषाएँ

टाइपिंग नियम

परिणाम

ओवरलोडिंग

उच्च-ऑर्डर टाइप

उपटाइपिंग

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories