अंतर्ज्ञानवादी प्रकार का सिद्धांत

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

डिजाइन

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

तार्किक संयोजकों के साथ एक-से-एक पत्राचार का पालन करने के लिए अंतर्ज्ञानवादी प्रकार के सिद्धांत के प्रकार के निर्माता बनाए गए थे। उदाहरण के लिए, तार्किक संयोजक जिसे निहितार्थ कहा जाता है ($A\implies B$) एक समारोह के प्रकार से मेल खाती है ($A\to B$). इस पत्राचार को करी-हावर्ड समरूपता कहा जाता है। पिछले प्रकार के सिद्धांतों ने भी इस तुल्याकारिता का अनुसरण किया था, लेकिन मार्टिन-लोफ़ ने सबसे पहले आश्रित प्रकारों को प्रस्तुत करके तर्क को विधेय करने के लिए इसका विस्तार किया।

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

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

यदि आप टाइप थ्योरी से अपरिचित हैं और सेट थ्योरी जानते हैं, तो एक त्वरित सारांश है: प्रकारों में शब्द होते हैं जैसे सेट में तत्व होते हैं। शर्तें एक और केवल एक प्रकार की होती हैं। शर्तें जैसे $2+2$ और $2\cdot 2$ 4 जैसे विहित शब्दों तक गणना (कम करें) करें। अधिक जानकारी के लिए, प्रकार सिद्धांत पर लेख देखें।

0 प्रकार, 1 प्रकार और 2 प्रकार

3 परिमित प्रकार हैं: 0 प्रकार में 0 पद होते हैं। 1 प्रकार में 1 प्रामाणिक शब्द है। और 2 प्रकार में 2 विहित शब्द हैं।

क्योंकि 0 प्रकार में 0 पद होते हैं, इसे रिक्त प्रकार भी कहा जाता है। इसका उपयोग ऐसी किसी भी चीज़ का प्रतिनिधित्व करने के लिए किया जाता है जो मौजूद नहीं हो सकती। यह भी लिखा है $\bot$ और कुछ भी अपुष्ट का प्रतिनिधित्व करता है। (अर्थात्, इसका प्रमाण मौजूद नहीं हो सकता है।) परिणामस्वरूप, निषेध को इसके कार्य के रूप में परिभाषित किया गया है: $\neg A:=A\to \bot$.

इसी तरह, 1 प्रकार में 1 विहित शब्द होता है और अस्तित्व का प्रतिनिधित्व करता है। इसे इकाई प्रकार भी कहा जाता है। यह अक्सर उन प्रस्तावों का प्रतिनिधित्व करता है जिन्हें सिद्ध किया जा सकता है और इसलिए, कभी-कभी लिखा जाता है $\top$.

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

Σ टाइप कन्स्ट्रक्टर

Σ-प्रकार में आदेशित जोड़े होते हैं। ठेठ आदेशित जोड़ी (या 2-ट्यूपल) प्रकारों के साथ, एक Σ-प्रकार कार्टेशियन उत्पाद का वर्णन कर सकता है, $A\times B$, दो अन्य प्रकार के, $A$ और $B$. तार्किक रूप से, इस तरह के आदेशित युग्म का एक प्रमाण होगा $A$ और का एक प्रमाण $B$, इसलिए कोई इस प्रकार लिखा हुआ देख सकता है $A\wedge B$.

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

