प्रकार सिद्धांत: Difference between revisions

From Vigyanwiki

प्रकार सिद्धांत

Latest revision as of 17:30, 19 February 2023

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

इतिहास

सहज समुच्चय सिद्धान्त और औपचारिक तर्क के आधार पर एक गणितीय आधार में एक विरोधाभास से बचने के लिए प्ररूप सिद्धांत बनाया गया था। बर्ट्रेंड रसेल द्वारा खोजा गया रसेल का विरोधाभास सम्मिलित था क्योंकि एक समुच्चय को "सभी संभव समुच्चयों" का उपयोग करके परिभाषित किया जा सकता था जिसमें वे स्वयं सम्मिलित थे। बर्ट्रेंड रसेल ने 1902 और 1908 के बीच, समस्या को सही करने के लिए विभिन्न " प्ररूप सिद्धांत" प्रस्तावित किए। 1908 तक रसेल एक "अपचेयता-अभिगृहीत" के साथ "प्रचलित" प्ररूप सिद्धांत पर पहुंचे, जिनमें से दोनों को व्हाइटहेड और रसेल के प्रिंसिपिया मैथेमेटिका में प्रमुखता से 1910 और 1913 के बीच प्रकाशित किया गया था। इस प्रणाली ने प्रकार के पदानुक्रम बनाकर और फिर प्रत्येक मूर्त गणितीय इकाई को एक प्रकार निर्दिष्ट करके रसेल के विरोधाभास से बचा लिया। किसी दिए गए प्रकार की इकाइयाँ विशेष रूप से उस प्रकार के उपप्रकारों से निर्मित होती है,^{[lower-alpha 1]} इस प्रकार किसी इकाई को स्वयं का उपयोग करके परिभाषित करने से रोकती हैं। रसेल के प्ररूप सिद्धांत ने स्वयं को समूह के सदस्य होने की संभावना को अस्वीकृत कर दिया।

तर्क में प्रकारों का हमेशा उपयोग नहीं किया जाता था। रसेल के विरोधाभास से बचने के लिए अन्य तकनीकें भी थीं।^[3] एक विशेष तर्क, अलोंजो चर्च के लैम्ब्डा कैलकुलस के साथ प्रयोग किए जाने पर प्रकारों ने अधिकार प्राप्त किया।

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

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

परिचय

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

मूल तत्व

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

प्ररूप सिद्धांत में, प्रत्येक पद का एक प्रकार होता है। एक पद और इसके प्रकार को प्रायः "पद: प्रकार" के रूप में एक साथ लिखा जाता है। प्ररूप सिद्धांत में सम्मिलित करने के लिए एक सामान्य प्रकार प्राकृतिक संख्या है, जिसे प्रायः " $\mathbb {N}$ '' or "nat" लिखा जाता है। दूसरा बूलियन तर्क मान है। तो, उनके प्रकारों के साथ कुछ बहुत ही सरल पद है

1 : nat
42 : nat
true : bool

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

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

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

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 $\twoheadrightarrow$ 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" तक कम हो जाते हैं। जब दो पद समान होते हैं, तो उन्हें एक दूसरे के लिए प्रतिस्थापित किया जा सकता है। समानता प्ररूप सिद्धांत में एक जटिल विषय है और कई प्रकार के समानता हैं। इस तरह की समानता, जहाँ दो पद एक ही पद के लिए संगणित होते हैं, "न्यायिक समानता" कहलाती है।

फलन

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

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

एक लैम्ब्डा पद "(λ चर नाम: टाइप 1 पद)" जैसा दिखता है और इसमें "टाइप 1 → टाइप 2" टाइप होता है। प्रकार "टाइप 1 → टाइप 2" इंगित करता है कि लैम्ब्डा पद एक ऐसा फलन है जो "टाइप 1" प्रकार का अंतःखंडी अनुपात लेता है और "टाइप 2" प्रकार के पद की गणना करता है। लैम्ब्डा पद के अंदर का पद "टाइप 2" का मान होना चाहिए, यह मानते हुए कि चर का प्रकार "टाइप 1" है।

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

(λ x : nat . (add x x)) : nat na

चर का नाम "x" है और चर का प्रकार "nat" है। पद "(योग X X )" में "x: nat" मानकर "nat" टाइप किया गया है। इस प्रकार, लैम्ब्डा पद का प्रकार "nat → nat" है, जिसका अर्थ है कि यदि इसे तर्क के रूप में "nat" दिया जाता है, तो यह "nat" की गणना करेगा। न्यूनीकरण (उर्फ अभिकलन) लैम्ब्डा शर्तों के लिए परिभाषित किया गया है। जब फलन लागू किया जाता है (जिसे उर्फ कहा जाता है), अंतःखंडी अनुपात के लिए तर्क प्रतिस्थापित किया जाता है।

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

(λ x : nat . (add x x)) 5 : nat

लैम्ब्डा पद प्रारूप "nat → nat" था, जिसका अर्थ था कि तर्क के रूप में "nat" दिया गया है, यह "nat" प्रकार का एक पद उत्पन्न करेगा। चूँकि हमने इसे "5" तर्क दिया है, उपरोक्त पद का प्रकार "nat" है। "(योग x x)" पद में अंतःखंडी अनुपात "x" के लिए तर्क "5" को प्रतिस्थापित करके कमी काम करती है, इसलिए पद की गणना होती है:

(add 5 5) : nat

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

10: nat

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

double : nat nat ::= (λ x : nat . (add x x))

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

double 5 : nat

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

10: nat

आश्रित प्ररूपण

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

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

यदि a 2 4: nat
यदि a असत्य सत्य है: बूल

लेकिन यदि b और c के अलग -अलग प्रकार होते हैं, तो b c के मूल्य पर निर्भर करता है। हम प्रतीक "Π" का उपयोग करते हैं; एक फलन को इंगित करने के लिए जो एक तर्क लेता है और एक प्रकार देता है। यह मानते हुए कि हमारे पास b" और c "और" "a : bool", "b : B" और "c : C" हैं, तो

यदि a b c : (Π a : bool B→ C→ यदि a B C)

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

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

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

विश्व समष्टि

Π-शर्तें एक प्रकार अप्रत्यागम हैं। तो उनका अप्रत्यागम मान किस प्रकार का है? पूर्ण रूप से एक प्रारूप होना चाहिए जिसमें प्रकार हों। एक प्रारूप जिसमें अन्य प्रकार होते हैं, उसे "विश्व समष्टि" कहा जाता है। इसे प्राय: $U$ चिन्ह के साथ लिखा जाता है। कभी -कभी विश्व समष्टि का एक पदानुक्रम होता है, जिसमे $U_{0}$ : $U_{1}$ , $U_{1}$ : $U_{2}$ आदि सम्मिलित है।

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

उदाहरण के लिए:^[5]

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

सामान्य "नियम द्वारा" प्रारूप और शर्तें

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

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

रिक्‍त प्रारूप

रिक्‍त प्रारूप की कोई शर्तें नहीं हैं। प्रारूप सामान्य रूप से '' $\bot$ '' या '' $\mathbb {0}$ '' मे लिखा जाता है।

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

इकाई प्रारूप

इकाई प्रारूप में 1 प्रामाणिक पद है। प्रारूप '' $\top$ '' या '' $\mathbb {1}$ '' लिखा जाता है और एकल प्रामाणिक पद ''*'' लिखा जाता है।

इकाई प्रारूप का उपयोग यह दिखाने के लिए किया जाता है कि कुछ सम्मिलित है या गणना योग्य है। यदि किसी प्रकार "A" के लिए, आप '' $\top \to$ A" प्रकार का फलन बना सकते हैं, तो आप जानते हैं कि "A" में एक या अधिक पद हैं। जब किसी प्रकार में कम से कम 1 पद होता है, तो हम कहते हैं कि यह " सयात्रिक" है।

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

बूलियन प्रारूप में 2 प्रामाणिक पद हैं। प्रारूप सामान्य रूप से र "बूल" या " $\mathbb {B}$ '' या '' $\mathbb {2}$ '' लिखा जाता है। प्रामाणिक पद सामान्य रूप से "सत्य" और "असत्य" होते हैं।

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

यदि सत्य b c $\twoheadrightarrow$ b
यदि असत्य b c $\twoheadrightarrow$ c

उत्पाद प्रारूप

उत्पाद प्रारूप में ऐसे पद होते हैं जो क्रमित जोड़े होते हैं। प्रकार "A" और "B" के लिए, उत्पाद प्रारूप A $\times$ B लिखा जाता है। संरचक फलन "जोड़ी" द्वारा प्रामाणिक पद बनाए जाते हैं। शर्तें "युग्म a b" हैं, जहां "a" प्रकार "A" का एक पद है और "b" प्रकार "B" का एक पद है। उत्पाद प्रकार को "प्रथम" और "द्वितीय" निरसक फलनों के साथ परिभाषित किया गया है:

प्रथम (युग्म a b) $\twoheadrightarrow$ a
द्वितीय (युग्म a b) $\twoheadrightarrow$ b

क्रमित किए गए युग्म के अतिरिक्त, इस प्रकार का उपयोग तार्किक संयोजन के लिए किया जाता है। क्योंकि इसमे A और B होते है। इसका उपयोग अन्तः क्रिया के लिए भी किया जाता है, क्योंकि यह दोनों प्रारूप में से एक को धारण करता है।

यदि एक प्ररूप सिद्धांत में निर्भर प्ररूपण है, तो इसमे आश्रित युग्म है एक आश्रित युग्म में, दूसरा प्रकार पहले पद के मान पर निर्भर करता है। इस प्रकार, प्रारूप $\Sigma$ A: a।B (a) लिखा जाता है, जहाँ b में प्रारूप A $\to$ U है। गुण "B(a)" के साथ "a" के स्थिति को दिखाते समय यह उपयोगी होता है।

योग प्रारूप

योग प्रकार एक "चिह्नित संघ" है। अर्थात्, प्रकार "A" और "B" के लिए, प्रकार "A+ B" में या तो "ए" प्रकार का पद या "B" प्रकार का पद होता है और यह जानता है कि यह कौन सा है। प्रकार संचरक "समादेश बायाँ" और "समादेश दायाँ" के साथ आता है। संकेत "समादेश बाएं A" "A: a" लेता है और "A+ B" प्रकार का एक प्रामाणिक पद देता है। इसी तरह, समादेश b" "b: B" लेता है और "A + B" प्रकार का एक विहित पद देता है। प्रारूप को एक निरसक फलन युग्म के साथ परिभाषित किया गया है जैसे कि एक प्रकार C और फलन F: A के लिए $\to$ c और g: b $\to$ c :

युग्म (समादेश बाएं a) c f g $\twoheadrightarrow$ (f a)
युग्म (समादेश दायें b) c f g $\twoheadrightarrow$ (g b)

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

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

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

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

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

R p pz ps 0 $\twoheadrightarrow$ PZ
R p pz ps (s $n$ ) $\twoheadrightarrow$ PS (R P PZ PS n)

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

योग: nat $\to$ nat $\to$ nat :: = R (λ n : nat। nat $\to$ nat) (λ n: nat। n) (λ g: nat $\to$ nat।(λ m: nat। SS (g m))

पहचान प्रकार

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

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

एक पहचान प्रकार के लिए एक ही प्रकार के दो पदों "a" और "b" की आवश्यकता होती है और इसे "a = b" लिखा जाता है। तो, "x + 1" और "1 + x" के लिए, प्रकार "x+1 = 1+x" होगा। प्रमाणिक पद संचरक "स्वतुल्यता" के साथ बनाए गए हैं। संकेत स्वतुल्यता a एक पद a लेता है और प्रारूप a = a का एक प्रामाणिक पद है।

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

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

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

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

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

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

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

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

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

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

समुच्चय सिद्धान्त में अनुमान और अभिगृहीत दोनों ही नियम हैं, जबकि प्रकार के सिद्धांतों में केवल नियम हैं। समुच्चय सिद्धान्त तर्क के शीर्ष पर बनाए गए हैं।इस प्रकार, ज़र्मेलो-फ्रेंकेल समुच्चय सिद्धान्त को प्रथम-क्रम तर्क और ज़र्मेलो-फ्रेंकेल समुच्चय सिद्धान्त अभिगृहीत के दोनों नियमों द्वारा परिभाषित किया गया है। (एक अभिगृहीत एक तार्किक व्युत्पत्ति के बिना सत्य के रूप में स्वीकार किया जाता है।) प्ररूप सिद्धांत, सामान्य रूप से, अभिगृहीत नहीं होते हैं और उनके नियमों के नियमों द्वारा परिभाषित होते हैं।
समुच्चय उपागम और तर्क में बाहर किए गए मध्य का नियम है।अर्थात्, हर प्रमेय सत्य या असत्य है। जब एक प्ररूप सिद्धांत और या या के रूप में अवधारणाओं को परिभाषित करता है, तो यह अंतर्ज्ञानवादी तर्क की ओर जाता है, जिसमें बाहर किए गए मध्य का नियम नहीं है। हालांकि, नियम कुछ प्रकार के लिए सिद्ध किया जा सकता है।
समुच्चय सिद्धान्त में, एक तत्व एक समुच्चय तक सीमित नहीं है। तत्व अन्य समुच्चयों के साथ उप-समुच्चय और समूहों में दिखाई दे सकता है। प्ररूप सिद्धांत में, पद (सामान्य रूप से) केवल एक प्रकार से संबंधित हैं। जहां एक उप-समुच्चय का उपयोग किया जाएगा, प्ररूप सिद्धांत एक विधेय (गणितीय तर्क) का उपयोग कर सकता है या एक निर्भर-प्रारूप उत्पाद प्रकार का उपयोग कर सकता है, जहां प्रत्येक तत्व $x$ एक प्रमाण के साथ जोड़ा जाता है कि उप-समुच्चय $x$ की गुण के लिए है। जहां एक समूह का उपयोग किया जाएगा, प्ररूप सिद्धांत योग प्रकार का उपयोग करता है, जिसमें नए प्रामाणिक पद सम्मिलित हैं।
प्ररूप सिद्धांत में गणना की एक अंतर्निहित धारणा है। इस प्रकार, 1+1 और 2 प्ररूप सिद्धांत में अलग -अलग पद हैं, लेकिन वे एक ही मूल्य की गणना करते हैं। इसके अतिरिक्त, फलनों को गणनीय रूप से लैम्ब्डा शर्तों के रूप में परिभाषित किया गया है। समुच्चय सिद्धान्त में, 1+1 = 2 का अर्थ है कि 1+1 मान 2 को संदर्भित करने का सिर्फ एक और तरीका है। प्ररूप सिद्धांत की गणना में समानता की एक जटिल अवधारणा की आवश्यकता होती है।
समुच्चय सिद्धान्त सामान्य रूप से संख्याओं को समुच्चय के रूप में एन्कोड करता है। (0 रिक्त समुच्चय है, 1 समुच्चय है जिसमें रिक्त समुच्चय है। प्राकृतिक संख्याओं की समुच्चय-सैद्धांतिक परिभाषा देखें।) प्रकार सिद्धांत चर्च एन्कोडिंग या अधिक स्वाभाविक रूप से आगमनात्मक प्रकारों का उपयोग करके फलनों के रूप में संख्याओं को एन्कोड कर सकता है। आगमनात्मक प्रकार द्वारा बनाए गए रचनाकार "0" और "S" पियानो के स्वयंसिद्धों के समान हैं।
समुच्चय उपागम में समुच्चय-संचरक सांकेतिक है। यह कोई भी समुच्चय बना सकता है जिसे परिभाषित किया जा सकता है। यह इसे अत्यधिक समुच्चय बनाने की अनुमति देता है। प्ररूप सिद्धांत सिंटेक्स हैं, जो उन्हें एक गिनने योग्य अनंत पदों तक सीमित करते हैं। इसके अतिरिक्त, अधिकांश प्रकार के सिद्धांतों को हमेशा रुकने और स्वयं को पुनरावर्ती रूप से उत्पन्न करने योग्य शर्तों तक सीमित करने के लिए गणना की आवश्यकता होती है। परिणामस्वरूप, अधिकांश प्रकार के सिद्धांत वास्तविक संख्याओं और गणना योग्य संख्याओं का उपयोग नहीं करते हैं।
समुच्चय सिद्धांत में, चयन का अभिगृहीत स्वयंसिद्ध है और विवादास्पद है, विशेषकर जब अत्यधिक समुच्चय पर लागू किया जाता है। प्रारूप सिद्धांत में, समतुल्य कथन एक प्रमेय (प्रकार) है और सिद्ध (एक पद द्वारा बना हुआ) है।
प्ररूप सिद्धांत में, प्रमाण गणितीय वस्तुएं हैं। प्रारूप X+1 = 1+x का उपयोग तब तक नहीं किया जा सकता जब तक कि प्रकार का पद न हो। यह पद एक प्रमाण का प्रतिनिधित्व करता है कि x+1 = 1+x है। इस प्रकार, प्ररूप सिद्धांत गणितीय वस्तुओं के रूप में अध्ययन किए जाने वाले प्रमाणों को प्रारंभ है।

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

तकनीकी विवरण

प्ररूप सिद्धांत एक गणितीय तर्क है। यह अनुमान के नियम का एक संग्रह है जो निर्णय (गणितीय तर्क) में परिणाम करता है।अधिकांश तर्क में निर्णय होते हैं जिसका अर्थ है "पद x सत्य है।" या "पद x एक सुनिर्मित सूत्र है।"^[6] प्ररूप सिद्धांत में अतिरिक्त निर्णय होते हैं जो प्रकारों और संबंधित पदों को प्रकारों तक परिभाषित करते हैं।

शर्तें

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

निर्णय

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

$T$ एक प्रकार है।
$t$ प्रकार का एक पद $T$ है।
प्रकार $T_{1}$ प्रकार के बराबर $T_{2}$ है।
शर्तें $t_{1}$ और $t_{2}$ दोनों प्रकार के $T$ और समान हैं।

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

x:bool, y:nat $\vdash$ (if x y y): nat

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

$\vdash$ S: nat $\to$ nat

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

निर्णय के लिए औपचारिक संकेतन	विवरण
$\Gamma \vdash T$ प्रारूप	$T$ क प्रकार है (धारणाओं के अंतर्गत $\Gamma$ )
$\Gamma \vdash t:T$	$t$ प्रकार का पद है $T$ (धारणाओं के अंतर्गत $\Gamma$ )
$\Gamma \vdash T_{1}=T_{2}$	प्रारूप $T_{1}$ प्रारूप के समान है $T_{2}$ (धारणाओं के अंतर्गत $\Gamma$ )
$\Gamma \vdash t_{1}=t_{2}:T$	पद $t_{1}$ और $t_{2}$ दोनों प्रारूप के हैं $T$ और समान है (धारणाओं के अंतर्गत $\Gamma$ )

(ध्यान दें: शर्तों की समानता का निर्णय वह है जहां वाक्यांश "न्यायिक समानता" आता है।)

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

नियम

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

{\begin{array}{c}\Gamma ,a:A\vdash b:B\\\hline \Gamma \vdash (\lambda a:A.b):A\to B\\\end{array}}

लैम्ब्डा पद बनाने के लिए आवश्यक निर्णय लाइन से ऊपर जाते हैं। इस स्थिति में, केवल एक निर्णय की आवश्यकता है। यह है कि कुछ प्रकार b का कुछ पद B है, यह मानते हुए कि कुछ प्रकार "" का कुछ पद "a" और कुछ अन्य धारणाएं

\Gamma

है। (टिप्पणी:

\Gamma

"a", "A", "b", और "B" सभी नियम में अधिचर हैं।) परिणामी निर्णय रेखा के नीचे जाता है। इस नियम के परिणामी निर्णय में कहा गया है कि नए लैम्ब्डा पद में अन्य धारणाओ

\Gamma

के अंतर्गत "A

\to

B प्रकार है।

नियम वाक्यात्मक हैंऔर पुनर्लेखन द्वारा कार्य करते हैं। इस प्रकार, परिवर्ती जैसे $\Gamma$ , "a", "A", आदि वास्तव में जटिल पदों से मिलकर बने हो सकते हैं जिनमें कई फलन अनुप्रयोग होते हैं, न कि केवल एकल प्रतीकों मे होते है।

प्ररूप सिद्धांत में एक विशेष निर्णय उत्पन्न करने के लिए, इसे उत्पन्न करने के लिए एक नियम होना चाहिए। फिर, उस नियम के सभी आवश्यक निविष्‍ट उत्पन्न करने के लिए नियम होने चाहिए। और फिर उन नियमों के लिए सभी निविष्‍ट के लिए लागू नियम एक प्रमाण वृक्ष बनाते हैं। यह सामान्य रूप से जेंटजन-शैली में तैयार किया जाता है,^[7] जहां लक्ष्य निर्णय (रूट) सबसे नीचे है और नियमों को शीर्ष पर किसी भी निविष्‍ट (पत्तियों) की आवश्यकता नहीं है ( प्राकृतिक निगमन प्रमाण_और_प्रारूप _सिद्धांत देखें) देखें। एक नियम का एक उदाहरण जिसमें किसी भी निविष्‍ट की आवश्यकता नहीं होती है, वह है जो बताता है कि NAT का एक पद 0 है:

{\begin{array}{c}\hline \vdash 0:nat\\\end{array}}

प्ररूप सिद्धांत में सामान्य रूप से कई नियम होते हैं, जिनमें सम्मिलित हैं:

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

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

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

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

मार्टिन-लोफ के अंतर्ज्ञानवादी प्रकार के सिद्धांत के नियम
होमोटॉपी प्ररूप सिद्धांत पुस्तक का परिशिष्ट A.2

प्रारूप सिद्धांतों के गुण

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

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

प्रारूपों के कुछ संयोजन प्रकार के अन्य संयोजनों के बराबर हैं। जब कार्यों को घातांक माना जाता है, तो प्रकारों के संयोजन को बीजगणितीय पहचान के समान लिखा जा सकता है।^[8] इस प्रकार, ${\mathbb {0} }+A\cong A$ , ${\mathbb {1} }\times A\cong A$ , ${\mathbb {1} }+{\mathbb {1} }\cong {\mathbb {2} }$ , $A^{B+C}\cong A^{B}\times A^{C}$ , $A^{B\times C}\cong (A^{B})^{C}$ ।

अभिगृहीत

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

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

यदि वे उन शर्तों पर गणना करने के तरीके के बिना शर्तों का उपक्रम देते हैं, तो अभिगृहीत समस्याओं का कारण बन सकते हैं। अर्थात्, अभिगृहीत प्ररूप सिद्धांत के सामान्य रूप (अमूर्त पुनर्लेखन) के साथ अन्तःक्षेप कर सकते हैं।^[9] कुछ सामान्य रूप से सामना किए गए अभिगृहीत हैं:

अभिगृहीत k पहचान प्रमाणों की विशिष्टता सुनिश्चित करता है। यही है, कि पहचान प्रकार का प्रत्येक पद स्वतुल्यता के बराबर है।^[10]
एकपक्षीय अभिगृहीत मानता है कि प्रकारों की तुल्यता प्रकारों की समानता है। इस गुण में अनुसंधान ने घनीय प्ररूप सिद्धांत का नेतृत्व किया, जहां गुण एक अभिगृहीत की आवश्यकता के बिना रखती है।^[11]
बाहर किए गए मध्य का नियम प्रायः उन उपयोगकर्ताओं को पूरा करने के लिए जोड़ा जाता है जो अंतर्ज्ञानवादी तर्क के अतिरिक्त शास्त्रीय तर्क चाहते हैं।

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

निर्णय समस्याएं

प्ररूप सिद्धांत स्वाभाविक रूप से प्रारूप स्थिति की निर्णय समस्या से जुड़ा हुआ है।^[12]

प्रारूप स्थिति

प्रारूप स्थिति की निर्णय समस्या (द्वारा संक्षिप्त) $\exists e.\Gamma \vdash e:\tau ?$ ) है:

