💻 computer science

Automaton-based Characterisations of First Order Logic over Infinite Trees

यह शोधपत्र यह स्थापित करता है कि अनंत वृक्षों (infinite trees) पर प्रथम-क्रम तर्क (First-Order Logic), \PolPCTL और \CTLsf के अनुरूप हिचकिचाते वृक्ष ऑटोमेटा (hesitant tree automata) के दो वर्गों द्वारा सटीक रूप से कैप्चर किया जाता है, जिससे एक समान ऑटोमेटा-सैद्धांतिक लक्षण वर्णन प्राप्त होता है और यह प्रकट होता है कि प्रथम-क्रम परिभाषितता (first-order definability) मौलिक रूप से प्रत्येक शाखा के साथ सुरक्षा (safety) या सह-सुरक्षा (co-safety) गुणों तक ही सीमित है।

मूल लेखक: Massimo Benerecetti, Dario Della Monica, Angelo Matteo, Fabio Mogavero, Gabriele Puppis

प्रकाशित 2026-04-30

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

CC BY 4.0

मूल लेखक: Massimo Benerecetti, Dario Della Monica, Angelo Matteo, Fabio Mogavero, Gabriele Puppis

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

मुख्य चित्र: जंगल का मानचित्रण

कल्पना कीजिए कि आप एक विशाल, अनंत जंगल का वर्णन करने की कोशिश कर रहे हैं। इसे करने के लिए आपके पास दो उपकरण हैं:

फर्स्ट-ऑर्डर लॉजिक (FO): एक बहुत ही सटीक, नियम-आधारित भाषा (जैसे निर्देशों का एक सख्त सेट) जो व्यक्तिगत पेड़ों, उनके माता-पिता, उनके बच्चों और उनके बीच के जुड़ाव के बारे में बात कर सकती है।
ट्री ऑटोमेटा (Tree Automata): एक प्रकार का रोबोट जो जंगल में घूमता है और यह जाँचता है कि क्या पेड़ कुछ नियमों का पालन कर रहे हैं।

इस शोध पत्र का मुख्य लक्ष्य एक कठिन प्रश्न का उत्तर देना है: क्या हम एक विशिष्ट प्रकार का रोबोट बना सकते हैं जो बिल्हीं उसी चीज़ की जाँच कर सके जिसकी हमारी सख्त नियम-आधारित भाषा करती है?

सरल रेखाओं की दुनिया में (जैसे पेड़ों का एक एकल पथ), हम पहले से ही जानते हैं कि उत्तर 'हाँ' है: वहाँ एक सटीक मिलान मौजूद है। लेकिन एक शाखाओं वाले जंगल में (जहाँ पेड़ कई बच्चों में विभाजित होते हैं), चीजें जटिल हो जाती हैं। इस शोध पत्र के लेखकों ने अंततः इस शाखाओं वाली दुनिया के लिए आदर्श रोबोट बनाए हैं।

रोबोटों के दो प्रकार

लेखकों ने केवल एक ही प्रकार का रोबोट नहीं बनाया; उन्होंने दो अलग-अलग प्रकार के रोबोट बनाए जो एक ही काम करते हैं, लेकिन बहुत अलग तरीकों से।

1. "आगे-पीछे" वाला रोबोट (Two-Way Linear HTA)

इस रोबोट को एक नक्शे के साथ हाइकर (पगडंडी पर चलने वाला) के रूप में सोचें।

यह कैसे चलता है: यह एक बच्चे के पेड़ की ओर आगे बढ़ सकता है, लेकिन यह अपने माता-पिता के पेड़ की ओर वापस भी देख सकता है। यह वंश वृक्ष (family tree) में ऊपर और नीचे जा सकता है।
यह कैसे सोचता है: यह बहुत सरल दिमाग वाला है। यह किसी भी समय केवल एक ही "मोड" में सोचता है (यह 'लीनियर' या रैखिक है)। यह एक साथ कई रास्तों के बारे में जटिल विचार नहीं रख सकता।
चुनौती: क्योंकि यह पीछे (अतीत) देख सकता है, इसलिए यह इतिहास को समझ सकता है। शोध पत्र दिखाता है कि यह रोबोट इतना शक्तिशाली है कि यह सब कुछ जाँच सकता है जो हमारी सख्त नियम-आधारित भाषा जाँच सकती है।

