लैम्ब्डा क्यूब

लैम्ब्डा क्यूब. प्रत्येक तीर की दिशा समावेशन की दिशा है।

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

• एक्स-अक्ष ($\rightarrow$): ऐसे प्रकार जो आश्रित प्रकारों के अनुरूप शब्दों को बांध सकते हैं।
• y-अक्ष ($\uparrow$): वे शब्द जो पैरामीट्रिक बहुरूपता के अनुरूप प्रकारों को बांध सकते हैं।
• z-अक्ष ($\nearrow$): ऐसे प्रकार जो (बाध्यकारी) प्रकार ऑपरेटरों के अनुरूप प्रकारों को बांध सकते हैं।

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

सिस्टम के उदाहरण

(λ→) बस लैम्ब्डा कैलकुलस टाइप किया गया

λ-क्यूब में पाई जाने वाली सबसे सरल प्रणाली सरल रूप से टाइप किया गया लैम्ब्डा कैलकुलस है, जिसे λ→ भी कहा जाता है। इस प्रणाली में, एक अमूर्तता का निर्माण करने का एकमात्र तरीका टाइपिंग नियम के साथ, एक शब्द को एक शब्द पर निर्भर बनाना है

${\frac {\Gamma ,x:\sigma \;\vdash \;t:\tau }{\Gamma \;\vdash \;\lambda x.t:\sigma \to \tau }}$

(λ2) सिस्टम एफ

सिस्टम एफ में (दूसरे क्रम में टाइप किए गए लैम्ब्डा कैलकुलस के लिए इसे λ2 भी कहा जाता है) एक अन्य प्रकार का अमूर्तन है, जिसे ए के साथ लिखा जाता है $\Lambda$, जो निम्नलिखित नियम के साथ शब्दों को प्रकारों पर निर्भर करने की अनुमति देता है:

${\frac {\Gamma \;\vdash \;t:\sigma }{\Gamma \;\vdash \;\Lambda \alpha .t:\Pi \alpha .\sigma }}\;{\text{ if }}\alpha {\text{ does not occur free in }}\Gamma$

ए से शुरू होने वाले शब्द $\Lambda$ इन्हें पैरामीट्रिक बहुरूपता कहा जाता है, क्योंकि इन्हें विभिन्न कार्यों को प्राप्त करने के लिए विभिन्न प्रकारों पर लागू किया जा सकता है, एमएल (प्रोग्रामिंग भाषा) | एमएल जैसी भाषाओं में बहुरूपी कार्यों के समान। उदाहरण के लिए, बहुरूपी पहचान

fun x -> x

OCaml का प्रकार है

'a -> 'a

मतलब यह किसी भी प्रकार का तर्क ले सकता है 'a और उस प्रकार का एक तत्व लौटाएँ। यह प्रकार λ2 में प्रकार से मेल खाता है $\Pi \alpha .\alpha \to \alpha$.

(λω) सिस्टम Fω

सिस्टम एफ में${\underline {\omega }}$ एक निर्माण को आपूर्ति प्रकारों के लिए पेश किया जाता है जो अन्य प्रकारों पर निर्भर होते हैं। इसे कंस्ट्रक्टर टाइप करें कहा जाता है और वैल्यू प्रकार के साथ फ़ंक्शन बनाने का एक तरीका प्रदान करता है। इस प्रकार के कंस्ट्रक्टर का एक उदाहरण बाइनरी पेड़ों का प्रकार है जिसमें किसी दिए गए प्रकार के डेटा द्वारा लेबल किए गए पत्ते होते हैं $A$: ${\mathsf {TREE}}:=\lambda A:*.\Pi B.(A\to B)\to (B\to B\to B)\to B$, कहाँ$A:*$अनौपचारिक रूप से मतलब है$A$ एक प्रकार है. यह एक फ़ंक्शन है जो एक प्रकार का पैरामीटर लेता है $A$ एक तर्क के रूप में और का प्रकार लौटाता है ${\mathsf {TREE}}$प्रकार के मानों का s $A$. In concrete programming, this feature corresponds to the ability to define type constructors inside the language, rather than considering them as primitives. The previous type constructor roughly corresponds to the following definition of a tree with labeled leaves in OCaml:

type 'a tree = | Leaf of 'a | Node of 'a tree * 'a tree

नए प्रकार प्राप्त करने के लिए इस प्रकार के कंस्ट्रक्टर को अन्य प्रकारों पर लागू किया जा सकता है। उदाहरण के लिए, पूर्णांकों के वृक्षों के प्रकार प्राप्त करने के लिए:

type int_tree = int tree

