1117 पेपर
यह शोध पत्र कंप्यूटर विज्ञान के परिचयात्मक पाठ्यक्रमों के लिए एक शैक्षणिक दृष्टिकोण प्रस्तावित करता है जो केवल विशिष्ट मौलिक विषयों पर ध्यान केंद्रित करने के बजाय ट्रांसिटिव क्लोजर (transitive closure) जैसे ठोस उदाहरणों के माध्यम से मौलिक प्रमाण तकनीकों और अमूर्त संरचनाओं को पढ़ाने को प्राथमिकता देता है, यह एक ऐसी विधि है जो लेखकों के स्टेफ़ानो बेरार्डी के साथ सहयोगात्मक शिक्षण अनुभव से प्रेरित है।
यह शोधपत्र स्टेफ़ानो बेरार्डी द्वारा शास्त्रीय तर्कशास्त्र (क्लासिकल लॉजिक) के गेम सेमेंटिक्स के संबंध में की गई दो अप्रकाशित टिप्पणियों को प्रस्तुत और स्पष्ट करता है।
यह शोध पत्र यह स्थापित करता है कि शुद्ध बहुरूपी आश्रित प्रकार सिद्धांत (P2) में, पैरामीट्रिक कोटिएंट प्रकार और सुदृढ़ सह-आगमन सिद्धांत परिभाषित नहीं किए जा सकते हैं, और फंक्शन एक्सटेंशनैलिटी (function extensionality) इंडक्शन सिद्धांतों को सिद्ध करने के लिए सख्ती से आवश्यक है, जो विशिष्ट मॉडलों का निर्माण करके किया गया है जहाँ ये सिद्धांत विफल हो जाते हैं।
यह शोध पत्र यह स्थापित करता है कि अनंत-अवरोहण (infinite-descent) प्रमाण प्रणाली LKID-omega में प्रमाणयोग्यता की तार्किक जटिलता -पूर्ण है, जो मानक और मानक पद मॉडलों (standard and standard term models) में वैधता की समानता को प्रदर्शित करके और -भाषाओं के सत्य विधेय (truth predicate) को आगमनात्मक परिभाषाओं (inductive definitions) तक विस्तारित करके सिद्ध होता है।
यह शोधपत्र नियमितता के मॉड्युली (moduli of regularity) की गणनात्मक सामग्री और तार्किक शक्ति की जांच करता है, जो निरंतर फलनों (continuous functions) के शून्यों और अनंत वृक्षों (infinite trees) में पथों की एल्गोरिद्मिक रूप से गणना करने की उनकी क्षमता को प्रदर्शित करता है, साथ ही यह भी स्थापित करता है कि कोई भी सुव्यवस्थित गैर-मानक सिद्धांत (tame nonstandard principle) इस संदर्भ में कॉम्पैक्टनेस (compactness) को मीट्रिक बंध्यता (metric boundedness) से प्रतिस्थापित नहीं कर सकता है।
यह शोध पत्र पूरे वृक्षों के बजाय वृक्ष की शाखाओं पर ध्यान केंद्रित करके लैम्ब्डा-कैलकुलस (lambda-calculus) पर एक अपरंपरागत परिप्रेक्ष्य प्रस्तावित करता है, जिससे बीटा-रिडक्शन (beta-reduction) का एक ऐसा पुनर्गठन होता है जो पदों (terms) का विस्तार इस प्रकार करता है कि कम किए गए पद का वृक्ष मूल को एक उप-वृक्ष (subtree) के रूप में समाहित करता है।
यह शोध पत्र इंटरसेक्शन टाइप सिस्टम में प्रिंसिपल टाइपिंग्स की ऐतिहासिक समझ को सरल बनाता है, जिसमें टाइप डेरिवेशंस के निर्माण के लिए तीन मौलिक ऑपरेशन्स की पहचान की गई है और एक सेमी-एल्गोरिदम को डिज़ाइन किया गया है जो सभी स्ट्रॉन्गली नॉर्मलाइज़िंग लैम्ब्डा टर्म्स के लिए प्रिंसिपल टाइपिंग्स की गणना करता है।
यह शोध पत्र कंटीन्यूअस मोडल लॉजिकल न्यूरल नेटवर्क्स (CMLNNs) को प्रस्तुत करता है, जो 'फ्लुइड लॉजिक' नामक एक ढांचा है जो न्यूरल स्टोकेस्टिक डिफरेंशियल इक्वेशंस का उपयोग करके मोडल रीजनिंग को विविक्त संरचनाओं से निरंतर मैनिफोल्ड्स तक ले जाता है ताकि तार्किक बाधाओं को सीधे न्यूरल नेटवर्क प्रशिक्षण में समाहित किया जा सके, जिससे बिना किसी स्पष्ट शासी समीकरणों की आवश्यकता के एपिस्टेमिक, टेम्पोरल और डियोन्टिक रीजनिंग कार्यों के लिए संरचनात्मक रूप से सुसंगत समाधान सक्षम हो सकें।
यह शोध पत्र प्रदर्शित करता है कि नॉन-ब्लॉकिंग ब्रॉडकास्ट प्रोटोकॉल को 'वेट-ओनली' (Wait-Only) प्रॉपर्टी तक सीमित करने से स्टेट और कॉन्फ़िगरेशन कवेरेबिलिटी समस्याओं की कम्प्यूटेशनल जटिलता, एकरमैन-हार्ड (Ackermann-hard) से घटकर क्रमशः पी-कम्प्लीट (P-complete) और पी-स्पेस-कम्प्लीट (PSPACE-complete) हो जाती है।
यह शोध पत्र लगभग रैखिक पुनरावर्ती अनुक्रमों (nearly linearly recurrent sequences) के लिए धनात्मकता समस्या (Positivity Problem) प्रस्तुत करता है, जो रैखिक पुनरावर्तनों का एक सामान्यीकरण है, और अनंत श्रेणियों के लिए एक नवीन अपरिमेयता परिणाम (transcendence result) द्वारा समर्थित क्रम-दो (order-two) मामलों के लिए एक निर्णय प्रक्रिया प्रस्तुत करता है।