Algebraic Semantics of Datalog with Equality

तकनीकी सारांश: समानता के साथ डैटलॉग (Datalog) का बीजगणितीय अर्थविज्ञान (Algebraic Semantics)

समस्या विवरण
यह शोध पत्र एक एकीकृत अर्थपूर्ण ढांचे (semantic framework) की आवश्यकता को संबोधित करता है जो ई-ग्राफ (e-graphs) और समानता संतृप्ति (equality saturation) तकनीकों में पाए जाने वाले समानता हैंडलिंग और आंशिक फलन (partial function) समर्थन के साथ डैटलॉग की तार्किक निष्कर्ष क्षमताओं को जोड़ता है। मानक डैटलॉग हॉर्न क्लॉज़ (Horn clauses) तक सीमित है जहाँ निष्कर्षों में चर (variables) अनिवार्य रूप से आधारों (premises) में दिखने चाहिए, और इसमें शब्दों (terms) को समान करने या निष्कर्षों में अस्तित्वगत चरों (existential variables) को पेश करने का मूल समर्थन नहीं है। जबकि ई-ग्राफ समानता और संगति (congruence) को कुशलतापूर्वक संभालते हैं, वे अक्सर एड-हॉक एल्गोरिदम के माध्यम से कार्यान्वित किए जाते हैं। लेखक एक ऐसी भाषा को औपचारिक रूप देने का प्रयास करते हैं जो डैटलॉग और इन समानता-आधारित अनुकूलनों दोनों को समाहित करती है, जो एक कठोर बीजगणितीय अर्थविज्ञान प्रदान करती है जो यह बताती है कि मूल्यांकन एल्गोरिदम (जैसे कि Eqlog इंजन में) कैसे काम करते हैं, न कि केवल यह कि वे क्या करते हैं।

कार्यप्रणाली
लेखक अपने प्रस्तावित लॉजिक्स के लिए अर्थविज्ञान (semantics) का निर्माण करने हेतु श्रेणी सिद्धांत (category theory), विशेष रूप से स्थानीय रूप से प्रस्तुत श्रेणियों (locally presentable categories) में अंतःक्षेपण (injectivity) और लंबवतता (orthogonality) के सिद्धांत का उपयोग करते हैं।

1. संबंधात्मक हॉर्न लॉजिक (Relational Horn Logic - RHL): लेखक RHL को डैटलॉग के विस्तार के रूप में परिभाषित करते हैं जो निम्नलिखित की अनुमति देता है:

   • सॉर्ट क्वांटिफिकेशन (sort quantification) (चर किसी सॉर्ट के किसी भी तत्व से मेल खाते हैं)।
   • वे चर जो केवल निष्कर्ष में दिखाई देते हैं (अस्तित्वगत क्वांटिफिकेशन के रूप में व्याख्यायित)।
   • निष्कर्षों में समानता परमाणु (equality atoms) ($u \equiv v$)।
     इसका अर्थविज्ञान संबंधात्मक संरचनाओं (relational structures) पर परिभाषित है। एक अनुक्रम (sequent) की संतुष्टि को "वर्गीकृत रूपांतरणों" (classifying morphisms) के विरुद्ध "लिफ्टिंग गुणों" (lifting properties) के माध्यम से वर्णित किया जाता है। विशेष रूप से, एक मॉडल एक अनुक्रम को तब संतुष्ट करता है जब वह एक विशिष्ट रूपांतरण के प्रति अंतःक्षेपी (injective) या लंबवत (orthogonal) होता है।

2. स्मॉल ऑब्जेक्ट तर्क (The Small Object Argument): मुक्त मॉडलों (free models) के अस्तित्व को सिद्ध करने के लिए, लेखक स्मॉल ऑब्जेक्ट तर्क का उपयोग करते हैं। इसे केवल एक होमोटॉपी-थ्योरेटिक उपकरण के रूप में नहीं, बल्कि डैटलॉग मूल्यांकन प्रक्रिया के एक अमूर्त सामान्यीकरण के रूप में प्रस्तुत किया गया है। एक सिद्धांत के वर्गीकृत रूपांतरणों को पुनरावर्ती रूप से लागू करके, वे संबंधात्मक संरचनाओं के एक अनुक्रम का निर्माण करते हैं जो एक मुक्त मॉडल (एक कमजोर प्रतिबिंब या मॉडल के उप-वर्ग में प्रतिबिंब) की ओर अभिसरित होता है।