सिस्टम एफ${\underline {\omega }}$ आम तौर पर इसका उपयोग अपने आप नहीं किया जाता है, लेकिन यह टाइप कंस्ट्रक्टर की स्वतंत्र सुविधा को अलग करने के लिए उपयोगी है।

(λP) लैम्ब्डा-पी

ΛΠ-कैलकुलस|λP प्रणाली में, जिसे ΛΠ भी कहा जाता है, और लॉजिकल फ्रेमवर्क#LF से निकटता से संबंधित है, एक तथाकथित आश्रित प्रकार है। ये ऐसे प्रकार हैं जिन्हें शर्तों पर निर्भर रहने की अनुमति है। सिस्टम का महत्वपूर्ण परिचय नियम है

${\frac {\Gamma ,x:A\;\vdash \;B:*}{\Gamma \;\vdash \;(\Pi x:A.B):*}}$ कहाँ $*$ वैध प्रकार का प्रतिनिधित्व करता है। नए प्रकार का कंस्ट्रक्टर $\Pi$ करी हावर्ड समरूपता के माध्यम से एक सार्वभौमिक क्वांटिफायर से मेल खाता है, और सिस्टम λP समग्र रूप से केवल संयोजी के रूप में निहितार्थ के साथ प्रथम-क्रम तर्क से मेल खाता है। ठोस प्रोग्रामिंग में इन आश्रित प्रकारों का एक उदाहरण एक निश्चित लंबाई पर वैक्टर का प्रकार है: लंबाई एक शब्द है, जिस पर प्रकार निर्भर करता है।

(Fω) सिस्टम Fω

सिस्टम एफ-ओमेगा|सिस्टम एफω दोनों को जोड़ता है $\Lambda$ सिस्टम F का कंस्ट्रक्टर और सिस्टम F से टाइप कंस्ट्रक्टर${\underline {\omega }}$. इस प्रकार सिस्टम Fω दोनों शब्द प्रदान करता है जो प्रकारों पर निर्भर करते हैं और प्रकार जो प्रकारों पर निर्भर करते हैं।

(λC) निर्माणों की गणना

निर्माणों की गणना में, घन में λC के रूप में या λPω के रूप में दर्शाया गया है, ये चार विशेषताएं सहवास करती हैं, जिससे प्रकार और पद दोनों प्रकार और पद पर निर्भर हो सकते हैं। शब्दों और प्रकारों के बीच λ→ में मौजूद स्पष्ट सीमा को कुछ हद तक समाप्त कर दिया गया है, क्योंकि सार्वभौमिक को छोड़कर सभी प्रकार $\square$ स्वयं एक प्रकार के पद हैं।

औपचारिक परिभाषा

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

प्रकार के सेट को इस प्रकार परिभाषित किया गया है $S:=\{*,\square \}$, प्रकार को अक्षर से दर्शाया जाता है $s$. एक सेट भी है $V$ चरों का, अक्षरों द्वारा दर्शाया गया $x,y,\dots$. घन की आठ प्रणालियों के मूल शब्द निम्नलिखित वाक्यविन्यास द्वारा दिए गए हैं:

$A:=x\mid s\mid A~A\mid \lambda x:A.A\mid \Pi x:A.A$ और $A\to B$ दर्शाने $\Pi x:A.B$ कब $x$ में मुक्त नहीं होता है $B$.

पर्यावरण, जैसा कि आमतौर पर टाइप की गई प्रणालियों में होता है, द्वारा दिया जाता है $\Gamma :=\emptyset \mid \Gamma ,x:T$ क्यूब में सभी प्रणालियों के लिए β-कमी की धारणा आम है। यह लिखा है $\to _{\beta }$ और नियमानुसार दिया गया है

$${\frac {}{(\lambda x:A.B)~C\to _{\beta }B[C/x]}}$$

$${\frac {B\to _{\beta }B'}{\lambda x:A.B\to _{\beta }\lambda x:A.B'}}$$

$${\frac {A\to _{\beta }A'}{\lambda x:A.B\to _{\beta }\lambda x:A'.B}}$$

$${\frac {B\to _{\beta }B'}{\Pi x:A.B\to _{\beta }\Pi x:A.B'}}$$

$${\frac {A\to _{\beta }A'}{\Pi x:A.B\to _{\beta }\Pi x:A'.B}}$$

इसका रिफ्लेक्सिव ट्रांजिटिव क्लोजर|रिफ्लेक्सिव, ट्रांजिटिव क्लोजर लिखा है $=_{\beta }$.

