View source for प्रकार सिद्धांत

{{short description|Concept in mathematical logic}}
गणित, तर्क और कंप्यूटर विज्ञान में,  '''प्ररूप सिद्धांत''' एक विशिष्ट प्रकार की प्रणाली की औपचारिक प्रस्तुति है, और सामान्य  प्ररूप सिद्धांत में  प्ररूप प्रणालियों का अकादमिक अध्ययन है। कुछ  प्ररूप सिद्धांत को गणित की आधार  के रूप में स्थापित करने के विकल्प के रूप में कार्य करते हैं। आधार  के रूप में प्रस्तावित दो प्रभावशाली  प्ररूप सिद्धांत अलोंजो चर्च के टाइप किए गए λ-गणना और प्रति मार्टिन-लोफ के अंतर्ज्ञानवादी  प्ररूप सिद्धांत हैं। अधिकांश कम्प्यूटरीकृत प्रमाण-लेखन प्रणालियाँ अपनी आधार  के लिए एक  प्ररूप सिद्धांत का उपयोग करती हैं।  सामान्य  थिएरी कोक्वांड की आगमनात्मक निर्माण की गणना है।

== इतिहास ==
{{Main|: प्रकार सिद्धांत का इतिहास}}

सहज समुच्चय सिद्धान्त और [[औपचारिक तर्क]] के आधार पर एक गणितीय आधार  में एक विरोधाभास से बचने के लिए  प्ररूप सिद्धांत बनाया गया था। बर्ट्रेंड रसेल द्वारा खोजा गया रसेल का विरोधाभास सम्मिलित था क्योंकि एक समुच्चय को "सभी संभव समुच्चयों" का उपयोग करके परिभाषित किया जा सकता था जिसमें वे स्वयं सम्मिलित थे। बर्ट्रेंड रसेल ने 1902 और 1908 के बीच, समस्या को सही करने के लिए विभिन्न " प्ररूप सिद्धांत" प्रस्तावित किए। 1908 तक रसेल एक "अपचेयता-अभिगृहीत" के साथ "प्रचलित"  प्ररूप सिद्धांत पर पहुंचे, जिनमें से दोनों को व्हाइटहेड और रसेल के प्रिंसिपिया मैथेमेटिका में प्रमुखता से 1910 और 1913 के बीच प्रकाशित किया गया था। इस प्रणाली ने प्रकार के पदानुक्रम बनाकर और फिर प्रत्येक मूर्त गणितीय इकाई को एक प्रकार निर्दिष्ट करके रसेल के विरोधाभास से बचा लिया। किसी दिए गए प्रकार की इकाइयाँ विशेष रूप से उस प्रकार के उपप्रकारों से निर्मित होती है,{{efn|name=JuliaSample|1= In [[Julia (programming language)|Julia]]'s type system, for example, abstract types have no subtype<ref name=juliaSample >Balbaert, Ivo (2015) ''Getting Started With Julia Programming'' ISBN 978-1-78328-479-5</ref>{{rp|110}} but concrete types are provided for "[[Julia_(programming_language)#Language_features|documentation, optimization, and dispatch]]".<ref name=juliaTypes >docs.julialang.org [https://docs.julialang.org/en/v1/manual/types/ v.1 Types] </ref>}} इस प्रकार किसी इकाई को स्वयं का उपयोग करके परिभाषित करने से रोकती हैं। रसेल के  प्ररूप सिद्धांत ने स्वयं को  समूह के सदस्य होने की संभावना को अस्वीकृत कर दिया।

तर्क में प्रकारों का हमेशा उपयोग नहीं किया जाता था। रसेल के विरोधाभास से बचने के लिए अन्य तकनीकें भी थीं।<ref name= sepErp>''Stanford Encyclopedia of Philosophy'' [https://plato.stanford.edu/entries/russell-paradox/#ERP (rev. Mon Oct 12, 2020) Russell’s Paradox] 3. Early Responses to the Paradox</ref> एक विशेष तर्क, अलोंजो चर्च के लैम्ब्डा कैलकुलस के साथ प्रयोग किए जाने पर प्रकारों ने अधिकार प्राप्त किया।

सबसे प्रसिद्ध प्रारंभिक उदाहरण चर्च का टाइप किया गया लैम्ब्डा गणना है। चर्च के प्रकारों का सिद्धांत<ref name="church">{{cite journal |author-link=Alonzo Church |first=Alonzo  |last=Church |title=A formulation of the simple theory of types |journal=The Journal of Symbolic Logic |volume=5 |issue=2 |pages=56–68 |year=1940 |doi=10.2307/2266170 |jstor=2266170|s2cid=15889861 }}</ref> औपचारिक प्रणाली को क्लेन -रॉसर विरोधाभास से बचने में सहायता की जो मूल अप्रकाशित लैम्ब्डा गणना से  प्रभावित था। चर्च ने प्रदर्शित किया कि यह गणित की आधार  के रूप में काम कर सकता है और इसे उच्च-क्रम के तर्क के रूप में संदर्भित किया गया था।

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

== परिचय ==

कई प्रकार के प्ररूप सिद्धांत हैं, जो एक व्यापक वर्गीकरण का निर्माण करना कठिन बनाते हैं, यह लेख एक संपूर्ण वर्गीकरण नहीं है। जो कुछ प्रकार के सिद्धांत से अपरिचित हैं, उनके लिए एक उपक्रम है, जिसमें कुछ प्रमुख दृष्टिकोण सम्मिलित हैं।

=== मूल तत्व ===

==== नियम और प्रकार ====

प्ररूप सिद्धांत में, प्रत्येक शब्द का एक प्रकार होता है। एक शब्द और इसके प्रकार को प्रायः "शब्द: प्रकार" के रूप में एक साथ लिखा जाता है।  प्ररूप सिद्धांत में सम्मिलित करने के लिए एक सामान्य प्रकार [[प्राकृतिक संख्या]] है, जिसे प्रायः "<math>\mathbb N</math><nowiki>''</nowiki> or "nat" लिखा जाता है। दूसरा बूलियन तर्क मान है। तो, उनके प्रकारों के साथ कुछ बहुत ही सरल शब्द है

* 1 : nat
* 42 : nat
* true : bool

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

* add 0 0 : nat
*add 2 3 : nat 
*add 1 (add 1 (add 1 0)) : nat

अंतिम अवधि में, संक्रिया के क्रम को इंगित करने के लिए कोष्ठक जोड़े गए थे। तकनीकी रूप से, अधिकांश प्रकार के सिद्धांतों को कोष्ठक को प्रत्येक संक्रिया के लिए सम्मिलित होने की आवश्यकता होती है, लेकिन, व्यवहार में, वे नहीं लिखे जाते हैं और लेखक मानते हैं कि पाठक यह जानने के लिए पूर्वता और सहयोगी का उपयोग कर सकते हैं कि वे कहां हैं। इसी तरह की आसानी के लिए, <math>x + y</math> के अतिरिक्त <math>x</math> <math>y</math> लिखना एक सामान्य संकेत है। इसलिए, उपरोक्त शर्तों को पुनः  लिखा जा सकता है:

* 0 + 0: nat
* 2 + 3: nat
* 1 + (1 + (1 + 0)): nat

शर्तों में चर भी सम्मिलित हो सकते हैं। चर में हमेशा एक प्ररूप होता है। इसलिए, "x" और "y" को "nat" प्रकार के चर मानते हुए, निम्नलिखित भी मान्य शब्द हैं:

* x: nat
* x + 2: NAT
* x + (x + y): NAT

"नेट" और "बूल" से अधिक प्रकार हैं। हम पहले ही "योग" शब्द देख चुके हैं, जो "नेट" नहीं है, लेकिन एक फलन है, जब दो "नेट" पर लागू किया जाता है, तो "नेट" की गणना होती है। "योग" के प्रकार को बाद में आवृत किया जाएगा। सबसे पहले, हमें "गणना" का वर्णन करने की आवश्यकता है।

==== गणना ====

प्ररूप सिद्धांत में गणना का एक अंतर्निहित संकेतन है। निम्नलिखित शर्तें सभी अलग हैं

* 1 + 4: nat
* 3 + 2: nat
* 0 + 5: nat

लेकिन वे सभी शब्द 5:  nat की गणना करते हैं। प्ररूप सिद्धांत में,हम गणना को संदर्भित करने के लिए "कमी" और "कम" शब्दों का उपयोग करते हैं। तो, हम कहते हैं कि 0 + 5: NAT 5: NAT तक कम हो जाता है। इसे 0 + 5: NAT  <math>\twoheadrightarrow</math> 5:  nat लिखा जा सकता है। गणना यांत्रिक है, शब्द के रचनाक्रम को पुनः लिखकर पूरा किया गया है।

जिन शर्तों में चर होते हैं उन्हें भी कम किया जा सकता है। तो शर्त "x + (1 + 4): nat" "x + 5: nat" को कम कर देता है। (हम चर्च-रॉसर प्रमेय के कारण किसी भी उप-पद को एक पद के अंदर कम कर सकते हैं।)

बिना किसी चर के एक शर्त जिसे अधिक कम नहीं किया जा सकता है, एक "विहित शर्त" है। उपरोक्त सभी शर्तें "5: nat" तक कम हो जाती हैं, जो कि एक प्रामाणिक शब्द है। प्राकृतिक संख्याओं की विहित शर्तें हैंː

* 0:  nat
* 1:  nat
* 2:  nat
* आदि।

स्पष्टतः, एक ही पद के लिए गणना करने वाले पद समान होते हैं। तो, "x: nat" मानते हुए, "x + (1 + 4) : nat" और "x + (4 + 1) : nat" पद समान हैं क्योंकि वे दोनों "x + 5: nat" तक कम हो जाते हैं। जब दो पद समान होते हैं, तो उन्हें एक दूसरे के लिए प्रतिस्थापित किया जा सकता है। समानता  प्ररूप सिद्धांत में एक जटिल विषय है और कई प्रकार के समानता हैं। इस तरह की समानता, जहाँ दो पद एक ही पद के लिए संगणित होते हैं, "न्यायिक समानता" कहलाती है।

=== फलन ===

प्ररूप सिद्धांत में, फलन पद हैं। फलन या तो लैम्ब्डा शर्तें हो सकते हैं या "नियम द्वारा" परिभाषित किए जा सकते हैं।

==== लैम्ब्डा शर्तें ====

एक लैम्ब्डा शब्द जैसा दिखता है (λ variablename: Type1। शब्द) और टाइप टाइप 1 है <math>\to</math> टाइप 2।टाइप टाइप 1 <math>\to</math> टाइप 2 इंगित करता है कि लैम्ब्डा शब्द एक फलन है जो टाइप टाइप 1 का एक पैरामीटर लेता है और टाइप टाइप 2 के शब्द की गणना करता है।लैम्ब्डा शब्द के अंदर का शब्द टाइप 2 का एक मान होना चाहिए, यह मानते हुए कि वेरिएबल में टाइप 1 है।

एक लैम्ब्डा शब्द का एक उदाहरण यह कार्य है जो अपने तर्क को दोगुना करता है:

* (λ x: nat। (x x जोड़ें)): nat <math>\to</math> नेट

चर नाम x है और चर में NAT प्रकार है।शब्द (X X जोड़ें) में NAT है, X: NAT मानते हुए।इस प्रकार, लैम्ब्डा शब्द का प्रकार NAT है <math>\to</math>  nat, जिसका अर्थ है कि यदि इसे एक तर्क के रूप में एक NAT दिया जाता है, तो यह एक NAT की गणना करेगा।कमी (a.k.a गणना) को लैम्ब्डा शर्तों के लिए परिभाषित किया गया है।जब फलन लागू किया जाता है (a.k.a. कहा जाता है), तो तर्क पैरामीटर के लिए प्रतिस्थापन (बीजगणित) होता है।

इससे पहले, हमने देखा कि फलन अनुप्रयोग को फलन टर्म के बाद पैरामीटर लगाकर लिखा गया है।इसलिए, यदि हम उपरोक्त फलन को NAT के पैरामीटर 5 के साथ  संकेत करना चाहते हैं, तो हम लिखते हैं:

* (λ x: nat। (x x जोड़ें)) 5: nat

लैम्ब्डा शब्द टाइप  nat था <math>\to</math>  nat, जिसका मतलब था कि एक तर्क को एक तर्क के रूप में दिया गया, यह प्रकार NAT का एक शब्द का उत्पादन करेगा।चूंकि हमने इसे तर्क 5 दिया है, उपरोक्त शब्द में NAT है।कमी शब्द में पैरामीटर x के लिए तर्क 5 को प्रतिस्थापित करके काम करता है (एक्स एक्स जोड़ें), इसलिए शब्द की गणना:

* (5 5 जोड़ें): नेट

जो स्पष्ट रूप से गणना करता है

* 10:  nat

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

* डबल:  nat <math>\to</math> nat :: = (λ x: nat। (x x जोड़ें))

यह ऊपर जैसा ही कार्य है, इसे लिखने का एक अलग तरीका है।तो शब्द

* डबल 5:  nat

अभी भी गणना करता है

* 10:  nat

==== आश्रित टाइपिंग ====

आश्रित टाइपिंग तब होती है जब किसी फलन द्वारा लौटा दिया जाता है, वह उसके तर्क के मूल्य पर निर्भर करता है।उदाहरण के लिए, जब एक  प्ररूप सिद्धांत में एक नियम होता है जो प्रकार के बूल को परिभाषित करता है, तो यह फलन को भी परिभाषित करता है।फलन यदि 3 तर्क लेते हैं और यदि सही b c B की गणना करता है और यदि FALSE B C C की गणना करता है।लेकिन यदि बी सी का प्रकार है तो क्या है?

यदि B और C का एक ही प्रकार है, तो यह स्पष्ट है: यदि B C का B और C के समान ही है।इस प्रकार, एक: बूल मानते हुए,

* यदि एक 2 4:  nat
* यदि एक झूठा सच: बूल

लेकिन यदि बी और सी के अलग -अलग प्रकार होते हैं, तो बी सी के मूल्य पर निर्भर करता है।हम प्रतीक & pi का उपयोग करते हैं;एक फलन को इंगित करने के लिए जो एक तर्क लेता है और एक प्रकार देता है।यह मानते हुए कि हमारे पास कुछ प्रकार हैं और सी और ए: बूल, बी: बी और सी: सी, फिर

* यदि a b c: (& pi; a: बूल। b। <math>\to</math> C <math>\to</math> यदि ए बी सी)

यही है, IF शब्द का प्रकार या तो दूसरे या तीसरे तर्क का प्रकार है, जो पहले तर्क के मूल्य पर निर्भर करता है।वास्तविकता में, यदि A B C को IF का उपयोग करके परिभाषित नहीं किया गया है, लेकिन यह विवरण में इस परिचय के लिए बहुत जटिल हो जाता है।

क्योंकि प्रकार में गणना हो सकती है, निर्भर टाइपिंग आश्चर्यजनक रूप से शक्तिशाली है।जब गणितज्ञों का कहना है कि एक संख्या सम्मिलित है <math>x</math> ऐसा है कि <math>x</math> प्राइम है या एक नंबर सम्मिलित है <math>x</math> ऐसी गुण <math>P(x)</math> होल्ड्स, इसे एक आश्रित प्रकार के रूप में व्यक्त किया जा सकता है।अर्थात्, गुण विशिष्ट के लिए सिद्ध होती है<math>x</math>और यह परिणाम के प्रकार में दिखाई देता है।

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

==== ब्रह्मांड ====

& Pi; -टर्म्स एक प्रकार लौटाते हैं।तो उनके रिटर्न वैल्यू का प्रकार क्या है?खैर, एक प्रकार होना चाहिए जिसमें प्रकार हों।एक प्रकार जिसमें अन्य प्रकार होते हैं, को एक ब्रह्मांड (गणित) कहा जाता है।यह प्रायः प्रतीक के साथ लिखा जाता है <math>U</math>।कभी -कभी ब्रह्मांड का एक पदानुक्रम होता है, साथ<math>U_0</math> : <math>U_1</math>,<math>U_1</math> : <math>U_2</math>, वगैरह..

यदि एक ब्रह्मांड में स्वयं होता है, तो यह गिरार्ड के विरोधाभास जैसे विरोधाभासों को जन्म दे सकता है। गिरार्ड का विरोधाभास।

उदाहरण के लिए:<ref>{{cite journal |last1=Rathjen |first1=Michael |date=October 2005 |title=The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory |url=https://link.springer.com/article/10.1007/s11229-004-6208-4 |journal=Synthese |volume=147 |pages=81–120 |doi=10.1007/s11229-004-6208-4 |s2cid=143295 |access-date=September 21, 2022}}</ref>

{{quote|मार्टिन-लोफ प्रकार के सिद्धांत का खुलापन विशेष रूप से तथाकथित  विश्व समष्टि के परिचय में प्रकट होता है। प्रारूप के विश्व समष्टि प्रतिबिंब की अनौपचारिक धारणा को समाहित करते हैं जिनकी भूमिका को निम्नानुसार समझाया जा सकता है। प्रारूप सिद्धांत के एक विशेष औपचारिकता के विकास के समय, प्रारूप सिद्धांतवादी प्रारूप के नियमों पर वापस देख सकते हैं, कहते हैं, C जिन्हें अब तक प्रस्तुत किया गया है और यह पहचानने के चरण का प्रदर्शन करता है कि वे मार्टिन-लोफ के अर्थ व्याख्या के अनौपचारिक शब्दार्थ के अनुसार मान्य हैं। यह 'आत्मनिरीक्षण' का कार्य उन अवधारणाओं से अवगत होने का एक प्रयास है जो अतीत में हमारे निर्माणों को नियंत्रित करती रही हैं। यह एक "प्रतिबिंब सिद्धांत को उत्पन्न करता है सामान्य रूप से  हम जो कुछ भी करने के लिए प्रवृत  हैं वह एक विश्व समष्टि (मार्टिन-लोफ 1975, 83) के अंदर किया जा सकता है" । औपचारिक स्तर पर, यह प्रारूप सिद्धांत के सम्मिलित औपचारिकता के विस्तार की ओर जाता है जिसमें C को प्रारूप बनाने की क्षमता एक प्रकार के  विश्व समष्टि UC प्रतिबिंब C में स्थापित हो जाती है।}}


=== नियम नियमों और शर्तों द्वारा सामान्य ===

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

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

==== [[खाली प्रकार]] ====

खाली प्रकार की कोई शर्तें नहीं हैं।प्रकार सामान्य रूप से लिखा जाता है<math>\bot</math>या<math>\mathbb 0</math>।

इसका उपयोग यह दिखाने के लिए किया जाता है कि कुछ अस्वीकार्य है।यदि एक प्रकार ए के लिए, आप टाइप ए का एक फलन बना सकते हैं <math>\to \bot</math>, आप जानते हैं कि ए की कोई शर्त नहीं है।टाइप ए के लिए एक उदाहरण हो सकता है एक संख्या सम्मिलित है <math>x</math> ऐसा दोनों <math>x</math> यहां तक कि और है <math>x</math> अजीब है ।(उदाहरण A का निर्माण कैसे किया जाता है, इसके लिए नीचे उत्पाद प्रकार देखें।) जब किसी प्रकार की कोई शर्तें नहीं हैं, तो हम कहते हैं कि यह निर्जन है।

==== इकाई प्रकार ====

यूनिट प्रकार में बिल्कुल 1 विहित शब्द है।प्रकार लिखा है<math>\top</math>या<math>\mathbb 1</math>और एकल विहित शब्द लिखा गया है *।

यूनिट प्रकार का उपयोग यह दिखाने के लिए किया जाता है कि कुछ सम्मिलित है या कम्प्यूटेशनल है।यदि एक प्रकार ए के लिए, आप प्रकार का एक फलन बना सकते हैं<math>\top \to</math> ए, आप जानते हैं कि ए में एक या एक से अधिक शब्द हैं।जब किसी प्रकार का कम से कम 1 शब्द होता है, तो हम कहते हैं कि यह बसा हुआ है।

==== बूलियन प्रकार ====

बूलियन प्रकार में ठीक 2 विहित शब्द हैं।प्रकार सामान्य रूप से बूल लिखा जाता है या<math>\mathbb B</math>या<math>\mathbb 2</math>।विहित शब्द सामान्य रूप से सही और झूठे होते हैं।

बूलियन प्रकार को एक एलिमिनेटर फलन के साथ परिभाषित किया गया है यदि ऐसा है:

* यदि सच बी सी <math>\twoheadrightarrow</math> बी
* यदि झूठी बी सी <math>\twoheadrightarrow</math> सी

==== उत्पाद प्रकार ====

उत्पाद प्रकार में ऐसे शब्द होते हैं जिन्हें जोड़ी का आदेश दिया जाता है।प्रकार ए और बी के लिए, उत्पाद प्रकार लिखा जाता है <math>\times</math> बी ।कंस्ट्रक्टर फलन जोड़ी द्वारा कैनोनिकल शब्द बनाए जाते हैं।शब्द एक बी हैं, जहां ए टाइप ए का एक शब्द है और बी टाइप बी का एक शब्द है।उत्पाद प्रकार को पहले और दूसरे कार्य के साथ परिभाषित किया गया है जैसे:

* पहला (जोड़ी ए बी) <math>\twoheadrightarrow</math> ए
* दूसरा (जोड़ी ए बी) <math>\twoheadrightarrow</math> बी

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

यदि एक  प्ररूप सिद्धांत में निर्भर टाइपिंग है, तो इसमें निर्भर प्रकार है।एक आश्रित जोड़ी में, दूसरा प्रकार पहले शब्द के मान पर निर्भर करता है।इस प्रकार, प्रकार लिखा है<math>\Sigma</math> A: a।B (a) जहाँ b में टाइप A है <math>\to</math> यू।यह उपयोगी है जब गुण बी (ए) के साथ ए की अस्तित्वगत मात्रा का ठहराव दिखाते हैं।

==== योग प्रकार ====

योग प्रकार एक टैग किया गया संघ है।अर्थात्, A और B प्रकारों के लिए, टाइप A + B या तो टाइप A या टाइप B का शब्द है और यह जानता है कि यह कौन सा है।प्रकार कंस्ट्रक्टर्स इंजेक्शनलफ्ट और इंजेक्शनराइट के साथ आता है। संकेत इंजेक्शनल ए: ए: ए और टाइप ए + बी का एक विहित शब्द लौटाता है।इसी तरह, इंजेक्शनराइट B B: B: B और टाइप A + B का एक विहित शब्द लौटाता है।टाइप को एक एलिमिनेटर फलन मैच के साथ परिभाषित किया गया है जैसे कि एक प्रकार C और फलन F: A के लिए <math>\to</math> सी और जी: बी <math>\to</math> सी :

* मैच (इंजेक्शनलफ्ट ए) सी एफ जी <math>\twoheadrightarrow</math> (च ए)
* मैच (इंजेक्शनराइट बी) सी एफ जी <math>\twoheadrightarrow</math> (जी बी)

योग प्रकार का उपयोग [[तार्किक या]] संघ (समुच्चय सिद्धान्त) के लिए किया जाता है।

==== प्राकृतिक संख्या ====

प्राकृतिक संख्या सामान्य रूप से मीनो अंकगणित की शैली में लागू की जाती है।एक विहित शब्द है, 0:  nat फॉर शून्य।शून्य से बड़ा कैनोनिकल मान कंस्ट्रक्टर फलन का उपयोग करें: NAT <math>\to</math>  nat।इस प्रकार, s 0 एक है।S (S 0) दो है।S (S 0))) तीन है।आदि दशमलव संख्या केवल उन शर्तों के बराबर है।

* 1: nat :: = s 0
* 2: nat :: = s (s 0)
* 3: nat :: = s (s (s 0))
* ...

प्राकृतिक संख्याओं को एक एलिमिनेटर फलन R के साथ परिभाषित किया गया है जो सभी NATs के लिए एक फलन को परिभाषित करने के लिए पुनरावृत्ति का उपयोग करता है।यह एक फलन P: NAT लेता है <math>\to</math> यू जो परिभाषित करने के लिए फलन का प्रकार है।यह एक शब्द PZ: P 0 भी लेता है जो शून्य पर मान है और एक फलन PS: P n <math>\to</math> P (s n) जो कहता है कि N + 1 पर मान को मान में मान को कैसे बदलना है।इस प्रकार, इसके गणना नियम हैं:

* R p pz ps 0 <math>\twoheadrightarrow</math> पेज
* R p pz ps (s <math>n</math>) <math>\twoheadrightarrow</math> पीएस (आर पी पीजेड पीएस <math>n</math>)

फलन ऐड, जिसका उपयोग पहले किया गया था, को आर का उपयोग करके परिभाषित किया जा सकता है।

* जोड़ें:  nat<math>\to</math>नेट<math>\to</math>रात :: = आर (λ एन: रात। रात<math>\to</math>nat) (λ n: nat। n) (λ g: nat<math>\to</math> nat।(λ एम:  nat। एस (जी एम))

{{anchor|Equality types}}


==== पहचान प्रकार ====

पहचान प्रकार  प्ररूप सिद्धांत में समानता की तीसरी अवधारणा है।पहला उल्लेखनीय समानता है, जो 2: nat :: = (s 0)) जैसी परिभाषाओं के लिए है, जिसका कोई गणितीय अर्थ नहीं है, लेकिन पाठकों के लिए उपयोगी है।दूसरा निर्णय समानता है, जो तब होता है जब दो शब्द एक ही शब्द की गणना करते हैं, जैसे कि x + (1 + 4) और x + (4 + 1), जो दोनों x + 5 से गणना करते हैं।लेकिन  प्ररूप सिद्धांत को समानता के एक और रूप की आवश्यकता होती है, जिसे पहचान प्रकार या प्रस्ताव समानता के रूप में जाना जाता है।

इसका कारण पहचान प्रकार की आवश्यकता है क्योंकि कुछ समान शब्द एक ही शब्द की गणना नहीं करते हैं।X: NAT, शर्तों को X + 1 और 1 + x एक ही शब्द की गणना नहीं करते हैं।याद रखें कि + फलन ऐड के लिए एक संकेतन है, जो फलन r के लिए एक संकेतन है।हम आर पर तब तक गणना नहीं कर सकते हैं जब तक कि एक्स के लिए मूल्य निर्दिष्ट नहीं किया जाता है और, जब तक कि यह निर्दिष्ट नहीं किया जाता है, आर के लिए दो अलग -अलग  संकेत एक ही शब्द की गणना नहीं करेंगे।

एक पहचान प्रकार के लिए एक ही प्रकार के दो शब्दों को और बी की आवश्यकता होती है और इसे ए = बी लिखा जाता है।तो, x + 1 और 1 + x के लिए, प्रकार x + 1 = 1 + x होगा।कंस्ट्रक्टर रिफ्लेक्सिटी के साथ कैनोनिकल शब्द बनाए जाते हैं। संकेत रिफ्लेक्सिटी ए एक शब्द ए लेता है और टाइप ए = ए का एक विहित शब्द लौटाता है।

पहचान प्रकार के साथ गणना एलिमिनेटर फलन j के साथ की जाती है।फलन j एक शब्द को A, B, और टाइप A = B के एक शब्द पर पुनः लिखा जाना देता है ताकि B को A द्वारा प्रतिस्थापित किया जाए।जबकि J एक दिशात्मक है, केवल B के साथ B को स्थानापन्न करने में सक्षम है, यह साबित किया जा सकता है कि पहचान प्रकार [[रिफ्लेक्सिटिविटी प्रॉपर्टी]], सममित गुण और सकर्मक गुण है।

यदि विहित शब्द हमेशा A = A और X+1 होते हैं, तो 1+x के समान शब्द की गणना नहीं करते हैं, हम x+1 = 1+x का एक शब्द कैसे बनाते हैं?हम आर फलन का उपयोग करते हैं।(ऊपर प्राकृतिक संख्याएं देखें।) R फलन का तर्क P को परिभाषित किया गया है (λ x: nat। X+1 = 1+x)।अन्य तर्क एक इंडक्शन प्रमाण के कुछ हिस्सों की तरह काम करते हैं, जहां PZ: P 0 बेस केस 0+1 = 1+0 और PS: P n बन जाता है <math>\to</math> P (s n) आगमनात्मक स्थिति बन जाता है।अनिवार्य रूप से, यह कहता है कि जब x+1 = 1+x को X को एक विहित मूल्य से बदल दिया जाता है, तो अभिव्यक्ति रिफ्लेक्सिटी (x+1) के समान होगी।फलन R के इस अनुप्रयोग में टाइप X: NAT है <math>\to</math> x+1 = 1+x।हम इसका उपयोग कर सकते हैं और फलन j को किसी भी शब्द में x+1 के लिए 1+x प्रतिस्थापित करने के लिए।इस तरह, पहचान प्रकार समानता को पकड़ने में सक्षम है जो निर्णय समानता के साथ संभव नहीं है।

स्पष्ट होने के लिए, टाइप 0 = 1 बनाना संभव है, लेकिन उस प्रकार की शर्तों को बनाने का कोई तरीका नहीं होगा।टाइप 0 = 1 के शब्द के बिना, किसी अन्य शब्द में 1 के लिए 0 के विकल्प के लिए फलन j का उपयोग करना संभव नहीं होगा।

प्ररूप सिद्धांत में समानता की जटिलताएं इसे एक सक्रिय अनुसंधान क्षेत्र बनाती हैं, होमोटॉपी  प्ररूप सिद्धांत देखें।

==== आगमनात्मक प्रकार ====

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

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

(नोट:  प्ररूप सिद्धांत में सामान्य रूप से [[समावेश]] सम्मिलित नहीं होता है। वे एक अनंत डेटा प्रकार का प्रतिनिधित्व करते हैं और अधिकांश  प्ररूप सिद्धांत खुद को उन कार्यों तक सीमित करते हैं जो रुकने के लिए साबित हो सकते हैं।)

== समुच्चय सिद्धान्त से अंतर ==

गणित के लिए पारंपरिक फाउंडेशन को एक तर्क के साथ जोड़ा गया सिद्धांत निर्धारित किया गया है।सबसे सामान्य एक उद्धृत Zermelo -Fraenkel समुच्चय सिद्धान्त है, जिसे ZF के रूप में जाना जाता है या, पसंद के [[स्वयंसिद्ध|अभिगृहीत]], ZFC के साथ। प्ररूप सिद्धांत इस आधार  से कई तरीकों से भिन्न होते हैं।

* समुच्चय सिद्धान्त में अनुमान और अभिगृहीत दोनों ही नियम हैं, जबकि प्रकार के सिद्धांतों में केवल नियम हैं।समुच्चय सिद्धान्त तर्क के शीर्ष पर बनाए गए हैं।इस प्रकार, ZFC को प्रथम-क्रम लॉजिक और Zermelo-fraenkel_set_stheory#Axioms के दोनों नियमों द्वारा परिभाषित किया गया है।(एक अभिगृहीत एक तार्किक व्युत्पत्ति के बिना सच के रूप में स्वीकार किया जाता है।)  प्ररूप सिद्धांत, सामान्य रूप से, अभिगृहीत नहीं होते हैं और उनके नियमों के नियमों द्वारा परिभाषित होते हैं।
* समुच्चय  उपागम और लॉजिक में बाहर किए गए मध्य का नियम है।अर्थात्, हर प्रमेय सच या गलत है।जब एक   प्ररूप सिद्धांत और या या के रूप में अवधारणाओं को परिभाषित करता है, तो यह [[अंतर्ज्ञानवादी तर्क]] की ओर जाता है, जिसमें बाहर किए गए मध्य का कानून नहीं है।हालांकि, कानून कुछ प्रकार के लिए सिद्ध किया जा सकता है।
* समुच्चय सिद्धान्त में, एक तत्व एक समुच्चय तक सीमित नहीं है।तत्व अन्य समुच्चयों के साथ उप-समुच्चय और यूनियनों में दिखाई दे सकता है। प्ररूप सिद्धांत में, शब्द (सामान्य रूप से) केवल एक प्रकार से संबंधित हैं।जहां एक उप-समुच्चय का उपयोग किया जाएगा,  प्ररूप सिद्धांत एक विधेय ([[गणितीय तर्क)]] का उपयोग कर सकता है या एक निर्भर-टाइप उत्पाद प्रकार का उपयोग कर सकता है, जहां प्रत्येक तत्व <math>x</math> एक सबूत के साथ जोड़ा जाता है कि उप-समुच्चय की गुण के लिए है <math>x</math>।जहां एक संघ का उपयोग किया जाएगा,  प्ररूप सिद्धांत योग प्रकार का उपयोग करता है, जिसमें नए विहित शब्द सम्मिलित हैं।
* प्ररूप सिद्धांत में गणना की एक अंतर्निहित धारणा है।इस प्रकार, 1+1 और 2  प्ररूप सिद्धांत में अलग -अलग शब्द हैं, लेकिन वे एक ही मूल्य की गणना करते हैं।इसके अतिरिक्त, कार्यों को कम्प्यूटेशनल रूप से लैम्ब्डा शर्तों के रूप में परिभाषित किया गया है।समुच्चय सिद्धान्त में, 1+1 = 2 का अर्थ है कि 1+1 मान 2 को संदर्भित करने का सिर्फ एक और तरीका है। प्ररूप सिद्धांत की गणना में समानता की एक जटिल अवधारणा की आवश्यकता होती है।
* समुच्चय सिद्धान्त सामान्य रूप से समुच्चय के रूप में संख्याओं को एन्कोड करता है।।कंस्ट्रक्टर्स 0 और एस द्वारा बनाई गई आगमनात्मक प्रकार से बारीकी से मीनो स्वयंसिद्धों से मिलते -जुलते हैं | पीनो के अभिगृहीत।
* समुच्चय  उपागम में समुच्चय-बिल्डर नोटेशन है।यह कोई भी समुच्चय बना सकता है जिसे परिभाषित किया जा सकता है।यह इसे बेशुमार समुच्चय बनाने की अनुमति देता है। प्ररूप सिद्धांत वाक्यविन्यास हैं, जो उन्हें एक अनगढ़ अनंत शब्दों में सीमित करता है।इसके अतिरिक्त, अधिकांश प्रकार के सिद्धांतों को हमेशा रुकने और खुद को [[पुनरावर्ती भाषा]] के शब्दों में सीमित करने के लिए गणना की आवश्यकता होती है।नतीजतन, अधिकांश  प्ररूप सिद्धांत [[वास्तविक संख्या]]ओं का उपयोग नहीं करते हैं, लेकिन [[कम्प्यूटेबल नंबर]]।
* समुच्चय सिद्धान्त में, [[पसंद का स्वयंसिद्ध|पसंद का अभिगृहीत]] एक अभिगृहीत है और विवादास्पद है, खासकर जब बेशुमार समुच्चय पर लागू होता है। प्ररूप सिद्धांत में, समतुल्य कथन एक प्रमेय (प्रकार) है और साबित करने योग्य है (एक शब्द द्वारा बसा हुआ)।
* प्ररूप सिद्धांत में, प्रमाण गणितीय वस्तुएं हैं।टाइप X+1 = 1+x का उपयोग तब तक नहीं किया जा सकता जब तक कि प्रकार का शब्द न हो।यह शब्द एक प्रमाण का प्रतिनिधित्व करता है कि x+1 = 1+x।इस प्रकार,  प्ररूप सिद्धांत गणितीय वस्तुओं के रूप में अध्ययन किए जाने वाले प्रमाणों को खोलता है।

प्ररूप सिद्धांत के समर्थक भी [[BHK व्याख्या]] के माध्यम से रचनात्मक गणित के लिए अपने संबंध को इंगित करेंगे, इसके करी -आओ -आइसोमोर्फिज्म द्वारा तर्क से जुड़े, और [[श्रेणी सिद्धांत]] से इसके कनेक्शन।

== तकनीकी विवरण ==

एक   प्ररूप सिद्धांत एक [[गणितीय तर्क]] है।यह अनुमान के नियम का एक संग्रह है जो [[निर्णय (गणितीय तर्क)]] में परिणाम करता है।अधिकांश लॉजिक्स में निर्णय शब्द हैं <math>x</math> क्या सच है।या शब्द <math>x</math> एक अच्छी तरह से गठित सूत्र है।<ref>{{cite web |last1=Bauer |first1=Andrej |title=What exactly is a judgement? |url=https://mathoverflow.net/questions/254518/what-exactly-is-a-judgement |website=mathoverflow |access-date=29 December 2021}}</ref>।एक  प्ररूप सिद्धांत में अतिरिक्त निर्णय होते हैं जो प्रकारों और संबंधित शब्दों को प्रकारों तक परिभाषित करते हैं।

=== शर्तें ===

एक शब्द (तर्क) को पुनरावर्ती रूप से एक निरंतर प्रतीक, चर या एक फलन अनुप्रयोग के रूप में परिभाषित किया जाता है, जहां एक शब्द दूसरे शब्द पर लागू होता है।कुछ निरंतर प्रतीक प्राकृतिक संख्याओं में से 0 होंगे, बूलियन का सच, और एस और इफ जैसे कार्य।इस प्रकार कुछ शब्द 0, (s 0), (s x)) हैं, और यदि सत्य 0 (s 0) हैं।

=== निर्णय ===

अधिकांश प्रकार के सिद्धांतों में 4 निर्णय होते हैं:

*<math>T</math> एक प्रकार है।
*<math>t</math> प्रकार का एक शब्द है <math>T</math>।
*  प्रकार <math>T_1</math> प्रकार के बराबर है <math>T_2</math>।
*  शर्तें <math>t_1</math> और <math>t_2</math> दोनों प्रकार के हैं <math>T</math> और समान हैं।

निर्णय एक धारणा के अंतर्गत किए जा सकते हैं।इस प्रकार, हम कह सकते हैं, मानते हुए <math>x</math> 'बूल' प्रकार का एक शब्द है और <math>y</math> प्रकार का एक शब्द है, ' nat', (यदि x y y) 'NAT' प्रकार का एक शब्द है।मान्यताओं के लिए गणितीय संकेतन शब्द की एक अल्पविराम-अलग सूची है: टाइप करें जो टर्नस्टाइल (प्रतीक) से पहले है '<math>\vdash</math>'।इस प्रकार, उदाहरण कथन औपचारिक रूप से लिखा गया है:

* x: बूल, y: nat <math>\vdash</math> (यदि x y y): nat

यदि कोई धारणा नहीं है, तो टर्नस्टाइल के बाईं ओर कुछ भी नहीं होगा:

* <math>\vdash</math> S: NAT <math>\to</math> नेट

मान्यताओं की सूची को संदर्भ कहा जाता है।प्रतीक को देखना बहुत सामान्य है '<math>\Gamma</math>'कुछ या सभी मान्यताओं का प्रतिनिधित्व करने के लिए उपयोग किया जाता है।इस प्रकार, 4 अलग -अलग निर्णयों के लिए औपचारिक संकेतन सामान्य रूप से है:

{| class="wikitable"
! निर्णय के लिए औपचारिक संकेतन !! विवरण
|-
| <math>\Gamma \vdash T</math> प्रारूप || <math>T</math> क प्रकार है (धारणाओं के अंतर्गत <math>\Gamma</math>)
|-
| <math>\Gamma \vdash t : T</math> || <math>t</math> प्रकार का पद है <math>T</math> (धारणाओं के अंतर्गत <math>\Gamma</math>)
|-
| <math>\Gamma \vdash T_1 = T_2 </math> || प्रारूप <math>T_1</math> प्रारूप के समान है <math>T_2</math> (धारणाओं के अंतर्गत <math>\Gamma</math>)
|-
| <math>\Gamma \vdash t_1 = t_2 : T </math> || पद <math>t_1</math> और <math>t_2</math> दोनों प्रारूप के हैं <math>T</math> और समान है (धारणाओं के अंतर्गत <math>\Gamma</math>)
|}
(ध्यान दें: शर्तों की समानता का निर्णय वह है जहां वाक्यांश "न्यायिक समानता" आता है।)

निर्णय लागू करते हैं कि प्रत्येक पद का एक प्रकार होता है। प्रारूप प्रतिबंधित करेगा कि कौन से नियम किसी पद पर लागू किए जा सकते हैं।

=== नियम ===

प्ररूप सिद्धांत के नियम का कहना है कि अन्य निर्णयों के अस्तित्व के आधार पर क्या निर्णय लिया जा सकता है। नियमों को रेखा के ऊपर आवश्यक  निविष्‍ट निर्णयों और रेखा के नीचे परिणामी निर्णय के साथ, एक क्षैतिज रेखा का उपयोग करके व्यक्त किया जाता है। लैम्ब्डा पद बनाने का नियम है:
<math display="block">
\begin{array}{c}
\Gamma , a:A \vdash b : B \\
\hline
\Gamma \vdash ( \lambda a:A . b ) : A \to B \\
\end{array}
</math>
लैम्ब्डा शब्द बनाने के लिए आवश्यक निर्णय लाइन से ऊपर जाते हैं।इस स्थिति में, केवल एक निर्णय की आवश्यकता है।यह है कि कुछ प्रकार बी का कुछ शब्द बी है, यह मानते हुए कि कुछ प्रकार ए और कुछ अन्य मान्यताओं का कुछ शब्द है<math>\Gamma</math>।(टिप्पणी:<math>\Gamma</math>ए, ए, बी, और बी नियम में सभी [[मेटावेरियस]] हैं।) परिणामस्वरूप निर्णय लाइन से नीचे चला जाता है।इस नियम के परिणामस्वरूप निर्णय में कहा गया है कि नए लैम्ब्डा शब्द में टाइप ए है <math>\to</math> B अन्य मान्यताओं के अंतर्गत <math>\Gamma</math>।

नियम वाक्यात्मक हैं और पुनर्लेखन द्वारा काम करते हैं।इस प्रकार, metavariables की तरह<math>\Gamma</math>, ए, ए, आदि वास्तव में उन जटिल शब्दों से युक्त हो सकते हैं जिनमें कई फलन अनुप्रयोग होते हैं, न कि केवल एकल प्रतीकों को।

प्ररूप सिद्धांत में एक विशेष निर्णय उत्पन्न करने के लिए, इसे उत्पन्न करने के लिए एक नियम होना चाहिए।फिर, उस नियम के सभी आवश्यक  निविष्‍ट उत्पन्न करने के लिए नियम होने चाहिए।और फिर उन नियमों के लिए सभी  निविष्‍ट के लिए नियम।लागू नियम एक प्रमाण ट्री बनाते हैं।यह सामान्य रूप से gentzen- शैली तैयार की जाती है,<ref>{{cite web |last1=Smith |first1=Peter |title=Types of proof system |url=https://www.logicmatters.net/resources/pdfs/ProofSystems.pdf |archive-url=https://ghostarchive.org/archive/20221009/https://www.logicmatters.net/resources/pdfs/ProofSystems.pdf |archive-date=2022-10-09 |url-status=live |website=logicmatters.net |access-date=29 December 2021}}</ref> जहां लक्ष्य निर्णय (रूट) सबसे नीचे है और नियमों को शीर्ष पर किसी भी  निविष्‍ट (पत्तियों) की आवश्यकता नहीं है (प्राकृतिक कटौती#proops_and_type_theory) देखें।एक नियम का एक उदाहरण जिसमें किसी भी  निविष्‍ट की आवश्यकता नहीं होती है, वह है जो बताता है कि NAT का एक शब्द 0 है:

<math display="block">
\begin{array}{c}
\hline
\vdash 0 : nat \\
\end{array}
</math>
एक  प्ररूप सिद्धांत में सामान्य रूप से कई नियम होते हैं, जिनमें सम्मिलित हैं:

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

इसके अतिरिक्त, नियम के प्रकार के लिए, 4 अलग -अलग प्रकार के नियम हैं

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

नियमों के उदाहरण:

* [https://hott.github.io/hott-2019/images/mltt-rules.pdf नियम मार्टिन-लफ़ के अंतर्ज्ञानवादी  प्ररूप सिद्धांत]
* परिशिष्ट A.2 of [https://homotopytypetheory.org/book/ homotopy  प्ररूप सिद्धांत] पुस्तक

=== टाइप सिद्धांतों के गुण ===

शब्द सामान्य रूप से एक प्रकार के होते हैं।हालांकि, ऐसे सिद्धांत हैं जो उपप्रकार को परिभाषित करते हैं।

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

प्रकारों के कुछ संयोजन प्रकार के अन्य संयोजनों के बराबर हैं।जब कार्यों को घातांक माना जाता है, तो प्रकारों के संयोजन को बीजगणितीय पहचान के समान लिखा जा सकता है।<ref>{{cite web |last1=Milewski |first1=Bartosz |title=Programming with Math (Exploring Type Theory) |url=https://www.youtube.com/watch?v=8AGWTWVOJ74 |website=YouTube}}</ref> इस प्रकार, <math>{\mathbb 0} + A \cong A</math>, <math>{\mathbb 1} \times A \cong A</math>, <math>{\mathbb 1} + {\mathbb 1} \cong {\mathbb 2}</math>, <math>A^{B+C} \cong A^B \times A^C</math>, <math>A^{B\times C} \cong (A^B)^C</math>।

=== Axioms ===

अधिकांश प्रकार के सिद्धांतों में अभिगृहीत नहीं होता है।ऐसा इसलिए है क्योंकि एक  प्ररूप सिद्धांत को इसके नियमों के नियमों द्वारा परिभाषित किया गया है।(ऊपर #rules देखें)।यह समुच्चय सिद्धान्त से परिचित लोगों के लिए भ्रम का एक स्रोत है, जहां एक सिद्धांत को एक तर्क के लिए अनुमान के नियमों (जैसे प्रथम-क्रम तर्क) और समुच्चय के बारे में अभिगृहीत दोनों द्वारा परिभाषित किया जाता है।

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

यदि वे उन शर्तों पर गणना करने के तरीके के बिना शर्तों का परिचय देते हैं, तो Axioms समस्याओं का कारण बन सकते हैं।अर्थात्, अभिगृहीत  प्ररूप सिद्धांत के [[सामान्य रूप (अमूर्त पुनर्लेखन)]] के साथ हस्तक्षेप कर सकते हैं।<ref>{{cite web |title=Axioms and Computation |url=https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html |website=Theorem Proving in Lean |access-date=21 January 2022}}</ref> कुछ सामान्य रूप से सामना किए गए अभिगृहीत हैं:
* Axiom k पहचान प्रमाणों की विशिष्टता सुनिश्चित करता है।यही है, कि पहचान प्रकार का प्रत्येक शब्द रिफ्लेक्सिटी के बराबर है।<ref>{{cite web |title=Axiom K |url=http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/axiom+K+(type+theory) |website=nLab}}</ref>
* एकतरफा अभिगृहीत मानता है कि प्रकारों की तुल्यता प्रकारों की समानता है।इस गुण में अनुसंधान ने [[क्यूबिकल टाइप थ्योरी|क्यूबिकल  प्ररूप सिद्धांत]] का नेतृत्व किया, जहां गुण एक अभिगृहीत की आवश्यकता के बिना रखती है।<ref name=":0">{{cite journal |last1=Cohen |first1=Cyril |last2=Coquand |first2=Thierry |last3=Huber |first3=Simon |last4=Mörtberg |first4=Anders |title=Cubical Type Theory: a constructive interpretation of the univalence axiom |journal=21st International Conference on Types for Proofs and Programs (TYPES 2015)|date=2016 |doi=10.4230/LIPIcs.CVIT.2016.23 |doi-broken-date=31 December 2022 |arxiv=1611.02108 |url=https://www.cse.chalmers.se/~simonhu/papers/cubicaltt.pdf |archive-url=https://ghostarchive.org/archive/20221009/https://www.cse.chalmers.se/~simonhu/papers/cubicaltt.pdf |archive-date=2022-10-09 |url-status=live}}</ref>
* बाहर किए गए मध्य का कानून प्रायः उन उपयोगकर्ताओं को संतुष्ट करने के लिए जोड़ा जाता है जो अंतर्ज्ञानवादी तर्क के अतिरिक्त [[शास्त्रीय तर्क]] चाहते हैं।

पसंद के अभिगृहीत को  प्ररूप सिद्धांत में जोड़े जाने की आवश्यकता नहीं है, क्योंकि अधिकांश प्रकार के सिद्धांतों में इसे अनुमान के नियमों से प्राप्त किया जा सकता है।यह  प्ररूप सिद्धांत के [[रचनात्मक गणित]] प्रकृति के कारण है, जहां यह साबित करना कि एक मूल्य सम्मिलित है, मूल्य की गणना करने के लिए एक विधि की आवश्यकता होती है।पसंद का अभिगृहीत अधिकांश निर्धारित सिद्धांतों की तुलना में  प्ररूप सिद्धांत में कम शक्तिशाली है, क्योंकि  प्ररूप सिद्धांत के फलन कम्प्यूटेशनल होने चाहिए और सिंटैक्स-चालित होने के कारण, एक प्रकार में शब्दों की संख्या गिनती करने योग्य होनी चाहिए।(देखना {{Section link|Axiom of choice#In constructive mathematics}}।)

=== [[निर्णय समस्या]]एं ===

एक   प्ररूप सिद्धांत स्वाभाविक रूप से टाइप निवास की निर्णय समस्या से जुड़ा हुआ है।<ref>{{cite book|author1=Henk Barendregt|author2=Wil Dekkers|author3=Richard Statman|title=Lambda Calculus with Types|url=https://books.google.com/books?id=2UVasvrhXl8C|date=20 June 2013|publisher=Cambridge University Press|isbn=978-0-521-76614-2|pages=66}}</ref>


==== टाइप निवास ====
{{Main|Type inhabitation}}
टाइप निवास की निर्णय समस्या (द्वारा संक्षिप्त) <math>\exists e.\Gamma \vdash e : \tau?</math>) है:
: एक प्रकार का वातावरण दिया <math>\Gamma</math> और एक प्रकार <math>\tau</math>, तय करें कि क्या कोई शब्द सम्मिलित है <math>e</math> जिसे प्रकार सौंपा जा सकता है <math>\tau</math> प्रकार के वातावरण में <math>\Gamma</math>।
प्रणाली यू#गिरार्ड का विरोधाभास | गिरार्ड के विरोधाभास से पता चलता है कि टाइप निवास दृढ़ता से करी -आओ -पत्राचार के साथ एक प्रकार की प्रणाली की स्थिरता से संबंधित है।ध्वनि होने के लिए, इस तरह की प्रणाली में निर्जन प्रकार होने चाहिए।

शब्दों और प्रकारों का विरोध कार्यान्वयन और विनिर्देश में से एक के रूप में भी हो सकता है।[[कार्यक्रम संश्लेषण]] (कम्प्यूटेशनल समकक्ष का) प्रकार के निवास (नीचे देखें) का उपयोग प्रकार की जानकारी के रूप में दिए गए विनिर्देश से (सभी या भागों के) कार्यक्रमों के निर्माण के लिए किया जा सकता है।<ref>
{{cite conference |last1=Heineman |first1=George T. |last2=Bessai |first2=Jan |last3=Düdder |first3=Boris |last4=Rehof |first4=Jakob |year=2016 |title=A long and winding road towards modular synthesis |publisher=Springer |book-title=Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques |conference=ISoLA 2016 |pages=303–317 |series=Lecture Notes in Computer Science |volume=9952 |doi=10.1007/978-3-319-47166-2_21 |isbn=978-3-319-47165-5 }}</ref>


==== टाइप इन्फ्रेंस ====
{{Main|Type inference}}
कई कार्यक्रम जो  प्ररूप सिद्धांत (जैसे, इंटरैक्टिव प्रमेय प्रोवर्स) के साथ काम करते हैं, वे भी टाइप इन्फ्रेंसिंग करते हैं।यह उन्हें उन नियमों का चयन करने देता है जो उपयोगकर्ता उपयोगकर्ता द्वारा कम कार्यों के साथ, उपयोगकर्ता का इरादा रखते हैं।

=== अनुसंधान क्षेत्र ===

होमोटॉपी   प्ररूप सिद्धांत अंतर्ज्ञानवादी  प्ररूप सिद्धांत से भिन्न होता है जो ज्यादातर समानता प्रकार की हैंडलिंग से होता है।2016 में क्यूबिकल  प्ररूप सिद्धांत प्रस्तावित किया गया था, जो सामान्यीकरण के साथ एक समस्थेयता   प्ररूप सिद्धांत है।<ref>{{Cite journal |last1=Sterling |first1=Jonathan |last2=Angiuli |first2=Carlo |date=2021-06-29 |title=Normalization for Cubical Type Theory |url=https://ieeexplore.ieee.org/document/9470719 |journal=2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |location=Rome, Italy |publisher=IEEE |pages=1–15 |doi=10.1109/LICS52264.2021.9470719 |arxiv=2101.11479 |isbn=978-1-6654-4895-6|s2cid=231719089 }}</ref><ref name=":0"/>


== व्याख्या ==

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

=== प्रकार [[प्रस्ताव]] हैं;शर्तें प्रमाण हैं ===

जब एक आधार  के रूप में उपयोग किया जाता है, तो कुछ प्रकारों की व्याख्या प्रस्तावों के रूप में की जाती है (बयान जो सिद्ध हो सकते हैं) और प्रकार का एक शब्द उस प्रस्ताव का एक प्रमाण है।इस प्रकार, प्रकार & pi;x: nat।x+1 = 1+x यह दर्शाता है कि, किसी भी x के लिए NAT, x+1 और 1+x समान हैं।और उस प्रकार का एक शब्द इसके प्रमाण का प्रतिनिधित्व करता है।

=== करी-हावर्ड पत्राचार ===

करी -होवर पत्राचार लॉजिक्स और प्रोग्रामिंग भाषाओं के बीच मनाया समानता है।तर्क में निहितार्थ, ए <math>\to</math> B टाइप A से टाइप B तक फलन जैसा दिखता है।विभिन्न प्रकार के लॉजिक्स के लिए, नियम एक प्रोग्रामिंग भाषा के प्रकारों में अभिव्यक्ति के समान हैं।समानता आगे बढ़ती है, क्योंकि नियमों के अनुप्रयोग प्रोग्रामिंग भाषाओं में कार्यक्रमों से मिलते जुलते हैं।इस प्रकार, पत्राचार को प्रायः कार्यक्रमों के रूप में प्रमाण के रूप में संक्षेपित किया जाता है।

लॉजिक ऑपरेटर्स सार्वभौमिक परिमाणीकरण और अस्तित्वगत मात्रा का ठहराव प्रति मार्टिन-लोफ ने आश्रित  प्ररूप सिद्धांत का आविष्कार करने के लिए नेतृत्व किया।

=== अंतर्ज्ञानवादी तर्क ===

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

तार्किक प्रस्तावों के लिए प्रकारों का एक प्राकृतिक संबंध है।यदि एक प्रस्ताव का प्रतिनिधित्व करने वाला एक प्रकार है, तो प्रकार का एक फलन बनाने में सक्षम है<math>\top \to </math> ए इंगित करता है कि ए में एक प्रमाण है और फलन ए बनाने में सक्षम है <math>\to \bot</math>इंगित करता है कि A में कोई प्रमाण नहीं है।अर्थात्, निवास योग्य प्रकार सिद्ध होते हैं और निर्जन प्रकार अस्वीकृत होते हैं।

चेतावनी: इस व्याख्या से बहुत भ्रम हो सकता है।एक  प्ररूप सिद्धांत में टाइप बूल की शर्तों को सही और गलत हो सकता है, जो एक [[बूलियन तर्क]] की तरह काम करता है, और एक ही समय में प्रकार होते हैं <math>\top</math> और <math>\bot</math> प्रस्ताव के लिए एक अंतर्ज्ञानवादी तर्क के हिस्से के रूप में, सच्चे (साबित) और झूठे (असुरक्षित) का प्रतिनिधित्व करने के लिए।

इस अंतर्ज्ञानवादी व्याख्या के अंतर्गत, ऐसे सामान्य प्रकार हैं जो तार्किक ऑपरेटरों के रूप में कार्य करते हैं:
{| class="wikitable"
! तर्क नाम !! तर्क संकेतन !! प्रकार संकेतन !! प्रारूप नाम
|-
| सत्य || <math>\top</math> || <math>\top</math> || इकाई प्रारूप
|-
| असत्य || <math>\bot</math> || <math>\bot</math> || रिक्त प्रारूप
|-
| [[Not (logic)|नहीं]] || <math>\neg A</math> || <math>A \to \bot</math> || रिक्त प्रारूप के फलन
|-
| [[Material conditional|निहितार्थ]] || <math>A \to B</math> || <math>A \to B</math> || फलन
|-
| [[And (logic)|और]] || <math>A \land B</math> || <math>A \times B</math> || उत्पाद प्रकार
|-
| [[Or (logic)|या]] || <math>A \lor B</math> || <math>A + B</math> || योग प्रकार
|-
| [[Universal quantification|सभी के लिए]] || <math>\forall a \in A, P(a)</math> || &Pi; a : A . P(a) || आश्रित फलन
|-
| सम्मिलित || <math>\exists a \in A, P(a)</math> || &Sigma; a : A . P(a)  || आश्रित उत्पाद प्रकार
|}
लेकिन इस व्याख्या के अंतर्गत, बीच में बहिष्कृत कोई कानून नहीं है।अर्थात्, प्रकार का कोई शब्द नहीं है & pi;ए ।ए + (ए) <math>\to \bot</math>)।

इसी तरह, कोई दोहराव नहीं है।प्रकार का कोई शब्द नहीं है & pi;ए ।((ए <math>\to \bot</math>) <math>\to \bot</math>) <math>\to </math> ए (नोट: अंतर्ज्ञानवादी तर्क अनुमति देता है <math>\lnot \lnot \lnot A \to \lnot A</math> और प्रकार का एक शब्द है ((ए) <math>\to \bot</math>) <math>\to \bot</math>) <math>\to \bot</math>) <math>\to </math> (ए <math>\to \bot</math>)।)

इस प्रकार, तर्क-के-प्रकार एक अंतर्ज्ञानवादी तर्क है। प्ररूप सिद्धांत को प्रायः ब्रूवर -हाइकिंग -कोलमोगोरोव व्याख्या के कार्यान्वयन के रूप में उद्धृत किया जाता है।

नियम या धारणा द्वारा एक  प्ररूप सिद्धांत में बहिष्कृत मध्य और दोहरे नकारात्मकता के कानून को सम्मिलित करना संभव है।हालांकि, शब्द विहित शब्दों की गणना नहीं कर सकते हैं और यह यह निर्धारित करने की क्षमता में हस्तक्षेप करेगा कि क्या दो शब्द एक दूसरे के बराबर हैं।

=== रचनात्मक गणित ===

मार्टिन-लोफ ने रचनात्मक गणित के लिए एक आधार  के रूप में अपने अंतर्ज्ञानवादी  प्ररूप सिद्धांत का प्रस्ताव रखा।रचनात्मक गणित की आवश्यकता होती है जब साबित होता है कि वहाँ सम्मिलित है <math>x</math> गुण के साथ पी (<math>x</math>), एक विशेष होना चाहिए <math>x</math> और एक प्रमाण है कि यह गुण पी है। प्ररूप सिद्धांत में, अस्तित्व को आश्रित उत्पाद प्रकार का उपयोग करके पूरा किया जाता है और, इसके प्रमाण को उस प्रकार के शब्द की आवश्यकता होती है।इस कार्यकाल के लिए <math>t</math>,  पहला <math>t</math>उत्पादन करेंगे <math>x</math> और दूसरा <math>t</math>P का प्रमाण तैयार करेगा (<math>x</math>)।

एक गैर-कंस्ट्रक्टिव सबूत का एक उदाहरण विरोधाभास द्वारा एक प्रमाण है।पहला कदम यह मान रहा है कि <math>x</math> विरोधाभास से सम्मिलित नहीं है और इसका खंडन करता है।उस कदम से निष्कर्ष यह है कि ऐसा नहीं है <math>x</math> सम्मिलित नहीं होना ।अंतिम चरण, दोहरे नकारात्मकता द्वारा, निष्कर्ष निकाला है <math>x</math> सम्मिलित।स्पष्ट होने के लिए, रचनात्मक गणित अभी भी विरोधाभास द्वारा खंडन करने की अनुमति देता है।यह साबित कर सकता है कि यह स्थिति नहीं है <math>x</math> सम्मिलित नहीं होना ।लेकिन रचनात्मक गणित यह निष्कर्ष निकालने के लिए दोहरे नकारात्मकता को हटाने के अंतिम चरण की अनुमति नहीं देता है <math>x</math> सम्मिलित।<ref>{{cite web |title=proof by contradiction |url=https://ncatlab.org/nlab/show/proof+by+contradiction |website=nlab |access-date=29 December 2021}}</ref>
रचनात्मक गणित ने प्रायः इंट्यूस्टिस्टिक लॉजिक का उपयोग किया है, जैसा कि ब्रूवर -हाइंग -कोलमोगोरोव व्याख्या द्वारा स्पष्ट किया गया है।

आधार  के रूप में प्रस्तावित अधिकांश  प्ररूप सिद्धांत रचनात्मक हैं।इसमें प्रमाण सहायक द्वारा उपयोग किए जाने वाले अधिकांश सम्मिलित हैं।

नियम या धारणा द्वारा, एक  प्ररूप सिद्धांत में गैर-कंस्ट्रक्टिव सुविधाओं को जोड़ना संभव है।इनमें गैर-कंस्ट्रक्टिव लॉजिक के संबंध में  संकेत/सीसी#जैसे निरंतरता पर ऑपरेटर सम्मिलित हैं।हालांकि, ये ऑपरेटर वांछनीय गुणों जैसे कि [[कैनोनिकिटी (टाइप थ्योरी)|कैनोनिकिटी ( प्ररूप सिद्धांत)]] और पैरमिकलिटी को तोड़ते हैं।

=== श्रेणी सिद्धांत ===

यद्यपि श्रेणी सिद्धांत के लिए प्रारंभिक प्रेरणा को संस्थागतवाद से दूर कर दिया गया था, लेकिन दो क्षेत्रों में गहरे संबंध थे।जैसा कि [[जॉन लेन बेल]] लिखते हैं: वास्तव में श्रेणियों को स्वयं एक निश्चित प्रकार के प्रकार के सिद्धांतों के रूप में देखा जा सकता है;यह तथ्य अकेले इंगित करता है कि  प्ररूप सिद्धांत श्रेणी सिद्धांत से बहुत अधिक निकटता से संबंधित है, क्योंकि यह सिद्धांत को समुच्चय करना है।संक्षेप में, एक श्रेणी को प्रकार (या प्रकार) के रूप में अपनी वस्तुओं के बारे में एक  प्ररूप सिद्धांत के रूप में देखा जा सकता है, अर्थात सामान्य रूप से  एक श्रेणी को इसके सिंटैक्स के एक  प्ररूप सिद्धांत के रूप में सोचा जा सकता है।कई महत्वपूर्ण परिणाम इस तरह से पालन करते हैं:<ref name="Sets and Extensions in the Twentieth Century">{{cite book |series=Handbook of the History of Logic |volume=6 |title=Sets and Extensions in the Twentieth Century|year=2012|publisher=Elsevier|isbn=978-0-08-093066-4 |first=John L. |last=Bell|chapter=Types, Sets and Categories | chapter-url = http://publish.uwo.ca/~jbell/types.pdf |editor-first=Akihiro |editor-last=Kanamory}}</ref>
* [[कार्टेशियन बंद श्रेणी]] टाइप किए गए λ-Calculus ([[Lambek]], 1970) के अनुरूप है;
* [[सी-मोनोइड]]्स (उत्पादों और घातांक के साथ श्रेणियां और एक गैर-टर्मिनल ऑब्जेक्ट) अप्रकाशित λ-Calculus (1980 के आसपास लैम्बेक और [[दाना स्कॉट]] द्वारा स्वतंत्र रूप से मनाया गया) के अनुरूप;
* [[स्थानीय रूप से कार्टेशियन बंद श्रेणी]] मार्टिन-लोफ  प्ररूप सिद्धांत के अनुरूप है। मार्टिन-लोफ टाइप थ्योरीज़ (सेली, 1984)।

इंटरप्ले, जिसे [[श्रेणीबद्ध तर्क]] के रूप में जाना जाता है, तब से सक्रिय अनुसंधान का विषय रहा है;उदाहरण के लिए जैकब्स (1999) का मोनोग्राफ देखें।

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

== टाइप थ्योरीज़ की सूची ==

=== मेजर ===
* बस टाइप किया गया लैम्ब्डा गणना जो एक उच्च-क्रम तर्क है
* अंतर्ज्ञानवादी  प्ररूप सिद्धांत
* प्रणाली एफ
* तार्किक ढांचे का उपयोग प्रायः अन्य प्रकार के सिद्धांतों को परिभाषित करने के लिए किया जाता है
* निर्माणों और उसके डेरिवेटिव की पथरी

=== माइनर ===
* [[स्वचालित]]
* सेंट  प्ररूप सिद्धांत
* UTT (LUO का एकीकृत सिद्धांत पर निर्भर प्रकार)
* [[संयोजक तर्क]] के कुछ रूप
* अन्य लोग लैम्ब्डा क्यूब में परिभाषित किए गए (जिसे शुद्ध प्रकार के प्रणाली के रूप में भी जाना जाता है)
* अन्य नाम के अंतर्गत लैम्ब्डा गणना टाइप किया गया

=== सक्रिय अनुसंधान ===
* समस्थेयता  प्ररूप सिद्धांत प्रकारों की समानता की खोज करता है
*NLAB: क्यूबिकल+टाइप+ उपागम समस्थेयता  प्ररूप सिद्धांत का कार्यान्वयन है

== अनुप्रयोग ==

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

श्रेणी सिद्धांत में काम करने वाले गणितज्ञों को पहले से ही ज़र्मेलो-फ्रेंकेल समुच्चय सिद्धांत की व्यापक रूप से स्वीकृत संस्थान के साथ काम करने में कठिनाई हुई थी। इससे व्यवस्थित ईटीसीएस (यूरोपीय ट्रेन नियंत्रण प्रणाली) की श्रेणी के लॉवर के प्राथमिक सिद्धांत जैसे प्रस्ताव सामने आए।<ref>{{nlab|id=ETCS}}</ref>  प्ररूप सिद्धांत का उपयोग करके इस लाइन में समस्थेयता (होमोटॉपी) प्ररूप सिद्धांत जारी है। शोधकर्ता निर्भर प्रकारों (विशेष रूप से पहचान प्रकार) और बीजगणितीय सांस्थिति (विशेष रूप से होमोटॉपी) के बीच संबंधों की खोज कर रहे हैं।

=== प्रमाण सहायक ===
{{main|प्रमाण सहायक}}

प्ररूप सिद्धांत में अधिकांश सम्मिलित शोध प्रमाण जाँचकर्ता, अन्योन्यक्रिया प्रमाण सहायक और स्वचालित प्रमेय समर्थक द्वारा संचालित होते हैं। इनमें से अधिकांश प्रणालियाँ एन्कोडिंग प्रमाणों के लिए गणितीय आधार के रूप में एक प्रकार के सिद्धांत का उपयोग करती हैं, जो आश्चर्यजनक नहीं है, प्रारूप सिद्धांत और प्रोग्रामिंग भाषाओं के बीच घनिष्ठ संबंध को देखते हुए:
* अन्य प्रकार के सिद्धांतों को परिभाषित करने के लिए तार्किक रूपरेखा का उपयोग प्रायः ट्वेलफ द्वारा किया जाता है;
* कई  प्ररूप सिद्धांत जो उच्च-क्रम के तर्क के अंतर्गत आते हैं, उनका उपयोग उच्च क्रम की भाषा (प्रमाण सहायक) और [[प्रोटोटाइप सत्यापन तंत्र|प्रोटोटाइप सत्यापन प्रणाली]] द्वारा किया जाता है;
* संगणनात्मक  प्रकार के सिद्धांत का उपयोग एनयूपीआरएल द्वारा किया जाता है;
* कॉक, मटिटा, और लीन द्वारा निर्माण और इसके व्युत्पन्न शब्द की गणना का उपयोग किया जाता है;
* यूटीटी (लुओ की निर्भरता के प्रकारों का एकीकृत सूत्र सिद्धांत) का उपयोग  ऑस्ट्रेलियाई ग्राफिक डिजाइन संघ (प्रोग्रामिंग भाषा) द्वारा किया जाता है जो [[अगदा (प्राग्रामिंग भाषा)|प्राग्रामिंग भाषा]] और प्रमाण सहायक दोनों है

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

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

प्रोग्रामिंग भाषा [[एमएल (प्रोग्रामिंग भाषा)|यंत्र अधिगम (प्रोग्रामिंग भाषा)]] को प्रकार के सिद्धांतों में  कुशलतापूर्वक प्रयोग करने के लिए विकसित किया गया था (गणना योग्य फलन के लिए तर्क देखें) और और इसका अपना प्रारूप प्रणाली उनसे काफी प्रभावित था।

=== भाषाविज्ञान ===
प्ररूप सिद्धांत का व्यापक रूप से प्राकृतिक भाषाओं के शब्दार्थ के औपचारिक सिद्धांतों में विशेष रूप से मोंटेग व्याकरण और उसके वंशजों में उपयोग किया जाता है।<ref>{{Cite book |last1=Chatzikyriakidis |first1=Stergios |url=https://books.google.com/books?id=iEEUDgAAQBAJ |title=Modern Perspectives in Type-Theoretical Semantics |last2=Luo |first2=Zhaohui |date=2017-02-07 |publisher=Springer |isbn=978-3-319-50422-3 |language=en}}</ref><ref>{{Cite book |last=Winter |first=Yoad |url=https://books.google.com/books?id=aDRWDwAAQBAJ&q=%22formal+semantics%22+%22type+theory%22 |title=Elements of Formal Semantics: An Introduction to the Mathematical Theory of Meaning in Natural Language |date=2016-04-08 |publisher=Edinburgh University Press |isbn=978-0-7486-7777-1 |language=en}}</ref><ref>Cooper, Robin. "[http://lecomte.al.free.fr/ressources/PARIS8_LSL/ddl-final.pdf Type theory and semantics in flux]." Handbook of the Philosophy of Science 14 (2012): 271-323.</ref> विशेष रूप से, श्रेणीबद्ध व्याकरण और  प्राक् समूह व्याकरण शब्दों के प्रकार (संज्ञा, क्रिया, आदि) को परिभाषित करने के लिए व्यापक रूप से प्रारूप संरचक का उपयोग करते हैं।

सबसे सामान्य निर्माण क्रमशः  विशिष्ट और सत्यता मान के लिए मूल प्रकार e और t  लेता है, और प्रकारों के समूह को पुनरावर्ती रूप से निम्नानुसार परिभाषित करता है:
* यदि <math>a</math> और <math>b</math> प्रकार हैं, तो <math>\langle a,b\rangle</math> है;
* मूल प्रकारों के अतिरिक्त कुछ भी नहीं, और पूर्व भाग के माध्यम से उनसे क्या निर्माण किया जा सकता है, वे प्रकार है।

एक जटिल प्रकार <math>\langle a,b\rangle</math> प्रकार की  स्थितियो से फलन (गणित) का प्रकार है <math>a</math> प्रकार की  स्थितियो के लिए <math>b</math> फलन का प्रकार है। इस प्रकार किसी के पास <math>\langle e,t\rangle</math> जैसे प्रकार होते हैं जिन्हें स्थिति से सत्य-मूल्यों अर्थात स्थितियों  के समुच्चय के संकेतक फलन  के समुच्चय के तत्वों के रूप में व्याख्या किया जाता है। प्रारूप  <math>\langle\langle e,t\rangle,t\rangle</math> का एक व्यंजक सत्वों के समुच्चयों से सत्य-मानों का एक फलन है, अर्थात् समुच्चयों के समुच्चय का एक संकेतक फलन है। इस बाद वाले प्रकार को मानक रूप से प्राकृतिक भाषा परिमाणक के प्रकार के रूप में लिया जाता है, जैसे हर कोई या कोई नहीं (मोंटेग 1973, बारवाइज और कूपर 1981)।{{full citation needed|date=July 2022}}


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

== यह भी देखें ==
* गणित की आधार 

==अग्रिम पठन==
{{refbegin}}
* {{cite web |first1=C. |last1=Aarts |first2=R. |last2=Backhouse |first3=P. |last3=Hoogendijk |first4=E. |last4=Voermans |first5=J. |last5=van der Woude |title=A Relational Theory of Datatypes |date=December 1992 |publisher=Technische Universiteit Eindhoven |url=https://www.researchgate.net/publication/277287583}}
* {{cite book
  | first = Peter
  | last = Andrews B.
  | year = 2002
  | isbn = 978-1-4020-0763-7
  | title = An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof |edition=2nd
  | publisher = Kluwer 
}}
*{{cite book
 | first = Bart
 | last = Jacobs
 | title = Categorical Logic and Type Theory
 | year = 1999
 | publisher = Elsevier
 | isbn = 978-0-444-50170-7
 | series = Studies in Logic and the Foundations of Mathematics |volume=141
 | url = https://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html }} Covers type theory in depth, including polymorphic and dependent type extensions. Gives [[categorical semantics]].
* {{cite book |first=Luca |last=Cardelli |chapter=Type Systems |chapter-url=http://citeseer.ist.psu.edu/cardelli97type.html |editor-first=Allen B. |editor-last=Tucker |title=The Computer Science and Engineering Handbook |publisher=CRC Press |year=1996 |isbn=9780849329098 |pages=2208–36 }}
* {{cite book
  | first = Jordan E.
  | last = Collins
  | year = 2012
  | isbn = 978-3-8473-2963-3
  | title = A History of the Theory of Types: Developments After the Second Edition of 'Principia Mathematica'
  | publisher = Lambert Academic Publishing
  | hdl = 11375/12315
 }} Provides a historical survey of the developments of the theory of types with a focus on the decline of the theory as a foundation of mathematics over the four decades following the publication of the second edition of 'Principia Mathematica'.
* {{cite book |author-link=Robert Lee Constable |last=Constable |first=Robert L. |chapter=Naïve Computational Type Theory |chapter-url=http://www.nuprl.org/documents/Constable/naive.pdf |archive-url=https://ghostarchive.org/archive/20221009/http://www.nuprl.org/documents/Constable/naive.pdf |archive-date=2022-10-09 |url-status=live |editor-first=H. |editor-last=Schwichtenberg |editor-first2=R. |editor-last2=Steinbruggen |title=Proof and System-Reliability |publisher=Springer |series=Nato Science Series II |volume=62 |year=2012 |orig-year=2002 |isbn=9789401004138 |pages=213–259 }} Intended as a type theory counterpart of [[Paul Halmos]]'s (1960) ''[[Naive Set Theory (book)|Naïve Set Theory]]''
* {{cite encyclopedia |author-link=Thierry Coquand |first=Thierry |last=Coquand |title=Type Theory |date=2018 |orig-year=2006 |encyclopedia=[[Stanford Encyclopedia of Philosophy]] |url=http://plato.stanford.edu/entries/type-theory/ }}
* {{cite book |first=Simon |last=Thompson |title=Type Theory and Functional Programming |publisher=Addison–Wesley |year=1991 |isbn=0-201-41667-0 |url=http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/}}
* {{cite book |author-link=J. Roger Hindley |first=J. Roger |last=Hindley |title=Basic Simple Type Theory |publisher=Cambridge University Press |year=2008 |orig-year=1995 |isbn=978-0-521-05422-5 }}<!-- no idea why these get different ISBNs, they don't appear to be different editions--> A good introduction to simple type theory for computer scientists; the system described is not exactly Church's STT though. [http://www.iwu.edu/~htiede/papers/pdf/jolli-review.pdf Book review]
* {{cite book |first1=Fairouz D. |last1=Kamareddine |first2=Twan |last2=Laan |first3=Rob P. |last3=Nederpelt |title=A modern perspective on type theory: from its origins until today |publisher=Springer |year=2004 |isbn=1-4020-2334-0 }}
* {{cite book |first1=José |last1=Ferreirós |first2=José Ferreirós |last2=Domínguez |title=Labyrinth of thought: a history of set theory and its role in modern mathematics |publisher=Springer |year=2007 |isbn=978-3-7643-8349-7 |edition=2nd |chapter=X. Logic and Type Theory in the Interwar Period }}
* {{cite thesis |first=T.D.L. |last=Laan |title=The evolution of type theory in logic and mathematics |date=1997 |type=PhD |publisher=Eindhoven University of Technology |url=https://pure.tue.nl/ws/files/1383309/498552.pdf |archive-url=https://ghostarchive.org/archive/20221009/https://pure.tue.nl/ws/files/1383309/498552.pdf |archive-date=2022-10-09 |url-status=live |doi=10.6100/IR498552 |isbn=90-386-0531-5 }}
{{refend}}


==टिप्पणियाँ==
{{Notelist}}


==संदर्भ==
{{Reflist|30em}}


==बाहरी संबंध==




=== परिचयात्मक सामग्री ===
* [https://ncatlab.org/nlab/show/type+theory प्ररूप सिद्धांत NLAB पर], जिसमें कई विषयों पर लेख हैं।
*[https://plato.stanford.edu/entries/type-theory-intuitionistic/ intuitionistic  प्ररूप सिद्धांत] दर्शन के स्टैनफोर्ड एनसाइक्लोपीडिया में लेख
*[https://home.ttic.edu/~dreyer/course/papers/barendregt.pdf लैम्ब्डा गणना टाइप्स के साथ] हेंक Barendregt द्वारा बुक
*[https://hbr.github.io/lambda-calculus/cc-tex Calluss of Construstions/Typed Lambda Callus.
*[https://archive-pml.github.io/martin-lof/pdfs/bibliopolis-book-retypeset-1984.pdf intuitionistic  प्ररूप सिद्धांत] प्रति मार्टिन-löf द्वारा नोट्स
*[https://www.cse.chalmers.se/research/group/logic/book/book.pdf मार्टिन-Löf के  प्ररूप सिद्धांत में प्रोग्रामिंग] बुक
*[https://homotopytypetheory.org/book/ homotopy  प्ररूप सिद्धांत] पुस्तक, जिसने एक गणितीय आधार  के रूप में समस्थेयता  प्ररूप सिद्धांत को प्रस्तावित किया।

=== उन्नत सामग्री ===
* {{scholarpedia|title=Computational type theory|urlname=Computational_type_theory|curator=Robert L. Constable}}
* [http://lists.seas.upenn.edu/mailman/listinfo/types-list प्रकार फोरम] & mdash;मॉडरेट ई-मेल फोरम कंप्यूटर साइंस में  प्ररूप सिद्धांत पर ध्यान केंद्रित करते हुए, 1987 के बाद से काम कर रहा है।
* [ftp://ftp.cs.cornell.edu/pub/nuprl/doc/book.ps.gz nuprl पुस्तक]।]
* [http://www.cs.chalmers.se/cs/research/logic/types/tutorials.html प्रकार प्रोजेक्ट लेक्चर नोट्स] समर स्कूलों 2005-2008 का
** [http://www.cs.chalmers.se/cs/research/logic/typesss05/program.html 2005 समर स्कूल] में परिचयात्मक व्याख्यान हैं
*[https://www.cs.uoregon.edu/research/summerschool/archives.html ओरेगन प्रोग्रामिंग लैंग्वेजेस समर स्कूल], कई व्याख्यान और कुछ नोट्स।
** [https://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html समर 2013 लेक्चर]] [https://www.youtube.com/watch?v=9snefrwbidclexrwbdcrwbdcrwbidc&lstclestclestclestclesprwbidc&lstclestcrwbidcrwbidc&lstclestlist।यूट्यूब पर]
** [https://www.cs.uoregon.edu/research/summerschool/summer15/curriculum.html समर 2015 प्रकार, तर्क, शब्दार्थ और सत्यापन]
* [http://math.andrej.com/category/type-theory/ आंद्रेज बाउर का ब्लॉग]

{{Computer science}}
{{Mathematical logic}}
{{Formal semantics}}

{{DEFAULTSORT:Type Theory}}

श्रेणी:  प्ररूप सिद्धांत
श्रेणी: औपचारिक तर्क प्रणाली
श्रेणी: पदानुक्रम


[[Category: Machine Translated Page]]
[[Category:Created On 13/02/2023]]