3. आंशिक हॉर्न लॉजिक (Partial Horn Logic - PHL): फलन प्रतीकों (function symbols) और आंशिक फलनों को संभालने के लिए, लेखक PHL को RHL के एक सिंटैक्टिक विस्तार के रूप में पेश करते हैं। PHL संयोजित शब्दों और फलन प्रतीकों की अनुमति देता है, जिन्हें फलन के ग्राफ का प्रतिनिधित्व करने वाले संबंधात्मक परमाणुओं में "डीसुगर" (desugared) किया जाता है, जिसके साथ कार्यात्मकता के सिद्धांत (functionality axioms) जुड़े होते हैं। यह PHL को RHL पर एक समकक्ष वर्णनात्मक शक्ति वाले सिंटैक्टिक शुगर के रूप में स्थापित करता है।

4. स्ट्रोंग थ्योरीज और एपिक अनुक्रम (Strong Theories and Epic Sequents): सामान्य सिद्धांतों और स्ट्रोंग सिद्धांतों (जहाँ अंतःक्षेपण, लंबवतता के साथ मेल खाता है) के बीच एक महत्वपूर्ण अंतर किया गया है। स्ट्रोंग सिद्धांतों के लिए, स्मॉल ऑब्जेक्ट तर्क एक अद्वितीय प्रतिबिंब (free model) प्रदान करता है। लेखक दिखाते हैं कि हालांकि किसी भी स्वैच्छिक RHL सिद्धांत की स्ट्रंगनेस की जांच करना अनिर्णायक (undecidable) है, लेकिन एपिक PHL सिद्धांतों का उपसमुच्चय (जहाँ निष्कर्ष में नए चर पेश नहीं किए जाते) आसानी से पहचाना जा सकता है और स्ट्रंगनेस की गारंटी देता है।

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

• मुक्त मॉडलों का नया निर्माण: यह शोध पत्र वर्गीकृत रूपांतरणों के विरुद्ध लिफ्टिंग गुणों का उपयोग करके RHL और PHL सिद्धांतों के लिए मुक्त मॉडलों का एक अभिनव निर्माण प्रदान करता है। यह निर्माण डैटलॉग मूल्यांकन के रूप में स्मॉल ऑब्जेक्ट तर्क को एक अमूर्त रूप प्रदान करता है। यह दिखाता है कि कैसे RHL/PHL सिद्धांतों का मूल्यांकन डैगलॉग के फिक्स्ड-पॉइंट इटरेशन का सामान्यीकरण करता है, जो स्वाभाविक रूप से समानता प्रसार (congruence) और नए पहचानकर्ताओं (identifiers) को शामिल करता है।
• सेटॉइड रूपांतरण (Setoid Transformation): एक न्यूनीकरण (reduction) प्रस्तुत किया गया है जो दिखाता है कि RHL को "विकल्प के साथ डैटलॉग" (Datalog with choice) में बदला जा सकता है। यह समानता परमाणुओं को स्पष्ट तुल्यता संबंधों ($Eqs$) में मैप करता है और संगति सिद्धांतों को लागू करता है। हालांकि यह सैद्धांतिक रूप से सुदृढ़ है, लेखक नोट करते हैं कि यह अक्सर तुल्यता संबंधों के लिए द्विघातीय मेमोरी आवश्यकताओं और संगति सिद्धांतों से होने वाली घातांकीय वृद्धि के कारण गणनात्मक रूप से अव्यवहार्य हो सकता है।
• व्यावहारिक भाषा के रूप में एपिक PHL: यह शोध पत्र तर्क देता है कि जबकि RHL सामान्य अर्थपूर्ण आधार है, एपिक PHL उपकरणों के लिए पसंदीदा इनपुट भाषा है। यह सत्यापित करने के लिए सिंटैक्टिक रूप से सरल है (यह जांचना कि क्या निष्कर्ष नए चर पेश करते हैं) और अद्वितीय मुक्त मॉडल गणना के लिए आवश्यक स्ट्रंग गुण की गारंटी देता है।