एक प्रकार का वातावरण

\Gamma

और एक प्रकार

\tau

, को देखते हुए, तय करें कि क्या कोई पद

e

सम्मिलित है जिसे प्रारूप के वातावरण

\tau

में प्रारूप

\Gamma

निर्दिष्ट किया जा सकता है।

गिरार्ड के विरोधाभास से पता चलता है कि करी-हावर्ड पत्राचार के साथ प्रारूप के स्थिति समष्टि एक प्रकार की प्रणाली की स्थिरता से दृढ़ता से संबंधित है। ध्वनि होने के लिए, ऐसी प्रणाली में निर्जन प्रकार होना चाहिए।

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

प्रारूप का अनुमान

कई कमानुदेश जो प्ररूप सिद्धांत (जैसे, अन्योन्य क्रियात्मक प्रमेय समर्थक) के साथ काम करते हैं, वे भी प्रारूप निष्कष करते हैं। यह उन्हें उन नियमों का चयन करने देता है जो उपयोगकर्ता द्वारा कम क्रियाओं के साथ उपयोगकर्ता चाहता है।

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

होमोटॉपी प्ररूप सिद्धांत अंतर्ज्ञानवादी प्ररूप सिद्धांत से भिन्न होता है जो अधिकतम समानता प्रारूप के संचालन से होता है। 2016 में घनीय प्ररूप सिद्धांत प्रस्तावित किया गया था, जो सामान्यीकरण के साथ एक समस्थेयता प्ररूप सिद्धांत है।^[14]^[11]

व्याख्या

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

प्रारूप प्रस्ताव हैं; शर्ते प्रमाण हैं

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

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

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

तर्क संचालिकाएँ "सभी के लिए" और "अस्तित्व में हैं" ने प्रति मार्टिन-लोफ़ को निर्भर प्रारूप सिद्धांत का आविष्कार करने के लिए प्रेरित किया।

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

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

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

चेतावनी: इस व्याख्या से बहुत भ्रम हो सकता है। एक प्ररूप सिद्धांत में बूल" प्रकार के सत्य और असत्य हो सकता है, जो एक बूलियन तर्क की तरह काम करता है, और साथ ही साथ "सत्य" (प्रमाणित) और "का प्रतिनिधित्व करने के लिए $\top$ और $\bot$ प्रारूप होते है। असत्य" (अप्रमाणित), प्रस्ताव के लिए एक अंतर्ज्ञानवादी तर्क के हिस्से के रूप में होते है।

इस अंतर्ज्ञानवादी व्याख्या के अंतर्गत, ऐसे सामान्य प्रकार हैं जो तार्किक संचालकों के रूप में कार्य करते हैं:

तर्क नाम	तर्क संकेतन	प्रकार संकेतन	प्रारूप नाम
सत्य	$\top$	$\top$	इकाई प्रारूप
असत्य	$\bot$	$\bot$	रिक्त प्रारूप
नहीं	$\neg A$	$A\to \bot$	रिक्त प्रारूप के फलन
निहितार्थ	$A\to B$	$A\to B$	फलन
और	$A\land B$	$A\times B$	उत्पाद प्रकार
या	$A\lor B$	$A+B$	योग प्रकार
सभी के लिए	$\forall a\in A,P(a)$	Π a : A . P(a)	आश्रित फलन
सम्मिलित	$\exists a\in A,P(a)$	Σ a : A . P(a)	आश्रित उत्पाद प्रकार

लेकिन इस व्याख्या के अंतर्गत, बीच में बहिष्कृत कोई नियम नहीं है। अर्थात्, प्रकार का कोई पद & pi;a ।a + (a) $\to \bot$ ) नहीं है ।

इसी तरह, कोई पुनरावृत्ति नहीं है। Π A प्रकार का कोई पद नहीं है। ((a $\to \bot$ ) $\to \bot$ ) $\to$ a (ध्यान दें: अंतर्ज्ञानवादी तर्क अनुमति देता है $\lnot \lnot \lnot A\to \lnot A$ और प्रकार का एक पद ((a) $\to \bot$ ) $\to \bot$ ) $\to \bot$ ) $\to$ (a $\to \bot$ )) है।

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

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

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

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

गैर-रचनात्मक प्रमाण का एक उदाहरण "विरोधाभास द्वारा प्रमाण" है। पहला चरण यह मानकर चल रहा है कि x की स्थिति नहीं है और विरोधाभास द्वारा इसका खंडन किया जा रहा है। उस चरण से निष्कर्ष "ऐसा नहीं है कि x सम्मिलित नहीं है"। अंतिम चरण है, द्विक निषेध द्वारा, यह निष्कर्ष निकालना कि x की स्थिति है। स्पष्ट होने के लिए, रचनात्मक गणित अभी भी "विरोधाभास द्वारा खंडन" की अनुमति देता है। यह साबित कर सकता है कि "ऐसा नहीं है कि x सम्मिलित नहीं है"। लेकिन रचनात्मक गणित द्विक निषेध को हटाने के अंतिम चरण को यह निष्कर्ष निकालने की अनुमति नहीं देता है कि x सम्मिलित है।^[15]

रचनात्मक गणित ने प्रायः अंतर्ज्ञानवादी तर्क का उपयोग किया है, जैसा कि ब्रौवर-हेटिंग-कोलमोगोरोव व्याख्या से स्पष्ट है।

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

नियम या धारणा द्वारा, एक प्रकार के सिद्धांत में गैर-रचनात्मक सुविधाओं को जोड़ना संभव है। इनमें निरंतरता वाले संचालक सम्मिलित हैं जैसे वर्तमान निरंतरता के साथ संकेत है। हालाँकि ये संचालक वांछनीय गुणों जैसे प्रामाणिकता और पैरा-मीट्रिकता को विभाजित करते हैं।

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

हालांकि श्रेणी सिद्धांत के लिए प्रारंभिक प्रेरणा मूलभूततावाद से बहुत दूर थी, लेकिन दोनों क्षेत्रों में गहरा संबंध था। जैसा कि जॉन लेन बेल लिखते हैं: "वास्तव में श्रेणियों को स्वयं एक निश्चित प्रकार के प्रकार के सिद्धांतों के रूप में देखा जा सकता है; यह तथ्य अकेले इंगित करता है कि प्रकार सिद्धांत श्रेणी सिद्धांत से बहुत अधिक निकटता से संबंधित है, जितना कि सिद्धांत को व्यवस्थित करना है।" संक्षेप में, एक श्रेणी को उसकी वस्तुओं को प्रकार (या प्रारूप) के रूप में देखकर एक प्रकार के सिद्धांत के रूप में देखा जा सकता है, अर्थात "सामान्य रूप से, एक श्रेणी को इसके संरचना से रहित प्रारूप सिद्धांत के रूप में माना जा सकता है।" इस प्रकार कई महत्वपूर्ण परिणाम सामने आते हैं।^[16]

कार्तीय बंद श्रेणियां टाइप किए गए λ-कलन (लैम्बेक, 1970) के अनुरूप हैं;
c-मोनोइड (उत्पादों और घातांक के साथ श्रेणियां और एक गैर-टर्मिनल वस्तुओ) अप्रकाशित λ-गणना (1980 के आसपास लैम्बेक और दाना स्कॉट द्वारा स्वतंत्र रूप से मनाया गया) के अनुरूप;
स्थानीय रूप से कार्टेशियन बंद श्रेणियां मार्टिन-लोफ प्रकार के सिद्धांतों (सीली, 1984) के अनुरूप हैं।

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

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

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

प्रमुख

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

गौण

ऑटोमैथ
समुच्चय प्ररूप सिद्धांत
यूटीटी (लुओ का आश्रित प्रकार का एकीकृत सिद्धांत)
कुछ प्रकार के संयोजन तर्क
अन्य लोग लैम्ब्डा घन में परिभाषित किए गए (जिसे शुद्ध प्रकार के प्रणाली के रूप में भी जाना जाता है)
अन्य नाम के अंतर्गत लैम्ब्डा गणना टाइप किया गया

सक्रिय अनुसंधान

समस्थेयता प्ररूप सिद्धांत प्रकारों की समानता की खोज करता है
घनीय प्रारूप उपागम समस्थेयता प्ररूप सिद्धांत का कार्यान्वयन है

अनुप्रयोग

गणितीय आधार

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

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

प्रमाण सहायक

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

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

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

प्रोग्रामिंग (क्रमादेशन) भाषाएँ

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

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

भाषाविज्ञान

प्ररूप सिद्धांत का व्यापक रूप से प्राकृतिक भाषाओं के शब्दार्थ के औपचारिक सिद्धांतों में विशेष रूप से मोंटेग व्याकरण और उसके वंशजों में उपयोग किया जाता है।^[18]^[19]^[20] विशेष रूप से, श्रेणीबद्ध व्याकरण और प्राक् समूह व्याकरण पदों के प्रकार (संज्ञा, क्रिया, आदि) को परिभाषित करने के लिए व्यापक रूप से प्रारूप संरचक का उपयोग करते हैं।

सबसे सामान्य निर्माण क्रमशः विशिष्ट और सत्यता मान के लिए मूल प्रकार e और t लेता है, और प्रकारों के समूह को पुनरावर्ती रूप से निम्नानुसार परिभाषित करता है:

यदि $a$ और $b$ प्रकार हैं, तो $\langle a,b\rangle$ है;
मूल प्रकारों के अतिरिक्त कुछ भी नहीं, और पूर्व भाग के माध्यम से उनसे क्या निर्माण किया जा सकता है, वे प्रकार है।

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

सामाजिक विज्ञान

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

यह भी देखें

गणित की आधार

अग्रिम पठन

Aarts, C.; Backhouse, R.; Hoogendijk, P.; Voermans, E.; van der Woude, J. (December 1992). "A Relational Theory of Datatypes". Technische Universiteit Eindhoven.
Andrews B., Peter (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (2nd ed.). Kluwer. ISBN 978-1-4020-0763-7.
Jacobs, Bart (1999). Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics. Vol. 141. Elsevier. ISBN 978-0-444-50170-7. Covers type theory in depth, including polymorphic and dependent type extensions. Gives categorical semantics.
Cardelli, Luca (1996). "Type Systems". In Tucker, Allen B. (ed.). The Computer Science and Engineering Handbook. CRC Press. pp. 2208–36. ISBN 9780849329098.
Collins, Jordan E. (2012). A History of the Theory of Types: Developments After the Second Edition of 'Principia Mathematica'. Lambert Academic Publishing. hdl:11375/12315. ISBN 978-3-8473-2963-3. 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'.
Constable, Robert L. (2012) [2002]. "Naïve Computational Type Theory" (PDF). In Schwichtenberg, H.; Steinbruggen, R. (eds.). Proof and System-Reliability. Nato Science Series II. Vol. 62. Springer. pp. 213–259. ISBN 9789401004138. Archived (PDF) from the original on 2022-10-09. Intended as a type theory counterpart of Paul Halmos's (1960) Naïve Set Theory
Coquand, Thierry (2018) [2006]. "Type Theory". Stanford Encyclopedia of Philosophy.
Thompson, Simon (1991). Type Theory and Functional Programming. Addison–Wesley. ISBN 0-201-41667-0.
Hindley, J. Roger (2008) [1995]. Basic Simple Type Theory. Cambridge University Press. ISBN 978-0-521-05422-5. A good introduction to simple type theory for computer scientists; the system described is not exactly Church's STT though. Book review
Kamareddine, Fairouz D.; Laan, Twan; Nederpelt, Rob P. (2004). A modern perspective on type theory: from its origins until today. Springer. ISBN 1-4020-2334-0.
Ferreirós, José; Domínguez, José Ferreirós (2007). "X. Logic and Type Theory in the Interwar Period". Labyrinth of thought: a history of set theory and its role in modern mathematics (2nd ed.). Springer. ISBN 978-3-7643-8349-7.
Laan, T.D.L. (1997). The evolution of type theory in logic and mathematics (PDF) (PhD). Eindhoven University of Technology. doi:10.6100/IR498552. ISBN 90-386-0531-5. Archived (PDF) from the original on 2022-10-09.

संदर्भ

↑ Balbaert, Ivo (2015) Getting Started With Julia Programming ISBN 978-1-78328-479-5
↑ docs.julialang.org v.1 Types
↑ Stanford Encyclopedia of Philosophy (rev. Mon Oct 12, 2020) Russell’s Paradox 3. Early Responses to the Paradox
↑ Church, Alonzo (1940). "A formulation of the simple theory of types". The Journal of Symbolic Logic. 5 (2): 56–68. doi:10.2307/2266170. JSTOR 2266170. S2CID 15889861.
↑ Rathjen, Michael (October 2005). "The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory". Synthese. 147: 81–120. doi:10.1007/s11229-004-6208-4. S2CID 143295. Retrieved September 21, 2022.
↑ Bauer, Andrej. "What exactly is a judgement?". mathoverflow. Retrieved 29 December 2021.
↑ Smith, Peter. "Types of proof system" (PDF). logicmatters.net. Archived (PDF) from the original on 2022-10-09. Retrieved 29 December 2021.
↑ Milewski, Bartosz. "Programming with Math (Exploring Type Theory)". YouTube.
↑ "Axioms and Computation". Theorem Proving in Lean. Retrieved 21 January 2022.
↑ "Axiom K". nLab.
↑ ^11.0 ^11.1 Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders (2016). "Cubical Type Theory: a constructive interpretation of the univalence axiom" (PDF). 21st International Conference on Types for Proofs and Programs (TYPES 2015). arXiv:1611.02108. doi:10.4230/LIPIcs.CVIT.2016.23 (inactive 31 December 2022). Archived (PDF) from the original on 2022-10-09.{{cite journal}}: CS1 maint: DOI inactive as of December 2022 (link)
↑ Henk Barendregt; Wil Dekkers; Richard Statman (20 June 2013). Lambda Calculus with Types. Cambridge University Press. p. 66. ISBN 978-0-521-76614-2.
↑ Heineman, George T.; Bessai, Jan; Düdder, Boris; Rehof, Jakob (2016). "A long and winding road towards modular synthesis". Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. ISoLA 2016. Lecture Notes in Computer Science. Vol. 9952. Springer. pp. 303–317. doi:10.1007/978-3-319-47166-2_21. ISBN 978-3-319-47165-5.
↑ Sterling, Jonathan; Angiuli, Carlo (2021-06-29). "Normalization for Cubical Type Theory". 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Rome, Italy: IEEE: 1–15. arXiv:2101.11479. doi:10.1109/LICS52264.2021.9470719. ISBN 978-1-6654-4895-6. S2CID 231719089.
↑ "proof by contradiction". nlab. Retrieved 29 December 2021.
↑ Bell, John L. (2012). "Types, Sets and Categories" (PDF). In Kanamory, Akihiro (ed.). Sets and Extensions in the Twentieth Century. Handbook of the History of Logic. Vol. 6. Elsevier. ISBN 978-0-08-093066-4.
↑ ETCS at the nLab
↑ Chatzikyriakidis, Stergios; Luo, Zhaohui (2017-02-07). Modern Perspectives in Type-Theoretical Semantics (in English). Springer. ISBN 978-3-319-50422-3.
↑ Winter, Yoad (2016-04-08). Elements of Formal Semantics: An Introduction to the Mathematical Theory of Meaning in Natural Language (in English). Edinburgh University Press. ISBN 978-0-7486-7777-1.
↑ Cooper, Robin. "Type theory and semantics in flux." Handbook of the Philosophy of Science 14 (2012): 271-323.

बाहरी संबंध

परिचयात्मक सामग्री

प्ररूप सिद्धांत NLAB पर, जिसमें कई विषयों पर लेख हैं।
intuitionistic प्ररूप सिद्धांत दर्शन के स्टैनफोर्ड एनसाइक्लोपीडिया में लेख
लैम्ब्डा गणना टाइप्स के साथ हेंक Barendregt द्वारा बुक
[https://hbr.github.io/lambda-calculus/cc-tex Calluss of Construstions/Typed Lambda Callus.
intuitionistic प्ररूप सिद्धांत प्रति मार्टिन-löf द्वारा नोट्स
मार्टिन-Löf के प्ररूप सिद्धांत में प्रोग्रामिंग बुक
homotopy प्ररूप सिद्धांत पुस्तक, जिसने एक गणितीय आधार के रूप में समस्थेयता प्ररूप सिद्धांत को प्रस्तावित किया।

उन्नत सामग्री

Robert L. Constable (ed.). "Computational type theory". Scholarpedia.
प्रकार फोरम & mdash;मॉडरेट ई-मेल फोरम कंप्यूटर साइंस में प्ररूप सिद्धांत पर ध्यान केंद्रित करते हुए, 1987 के बाद से काम कर रहा है।
nuprl पुस्तक।]
प्रकार प्रोजेक्ट लेक्चर नोट्स समर स्कूलों 2005-2008 का
- 2005 समर स्कूल में परिचयात्मक व्याख्यान हैं
ओरेगन प्रोग्रामिंग लैंग्वेजेस समर स्कूल, कई व्याख्यान और कुछ नोट्स।
- समर 2013 लेक्चर] पर
- समर 2015 प्रकार, तर्क, शब्दार्थ और सत्यापन
आंद्रेज बाउर का ब्लॉग

