💻 computer science

A unification of graded and substructural logics

यह शोध पत्र GRASS प्रस्तुत करता है, जो एक एकीकृत प्रकार प्रणाली (unified type system) है जो सब्स्ट्रक्चरल लॉजिक के रिसोर्स रिस्ट्रिक्शन तंत्र को ग्रेडेड सिस्टम्स की क्वांटिटेटिव ट्रैकिंग के साथ एकीकृत करता है, जिससे एक ही ढांचे के भीतर वेरिएबल यूसेज पर लचीला, हेटेरोजेनियस नियंत्रण सक्षम होता है और अपने कैटेगोरिकल सेमैंटिक्स के माध्यम से LNL, एडजॉइंट लॉजिक और mGL जैसे स्थापित मॉडलों को समाहित करता है।

मूल लेखक: Peter Hanukaev, Harley Eades III

प्रकाशित 2026-05-19

📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Peter Hanukaev, Harley Eades III

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप एक व्यस्त रसोई का संचालन करने वाले शेफ हैं। एक पारंपरिक रसोई (मानक प्रोग्रामिंग) में, यदि आपको एक अंडे की आवश्यकता है, तो आप एक उठा सकते हैं, उसका उपयोग कर सकते हैं, और फिर बिना इस बात की चिंता किए उसी कार्टन से दूसरा अंडा उठा सकते हैं कि कितने बचे हैं। आप एक अंडा फेंक भी सकते हैं यदि आपको उसकी आवश्यकता नहीं है। यह चरों (variables) को "प्रस्तावों" (propositions) के रूप में मानने जैसा है जिन्हें स्वतंत्र रूप से पुन: उपयोग या त्याग किया जा सकता है।

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

यहाँ यह पेपर इसे सरल उपमाओं का उपयोग करके कैसे तोड़ता है, दिया गया है:

1. सामग्रियों को प्रबंधित करने के दो पुराने तरीके

Grass से पहले, शेफ सामग्रियों को प्रबंधित करने के दो मुख्य तरीकों का उपयोग करते थे:

"कठोर नियम" दृष्टिकोण (Substructural Logics): कल्पना करें कि एक रसोई है जहाँ नियम बहुत सख्त हैं। आपको किसी सामग्री का दो बार उपयोग करने या उसे फेंकने से मनाही है, जब तक कि आपके पास एक विशेष "जादुई पास" (एक मोडैलिटी) न हो। यह बर्बादी को रोकने के लिए बहुत अच्छा है, लेकिन यह उन चीजों के लिए कठिन है जिन्हें पुन: उपयोग योग्य होना चाहिए, जैसे कि नमक का डिब्बा।
"स्कोरकार्ड" दृष्टिकोण (Graded Systems): कल्पना करें कि एक रसोई है जहाँ आप सामग्रियों का स्वतंत्र रूप से उपयोग कर सकते हैं, लेकिन हर बार जब आप कुछ उठाते हैं, तो आपको एक स्कोरकार्ड पर एक संख्या लिखनी पड़ती है। यदि आप "1" उठाते हैं, तो आपने इसका एक बार उपयोग किया। यदि आप "2" उठाते हैं, तो आपने इसका दो बार उपयोग किया। यह लचीला है, लेकिन यह हर चीज़ के साथ एक संख्या की तरह व्यवहार करता है, जो उन चीजों के लिए बहुत कठोर हो सकता है जिन्हें सख्त "पुन: उपयोग न करें" नियमों की आवश्यकता होती है।

2. नया समाधान: Grass

लेखकों ने Grass बनाया है (Graded and Substructural)। Grass को एक सार्वभौमिक किचन मैनेजर के रूप में समझें जो दोनों दुनियाओं के सर्वश्रेष्ठ गुणों को जोड़ता है।