निम्नलिखित टाइपिंग नियम भी क्यूब की सभी प्रणालियों के लिए सामान्य हैं:

$${\frac {}{\vdash *:\square }}\quad {\text{(Axiom)}}$$

$${\frac {\Gamma \vdash A:s\quad x{\text{ does not occur in }}\Gamma }{\Gamma ,x:A\vdash x:A}}\quad {\text{(Start)}}$$

$${\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s}{\Gamma ,x:C\vdash A:B}}\quad {\text{(Weakening)}}$$

$${\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash a:A}{\Gamma \vdash Ca:B[a/x]}}\quad {\text{(Application)}}$$

$${\frac {\Gamma \vdash A:B\quad B=_{\beta }B'\quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(Conversion)}}$$

प्रणालियों के बीच अंतर प्रकार के जोड़े में है ${\textstyle (s_{1},s_{2})}$ निम्नलिखित दो टाइपिंग नियमों में इसकी अनुमति है:

$${\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}}{\Gamma \vdash \Pi x:A.B:s_{2}}}\quad {\text{(Product)}}$$

${\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash b:B\quad \Gamma ,x:A\vdash B:s_{2}}{\Gamma \vdash \lambda x:A.b:\Pi x:A.B}}\quad {\text{(Abstraction)}}$ सिस्टम और जोड़ियों के बीच पत्राचार ${\textstyle (s_{1},s_{2})}$ नियमों में निम्नलिखित की अनुमति है:

$(s_{1},s_{2})$	$(*,*)$	$(*,\square )$	$(\square ,*)$	$(\square ,\square )$
λ→
λP
λ2
λω
λP2
λPω
λω
λC

घन की प्रत्येक दिशा एक जोड़ी (जोड़ी को छोड़कर) से मेल खाती है ${\textstyle (*,*)}$ सभी प्रणालियों द्वारा साझा किया जाता है), और बदले में प्रत्येक जोड़ी शब्दों और प्रकारों के बीच निर्भरता की एक संभावना से मेल खाती है:

• ${\textstyle (*,*)}$ शर्तों को शर्तों पर निर्भर रहने की अनुमति देता है।
• ${\textstyle (*,\square )}$ प्रकारों को शर्तों पर निर्भर करने की अनुमति देता है।
• ${\textstyle (\square ,*)}$ शर्तों को प्रकारों पर निर्भर करने की अनुमति देता है।
• ${\textstyle (\square ,\square )}$ प्रकारों को प्रकारों पर निर्भर रहने की अनुमति देता है।

प्रणालियों के बीच तुलना

λ→

एक विशिष्ट व्युत्पत्ति जो प्राप्त की जा सकती है वह है

$$\alpha :*\vdash \lambda x:\alpha .x:\Pi x:\alpha .\alpha$$

या तीर शॉर्टकट के साथ

$$\alpha :*\vdash \lambda x:\alpha .x:\alpha \to \alpha$$

पहचान से काफी मिलता-जुलता (प्रकार का)। ${\textstyle \alpha }$) सामान्य λ→ का। ध्यान दें कि उपयोग किए गए सभी प्रकार संदर्भ में दिखाई देने चाहिए, क्योंकि एकमात्र व्युत्पत्ति जो खाली संदर्भ में की जा सकती है ${\textstyle \vdash *:\square }$.

कंप्यूटिंग शक्ति काफी कमजोर है, यह विस्तारित बहुपद (एक सशर्त ऑपरेटर के साथ बहुपद) से मेल खाती है।

λ2

λ2 में, ऐसे पद प्राप्त किए जा सकते हैं

$$\vdash (\lambda \beta :*.\lambda x:\bot .x\beta ):\Pi \beta :*.\bot \to \beta$$

साथ ${\textstyle \bot =\Pi \alpha :*.\alpha }$. अगर कोई पढ़ता है ${\textstyle \Pi }$ एक सार्वभौमिक परिमाणीकरण के रूप में, करी-हावर्ड समरूपता के माध्यम से, इसे विस्फोट के सिद्धांत के प्रमाण के रूप में देखा जा सकता है। सामान्य तौर पर, λ2 में असंभाव्यता प्रकार जैसे होने की संभावना जुड़ती है ${\textstyle \bot }$, यह स्वयं सहित सभी प्रकारों पर मात्रा निर्धारित करने वाला शब्द है।
बहुरूपता उन कार्यों के निर्माण की भी अनुमति देती है जो λ→ में निर्माण योग्य नहीं थे। अधिक सटीक रूप से, λ2 में परिभाषित कार्य दूसरे क्रम के पीनो अंकगणित में सिद्ध रूप से कुल हैं। विशेष रूप से, सभी आदिम पुनरावर्ती कार्य निश्चित हैं।