v t e कंप्यूटर विज्ञान
Note: This template roughly follows the 2012 ACM Computing Classification System.
हार्डवेयर	मुद्रित सर्किट बोर्ड परिधीय एकीकृत परिपथ बड़े पैमाने पर एकीकरण चिप पर सिस्टम (एसओसी) ऊर्जा की खपत (ग्रीन कंप्यूटिंग) इलेक्ट्रॉनिक डिजाइन स्वचालन हार्डवेयर एक्सिलरेशन
कंप्यूटर सिस्टम संगठन	कंप्यूटर आर्किटेक्चर अंतः स्थापित प्रणाली रीयल-टाइम कंप्यूटिंग निर्भरता
नेटवर्क	नेटवर्क आर्किटेक्चर नेटवर्क प्रोटोकॉल नेटवर्क घटक नेटवर्क अनुसूचक नेटवर्क प्रदर्शन मूल्यांकन नेटवर्क सेवा
सॉफ्टवेयर संगठन	दुभाषिया मध्यस्थ आभासी मशीन ऑपरेटिंग सिस्टम सॉफ्टवेयर गुणवत्ता
सॉफ्टवेयर नोटेशन और टूल्स	प्रोग्रामिंग प्रतिमान प्रोग्रामिंग भाषा संकलक डोमेन-विशिष्ट भाषा मॉडलिंग भाषा सॉफ्टवेयर फ्रेमवर्क समन्वित विकास पर्यावरण सॉफ्टवेयर विन्यास प्रबंधन सॉफ्टवेयर लाइब्रेरी सॉफ्टवेयर रिपोजिटरी
सॉफ्टवेयर डेवलपमेंट	नियंत्रण चर सॉफ्टवेयर विकास प्रक्रिया आवश्यकताओं के विश्लेषण सॉफ्टवेर डिज़ाइन सॉफ्टवेयर निर्माण सॉफ्टवेयर परिनियोजन सॉफ्टवेयर इंजीनियरिंग सॉफ्टवेयर की रखरखाव प्रोग्रामिंग टीम ओपन-सोर्स मॉडल
गणना का सिद्धांत	गणना का मॉडल औपचारिक भाषा ऑटोमेटा सिद्धांत कम्प्यूटेबिलिटी सिद्धांत कम्प्यूटेशनल जटिलता सिद्धांत तर्क शब्दार्थ
कलन विधि	एल्गोरिदम डिजाइन एल्गोरिदम का विश्लेषण एल्गोरिदमिक दक्षता यादृच्छिक एल्गोरिदम कम्प्यूटेशनल ज्यामिति
कंप्यूटिंग का गणित	गणित पृथक करें संभावना सांख्यिकी गणितीय सॉफ्टवेयर सूचना सिद्धांत गणितीय विश्लेषण संख्यात्मक विश्लेषण सैद्धांतिक कंप्यूटर विज्ञान
सूचना प्रणाली	डेटाबेस प्रबंधन प्रणाली सूचना भंडारण प्रणाली उद्यम सूचना प्रणाली सामाजिक सूचना प्रणाली भौगोलिक सूचना प्रणाली निर्णय समर्थन प्रणाली प्रक्रिया नियंत्रण प्रणाली मल्टीमीडिया सूचना प्रणाली डेटा माइनिंग डिजिटल लाइब्रेरी कंप्यूटिंग प्लेटफॉर्म डिजिटल विपणन वर्ल्ड वाइड वेब सूचना की पुनर्प्राप्ति
सुरक्षा	क्रिप्टोग्राफी औपचारिक तरीके सुरक्षा सेवाएं अतिक्रमण संसूचन प्रणाली हार्डवेयर सुरक्षा नेटवर्क सुरक्षा सूचना सुरक्षा आवेदन सुरक्षा
मानव-कंप्यूटर संपर्क	पारस्परिक प्रभाव वाली डिज़ाइन सामाजिक कंप्यूटिंग सर्वव्यापक कंप्यूटिंग विज़ुअलाइज़ेशन एक्सेसिबिलिटी
Concurrency	समवर्ती कंप्यूटिंग समानांतर कंप्यूटिंग वितरित अभिकलन मल्टीथ्रेडिंग मल्टीप्रोसेसिंग
कृत्रिम बुद्धि	प्राकृतिक भाषा प्रसंस्करण ज्ञान प्रतिनिधित्व और तर्क कंप्यूटर दृष्टी स्वचालित योजना और समय-निर्धारण खोज पद्धति नियंत्रण विधि कृत्रिम बुद्धि का दर्शन डिस्ट्रिब्यूटेड आर्टिफिशियल इंटेलिजेंस
मशीन लर्निंग	पर्यवेक्षित अध्ययन अनपर्यवेक्षित लर्निंग सुदृढीकरण सीखना बहु-कार्य सीखने क्रॉस-सत्यापन
ग्राफिक्स	एनिमेशन रेंडरिंग छवि हेरफेर ग्राफ़िक्स प्रोसेसिंग युनिट मिश्रित वास्तविकता आभासी वास्तविकता छवि संपीड़न सॉलिड मॉडलिंग
एप्लाइड कंप्यूटिंग	ई-कॉमर्स उपक्रम सॉफ्टवेयर कम्प्यूटेशनल गणित कम्प्यूटेशनल भौतिकी कम्प्यूटेशनल केमिस्ट्री कम्प्यूटेशनल बायोलॉजी कम्प्यूटेशनल सामाजिक विज्ञान कम्प्यूटेशनल इंजीनियरिंग कम्प्यूटेशनल हेल्थकेयर डिजिटल कला इलेक्ट्रॉनिक प्रकाशन सायबर युद्ध इलेक्ट्रॉनिक वोटिंग वीडियो गेम वर्ड प्रोसेसिंग संचालन अनुसंधान शैक्षिक प्रौद्योगिकी दस्तावेज़ प्रबंधन
Category Outline WikiProject Commons

गणितीय तर्क

आम