यह एक हाइब्रिड है: Grass आपको ऐसी सामग्रियां रखने की अनुमति देता है जो सख्त "पुन: उपयोग न करें" नियमों का पालन करती हैं (जैसे लीनियर लॉजिक) और अन्य जो लचीले "स्कीकार्ड" नियमों का पालन करती हैं (जैसे एक ग्रेडेड सिस्टम), और यह सब एक ही रेसिपी में।
"मोड्स" (Modes) की अवधारणा: यही इस पेपर का बड़ा नवाचार है। कल्पना करें कि रसोई में अलग-अलग "ज़ोन" या मोड्स हैं।
- ज़ोन A (सख्त): इस ज़ोन में, आप सामग्रियों का पुन: उपयोग नहीं कर सकते।
- ज़ोन B (लचीला): इस ज़ोन में, आप सामग्रियों का पुन: उपयोग कर सकते हैं, लेकिन आपको यह ट्रैक करना होगा कि कितनी बार।
- ज़ोन C (सुरक्षित): इस ज़ोन में, आप सुरक्षा मंजूरी स्तरों को ट्रैक कर सकते हैं।
Grass आपको इन ज़ोनों के बीच सामग्रियों को ले जाने की अनुमति देता है। आप "सुरक्षित ज़ोन" से एक "सुरक्षित कुंजी" ले सकते हैं और उसका उपयोग "लचीले ज़ोन" में एक फ़ाइल को अनलॉक करने के लिए कर सकते हैं, लेकिन सिस्टम यह सुनिश्चित करता है कि कुंजी को दोनों ज़ोनों के नियमों के अनुसार सही ढंग से संभाला जाए।

3. यह उपयोग को कैसे नियंत्रित करता है ( "आइडियल" की अवधारणा)

पेपर सामग्रियों को कैसे संयोजित किया जा सकता है, इसे नियंत्रित करने के लिए एक गणितीय अवधारणा "आइडियल" (Ideal) पेश करता है।

उपमा: एक "कॉन्ट्रैक्टेबल" वस्तुओं (ऐसी चीजें जिन्हें आप मिला सकते हैं) के बाल्टी की कल्पना करें। यदि आपके पास दो "1s" (प्रत्येक एक उपयोग) हैं, तो क्या आप उन्हें एक "2" (दो उपयोग) में मिला सकते हैं?
- कुछ ज़ोन में, हाँ: आप दो एकल-उपयोग वाली वस्तुओं को एक दोहरे-उपयोग वाली वस्तु में मिला सकते हैं।
- अन्य ज़ोन में, नहीं: आप दो एकल-उपयोग वाली वस्तुओं को नहीं मिला सकते। यदि आप एक फ़ाइल हैंडल को दो बार उपयोग करने का प्रयास करते हैं, तो सिस्टम आपको रोक देगा क्योंकि इस विशिष्ट ज़ोन में दो "1s" मिलकर "2" नहीं बन सकते।

यह खतरनाक त्रुटियों को रोकता है, जैसे कि दो अलग-अलग फ़ाइल हैंडल को एक विशाल हैंडल के रूप में उपयोग करने का प्रयास करना जिसे दो बार उपयोग किया जा सके।

4. "अनुवाद" प्रणाली

यह पेपर विभिन्न ज़ोनों के बीच मॉर्फिज्म (morphisms) (अनुवाद कार्यों) का उपयोग करके कैसे आगे बढ़ना है, इसका वर्णन करता है।

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

5. गणितीय "ब्लूप्रिंट" (कैटेगोरिकल सेमैंटिक्स)

अंत में, लेखकों ने यह सिद्ध करने के लिए कि उनका सिस्टम काम करता है, एक गणितीय "ब्लूप्रिंट" (कैटेगोरिकल सेमैंटिक्स) बनाया है।

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

सारांश

संक्षेप में, यह पेपर Grass प्रस्तुत करता है, जो कोड लिखने का एक नया तरीका है जो चरों को भौतिक संसाधनों की तरह मानता है। यह प्रोग्रामर को एक ही प्रोग्राम के भीतर विभिन्न चरों के लिए अलग-अलग नियमों को मिलाने की अनुमति देता है।