λP

λP में, शब्दों के आधार पर प्रकार रखने की क्षमता का मतलब है कि कोई तार्किक विधेय व्यक्त कर सकता है। उदाहरण के लिए, निम्नलिखित व्युत्पन्न है:

$$\alpha :*,a_{0}:\alpha ,p:\alpha \to *,q:*\vdash \lambda z:(\Pi x:\alpha .px\to q).\lambda y:(\Pi x:\alpha .px).(za_{0})(ya_{0}):(\Pi x:\alpha .px\to q)\to (\Pi x:\alpha .px)\to q$$

जो, करी-हावर्ड समरूपता के माध्यम से, के प्रमाण से मेल खाता है $(\forall x:A,Px\to Q)\to (\forall x:A,Px)\to Q$.
कम्प्यूटेशनल दृष्टिकोण से, हालांकि, आश्रित प्रकार होने से कम्प्यूटेशनल शक्ति में वृद्धि नहीं होती है, केवल अधिक सटीक प्रकार के गुणों को व्यक्त करने की संभावना होती है। आश्रित प्रकारों से निपटने के दौरान रूपांतरण नियम की अत्यधिक आवश्यकता होती है, क्योंकि यह प्रकार की शर्तों पर गणना करने की अनुमति देता है। उदाहरण के लिए, यदि आपके पास है $\Gamma \vdash A:P((\lambda x.x)y)$ और $\Gamma \vdash B:\Pi x:P(y).C$, प्राप्त करने के लिए आपको रूपांतरण नियम लागू करना होगा $\Gamma \vdash A:P(y)$ टाइप करने में सक्षम होने के लिए $\Gamma \vdash BA:C$.

एल

एलō में, निम्नलिखित ऑपरेटर

$$AND:=\lambda \alpha :*.\lambda \beta :*.\Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma$$

निश्चित है, अर्थात् $\vdash AND:*\to *\to *$. व्युत्पत्ति

$$\alpha :*,\beta :*\vdash \Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma :*$$

पहले से ही λ2 में प्राप्त किया जा सकता है, हालाँकि बहुरूपी ${\textstyle AND}$ केवल तभी परिभाषित किया जा सकता है जब नियम ${\textstyle (\square ,*)}$ भी मौजूद है.

कंप्यूटिंग के दृष्टिकोण से, λω बेहद मजबूत है, और इसे प्रोग्रामिंग भाषाओं के लिए आधार माना गया है।

λC

निर्माणों की गणना में λP की विधेय अभिव्यंजना और λω की कम्प्यूटेशनल शक्ति दोनों हैं, इसलिए λC को λPω भी कहा जाता है, इसलिए यह तार्किक पक्ष और कम्प्यूटेशनल पक्ष दोनों पर बहुत शक्तिशाली है।

अन्य प्रणालियों से संबंध

सिस्टम स्वचालित तार्किक दृष्टिकोण से λ2 के समान है। एमएल (प्रोग्रामिंग भाषा)|एमएल जैसी भाषाएं, टाइपिंग के दृष्टिकोण से, λ→ और λ2 के बीच कहीं स्थित होती हैं, क्योंकि वे एक प्रतिबंधित प्रकार के बहुरूपी प्रकारों को स्वीकार करते हैं, जो कि प्रीनेक्स सामान्य रूप में प्रकार हैं। हालाँकि, क्योंकि उनमें कुछ रिकर्सन ऑपरेटर होते हैं, उनकी कंप्यूटिंग शक्ति λ2 से अधिक होती है।Coq प्रणाली केवल एक अप्राप्य के बजाय ब्रह्मांडों के एक रैखिक पदानुक्रम के साथ λC के विस्तार पर आधारित है ${\textstyle \square }$, और आगमनात्मक प्रकार के निर्माण की क्षमता।

शुद्ध प्रकार की प्रणालियों को घन के सामान्यीकरण के रूप में देखा जा सकता है, जिसमें प्रकार, स्वयंसिद्ध, उत्पाद और अमूर्त नियमों का एक मनमाना सेट होता है। इसके विपरीत, लैम्ब्डा क्यूब के सिस्टम को दो प्रकार के शुद्ध प्रकार के सिस्टम के रूप में व्यक्त किया जा सकता है $\{*,\square \}$, एकमात्र स्वयंसिद्ध ${\textstyle \{*,\square \}}$, और नियमों का एक सेट ${\textstyle R}$ ऐसा है कि $\{(*,*,*)\}\subseteq R\subseteq \{(*,*,*),(*,\square ,\square ),(\square ,*,*),(\square ,\square ,\square )\}$.

