नियमित हैकेल बीजगणितीय डेटा प्रकार संदर्भ मुक्त व्याकरण के बराबर हैं? GADTS के बारे में क्या?

Question

बीजगणित डेटा प्रकारों के लिए वाक्यविन्यास Backus–Naur Form के सिंटैक्स के समान है, जिसका उपयोग संदर्भ मुक्त व्याकरण का वर्णन करने के लिए किया जाता है। मुझे लगता है कि अगर हम किसी भाषा के लिए पार्सर के रूप में हास्केल प्रकार चेकर के बारे में सोचते हैं, तो बीजगणितीय डेटा प्रकार (उदाहरण के लिए टर्मिनल प्रतीकों का प्रतिनिधित्व करने वाले न्युलरी प्रकार के रचनाकार) के रूप में प्रतिनिधित्व किया जाता है, तो सभी भाषाओं का सेट स्वीकार किया जाता है संदर्भ मुक्त भाषाओं का सेट? साथ ही, इस व्याख्या के साथ, औपचारिक भाषाओं का कौन सा सेट जीएडीटी स्वीकार कर सकता है?

Answer 1

सबसे पहले, डेटा प्रकार हमेशा तारों के सेट का वर्णन नहीं करते हैं (यानी, एक भाषा)। यही है, जबकि एक सूची प्रकार करता है, एक पेड़ प्रकार नहीं करता है। कोई इसका सामना कर सकता है कि हम पेड़ों को सूचियों में "फटकार" सकते हैं और उनकी भाषा के रूप में सोच सकते हैं। फिर भी, क्या

data F = F Int (Int -> Int) 

या की तरह डेटा प्रकार, बदतर

data R = R (R -> Int) 

के बारे में?

बहुपद प्रकार (-> के बिना प्रकार) लगभग पेड़ों का वर्णन करते हैं, जिन्हें चपटा (इन-ऑर्डर का दौरा किया जा सकता है), तो चलिए उन्हें उदाहरण के रूप में उपयोग करते हैं। जब से तुम प्रत्यावर्तन दोहन कर सकते हैं

data A = A1 Int A | A2 Int B 
data B = B1 Int B Char | B2 

A ऊपर

व्यक्त करता { Int^m Char^n | m>n }

आप महसूस किया होगा, एक CFG एक (बहुपद) प्रकार के रूप में लेखन, आसान है।

जीएडीटी संदर्भ-मुक्त भाषाओं से काफी दूर है।

data Z 
data S n 

data ListN a n where 
    L1 :: ListN a Z 
    L2 :: a -> ListN a n -> ListN a (S n) 

data A 
data B 
data C 

data ABC where 
    ABC :: ListN A n -> ListN B n -> ListN C n -> ABC 

ABC ऊपर

(चपटा) भाषा A^n B^n C^n, जो विषय से मुक्त नहीं है व्यक्त करता है।

आप जीएडीटी के साथ बहुत अधिक अप्रतिबंधित हैं, क्योंकि उनके साथ अंकगणित एन्कोड करना आसान है। यह है कि आप एक प्रकार Plus a b c बना सकते हैं जो पीनो स्वाभाविक के साथ गैर-खाली iff c=a+b है। आप एक प्रकार Halt n m भी बना सकते हैं जो ट्यूरिंग मशीन m इनपुट m पर रोकता है, तो गैर-खाली iff है। तो, आप एक भाषा

{ A^n B^m proof | n halts on m , and proof proves it } 

जो रिकर्सिव (और किसी भी सरल वर्ग में, मोटे तौर पर नहीं) बना सकते हैं।

फिलहाल, मुझे नहीं पता कि आप जीएडीटी में पुनरावर्ती संख्यात्मक (संगणनीय रूप से गणना करने योग्य) भाषाओं का वर्णन कर सकते हैं या नहीं। यहां तक ​​कि रोकथाम की समस्या उदाहरण में, मुझे इसे काम करने के लिए जीएडीटी के अंदर "सबूत" शब्द शामिल करना होगा।

Intuitively, अगर आप लंबाई n के एक स्ट्रिंग है और आप इसे एक एक GADT के खिलाफ जांच करना चाहते हैं, तो आप गहराई n के सभी GADT शर्तों, निर्माण उन्हें समतल, और फिर स्ट्रिंग के लिए तुलना कर सकते हैं। यह साबित करना चाहिए कि ऐसी भाषा हमेशा रिकर्सिव होती है। हालांकि, अस्तित्व के प्रकार इस पेड़ की इमारत दृष्टिकोण काफी मुश्किल बनाते हैं, इसलिए मेरे पास अभी एक निश्चित उत्तर नहीं है।