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

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

इतिहास

Main article: प्रकार सिद्धांत का इतिहास

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

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

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

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

परिचय

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

मूल तत्व

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

प्ररूप सिद्धांत में, प्रत्येक पद का एक प्रकार होता है। एक पद और इसके प्रकार को प्रायः "पद: प्रकार" के रूप में एक साथ लिखा जाता है। प्ररूप सिद्धांत में सम्मिलित करने के लिए एक सामान्य प्रकार प्राकृतिक संख्या है, जिसे प्रायः "$\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}$ आदि सम्मिलित है।

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

उदाहरण के लिए:

मार्टिन-लोफ प्रकार के सिद्धांत का खुलापन विशेष रूप से तथाकथित विश्व समष्टि के परिचय में प्रकट होता है। प्रारूप के विश्व समष्टि प्रतिबिंब की अनौपचारिक धारणा को समाहित करते हैं जिनकी भूमिका को निम्नानुसार समझाया जा सकता है। प्रारूप सिद्धांत के एक विशेष औपचारिकता के विकास के समय, प्रारूप सिद्धांतवादी प्रारूप के नियमों पर वापस देख सकते हैं, कहते हैं, 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 एक सुनिर्मित सूत्र है।" प्ररूप सिद्धांत में अतिरिक्त निर्णय होते हैं जो प्रकारों और संबंधित पदों को प्रकारों तक परिभाषित करते हैं।

शर्तें

तर्क में एक पद को पुनरावर्ती रूप से एक स्थिर प्रतीक, चर, या एक फलन अनुप्रयोग के रूप में परिभाषित किया जाता है, जहां एक पद दूसरे पद पर लागू होता है। कुछ स्थिर प्रतीक प्राकृतिक संख्याओं के "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", आदि वास्तव में जटिल पदों से मिलकर बने हो सकते हैं जिनमें कई फलन अनुप्रयोग होते हैं, न कि केवल एकल प्रतीकों मे होते है।

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

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

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

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

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

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

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

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

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

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

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

प्रारूपों के कुछ संयोजन प्रकार के अन्य संयोजनों के बराबर हैं। जब कार्यों को घातांक माना जाता है, तो प्रकारों के संयोजन को बीजगणितीय पहचान के समान लिखा जा सकता है। इस प्रकार, ${\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}$।

अभिगृहीत

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

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

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

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

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

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

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

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

Main article: प्रारूप स्थिति

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

एक प्रकार का वातावरण $\Gamma$ और एक प्रकार $\tau$, को देखते हुए, तय करें कि क्या कोई पद $e$ सम्मिलित है जिसे प्रारूप के वातावरण $\tau$ में प्रारूप $\Gamma$ निर्दिष्ट किया जा सकता है।

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

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

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

Main article: प्रारूप का अनुमान

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

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

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

व्याख्या

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

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

जब एक नींव के रूप में उपयोग किया जाता है, तो कुछ प्रकारों की व्याख्या प्रस्तावों के रूप में की जाती है (ऐसे कथन जिन्हें सिद्ध किया जा सकता है) और प्रकार का एक पद उस प्रस्ताव का प्रमाण है। इस प्रकार, प्रकार "Π 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 सम्मिलित है।

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

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

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

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

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

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

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

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

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

प्रमुख

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

गौण

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

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

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

अनुप्रयोग

गणितीय आधार

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

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

प्रमाण सहायक

Main article: प्रमाण सहायक

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

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

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

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

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

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

भाषाविज्ञान

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

सबसे सामान्य निर्माण क्रमशः विशिष्ट और सत्यता मान के लिए मूल प्रकार 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)।

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

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

यह भी देखें

• गणित की आधार

अग्रिम पठन

• 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.

बाहरी संबंध

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

• प्ररूप सिद्धांत 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 प्रकार, तर्क, शब्दार्थ और सत्यापन
• आंद्रेज बाउर का ब्लॉग

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