करी-हावर्ड समरूपता के माध्यम से, लैम्ब्डा क्यूब और तार्किक प्रणालियों में सिस्टम के बीच एक-से-एक पत्राचार होता है,अर्थात्:

System of the cube	Logical System
λ→	(First-order) Propositional Calculus
λ2	Second-order Propositional Calculus
λω	Weakly Higher Order Propositional Calculus
λω	Higher Order Propositional Calculus
λP	(First order) Predicate Logic
λP2	Second-order Predicate Calculus
λPω	Weak Higher Order Predicate Calculus
λC	Calculus of Constructions

सभी तर्क एक निहितार्थ हैं (अर्थात केवल संयोजक हैं ${\textstyle \to }$ और ${\textstyle \forall }$), हालाँकि कोई अन्य संयोजकों को परिभाषित कर सकता है जैसे कि $\wedge$ या $\neg$ दूसरे और उच्च क्रम के तर्कों में एक अव्यवहारिक तरीके से। कमजोर उच्च क्रम तर्कशास्त्र में, उच्च क्रम विधेय के लिए चर होते हैं, लेकिन उन पर कोई परिमाणीकरण नहीं किया जा सकता है।

सामान्य गुण

क्यूब के सभी सिस्टम आनंद लेते हैं

• चर्च-रोसेर संपत्ति: यदि $M\to _{\beta }N$ और $M\to _{\beta }N'$ तो वहाँ अस्तित्व है $N''$ ऐसा है कि $N\to _{\beta }^{*}N''$ और $N'\to _{\beta }^{*}N''$;
• विषय में कमी: यदि $\Gamma \vdash M:T$ और $M\to _{\beta }M'$ तब $\Gamma \vdash M':T$;
• प्रकारों की विशिष्टता: यदि $\Gamma \vdash A:B$ और $\Gamma \vdash A:B'$ तब $B=_{\beta }B'$.

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

उपप्रकार

हालाँकि, सबटाइपिंग को क्यूब में प्रदर्शित नहीं किया जाता है, भले ही सिस्टम पसंद करता हो $F_{<:}^{\omega }$, जिसे उच्च-क्रम सीमाबद्ध परिमाणीकरण के रूप में जाना जाता है, जो उपप्रकार और बहुरूपता को जोड़ता है, व्यावहारिक रुचि का है, और इसे आगे बंधे हुए प्रकार के ऑपरेटरों के लिए सामान्यीकृत किया जा सकता है। आगे विस्तार $F_{<:}^{\omega }$ विशुद्ध रूप से कार्यात्मक वस्तुओं की परिभाषा की अनुमति दें; ये सिस्टम आम तौर पर लैम्ब्डा क्यूब पेपर प्रकाशित होने के बाद विकसित किए गए थे। क्यूब का विचार गणितज्ञ हेन्क बेरेन्ड्रेट (1991) की देन है। शुद्ध प्रकार की प्रणालियों का ढांचा लैम्ब्डा क्यूब को इस अर्थ में सामान्यीकृत करता है कि क्यूब के सभी कोनों, साथ ही कई अन्य प्रणालियों को इस सामान्य ढांचे के उदाहरण के रूप में दर्शाया जा सकता है। यह ढांचा लैम्ब्डा क्यूब से कुछ साल पहले का है। अपने 1991 के पेपर में, बेरेन्ड्रेट ने इस ढांचे में घन के कोनों को भी परिभाषित किया है।

यह भी देखें

• अनुसंधान को निर्देशित करने की उनकी क्षमता में, ओलिवियर रिडौक्स लैम्ब्डा क्यूब का एक कट-आउट टेम्प्लेट देता है और क्यूब का एक ऑक्टाहेड्रोन के रूप में दोहरा प्रतिनिधित्व भी देता है, जहां 8 शीर्षों को चेहरों द्वारा प्रतिस्थापित किया जाता है, साथ ही डोडेकाहेड्रोन के रूप में एक दोहरा प्रतिनिधित्व दिया जाता है, जहां 12 किनारों को बदल दिया जाता है। चेहरे के।
• होमोटोपी प्रकार सिद्धांत

अग्रिम पठन

• Peyton Jones, Simon; Meijer, Erik (1997). "Henk: A Typed Intermediate Language" (PDF). Microsoft. Henk is based directly on the lambda cube, an expressive family of typed lambda calculi.

बाहरी संबंध

• Barendregt's Lambda Cube in the context of pure type systems by Roger Bishop Jones