Fully Evaluated Left-Sequential Logics

तकनीकी सारांश: पूर्णतः मूल्यांकित बाएँ-अनुक्रमिक तर्क (Fully Evaluated Left-Sequential Logics)

समस्या विवरण
यह शोध पत्र "पूर्णतः मूल्यांकित बाएँ-अनुक्रमिक तर्क" (FELs) के औपचारिककरण और स्वयंसिद्धीकरण (axiomatization) को संबोधित करता है। शॉर्ट-सर्किट लॉजिक्स (SCLs) के विपरीत, जहाँ एक संयुक्त अभिव्यक्ति के परिणाम के निर्धारित होते ही मूल्यांकन रुक जाता है, FELs एक "पूर्ण" या "सख्त" मूल्यांकन रणनीति निर्धारित करते हैं: प्रत्येक परमाणु प्रस्ताव (atomic proposition) को एक टर्म के भीतर मूल्यांकित किया जाता है, चाहे उसका मान अंतिम परिणाम के लिए अनिवार्य रूप से आवश्यक हो या नहीं। इस रणनीति का उद्देश्य उन प्रोग्रामिंग संदर्भों से प्रेरित है जहाँ सभी परमाणुओं के लिए साइड इफेक्ट्स (जैसे कि स्टेट परिवर्तन) का होना सुनिश्चित किया जाना चाहिए। लेखक ऐसे तर्कों की एक श्रेणी (hierarchy) को परिभाषित करने का लक्ष्य रखते हैं, जो सबसे कमजोर (Free FEL) से लेकर सबसे मजबूत (Static FEL) तक विस्तृत है, जहाँ Free FEL परमाणु साइड इफेक्ट्स के प्रति प्रतिरक्षित है, और Static FEL एक शास्त्रीय प्रस्तावात्मक तर्क के अनुक्रमिक संस्करण की तरह व्यवहार करता है। इसके अतिरिक्त, यह शोध पत्र इन तर्कों को "अपरिभाषितता" ($U$) को संभालने के लिए एक त्रि-मान (three-valued) सेटिंग में विस्तारित करता है, जो प्रोग्रामिंग और तर्क (जैसे कि शून्य से विभाजन) में एक सामान्य विशेषता है।

कार्यप्रणाली
लेखक मूल्यांकन वृक्षों (evaluation trees) पर आधारित एक अर्थ संबंधी ढांचे (semantic framework) का उपयोग करते हैं, जो उनके पूर्व कार्य [19] में प्रस्तुत किया गया था।

1. अर्थ विज्ञान (Semantics): मूल्यांकन वृक्ष बाइनरी ट्री (binary trees) हैं जहाँ आंतरिक नोड्स परमाणुओं का प्रतिनिधित्व करते हैं और लीव्स (leaves) सत्य मूल्यों ($T$, $F$, या $U$) का प्रतिनिधित्व करते हैं। रूट से लीफ तक का एक पथ मूल्यांकन अनुक्रम को मॉडल करता है।
   • Free FEL (FFEL) में, वृक्ष संरचना मूल्यांकन के क्रम को सख्ती से बनाए रखती है और एक ही परमाणु के बार-बार होने की अनुमति देती है, जो संभावित साइड इफेक्ट्स को मॉडल करती है।
   • Memorising FEL (MFEL) में, अर्थ विज्ञान को इस प्रकार परिष्कृत किया गया है कि वृक्ष के किसी भी पथ में एक ही परमाणु के कई उदाहरण नहीं होते; यदि कोई परमाणु दोबारा आता है, तो उसका मूल्यांकन "याद" (memorized) कर लिया जाता है।
   • Conditional FEL (CℓFEL) में, तर्क परमाणुओं की क्रमविनिमेयता (commutativity) को शामिल करता है, प्रभावी रूप से स्वतंत्र परमाणुओं के क्रम को अप्रासंगिक मानता है।
   • Static FEL (SFEL) में, तर्क एक प्रस्तावात्मक तर्क के अनुक्रमिक संस्करण में सिमट जाता है जहाँ अवशोषण नियम (absorption laws) लागू होते हैं।
2. त्रि-मान विस्तार: सभी तर्कों के लिए, सिवाय SFEL के, लेखक एक स्थिरांक $U$ (अपरिभाषित) पेश करते हैं। अर्थ विज्ञान को $\{T, F, U\}$ में लीव्स वाले वृक्षों के लिए विस्तारित किया गया है, जहाँ $U$ एक अवशोषक तत्व के रूप में कार्य करता है (उदाहरण के लिए, $U \land_r x = U$)।
3. स्वयंसिद्धीकरण (Axiomatization): प्राथमिक पद्धतिगत योगदान प्रत्येक तर्क के लिए पूर्ण समीकरण स्वयंसिद्धीकरण (complete equational axiomatizations) का व्युत्पन्न है। लेखक पूर्णता सिद्ध करने के लिए सामान्य रूपों (जैसे, FEL Normal Form, $\sigma$-normal forms) को परिभाषित करते हैं। वे व्युत्पन्नता को सत्यापित करने के लिए थ्योरम प्रूवर Prover9 का और स्वतंत्रता को सिद्ध करने के लिए सीमित प्रति-मॉडल (counter-models) उत्पन्न करने के लिए Mace4 का उपयोग करते हैं।

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