2. विशेष चश्मे वाला "एक-तरफा" रोबोट (Counter-Free Visible HTA)

इस रोबोट को एक गाइड के रूप में सोचें जो केवल आगे की ओर चलता है।

यह कैसे चलता है: यह केवल माता-पिता से बच्चे की ओर नीचे की ओर चल सकता है। यह पीछे नहीं देख सकता।
यह कैसे सोचता है: इसका दिमाग अधिक जटिल है। यह विभिन्न कार्यों को संभालने के लिए समूहों (घटकों) में विभाजित हो सकता है। हालाँकि, इसके दो सख्त नियम हैं:
- कोई लूप नहीं (No Loops): यह बार-बार एक ही चीज़ की जाँच करने के चक्र में नहीं फंस सकता (इसे "काउंटर-फ्री" कहा जाता है)।
- स्पष्ट दृष्टि (Visibility): जब यह कोई निर्णय लेता है, तो उसे पूरी तरह स्पष्ट होना चाहिए। यह अस्पष्ट नहीं हो सकता। यदि यह कहता है "बाएँ जाओ," तो इसे 100% सुनिश्चित होना चाहिए कि "बाएँ जाओ" का अर्थ एक विशिष्ट चीज़ है और "दाएँ जाओ" का ठीक उल्टा अर्थ है।
परिणाम: भले ही यह पीछे नहीं देख सकता, लेकिन स्पष्टता और गैर-दोहराव के बारे में इसके सख्त नियम इसे हमारी सख्त नियम-आधारित भाषा के समान ही चीज़ों की जाँच करने की अनुमति देते हैं।

"पोलराइजेशन" (Polarization) का रहस्य

इस शोध पत्र की सबसे दिलचस्प खोजों में से एक एक छिपा हुआ पैटर्न है जिसे पोलराइजेशन कहा जाता है।

कल्पना कीजिए कि जंगल में दो प्रकार के नियम हैं:

सुरक्षा नियम (Safety Rules): "कुछ भी बुरा कभी नहीं होता।" (जैसे, "कोई भी पेड़ कभी आग की चपेट में नहीं आता।")
सह-सुरक्षा नियम (Co-Safety Rules): "कुछ अच्छा अंततः होता है।" (जैसे, "एक फूल अंततः खिलेगा।")

लेखकों ने पाया कि सख्त नियम-आधारित भाषा (FO) में एक अजीब सीमा है:

यदि आप एक ऐसे पथ की तलाश कर रहे हैं जहाँ कुछ अच्छा होता है (existential), तो आप केवल सह-सुरक्षा गुणों (अच्छी चीजें अंततः होने) का वर्णन कर सकते हैं।
यदि आप एक ऐसे पथ की तलाश कर रहे हैं जहाँ कुछ बुरा नहीं होता (universal), तो आप केवल सुरक्षा गुणों (बुरी चीजें कभी न होने) का वर्णन कर सकते हैं।

आप उन्हें आसानी से मिला नहीं सकते। यह कहने जैसा है कि, "मैं केवल तभी वादा कर सकता हूँ कि एक अच्छी चीज़ होगी यदि मैं एक विशिष्ट पथ की तलाश कर रहा हूँ, लेकिन मैं केवल तभी वादा कर सकता हूँ कि एक बुरी चीज़ नहीं होगी यदि मैं सभी पथों की जाँच कर रहा हूँ।" शोध पत्र यह सिद्ध करता है कि यह केवल भाषा की एक खामी नहीं है; यह एक मौलिक नियम है कि ये नियम अनंत पेड़ों पर कैसे काम करते हैं।

यह क्यों महत्वपूर्ण है

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