प्रमेय ( सूची
& amp; विरोधाभास

तर्क

पारंपरिक	शास्त्रीय तर्क तार्किक सत्य टॉटोलॉजी प्रस्ताव अनुमान तार्किक समतुल्यता गाढ़ापन समानता तर्क ध्वनि वैधता युक्तिवाक्य विरोध का वर्ग वेन आरेख
प्रस्ताव	बूलियन बीजगणित बूलियन फ़ंक्शन तार्किक संयोजी प्रस्ताव पथरी प्रस्ताव सूत्र ट्रुथ टेबल कई-मूल्यवान तर्क 3 परिमित अनंत-मूल्यवान लॉजिक
विधेय	प्रथम-क्रम list दूसरा-आदेश मोनाडिक उच्च-क्रम मुक्त क्वांटिफायर विधेय मोनाडिक विधेय कैलकुलस

समुच्चय सिद्धान्त

सेट वंशानुगत वर्ग ( उर-) तत्व क्रमित युग्म क्रमसूचक संख्या सबसेट समानता विस्तार फोर्सिंग संबंध समतुल्यता विभाजन संचालन सेट करें: चौराहा संघ पूरक कार्तीय गुणन सत्ता स्थापित पहचान
सेट के प्रकार	काउंट करने योग्य बेशुमार खाली निवास सिंगलटन परिमित अनंत सकर्मक अल्ट्राफिल्टर पुनरावर्ती फजी यूनिवर्सल ब्रह्मांड निर्माण योग्य Grothendieck वॉन न्यूमैन
मानचित्र & amp; कार्डिनलिटी	फ़ंक्शन/ मानचित्र डोमेन कोडोमैन [[छवि (गणित) \|Image]] In/Sur/Bi-jection Schröder–Bernstein theorem Isomorphism Gödel numbering Enumeration Large cardinal Inaccessible Aleph number Operation Binary
सिद्धांत सेट करें	Zermelo -Fraenkel पसंद का स्वयंसिद्ध सातत्य परिकल्पना सामान्य क्रिपके -प्लाटेक मोर्स -केली भोला नई नींव टार्स्की -ग्रोथेन्डिंक वॉन न्यूमैन -बर्नेज़ -गोदेल रचनात्मक

औपचारिक प्रणाली (list),
भाषा & amp; सिंटैक्स

Example axiomatic
systems (list)

प्रूफ थ्योरी

मॉडल सिद्धांत

कम्प्यूटिबिलिटी थ्योरी

@@ Line 1: / Line 1: @@
 {{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>}} इस प्रकार किसी इकाई को स्वयं का उपयोग करके परिभाषित करने से रोकती हैं। रसेल के  प्ररूप सिद्धांत ने स्वयं को  समूह के सदस्य होने की संभावना को अस्वीकृत कर दिया।
+सहज समुच्चय सिद्धान्त और [[औपचारिक तर्क]] के आधार पर एक गणितीय आधार में एक विरोधाभास से बचने के लिए प्ररूप सिद्धांत बनाया गया था। बर्ट्रेंड रसेल द्वारा खोजा गया रसेल का विरोधाभास सम्मिलित था क्योंकि एक समुच्चय को "सभी संभव समुच्चयों" का उपयोग करके परिभाषित किया जा सकता था जिसमें वे स्वयं सम्मिलित थे। बर्ट्रेंड रसेल ने 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> औपचारिक प्रणाली को क्लेन -रॉसर विरोधाभास से बचने में सहायता की जो मूल अप्रकाशित लैम्ब्डा गणना से  प्रभावित था। चर्च ने प्रदर्शित किया कि यह गणित की आधार  के रूप में काम कर सकता है और इसे उच्च-क्रम के तर्क के रूप में संदर्भित किया गया था।
+सबसे प्रसिद्ध प्रारंभिक उदाहरण चर्च का टाइप किया गया लैम्ब्डा गणना है। चर्च के प्रकारों का सिद्धांत<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> सामान्य रूप से लैम्ब्डा गणना के आसपास आधारित एक  प्ररूप प्रणाली को संदर्भित करता है। एक प्रभावशाली प्रणाली प्रति मार्टिन-लोफ का अंतर्ज्ञानवादी प्रकार का सिद्धांत है, जिसे रचनात्मक गणित की नींव के रूप में प्रस्तावित किया गया था। और अन्य थियरी कोक्वांड का निर्माणों का कलन, जिसका उपयोग कोक, लीन और अन्य "प्रमाण सहायक" (कम्प्यूटरीकृत प्रमाण लेखन क्रमादेश) द्वारा नींव के रूप में किया जाता है।  प्ररूप सिद्धांत सक्रिय अनुसंधान का एक क्षेत्र है, जैसा कि  समस्थेयता प्ररूप सिद्धांत द्वारा प्रदर्शित किया गया है।
+वाक्यांश <nowiki>''</nowiki> प्ररूप सिद्धांत<nowiki>''</nowiki> सामान्य रूप से लैम्ब्डा गणना के आसपास आधारित एक प्ररूप प्रणाली को संदर्भित करता है। एक प्रभावशाली प्रणाली प्रति मार्टिन-लोफ का अंतर्ज्ञानवादी प्रकार का सिद्धांत है, जिसे रचनात्मक गणित की नींव के रूप में प्रस्तावित किया गया था। और अन्य थियरी कोक्वांड का निर्माणों का कलन, जिसका उपयोग कोक, लीन और अन्य "प्रमाण सहायक" (कम्प्यूटरीकृत प्रमाण लेखन क्रमादेश) द्वारा नींव के रूप में किया जाता है। प्ररूप सिद्धांत सक्रिय अनुसंधान का एक क्षेत्र है, जैसा कि समस्थेयता प्ररूप सिद्धांत द्वारा प्रदर्शित किया गया है।
 == परिचय ==
@@ Line 21: / Line 21: @@
 ==== नियम और प्रकार ====
-प्ररूप सिद्धांत में, प्रत्येक शब्द का एक प्रकार होता है। एक शब्द और इसके प्रकार को प्रायः "शब्द: प्रकार" के रूप में एक साथ लिखा जाता है।  प्ररूप सिद्धांत में सम्मिलित करने के लिए एक सामान्य प्रकार [[प्राकृतिक संख्या]] है, जिसे प्रायः "<math>\mathbb N</math><nowiki>''</nowiki> or "nat" लिखा जाता है। दूसरा बूलियन तर्क मान है। तो, उनके प्रकारों के साथ कुछ बहुत ही सरल शब्द है
+प्ररूप सिद्धांत में, प्रत्येक पद का एक प्रकार होता है। एक पद और इसके प्रकार को प्रायः "पद: प्रकार" के रूप में एक साथ लिखा जाता है। प्ररूप सिद्धांत में सम्मिलित करने के लिए एक सामान्य प्रकार [[प्राकृतिक संख्या]] है, जिसे प्रायः "<math>\mathbb N</math><nowiki>''</nowiki> or "nat" लिखा जाता है। दूसरा बूलियन तर्क मान है। तो, उनके प्रकारों के साथ कुछ बहुत ही सरल पद है
 * 1 : nat
@@ Line 27: / Line 27: @@
 * true : bool
-फलन  संकेत का उपयोग करके शर्तों को अन्य शर्तों से बनाया जा सकता है। प्ररूप सिद्धांत में, एक फलन  संकेत को फलन अनुप्रयोग कहा जाता है। फलन अनुप्रयोग किसी दिए गए प्ररूप का शब्द लेता है और किसी अन्य प्रकार के शब्द में परिणाम देता है। पारंपरिक "फलन (तर्क, तर्क, ...)" के अतिरिक्त फलन अनुप्रयोग को "फलन तर्क तर्क ..." लिखा गया है। प्राकृतिक संख्याओं के लिए, "योग" नामक फलन को परिभाषित करना संभव है जो दो प्राकृतिक संख्याओं को लेता है। इस प्रकार, उनके प्रारूपों के साथ कुछ और पद इस प्रकार हैं:
+फलन संकेत का उपयोग करके शर्तों को अन्य शर्तों से बनाया जा सकता है। प्ररूप सिद्धांत में, एक फलन संकेत को फलन अनुप्रयोग कहा जाता है। फलन अनुप्रयोग किसी दिए गए प्ररूप का पद लेता है और किसी अन्य प्रकार के पद में परिणाम देता है। पारंपरिक "फलन (तर्क, तर्क, ...)" के अतिरिक्त फलन अनुप्रयोग को "फलन तर्क तर्क ..." लिखा गया है। प्राकृतिक संख्याओं के लिए, "योग" नामक फलन को परिभाषित करना संभव है जो दो प्राकृतिक संख्याओं को लेता है। इस प्रकार, उनके प्रारूपों के साथ कुछ और पद इस प्रकार हैं:
 * add 0 0 : nat
@@ Line 33: / Line 33: @@
 *add 1 (add 1 (add 1 0)) : nat
-अंतिम अवधि में, संक्रिया के क्रम को इंगित करने के लिए कोष्ठक जोड़े गए थे। तकनीकी रूप से, अधिकांश प्रकार के सिद्धांतों को कोष्ठक को प्रत्येक संक्रिया के लिए सम्मिलित होने की आवश्यकता होती है, लेकिन, व्यवहार में, वे नहीं लिखे जाते हैं और लेखक मानते हैं कि पाठक यह जानने के लिए पूर्वता और सहयोगी का उपयोग कर सकते हैं कि वे कहां हैं। इसी तरह की आसानी के लिए, <math>x + y</math> के अतिरिक्त <math>x</math> <math>y</math> लिखना एक सामान्य संकेत है। इसलिए, उपरोक्त शर्तों को पुनः  लिखा जा सकता है:
+अंतिम अवधि में, संक्रिया के क्रम को इंगित करने के लिए कोष्ठक जोड़े गए थे। तकनीकी रूप से, अधिकांश प्रकार के सिद्धांतों को कोष्ठक को प्रत्येक संक्रिया के लिए सम्मिलित होने की आवश्यकता होती है, लेकिन, व्यवहार में, वे नहीं लिखे जाते हैं और लेखक मानते हैं कि पाठक यह जानने के लिए पूर्वता और सहयोगी का उपयोग कर सकते हैं कि वे कहां हैं। इसी तरह की आसानी के लिए, <math>x + y</math> के अतिरिक्त <math>x</math> <math>y</math> लिखना एक सामान्य संकेत है। इसलिए, उपरोक्त शर्तों को पुनः लिखा जा सकता है:
 * 0 + 0: nat
@@ Line 39: / Line 39: @@
 * 1 + (1 + (1 + 0)): nat
-शर्तों में चर भी सम्मिलित हो सकते हैं। चर में हमेशा एक प्ररूप होता है। इसलिए, "x" और "y" को "nat" प्रकार के चर मानते हुए, निम्नलिखित भी मान्य शब्द हैं:
+शर्तों में चर भी सम्मिलित हो सकते हैं। चर में हमेशा एक प्ररूप होता है। इसलिए, "x" और "y" को "nat" प्रकार के चर मानते हुए, निम्नलिखित भी मान्य पद हैं:
 * x: nat
@@ Line 45: / Line 45: @@
 * x + (x + y): NAT
-"नेट" और "बूल" से अधिक प्रकार हैं। हम पहले ही "योग" शब्द देख चुके हैं, जो "नेट" नहीं है, लेकिन एक फलन है, जब दो "नेट" पर लागू किया जाता है, तो "नेट" की गणना होती है। "योग" के प्रकार को बाद में आवृत किया जाएगा। सबसे पहले, हमें "गणना" का वर्णन करने की आवश्यकता है।
+"नेट" और "बूल" से अधिक प्रकार हैं। हम पहले ही "योग" पद देख चुके हैं, जो "नेट" नहीं है, लेकिन एक फलन है, जब दो "नेट" पर लागू किया जाता है, तो "नेट" की गणना होती है। "योग" के प्रकार को बाद में आवृत किया जाएगा। सबसे पहले, हमें "गणना" का वर्णन करने की आवश्यकता है।
 ==== गणना ====
@@ Line 55: / Line 55: @@
 * 0 + 5: nat
-लेकिन वे सभी शब्द 5:  nat की गणना करते हैं। प्ररूप सिद्धांत में,हम गणना को संदर्भित करने के लिए "कमी" और "कम" शब्दों का उपयोग करते हैं। तो, हम कहते हैं कि 0 + 5: NAT 5: NAT तक कम हो जाता है। इसे 0 + 5: NAT  <math>\twoheadrightarrow</math> 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" तक कम हो जाती हैं, जो कि एक प्रामाणिक शब्द है। प्राकृतिक संख्याओं की विहित शर्तें हैंː
+बिना किसी चर के एक शर्त जिसे अधिक कम नहीं किया जा सकता है, एक "प्रामाणिक शर्त" है। उपरोक्त सभी शर्तें "5: nat" तक कम हो जाती हैं, जो कि एक प्रामाणिक पद है। प्राकृतिक संख्याओं की प्रामाणिक शर्तें हैंː
-* 0:  nat
+* 0: nat
-* 1:  nat
+* 1: nat
-* 2:  nat
+* 2: nat
 * आदि।
-स्पष्टतः, एक ही पद के लिए गणना करने वाले पद समान होते हैं। तो, "x: nat" मानते हुए, "x + (1 + 4) : nat" और "x + (4 + 1) : nat" पद समान हैं क्योंकि वे दोनों "x + 5: 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 है।
+एक लैम्ब्डा पद "(λ चर नाम: टाइप 1 पद)" जैसा दिखता है और इसमें "टाइप 1 → टाइप 2" टाइप होता है। प्रकार "टाइप 1 → टाइप ''2''" इंगित करता है कि लैम्ब्डा पद एक ऐसा फलन है जो "टाइप 1" प्रकार का अंतःखंडी अनुपात लेता है और "टाइप 2" प्रकार के पद की गणना करता है। लैम्ब्डा पद के अंदर का पद "टाइप 2" का मान होना चाहिए, यह मानते हुए कि चर का प्रकार "टाइप 1" है।
-एक लैम्ब्डा शब्द का एक उदाहरण यह कार्य है जो अपने तर्क को दोगुना करता है:
+एक लैम्ब्डा पद का एक उदाहरण यह फलन है जो अपने तर्क को दोगुना करता है:
-* (λ x: nat। (x x जोड़ें)): nat <math>\to</math> नेट
+* (λ x : nat . (add x x)) : nat  na
-चर नाम x है और चर में NAT प्रकार है।शब्द (X X जोड़ें) में NAT है, X: NAT मानते हुए।इस प्रकार, लैम्ब्डा शब्द का प्रकार NAT है <math>\to</math>  nat, जिसका अर्थ है कि यदि इसे एक तर्क के रूप में एक NAT दिया जाता है, तो यह एक NAT की गणना करेगा।कमी (a.k.a गणना) को लैम्ब्डा शर्तों के लिए परिभाषित किया गया है।जब फलन लागू किया जाता है (a.k.a. कहा जाता है), तो तर्क पैरामीटर के लिए प्रतिस्थापन (बीजगणित) होता है।
+चर का नाम "x" है और चर का प्रकार "nat" है। पद "(योग X X )" में "x: nat" मानकर "nat" टाइप किया गया है। इस प्रकार, लैम्ब्डा पद का प्रकार "nat → nat" है, जिसका अर्थ है कि यदि इसे तर्क के रूप में "nat" दिया जाता है, तो यह "nat" की गणना करेगा। न्यूनीकरण (उर्फ अभिकलन) लैम्ब्डा शर्तों के लिए परिभाषित किया गया है। जब फलन लागू किया जाता है (जिसे उर्फ कहा जाता है), अंतःखंडी अनुपात के लिए तर्क प्रतिस्थापित किया जाता है।
-इससे पहले, हमने देखा कि फलन अनुप्रयोग को फलन टर्म के बाद पैरामीटर लगाकर लिखा गया है।इसलिए, यदि हम उपरोक्त फलन को NAT के पैरामीटर 5 के साथ  संकेत करना चाहते हैं, तो हम लिखते हैं:
+इससे पहले, हमने देखा कि फलन अनुप्रयोग को फलन पद के बाद अंतःखंडी अनुपात लगाकर लिखा गया है। इसलिए, यदि हम उपरोक्त फलन को NAT के अंतःखंडी अनुपात 5 के साथ स्थगित करना चाहते हैं, तो हम लिखते हैं:
-* (λ x: nat। (x x जोड़ें)) 5: nat
+* (λ x : nat . (add x x)) 5 : nat
-लैम्ब्डा शब्द टाइप  nat था <math>\to</math>  nat, जिसका मतलब था कि एक तर्क को एक तर्क के रूप में दिया गया, यह प्रकार NAT का एक शब्द का उत्पादन करेगा।चूंकि हमने इसे तर्क 5 दिया है, उपरोक्त शब्द में NAT है।कमी शब्द में पैरामीटर x के लिए तर्क 5 को प्रतिस्थापित करके काम करता है (एक्स एक्स जोड़ें), इसलिए शब्द की गणना:
+लैम्ब्डा पद प्रारूप "nat → nat" था, जिसका अर्थ था कि तर्क के रूप में "nat" दिया गया है, यह "nat" प्रकार का एक पद उत्पन्न करेगा। चूँकि हमने इसे "5" तर्क दिया है, उपरोक्त पद का प्रकार "nat" है। "(योग x x)" पद में अंतःखंडी अनुपात "x" के लिए तर्क "5" को प्रतिस्थापित करके कमी काम करती है, इसलिए पद की गणना होती है:
-* (5 5 जोड़ें): नेट
+* (add 5 5) : nat
 जो स्पष्ट रूप से गणना करता है
-* 10:  nat
+* 10: nat
-एक लैम्ब्डा शब्द को प्रायः एक अनाम कार्य कहा जाता है क्योंकि इसका कोई नाम नहीं है।प्रायः, चीजों को पढ़ने में आसान बनाने के लिए, एक नाम एक लैम्ब्डा शब्द को दिया जाता है।यह केवल एक संकेतन है और इसका कोई गणितीय अर्थ नहीं है।कुछ लेखक इसे उल्लेखनीय समानता कहते हैं।नोटेशन का उपयोग करके ऊपर के फलन को एक नाम दिया जा सकता है:
+लैम्ब्डा पद को प्रायः "अस्पष्ट फलन" कहा जाता है क्योंकि इसका कोई नाम नहीं है। प्रायः, वस्तुओ को पढ़ने में आसान बनाने के लिए लैम्ब्डा पद को एक नाम दिया जाता है। यह केवल एक अंकन है और इसका कोई गणितीय अर्थ नहीं है। कुछ लेखक इसे "सांकेतिक समानता" कहते हैं। सांकेतिक का उपयोग करके उपरोक्त फलन को एक नाम दिया जा सकता है
-* डबल:  nat <math>\to</math> nat :: = (λ x: nat। (x x जोड़ें))
+* double : nat  nat  ::= (λ x : nat . (add x x))
-यह ऊपर जैसा ही कार्य है, इसे लिखने का एक अलग तरीका है।तो शब्द
+यह उपरोक्त जैसा ही फलन है, इसे लिखने का एक अलग तरीका है। तो पद
-* डबल 5:  nat
+* double 5 : nat
 अभी भी गणना करता है
-* 10:  nat
+* 10: nat
-==== आश्रित टाइपिंग ====
+==== आश्रित प्ररूपण ====
-आश्रित टाइपिंग तब होती है जब किसी फलन द्वारा लौटा दिया जाता है, वह उसके तर्क के मूल्य पर निर्भर करता है।उदाहरण के लिए, जब एक  प्ररूप सिद्धांत में एक नियम होता है जो प्रकार के बूल को परिभाषित करता है, तो यह फलन को भी परिभाषित करता है।फलन यदि 3 तर्क लेते हैं और यदि सही b c B की गणना करता है और यदि FALSE B C C की गणना करता है।लेकिन यदि बी सी का प्रकार है तो क्या है?
+आश्रित प्ररूपण तब होता है जब किसी फलन द्वारा दिया गया प्रारूप उसके तर्क के मान पर निर्भर करता है। उदाहरण के लिए, जब एक प्ररूप सिद्धांत में एक नियम होता है जो प्रकार के बूल को परिभाषित करता है, तो यह <nowiki>'शर्त' फलन को भी परिभाषित करता है। फलन ''यदि'' 3 तर्क लेते हैं और ''यदि सही b c" "b" की गणना करता है और यदि असत्य b c" "c" की गणना करता है। लेकिन ''शर्त b c''</nowiki> का प्रारूप क्या है?
-यदि B और C का एक ही प्रकार है, तो यह स्पष्ट है: यदि B C का B और C के समान ही है।इस प्रकार, एक: बूल मानते हुए,
+यदि "b" और "c" का एक ही प्रकार है, तो यह स्पष्ट है: "यदि a b c" का "b" और "c" के समान प्रकार है। इस प्रकार, "a: बूल" मानते हुए,
-* यदि एक 2 4:  nat
+* यदि a 2 4: nat
-* यदि एक झूठा सच: बूल
+* यदि a असत्य सत्य है: बूल
-लेकिन यदि बी और सी के अलग -अलग प्रकार होते हैं, तो बी सी के मूल्य पर निर्भर करता है।हम प्रतीक & pi का उपयोग करते हैं;एक फलन को इंगित करने के लिए जो एक तर्क लेता है और एक प्रकार देता है।यह मानते हुए कि हमारे पास कुछ प्रकार हैं और सी और ए: बूल, बी: बी और सी: सी, फिर
+लेकिन यदि b और c के अलग -अलग प्रकार होते हैं, तो b c के मूल्य पर निर्भर करता है। हम प्रतीक "Π" का उपयोग करते हैं; एक फलन को इंगित करने के लिए जो एक तर्क लेता है और एक प्रकार देता है। यह मानते हुए कि हमारे पास b" और c "और" "a : bool", "b : B" और "c : C" हैं, तो
-* यदि a b c: (& pi; a: बूल। b। <math>\to</math> C <math>\to</math> यदि ए बी सी)
+* यदि a b c : (Π a : bool B→ C→ यदि a B C)
-यही है, IF शब्द का प्रकार या तो दूसरे या तीसरे तर्क का प्रकार है, जो पहले तर्क के मूल्य पर निर्भर करता है।वास्तविकता में, यदि A B C को IF का उपयोग करके परिभाषित नहीं किया गया है, लेकिन यह विवरण में इस परिचय के लिए बहुत जटिल हो जाता है।
+अर्थात्, "यदि" पद का प्रकार या तो दूसरे या तीसरे तर्क का प्रकार है, जो पहले तर्क के मान पर निर्भर करता है। वास्तव में, "यदि एक B C" को "यदि" का उपयोग करके परिभाषित नहीं किया गया है, लेकिन यह विवरण इस उपक्रम के लिए बहुत जटिल हो जाता है।
-क्योंकि प्रकार में गणना हो सकती है, निर्भर टाइपिंग आश्चर्यजनक रूप से शक्तिशाली है।जब गणितज्ञों का कहना है कि एक संख्या सम्मिलित है <math>x</math> ऐसा है कि <math>x</math> प्राइम है या एक नंबर सम्मिलित है <math>x</math> ऐसी गुण <math>P(x)</math> होल्ड्स, इसे एक आश्रित प्रकार के रूप में व्यक्त किया जा सकता है।अर्थात्, गुण विशिष्ट के लिए सिद्ध होती है<math>x</math>और यह परिणाम के प्रकार में दिखाई देता है।
+क्योंकि प्रकार में गणना हो सकती है, आश्रित टाइपिंग आश्चर्यजनक रूप से शक्तिशाली है। जब गणितज्ञों का कहना है कि एक संख्या <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>, वगैरह..
+Π-शर्तें एक प्रकार अप्रत्यागम हैं। तो उनका अप्रत्यागम मान किस प्रकार का है? पूर्ण रूप से एक प्रारूप होना चाहिए जिसमें प्रकार हों। एक प्रारूप जिसमें अन्य प्रकार होते हैं, उसे "विश्व समष्टि" कहा जाता है। इसे प्राय: <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>
@@ Line 136: / Line 136: @@
-=== नियम नियमों और शर्तों द्वारा सामान्य ===
+=== सामान्य "नियम द्वारा" प्रारूप और शर्तें ===
-प्रकार के सिद्धांतों को उनके नियम के नियम द्वारा परिभाषित किया गया है।एक कार्यात्मक कोर के लिए नियम हैं, जो ऊपर वर्णित हैं, और नियम जो प्रकार और शब्द बनाते हैं।नीचे सामान्य प्रकारों और उनके संबंधित शब्दों की एक गैर-थकाऊ सूची है।
+प्रकार के सिद्धांतों को उनके अनुमान के नियमों द्वारा परिभाषित किया गया है। ऊपर वर्णित "कार्यात्मक कोर" के लिए नियम हैं, और नियम जो प्रकार और शर्तें बनाते हैं। नीचे सामान्य प्रकारों और उनसे संबंधित पदों की एक गैर-विस्तृत सूची है।
-सूची आगमनात्मक प्रकारों के साथ समाप्त होती है, जो एक शक्तिशाली तकनीक है जो सूची में अन्य सभी लोगों का निर्माण करने में सक्षम है।प्रमाण सहायक कोक और लीन द्वारा उपयोग की जाने वाली गणितीय आधार  आगमनात्मक निर्माणों के लिए पथरी पर आधारित हैं जो आगमनात्मक प्रकारों के साथ निर्माणों (इसके कार्यात्मक कोर) की पथरी है।
+सूची "आगमनात्मक प्रकार" के साथ समाप्त होती है, जो एक शक्तिशाली तकनीक है जो सूची में अन्य सभी का निर्माण करने में सक्षम है। प्रमाण सहायक "कोक" और "लीन" द्वारा उपयोग किए जाने वाले गणितीय नींव "आगमनात्मक निर्माण के लिए कलन" पर आधारित हैं, जो आगमनात्मक प्रकारों के साथ "निर्माण की गणना" (इसका "कार्यात्मक कोर") है।
-==== [[खाली प्रकार]] ====
+==== [[खाली प्रकार|रिक्‍त प्रारूप]] ====
-खाली प्रकार की कोई शर्तें नहीं हैं।प्रकार सामान्य रूप से लिखा जाता है<math>\bot</math>या<math>\mathbb 0</math>।
+[[खाली प्रकार|रिक्‍त]] प्रारूप की कोई शर्तें नहीं हैं। प्रारूप सामान्य रूप से <nowiki>''</nowiki><math>\bot</math><nowiki>'' या ''</nowiki><math>\mathbb 0</math><nowiki>''</nowiki> मे लिखा जाता है।
-इसका उपयोग यह दिखाने के लिए किया जाता है कि कुछ अस्वीकार्य है।यदि एक प्रकार ए के लिए, आप टाइप ए का एक फलन बना सकते हैं <math>\to \bot</math>, आप जानते हैं कि ए की कोई शर्त नहीं है।टाइप ए के लिए एक उदाहरण हो सकता है एक संख्या सम्मिलित है <math>x</math> ऐसा दोनों <math>x</math> यहां तक कि और है <math>x</math> अजीब है ।(उदाहरण A का निर्माण कैसे किया जाता है, इसके लिए नीचे उत्पाद प्रकार देखें।) जब किसी प्रकार की कोई शर्तें नहीं हैं, तो हम कहते हैं कि यह निर्जन है।
+इसका उपयोग यह दिखाने के लिए किया जाता है कि कुछ अगणनीय है। यदि "A" प्रारूप के लिए, <nowiki>''A''</nowiki> <math>\to \bot</math> प्रकार का फलन बना सकते है, तो आप जानते हैं कि "A" में कोई पद नहीं है। "A" प्रारूप के लिए एक उदाहरण हो सकता है एक संख्या <math>x</math> सम्मिलित है जैसे दोनों <math>x</math> सम है और <math>x</math> विषम है। (उदाहरण A का निर्माण कैसे किया जाता है, इसके लिए नीचे उत्पाद प्रारूप देखें।) जब किसी प्रारूप की कोई शर्तें नहीं हैं, तो हम कहते हैं कि यह निर्जन है।
-==== इकाई प्रकार ====
+==== इकाई प्रारूप ====
-यूनिट प्रकार में बिल्कुल 1 विहित शब्द है।प्रकार लिखा है<math>\top</math>या<math>\mathbb 1</math>और एकल विहित शब्द लिखा गया है *।
+इकाई प्रारूप में 1 प्रामाणिक पद है। प्रारूप <nowiki>''</nowiki><math>\top</math><nowiki>'' या ''</nowiki><math>\mathbb 1</math><nowiki>''</nowiki> लिखा जाता है और एकल प्रामाणिक पद <nowiki>''</nowiki>*<nowiki>''</nowiki> लिखा जाता है।
-यूनिट प्रकार का उपयोग यह दिखाने के लिए किया जाता है कि कुछ सम्मिलित है या कम्प्यूटेशनल है।यदि एक प्रकार ए के लिए, आप प्रकार का एक फलन बना सकते हैं<math>\top \to</math> ए, आप जानते हैं कि ए में एक या एक से अधिक शब्द हैं।जब किसी प्रकार का कम से कम 1 शब्द होता है, तो हम कहते हैं कि यह बसा हुआ है।
+इकाई प्रारूप का उपयोग यह दिखाने के लिए किया जाता है कि कुछ सम्मिलित है या गणना योग्य है। यदि किसी प्रकार "A" के लिए, आप <nowiki>''</nowiki><math>\top \to</math>A" प्रकार का फलन बना सकते हैं, तो आप जानते हैं कि "A" में एक या अधिक पद हैं। जब किसी प्रकार में कम से कम 1 पद होता है, तो हम कहते हैं कि यह " सयात्रिक" है।
-==== बूलियन प्रकार ====
+==== बूलियन प्रारूप ====
-बूलियन प्रकार में ठीक 2 विहित शब्द हैं।प्रकार सामान्य रूप से बूल लिखा जाता है या<math>\mathbb B</math>या<math>\mathbb 2</math>।विहित शब्द सामान्य रूप से सही और झूठे होते हैं।
+बूलियन प्रारूप में 2 प्रामाणिक पद हैं। प्रारूप सामान्य रूप से र "बूल" या "<math>\mathbb B</math><nowiki>'' या ''</nowiki><math>\mathbb 2</math><nowiki>''</nowiki> लिखा जाता है। प्रामाणिक पद सामान्य रूप से "सत्य" और "असत्य" होते हैं।
-बूलियन प्रकार को एक एलिमिनेटर फलन के साथ परिभाषित किया गया है यदि ऐसा है:
+बूलियन प्रारूप को निराकरक फलन "यदि" के साथ परिभाषित किया गया है:
-* यदि सच बी सी <math>\twoheadrightarrow</math> बी
+* यदि सत्य b c <math>\twoheadrightarrow</math> b
-* यदि झूठी बी सी <math>\twoheadrightarrow</math> सी
+* यदि असत्य b c <math>\twoheadrightarrow</math> c
-==== उत्पाद प्रकार ====
+==== उत्पाद प्रारूप ====
-उत्पाद प्रकार में ऐसे शब्द होते हैं जिन्हें जोड़ी का आदेश दिया जाता है।प्रकार ए और बी के लिए, उत्पाद प्रकार लिखा जाता है <math>\times</math> बी ।कंस्ट्रक्टर फलन जोड़ी द्वारा कैनोनिकल शब्द बनाए जाते हैं।शब्द एक बी हैं, जहां ए टाइप ए का एक शब्द है और बी टाइप बी का एक शब्द है।उत्पाद प्रकार को पहले और दूसरे कार्य के साथ परिभाषित किया गया है जैसे:
+उत्पाद प्रारूप में ऐसे पद होते हैं जो क्रमित जोड़े होते हैं। प्रकार "A" और "B" के लिए, उत्पाद प्रारूप A <math>\times</math> B लिखा जाता है। संरचक फलन "जोड़ी" द्वारा प्रामाणिक पद बनाए जाते हैं। शर्तें "युग्म a b" हैं, जहां "a" प्रकार "A" का एक पद है और "b" प्रकार "B" का एक पद है। उत्पाद प्रकार को "प्रथम" और "द्वितीय" निरसक फलनों के साथ परिभाषित किया गया है:
-* पहला (जोड़ी ए बी) <math>\twoheadrightarrow</math> ए
+* प्रथम (युग्म a b) <math>\twoheadrightarrow</math> a
-* दूसरा (जोड़ी ए बी) <math>\twoheadrightarrow</math> बी
+* द्वितीय (युग्म a b) <math>\twoheadrightarrow</math> b
-ऑर्डर किए गए जोड़े के अतिरिक्त, इस प्रकार का उपयोग तार्किक संयोजन के लिए किया जाता है। तार्किक ऑपरेटर और, क्योंकि यह ए और ए बी रखता है।इसका उपयोग चौराहे के लिए भी किया जाता है, क्योंकि यह दोनों प्रकारों में से एक है।
+क्रमित किए गए युग्म के अतिरिक्त, इस प्रकार का उपयोग तार्किक संयोजन के लिए किया जाता है। क्योंकि इसमे A और B होते है। इसका उपयोग अन्तः क्रिया के लिए भी किया जाता है, क्योंकि यह दोनों प्रारूप में से एक को धारण करता है।
-यदि एक  प्ररूप सिद्धांत में निर्भर टाइपिंग है, तो इसमें निर्भर प्रकार है।एक आश्रित जोड़ी में, दूसरा प्रकार पहले शब्द के मान पर निर्भर करता है।इस प्रकार, प्रकार लिखा है<math>\Sigma</math> A: a।B (a) जहाँ b में टाइप A है <math>\to</math> यू।यह उपयोगी है जब गुण बी (ए) के साथ ए की अस्तित्वगत मात्रा का ठहराव दिखाते हैं।
+यदि एक प्ररूप सिद्धांत में निर्भर प्ररूपण है, तो इसमे आश्रित युग्म है एक आश्रित युग्म में, दूसरा प्रकार पहले पद के मान पर निर्भर करता है। इस प्रकार, प्रारूप <math>\Sigma</math> A: a।B (a) लिखा जाता है, जहाँ b में प्रारूप A <math>\to</math> U है। गुण "B(a)" के साथ "a" के स्थिति को दिखाते समय यह उपयोगी होता है।
-==== योग प्रकार ====
+==== योग प्रारूप ====
-योग प्रकार एक टैग किया गया संघ है।अर्थात्, A और B प्रकारों के लिए, टाइप A + B या तो टाइप A या टाइप B का शब्द है और यह जानता है कि यह कौन सा है।प्रकार कंस्ट्रक्टर्स इंजेक्शनलफ्ट और इंजेक्शनराइट के साथ आता है। संकेत इंजेक्शनल ए: ए: ए और टाइप ए + बी का एक विहित शब्द लौटाता है।इसी तरह, इंजेक्शनराइट B B: B: B और टाइप A + B का एक विहित शब्द लौटाता है।टाइप को एक एलिमिनेटर फलन मैच के साथ परिभाषित किया गया है जैसे कि एक प्रकार C और फलन F: A के लिए <math>\to</math> सी और जी: बी <math>\to</math> सी :
+योग प्रकार एक "चिह्नित संघ" है। अर्थात्, प्रकार "A" और "B" के लिए, प्रकार "A+ B" में या तो "ए" प्रकार का पद या "B" प्रकार का पद होता है और यह जानता है कि यह कौन सा है। प्रकार संचरक "समादेश बायाँ" और "समादेश दायाँ" के साथ आता है। संकेत "समादेश बाएं A" "A: a" लेता है और "A+ B" प्रकार का एक प्रामाणिक पद देता है। इसी तरह, समादेश b" "b: B" लेता है और "A + B" प्रकार का एक विहित पद देता है। प्रारूप को एक निरसक फलन युग्म के साथ परिभाषित किया गया है जैसे कि एक प्रकार C और फलन F: A के लिए <math>\to</math> c और g: b <math>\to</math> c :
-* मैच (इंजेक्शनलफ्ट ए) सी एफ जी <math>\twoheadrightarrow</math> (च ए)
+* युग्म (समादेश बाएं a) c f g <math>\twoheadrightarrow</math> (f a)
-* मैच (इंजेक्शनराइट बी) सी एफ जी <math>\twoheadrightarrow</math> (जी बी)
+* युग्म (समादेश दायें b) c f g <math>\twoheadrightarrow</math> (g b)
-योग प्रकार का उपयोग [[तार्किक या]] संघ (समुच्चय सिद्धान्त) के लिए किया जाता है।
+योग प्रारूप का उपयोग [[तार्किक या]] संघ (समुच्चय सिद्धान्त) के लिए किया जाता है।
 ==== प्राकृतिक संख्या ====
-प्राकृतिक संख्या सामान्य रूप से मीनो अंकगणित की शैली में लागू की जाती है।एक विहित शब्द है, 0:  nat फॉर शून्य।शून्य से बड़ा कैनोनिकल मान कंस्ट्रक्टर फलन का उपयोग करें: NAT <math>\to</math>  nat।इस प्रकार, s 0 एक है।S (S 0) दो है।S (S 0))) तीन है।आदि दशमलव संख्या केवल उन शर्तों के बराबर है।
+प्राकृतिक संख्या सामान्य रूप से पियानो अंकगणित की शैली में लागू की जाती है। शून्य के लिए एक विहित पद "0: nat" है। शून्य से बड़ा विहित मान संचरक फलन NAT <math>\to</math> nat का उपयोग करते है। इस प्रकार, "S 0" एक है। "S (S 0)" दो है। "S (S (S 0)))" तीन आदि है। दशमलव संख्याएँ केवल सांकेतिक रूप से उन पदों के बराबर होती हैं।
 * 1: nat :: = s 0
