1086 पेपर
यह शोध पत्र एक नवीन क्वांटम प्रोग्रामिंग भाषा प्रस्तुत करता है जो एक लीनियर टाइप सिस्टम से सुसज्जित है जो क्वांटम कंडीशनल ब्रांचिंग में पत्राचार समस्या (correspondence problem) को हल करता है, जिससे सामान्य क्वांटम चैनलों पर क्वांटम SWITCH की सुस्पष्ट अभिव्यक्ति संभव हो पाती है।
यह खंड 21वें लॉजिकल एंड सिमेंटिक फ्रेमवर्क्स विद एप्लिकेशन्स वर्कशॉप (LSFA 2026) के कार्यवाही विवरण को प्रस्तुत करता है, जो जुलाई 2026 में लिस्बन में आयोजित किया गया था, जिसका उद्देश्य लैम्ब्डा कैलकुलस और मशीन लर्निंग जैसे क्षेत्रों में सैद्धांतिक प्रगति को उनके व्यावहारिक कार्यान्वयन और अनुप्रयोग के साथ जोड़ना है।
यह शोध पत्र एक क्वांटम कंट्रोल वाले टाइपड लैम्ब्डा कैलकुलस का प्रस्ताव करता है, जो अंतर्ज्ञानवादी (intuitionistic) BV लॉजिक और एक नवीन Caus-संबंधित मॉडल पर आधारित है, ताकि भौतिक कार्य-कारणता (physical causality) को औपचारिक रूप से लागू किया जा सके और यह प्रदर्शित किया जा सके कि अनिश्चित कार्य-कारण क्रम (indefinite causal order) वाली कुछ भौतिक रूप से अव्यवहार्य प्रक्रियाएं इस भाषा के भीतर अनिर्धारित (undefinable) हैं।
यह शोध पत्र समृद्ध श्रेणी सिद्धांत (enriched category theory) का उपयोग करके पैरामीटराइज्ड क्वांटम सर्किट को मॉडल करने के लिए एक रूपरेखा प्रस्तावित करता है, जो नियंत्रित ऑपरेशन्स के लिए नए दृष्टिकोण प्रदान करता है और कार्टेशियन और मोनॉइडल क्लोज्ड पैरामीटर मामलों के माध्यम से क्वांटम नियंत्रण के विभिन्न दृष्टिकोणों को एकीकृत करता है।
यह शोध पत्र लीनियर एक्सपोनेंशियल कोमोनेड्स (linear exponential comonads) और कोडरिलेक्शन ट्रांसफॉर्मेशन (codereliction transformations) के द्विकैटेगोरिकल संस्करणों को पेश करके मोनॉइडल द्विकैटेगरीज (monoidal bicategories) के सिद्धांत को आगे बढ़ाता है, जिससे प्रेशेफ श्रेणियों (presheaf categories) के बीच एकल-चर से बहु-चर संदर्भों तक जॉयल के एनालिटिक फंक्टर्स के डिफरेंशियल कैलकुलस का विस्तार किया जाता है।
यह शोध पत्र एब्स्ट्रैक्ट सटीक वास्तविक संख्याओं (abstract exact real numbers) और पॉलिश स्पेस (Polish spaces) पर हाइपरस्पेस और उपसमुच्चय ऑपरेशन्स का एक कोक (Coq) औपचारिकीकरण प्रस्तुत करता है, जो एक नॉन-डिटरमिनिस्टिक निरंतरता सिद्धांत (nondeterministic continuity principle) के माध्यम से जेनेरिक टोपोलॉजिकल और कुशल मेट्रिक एनकोडिंग्स के बीच कम्प्यूटेशनल तुल्यता स्थापित करके फ्रैक्टल जनरेशन जैसे कार्यों के लिए प्रमाणित, त्रुटि-मुक्त प्रोग्राम व्युत्पन्न करता है।
यह शोधपत्र तर्क देता है कि डिपेंडेंट टाइप थ्योरी के लिए डेफिनिशनल इक्वैलिटी (definitional equality) हेतु निर्णय प्रक्रियाओं (decision procedures) को प्रमाणित करने के लिए नॉर्मलाइजेशन (normalization) के बजाय इंजेक्टिविटी गुण (injectivity properties), पूर्णतः अनटाइप्ड कन्वर्जन चेकर्स (fully untyped conversion checkers) सहित, एक महत्वपूर्ण और पर्याप्त आधार हैं।
यह शोध पत्र "भौतिक गणना असंभवता प्रमेय" (Physical Counting Impossibility Theorem) को स्थापित करता है, जो यह तर्क देता है कि कोई भी निश्चित-बजट वाला भौतिक आधार सार्वभौमिक सटीक प्रमाण प्रदान नहीं कर सकता क्योंकि आवश्यक अपरिवर्तनीय रिकॉर्ड बनाए रखने की ऊष्मागतिक लागत अंततः प्रणाली की सीमित क्षमता से अधिक हो जाती है।
यह शोध पत्र CoreForge पर रिपोर्ट करता है, जो एक ऐसा प्रयोग है जो यह प्रदर्शित करता है कि बड़े भाषा मॉडल (large language models) एक पुनरावृत्ति कार्यप्रवाह (iterative workflow) के माध्यम से सीधे शोध पत्रों से एक कार्यात्मक अनवेटेड मैक्ससैट (unweighted MaxSAT) सॉल्वर बनाने में सफलतापूर्वक सहायता कर सकते हैं, हालांकि परिणामी प्रणाली को अभी भी मानव मार्गदर्शन और सत्यापन की आवश्यकता होती है और प्रदर्शन के मामले में हाथ से निर्मित (hand-engineered) सॉल्वरों से पीछे है।
यह लेख प्रोसेस अलजेब्रा फॉर्मलिज्म μCRL और इसके उत्तराधिकारी mCRL2 के विकास, गणितीय आधारों और व्यावहारिक अनुप्रयोगों का एक व्यापक ऐतिहासिक अवलोकन प्रदान करता है, जो सैद्धांतिक अवधारणाओं से लेकर जटिल परस्पर क्रिया करने वाले कंप्यूटर सिस्टम के मॉडलिंग और विश्लेषण के लिए बहुमुखी उपकरणों तक उनके विकास को रेखांकित करता है।