यह नियमों के सेट (सख्त बनाम लचीला) को परिभाषित करने के लिए मोड्स (Modes) का उपयोग करता है।
यह तय करने के लिए कि संसाधनों को कब मिलाया या विभाजित किया जा सकता है, आइडियल्स (Ideals) का उपयोग करता है।
यह सुनिश्चित करने के लिए कि विभिन्न नियम सेटों के बीच जाना कभी भी प्रोग्राम को क्रैश नहीं करेगा या गलत व्यवहार नहीं करेगा, गणितीय प्रमाणों (Mathematical Proofs) का उपयोग करता है।

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

तकनीकी सारांश: ग्रेडेड और सबस्ट्रक्चरल लॉजिक्स का एकीकरण (Grass)

समस्या विवरण

प्रोग्राम वेरिएबल्स को संसाधनों के रूप में मानना मेमोरी सेफ्टी और सूचना प्रवाह (information flow) जैसे शुद्धता गुणों को सत्यापित करने के लिए केंद्रीय हो गया है। दो अलग-अलग दृष्टिकोण साहित्य में हावी हैं:

सबस्ट्रक्चरल लॉजिक्स (Substructural Logics): सिस्टम जैसे कि लीनियर लॉजिक डिफ़ॉल्ट रूप से स्ट्रक्चरल नियमों (वीकनिंग और कॉन्ट्रैक्शन) को प्रतिबंधित करते हैं, और मोडैलिटीज़ (जैसे कि "ऑफ-कोर्स" मोडैलिटी $!$ ) के माध्यम से उन्हें चुनिंदा रूप से पुन: पेश करते हैं। हालांकि ये शक्तिशाली हैं, लेकिन ये जटिल एडजंक्शनों (adjunctions) के बिना विभिन्न स्ट्रक्चरल नियमों वाले विभिन्न लॉजिक्स को एक ही फ्रेमवर्क के भीतर संयोजित करने में संघर्ष करते हैं।
ग्रेडेड सिस्टम्स (Graded Systems): ये सिस्टम स्ट्रक्चरल नियमों की अनुमति डिफ़ॉल्ट रूप से देते हैं लेकिन धारणाओं (assumptions) को "ग्रेड्स" के साथ एनोटेट करते हैं जो एक बीजगणितीय संरचना (आमतौर पर एक सेमीरिंग) से प्राप्त होते हैं। ग्रेड्स संसाधन उपयोग को मात्रात्मक रूप से ट्रैक करते हैं (जैसे कि कॉन्ट्रैक्शन के लिए जोड़ और वीकनिंग के लिए शून्य तत्व)। हालांकि ये लचीले हैं, मानक ग्रेडेड सिस्टम आमतौर पर एक एकल ग्रेड बीजगणक (algebra) मानते हैं और विशिष्ट वेरिएबल्स को कॉन्ट्रैक्ट या वीकन किया जा सकता है, यह नियंत्रित करने में सक्षम नहीं हो सकते हैं, क्योंकि वे अक्सर सभी वेरिएबल्स को एक ही बीजगणितीय शासन के तहत समान रूप से देखते हैं।

मुख्य समस्या एक ऐसे एकीकृत टाइप सिस्टम की कमी है जो एक साथ निम्नलिखित का समर्थन कर सके:

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

कार्यप्रणाली (Methodology)

लेखक Grass (ग्रेडेड और सबस्ट्रक्चरल) प्रस्तुत करते हैं, जो निम्नलिखित तंत्रों के माध्यम से इन दृष्टिकोणों को एकीकृत करता है:

1. मोड्स और ग्रेड बीजगणक (Modes and Grade Algebras)

Grass मोड्स के एक संग्रह द्वारा पैरामीटराइज्ड है। प्रत्येक मोड $m$ एक ट्रिपल $(R_m, \text{Cont}(m), \text{Weak}(m))$ है, जहाँ:

$R_m$ एक ग्रेड बीजगणक (एक प्रीऑर्डर्ड सेमीरिंग) है।
$\text{Cont}(m) \subseteq R_m$ उस सेमीरिंग के भीतर एक आइडियल (ideal) है। यह आइडियल उन ग्रेड्स के सेट को परिभाषित करता है जो परस्पर कॉन्ट्रैक्ट करने योग्य (mutually contractible) हैं।
$\text{Weak}(m) \in \{\text{true}, \text{false}\}$ एक बूलियन फ्लैग है जो यह दर्शाता है कि वीकनिंग की अनुमति है या नहीं।