@@ Line 192: / Line 192: @@
 * ...
-प्राकृतिक संख्याओं को एक एलिमिनेटर फलन R के साथ परिभाषित किया गया है जो सभी NATs के लिए एक फलन को परिभाषित करने के लिए पुनरावृत्ति का उपयोग करता है।यह एक फलन P: NAT लेता है <math>\to</math> यू जो परिभाषित करने के लिए फलन का प्रकार है।यह एक शब्द PZ: P 0 भी लेता है जो शून्य पर मान है और एक फलन PS: P n <math>\to</math> P (s n) जो कहता है कि N + 1 पर मान को मान में मान को कैसे बदलना है।इस प्रकार, इसके गणना नियम हैं:
+प्राकृतिक संख्याओं को एक विलोपक फलन R के साथ परिभाषित किया गया है जो सभी NATs के लिए एक फलन को परिभाषित करने के लिए पुनरावृत्ति का उपयोग करता है। यह एक फलन P: NAT <math>\to</math> U लेता है जो परिभाषित करने के लिए फलन का प्रकार है। यह एक पद PZ: P 0 भी है जो शून्य पर मान है और एक फलन PS: P n <math>\to</math> P (s n) है,जो बताता है कि "n" के मान को "पर मान में N + 1 मान को कैसे बदलना है। इस प्रकार, इसके गणना नियम हैं:
-* R p pz ps 0 <math>\twoheadrightarrow</math> पेज
+* R p pz ps 0 <math>\twoheadrightarrow</math> PZ
-* R p pz ps (s <math>n</math>) <math>\twoheadrightarrow</math> पीएस (आर पी पीजेड पीएस <math>n</math>)
+* R p pz ps (s <math>n</math>) <math>\twoheadrightarrow</math> PS (R P PZ PS n)
-फलन ऐड, जिसका उपयोग पहले किया गया था, को आर का उपयोग करके परिभाषित किया जा सकता है।
+फलन योग, जिसका उपयोग पहले किया गया था, और R का उपयोग करके परिभाषित किया जा सकता है।
-* जोड़ें:  nat<math>\to</math>नेट<math>\to</math>रात :: = आर (λ एन: रात। रात<math>\to</math>nat) (λ n: nat। n) (λ g: nat<math>\to</math> nat।(λ एम:  nat। एस (जी एम))
+* योग: nat<math>\to</math>nat <math>\to</math>nat :: = R (λ n : nat। nat<math>\to</math>nat) (λ n: nat। n) (λ g: nat<math>\to</math> nat।(λ m: nat। SS (g m))
-{{anchor|Equality types}}
 ==== पहचान प्रकार ====
-पहचान प्रकार  प्ररूप सिद्धांत में समानता की तीसरी अवधारणा है।पहला उल्लेखनीय समानता है, जो 2: nat :: = (s 0)) जैसी परिभाषाओं के लिए है, जिसका कोई गणितीय अर्थ नहीं है, लेकिन पाठकों के लिए उपयोगी है।दूसरा निर्णय समानता है, जो तब होता है जब दो शब्द एक ही शब्द की गणना करते हैं, जैसे कि x + (1 + 4) और x + (4 + 1), जो दोनों x + 5 से गणना करते हैं।लेकिन  प्ररूप सिद्धांत को समानता के एक और रूप की आवश्यकता होती है, जिसे पहचान प्रकार या प्रस्ताव समानता के रूप में जाना जाता है।
+पहचान प्रकार प्ररूप सिद्धांत में समानता की तीसरी अवधारणा है।पहला उल्लेखनीय समानता है, जो 2: nat :: = (s 0)) जैसी परिभाषाओं के लिए है, जिसका कोई गणितीय अर्थ नहीं है, लेकिन पाठकों के लिए उपयोगी है। दूसरा निर्णय समानता है, जो तब होता है जब दो पद एक ही पद की गणना करते हैं, जैसे कि x + (1 + 4) और x + (4 + 1), जो दोनों x + 5 से गणना करते हैं। लेकिन प्ररूप सिद्धांत को समानता के एक और रूप की आवश्यकता होती है, जिसे पहचान प्रकार या प्रस्ताव समानता के रूप में जाना जाता है।
-इसका कारण पहचान प्रकार की आवश्यकता है क्योंकि कुछ समान शब्द एक ही शब्द की गणना नहीं करते हैं।X: NAT, शर्तों को X + 1 और 1 + x एक ही शब्द की गणना नहीं करते हैं।याद रखें कि + फलन ऐड के लिए एक संकेतन है, जो फलन r के लिए एक संकेतन है।हम आर पर तब तक गणना नहीं कर सकते हैं जब तक कि एक्स के लिए मूल्य निर्दिष्ट नहीं किया जाता है और, जब तक कि यह निर्दिष्ट नहीं किया जाता है, आर के लिए दो अलग -अलग  संकेत एक ही शब्द की गणना नहीं करेंगे।
+इसका कारण पहचान प्रकार की आवश्यकता है क्योंकि कुछ समान पद एक ही पद की गणना नहीं करते हैं। X: NAT, शर्तों को X + 1 और 1 + x एक ही पद की गणना नहीं करते हैं। याद रखें कि + फलन योग के लिए एक संकेतन है, जो फलन R के लिए एक संकेतन है। हम R पर तब तक गणना नहीं कर सकते हैं जब तक कि X के लिए मूल्य निर्दिष्ट नहीं किया जाता है और, जब तक कि यह निर्दिष्ट नहीं किया जाता है, R के लिए दो अलग -अलग संकेत एक ही पद की गणना नहीं करेंगे।
-एक पहचान प्रकार के लिए एक ही प्रकार के दो शब्दों को और बी की आवश्यकता होती है और इसे ए = बी लिखा जाता है।तो, x + 1 और 1 + x के लिए, प्रकार x + 1 = 1 + x होगा।कंस्ट्रक्टर रिफ्लेक्सिटी के साथ कैनोनिकल शब्द बनाए जाते हैं। संकेत रिफ्लेक्सिटी ए एक शब्द ए लेता है और टाइप ए = ए का एक विहित शब्द लौटाता है।
+एक पहचान प्रकार के लिए एक ही प्रकार के दो पदों "a" और "b" की आवश्यकता होती है और इसे "a = b" लिखा जाता है। तो, "x + 1" और "1 + x" के लिए, प्रकार "x+1 = 1+x" होगा। प्रमाणिक पद संचरक "स्वतुल्यता" के साथ बनाए गए हैं। संकेत स्वतुल्यता a एक पद a लेता है और प्रारूप a = a का एक प्रामाणिक पद है।
-पहचान प्रकार के साथ गणना एलिमिनेटर फलन j के साथ की जाती है।फलन j एक शब्द को A, B, और टाइप A = B के एक शब्द पर पुनः लिखा जाना देता है ताकि B को A द्वारा प्रतिस्थापित किया जाए।जबकि J एक दिशात्मक है, केवल B के साथ B को स्थानापन्न करने में सक्षम है, यह साबित किया जा सकता है कि पहचान प्रकार [[रिफ्लेक्सिटिविटी प्रॉपर्टी]], सममित गुण और सकर्मक गुण है।
+पहचान प्रकार के साथ गणना विलोपक फलन 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 प्रतिस्थापित करने के लिए।इस तरह, पहचान प्रकार समानता को पकड़ने में सक्षम है जो निर्णय समानता के साथ संभव नहीं है।
+यदि प्रामाणिक पद हमेशा A = A और X+1 होते हैं, तो 1+x के समान पद की गणना नहीं करते हैं, हम x+1 = 1+x का एक पद कैसे बनाते हैं? हम R फलन का उपयोग करते हैं। (ऊपर प्राकृतिक संख्याएं देखें।) 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 प्रारूप है। हम किसी भी पद में "x+1" के लिए "1+x" को प्रतिस्थापित करने के लिए इसका और फलन "J" का उपयोग कर सकते हैं। इस प्रकार, पहचान प्रकार उन समानताओं को स्वीकृत में सक्षम होता है जो न्यायिक समानता के साथ संभव नहीं हैं।
-स्पष्ट होने के लिए, टाइप 0 = 1 बनाना संभव है, लेकिन उस प्रकार की शर्तों को बनाने का कोई तरीका नहीं होगा।टाइप 0 = 1 के शब्द के बिना, किसी अन्य शब्द में 1 के लिए 0 के विकल्प के लिए फलन j का उपयोग करना संभव नहीं होगा।
+स्पष्ट होने के लिए, "0 = 1" प्रकार बनाना संभव है, लेकिन उस प्रकार की शर्तें बनाने का कोई तरीका नहीं होगा। "0 = 1" के प्रकार के बिना, दूसरे पद में "1" के लिए "0" को प्रतिस्थापित करने के लिए "J" फलन का उपयोग करना संभव नहीं होगा।
-प्ररूप सिद्धांत में समानता की जटिलताएं इसे एक सक्रिय अनुसंधान क्षेत्र बनाती हैं, होमोटॉपी  प्ररूप सिद्धांत देखें।
+प्ररूप सिद्धांत में समानता की जटिलताएं इसे एक सक्रिय अनुसंधान क्षेत्र बनाती हैं, होमोटॉपी प्ररूप सिद्धांत देखें।
 ==== आगमनात्मक प्रकार ====
-आगमनात्मक प्रकार बड़े प्रकार के प्रकार बनाने का एक तरीका है।वास्तव में, ऊपर वर्णित सभी प्रकारों को आगमनात्मक प्रकारों के नियमों का उपयोग करके परिभाषित किया जा सकता है।एक बार प्रकार के प्रकार के कंस्ट्रक्टर निर्दिष्ट हो जाने के बाद, एलिमिनेटर फलन और गणना संरचनात्मक पुनरावर्ती द्वारा निर्धारित किया जाता है।
+आगमनात्मक प्रकार बड़ी संख्या में प्रकार बनाने का एक तरीका है। वास्तव में, ऊपर और अधिक वर्णित सभी प्रकारों को आगमनात्मक प्रकारों के नियमों का उपयोग करके परिभाषित किया जा सकता है। एक बार प्रकार के प्रारूप के संरचक निर्दिष्ट हो जाने के बाद, विलोपक फलन और गणना संरचनात्मक पुनरावर्ती द्वारा निर्धारित किया जाता है।
-प्रकार बनाने के लिए समान, अधिक शक्तिशाली तरीके हैं।इनमें [[प्रेरणा-पुनरावर्तन]] और [[प्रेरण]] सम्मिलित हैं।केवल लैम्ब्डा शब्दों का उपयोग करके समान प्रकार बनाने का एक तरीका भी है, जिसे मोगेनसेन -स्कॉट एन्कोडिंग कहा जाता है।
+प्रकार बनाने के लिए समान, अधिक शक्तिशाली तरीके हैं।इनमें [[प्रेरणा-पुनरावर्तन]] और [[प्रेरण]] सम्मिलित हैं।केवल लैम्ब्डा पदों का उपयोग करके समान प्रकार बनाने का एक तरीका भी है, जिसे मोगेनसेन -स्कॉट एन्कोडिंग कहा जाता है।
-(नोट:  प्ररूप सिद्धांत में सामान्य रूप से [[समावेश]] सम्मिलित नहीं होता है। वे एक अनंत डेटा प्रकार का प्रतिनिधित्व करते हैं और अधिकांश  प्ररूप सिद्धांत खुद को उन कार्यों तक सीमित करते हैं जो रुकने के लिए साबित हो सकते हैं।)
+(नोट: प्ररूप सिद्धांत में सामान्य रूप से [[समावेश]] सम्मिलित नहीं होता है। वे एक अनंत डेटा प्रकार का प्रतिनिधित्व करते हैं और अधिकांश प्ररूप सिद्धांत खुद को उन कार्यों तक सीमित करते हैं जो रुकने के लिए प्रमाणित हो सकते हैं।)
 == समुच्चय सिद्धान्त से अंतर ==
