आश्रित प्रकार

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

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

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

इतिहास

1934 में, हास्केल करी ने देखा कि टाइप किए गए लैम्ब्डा कैलकुलस में उपयोग किए जाने वाले प्रकार, और इसके संयोजन तर्क प्रतिरूप में, प्रस्तावक कलन में स्वयंसिद्धों के समान पैटर्न का पालन किया। आगे जाकर, तर्क में प्रत्येक प्रमाण के लिए, प्रोग्रामिंग भाषा में एक मिलान कार्य (शब्द) था। करी के उदाहरणों में से एक केवल टाइप किए गए लैम्ब्डा कैलकुस और अंतर्ज्ञानवादी तर्क के बीच पत्राचार था।Cite error: Closing </ref> missing for <ref> tag^{[full citation needed]} अधिक ठोस उदाहरण के लिए, लेना $A$ फिर से 0 से 255 तक अहस्ताक्षरित पूर्णांकों के परिवार के बराबर होना, और $B (a)$ फिर से बराबर होना $X a$ 256 और मनमानी के लिए $X a$ , तब ${\textstyle \sum _{x:A}B(x)}$ योग में जाता है $X 0 + X 1 + X 2 + ... + X 253 + X 254 + X 255$ उन्हीं कारणों से जो आश्रित फलन के कोडोमेन का हुआ।

अस्तित्वगत परिमाणीकरण के रूप में उदाहरण

होने देना $A:{\mathcal {U}}$ किसी प्रकार का हो, और रहने दो $B:A\to {\mathcal {U}}$ . करी-हावर्ड पत्राचार द्वारा, $B$ के संदर्भ में एक तार्किक विधेय (गणितीय तर्क) के रूप में व्याख्या की जा सकती है $A$ . किसी प्रदत्त के लिए $a:A$ , चाहे प्रकार हो $B (a)$ बसा हुआ है इंगित करता है कि क्या $a$ इस विधेय को संतुष्ट करता है। पत्राचार को अस्तित्वगत परिमाणीकरण और आश्रित जोड़े तक बढ़ाया जा सकता है: प्रस्ताव $\exists {a}{\in }A\,B(a)$ सत्य है अगर और केवल अगर प्रकार ${\textstyle \sum _{a:A}B(a)}$ आबाद है।

उदाहरण के लिए, $m:\mathbb {N}$ से कम या बराबर है $n:\mathbb {N}$ यदि और केवल यदि कोई अन्य प्राकृतिक संख्या मौजूद है $k:\mathbb {N}$ ऐसा है कि $m + k = n$ . तर्क में, यह कथन अस्तित्वगत परिमाणीकरण द्वारा संहिताबद्ध है:

m\leq n\iff \exists {k}{\in }\mathbb {N} \,m+k=n.

यह प्रस्ताव निर्भर जोड़ी प्रकार से मेल खाता है:

\sum _{k:\mathbb {N} }m+k=n.

अर्थात् इस कथन का प्रमाण है कि

m

से कम या बराबर है

n

एक जोड़ी है जिसमें एक गैर-ऋणात्मक संख्या दोनों होती है

k

, जो बीच का अंतर है

m

और

n

, और समानता का प्रमाण

m + k = n

.

लैम्ब्डा घन के सिस्टम

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

प्रथम क्रम आश्रित प्रकार सिद्धांत

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

दूसरे क्रम पर निर्भर प्रकार का सिद्धांत

प्रणाली $\lambda \Pi 2$ दूसरे क्रम के आश्रित प्रकार से प्राप्त किया जाता है $\lambda \Pi$ टाइप कंस्ट्रक्टर्स पर परिमाणीकरण की अनुमति देकर। इस सिद्धांत में निर्भर उत्पाद ऑपरेटर दोनों को शामिल करता है $\to$ बस टाइप किए गए लैम्ब्डा कैलकुस के ऑपरेटर और $\forall$ सिस्टम एफ की बाइंडर।

उच्च क्रम निर्भर रूप से टाइप किए गए बहुरूपी लैम्ब्डा कैलकुलस

उच्च आदेश प्रणाली $\lambda \Pi \omega$ फैली $\lambda \Pi 2$ लैम्ब्डा क्यूब से अबास्ट्रक्शन के सभी चार रूपों के लिए: शब्दों से शब्दों तक, प्रकार से प्रकार, शब्दों से प्रकार और प्रकार से शर्तों तक कार्य करता है। प्रणाली निर्माणों की गणना से मेल खाती है जिसका व्युत्पन्न, आगमनात्मक निर्माणों की गणना Coq की अंतर्निहित प्रणाली है।

एक साथ प्रोग्रामिंग भाषा और तर्क

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