परिणाम

• मॉडलों का अस्तित्व: यह शोध पत्र सिद्ध करता है कि किसी भी RHL सिद्धांत के लिए, एक कमजोर रूप से मुक्त मॉडल मौजूद होता है। यदि सिद्धांत स्ट्रोंग है (जैसे कि एक एपिक PHло सिद्धांत), तो एक मुक्त मॉडल मौजूद होता है।
• समाप्ति (Termination): लेखक सिद्ध करते हैं कि केवल सरफेसिव अनुक्रमों (जहाँ सभी निष्कर्ष चर आधार में दिखाई देते हैं) वाले सिद्धांतों के लिए, मूल्यांकन प्रक्रिया परिमित इनपुट संरचनाओं पर समाप्त हो जाती है। यह मानक डैगलॉग के ज्ञात समाप्ति गुण का सामान्यीकरण करता है।
• पूर्णता (Completeness): यह स्थापित करता है कि प्रत्येक परिमित संबंधात्मक संरचना के रूपांतरण को एक RHL अनुक्रम के वर्गीकृत रूपांतरण के रूप में वर्णित किया जा सकता है। इसी तरह, प्रत्येक परिमित बीजगणितीय संरचना का प्रत्येक एपिक PHL अनुक्रम के अनुरूप होता है।
• श्रेणियों की तुल्यता: यह दिखाया गया है कि RHL सिद्धांत के मॉडलों की श्रेणी, उसके 'डैटलॉग-विद-चॉइस' रूपांतरण के सेटॉइड मॉडलों की श्रेणी के समतुल्य है। इसके अतिरिक्त, एक एपिक PHL सिद्धांत के मॉडलों की श्रेणी बीजगणितीय संरचनाओं और संबंधात्मक संरचनाओं दोनों के परावर्तक उप-वर्ग (reflective subcategory) के रूप में है।

महत्व और दावे
यह शोध पत्र Eqlog डैगलॉग इंजन के लिए बीजगणितीय अर्थविज्ञान प्रदान करने का दावा करता है, जो एपिक PHL सिद्धांतों के मुक्त मॉडल की गणना करता है। इसका महत्व निम्नलिखित है:

1. सैद्धांतिक आधार: यह Eqlog एल्गोरिदम के लिए एक कठोर श्रेणीगत औचित्य प्रदान करता है, जिसे स्मॉल ऑब्जेक्ट तर्क के कार्यान्वयन के रूप में फ्रेम किया गया है।
2. समुदायों को जोड़ना: यह डैगलॉग समुदाय (प्रोग्राम विश्लेषण, पॉइंट्स-टू विश्लेषण) को ई-ग्राफ समुदाय (इक्वैलिटी सैचुरेशन, प्रोग्राम ऑप्टिमाइज़ेशन) के साथ एक एकल तार्किक ढांचे (PHL) के तहत जोड़ता है।
3. सिंटैक्टिक बनाम सिमेंटिक स्पष्टता: यह स्पष्ट करता है कि जबकि RHL सामान्य अर्थपूर्ण वाहन है, PHL (विशेष रूप से एपिक खंड) अनिश्चित निर्णय योग्यताओं के बिना अद्वितीय, निर्धारित गणनाओं को सुनिश्चित करने के लिए व्यावहारिक भाषा है।

लेखक स्पष्ट रूप से कहते हैं कि मूल्यांकन एल्गोरिदम (जो सेमी-नेइव इवैल्यूएशन और यूनियन-फाइंड तकनीकों को जोड़ता है) को एक अलग कार्य (Bidlingmaier, 2023) में विस्तृत किया गया है, और Egglog टूल (Willsey et al., 2021) स्वतंत्र रूप से समान विचारों तक पहुँचा है। इस शोध पत्र का योगदान विशेष रूप से अर्थपूर्ण ढांचे और ऐसे इंजनों द्वारा गणना किए गए मॉडलों के अस्तित्व और विशिष्टता के प्रमाण तक सीमित है।