यह संरचना सूक्ष्म नियंत्रण प्रदान करती है: कॉन्ट्रैक्शन एक वैश्विक नियम नहीं है बल्कि मोड के विशिष्ट आइडियल तक सीमित है। वीकनिंग भी इसी तरह नियंत्रित है, लेकिन लेखक नोट करते हैं कि वीकनिंग को सक्षम करने से अप्रयुक्त वेरिएबल्स को किसी भी ग्रेड $q \geq 0$ पर पेश करने की अनुमति मिलती है।

2. सिंटैक्स और टाइपिंग नियम

सिंटैक्स मानक ग्रेडेड मोडल टाइप्स को निम्नलिखित के साथ विस्तारित करता है:

हेटरोजीनियस कॉन्टेक्स्ट्स (Heterogeneous Contexts): एक टाइपिंग जजमेंट $\rho \mid M \odot \Gamma \vdash_m t : T$ एक ग्रेड वेक्टर $\rho$ और एक मोड वेक्टर $M$ शामिल करता है। कॉन्टेक्स्ट $\Gamma$ में वेरिएबल्स अलग-अलग मोड्स के हो सकते हैं, बशर्ते कि वर्तमान मोड $m$ के स्ट्रक्चरल नियमों का पालन किया जाए।
मोड शिफ्टिंग के लिए मोडैलिटीज़:
- ड्रॉप ( $\downarrow^q_{n \leq m}$ ): एक टर्म को मोड $m$ से एक "सख्त" (stricter) मोड $n$ (जहाँ $n \leq m$ ) में प्रमोट करता है, जो एक विशिष्ट उपयोग ग्रेड $q$ को लागू करता है। यह ग्रेडेड मोडैलिटी $\Box_q A$ का सामान्यीकरण है।
- रेज़ ( $\uparrow^{m \leq n}$ ): एक टर्म को सख्त मोड $n$ से अधिक उदार मोड $m$ में ऊपर उठाता है।
स्ट्रक्चरल नियम:
- कॉन्ट्रैक्शन: केवल तभी अनुमत है जब वेरिएबल्स के ग्रेड्स कॉन्ट्रैक्शन के लिए निर्धारित आइडियल $\text{Cont}(m)$ के तत्व हों।
- वीकनिंग: केवल तभी अनुमत है जब $\text{Weak}(m)$ सत्य (true) हो।
- सबस्टीट्यूशन: विभिन्न मोड्स और ग्रेड मल्टीप्लिकेशन के बीच इंटरैक्शन को संभालने के लिए परिभाषित किया गया है, यह सुनिश्चित करते हुए कि "स्वतंत्रता" (independence) गुण बना रहे (अर्थात, सख्त मोड्स के टर्म लूज़ मोड्स के वेरिएबल्स पर निर्भर नहीं हो सकते)।

3. कैटेगोरिकल सेमेंटिक्स

लेखक ग्रेडेड लीनियर एक्सपोनेंशियल कोमोनैड्स पर आधारित एक कैटेगोरिकल सेमेंटिक्स विकसित करते हैं।