-गणित के लिए पारंपरिक फाउंडेशन को एक तर्क के साथ जोड़ा गया सिद्धांत निर्धारित किया गया है।सबसे सामान्य एक उद्धृत Zermelo -Fraenkel समुच्चय सिद्धान्त है, जिसे ZF के रूप में जाना जाता है या, पसंद के [[स्वयंसिद्ध|अभिगृहीत]], ZFC के साथ। प्ररूप सिद्धांत इस आधार  से कई तरीकों से भिन्न होते हैं।
+गणित के लिए पारंपरिक आधार एक तर्क के साथ जोड़े गए सिद्धांत को निर्धारित किया गया है। सबसे सामान्य एक उद्धृत ज़र्मेलो-फ्रेंकेल समुच्चय सिद्धान्त है, जिसे ज़र्मेलो-फ्रेंकेल के रूप में जाना जाता है या, विकल्प के [[स्वयंसिद्ध|अभिगृहीत]], ज़र्मेलो-फ्रेंकेल समुच्चय सिद्धान्त के रूप में जाना जाता है। प्ररूप सिद्धांत इस आधार से कई तरीकों से भिन्न होते हैं।
-* समुच्चय सिद्धान्त में अनुमान और अभिगृहीत दोनों ही नियम हैं, जबकि प्रकार के सिद्धांतों में केवल नियम हैं।समुच्चय सिद्धान्त तर्क के शीर्ष पर बनाए गए हैं।इस प्रकार, ZFC को प्रथम-क्रम लॉजिक और Zermelo-fraenkel_set_stheory#Axioms के दोनों नियमों द्वारा परिभाषित किया गया है।(एक अभिगृहीत एक तार्किक व्युत्पत्ति के बिना सच के रूप में स्वीकार किया जाता है।)  प्ररूप सिद्धांत, सामान्य रूप से, अभिगृहीत नहीं होते हैं और उनके नियमों के नियमों द्वारा परिभाषित होते हैं।
+* समुच्चय सिद्धान्त में अनुमान और अभिगृहीत दोनों ही नियम हैं, जबकि प्रकार के सिद्धांतों में केवल नियम हैं। समुच्चय सिद्धान्त तर्क के शीर्ष पर बनाए गए हैं।इस प्रकार, ज़र्मेलो-फ्रेंकेल समुच्चय सिद्धान्त को प्रथम-क्रम तर्क और ज़र्मेलो-फ्रेंकेल समुच्चय सिद्धान्त अभिगृहीत के दोनों नियमों द्वारा परिभाषित किया गया है। (एक अभिगृहीत एक तार्किक व्युत्पत्ति के बिना सत्य के रूप में स्वीकार किया जाता है।) प्ररूप सिद्धांत, सामान्य रूप से, अभिगृहीत नहीं होते हैं और उनके नियमों के नियमों द्वारा परिभाषित होते हैं।
-* समुच्चय  उपागम और लॉजिक में बाहर किए गए मध्य का नियम है।अर्थात्, हर प्रमेय सच या गलत है।जब एक   प्ररूप सिद्धांत और या या के रूप में अवधारणाओं को परिभाषित करता है, तो यह [[अंतर्ज्ञानवादी तर्क]] की ओर जाता है, जिसमें बाहर किए गए मध्य का कानून नहीं है।हालांकि, कानून कुछ प्रकार के लिए सिद्ध किया जा सकता है।
+* समुच्चय उपागम और तर्क में बाहर किए गए मध्य का नियम है।अर्थात्, हर प्रमेय सत्य या असत्य है। जब एक प्ररूप सिद्धांत और या या के रूप में अवधारणाओं को परिभाषित करता है, तो यह [[अंतर्ज्ञानवादी तर्क]] की ओर जाता है, जिसमें बाहर किए गए मध्य का नियम नहीं है। हालांकि, नियम कुछ प्रकार के लिए सिद्ध किया जा सकता है।
-* समुच्चय सिद्धान्त में, एक तत्व एक समुच्चय तक सीमित नहीं है।तत्व अन्य समुच्चयों के साथ उप-समुच्चय और यूनियनों में दिखाई दे सकता है। प्ररूप सिद्धांत में, शब्द (सामान्य रूप से) केवल एक प्रकार से संबंधित हैं।जहां एक उप-समुच्चय का उपयोग किया जाएगा,  प्ररूप सिद्धांत एक विधेय ([[गणितीय तर्क)]] का उपयोग कर सकता है या एक निर्भर-टाइप उत्पाद प्रकार का उपयोग कर सकता है, जहां प्रत्येक तत्व <math>x</math> एक सबूत के साथ जोड़ा जाता है कि उप-समुच्चय की गुण के लिए है <math>x</math>।जहां एक संघ का उपयोग किया जाएगा,  प्ररूप सिद्धांत योग प्रकार का उपयोग करता है, जिसमें नए विहित शब्द सम्मिलित हैं।
+* समुच्चय सिद्धान्त में, एक तत्व एक समुच्चय तक सीमित नहीं है। तत्व अन्य समुच्चयों के साथ उप-समुच्चय और समूहों में दिखाई दे सकता है। प्ररूप सिद्धांत में, पद (सामान्य रूप से) केवल एक प्रकार से संबंधित हैं। जहां एक उप-समुच्चय का उपयोग किया जाएगा, प्ररूप सिद्धांत एक विधेय ([[गणितीय तर्क)]] का उपयोग कर सकता है या एक निर्भर-प्रारूप उत्पाद प्रकार का उपयोग कर सकता है, जहां प्रत्येक तत्व <math>x</math> एक प्रमाण के साथ जोड़ा जाता है कि उप-समुच्चय <math>x</math> की गुण के लिए है। जहां एक समूह का उपयोग किया जाएगा, प्ररूप सिद्धांत योग प्रकार का उपयोग करता है, जिसमें नए प्रामाणिक पद सम्मिलित हैं।
-* प्ररूप सिद्धांत में गणना की एक अंतर्निहित धारणा है।इस प्रकार, 1+1 और 2  प्ररूप सिद्धांत में अलग -अलग शब्द हैं, लेकिन वे एक ही मूल्य की गणना करते हैं।इसके अतिरिक्त, कार्यों को कम्प्यूटेशनल रूप से लैम्ब्डा शर्तों के रूप में परिभाषित किया गया है।समुच्चय सिद्धान्त में, 1+1 = 2 का अर्थ है कि 1+1 मान 2 को संदर्भित करने का सिर्फ एक और तरीका है। प्ररूप सिद्धांत की गणना में समानता की एक जटिल अवधारणा की आवश्यकता होती है।
+* प्ररूप सिद्धांत में गणना की एक अंतर्निहित धारणा है। इस प्रकार, 1+1 और 2 प्ररूप सिद्धांत में अलग -अलग पद हैं, लेकिन वे एक ही मूल्य की गणना करते हैं। इसके अतिरिक्त, फलनों को गणनीय रूप से लैम्ब्डा शर्तों के रूप में परिभाषित किया गया है। समुच्चय सिद्धान्त में, 1+1 = 2 का अर्थ है कि 1+1 मान 2 को संदर्भित करने का सिर्फ एक और तरीका है। प्ररूप सिद्धांत की गणना में समानता की एक जटिल अवधारणा की आवश्यकता होती है।
-* समुच्चय सिद्धान्त सामान्य रूप से समुच्चय के रूप में संख्याओं को एन्कोड करता है।।कंस्ट्रक्टर्स 0 और एस द्वारा बनाई गई आगमनात्मक प्रकार से बारीकी से मीनो स्वयंसिद्धों से मिलते -जुलते हैं | पीनो के अभिगृहीत।
+* समुच्चय सिद्धान्त सामान्य रूप से संख्याओं को समुच्चय के रूप में एन्कोड करता है। (0 रिक्त समुच्चय है, 1 समुच्चय है जिसमें रिक्त समुच्चय है। प्राकृतिक संख्याओं की समुच्चय-सैद्धांतिक परिभाषा देखें।) प्रकार सिद्धांत चर्च एन्कोडिंग या अधिक स्वाभाविक रूप से आगमनात्मक प्रकारों का उपयोग करके फलनों के रूप में संख्याओं को एन्कोड कर सकता है। आगमनात्मक प्रकार द्वारा बनाए गए रचनाकार "0" और "S" पियानो के स्वयंसिद्धों के समान हैं।
-* समुच्चय  उपागम में समुच्चय-बिल्डर नोटेशन है।यह कोई भी समुच्चय बना सकता है जिसे परिभाषित किया जा सकता है।यह इसे बेशुमार समुच्चय बनाने की अनुमति देता है। प्ररूप सिद्धांत वाक्यविन्यास हैं, जो उन्हें एक अनगढ़ अनंत शब्दों में सीमित करता है।इसके अतिरिक्त, अधिकांश प्रकार के सिद्धांतों को हमेशा रुकने और खुद को [[पुनरावर्ती भाषा]] के शब्दों में सीमित करने के लिए गणना की आवश्यकता होती है।नतीजतन, अधिकांश  प्ररूप सिद्धांत [[वास्तविक संख्या]]ओं का उपयोग नहीं करते हैं, लेकिन [[कम्प्यूटेबल नंबर]]।
+* समुच्चय उपागम में समुच्चय-संचरक सांकेतिक है। यह कोई भी समुच्चय बना सकता है जिसे परिभाषित किया जा सकता है। यह इसे अत्यधिक समुच्चय बनाने की अनुमति देता है। प्ररूप सिद्धांत सिंटेक्स हैं, जो उन्हें एक गिनने योग्य अनंत पदों तक सीमित करते हैं। इसके अतिरिक्त, अधिकांश प्रकार के सिद्धांतों को हमेशा रुकने और स्वयं को पुनरावर्ती रूप से उत्पन्न करने योग्य शर्तों तक सीमित करने के लिए गणना की आवश्यकता होती है। परिणामस्वरूप, अधिकांश प्रकार के सिद्धांत वास्तविक संख्याओं और गणना योग्य संख्याओं का उपयोग नहीं करते हैं।
-* समुच्चय सिद्धान्त में, [[पसंद का स्वयंसिद्ध|पसंद का अभिगृहीत]] एक अभिगृहीत है और विवादास्पद है, खासकर जब बेशुमार समुच्चय पर लागू होता है। प्ररूप सिद्धांत में, समतुल्य कथन एक प्रमेय (प्रकार) है और साबित करने योग्य है (एक शब्द द्वारा बसा हुआ)।
+* समुच्चय सिद्धांत में, चयन का अभिगृहीत स्वयंसिद्ध है और विवादास्पद है, विशेषकर जब अत्यधिक समुच्चय पर लागू किया जाता है। प्रारूप सिद्धांत में, समतुल्य कथन एक प्रमेय (प्रकार) है और सिद्ध (एक पद द्वारा बना हुआ) है।
-* प्ररूप सिद्धांत में, प्रमाण गणितीय वस्तुएं हैं।टाइप X+1 = 1+x का उपयोग तब तक नहीं किया जा सकता जब तक कि प्रकार का शब्द न हो।यह शब्द एक प्रमाण का प्रतिनिधित्व करता है कि x+1 = 1+x।इस प्रकार,  प्ररूप सिद्धांत गणितीय वस्तुओं के रूप में अध्ययन किए जाने वाले प्रमाणों को खोलता है।
+* प्ररूप सिद्धांत में, प्रमाण गणितीय वस्तुएं हैं। प्रारूप X+1 = 1+x का उपयोग तब तक नहीं किया जा सकता जब तक कि प्रकार का पद न हो। यह पद एक प्रमाण का प्रतिनिधित्व करता है कि x+1 = 1+x है। इस प्रकार, प्ररूप सिद्धांत गणितीय वस्तुओं के रूप में अध्ययन किए जाने वाले प्रमाणों को प्रारंभ है।
-प्ररूप सिद्धांत के समर्थक भी [[BHK व्याख्या]] के माध्यम से रचनात्मक गणित के लिए अपने संबंध को इंगित करेंगे, इसके करी -आओ -आइसोमोर्फिज्म द्वारा तर्क से जुड़े, और [[श्रेणी सिद्धांत]] से इसके कनेक्शन।
+प्ररूप सिद्धांत के समर्थक भी [[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>।एक  प्ररूप सिद्धांत में अतिरिक्त निर्णय होते हैं जो प्रकारों और संबंधित शब्दों को प्रकारों तक परिभाषित करते हैं।
+प्ररूप सिद्धांत एक [[गणितीय तर्क]] है। यह अनुमान के नियम का एक संग्रह है जो [[निर्णय (गणितीय तर्क)]] में परिणाम करता है।अधिकांश तर्क में निर्णय होते हैं जिसका अर्थ है "पद x सत्य है।" या "पद x एक सुनिर्मित सूत्र है।"<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) हैं।
+तर्क में एक पद को पुनरावर्ती रूप से एक स्थिर प्रतीक, चर, या एक फलन अनुप्रयोग के रूप में परिभाषित किया जाता है, जहां एक पद दूसरे पद पर लागू होता है। कुछ स्थिर प्रतीक प्राकृतिक संख्याओं के "0", बूलियन्स के "सत्य" और "S" और "यदि" जैसे फलन होंगे। इस प्रकार कुछ पद "0", "(S0)", "(S (S x))", और "यदि सत्य 0 (S0)" है।
 === निर्णय ===
@@ Line 256: / Line 255: @@
 *<math>T</math> एक प्रकार है।
-*<math>t</math> प्रकार का एक शब्द है <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_1</math> और <math>t_2</math> दोनों प्रकार के हैं <math>T</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' प्रकार का पद है,(यदि x y y) 'nat' प्रकार का पद है"। मान्यताओं के लिए गणितीय संकेतन "पद: प्रकार" की एक अल्पविराम से अलग सूची है जो पद की एक अल्पविराम-अलग सूची है: टाइप करें जो टर्नस्टाइल (प्रतीक) '<math>\vdash</math>' से पहले है। इस प्रकार, उदाहरण कथन औपचारिक रूप से लिखा गया है:
-* x: बूल, y: nat <math>\vdash</math> (यदि x y y): nat
+* x:bool, y:nat <math>\vdash</math> (if x y y): nat
 यदि कोई धारणा नहीं है, तो टर्नस्टाइल के बाईं ओर कुछ भी नहीं होगा:
-* <math>\vdash</math> S: NAT <math>\to</math> नेट
+* <math>\vdash</math> S: nat <math>\to</math> nat
-मान्यताओं की सूची को संदर्भ कहा जाता है।प्रतीक को देखना बहुत सामान्य है '<math>\Gamma</math>'कुछ या सभी मान्यताओं का प्रतिनिधित्व करने के लिए उपयोग किया जाता है।इस प्रकार, 4 अलग -अलग निर्णयों के लिए औपचारिक संकेतन सामान्य रूप से है:
+अनुमानों की सूची को "संदर्भ" कहा जाता है। कुछ या सभी धारणाओं का प्रतिनिधित्व करने के लिए प्रयुक्त प्रतीक '<math>\Gamma</math>' देखना बहुत सामान्य है। इस प्रकार, 4 अलग -अलग निर्णयों के लिए औपचारिक संकेतन सामान्य रूप से है:
 {| class="wikitable"
@@ Line 287: / Line 286: @@
 === नियम ===
-प्ररूप सिद्धांत के नियम का कहना है कि अन्य निर्णयों के अस्तित्व के आधार पर क्या निर्णय लिया जा सकता है। नियमों को रेखा के ऊपर आवश्यक  निविष्‍ट निर्णयों और रेखा के नीचे परिणामी निर्णय के साथ, एक क्षैतिज रेखा का उपयोग करके व्यक्त किया जाता है। लैम्ब्डा पद बनाने का नियम है:
+प्ररूप सिद्धांत के नियम का कहना है कि अन्य निर्णयों के अस्तित्व के आधार पर क्या निर्णय लिया जा सकता है। नियमों को रेखा के ऊपर आवश्यक निविष्‍ट निर्णयों और रेखा के नीचे परिणामी निर्णय के साथ, एक क्षैतिज रेखा का उपयोग करके व्यक्त किया जाता है। लैम्ब्डा पद बनाने का नियम है:
 <math display="block">
 \begin{array}{c}
@@ Line 295: / Line 294: @@
 \end{array}
 </math>
-लैम्ब्डा शब्द बनाने के लिए आवश्यक निर्णय लाइन से ऊपर जाते हैं।इस स्थिति में, केवल एक निर्णय की आवश्यकता है।यह है कि कुछ प्रकार बी का कुछ शब्द बी है, यह मानते हुए कि कुछ प्रकार ए और कुछ अन्य मान्यताओं का कुछ शब्द है<math>\Gamma</math>।(टिप्पणी:<math>\Gamma</math>ए, ए, बी, और बी नियम में सभी [[मेटावेरियस]] हैं।) परिणामस्वरूप निर्णय लाइन से नीचे चला जाता है।इस नियम के परिणामस्वरूप निर्णय में कहा गया है कि नए लैम्ब्डा शब्द में टाइप ए है <math>\to</math> B अन्य मान्यताओं के अंतर्गत <math>\Gamma</math>।
+लैम्ब्डा पद बनाने के लिए आवश्यक निर्णय लाइन से ऊपर जाते हैं। इस स्थिति में, केवल एक निर्णय की आवश्यकता है। यह है कि कुछ प्रकार b का कुछ पद B है, यह मानते हुए कि कुछ प्रकार "" का कुछ पद "a" और कुछ अन्य धारणाएं <math>\Gamma</math>है। (टिप्पणी: <math>\Gamma</math>"a", "A", "b", और "B" सभी नियम में अधिचर हैं।) परिणामी निर्णय रेखा के नीचे जाता है। इस नियम के परिणामी निर्णय में कहा गया है कि नए लैम्ब्डा पद में अन्य धारणाओ <math>\Gamma</math> के अंतर्गत "A <math>\to</math> B प्रकार है।
-नियम वाक्यात्मक हैं और पुनर्लेखन द्वारा काम करते हैं।इस प्रकार, metavariables की तरह<math>\Gamma</math>, ए, ए, आदि वास्तव में उन जटिल शब्दों से युक्त हो सकते हैं जिनमें कई फलन अनुप्रयोग होते हैं, न कि केवल एकल प्रतीकों को।
+नियम वाक्यात्मक हैंऔर पुनर्लेखन द्वारा कार्य करते हैं। इस प्रकार, परिवर्ती जैसे <math>\Gamma</math>, "a", "A", आदि वास्तव में जटिल पदों से मिलकर बने हो सकते हैं जिनमें कई फलन अनुप्रयोग होते हैं, न कि केवल एकल प्रतीकों मे होते है।
-प्ररूप सिद्धांत में एक विशेष निर्णय उत्पन्न करने के लिए, इसे उत्पन्न करने के लिए एक नियम होना चाहिए।फिर, उस नियम के सभी आवश्यक  निविष्‍ट उत्पन्न करने के लिए नियम होने चाहिए।और फिर उन नियमों के लिए सभी  निविष्‍ट के लिए नियम।लागू नियम एक प्रमाण ट्री बनाते हैं।यह सामान्य रूप से 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 है:
+प्ररूप सिद्धांत में एक विशेष निर्णय उत्पन्न करने के लिए, इसे उत्पन्न करने के लिए एक नियम होना चाहिए। फिर, उस नियम के सभी आवश्यक निविष्‍ट उत्पन्न करने के लिए नियम होने चाहिए। और फिर उन नियमों के लिए सभी निविष्‍ट के लिए लागू नियम एक प्रमाण वृक्ष बनाते हैं। यह सामान्य रूप से जेंटजन-शैली में तैयार किया जाता है,<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> जहां लक्ष्य निर्णय (रूट) सबसे नीचे है और नियमों को शीर्ष पर किसी भी निविष्‍ट (पत्तियों) की आवश्यकता नहीं है ( प्राकृतिक निगमन प्रमाण_और_प्रारूप _सिद्धांत देखें) देखें। एक नियम का एक उदाहरण जिसमें किसी भी निविष्‍ट की आवश्यकता नहीं होती है, वह है जो बताता है कि NAT का एक पद 0 है:
 <math display="block">
@@ Line 307: / Line 306: @@
 \end{array}
 </math>
-एक  प्ररूप सिद्धांत में सामान्य रूप से कई नियम होते हैं, जिनमें सम्मिलित हैं:
+प्ररूप सिद्धांत में सामान्य रूप से कई नियम होते हैं, जिनमें सम्मिलित हैं:
 * एक संदर्भ बनाएं
-* संदर्भ में एक धारणा जोड़ें (कमजोर)
+* संदर्भ में एक धारणा जोड़ें (निर्बलीकरण)
 * संरचनात्मक नियम
-* एक चर बनाने के लिए एक धारणा का उपयोग करें
+* चर बनाने के लिए एक धारणा का उपयोग करें
-* निर्णय समानता के लिए रिफ्लेक्सिटी, समरूपता और संक्रमण को परिभाषित करें
+* निर्णय समानता के लिए स्वतुल्यता, समरूपता और संक्रमण को परिभाषित करें
-* लैम्ब्डा शर्तों के आवेदन के लिए प्रतिस्थापन को परिभाषित करें
+* लैम्ब्डा शर्तों के अनुप्रयोग के लिए प्रतिस्थापन को परिभाषित करें
-* समानता, प्रतिस्थापन, आदि की सभी बातचीत
+* समानता, प्रतिस्थापन, आदि की सभी अंतःक्रियाएँ।
-* ब्रह्मांडों को परिभाषित करें
+* समष्टि को परिभाषित करें
 इसके अतिरिक्त, नियम के प्रकार के लिए, 4 अलग -अलग प्रकार के नियम हैं
-* प्रकार के गठन नियम कहते हैं कि प्रकार कैसे बनाएं
+* प्रकार रचना के नियम कहते हैं कि प्रारूप कैसे बनाएं
-* टर्म परिचय नियम जोड़ी और एस की तरह विहित शब्दों और कंस्ट्रक्टर कार्यों को परिभाषित करते हैं।
+* पद उपक्रम नियम जोड़ी और S की तरह प्रामाणिक पदों और संरचक कार्यों को परिभाषित करते हैं।
-* शब्द उन्मूलन नियम पहले, दूसरे और आर जैसे अन्य कार्यों को परिभाषित करते हैं।
+* पद उन्मूलन नियम पहले, दूसरे और आर जैसे अन्य कार्यों को परिभाषित करते हैं।
-* गणना नियम निर्दिष्ट करें कि प्रकार-विशिष्ट कार्यों के साथ गणना कैसे की जाती है।
+* गणना नियम निर्दिष्ट करें कि प्रारूप-विशिष्ट कार्यों के साथ गणना कैसे की जाती है।
 नियमों के उदाहरण:
-* [https://hott.github.io/hott-2019/images/mltt-rules.pdf नियम मार्टिन-लफ़ के अंतर्ज्ञानवादी  प्ररूप सिद्धांत]
+* [https://hott.github.io/hott-2019/images/mltt-rules.pdf मार्टिन-लोफ के अंतर्ज्ञानवादी प्रकार के सिद्धांत के नियम]
-* परिशिष्ट A.2 of [https://homotopytypetheory.org/book/ homotopy  प्ररूप सिद्धांत] पुस्तक
+* [https://homotopytypetheory.org/book/ होमोटॉपी प्ररूप सिद्धांत] पुस्तक का परिशिष्ट A.2
-=== टाइप सिद्धांतों के गुण ===
+=== प्रारूप सिद्धांतों के गुण ===
-शब्द सामान्य रूप से एक प्रकार के होते हैं।हालांकि, ऐसे सिद्धांत हैं जो उपप्रकार को परिभाषित करते हैं।
+पद सामान्य रूप से एक प्रकार के होते हैं। हालांकि, ऐसे समुच्चय सिद्धांत हैं जो उपप्रकार को परिभाषित करते हैं।
-गणना नियमों के बार -बार आवेदन द्वारा होती है।कई  प्ररूप सिद्धांत दृढ़ता से सामान्य हो रहे हैं, जिसका अर्थ है कि नियमों को लागू करने का कोई भी आदेश हमेशा एक ही परिणाम में समाप्त हो जाएगा।हालांकि, कुछ नहीं हैं।एक सामान्य  प्ररूप सिद्धांत में, एक-दिशात्मक संगणना नियमों को कमी नियम कहा जाता है और नियमों को लागू करने से शब्द को कम करता है।यदि कोई नियम एक-दिशात्मक नहीं है, तो इसे रूपांतरण नियम कहा जाता है।
+गणना नियमों के बार-बार लागू होने से होती है। कई प्ररूप सिद्धांत दृढ़ता से सामान्य हो रहे हैं, जिसका अर्थ है कि नियमों को लागू करने का कोई भी क्रम हमेशा एक ही परिणाम में समाप्त हो जाएगा।हालांकि, कुछ नहीं हैं। एक सामान्य प्ररूप सिद्धांत में, एक-दिशात्मक संगणना नियमों को कमी नियम कहा जाता है और नियमों को लागू करने से पद को कम करता है। यदि कोई नियम एक-दिशात्मक नहीं है, तो इसे रूपांतरण नियम कहा जाता है।
-प्रकारों के कुछ संयोजन प्रकार के अन्य संयोजनों के बराबर हैं।जब कार्यों को घातांक माना जाता है, तो प्रकारों के संयोजन को बीजगणितीय पहचान के समान लिखा जा सकता है।<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>।
+प्रारूपों के कुछ संयोजन प्रकार के अन्य संयोजनों के बराबर हैं। जब कार्यों को घातांक माना जाता है, तो प्रकारों के संयोजन को बीजगणितीय पहचान के समान लिखा जा सकता है।<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> कुछ सामान्य रूप से सामना किए गए अभिगृहीत हैं:
+यदि वे उन शर्तों पर गणना करने के तरीके के बिना शर्तों का उपक्रम देते हैं, तो अभिगृहीत समस्याओं का कारण बन सकते हैं। अर्थात्, अभिगृहीत प्ररूप सिद्धांत के [[सामान्य रूप (अमूर्त पुनर्लेखन)]] के साथ अन्तःक्षेप कर सकते हैं।<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>
+* अभिगृहीत 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>
+* एकपक्षीय अभिगृहीत मानता है कि प्रकारों की तुल्यता प्रकारों की समानता है। इस गुण में अनुसंधान ने [[क्यूबिकल टाइप थ्योरी|घनीय प्ररूप सिद्धांत]] का नेतृत्व किया, जहां गुण एक अभिगृहीत की आवश्यकता के बिना रखती है।<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}}।)
+विकल्प के अभिगृहीत को प्ररूप सिद्धांत में जोड़े जाने की आवश्यकता नहीं है, क्योंकि अधिकांश प्रकार के सिद्धांतों में इसे अनुमान के नियमों से प्राप्त किया जा सकता है। यह प्ररूप सिद्धांत के [[रचनात्मक गणित]] प्रकृति के कारण है, जहां यह प्रमाणित करना कि एक मूल्य सम्मिलित है, मूल्य की गणना करने के लिए एक विधि की आवश्यकता होती है। विकल्प का अभिगृहीत अधिकांश निर्धारित सिद्धांतों की तुलना में प्ररूप सिद्धांत में कम शक्तिशाली है, क्योंकि प्ररूप सिद्धांत के फलन गणनीय होने चाहिए और सिंटैक्स-संचालित होने के कारण, एक प्रकार में पदों की संख्या गणना योग्य होनी चाहिए। ( {{Section link|रचनात्मक गणित में चयन का स्वयंसिद्ध#देखें। }})
 === [[निर्णय समस्या]]एं ===
-एक   प्ररूप सिद्धांत स्वाभाविक रूप से टाइप निवास की निर्णय समस्या से जुड़ा हुआ है।<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>
+प्ररूप सिद्धांत स्वाभाविक रूप से प्रारूप स्थिति की निर्णय समस्या से जुड़ा हुआ है।<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}}
+{{Main|प्रारूप स्थिति}}
-टाइप निवास की निर्णय समस्या (द्वारा संक्षिप्त) <math>\exists e.\Gamma \vdash e : \tau?</math>) है:
-: एक प्रकार का वातावरण दिया <math>\Gamma</math> और एक प्रकार <math>\tau</math>, तय करें कि क्या कोई शब्द सम्मिलित है <math>e</math> जिसे प्रकार सौंपा जा सकता है <math>\tau</math> प्रकार के वातावरण में <math>\Gamma</math>।
-प्रणाली यू#गिरार्ड का विरोधाभास | गिरार्ड के विरोधाभास से पता चलता है कि टाइप निवास दृढ़ता से करी -आओ -पत्राचार के साथ एक प्रकार की प्रणाली की स्थिरता से संबंधित है।ध्वनि होने के लिए, इस तरह की प्रणाली में निर्जन प्रकार होने चाहिए।
-शब्दों और प्रकारों का विरोध कार्यान्वयन और विनिर्देश में से एक के रूप में भी हो सकता है।[[कार्यक्रम संश्लेषण]] (कम्प्यूटेशनल समकक्ष का) प्रकार के निवास (नीचे देखें) का उपयोग प्रकार की जानकारी के रूप में दिए गए विनिर्देश से (सभी या भागों के) कार्यक्रमों के निर्माण के लिए किया जा सकता है।<ref>
+प्रारूप स्थिति की निर्णय समस्या (द्वारा संक्षिप्त) <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}}
+{{Main|प्रारूप का अनुमान}}
-कई कार्यक्रम जो  प्ररूप सिद्धांत (जैसे, इंटरैक्टिव प्रमेय प्रोवर्स) के साथ काम करते हैं, वे भी टाइप इन्फ्रेंसिंग करते हैं।यह उन्हें उन नियमों का चयन करने देता है जो उपयोगकर्ता उपयोगकर्ता द्वारा कम कार्यों के साथ, उपयोगकर्ता का इरादा रखते हैं।
+कई कमानुदेश जो प्ररूप सिद्धांत (जैसे, अन्योन्य क्रियात्मक प्रमेय समर्थक) के साथ काम करते हैं, वे भी प्रारूप निष्कष करते हैं। यह उन्हें उन नियमों का चयन करने देता है जो उपयोगकर्ता द्वारा कम क्रियाओं के साथ उपयोगकर्ता चाहता है।
 === अनुसंधान क्षेत्र ===
-होमोटॉपी   प्ररूप सिद्धांत अंतर्ज्ञानवादी  प्ररूप सिद्धांत से भिन्न होता है जो ज्यादातर समानता प्रकार की हैंडलिंग से होता है।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"/>
+होमोटॉपी प्ररूप सिद्धांत अंतर्ज्ञानवादी प्ररूप सिद्धांत से भिन्न होता है जो अधिकतम समानता प्रारूप के संचालन से होता है। 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 समान हैं।और उस प्रकार का एक शब्द इसके प्रमाण का प्रतिनिधित्व करता है।
+जब एक नींव के रूप में उपयोग किया जाता है, तो कुछ प्रकारों की व्याख्या प्रस्तावों के रूप में की जाती है (ऐसे कथन जिन्हें सिद्ध किया जा सकता है) और प्रकार का एक पद उस प्रस्ताव का प्रमाण है। इस प्रकार, प्रकार "Π x:nat . x+1=1+x" दर्शाता है कि, "nat" प्रकार के किसी भी "x" के लिए, "x+1" और "1+x" समान हैं। और उस प्रकार का पद इसके प्रमाण का प्रतिनिधित्व करता है।
 === करी-हावर्ड पत्राचार ===
-करी -होवर पत्राचार लॉजिक्स और प्रोग्रामिंग भाषाओं के बीच मनाया समानता है।तर्क में निहितार्थ, ए <math>\to</math> B टाइप A से टाइप B तक फलन जैसा दिखता है।विभिन्न प्रकार के लॉजिक्स के लिए, नियम एक प्रोग्रामिंग भाषा के प्रकारों में अभिव्यक्ति के समान हैं।समानता आगे बढ़ती है, क्योंकि नियमों के अनुप्रयोग प्रोग्रामिंग भाषाओं में कार्यक्रमों से मिलते जुलते हैं।इस प्रकार, पत्राचार को प्रायः कार्यक्रमों के रूप में प्रमाण के रूप में संक्षेपित किया जाता है।
+करी -होवर पत्राचार तर्क और प्रोग्रामिंग भाषाओं के बीच देखी गई समानता है। तर्क में निहितार्थ, a <math>\to</math> B टाइप A से टाइप B तक फलन जैसा दिखता है। विभिन्न प्रकार के तर्क के लिए, नियम एक प्रोग्रामिंग भाषा के प्रकारों में अभिव्यक्ति के समान हैं। समानता आगे बढ़ती है, क्योंकि नियमों के अनुप्रयोग प्रोग्रामिंग भाषाओं में प्रोग्राम के समान होते हैं। इस प्रकार, पत्राचार को प्रायः "प्रोग्राम के रूप में प्रमाण" के रूप में संक्षेपित किया जाता है।
-लॉजिक ऑपरेटर्स सार्वभौमिक परिमाणीकरण और अस्तित्वगत मात्रा का ठहराव प्रति मार्टिन-लोफ ने आश्रित  प्ररूप सिद्धांत का आविष्कार करने के लिए नेतृत्व किया।
+तर्क संचालिकाएँ "सभी के लिए" और "अस्तित्व में हैं" ने प्रति मार्टिन-लोफ़ को निर्भर प्रारूप सिद्धांत का आविष्कार करने के लिए प्रेरित किया।
 === अंतर्ज्ञानवादी तर्क ===
-जब कुछ प्रकारों की व्याख्या प्रस्तावों के रूप में की जाती है, तो सामान्य प्रकारों का एक समुच्चय होता है जिसका उपयोग उन्हें प्रकार से बाहर तर्क देने के लिए कनेक्ट करने के लिए किया जा सकता है।हालाँकि, यह तर्क शास्त्रीय तर्क नहीं बल्कि अंतर्ज्ञानवादी तर्क है।यही है, इसमें न तो बाहर किए गए मध्य और न ही दोहराव का कानून है।
+जब कुछ प्रकारों की व्याख्या प्रस्तावों के रूप में की जाती है, तो सामान्य प्रकारों का एक समुच्चय होता है जिसका उपयोग उन्हें प्रकार से बाहर तर्क देने के लिए संपर्क करने के लिए किया जा सकता है। हालाँकि, यह तर्क शास्त्रीय तर्क नहीं बल्कि अंतर्ज्ञानवादी तर्क है। यही है, इसमें न तो बाहर किए गए मध्य और न ही पुनरावृत्ति का नियम है।
-तार्किक प्रस्तावों के लिए प्रकारों का एक प्राकृतिक संबंध है।यदि एक प्रस्ताव का प्रतिनिधित्व करने वाला एक प्रकार है, तो प्रकार का एक फलन बनाने में सक्षम है<math>\top \to </math> ए इंगित करता है कि ए में एक प्रमाण है और फलन ए बनाने में सक्षम है <math>\to \bot</math>इंगित करता है कि A में कोई प्रमाण नहीं है।अर्थात्, निवास योग्य प्रकार सिद्ध होते हैं और निर्जन प्रकार अस्वीकृत होते हैं।
+तार्किक प्रस्तावों के लिए प्रकारों का एक प्राकृतिक संबंध है। यदि एक प्रस्ताव का प्रतिनिधित्व करने वाला एक प्रकार है, तो <math>\top \to </math> a प्रारूप का एक फलन बनाने में सक्षम होने मे इंगित करता है कि A के पास एक प्रमाण है और "A <math>\to \bot</math>फलन बनाने में सक्षम करता है कि A के पास प्रमाण नहीं है। अर्थात्, स्थिति योग्य प्रारूप सिद्ध होते हैं और निर्जन प्रकार अप्रमाणित होते हैं।
-चेतावनी: इस व्याख्या से बहुत भ्रम हो सकता है।एक  प्ररूप सिद्धांत में टाइप बूल की शर्तों को सही और गलत हो सकता है, जो एक [[बूलियन तर्क]] की तरह काम करता है, और एक ही समय में प्रकार होते हैं <math>\top</math> और <math>\bot</math> प्रस्ताव के लिए एक अंतर्ज्ञानवादी तर्क के हिस्से के रूप में, सच्चे (साबित) और झूठे (असुरक्षित) का प्रतिनिधित्व करने के लिए।
+चेतावनी: इस व्याख्या से बहुत भ्रम हो सकता है। एक प्ररूप सिद्धांत में बूल" प्रकार के सत्य और असत्य हो सकता है, जो एक [[बूलियन तर्क]] की तरह काम करता है, और साथ ही साथ "सत्य" (प्रमाणित) और "का प्रतिनिधित्व करने के लिए <math>\top</math> और <math>\bot</math> प्रारूप होते है। असत्य" (अप्रमाणित), प्रस्ताव के लिए एक अंतर्ज्ञानवादी तर्क के हिस्से के रूप में होते है।
-इस अंतर्ज्ञानवादी व्याख्या के अंतर्गत, ऐसे सामान्य प्रकार हैं जो तार्किक ऑपरेटरों के रूप में कार्य करते हैं:
+इस अंतर्ज्ञानवादी व्याख्या के अंतर्गत, ऐसे सामान्य प्रकार हैं जो तार्किक संचालकों के रूप में कार्य करते हैं:
 {| class="wikitable"
 ! तर्क नाम !! तर्क संकेतन !! प्रकार संकेतन !! प्रारूप नाम
@@ Line 417: / Line 418: @@
 | सम्मिलित || <math>\exists a \in A, P(a)</math> || &Sigma; a : A . P(a)  || आश्रित उत्पाद प्रकार
 |}
-लेकिन इस व्याख्या के अंतर्गत, बीच में बहिष्कृत कोई कानून नहीं है।अर्थात्, प्रकार का कोई शब्द नहीं है & pi;ए ।ए + (ए) <math>\to \bot</math>)।
+लेकिन इस व्याख्या के अंतर्गत, बीच में बहिष्कृत कोई नियम नहीं है। अर्थात्, प्रकार का कोई पद & pi;a ।a + (a) <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>)।)
+इसी तरह, कोई पुनरावृत्ति नहीं है। Π A प्रकार का कोई पद नहीं है। ((a <math>\to \bot</math>) <math>\to \bot</math>) <math>\to </math> a (ध्यान दें: अंतर्ज्ञानवादी तर्क अनुमति देता है <math>\lnot \lnot \lnot A \to \lnot A</math> और प्रकार का एक पद ((a) <math>\to \bot</math>) <math>\to \bot</math>) <math>\to \bot</math>) <math>\to </math> (a <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>)।
+प्रति मार्टिन-लोफ ने रचनात्मक गणित की नींव के रूप में अपने अंतर्ज्ञानवादी प्रकार के सिद्धांत को प्रस्तावित किया। रचनात्मक गणित की आवश्यकता है जब प्रमाणित करते समय "P(x) गुण के साथ एक x सम्मिलित है", एक विशेष x और एक प्रमाण होना चाहिए कि इसकी संपत्ति "p" है। प्रारूप सिद्धांत में, निर्भर उत्पाद प्रकार का उपयोग करके स्थिति को पूरा किया जाता है और इसके प्रमाण के लिए उस प्रकार की एक अवधि की आवश्यकता होती है। पद t के लिए, "पहला t" x का उत्पादन करेगा और "दूसरा t" P(x) के प्रमाण का उत्पादन करेगा।
+गैर-रचनात्मक प्रमाण का एक उदाहरण "विरोधाभास द्वारा प्रमाण" है। पहला चरण यह मानकर चल रहा है कि x की स्थिति नहीं है और विरोधाभास द्वारा इसका खंडन किया जा रहा है। उस चरण से निष्कर्ष "ऐसा नहीं है कि x सम्मिलित नहीं है"। अंतिम चरण है, द्विक निषेध द्वारा, यह निष्कर्ष निकालना कि x की स्थिति है। स्पष्ट होने के लिए, रचनात्मक गणित अभी भी "विरोधाभास द्वारा खंडन" की अनुमति देता है। यह साबित कर सकता है कि "ऐसा नहीं है कि x सम्मिलित नहीं है"। लेकिन रचनात्मक गणित द्विक निषेध को हटाने के अंतिम चरण को यह निष्कर्ष निकालने की अनुमति नहीं देता है कि x सम्मिलित है।<ref>{{cite web |title=proof by contradiction |url=https://ncatlab.org/nlab/show/proof+by+contradiction |website=nlab |access-date=29 December 2021}}</ref>
-एक गैर-कंस्ट्रक्टिव सबूत का एक उदाहरण विरोधाभास द्वारा एक प्रमाण है।पहला कदम यह मान रहा है कि <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>
+हालांकि श्रेणी सिद्धांत के लिए प्रारंभिक प्रेरणा मूलभूततावाद से बहुत दूर थी, लेकिन दोनों क्षेत्रों में गहरा संबंध था। जैसा कि जॉन लेन बेल लिखते हैं: "वास्तव में श्रेणियों को स्वयं एक निश्चित प्रकार के प्रकार के सिद्धांतों के रूप में देखा जा सकता है; यह तथ्य अकेले इंगित करता है कि प्रकार सिद्धांत श्रेणी सिद्धांत से बहुत अधिक निकटता से संबंधित है, जितना कि सिद्धांत को व्यवस्थित करना है।" संक्षेप में, एक श्रेणी को उसकी वस्तुओं को प्रकार (या प्रारूप) के रूप में देखकर एक प्रकार के सिद्धांत के रूप में देखा जा सकता है, अर्थात "सामान्य रूप से, एक श्रेणी को इसके संरचना से रहित प्रारूप सिद्धांत के रूप में माना जा सकता है।" इस प्रकार कई महत्वपूर्ण परिणाम सामने आते हैं।<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) के अनुरूप है;
+* कार्तीय बंद श्रेणियां टाइप किए गए λ-कलन (लैम्बेक, 1970) के अनुरूप हैं;
-* [[सी-मोनोइड]]्स (उत्पादों और घातांक के साथ श्रेणियां और एक गैर-टर्मिनल ऑब्जेक्ट) अप्रकाशित λ-Calculus (1980 के आसपास लैम्बेक और [[दाना स्कॉट]] द्वारा स्वतंत्र रूप से मनाया गया) के अनुरूप;
+* [[सी-मोनोइड|c-मोनोइड]] (उत्पादों और घातांक के साथ श्रेणियां और एक गैर-टर्मिनल वस्तुओ) अप्रकाशित λ-गणना (1980 के आसपास लैम्बेक और [[दाना स्कॉट]] द्वारा स्वतंत्र रूप से मनाया गया) के अनुरूप;
-* [[स्थानीय रूप से कार्टेशियन बंद श्रेणी]] मार्टिन-लोफ  प्ररूप सिद्धांत के अनुरूप है। मार्टिन-लोफ टाइप थ्योरीज़ (सेली, 1984)।
+* स्थानीय रूप से कार्टेशियन बंद श्रेणियां मार्टिन-लोफ प्रकार के सिद्धांतों (सीली, 1984) के अनुरूप हैं।
-इंटरप्ले, जिसे [[श्रेणीबद्ध तर्क]] के रूप में जाना जाता है, तब से सक्रिय अनुसंधान का विषय रहा है;उदाहरण के लिए जैकब्स (1999) का मोनोग्राफ देखें।
+परस्पर क्रिया, जिसे श्रेणीबद्ध तर्क के रूप में जाना जाता है, तब से सक्रिय शोध का विषय रहा है; उदाहरण के लिए जैकब्स (1999) का मोनोग्राफ देखें।
-समस्थेयता  प्ररूप सिद्धांत  प्ररूप सिद्धांत और श्रेणी सिद्धांत को संयोजित करने का प्रयास करता है।यह समानता पर केंद्रित है, विशेष रूप से प्रकारों के बीच समानताएं।
+समस्थेयता प्ररूप सिद्धांत प्ररूप सिद्धांत और श्रेणी सिद्धांत को संयोजित करने का प्रयास करता है। यह समानता, विशेष रूप से प्रकारों के बीच समानता पर केंद्रित है।
 == टाइप थ्योरीज़ की सूची ==
-=== मेजर ===
+=== प्रमुख ===
-* बस टाइप किया गया लैम्ब्डा गणना जो एक उच्च-क्रम तर्क है
+* सरलतम टाइप किया गया लैम्ब्डा गणना जो एक उच्च-क्रम तर्क है
-* अंतर्ज्ञानवादी  प्ररूप सिद्धांत
+* अंतर्ज्ञानवादी प्ररूप सिद्धांत
-* प्रणाली एफ
+* प्रणाली F
-* तार्किक ढांचे का उपयोग प्रायः अन्य प्रकार के सिद्धांतों को परिभाषित करने के लिए किया जाता है
+* LF का प्रयोग प्रायः अन्य प्रकार के सिद्धांतों को परिभाषित करने के लिए किया जाता है
-* निर्माणों और उसके डेरिवेटिव की पथरी
+* निर्माणों और उसके व्युत्पन्न पद की गणना
-=== माइनर ===
+=== गौण ===
-* [[स्वचालित]]
+* [[स्वचालित|ऑटोमैथ]]
-* सेंट  प्ररूप सिद्धांत
+* समुच्चय प्ररूप सिद्धांत
-* UTT (LUO का एकीकृत सिद्धांत पर निर्भर प्रकार)
+* यूटीटी (लुओ का आश्रित प्रकार का एकीकृत सिद्धांत)
-* [[संयोजक तर्क]] के कुछ रूप
+* कुछ प्रकार के संयोजन तर्क
-* अन्य लोग लैम्ब्डा क्यूब में परिभाषित किए गए (जिसे शुद्ध प्रकार के प्रणाली के रूप में भी जाना जाता है)
+* अन्य लोग लैम्ब्डा घन में परिभाषित किए गए (जिसे शुद्ध प्रकार के प्रणाली के रूप में भी जाना जाता है)
 * अन्य नाम के अंतर्गत लैम्ब्डा गणना टाइप किया गया
 === सक्रिय अनुसंधान ===
-* समस्थेयता  प्ररूप सिद्धांत प्रकारों की समानता की खोज करता है
+* समस्थेयता प्ररूप सिद्धांत प्रकारों की समानता की खोज करता है
-*NLAB: क्यूबिकल+टाइप+ उपागम समस्थेयता  प्ररूप सिद्धांत का कार्यान्वयन है
+*घनीय प्रारूप उपागम समस्थेयता प्ररूप सिद्धांत का कार्यान्वयन है
 == अनुप्रयोग ==
@@ Line 473: / Line 475: @@
 कंप्यूटर पर गणित को एन्कोड करने के लिए ऑटोमैथ नामक पहले कंप्यूटर प्रमाण सहायक ने प्रारूप सिद्धांत का इस्तेमाल किया। मार्टिन-लोफ ने गणित के लिए एक नई नींव के रूप में सेवा करने के लिए सभी गणित को एन्कोड करने के लिए विशेष रूप से अंतर्ज्ञानवादी प्रकार सिद्धांत विकसित किया। समस्थेयता प्रकार के सिद्धांत का उपयोग करते हुए गणितीय नींव में अनुसंधान जारी है।
-श्रेणी सिद्धांत में काम करने वाले गणितज्ञों को पहले से ही ज़र्मेलो-फ्रेंकेल समुच्चय सिद्धांत की व्यापक रूप से स्वीकृत संस्थान के साथ काम करने में कठिनाई हुई थी। इससे व्यवस्थित ईटीसीएस (यूरोपीय ट्रेन नियंत्रण प्रणाली) की श्रेणी के लॉवर के प्राथमिक सिद्धांत जैसे प्रस्ताव सामने आए।<ref>{{nlab|id=ETCS}}</ref>  प्ररूप सिद्धांत का उपयोग करके इस लाइन में समस्थेयता (होमोटॉपी) प्ररूप सिद्धांत जारी है। शोधकर्ता निर्भर प्रकारों (विशेष रूप से पहचान प्रकार) और बीजगणितीय सांस्थिति (विशेष रूप से होमोटॉपी) के बीच संबंधों की खोज कर रहे हैं।
+श्रेणी सिद्धांत में काम करने वाले गणितज्ञों को पहले से ही ज़र्मेलो-फ्रेंकेल समुच्चय सिद्धांत की व्यापक रूप से स्वीकृत संस्थान के साथ काम करने में कठिनाई हुई थी। इससे व्यवस्थित ईटीसीएस (यूरोपीय ट्रेन नियंत्रण प्रणाली) की श्रेणी के लॉवर के प्राथमिक सिद्धांत जैसे प्रस्ताव सामने आए।<ref>{{nlab|id=ETCS}}</ref> प्ररूप सिद्धांत का उपयोग करके इस लाइन में समस्थेयता (होमोटॉपी) प्ररूप सिद्धांत जारी है। शोधकर्ता निर्भर प्रकारों (विशेष रूप से पहचान प्रकार) और बीजगणितीय सांस्थिति (विशेष रूप से होमोटॉपी) के बीच संबंधों की खोज कर रहे हैं।
 === प्रमाण सहायक ===
@@ Line 480: / Line 482: @@
 प्ररूप सिद्धांत में अधिकांश सम्मिलित शोध प्रमाण जाँचकर्ता, अन्योन्यक्रिया प्रमाण सहायक और स्वचालित प्रमेय समर्थक द्वारा संचालित होते हैं। इनमें से अधिकांश प्रणालियाँ एन्कोडिंग प्रमाणों के लिए गणितीय आधार के रूप में एक प्रकार के सिद्धांत का उपयोग करती हैं, जो आश्चर्यजनक नहीं है, प्रारूप सिद्धांत और प्रोग्रामिंग भाषाओं के बीच घनिष्ठ संबंध को देखते हुए:
 * अन्य प्रकार के सिद्धांतों को परिभाषित करने के लिए तार्किक रूपरेखा का उपयोग प्रायः ट्वेलफ द्वारा किया जाता है;
-* कई  प्ररूप सिद्धांत जो उच्च-क्रम के तर्क के अंतर्गत आते हैं, उनका उपयोग उच्च क्रम की भाषा (प्रमाण सहायक) और [[प्रोटोटाइप सत्यापन तंत्र|प्रोटोटाइप सत्यापन प्रणाली]] द्वारा किया जाता है;
+* कई प्ररूप सिद्धांत जो उच्च-क्रम के तर्क के अंतर्गत आते हैं, उनका उपयोग उच्च क्रम की भाषा (प्रमाण सहायक) और [[प्रोटोटाइप सत्यापन तंत्र|प्रोटोटाइप सत्यापन प्रणाली]] द्वारा किया जाता है;
-* संगणनात्मक  प्रकार के सिद्धांत का उपयोग एनयूपीआरएल द्वारा किया जाता है;
+* संगणनात्मक प्रकार के सिद्धांत का उपयोग एनयूपीआरएल द्वारा किया जाता है;
-* कॉक, मटिटा, और लीन द्वारा निर्माण और इसके व्युत्पन्न शब्द की गणना का उपयोग किया जाता है;
+* कॉक, मटिटा, और लीन द्वारा निर्माण और इसके व्युत्पन्न पद की गणना का उपयोग किया जाता है;
-* यूटीटी (लुओ की निर्भरता के प्रकारों का एकीकृत सूत्र सिद्धांत) का उपयोग  ऑस्ट्रेलियाई ग्राफिक डिजाइन संघ (प्रोग्रामिंग भाषा) द्वारा किया जाता है जो [[अगदा (प्राग्रामिंग भाषा)|प्राग्रामिंग भाषा]] और प्रमाण सहायक दोनों है
+* यूटीटी (लुओ की निर्भरता के प्रकारों का एकीकृत सूत्र सिद्धांत) का उपयोग ऑस्ट्रेलियाई ग्राफिक डिजाइन संघ (प्रोग्रामिंग भाषा) द्वारा किया जाता है जो [[अगदा (प्राग्रामिंग भाषा)|प्राग्रामिंग भाषा]] और प्रमाण सहायक दोनों है
-लेगो और इसाबेल द्वारा कई प्रकार के सिद्धांतों का समर्थन किया जाता है। इसाबेल जेडएफसी जैसे प्रारूप सिद्धांत के अतिरिक्त संस्थान का भी समर्थन करती है। मिज़ार प्रमाणित प्रणाली का एक उदाहरण है  जो केवल समुच्चय सिद्धांत का समर्थन करता है।
+लेगो और इसाबेल द्वारा कई प्रकार के सिद्धांतों का समर्थन किया जाता है। इसाबेल जेडएफसी जैसे प्रारूप सिद्धांत के अतिरिक्त संस्थान का भी समर्थन करती है। मिज़ार प्रमाणित प्रणाली का एक उदाहरण है जो केवल समुच्चय सिद्धांत का समर्थन करता है।
 === प्रोग्रामिंग (क्रमादेशन) भाषाएँ ===
-कोई भी स्थिर प्रोग्राम विश्लेषण, जैसे कि [[संकलक]] के सिमेंटिक विश्लेषण (कंपाइलर) चरण में प्रारूप की जाँच एल्गोरिदम,  प्ररूप सिद्धांत से जुड़ा है। एक प्रमुख उदाहरण एजीडीए है, एक प्रोग्रामिंग भाषा जो अपने प्रकार की प्रणाली के लिए यूटीटी (लुओ का आश्रित प्रारूप का एकीकृत सिद्धांत) का उपयोग करती है।
+कोई भी स्थिर प्रोग्राम विश्लेषण, जैसे कि [[संकलक]] के सिमेंटिक विश्लेषण (कंपाइलर) चरण में प्रारूप की जाँच एल्गोरिदम, प्ररूप सिद्धांत से जुड़ा है। एक प्रमुख उदाहरण एजीडीए है, एक प्रोग्रामिंग भाषा जो अपने प्रकार की प्रणाली के लिए यूटीटी (लुओ का आश्रित प्रारूप का एकीकृत सिद्धांत) का उपयोग करती है।
-प्रोग्रामिंग भाषा [[एमएल (प्रोग्रामिंग भाषा)|यंत्र अधिगम (प्रोग्रामिंग भाषा)]] को प्रकार के सिद्धांतों में  कुशलतापूर्वक प्रयोग करने के लिए विकसित किया गया था (गणना योग्य फलन के लिए तर्क देखें) और और इसका अपना प्रारूप प्रणाली उनसे काफी प्रभावित था।
+प्रोग्रामिंग भाषा [[एमएल (प्रोग्रामिंग भाषा)|यंत्र अधिगम (प्रोग्रामिंग भाषा)]] को प्रकार के सिद्धांतों में कुशलतापूर्वक प्रयोग करने के लिए विकसित किया गया था (गणना योग्य फलन के लिए तर्क देखें) और और इसका अपना प्रारूप प्रणाली उनसे काफी प्रभावित था।
 === भाषाविज्ञान ===
-प्ररूप सिद्धांत का व्यापक रूप से प्राकृतिक भाषाओं के शब्दार्थ के औपचारिक सिद्धांतों में विशेष रूप से मोंटेग व्याकरण और उसके वंशजों में उपयोग किया जाता है।<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> विशेष रूप से, श्रेणीबद्ध व्याकरण और  प्राक् समूह व्याकरण शब्दों के प्रकार (संज्ञा, क्रिया, आदि) को परिभाषित करने के लिए व्यापक रूप से प्रारूप संरचक का उपयोग करते हैं।
+प्ररूप सिद्धांत का व्यापक रूप से प्राकृतिक भाषाओं के शब्दार्थ के औपचारिक सिद्धांतों में विशेष रूप से मोंटेग व्याकरण और उसके वंशजों में उपयोग किया जाता है।<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  लेता है, और प्रकारों के समूह को पुनरावर्ती रूप से निम्नानुसार परिभाषित करता है:
+सबसे सामान्य निर्माण क्रमशः विशिष्ट और सत्यता मान के लिए मूल प्रकार 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}}
+एक जटिल प्रकार <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}}
@@ Line 563: / Line 565: @@
 === परिचयात्मक सामग्री ===
 * [https://ncatlab.org/nlab/show/type+theory प्ररूप सिद्धांत NLAB पर], जिसमें कई विषयों पर लेख हैं।
-*[https://plato.stanford.edu/entries/type-theory-intuitionistic/ intuitionistic  प्ररूप सिद्धांत] दर्शन के स्टैनफोर्ड एनसाइक्लोपीडिया में लेख
+*[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://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://www.cse.chalmers.se/research/group/logic/book/book.pdf मार्टिन-Löf के प्ररूप सिद्धांत में प्रोग्रामिंग] बुक
-*[https://homotopytypetheory.org/book/ homotopy  प्ररूप सिद्धांत] पुस्तक, जिसने एक गणितीय आधार  के रूप में समस्थेयता  प्ररूप सिद्धांत को प्रस्तावित किया।
+*[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 के बाद से काम कर रहा है।
+* [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 का
@@ Line 587: / Line 589: @@
 {{DEFAULTSORT:Type Theory}}
-श्रेणी:  प्ररूप सिद्धांत
+श्रेणी: प्ररूप सिद्धांत
 श्रेणी: औपचारिक तर्क प्रणाली
 श्रेणी: पदानुक्रम
+[[Category:All articles with incomplete citations|Type Theory]]
-[[Category: Machine Translated Page]]
+[[Category:Articles with hatnote templates targeting a nonexistent page|Type Theory]]
-[[Category:Created On 13/02/2023]]
+[[Category:Articles with incomplete citations from July 2022|Type Theory]]
+[[Category:CS1 English-language sources (en)]]
+[[Category:CS1 maint]]
+[[Category:Collapse templates|Type Theory]]
+[[Category:Created On 13/02/2023|Type Theory]]
+[[Category:Lua-based templates|Type Theory]]
+[[Category:Machine Translated Page|Type Theory]]
+[[Category:Navigational boxes| ]]
+[[Category:Navigational boxes without horizontal lists|Type Theory]]
+[[Category:Pages that use a deprecated format of the math tags|Type Theory]]
+[[Category:Pages with empty portal template|Type Theory]]
+[[Category:Pages with script errors|Type Theory]]
+[[Category:Portal-inline template with redlinked portals|Type Theory]]
+[[Category:Short description with empty Wikidata description|Type Theory]]
+[[Category:Sidebars with styles needing conversion|Type Theory]]
+[[Category:Template documentation pages|Documentation/doc]]
+[[Category:Templates Vigyan Ready|Type Theory]]
+[[Category:Templates generating microformats|Type Theory]]
+[[Category:Templates that add a tracking category|Type Theory]]
+[[Category:Templates that are not mobile friendly|Type Theory]]
+[[Category:Templates that generate short descriptions|Type Theory]]
+[[Category:Templates using TemplateData|Type Theory]]
+[[Category:Wikipedia metatemplates|Type Theory]]

Anonymous

Search