अब, हमारे पास दो स्पष्ट ब्लूप्रिंट हैं:

हाइकर (Hiker): यदि आप इन नियमों की जाँच करना चाहते हैं, तो एक ऐसा रोबोट बनाएँ जो ऊपर-नीचे चल सके लेकिन अपने विचार सरल रखे।
गाइड (Tour Guide): यदि आप एक ऐसा रोबोट बनाना चाहते हैं जो केवल नीचे की ओर चले, तो सुनिश्चित करें कि वह कभी लूप में न फंसे और हमेशा स्पष्ट रूप से बोले।

यह कंप्यूटर वैज्ञानिकों को एक "नॉर्मल फॉर्म" देता है—इन नियमों को लिखने और उन्हें जाँचने वाली मशीनें बनाने का एक मानक, स्वच्छ तरीका। यह दो अलग-अलग भाषाओं के बीच एक आदर्श अनुवाद शब्दकोश खोजने जैसा है, जिससे हम बेहतर सॉफ्टवेयर सत्यापन उपकरण (verification tools) बना सकते हैं जो यह सिद्ध कर सकें कि जटिल प्रणालियाँ (जैसे ट्रैफिक लाइट या नेटवर्क प्रोटोकॉल) कभी क्रैश नहीं होंगी।

सारांश

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

यहाँ बेनेरेसेटी और अन्य द्वारा लिखित शोध पत्र "Automaton-Based Characterisations of First Order Logic Over Infinite Trees" का विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण (Problem Statement)

यह शोध पत्र अन्रैंक्ड (unranked), अनऑर्डर्ड (unordered), अनंत वृक्षों (infinite trees) पर प्रथम-क्रम तर्क (First-Order Logic - FO) की अभिव्यंजक शक्ति (expressive power) के लक्षण वर्णन की मौलिक समस्या को संबोधित करता है।

संदर्भ: जबकि रैखिक संरचनाओं (शब्दों) के लिए FO और ऑटोमेटा के बीच का संबंध अच्छी तरह से समझ में आता है, ब्रांचिंग-टाइम सेटिंग (वृक्ष) महत्वपूर्ण संरचनात्मक चुनौतियाँ प्रस्तुत करती है। थॉमस द्वारा 1980 के दशक में उठाया गया एक प्रमुख खुला प्रश्न यह है कि क्या यह तय किया जा सकता है कि दिया गया रेगुलर ट्री लैंग्वेज (regular tree language) FO-परिभाषित (FO-definable) है या नहीं।
अंतराल (Gap): मौजूदा बीजगणितीय दृष्टिकोणों (जैसे कि सिंटैक्टिक बीजगणित का उपयोग करके) ने केवल आंशिक परिणाम दिए हैं, जो मुख्य रूप से परिमित वृक्षों या विशिष्ट टोपोलॉजिकल वर्गों तक सीमित हैं। अनंत वृक्षों पर FO के लिए एक पूर्ण, एकसमान ऑटोमेटा-आधारित लक्षण वर्णन का अभाव है जो मोनैडिक सेकंड-ऑर्डर लॉजिक (MSO) पर निर्भर हुए बिना इसकी पूर्ण अभिव्यंजक शक्ति को पकड़ सके।
लक्ष्य: हेज़िटेंट ट्री ऑटोमेटा (hesitant tree automata) के विशिष्ट वर्गों का उपयोग करके अनंत वृक्षों पर FO के सुदृढ़ लक्षण वर्णन प्रदान करना और अनंत वृक्षों पर FO की सटीक संरचनात्मक सीमाओं की पहचान करना।

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

लेखक तर्क (logic), ऑटोमेटा सिद्धांत और मॉडल थ्योरी को संयोजित करने वाला एक बहुआयामी दृष्टिकोण अपनाते हैं:

तार्किक तुल्यता (Logical Equivalence): लेखक ज्ञात परिणामों पर निर्माण करते हैं जो यह स्थापित करते हैं कि अनंत वृक्षों पर FO, दो विशिष्ट ब्रांचिंग-टाइम टेम्पोरल लॉजिक के साथ अभिव्यंजक रूप से समतुल्य है:
- PastCTL $^\pm$ : काउंटिंग मोडालिटीज (counting modalities) वाले पास्ट ऑपरेटर्स वाला CTL का एक खंड।
- CTL $^*_f$ : फिनिट पाथ क्वांटिफिकेशन (finite path quantification) तक सीमित पूर्ण कम्प्यूटेशन ट्री लॉजिक (Full Computation Tree Logic)।
ऑटोमेटा वर्ग (Automaton Classes): वे हेज़िटेंट ट्री ऑटोमेटा (HTA) के दो विशिष्ट वर्गों को पेश करते हैं और उनका विश्लेषण करते हैं:
- Two-Way Linear Polarised Hesitant Tree Automata (2W-L-HTA $^\pm$ ): ये ऑटोमेटा हेड को ऊपर (पैरेंट की ओर) और नीचे (चिल्ड्रन की ओर) जाने की अनुमति देते हैं। "लीनियर" प्रतिबंध यह आवश्यक बनाता है कि स्टेट स्पेस को सिंगलटन कंपोनेंट्स में विभाजित किया जाए।
- Counter-Free Visible Polarised Hesitant Tree Automata (CF-V-HTA $^\pm$ ): ये वन-वे (one-way) ऑटोमेटा हैं। वे दो प्रमुख प्रतिबंध लागू करते हैं:
  - काउंटर-फ्रीनेस (Counter-freeness): प्रत्येक कंपोनेंट का लीनियराइजेशन (जिसे $\omega$ -वर्ड ऑटोमेटा के रूप में देखा जाता है) काउंटर-फ्री (एपीरियॉडिक) होना चाहिए।
  - विजिबिलिटी (Visibility): एक सिमेंटिक स्थिति जो यह सुनिश्चित करती है कि ट्रांजिशन में उपयोग किए जाने वाले एनोटेशन (सब-फॉर्मूला को दर्शाने वाले सेट) परस्पर अनन्य (mutually exclusive) हैं ताकि "छिपे हुए" काउंटिंग व्यवहार को रोका जा सके।
पोलराइजेशन विश्लेषण (Polarization Analysis): लेखक एक "पोलराइजेशन" गुण की जांच करते हैं जहाँ अस्तित्वगत पाथ क्वांटिफायर (existential path quantifiers) को को-सेफ्टी (co-safety) गुणों तक और सार्वभौमिक पाथ क्वांटिफायर (universal path quantifiers) को सेफ्टी (safety) गुणों तक सीमित किया जाता है। वे दिखाते हैं कि यह वृक्षों पर FO का एक मौलिक सिमेंटिक फीचर है।
अनुवाद और सामान्यीकरण (Translation and Normalization): वे तार्किक औपचारिकताओं (logical formalisms) और ऑटोमेटा के बीच प्रभावी अनुवाद का निर्माण करते हैं, और CTL $^*$ के लिए एक नया नॉर्मल फॉर्म (जिसे CTL $^*_\pm$ कहा जाता है) प्राप्त करते हैं जो सिंटैक्टिक रूप से पोलराइजेशन गुण को लागू करता है।

3. प्रमुख योगदान (Key Contributions)

A. नए ऑटोमेटा लक्षण वर्णन (New Automaton Characterizations)

यह शोध पत्र अनंत वृक्षों पर FO के पहले पूर्ण ऑटोमेटा-आधारित लक्षण वर्णन प्रदान करता है:

Theorem 5.1 & 5.2: Two-Way Linear HTA $^\pm$ (जो PastCTL $^\pm$ (और इस प्रकार FO) के अभिव्यंजक रूप से समतुल्य हैं) आश्चर्यजनक हैं क्योंकि शब्दों पर FO को वन-वे अल्टरनेटिंग ऑटोमेटा द्वारा वर्णित किया जाता है, जबकि पूर्ण अभिव्यक्ति प्राप्त करने के लिए वृक्षों पर टू-वे (two-way) मूवमेंट की आवश्यकता होती है, भले ही इसमें गंभीर "लीनियर" (सिंगलटन कंपोनेंट) प्रतिबंध हो।
Theorem 7.4 & 7.5: Counter-Free Visible HTA $^\pm$ (जो CTL $^*_f$ (और इस प्रकार FO) के अभिव्यंजक रूप से समतुल्य हैं) एक ही प्रकार की शक्ति प्राप्त करते हैं, लेकिन इसके लिए जटिल "विजिबिलिटी" और "काउंटर-फ्री" बाधाओं की आवश्यकता होती है।

B. तार्किक नॉर्मल फॉर्म और पोलराइजेशन (Logical Normal Forms and Polarization)

CTL $^*_\pm$ : लेखक CTL $^*$ के एक नए सिंटैक्टिक खंड को CTL $^*_\pm$ कहते हैं। वे सिद्ध करते हैं कि CTL $^*_f$ (जो फिनिट पाथ तक सिमेंटिक रूप से सीमित है) इस सिंटैक्टिक खंड के समतुल्य है।
पोलराइजेशन गुण (Polarization Property): वे प्रदर्शित करते हैं कि वृक्षों पर FO फॉर्मूला एक सख्त पोलराइजेशन प्रदर्शित करते हैं:
- अस्तित्वगत (Existential) पाथ क्वांटिफिकेशन वाले फॉर्मूला केवल को-सेफ्टी गुण व्यक्त कर सकते हैं (ऐसे गुण जहाँ उल्लंघन एक परिमित प्रीफिक्स द्वारा प्रमाणित होता है)।
- सार्वभौमिक (Universal) पाथ क्वांटिफिकेशन वाले फॉर्मूला केवल सेफ्टी गुण व्यक्त कर सकते हैं (ऐसे गुण जहाँ उल्लंघन एक परिमित प्रीफिक्स द्वारा प्रमाणित होता है, लेकिन यदि कोई उल्लंघन नहीं होता है तो गुण बना रहता है)।
- यह एक स्पष्ट सीमा को प्रकट करता है: FO एक एकल ब्रांच के साथ सेफ्टी और को-सेफ्टी को गैर-पोलराइज्ड तरीके से मिलाने वाले गुणों को परिभाषित नहीं कर सकता है।

C. लीनियर-टाइम परिणाम (Linear-Time Results)

एक सह-योगदान के रूप में, शोध पत्र लीनियर टेम्पोरल लॉजिक (LTL) के सेफ्टी और को-सेफ्टी खंडों के लिए प्रत्यक्ष ऑटोमेटा-आधारित लक्षण वर्णन प्रदान करता है:

SafeLTL, Counter-free Looping Universal Büchi Automata (UBA) के समतुल्य है।
coSafeLTL, Counter-free Looping Nondeterministic co-Büchi Automata (NCA) के समतुल्य है।
यह वृक्ष परिणामों के लिए एक आधारभूत एनालॉग के रूप में कार्य करता है।

4. मुख्य परिणाम (Key Results)