$\sum _{n\mathbin {:} {\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)$

सेट-थ्योरी शब्दावली का उपयोग करते हुए, यह सेट के अनुक्रमित असंयुक्त संघों के समान है। सामान्य क्रमित युग्मों के मामले में, दूसरे पद का प्रकार पहले पद के मान पर निर्भर नहीं करता है। इस प्रकार कार्तीय उत्पाद का वर्णन करने वाला प्रकार ${\mathbb {N} }\times {\mathbb {R} }$ लिखा है:

$\sum _{n\mathbin {:} {\mathbb {N} }}{\mathbb {R} }$

यहाँ यह ध्यान रखना महत्वपूर्ण है कि पहले पद का मान, $n$, दूसरे पद के प्रकार पर निर्भर नहीं है, ${\mathbb {R} }$.

Σ-प्रकार का उपयोग गणित और अधिकांश प्रोग्रामिंग भाषाओं में उपयोग किए जाने वाले रिकॉर्ड (कंप्यूटर विज्ञान) में उपयोग किए जाने वाले निर्भर रूप से टाइप किए गए टुपल्स के निर्माण के लिए किया जा सकता है। आश्रित रूप से टाइप किए गए 3-ट्यूपल का एक उदाहरण दो पूर्णांक हैं और एक प्रमाण है कि पहला पूर्णांक दूसरे पूर्णांक से छोटा है, जिसे इस प्रकार वर्णित किया गया है:

$\sum _{m\mathbin {:} {\mathbb {Z} }}{\sum _{n\mathbin {:} {\mathbb {Z} }}((m<n)={\text{True}})}$

आश्रित टाइपिंग Σ-प्रकार को अस्तित्वगत क्वांटिफायर की भूमिका निभाने की अनुमति देती है। वहाँ बयान मौजूद है $n$ प्रकार का ${\mathbb {N} }$, ऐसा है कि $P(n)$ सिद्ध किया गया आदेशित जोड़े का प्रकार बन जाता है जहां पहला आइटम मान होता है $n$ प्रकार का ${\mathbb {N} }$ और दूसरी वस्तु का प्रमाण है $P(n)$. ध्यान दें कि दूसरी वस्तु का प्रकार (के प्रमाण $P(n)$) क्रमित युग्म के पहले भाग के मान पर निर्भर करता है ($n$). इसका प्रकार होगा:

$\sum _{n\mathbin {:} {\mathbb {N} }}P(n)$

Π टाइप कन्स्ट्रक्टर

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

एक उदाहरण के रूप में, एक फ़ंक्शन का प्रकार, जिसे एक प्राकृतिक संख्या दी गई है $n$, युक्त सदिश लौटाता है $n$ वास्तविक संख्याएँ लिखी जाती हैं:

$\prod _{n\mathbin {:} {\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)$

जब आउटपुट प्रकार इनपुट मान पर निर्भर नहीं करता है, तो फ़ंक्शन प्रकार को अक्सर केवल a के साथ लिखा जाता है $\to$. इस प्रकार, ${\mathbb {N} }\to {\mathbb {R} }$ प्राकृतिक संख्या से वास्तविक संख्या तक के कार्यों का प्रकार है। ऐसे Π-प्रकार तार्किक निहितार्थ के अनुरूप हैं। तार्किक प्रस्ताव $A\implies B$ प्रकार से मेल खाता है $A\to B$, जिसमें ऐसे कार्य होते हैं जो प्रूफ-ऑफ-ए लेते हैं और प्रूफ-ऑफ-बी लौटाते हैं। इस प्रकार को अधिक सुसंगत रूप से लिखा जा सकता है:

$\prod _{a\mathbin {:} A}B$

सार्वभौमिक परिमाणीकरण के लिए तर्क में Π-प्रकार का भी उपयोग किया जाता है। प्रत्येक के लिए बयान $n$ प्रकार का ${\mathbb {N} }$, $P(n)$ सिद्ध होता है से एक कार्य बन जाता है $n$ प्रकार का ${\mathbb {N} }$ के सबूत के लिए $P(n)$. इस प्रकार, के लिए मूल्य दिया $n$ फ़ंक्शन एक प्रमाण उत्पन्न करता है कि $P()$ उस मान के लिए रखता है। प्रकार होगा

$\prod _{n\mathbin {:} {\mathbb {N} }}P(n)$

= कंस्ट्रक्टर टाइप करें

=-प्रकार दो शब्दों से बनाए जाते हैं। जैसे दो पद दिए गए हैं $2+2$ और $2\cdot 2$, आप एक नया प्रकार बना सकते हैं $2+2=2\cdot 2$. उस नए प्रकार की शर्तें इस सबूत का प्रतिनिधित्व करती हैं कि जोड़ी एक ही प्रामाणिक शब्द तक कम हो जाती है। इस प्रकार, दोनों के बाद से $2+2$ और $2\cdot 2$ विहित शब्द की गणना करें $4$, प्रकार का एक शब्द होगा $2+2=2\cdot 2$. अंतर्ज्ञानवादी प्रकार के सिद्धांत में, =-प्रकार की शर्तों को बनाने का एक ही तरीका है और वह रिफ्लेक्सिव रिलेशन द्वारा है:

$\operatorname {refl} \mathbin {:} \prod _{a\mathbin {:} A}(a=a).$

=-प्रकार जैसे बनाना संभव है $1=2$ जहां शर्तें एक ही प्रामाणिक शब्द तक कम नहीं होतीं, लेकिन आप उस नए प्रकार की शर्तों को बनाने में असमर्थ होंगे। वास्तव में, यदि आप का एक शब्द बनाने में सक्षम थे $1=2$, आप का एक शब्द बना सकते हैं $\bot$. इसे एक फंक्शन में डालने से एक प्रकार का फंक्शन उत्पन्न होगा $1=2\to \bot$. तब से $\ldots \to \bot$ यह है कि कैसे अंतर्ज्ञानवादी प्रकार का सिद्धांत निषेध को परिभाषित करता है, आपके पास होगा $\neg (1=2)$ या, अंत में, $1\neq 2$.

प्रमाणों की समानता प्रमाण सिद्धांत में सक्रिय अनुसंधान का एक क्षेत्र है और इसने होमोटॉपी प्रकार के सिद्धांत और अन्य प्रकार के सिद्धांतों के विकास को प्रेरित किया है।

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

Main article: Inductive type

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

आगमनात्मक प्रकार शून्य जैसे नए स्थिरांक को परिभाषित करते हैं $0\mathbin {:} {\mathbb {N} }$ और उत्तराधिकारी समारोह $S\mathbin {:} {\mathbb {N} }\to {\mathbb {N} }$. तब से $S$ इसकी कोई परिभाषा नहीं है और प्रतिस्थापन, जैसे शब्दों का उपयोग करके इसका मूल्यांकन नहीं किया जा सकता है $S0$ और $SSS0$ प्राकृतिक संख्याओं के विहित पद बन जाते हैं।

स्ट्रक्चरल इंडक्शन द्वारा आगमनात्मक प्रकारों पर प्रमाण संभव हैं। प्रत्येक नए आगमनात्मक प्रकार का अपना आगमनात्मक नियम होता है। एक विधेय साबित करने के लिए $P()$ प्रत्येक प्राकृतिक संख्या के लिए, आप निम्नलिखित नियम का उपयोग करते हैं:

${\operatorname {{\mathbb {N} }-elim} }\,\mathbin {:} P(0)\,\to \left(\prod _{n\mathbin {:} {\mathbb {N} }}P(n)\to P(S(n))\right)\to \prod _{n\mathbin {:} {\mathbb {N} }}P(n)$

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

ब्रह्मांड प्रकार

ब्रह्मांड प्रकार अन्य प्रकार के कंस्ट्रक्टरों के साथ बनाए गए सभी प्रकारों के बारे में प्रमाण लिखने की अनुमति देता है। ब्रह्मांड प्रकार में हर शब्द ${\mathcal {U}}_{0}$ के किसी भी संयोजन के साथ बनाए गए प्रकार के लिए मैप किया जा सकता है $0,1,2,\Sigma ,\Pi ,=,$ और आगमनात्मक प्रकार के निर्माता। हालाँकि, विरोधाभास से बचने के लिए, इसमें कोई शब्द नहीं है ${\mathcal {U}}_{0}$ जो मैप करता है ${\mathcal {U}}_{0}$.

सभी छोटे प्रकारों के बारे में प्रमाण लिखना और ${\mathcal {U}}_{0}$, तुम्हें अवश्य उपयोग करना चाहिए ${\mathcal {U}}_{1}$, जिसमें के लिए एक शब्द है ${\mathcal {U}}_{0}$, लेकिन अपने लिए नहीं ${\mathcal {U}}_{1}$. इसी प्रकार, के लिए ${\mathcal {U}}_{2}$. ब्रह्मांडों का एक अभेद्यता पदानुक्रम है, इसलिए किसी निश्चित स्थिरांक पर एक प्रमाण की मात्रा निर्धारित करने के लिए $k$ ब्रह्मांड, आप उपयोग कर सकते हैं ${\mathcal {U}}_{k+1}$.

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

निर्णय

अंतर्ज्ञानवादी प्रकार के सिद्धांत की औपचारिक परिभाषा निर्णयों का उपयोग करते हुए लिखी गई है। उदाहरण के लिए, यदि कथन में $A$ एक प्रकार है और $B$ तब एक प्रकार है $\textstyle \sum _{a:A}B$ एक प्रकार है वहाँ के निर्णय हैं एक प्रकार है, और, और यदि ... तो ...। भाव $\textstyle \sum _{a:A}B$ निर्णय नहीं है; यह परिभाषित किया जा रहा प्रकार है।

टाइप थ्योरी का यह दूसरा स्तर भ्रामक हो सकता है, खासकर जहां समानता की बात आती है। शब्द समानता का एक निर्णय है, जो कह सकता है $4=2+2$. यह एक कथन है कि दो शब्द एक ही विहित शब्द में घटते हैं। प्रकार समानता का एक निर्णय भी है, ऐसा कहें $A=B$, जिसका अर्थ है हर तत्व $A$ प्रकार का तत्व है $B$ और इसके विपरीत। प्रकार के स्तर पर, एक प्रकार होता है $4=2+2$ और इसमें शर्तें शामिल हैं यदि कोई प्रमाण है कि $4$ और $2+2$ उसी मूल्य को कम करें। (इस प्रकार की शर्तें शब्द-समानता निर्णय का उपयोग करके उत्पन्न होती हैं।) अंत में, समानता का एक अंग्रेजी-भाषा स्तर है, क्योंकि हम शब्द चार और प्रतीक का उपयोग करते हैं$4$विहित शब्द का उल्लेख करने के लिए $SSSS0$. इस तरह के समानार्थी शब्दों को मार्टिन-लोफ द्वारा निश्चित रूप से बराबर कहा जाता है।

नीचे दिए गए फैसलों का विवरण नॉर्डस्ट्रॉम, पीटरसन और स्मिथ में हुई चर्चा पर आधारित है।

औपचारिक सिद्धांत प्रकार और वस्तुओं के साथ काम करता है।

एक प्रकार द्वारा घोषित किया गया है:

• $A\ {\mathsf {Type}}$

एक वस्तु मौजूद है और एक प्रकार में है यदि:

• $a\mathbin {:} A$

वस्तुएं बराबर हो सकती हैं

• $a=b$

और प्रकार बराबर हो सकते हैं

• $A=B$

एक प्रकार जो किसी वस्तु पर दूसरे प्रकार से निर्भर करता है, घोषित किया जाता है

• $(x\mathbin {:} A)B$

और प्रतिस्थापन द्वारा हटा दिया गया

• $B[x/a]$, चर की जगह $x$ वस्तु के साथ $a$ में $B$.

एक वस्तु जो किसी वस्तु पर दूसरे प्रकार से निर्भर करती है, दो तरह से की जा सकती है। यदि वस्तु अमूर्त है, तो इसे लिखा जाता है

• $[x]b$

और प्रतिस्थापन द्वारा हटा दिया गया

• $b[x/a]$, चर की जगह $x$ वस्तु के साथ $a$ में $b$.

ऑब्जेक्ट-ऑन-ऑब्जेक्ट को रिकर्सिव प्रकार के हिस्से के रूप में स्थिर के रूप में भी घोषित किया जा सकता है। पुनरावर्ती प्रकार का एक उदाहरण है:

• $0\mathbin {:} \mathbb {N}$
• $S\mathbin {:} \mathbb {N} \to \mathbb {N}$

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

${\begin{aligned}\operatorname {add} &\mathbin {:} \ (\mathbb {N} \times \mathbb {N} )\to \mathbb {N} \\\operatorname {add} (0,b)&=b\\\operatorname {add} (S(a),b)&=S(\operatorname {add} (a,b)))\end{aligned}}$

$S$ एक अपारदर्शी स्थिरांक के रूप में हेरफेर किया जाता है - इसमें प्रतिस्थापन के लिए कोई आंतरिक संरचना नहीं होती है।

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

$\Gamma \vdash \sigma \ {\mathsf {Type}}$	σ is a well-formed type in the context Γ.
$\Gamma \vdash t\mathbin {:} \sigma$	t is a well-formed term of type σ in context Γ.
$\Gamma \vdash \sigma \equiv \tau$	σ and τ are equal types in context Γ.
$\Gamma \vdash t\equiv u\mathbin {:} \sigma$	t and u are judgmentally equal terms of type σ in context Γ.
$\vdash \Gamma \ {\mathsf {Context}}$	Γ is a well-formed context of typing assumptions.

परंपरा के अनुसार, एक प्रकार है जो अन्य सभी प्रकारों का प्रतिनिधित्व करता है। यह कहा जाता है ${\mathcal {U}}$ (या $\operatorname {Set}$). तब से ${\mathcal {U}}$ एक प्रकार है, इसके सदस्य वस्तुएँ हैं। एक आश्रित प्रकार है $\operatorname {El}$ जो प्रत्येक वस्तु को उसके अनुरूप प्रकार से मैप करता है। अधिकांश ग्रंथों में $\operatorname {El}$ कभी नहीं लिखा है। बयान के संदर्भ से, एक पाठक लगभग हमेशा बता सकता है कि क्या $A$ एक प्रकार को संदर्भित करता है, या क्या यह वस्तु को संदर्भित करता है ${\mathcal {U}}$ जो प्रकार से मेल खाता है।

यह सिद्धांत का पूर्ण आधार है। बाकी सब कुछ व्युत्पन्न है।

तर्क को लागू करने के लिए, प्रत्येक प्रस्ताव को अपना प्रकार दिया जाता है। उन प्रकारों में वस्तुएं प्रस्ताव को साबित करने के विभिन्न संभावित तरीकों का प्रतिनिधित्व करती हैं। यदि तर्कवाक्य के लिए कोई प्रमाण नहीं है, तो प्रकार में कोई वस्तु नहीं है। ऑपरेटरों जैसे और और या जो प्रस्तावों पर काम करते हैं, नए प्रकार और नई वस्तुओं को पेश करते हैं। इसलिए $A\times B$ एक प्रकार है जो प्रकार पर निर्भर करता है $A$ और प्रकार $B$. उस आश्रित प्रकार की वस्तुओं को वस्तुओं की प्रत्येक जोड़ी के लिए अस्तित्व में परिभाषित किया गया है $A$ और $B$. यदि $A$ या $B$ कोई सबूत नहीं है और एक खाली प्रकार है, फिर नया प्रकार दर्शाता है $A\times B$ भी खाली है।

यह अन्य प्रकार (बूलियन, प्राकृतिक संख्या, आदि) और उनके ऑपरेटरों के लिए किया जा सकता है।

== टाइप थ्योरी == के श्रेणीबद्ध मॉडल श्रेणी सिद्धांत की भाषा का उपयोग करते हुए, R.A.G. सीली ने प्रकार सिद्धांत के मूल मॉडल के रूप में स्थानीय रूप से कार्टेशियन बंद श्रेणी (LCCC) की धारणा पेश की। कार्टमेल द्वारा पहले के काम के आधार पर इसे हॉफमैन और डायबजर द्वारा परिवारों के साथ श्रेणियों या विशेषताओं के साथ श्रेणियों में परिष्कृत किया गया है। परिवारों के साथ एक श्रेणी संदर्भों की श्रेणी सी है (जिसमें वस्तुएं संदर्भ हैं, और संदर्भ morphisms प्रतिस्थापन हैं), एक साथ एक functor T : C के साथ^op → परिवार (सेट)।

Fam(Set) समुच्चयों के परिवारों की श्रेणी है, जिसमें वस्तुएं जोड़े हैं $(A,B)$ एक इंडेक्स सेट A और एक फ़ंक्शन B: X → A, और morphisms फ़ंक्शन f : A → A' और g : X → X' के जोड़े हैं, जैसे कि B' _° जी = च _° B — दूसरे शब्दों में, एफ मानचित्र बी_aबी के लिए_g(a).

फ़ैक्टर टी एक संदर्भ जी को एक सेट असाइन करता है $Ty(G)$ प्रकार के, और प्रत्येक के लिए $A:Ty(G)$, एक सेट $Tm(G,A)$ शर्तों का। फ़नकार के लिए सिद्धांतों की आवश्यकता है कि ये प्रतिस्थापन के साथ सुसंगत रूप से खेलते हैं। प्रतिस्थापन आमतौर पर होता है एफ़ या एफ़ के रूप में लिखा गया है, जहां ए एक प्रकार है $Ty(G)$ और a एक पद है $Tm(G,A)$, और f एक प्रतिस्थापन है डी से जी यहाँ $Af:Ty(D)$ और $af:Tm(D,Af)$.

श्रेणी सी में एक टर्मिनल ऑब्जेक्ट (खाली संदर्भ) और फॉर्म के लिए एक अंतिम ऑब्जेक्ट होना चाहिए उत्पाद की समझ, या संदर्भ विस्तार कहा जाता है, जिसमें सही तत्व बाएं तत्व के संदर्भ में एक प्रकार है। यदि जी एक संदर्भ है, और $A:Ty(G)$, तो कोई वस्तु होनी चाहिए $(G,A)$ के बीच अंतिम मैपिंग पी के साथ संदर्भ डी: डी → जी, क्यू: टीएम (डी, एपी)।

एक तार्किक ढांचा, जैसे कि मार्टिन-लोफ का रूप लेता है प्रकार और शर्तों के संदर्भ निर्भर सेट पर बंद होने की स्थिति: कि एक प्रकार कहा जाना चाहिए सेट करें, और प्रत्येक सेट के लिए एक प्रकार, कि प्रकारों को आश्रित योग के रूपों के तहत बंद किया जाना चाहिए और उत्पाद, और आगे।

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

विस्तृत बनाम गहन

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

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

प्रकार के सिद्धांत का कार्यान्वयन

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

मार्टिन-लोफ प्रकार के सिद्धांत

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

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

MLTT72 को 1972 के प्रीप्रिंट में प्रस्तुत किया गया था जो अब प्रकाशित हो चुका है। उस सिद्धांत में एक ब्रह्मांड वी और कोई पहचान प्रकार नहीं था। ब्रह्माण्ड इस अर्थ में भविष्यवाणी था कि किसी वस्तु पर V से वस्तुओं के एक परिवार का आश्रित उत्पाद जो V में नहीं था, उदाहरण के लिए, V स्वयं, V में नहीं माना गया था। ब्रह्मांड एक ला रसेल का सिद्धांत था गणित, यानी, कोई अतिरिक्त कन्स्ट्रक्टर जैसे El के बिना सीधे T∈V और t∈T (मार्टिन-लोफ आधुनिक : ) के बजाय साइन ∈ का उपयोग करता है।

'एमएलटीटी73' एक प्रकार के सिद्धांत की पहली परिभाषा थी जिसे प्रति मार्टिन-लोफ ने प्रकाशित किया था (इसे लॉजिक कोलोक्वियम '73 में प्रस्तुत किया गया था और 1975 में प्रकाशित किया गया था।). ऐसे पहचान प्रकार हैं जिन्हें वह प्रस्ताव कहते हैं लेकिन चूंकि प्रस्तावों और बाकी प्रकारों के बीच कोई वास्तविक अंतर पेश नहीं किया गया है, इसका अर्थ स्पष्ट नहीं है। कुछ ऐसा है जो बाद में जे-एलिमिनेटर का नाम ले लेता है लेकिन फिर भी बिना नाम के (देखें पीपी। 94-95)। इस सिद्धांत में ब्रह्मांड V का एक अनंत क्रम है₀, ..., में_n, ... . ब्रह्माण्ड विधेयात्मक हैं, आ ला रसेल और गैर-संचयी हैं। वास्तव में, पृष्ठ पर परिणाम 3.10। 115 का कहना है कि अगर A∈V_m और बी∈वी_n ऐसे हैं कि ए और बी परिवर्तनीय हैं तो m = n। इसका मतलब है, उदाहरण के लिए, कि इस सिद्धांत में एकरूपता तैयार करना मुश्किल होगा- प्रत्येक वी में संविदात्मक प्रकार हैं_i लेकिन यह स्पष्ट नहीं है कि उन्हें समान कैसे घोषित किया जाए क्योंकि V को जोड़ने वाला कोई पहचान प्रकार नहीं है_i और वी_j मैं ≠ जे के लिए।

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

'बिब्लियोपोलिस': 1984 से बिब्लियोपोलिस पुस्तक में एक प्रकार के सिद्धांत की चर्चा है लेकिन यह कुछ हद तक खुला हुआ है और ऐसा लगता है कि यह विकल्पों के किसी विशेष सेट का प्रतिनिधित्व नहीं करता है और इसलिए इसके साथ कोई विशिष्ट प्रकार का सिद्धांत नहीं जुड़ा है।

यह भी देखें

• अंतर्ज्ञानवादी तर्क
• टाइप लैम्ब्डा कैलकुस

संदर्भ

• Martin-Löf, Per (1984). Intuitionistic type theory (PDF). Sambin, Giovanni. Napoli: Bibliopolis. ISBN 978-8870881059. OCLC 12731401.

आगे की पढाई

• Per Martin-Löf's Notes, as recorded by Giovanni Sambin (1980)
• Nordström, Bengt; Petersson, Kent; Smith, Jan M. (1990). Programming in Martin-Löf's Type Theory. Oxford University Press. ISBN 9780198538141.
• Thompson, Simon (1991). Type Theory and Functional Programming. Addison-Wesley. ISBN 0-201-41667-0.
• Granström, Johan G. (2011). Treatise on Intuitionistic Type Theory. Springer. ISBN 978-94-007-1735-0.

बाहरी कड़ियाँ

• EU Types Project: Tutorials – lecture notes and slides from the Types Summer School 2005
• n-Categories - Sketch of a Definition – letter from John Baez and James Dolan to Ross Street, November 29, 1995