एक्सपोनेंशियल एक्शन्स: प्रत्येक मोड $m$ के लिए, सेमेंटिक्स एक सिमेट्रिक मोनॉइडल क्लोज्ड कैटेगरी (SMCC) पर एक एक्सपोनेंशियल एक्शन को परिभाषित करता है। इसमें एक फन्क्टर $D: R_m^{op} \to \text{SMC}(C, C)$ शामिल है जो कॉन्ट्रैक्शन ( $c$ ) और वीकनिंग ( $w$ ) के लिए नेचुरल ट्रांसफॉर्मेशन के साथ सुसज्जित है और कोहेरेंस कंडीशंस को पूरा करता है।
एक्शन्स के मॉर्फिज्म: विभिन्न मोड्स को जोड़ने के लिए, लेखक एक्सपोनेंशियल एक्शन्स के बीच मॉर्फिज्म की एक नई अवधारणा पेश करते हैं। ये सिमेट्रिक लैक्स मोनॉइडल एडजंक्शन $F \dashv G$ हैं जो एक "लाइनिएटर" (lineator) नेचुरल ट्रांसफॉर्मेशन $\ell$ से लैस हैं। यह संरचना सिंटैक्टिक मोडैलिटी $\downarrow$ और $\uparrow$ को दर्शाती है।
मॉडेल्स: सेमेंटिक्स दिखाता है कि इंट्यूशनिस्टिक, लीनियर, रेलिवेंट और एफाइन लॉज के ज्ञात मॉडल्स को Grass मोड्स के विशिष्ट इंस्टेंशिएशन के रूप में प्राप्त किया जा सकता है। इसके अलावा, सेमेंटिक्स LNL, एडजॉइंट लॉजिक और mGL जैसे स्थापित सिस्टमों को समाहित करता है।

मुख्य योगदान और परिणाम

लॉजिक्स का एकीकरण: Grass एक ऐसा एकल फ्रेमवर्क प्रदान करता है जहाँ वेरिएबल्स को एक ही समय में विभिन्न ग्रेड बीजगणक द्वारा नियंत्रित किया जा सकता है। उदाहरण के लिए, एक फंक्शन एक "सिक्योरिटी" बीजगणक द्वारा ग्रेडेड की (key) स्वीकार कर सकता है (जहाँ $High $एक सुरक्षित संदर्भ को दर्शाता है) और एक "यूसेज" बीजगणक द्वारा ग्रेडेड फाइल हैंडल (जहाँ$ 1$ लीनियर उपयोग को दर्शाता है)।
सूक्ष्म स्ट्रक्चरल नियंत्रण: मोड के रूप में आइडियल्स को परिभाषित करके, Grass उन संसाधन-संवेदनशील अंतरों को व्यक्त करने की अनुमति देता है जिन्हें पिछले ग्रेडेड सिस्टम आसानी से व्यक्त नहीं कर सके। उदाहरण के लिए, दो लीनियर रूप से उपयोग किए जाने वाले फाइल हैंडल (ग्रेड 1) को एक एकल अनरिस्ट्रिक्टेड हैंडल (ग्रेड $\omega$ ) में कॉन्ट्रैक्ट नहीं किया जा सकता है, जो असुरक्षित रिसोर्स मर्जिंग को रोकता है।
मौजूदा सिस्टम की रिकवरी: पेपर यह प्रदर्शित करता है कि विशिष्ट मोड्स को इंस्टेंशिएट करके, Grass निम्नलिखित को रिकवर करता है:
- इंट्यूशनिस्टिक लॉजिक: मोड $U = (\top, \top, \text{true})$ ।
- लीनियर लॉजिक: मोड $L = (\mathbb{N}, \{0\}, \text{false})$ (डिस्क्रीट ऑर्डरिंग के साथ)।
- रेलिवेंट लॉजिक: मोड $R = (\top, \top, \text{false})$ ।
- एफाइन लॉजिक: मोड $A = (\{0, 1\}, \{0\}, \text{true})$ ।
- LNL और एडजॉइंट लॉजिक: उपयुक्त मॉर्फिज्म के साथ मोड्स को मिलाकर।
कैटेगोरिकल साउंडनेस: लेखक सिद्ध करते हैं कि $\beta$ - और $\eta$ -कन्वर्जन कैटेगोरिकल सेमेंटिक्स के सापेक्ष साउंड हैं। टर्म्स का कैटेगोरिकल मॉडल में इंटरप्रिटेशन टाइपिंग और ग्रेडिंग को सुरक्षित रखता है।

महत्व और दावे

पेपर दावा करता है कि Grass "वेरिएबल उपयोग पर अधिकतम लचीला नियंत्रण" प्रदान करता है क्योंकि यह दोनों (सबस्ट्रक्चरल और ग्रेडेड) लॉजिक्स से तंत्रों को शामिल करता है। इसका प्राथमिक महत्व है:

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

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