तुल्यता श्रृंखला (Equivalence Chain):
$\text{FO} \equiv \text{PastCTL}^\pm \equiv \text{CTL}^*_f \equiv \text{CTL}^*_\pm \equiv \text{2W-L-HTA}^\pm \equiv \text{CF-V-HTA}^\pm$
यह तर्क, इसके टेम्पोरल वेरिएंट और दो अलग-अलग ऑटोमेटा वर्गों के बीच पूर्ण पारस्परिक तुल्यता स्थापित करता है।
टू-वे बनाम वन-वे (Two-Way vs. One-Way):
- Two-Way Linear HTA $^\pm$ (सिंगलटन कंपोनेंट्स के साथ) Linear HTA $^\pm$ (वन-वे) की तुलना में काफी अधिक अभिव्यंजक हैं। वृक्षों पर FO को कैप्चर करने के लिए टू-वे क्षमता आवश्यक है, जब कंपोनेंट्स को सिंगलटन तक सीमित किया जाता है।
- Counter-Free Visible HTA $^\pm$ (वन-वे) समान शक्ति प्राप्त करते हैं, लेकिन इसके लिए जटिल आंतरिक संरचनाओं (कंपोनेंट्स जो काउंटर-फ्री वर्ड ऑटोमेटा के रूप में कार्य करते हैं) और विजिबिलिटी प्रतिबंध की आवश्यकता होती है।
अभिव्यंजक सीमा (Expressive Limitation): पोलराइजेशन परिणाम यह दर्शाता है कि FO अनंत वृक्षों पर उन गुणों को परिभाषित नहीं कर सकता है जिनमें पोलराइजेशन प्रतिबंध का उल्लंघन किए बिना एक ब्रांच के साथ सेफ्टी और को-सेफ्टी को "मिक्स" करने की आवश्यकता होती है। उदाहरण के लिए, यह ऐसे गुणों को परिभाषित नहीं कर सकता है जिनमें एक विशिष्ट संरचनात्मक अलगाव के बिना एक साथ सुरक्षा स्थिति और को-सेफ्टी स्थिति की जाँच करने की आवश्यकता होती है।

5. महत्व और निहितार्थ (Significance and Implications)

परिभाषा संबंधी प्रश्नों का समाधान (Resolution of Definability Questions): हालांकि रेगुलर ट्री लैंग्वेजेस के लिए FO-डेफिनेबिलिटी की सामान्य निर्णय क्षमता (decidability) अभी भी खुली है, यह कार्य विशिष्ट भाषाओं के लिए डेफिनेबिलिटी का विश्लेषण करने के लिए एक ठोस, ऑटोमेटा-आधारित ढांचा प्रदान करता है।
FO संरचना की समझ (Understanding FO Structure): ये परिणाम गहराई से समझाते हैं कि वृक्षों पर FO, शब्दों की तुलना में क्यों "व्यवहारहीन" या अप्रत्याशित है। लीनियर ऑटोमेटा मॉडल में टू-वे मूवमेंट की आवश्यकता वृक्ष संरचनाओं के भीतर प्रथम-क्रम बाधाओं के साथ नेविगेट करने की जटिलता को उजागर करती है।
MSO खंडों के साथ सेतु (Bridge to MSO Fragments): यह शोध पत्र FO को Weak Chain Logic (WCL) और Modal $\mu$ -calculus से जोड़ता है, जिससे पता चलता है कि FO में देखा गया पोलराइजेशन घटना WCL में भी दिखाई देता है। यह एक ऐसी अभिव्यंजक पदानुक्रम (hierarchy) का सुझाव देता है जहाँ FO, Monadic Path Logic (MPL) और CTL $^*$ से स्पष्ट रूप से नीचे है।
भविष्य की दिशाएं (Future Directions): लेखक पहचानते हैं कि इन परिणामों को परिमित वृक्षों (finite trees) तक विस्तारित करना एक बड़ी चुनौती बनी हुई है, विशेष रूप से नियत (deterministic) ट्री ऑटोमेटा के लिए अपघटन प्रमेय (decomposition theorem) की कमी के कारण (शब्दों के लिए Krohn-Rhodes प्रमेय के विपरीत)। वे टू-वे लीनियर और वन-वे विज़िबल ऑटोमेटा मॉडलों के बीच सीधा अनुवाद खोजने का खुला प्रश्न भी रखते हैं, जो गहरे संरचनात्मक अंतर्दृष्टि प्रदान करेगा।

संक्षेप में, यह शोध पत्र नवीन ऑटोमेटा वर्गों को पेश करके और ब्रांचिंग-टाइम संरचनाओं में निहित एक मौलिक "पोलराइजेशन" बाधा को प्रकट करके, अनंत वृक्षों पर फर्स्ट-ऑर्डर लॉजिक और ऑटोमेटा सिद्धांत के बीच के अंतर को सफलतापूर्वक पाटता है।