1. द्वि-मान FELs की श्रेणी (Hierarchy):

   • Free FEL (FFEL): सबसे कमजोर तर्क, जिसे $EqFFEL$ द्वारा स्वयंसिद्ध किया गया है। यह इडेम्पोटेंस (idempotence) को खंडित करता है ($x \land_r x \neq x$) लेकिन साहचर्य (associativity) को संतुष्ट करता है। यह साइड-इफेक्ट बाधाओं के बिना पूर्ण मूल्यांकन का तर्क है।
   • Memorising FEL (MFEL): FFEL में एक स्वयंसिद्ध जोड़ने से स्वयंसिद्ध किया गया है (विशेष रूप से, $(x \lor_r y) \land_r z = (\neg x \land_r (y \land_r z)) \lor_r (x \land_r z)$)। यह सुनिश्चित करता है कि दोहराए गए परमाणुओं को समान माना जाए, जिससे साइड इफेक्ट्स समाप्त हो जाते हैं।
   • Conditional FEL (CℓFEL$_2$): MFEL में क्रमविनिमेयता ($x \land_r y = y \land_r x$) जोड़ने से स्वयंसिद्ध किया गया है। यह तर्क Conditional Logic (Guzmán और Squier [12]) के द्वि-मान उप-तर्क के समकक्ष है।
   • Static FEL (SFEL): सबसे मजबूत तर्क, जो CℓFEL$_2$ में $x \land_r F = F$ जोड़ने से प्राप्त होता है। यह SSCL और अनुक्रमिक मूल्यांकन के तहत मानक प्रस्तावात्मक तर्क के समकक्ष है।

2. त्रि-मान विस्तार (FELU):

   • लेखक $\neg U = U$ और $U \land_r x = U$ स्वयंसिद्धों को जोड़कर तीन-मान संस्करण (FFELU, MFELU, CℓFEL) को परिभाषित करते हैं।
   • CℓFEL (तीन-मान Conditional FEL) को Bochvar के सख्त तर्क [8] के समकक्ष सिद्ध किया गया है।
   • SFEL को $U$ के साथ विस्तारित नहीं किया जा सकता क्योंकि अवशोषण नियम $F = U \land_r F = U$ सत्य मूल्यों के पतन (collapse) की ओर ले जाता है।

3. पूर्णता और स्वतंत्रता (Completeness and Independence):

   • सभी परिभाषित तर्कों के लिए पूर्ण समीकरण स्वयंसिद्धीकरण प्रदान किए गए हैं।
   • लेखक प्रत्येक तर्क के लिए वैकल्पिक, अधिक संक्षिप्त स्वतंत्र स्वयंसिद्धों के सेट प्रस्तुत करते हैं (जैसे, MFEL के लिए $MF$ सेट), जिन्हें स्वचालित उपकरणों द्वारा सत्यापित किया गया है।
   • सामान्य रूपों का निर्माण यह सिद्ध करने के लिए किया गया है कि सामान्य रूपों की वाक्यात्मक समानता (syntactic equality) मूल्यांकन वृक्षों की अर्थ संबंधी समानता के अनुरूप है।

महत्व और दावे
यह शोध पत्र पूर्ण बाएँ-अनुक्रमिक मूल्यांकन को समझने के लिए एक एकीकृत ढांचा प्रदान करने का दावा करता है, जो शॉर्ट-सर्किट लॉजिक्स और शास्त्रीय प्रस्तावात्मक तर्क के बीच के अंतर को पाटता है।

• पूर्वानुमेयता (Predictability): लेखक तर्क देते हैं कि SCLs की तुलना में FELs मूल्यांकन के बाद वातावरण की स्थिति (साइड इफेक्ट्स) के संबंध में अधिक पूर्वानुमान क्षमता प्रदान करते हैं, क्योंकि सभी परमाणुओं का मूल्यांकन होना सुनिश्चित है।
• अभिव्यक्ति क्षमता (Expressiveness): शोध पत्र प्रदर्शित करता है कि जबकि FFEL कुछ समान मूल्यांकन वृक्षों (जैसे, ऐसे वृक्ष जहाँ एक परमाणु विभिन्न शाखाओं में अलग-अलग परिणामों के साथ दिखाई देता है) को व्यक्त नहीं कर सकता है, MFEL और उससे मजबूत तर्क इन्हें व्यक्त कर सकते हैं, जिससे तर्क की अभिव्यक्ति शक्ति बढ़ जाती है।
• मौजूदा कार्य से संबंध: यह कार्य CℓFEL को तर्कों की श्रेणी में स्थापित करता है, यह दिखाते हुए कि यह Bochvar के तर्क और Conditional Logic के एक उप-तर्क के समकक्ष है। यह FELs और शॉर्ट-सर्किट लॉजिक्स (SCLs) के बीच संबंध को भी स्पष्ट करता है, यह नोट करते हुए कि FEL कनेक्टिव्स को SCL फ्रेमवर्क के भीतर परिभाषित किया जा सकता है (और विशिष्ट स्थितियों के तहत इसके विपरीत भी), हालांकि FELs एक सख्त मूल्यांकन अनुशासन लागू करते हैं।

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